mc-imperial / spirv-control-flow

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

test_0.xml example uses old format #26

Closed Jack-Clark closed 1 year ago

Jack-Clark commented 2 years ago

The test_0.xml file that we use as a fleshing example uses the old input format, causing the current flesher to fail i.e. in the fleshing folder, running:

python fleshout.py test_0.xml --l 24 --seed 6179875240267643350

Causes the following error:

Fleshing with seed 6179875240267643350
Traceback (most recent call last):
  File "/home/c/OPENSOURCE/spirv-control-flow/fleshing/fleshout.py", line 1490, in <module>
    main()
  File "/home/c/OPENSOURCE/spirv-control-flow/fleshing/fleshout.py", line 1481, in main
    asm = fleshout(args.xml, path_length=args.l, seed=args.seed, x_threads=args.x_threads, y_threads=args.y_threads, z_threads=args.z_threads, x_workgroups=args.x_workgroups, y_workgroups=args.y_workgroups, z_workgroups=args.z_workgroups, include_barriers=args.simple_barriers, include_op_phi=args.op_phi)
  File "/home/c/OPENSOURCE/spirv-control-flow/fleshing/fleshout.py", line 1402, in fleshout
    cfg = CFG(get_jump_relation(instance),
  File "/home/c/OPENSOURCE/spirv-control-flow/fleshing/fleshout.py", line 550, in __init__
    self.topological_ordering: List[str] = self.compute_topological_ordering()
  File "/home/c/OPENSOURCE/spirv-control-flow/fleshing/fleshout.py", line 591, in compute_topological_ordering
    in_degree[successor] += 1
KeyError: 'StructurallyReachableBlock$0'

We should create a new test_0.xml file that uses the new input format and update the explanantion to match.