mc-imperial / spirv-control-flow

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

The SPIR-V specification does not define the term "outer" for constructs #46

Open afd opened 3 years ago

afd commented 3 years ago

Spec version: Version 1.5, Revision 5, Unified January 7, 2021

The spec says (2.11, page 29):

Furthermore, these structured control-flow constructs are additionally defined to exclude all outer constructs’ continue constructs and exclude all blocks dominated by all outer constructs’ merge blocks.

and later:

... a branch to an outer OpSwitch merge block is ...

However, the notion of an "outer" construct is not explicitly defined.

It might be reasonable to say that construct A is an outer construct for construct B if the header of A dominates the header of B.