Post-dominance without exit blocks

[vili-1]

Our Alloy model generated the valid example attached. SPIRV-VAL however rejects it with the cause:

error: line 31: The continue construct with the continue target 13[%13] is not post dominated by the back-edge block 14[%14]
  %14 = OpLabel

But here there are no exit blocks (function-return instructions). Looks like SPIRV-VAL “believes” that block 15 is an exit! @afd What do you think should happen with post-dominance if there are no exit blocks?

!BackEdgePostDominatesContinueTarget.zip

[afd]

Sorry it took me a while to get to this. Very interesting!

By the strict definition, if there are no exit blocks then I think B post dominates A holds for all blocks A and B (because there are no paths from A to an exit block, so all 0 of them pass through B.)

However, the example looks intuitively wrong, because of the edge from 14 to 15. 14 is the merge block for the loop headed at 13, and 15 is the continue target, so it seems very undesirable for there to be a branch from the merge block to the continue target. Do you see what I mean?

Is it possible to come up with an even simpler example that exposes this issue?

[vili-1]

Here's a simpler example: yet SPIRV-VAL says:

error: line 22: The continue construct with the continue target 11[%11] is not post dominated by the back-edge block 12[%12]
  %12 = OpLabel

Now, the edge 12->13 by definition is not an exit, right? (because 13 is contained in the innermost construct containing 12. Haven't figured out though what constraint should rule out a merge->continue edge here, but will keep thinking..

[afd]

Can we please try two alternative graphs:

(1) The same as the above graph, but eliminating nodes 9 and 10, so that 8 branches straight to 11, and there is no edge 12->9

(2) The same as (1), but with an extra node 14, which is an exit node, and an edge 12-14.

It would be great to know which (if either) of these is valid according to our model.

[vili-1]

Alternative 1: Alloy model is happy; spirv-val is happy, too.

Archive 3.zip

Alternative 2: Alloy reject this (because of 2 edges 10->11 and 10->12 leaving away from 10), but spirv-val accepts it.
We have a rule in our model which says:
A non-header Block B can have 2 successors, C and D, if at least one of the edges B->C and B->D is an exit edge
where exit edge is defined as an edge exiting a construct

issue28simple2.zip

[vili-1]

The Alternative 2 violates the rule:

Let B be a continue target; suppose that B is not a loop header and let A->B a control flow edge. Then A is part of the loop associated with B.

The "original" spirv-val accepts Alternative 2 above (bug); the new spirv-val however rejects it.