mc-imperial / spirv-control-flow

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

HeaderBlockStrictlyDominatesItsMergeBlock #51

Open vili-1 opened 2 years ago

vili-1 commented 2 years ago

After switching everything to structured-dominance, this shader is not accepted by our model due to the rule:

/**
  *  "..each header block must strictly dominate its merge block, unless the merge block
  *   is unreachable in the CFG"
  *   (The Khronos Group, 2021, p.29)
  *   https://www.khronos.org/registry/spir-v/specs/unified1/SPIRV.pdf
  */

167

because %13 actually is not structured-dominated by %15 due to edge (%11, %13)

@afd is this a 'good' cfg?

afd commented 2 years ago

I took a look at this example that this came from, and made two different but related SPIR-V shaders from it.

Example 1:

               OpCapability Shader
          %1 = OpExtInstImport "GLSL.std.450"
               OpMemoryModel Logical GLSL450
               OpEntryPoint Fragment %10 "main"
               OpExecutionMode %10 OriginUpperLeft
               OpSource ESSL 310
          %2 = OpTypeVoid
          %3 = OpTypeFunction %2
         %14 = OpTypeBool
         %64 = OpConstantTrue %14
         %10 = OpFunction %2 None %3
         %11 = OpLabel
           OpBranch %23
         %23 = OpLabel
               OpLoopMerge %25 %34 None
               OpBranchConditional %64 %32 %25
         %32 = OpLabel
               OpLoopMerge %34 %35 None
               OpBranchConditional %64 %33 %35
         %33 = OpLabel
               OpReturn
         %35 = OpLabel
               OpBranch %32
         %34 = OpLabel
               OpBranch %23
         %25 = OpLabel
           OpReturn
               OpFunctionEnd

Here is its CFG:

image

Example 2:

               OpCapability Shader
          %1 = OpExtInstImport "GLSL.std.450"
               OpMemoryModel Logical GLSL450
               OpEntryPoint Fragment %10 "main"
               OpExecutionMode %10 OriginUpperLeft
               OpSource ESSL 310
          %2 = OpTypeVoid
          %3 = OpTypeFunction %2
         %14 = OpTypeBool
         %64 = OpConstantTrue %14
         %10 = OpFunction %2 None %3
         %11 = OpLabel
           OpBranch %23
         %23 = OpLabel
               OpLoopMerge %25 %34 None
               OpBranchConditional %64 %32 %25
         %32 = OpLabel
               OpLoopMerge %34 %35 None
               OpBranchConditional %64 %33 %35
         %33 = OpLabel
               OpBranch %34
         %35 = OpLabel
               OpBranch %32
         %34 = OpLabel
               OpBranch %23
         %25 = OpLabel
           OpReturn
               OpFunctionEnd

Here is its CFG:

image

These examples are the same as each other, except for block %33. In the first example, %33 has a return instruction, while in the second instruction %33 branches to %34, which is the merge block of the loop headed by %32, and also the continue target of the loop headed by %23.

According to spirv-val, example 1 (which is like your example above, @vili-1, but a bit simpler) is valid, but example 2 is invalid.

For example 2, the validator complains:

"Header block 32[%32] is contained in the loop construct headed by 23[%23], but its merge block 34[%34] is not"

I feel like the same complaint should apply to example 1.

I think that according to our model, both examples should be invalid, due to structured dominance, and I think that's a good thing.

Let me know what you reckon, @vili-1.

afd commented 2 years ago

@johnwickerson it would be good if you could take a careful look at this too, thanks.

vili-1 commented 2 years ago

@afd so you are saying to apply structured-dominance holistically, right?. My concern is how do we sell that Example 1 (and the CTS example of this issue) are invalid.

afd commented 2 years ago

Yes, that's what I'm suggesting.

And I think we argue those examples are invalid because they exhibit construct B nested inside construct A, but with the merge block of B not belonging to A.

That's what the validator complains about for example 2, and it seems reasonable that the same complaint should apply to example 1.

Do you see what I mean about the examples being essentially the same, except that in example 1 there's a return from the inner construct and in example 2 there's a break?

vili-1 commented 2 years ago

Ok, agree.

vili-1 commented 2 years ago

This top example is one of the three CTS examples our model rejects