mc-imperial / spirv-control-flow

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

Should OpSwitch be allowed in a non-header node? #45

Open afd opened 3 years ago

afd commented 3 years ago

Spec version: Version 1.5, Revision 5, Unified January 7, 2021

In relation to switch, the spec says (2.11, page 29):

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)

It also says:

a branch to an outer OpSwitch merge block is ...

However, the spec does not say what the merge block associated with an OpSwitch instruction is.

If OpSwitch were required to only appear as the terminator of a header block then the merge block could be defined to be the merge associated with the header block.

However, spirv-val accepts fragments of SPIR-V like this one:

               OpCapability Shader
          %1 = OpExtInstImport "GLSL.std.450"
               OpMemoryModel Logical GLSL450
               OpEntryPoint Fragment %4 "main"
               OpExecutionMode %4 OriginUpperLeft
               OpSource ESSL 320
          %2 = OpTypeVoid
          %3 = OpTypeFunction %2
         %10 = OpTypeBool
         %11 = OpConstantTrue %10
         %19 = OpTypeInt 32 0
         %20 = OpUndef %19
          %4 = OpFunction %2 None %3
          %5 = OpLabel
               OpBranch %6
          %6 = OpLabel
               OpLoopMerge %8 %9 None
               OpBranch %7
          %7 = OpLabel
               OpSwitch %20 %8 0 %21 1 %22
         %21 = OpLabel
               OpBranch %22
         %22 = OpLabel
               OpBranch %9
          %9 = OpLabel
               OpBranch %6
          %8 = OpLabel
               OpReturn
               OpFunctionEnd

Block %7 end with OpSwitch, but it is not a header block.

The CFG looks like this:

image

You can see that node 7 ends with OpSwitch because it has 3 outgoing edges.