GaloisInc / saw-script

The SAW scripting language.
BSD 3-Clause "New" or "Revised" License
442 stars 63 forks source link

Bogus stack trace with MIR verification and wrong return type #2108

Open sauclovian-g opened 2 months ago

sauclovian-g commented 2 months ago

I just accidentally wrote a spec with a wrong return type, and this fails with a stack trace. Now that the position tracking has been degarbled upstream of this, it's become clear that something else is wrong.

The example I'm working with is complicated and has lots of saw-script support code, so the stack trace is fairly substantial. This reveals that it's fairly off:

It appears that the positions and functions are misaligned, possibly with a bad zip or equivalent, but there's also something odd going on with closures, and what should probably be the last entry (the failing mir_return) is missing.

This wants a simpler test, or possibly two (one for the closure) but that probably won't be that difficult.