Call stacks #995
Merged
Call stacks #995
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
into the typechecked AST. This should eventually allow us to emit more useful error messages for runtime errors.
for primitives that is evaluated to values when a primitive is looked up at evaluation time. Currently, this does not add any additional capabilities, but gives us the ability to modify the representation of values without touching all the primitive definitions, and gives us a place to hook in additional capabilies to the primitives. As part of this refactoring, the primitives that are defined totally generically are moved to the `Cryptol.Eval.Generic` module and used uniformly in all the backends.
This turns out to be surprisingly involved! Every evaluation helper and primitive that can raise a runtime error requires knowledge of it's current source location, and we need to rearrange slightly how variable lookups work so we can track the source location of the calling context for primitives, rather than just the location where the primitive was declared.
inputs. Error messages now properly locate subexpressions inside batch interaction files, and line numbers count up on succesive REPL inputs.
the expression concretely with the computed inputs to find and print the actual concrete error generated by the counterexample.
This allows us to print call stacks in addition to just the source location on program errors.
primitives. We rely on the tracked call stack information instead.
counterexamples/models are not avalaible.
robdockins
force-pushed
the
call-stack
branch
from
0bca85e to
bdfefd5
Compare
robdockins
commented
Dec 8, 2020
source location and call stack tracking. Computing call stacks, in particular, can add pretty significant interpreter overheads.
The tuple approach was starting to become unwieldly.
robdockins
commented
Dec 9, 2020
| else concat <$> (forM xs $ \x -> | ||
| then rPutStrLn "There are no properties in scope." | ||
| else forM_ xs $ \x -> | ||
| -- TOOD, this is pretty bogus. Should find a way to do |
There was a problem hiding this comment.
Note to self: should open a ticket about this
There was a problem hiding this comment.
Actually, I think #639 is caused by this. We just take the name of the property and parse it in the current scope, which might fail.
This was referenced Dec 10, 2020
brianhuffman
pushed a commit
to GaloisInc/saw-core
that referenced
this pull request
Jan 28, 2021
brianhuffman
pushed a commit
to GaloisInc/saw-script
that referenced
this pull request
Jan 28, 2021
brianhuffman
pushed a commit
to GaloisInc/saw-script
that referenced
this pull request
Jan 28, 2021
brianhuffman
pushed a commit
to GaloisInc/saw-script
that referenced
this pull request
Jan 28, 2021
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Builds on PR #985
This PR adds call stack handling to the interpreter, and prints backtraces when evaluation errors occur. Getting this to work is a bit fiddly, but this seems to be operating more or less the way I expect.