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

term model panic #1367

Closed
robdockins opened this issue Jul 2, 2021 · 0 comments
Closed

term model panic #1367

robdockins opened this issue Jul 2, 2021 · 0 comments
Labels
type: bug Issues reporting bugs or unexpected/unwanted behavior

Comments

@robdockins
Copy link
Contributor

Running the following script yields a panic.

enable_experimental;

f <- fresh_symbolic "f" {| [100][8] |};
a <- normalize_term {{ \n -> f @ n }};
%< ---------------------------------------------------
  Revision:  abd6f202ccc481130b587db87716a3c7c4cd233a
  Branch:    recursor-refactor (uncommited files present)
  Location:  Verifier.SAW.Simulator.Prims
  Message:   atOp: expected Nat, got <extra> fresh:i#786 : PrimName {primVarIndex = 133, primName = Prelude.Nat, primType = sort 0}
CallStack (from HasCallStack):
  panic, called at src/Verifier/SAW/Utils.hs:37:9 in saw-core-0.1-inplace:Verifier.SAW.Utils
  panic, called at src/Verifier/SAW/Simulator/Prims.hs:376:13 in saw-core-0.1-inplace:Verifier.SAW.Simulator.Prims
  panic, called at src/Verifier/SAW/Simulator/Prims.hs:705:12 in saw-core-0.1-inplace:Verifier.SAW.Simulator.Prims
%< ---------------------------------------------------

Basically, the problem is that the at primitive is too strict about the form it expects from its arguments and panics when it should instead continue with term reconstruction. Some of the other sequence primitives have similar problems. We'll need to reorganize these primitives so they don't panic in these situations.

@robdockins robdockins added the type: bug Issues reporting bugs or unexpected/unwanted behavior label Jul 2, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
type: bug Issues reporting bugs or unexpected/unwanted behavior
Projects
None yet
Development

No branches or pull requests

1 participant