mc-imperial / spirv-control-flow

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

Valid continue-blocks #49

Open vili-1 opened 3 years ago

vili-1 commented 3 years ago

With regard to the validity of continue-blocks, the spec says (p.29 in [1]): "a continue block is valid only for the innermost loop it is nested inside of"

Trivially, we can infer from the above that "a continue block is not valid for any loop outer to the one the continue block is nested inside of"

Let:

Then, according to the rule above, the 'jump'-edge A -> C is a reject because C cannot be valid for A.

In the graph below the edge b2->jump->b3 is such an edge, which I guess is an acceptable one.

image

So, if we all agree that the graph above is a good one, then a better wording might be: "a continue block is not valid from within any loop nested into the continue-block’s header"

[1] The Khronos Group, 2021, p.29)

afd commented 3 years ago

Nice example!

I agree that the CFG you have shown should be allowed. The special case here is that the continue block b3 is also the header of a loop. Maybe the wording could be cleared up with something referring to that special case. Let's think about it.

afd commented 3 years ago

@vili-1 I presume this arose as a result of one of the control flow graphs we scraped from CTS. Would you be able to note the associated Amber file here?

vili-1 commented 3 years ago

https://github.com/KhronosGroup/VK-GL-CTS/blob/master/external/vulkancts/data/vulkan/amber/spirv_assembly/instruction/spirv1p4/nonwritable/private_nonwritable.amber