mc-imperial / spirv-control-flow

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

Definitions of break and continue block are problematic #35

Open afd opened 2 years ago

afd commented 2 years ago

The spec defines a break block and a continue block, and says that they are valid only for the innermost loop they are nested inside of.

This prohibits entering a single-block loop, because technically the predecessor of the loop header that is not in the loop becomes both a break block and a continue block.

This CFG, from @vili-1's mc-imperial/spirv-control-flow#36, illustrates the issue:

image

The edge 14->16 is problematic according to the current definition of break and continue blocks.

vili-1 commented 2 years ago

..