Breaks from nested conditionals

[afd]

The following shader has two nested conditionals, and the body of the inner conditional breaks directly to the merge of the outer conditional:

               OpCapability Shader
          %1 = OpExtInstImport "GLSL.std.450"
               OpMemoryModel Logical GLSL450
               OpEntryPoint Fragment %4 "main"
               OpExecutionMode %4 OriginUpperLeft
               OpSource ESSL 320
               OpName %4 "main"
          %2 = OpTypeVoid
          %3 = OpTypeFunction %2
          %6 = OpTypeBool
          %7 = OpConstantTrue %6
          %4 = OpFunction %2 None %3
          %5 = OpLabel
               OpSelectionMerge %9 None
               OpBranchConditional %7 %8 %9
          %8 = OpLabel
               OpSelectionMerge %11 None
               OpBranchConditional %7 %10 %11
         %10 = OpLabel
               OpBranch %9
         %11 = OpLabel
               OpBranch %9
          %9 = OpLabel
               OpReturn
               OpFunctionEnd

Here is the CFG:

The edge 10->9 is the edge that breaks from inside the inner conditional to the merge of the outer conditional.

spirv-val rejects this example with:

error: line 19: block <ID> 10[%10] exits the selection headed by <ID> 8[%8], but not via a structured exit

I'm fairly sure it is intended that this is disallowed, but I cannot find wording in the spec that actually disallows it.

@vili-1 Does our model allow or disallow it?

Here is the .als file.

[vili-1]

Our model allows this. I can't match a rule fom the specs to explicitely disallow this. There is a rule saying that "all branches into a construct from reachable blocks outside the construct must be to the header block" - but block 9 is not member of any construct because merge blocks are excluded from selection constructs by definition.

[vili-1]

We defined a new rule about exiting the construct and then our model disallows this example