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

Strange error from spirv-val about back-edges #34

Open vili-1 opened 2 years ago

vili-1 commented 2 years ago

The example attached is generated by Alloy as a valid one. spirv-val says:

error: line 17: Back-edges (9[%9] -> 14[%14]) can only be formed between a block and a loop header.
  %9 = OpLabel

Looks like spirv-val is confused due to the unreachabe isle on the right. I guess, the reason has to do with building the DF spanning tree and picking the node 14 as start node of the isle; it cnsiders 14->9 as a forward edge. What do you think @afd?

cfg_1

Archive 2.zip

Simplified: issue25_1_simple

Archive 2.zip

vili-1 commented 2 years ago

Same error here:

error: line 17: Back-edges (9[%9] -> 12[%12]) can only be formed between a block and a loop header.
  %9 = OpLabel

cfg_1 Archive 3.zip

afd commented 2 years ago

What's weird about these examples is that the edge spirv-val mentions doesn't exist! There is no regular control flow edge 9->12 in the above example, for instance.

I believe these examples should be considered valid, and hopefully if in the future spirv-val adopts structural dominance and does its checking using structural dominance they will indeed be considered valid by the tool.

vili-1 commented 2 years ago

The new spirv-val (which adopts structural dominance and does its checking using structural dominance) does validate now the examples above.