Better SMT2 debugging #374
Conversation
msooseth
force-pushed
the
fix-debugging-smt2
branch
from
4fe0e3b to
28912be
Compare
msooseth
force-pushed
the
fix-debugging-smt2
branch
from
28912be to
c63c577
Compare
| @@ -103,8 +104,14 @@ data SMTCex = SMTCex | |||
|
|
|||
|
|
|||
| -- | Used for abstraction-refinement of the SMT formula. Contains assertions that make our query fully precise. These will be added to the assertion stack if we get `sat` with the abstracted query. | |||
| newtype RefinementEqs = RefinementEqs [Builder] | |||
| deriving (Eq, Show, Monoid, Semigroup) | |||
| data RefinementEqs = RefinementEqs [Builder] [Prop] | |||
There was a problem hiding this comment.
what are the extra props for?
There was a problem hiding this comment.
So the SMT2 can store the original set of Prop-s that were used to generate the SMT2 query. When the SMT2 gets to runTask, it only has the SMT2. I wanted the SMT2 to also contain the Prop-s that were used to create it, so we can dump the props together with the SMT2 query when we actually send it to the solver.
Honestly, without a facility like this PR, it is essentially impossible for me to do proper debugging. I think you probably have other methods of doing this, but I have had a bit of a trouble fighting the repl just trying to get something meaningful info out of a single test file. I'd rather have something that actually works by simply setting a debug flag, without me having to understand the full, recursive, function-passing, iterative, self-folding callchain and insert some helper function/trace every time I need to do some minor debugging.
There was a problem hiding this comment.
Note that having the Prop-s at the top of the SMT2 file is incredibly valuable. I wanted to make sure that information stays there, and is always exactly correct. The only way I found to ensure this is to pass it along with the SMT2, inserting it as part of assertProps. This is the only way I have found that can do that while making sure things stay relatively clean & always having matching Prop-s to the SMT2 being generated.
| @@ -125,17 +132,20 @@ collapse model = case toBuf model of | |||
| getVar :: SMTCex -> TS.Text -> W256 | |||
| getVar cex name = fromJust $ Map.lookup (Var name) cex.vars | |||
|
|
|||
| data SMT2 = SMT2 [Builder] RefinementEqs CexVars | |||
| data SMT2 = SMT2 [Builder] RefinementEqs CexVars [Prop] | |||
There was a problem hiding this comment.
what are the extra props for?
| @@ -128,7 +136,9 @@ withSolvers solver count timeout cont = do | |||
| "unknown" -> pure Unknown | |||
| "sat" -> if null refineEqs then Sat <$> getModel inst cexvars | |||
| else do | |||
| _ <- sendScript inst (SMT2 refineEqs mempty mempty) | |||
| let refinedSMT2 = SMT2 refineEqs mempty mempty (ps <> refps) | |||
| writeSMT2File refinedSMT2 fileCounter "refined" | |||
There was a problem hiding this comment.
what do you think about doing this inside of sendLine and friends? and just append every line we send for each SMT2 to the same file?
There was a problem hiding this comment.
Can we do that as a follow-up? You mean that all send... functions should now take another parameter, an open IO (Maybe FileIO or something?) for a file that is open? Honestly, I am a bit scared of the file IO in Haskell, I can barely use it. I have a feeling I'd make a mess of it and then this PR will stall even longer :(
There was a problem hiding this comment.
Anyway, I'm gonna do it, but I'm sure it's just gonna be wrong. But anyway, let me see.
There was a problem hiding this comment.
I just reverted it, it's here cf769b9 but it's incomplete and a lot more noisy than the 2 lines of writeSMT2File. It is also has a bunch of complications and I'm not sure it's worth it, I think those 2 lines are easy enough.
Co-authored-by: dxo <[email protected]>
Co-authored-by: dxo <[email protected]>
This reverts commit cf769b9.
|
In the end, I think the most important thing to do is to add https://gist.github.com/d-xo/314b84c260907ef0920c3b2e6b98738b to everything. First without the |
Description
Debugging SMT2 is currently partially broken, this is a future attempt at fixing it.
Checklist