Add rule to model to avoid conditional branch on loop header that does not target a merge or continue

[afd]

This spirv-val PR relates to this rule in the spec:

Selections must be structured. That is, an OpSelectionMerge instruction is required to precede:

an OpSwitch instruction

an OpBranchConditional instruction that has different True Label and False Label operands where neither are declared merge blocks or Continue Targets.

It appears that we do not have a corresponding rule for this.

I think we need a rule to require the following:

• If B is a loop header and B has two successors then at least one of the successors must be the loop merge block or the loop continue target

Another way of stating this:

• If B is a loop header and B has successors C and D then at least one of the following must hold:

  • C is the merge block for the loop
  • C is the continue target for the loop
  • D is the merge block for the loop
  • D is the continue target for the loop

[afd]

@vili-1 would you be able to look into adding this, and check that it doesn't lead to any good examples being rejected?

[vili-1]

@afd I modelled this (and the test case is rejected now of course). I laso checked again most of the CFGs extracted from VK-GL-CTS and no surprises.

[afd]

Great - once we're fully confident that we want this new rule, can you commit it to the model and close this issue? Thanks.