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

Data.Vector calls 'error' inside splitOp #1230

Closed
langston-barrett opened this issue Sep 23, 2019 · 4 comments
Closed

Data.Vector calls 'error' inside splitOp #1230

langston-barrett opened this issue Sep 23, 2019 · 4 comments
Assignees
@brianhuffman
Labels
subsystem: saw-core Issues related to the saw-core representation or the saw-core subsystem

Comments

@langston-barrett
Copy link
Contributor

When SAW is checking proof obligations on my proof and the w4_unint_z3 tactic, it fails with:

[21:46:03.377] ./Data/Vector/Generic.hs:396 (slice): invalid slice (1024,512,1296)
CallStack (from HasCallStack):
  error, called at ./Data/Vector/Internal/Check.hs:87:5 in vector-0.12.0.2-AoZ9EwUsgIW1yrOc105QXH:Data.Vector.Internal.Check
CallStack (from -prof):
  Data.Vector.Internal.Check.error (Data/Vector/Internal/Check.hs:(86,1)-(87,41))
  Verifier.SAW.Simulator.Prims.splitOp.\.\.\.f (src/Verifier/SAW/Simulator/Prims.hs:712:11-52)
  Verifier.SAW.Simulator.Prims.splitOp.\.\.\ (src/Verifier/SAW/Simulator/Prims.hs:(710,3)-(717,50))
  Verifier.SAW.Simulator.Prims.splitOp.\.\ (src/Verifier/SAW/Simulator/Prims.hs:(707,36)-(717,50))
  Verifier.SAW.Simulator.Prims.natFun.g (src/Verifier/SAW/Simulator/Prims.hs:(268,9)-(269,33))
  Verifier.SAW.Simulator.Value.strictFun.\ (src/Verifier/SAW/Simulator/Value.hs:116:27-39)
  Verifier.SAW.Simulator.Value.strictFun (src/Verifier/SAW/Simulator/Value.hs:116:1-40)
  Verifier.SAW.Simulator.Prims.natFun (src/Verifier/SAW/Simulator/Prims.hs:(267,1)-(269,33))
  Verifier.SAW.Simulator.Prims.splitOp (src/Verifier/SAW/Simulator/Prims.hs:(705,1)-(717,50))
  Verifier.SAW.Simulator.Prims.constMap (src/Verifier/SAW/Simulator/Prims.hs:(129,1)-(244,3))
  Verifier.SAW.Simulator.evalTermF (src/Verifier/SAW/Simulator.hs:(124,1)-(172,34))
  Verifier.SAW.Simulator.evalLocalTermF (src/Verifier/SAW/Simulator.hs:(473,1)-(480,56))
  Verifier.SAW.Simulator.mkMemoLocal.goTermF (src/Verifier/SAW/Simulator.hs:(444,5)-(452,37))
  Verifier.SAW.Simulator.mkMemoLocal.go (src/Verifier/SAW/Simulator.hs:(434,5)-(441,44))
  Verifier.SAW.Simulator.mkMemoLocal (src/Verifier/SAW/Simulator.hs:(431,1)-(452,37))
  Verifier.SAW.Simulator.evalOpen.eval (src/Verifier/SAW/Simulator.hs:(504,7)-(508,29))
  Verifier.SAW.Simulator.evalOpen (src/Verifier/SAW/Simulator.hs:(501,1)-(511,8))
  Verifier.SAW.Simulator.evalClosedTermF.lam (src/Verifier/SAW/Simulator.hs:405:5-33)
  Verifier.SAW.Simulator.evalClosedTermF (src/Verifier/SAW/Simulator.hs:(403,1)-(410,57))
  Verifier.SAW.Simulator.mkMemoClosed.\ (src/Verifier/SAW/Simulator.hs:368:25-78)
  Verifier.SAW.Simulator.mkMemoClosed (src/Verifier/SAW/Simulator.hs:(367,1)-(383,18))
  Verifier.SAW.Simulator.evalSharedTerm (src/Verifier/SAW/Simulator.hs:(353,1)-(355,30))
  Verifier.SAW.Simulator.Value.apply (src/Verifier/SAW/Simulator/Value.hs:(203,1)-(205,54))
  Verifier.SAW.Simulator.Value.applyAll (src/Verifier/SAW/Simulator/Value.hs:208:1-22)
  Verifier.SAW.Simulator.What4.w4Solve (src/Verifier/SAW/Simulator/What4.hs:(634,1)-(663,31))
  SAWScript.Prover.What4.prepWhat4 (src/SAWScript/Prover/What4.hs:(118,1)-(128,28))
  SAWScript.Prover.What4.satWhat4_solver (src/SAWScript/Prover/What4.hs:(81,1)-(111,50))
  SAWScript.Prover.What4.satWhat4_sym (src/SAWScript/Prover/What4.hs:(49,1)-(52,36))
  SAWScript.Prover.What4.satWhat4_z3 (src/SAWScript/Prover/What4.hs:62:1-43)
  SAWScript.Builtins.withFirstGoal (src/SAWScript/Builtins.hs:(335,1)-(343,83))
  SAWScript.Builtins.wrapProver (src/SAWScript/Builtins.hs:(688,1)-(699,41))
  SAWScript.Builtins.satWhat4_UnintZ3 (src/SAWScript/Builtins.hs:750:1-50)
  SAWScript.Value.addTraceIO (src/SAWScript/Value.hs:(835,1)-(840,63))
  SAWScript.Value.underStateT (src/SAWScript/Value.hs:810:1-72)
  SAWScript.Value.underReaderT (src/SAWScript/Value.hs:813:1-79)
  SAWScript.Value.addTraceTopLevel (src/SAWScript/Value.hs:(852,1)-(853,54))
  SAWScript.Value.addTrace (src/SAWScript/Value.hs:(821,1)-(830,27))
  SAWScript.Value.withPosition (src/SAWScript/Value.hs:404:1-82)
  SAWScript.Interpreter.interpretStmt (src/SAWScript/Interpreter.hs:(361,1)-(388,83))
  SAWScript.Interpreter.interpretFile (src/SAWScript/Interpreter.hs:(391,1)-(404,53))
  SAWScript.Value.runTopLevel (src/SAWScript/Value.hs:398:1-63)
  SAWScript.Interpreter.processFile (src/SAWScript/Interpreter.hs:(479,1)-(487,11))
  Main.main (saw/Main.hs:(27,1)-(50,31))

