mc-imperial / spirv-control-flow

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

SwiftShader: Segfault #9

Open Jack-Clark opened 2 years ago

Jack-Clark commented 2 years ago

I think this is allowed, but @vili-1 can you confirm that a loop header can be its own continue target? See the CFG below.

Executing amber -t spv1.3 -v 1.1 reduced-segfault.amber leads to a segfault. I think this may be related to #8 as both seem to rely on there being input variable accesses in a selection header followed by a loop header.

I have attached an archive containing the files.

Segfault

vili-1 commented 2 years ago

Yes @Jack-Clark , a loop header can be its own continue target (this example is allowed - SHO is Entry). About the segfault I have to dig a bit into this.

vili-1 commented 2 years ago

@Jack-Clark, I don't get segfault in my Mac

Summary: 1 pass, 0 fail

Jack-Clark commented 2 years ago

Great, thanks for confirming this. Regarding the segfault, dId you use SwiftShader or moltenVK?

vili-1 commented 2 years ago

MoltenVK

$ ./amber -d -V
Amber        : d8acae6
SPIRV-Tools  : 97f1d485
SPIRV-Headers: dc77030
GLSLang      : 07a55839
Shaderc      : 821d564

Physical device properties:
  apiVersion: 1.1.170
  driverVersion: 10102
  vendorID: 32902
  deviceID: 35411
  deviceType: integrated gpu
  deviceName: Intel(R) Iris(TM) Plus Graphics
  driverName: MoltenVK
  driverInfo: 1.1.2
End of physical device properties.
vili-1 commented 2 years ago

As stated in #8, we get an error when the node in the fleshing path is both a switch case and merge block of the switch and further, the switch is the head of the path. The successful execution that I mentioned above was using a fleshing path other than this. Maybe we have a chat with @afd at some point to clarify this (not clear to me at the moment).

vili-1 commented 2 years ago

Loading the SwiftShader I get no error! issue9

Jack-Clark commented 2 years ago

Hmmm, which commit are you using for SwiftShader? I installed SwiftShader on my desktop (using the commit in the original post) and could reproduce the segfault.