Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
sauclovian-g opened this issue Aug 27, 2024 · 1 comment
Open

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

sauclovian-g opened this issue Aug 27, 2024 · 1 comment
Labels
needs test Issues for which we should add a regression test topics: error-handling Issues involving the way SAW responds to an error condition topics: error-messages Issues involving the messages SAW produces on error type: bug Issues reporting bugs or unexpected/unwanted behavior
Milestone

Comments

@sauclovian-g
Copy link
Collaborator

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:

  • The first entry is attributed to a function f, but located at the (top-level) call site of f.
  • The second entry is attributed to a function g, but located in f. It's at the call site of g.
  • Both the third and fourth entries are located in g, one attributed to and at the call site of mir_unsafe_assume_spec, the other attributed to the function passed to mir_unsafe_assume_spec and located at the partial closure in the mir_unsafe_assume_spec call site.
  • The next two entries repeat the pattern of being at the call site of the function they're attributed to.
  • The last entry is attributed to the same function as the second-last, but located within it.
  • The mir_return that failed is never directly mentioned, although it's near the location of the second-last entry.

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.

@sauclovian-g sauclovian-g added type: bug Issues reporting bugs or unexpected/unwanted behavior topics: error-messages Issues involving the messages SAW produces on error topics: error-handling Issues involving the way SAW responds to an error condition labels Aug 27, 2024
@sauclovian-g sauclovian-g added the needs test Issues for which we should add a regression test label Nov 8, 2024
@sauclovian-g sauclovian-g added this to the 2024T3 milestone Nov 8, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
needs test Issues for which we should add a regression test topics: error-handling Issues involving the way SAW responds to an error condition topics: error-messages Issues involving the messages SAW produces on error type: bug Issues reporting bugs or unexpected/unwanted behavior
Projects
None yet
Development

No branches or pull requests

2 participants
@sauclovian-g and others