search

mc-imperial / spirv-control-flow

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

Branch to continue target #29

Open vili-1 opened 2 years ago

vili-1 commented 2 years ago

@afd the attached example is rejected by Alloy because of the rule:

  • for a loop construct that is not a single block loop, if there is a branch edge from a block 'B' to the loop's continue target, then 'B' must belong to the loop construct

Here, edge 12 does not belong to the loop construct. SPIRV-VAL acceppts it. Do you see anything wrong with this example?

noExit

afd commented 2 years ago

Very interesting!

This example looks bogus to me, because of a path like 8, 9, 10, 14, 17, 11, 9. The edge from 9 to 10 exits the loop, and indeed 12 is not part of the loop, so the edge from 12 to 11 allows getting into the loop's continue from outside the loop.

Thus, I think spirv-val is wrong.

Can the example be simplified? E.g. can the construct headed at 10 be collapsed to a single block?

vili-1 commented 2 years ago

Here's a simplified version.

noExitSimpl

This example came up as I was asking Alloy to generate examples without exit blocks (terminals) but none was found by Alloy. Then, I realised that by disabling the rule above Alloy could generate examples without exit blocks (like the one here). Can you think of any example with no exit blocks?

afd commented 2 years ago

Fascinating: indeed, I think it's the case that with our rules it's impossible to have an example without a structurally reachable exit block.

Suppose a control flow graph has no structurally-reachable exit blocks. Then every structurally reachable block must be contained in some loop (we can't follow a chain of edges forever without hitting an exit unless we're in a loop). Then consider the outermost structurally-reachable loop. Its merge block is structurally reachable, but is not contained in any loop. Contradiction!

This is great. And I think you've indeed found a bug in spirv-val - can you file it, using the simple example?

(Of course: we can have CFGs where no exit block is reachable by control flow edges, so we still need the notion of "doomed" blocks in fleshing.)

@Jack-Clark and @johnwickerson for info.

vili-1 commented 2 years ago

We shared this with Alan (https://docs.google.com/document/d/1B2AEGChk4VgOzjWwScb1Hc580WP_nWu1ONcpOpLB0ig/edit) and Alan acknowledged that there was a bug in spirv-val (email 5 Apr)