Assertion failure in src/il2al/il2il.ml

[tlively]

I ran into this assertion failure:

== Parsing...
== Elaboration...
== IL Validation...
== Running pass sideconditions...
== IL Validation after pass sideconditions...
== Running pass animate...
== IL Validation after pass animate...
== Translating to AL...
/usr/local/google/home/tlively/code/spectec/spectec/test-prose/../watsup: uncaught exception File "src/il2al/il2il.ml", line 192, characters 11-17: Assertion failed
Raised at Il2al__Il2il.overlap_typ in file "src/il2al/il2il.ml", line 192, characters 11-23
Called from Il2al__Il2il.overlap in file "src/il2al/il2il.ml", line 168, characters 15-42
Called from Stdlib__List.fold_left in file "list.ml", line 121, characters 24-34
Called from Il2al__Il2il.unify_lhs' in file "src/il2al/il2il.ml", line 255, characters 17-45
Called from Il2al__Il2il.unify_lhs in file "src/il2al/il2il.ml", line 262, characters 10-56
Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Il2al__Translate.translate_rules in file "src/il2al/translate.ml", line 1026, characters 2-149
Called from Il2al__Translate.translate in file "src/il2al/translate.ml", line 1039, characters 25-43
Called from Dune__exe__Main in file "src/exe-watsup/main.ml", line 201, characters 9-37

when running make test-prose on my local development. I've pushed the reproducer to this branch: https://github.com/tlively/spectec/tree/assertion-failure. The last commit on that branch triggers the failure; everything works fine before that commit.

[rossberg]

Hi Thomas, thanks for the report, we'll look into it.

[f52985]

Hello Thomas,

The assertion failure happened due to the reduction rules for stack.switch on line 570 ~ 576.

Our system had an assumption that when there are multiple rules for a wasm instruction, all rules must come from the same relation.

The first rule, stack.switch-null, is from the relation Step_pure (thus no z), and the second rule, stack.switch-stack, is from the relation Step (thus z appearing), resulting in a failure of merging these two rules into a single prose.

For now, making both of the rules as Step (or I guess Step_read would also work) will solve the issue for now.

@rossberg, what do you think is the proper way to handle this kind of situation of mixed use of relations?:

1. Disallow the mixed use of relations (either at the frontend or during the il2al translation), or
2. Allow the mixed use of relations (and let the il2al translator handle it)?

p.s. Unfortunately, the system currently will result in failure of generating prose for stack.switch even after unifying their relations, due to the fact that the length of the value stack from two rules differ.

For now, please also add val^n to the value stack of the rule stack.switch-null as in val^n (REF.NULL ht) (STACK.SWITCH x) ~> TRAP for circumventing the problem and properly generate the prose.

[rossberg]

@f52985, I think it's okay if we require the same relation, unless it would be super-easy for the translation to handle mixed cases :). As for who gives the error, the frontend does not even know what a reduction relation is; this is a restriction of AL-specific backends, so the AL translation should produce a proper error message (also for the missing operands).

[tlively]

Would it be easy enough to handle the missing operands automatically by assuming they are there below the listed operands on the stack and assuming that the reduction rule simply leaves them there? The reduction rule for call similarly does not need to mention the call arguments because they are not modified.

[f52985]

Would it be easy enough to handle the missing operands automatically by assuming they are there below the listed operands on the stack and assuming that the reduction rule simply leaves them there?

Handling the missing operands manually (i.e. manually write the algorithmic prose) would be trivial, but generating it automatically (in a robust manner) was a bit challenging, and left as TODO.

The reduction rule for call similarly does not need to mention the call arguments because they are not modified.

Yes, and for that reason, the prose for CALL_REF was not automatically generated, and the manually written prose was being used instead.

---

For now, I added some code for handling the missing operands, which is robustness enough to handle both CALL_REF and STACK.SWITCH, so you can maintain the current reduction rules!

[tlively]

Thank you!