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.

Sign up for GitHub

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

Jump to bottom

Evaluation of fromZ causes panic #936

Closed
brianhuffman opened this issue Nov 24, 2020 · 4 comments
Closed

Evaluation of fromZ causes panic #936

brianhuffman opened this issue Nov 24, 2020 · 4 comments
Assignees
@brianhuffman
Labels
type: bug Issues reporting bugs or unexpected/unwanted behavior

Comments

@brianhuffman
Copy link
Contributor

It seems that evaluation of any expression containing the cryptol function fromZ causes the evaluator to panic:

sawscript> print {{ fromZ`{13} 2 == 0 }}
saw: You have encountered a bug in SawCore's implementation.
*** Please create an issue at https://github.com/GaloisInc/saw-core/issues

%< ---------------------------------------------------
  Revision:  056ac76c3ba0cdafe0ea054131da8d48660448c9
  Branch:    prettyprinter (uncommited files present)
  Location:  Verifier.SAW.Simulator.Prims
  Message:   expected Integer intEq x
CallStack (from HasCallStack):
  panic, called at src/Verifier/SAW/Utils.hs:37:9 in saw-core-0.1-J19DkSUjZjgBlGUiDiS4Ri:Verifier.SAW.Utils
  panic, called at src/Verifier/SAW/Simulator/Prims.hs:268:13 in saw-core-0.1-J19DkSUjZjgBlGUiDiS4Ri:Verifier.SAW.Simulator.Prims
  panic, called at src/Verifier/SAW/Simulator/Prims.hs:298:15 in saw-core-0.1-J19DkSUjZjgBlGUiDiS4Ri:Verifier.SAW.Simulator.Prims
%< ---------------------------------------------------
@brianhuffman brianhuffman added the type: bug Issues reporting bugs or unexpected/unwanted behavior label Nov 24, 2020
@brianhuffman
Copy link
Contributor Author

In Cryptol.sawcore, the cryptol function fromZ is defined in terms of the saw-core primitive fromIntMod.

@brianhuffman
Copy link
Contributor Author

I've identified the problem: In the concrete backend, values of the IntMod type were originally represented using VInt, the same constructor used to represent type Integer. The integers are always represented in reduced form, so the original definition of fromIntMod was basically just an identity function.

But since GaloisInc/saw-core#93, the IntMod type now uses a new, separate value constructor VIntMod that also carries the modulus. So the implementation of fromIntMod as an identity function is now incorrect.

@brianhuffman brianhuffman self-assigned this Nov 24, 2020
brianhuffman pushed a commit to GaloisInc/saw-core that referenced this issue Nov 24, 2020
Fix implementation of fromIntMod in concrete evaluation backend.
2d04786 
It had been broken since #93 introduced a separate value constructor
for the `IntMod` type.

(GaloisInc/saw-script#936)
@brianhuffman brianhuffman mentioned this issue Nov 24, 2020
Merged
@brianhuffman
Copy link
Contributor Author

I have a fix for this in GaloisInc/saw-core#109. I'll close the ticket when everything gets merged into saw-script master.

@brianhuffman
Copy link
Contributor Author

The fix was merged into saw-script master when the saw-core submodule was bumped in #941.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@brianhuffman brianhuffman

Labels
type: bug Issues reporting bugs or unexpected/unwanted behavior
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@brianhuffman