afd
commented
3 years ago Interesting example! Nothing gets past Alloy :)
Yes: the issue here is that 14 is technically a break block, because of the edge 14->16 and because 16 is a loop merge (by the same logic, 14 is also a continue block). But the block 16 is one of those weird single-block loops.
Now that we have rules for exits, I think we can replace our rule that allows a non-header to have multiple successors only under certain conditions with the following rule:
- A non-header block B must have 0 or 1 successor, with one exception. A non-header block can have 2 successors, C and D, if at least one of the edges B->C and B->D is an exit edge.
By this, I mean that B is in some construct, and at least one of the edges B->C, B->D leaves the construct according to the various legal rules for structured exits that we have been discussing.
That would exclude this example, because neither 14->15 nor 14->16 is an exit edge.
How does that sound? Could you try modelling it?
This is generated as valid by Alloy; the spirv-val says:
We have a rule which allows %14 to have multiple successors if %14 is a continue block. In the spec the definition of continue block is:
So we our model is in line with this definition, but I guess the intention in the spec is that the loop construct in question should contain the continue block; what do you think @afd
Archive.zip