mc-imperial / spirv-control-flow

Formal modelling of SPIR-V control flow using Alloy
Apache License 2.0
2 stars 0 forks source link

OpSwitchBlockDominatesAllItsCases #37

Open vili-1 opened 2 years ago

vili-1 commented 2 years ago

In this example the OpSwitch %21 does not structurally dominate its case %20. s045

afd commented 2 years ago

This is a very interesting example!

The edge 21->20 goes directly from the header of a switch construct to the continue target of a loop that encloses the switch construct.

The current SPIR-V specification says:

a case construct: the blocks dominated by an OpSwitch Target or Default (this construct is only defined for those OpSwitch Target or Default that are not equal to the OpSwitch’s corresponding merge block)

According to this definition, block 20 is indeed a case construct, and if 20 dominated more blocks (which it doesn't here), these would be part of the case construct.

That seems wrong, because the branch 21->20 is an "early continue" branch.

I think the spec should be adapted to say:

a case construct: the blocks dominated by an OpSwitch Target or Default (this construct is only defined for those OpSwitch Target or Default that are not equal to the OpSwitch’s corresponding merge block, and that are not equal to the merge or continue block of a loop containing the OpSwitch instruction)

Or something along those lines.

If we added that language, 20 would no longer be a case construct and the problem would go away.

What do you think, @vili-1 ?