mc-imperial / spirv-control-flow

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

Structural semantics is stronger #32

Open vili-1 opened 2 years ago

vili-1 commented 2 years ago

For this example, spirv-val says:

error: line 21: block <ID> 12 branches to the selection construct, but not to the selection header <ID> 11
  %12 = OpLabel

This is due to the fact that the semantics of structural dominance is more restrictive: in spirv-val semantics block 9 is member of selection headed by 11 but in structural semantics it's not because %9 is not structurally dominated by %11

cfg_1 Archive 4.zip

afd commented 2 years ago

Nice example!

I think this is acceptable.

Could you find the simplest possible example that illustrates this phenomenon and add it to the structural dominance doc?

Thanks

vili-1 commented 2 years ago

While trying to simplify the example above, I noticed something strange. Just take a look at the graphs below: for the first one spirv-val is complaining that %11 branches to the selection construct, but not to the selection header %10. Firstly, node 9 (where 11 is branching to) is not part of the selection headed at 10 because it is dominated by an outer constructs’ merge blocks. Am I right? The spec by the way is not crystal clear when the outer is a switch/case. But even if we take for granted what spirv-val says, that %11 branches to the selection construct, why if we remove the node 12 the graph is then accepted by spirv-val?

rejected

Archive.zip

accepted Archive 2.zip

afd commented 2 years ago

To me this seems like a bug in spirv-val - I don't think there is anything wrong with the example that spirv-val rejects. It would be good to include this in the doc under the "synthetic" section.

vili-1 commented 2 years ago

Alan acknowledged that spirv-val should accept the example above (email 5 Apr). This is one of the mismatches here: https://docs.google.com/document/d/1B2AEGChk4VgOzjWwScb1Hc580WP_nWu1ONcpOpLB0ig/edit