mc-imperial / spirv-control-flow

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

Merge Block and Continue Target must be different ids #52

Open vili-1 opened 2 years ago

vili-1 commented 2 years ago

The shader attached was randomly generated conforming to all SPIR-V rules with structured-reachablity/dominance encoded.

image Merge_Block_and_Continue_Target_must_be_different_ids.zip

The validator however returns:

error: line 19: Merge Block and Continue Target must be different ids OpLoopMerge %12 %12 None

..complaining that the 'merge' and 'continue' edges from block 11 are converging to block 12.

@afd , structured-reachability here hides the problem: without structured-dominance the graph would not have been deemed infeasible; do you agree? Then, we have to use the 'original' reachability/dominance for this case, i.e., for the rule "each header block must strictly dominate its merge block, unless the merge block is unreachable in the CFG"

But I think there is no rule in the specs talking about "Merge Block and Continue Target must be different ids", so we can use this finding to claim an underspecification.