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

Discrepancy between model/spec and validator regarding OpSwitch targets #39

Open afd opened 2 years ago

afd commented 2 years ago

This example:

case.txt

gives this control flow graph:

image

The assembly contains this:

               OpSwitch %7 %10 2 %9 1 %8

The spec says that if Target T1 branches to Target T2 then T1 must appear before T2. Here, %8 does not branch to %9. However, the case construct headed by %8 branches to %9, because %8 branches to %20.

The validator rejects this example. And I think that is probably the intent of the specification authors - that "Target T1 branches to Target T2" is intended to mean "The case construct headed by Target T1".

It would be good to open a spec issue for this.