mc-imperial / spirv-control-flow

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

Pushing a set of samples at https://github.com/dneto0/spirv-samples through our tooling #38

Open vili-1 opened 2 years ago

vili-1 commented 2 years ago

Out of 243 examples (these are the interesting ones having names starting with "SpvParserCFGTest"), the 9 cases below are deemed infeasible.

  1. Blocks not structurally-reachable. This, this, this and this have blocks which are structurally unreachable. jump (0)

  2. This and this one is rejected due to the constraint MultipleOutedges which says that "if a non-header block 'b' has multiple successors then 'b' must be a break block or a continue one".....Later we augmented the rule to: "A non-header block B can have 2 successors, C and D, if at least one of the edges B->C and B->D is an exit edge." Pasted Graphic 5

    selectionHeader
  3. Here, here and here there are two backedges branching to a loop header. LoopHeader