With the unint_z3 tactic, I see

[21:34:18.971] ./Data/Vector/Generic.hs:396 (slice): invalid slice (1024,512,1296)
CallStack (from HasCallStack):
  error, called at ./Data/Vector/Internal/Check.hs:87:5 in vector-0.12.0.2-AoZ9EwUsgIW1yrOc105QXH:Data.Vector.Internal.Check
CallStack (from -prof):
  Data.Vector.Internal.Check.error (Data/Vector/Internal/Check.hs:(86,1)-(87,41))
  Verifier.SAW.Simulator.Prims.splitOp.\.\.\.f (src/Verifier/SAW/Simulator/Prims.hs:712:11-52)
  Verifier.SAW.Simulator.Prims.splitOp.\.\.\ (src/Verifier/SAW/Simulator/Prims.hs:(710,3)-(717,50))
  Verifier.SAW.Simulator.Prims.splitOp.\.\ (src/Verifier/SAW/Simulator/Prims.hs:(707,36)-(717,50))
  Verifier.SAW.Simulator.Prims.natFun.g (src/Verifier/SAW/Simulator/Prims.hs:(268,9)-(269,33))
  Verifier.SAW.Simulator.Value.strictFun.\ (src/Verifier/SAW/Simulator/Value.hs:116:27-39)
  Verifier.SAW.Simulator.Value.strictFun (src/Verifier/SAW/Simulator/Value.hs:116:1-40)
  Verifier.SAW.Simulator.Prims.natFun (src/Verifier/SAW/Simulator/Prims.hs:(267,1)-(269,33))
  Verifier.SAW.Simulator.Prims.splitOp (src/Verifier/SAW/Simulator/Prims.hs:(705,1)-(717,50))
  Verifier.SAW.Simulator.Prims.constMap (src/Verifier/SAW/Simulator/Prims.hs:(129,1)-(244,3))
  Verifier.SAW.Simulator.evalTermF (src/Verifier/SAW/Simulator.hs:(124,1)-(172,34))
  Verifier.SAW.Simulator.evalLocalTermF (src/Verifier/SAW/Simulator.hs:(473,1)-(480,56))
  Verifier.SAW.Simulator.mkMemoLocal.goTermF (src/Verifier/SAW/Simulator.hs:(444,5)-(452,37))
  Verifier.SAW.Simulator.mkMemoLocal.go (src/Verifier/SAW/Simulator.hs:(434,5)-(441,44))
  Verifier.SAW.Simulator.mkMemoLocal (src/Verifier/SAW/Simulator.hs:(431,1)-(452,37))
  Verifier.SAW.Simulator.evalOpen.eval (src/Verifier/SAW/Simulator.hs:(504,7)-(508,29))
  Verifier.SAW.Simulator.evalOpen (src/Verifier/SAW/Simulator.hs:(501,1)-(511,8))
  Verifier.SAW.Simulator.evalClosedTermF.lam (src/Verifier/SAW/Simulator.hs:405:5-33)
  Verifier.SAW.Simulator.evalClosedTermF (src/Verifier/SAW/Simulator.hs:(403,1)-(410,57))
  Verifier.SAW.Simulator.mkMemoClosed.\ (src/Verifier/SAW/Simulator.hs:368:25-78)
  Verifier.SAW.Simulator.mkMemoClosed (src/Verifier/SAW/Simulator.hs:(367,1)-(383,18))
  Verifier.SAW.Simulator.evalSharedTerm (src/Verifier/SAW/Simulator.hs:(353,1)-(355,30))
  Verifier.SAW.Simulator.SBV.sbvSolveBasic (src/Verifier/SAW/Simulator/SBV.hs:(533,1)-(541,26))
  Verifier.SAW.Simulator.Value.apply (src/Verifier/SAW/Simulator/Value.hs:(203,1)-(205,54))
  Verifier.SAW.Simulator.Value.applyAll (src/Verifier/SAW/Simulator/Value.hs:208:1-22)
  Verifier.SAW.Simulator.SBV.sbvSolve (src/Verifier/SAW/Simulator/SBV.hs:(625,1)-(641,22))
  SAWScript.Prover.SBV.prepSBV (src/SAWScript/Prover/SBV.hs:(79,1)-(90,29))
  Data.SBV.Core.Symbolic.runSymbolic (Data/SBV/Core/Symbolic.hs:(1405,1)-(1474,18))
  Data.SBV.Dynamic.satWith (Data/SBV/Dynamic.hs:174:1-48)
  SAWScript.Prover.SBV.satUnintSBV (src/SAWScript/Prover/SBV.hs:(44,1)-(73,79))
  SAWScript.Builtins.withFirstGoal (src/SAWScript/Builtins.hs:(335,1)-(343,83))
  SAWScript.Builtins.wrapProver (src/SAWScript/Builtins.hs:(688,1)-(699,41))
  SAWScript.Builtins.satUnintSBV (src/SAWScript/Builtins.hs:(678,1)-(680,53))
  SAWScript.Builtins.satUnintZ3 (src/SAWScript/Builtins.hs:721:1-31)
  SAWScript.Value.addTraceIO (src/SAWScript/Value.hs:(835,1)-(840,63))
  SAWScript.Value.underStateT (src/SAWScript/Value.hs:810:1-72)
  SAWScript.Value.underReaderT (src/SAWScript/Value.hs:813:1-79)
  SAWScript.Value.addTraceTopLevel (src/SAWScript/Value.hs:(852,1)-(853,54))
  SAWScript.Value.addTrace (src/SAWScript/Value.hs:(821,1)-(830,27))
  SAWScript.Value.withPosition (src/SAWScript/Value.hs:404:1-82)
  SAWScript.Interpreter.interpretStmt (src/SAWScript/Interpreter.hs:(361,1)-(388,83))
  SAWScript.Interpreter.interpretFile (src/SAWScript/Interpreter.hs:(391,1)-(404,53))
  SAWScript.Value.runTopLevel (src/SAWScript/Value.hs:398:1-63)
  SAWScript.Interpreter.processFile (src/SAWScript/Interpreter.hs:(479,1)-(487,11))
  Main.main (saw/Main.hs:(27,1)-(50,31)

This is with saw-core affad38.
@brianhuffman
Copy link
Contributor

It looks like split has been called with an argument of the wrong size. Something must have generated an ill-typed saw-core term in a proof goal.

@brianhuffman brianhuffman self-assigned this Nov 16, 2019
@brianhuffman brianhuffman transferred this issue from GaloisInc/saw-core Apr 27, 2021
@brianhuffman brianhuffman added the subsystem: saw-core Issues related to the saw-core representation or the saw-core subsystem label Apr 27, 2021
@brianhuffman
Copy link
Contributor

I could add an additional check on the length inside splitOp, so that it won't call Data.Vector.slice with invalid indices. But that wouldn't fix the problem; it would still panic, just maybe with a slightly nicer error message.

The real problem here lies much earlier, when the ill-typed saw-core term is constructed in the first place. @langston-barrett, do you still know to trigger this bug? I could probably diagnose it if I was able to reproduce it. Otherwise we might as well close the ticket.

@langston-barrett
Copy link
Contributor Author

@langston-barrett, do you still know to trigger this bug?

No, sorry!

@brianhuffman
Copy link
Contributor

I guess I'll optimistically assume that maybe the problem no longer exists; we can reopen if it ever comes up again.

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

@brianhuffman brianhuffman

Labels
subsystem: saw-core Issues related to the saw-core representation or the saw-core subsystem
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@brianhuffman @langston-barrett