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

Better SMT2 debugging #374

Closed
wants to merge 12 commits into from
Closed

Better SMT2 debugging #374

Show file tree
Hide file tree
Changes from 8 commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
7a63664
The SMT2 file ought to be printed while executing it
msooseth Sep 6, 2023
e96eef0
fileCounter + ReaderT
d-xo Sep 6, 2023
2cd5d78
Rebase fix
msooseth Sep 20, 2023
c63c577
Almost clean setup
msooseth Sep 20, 2023
1dde6a1
All queries are saved
msooseth Sep 21, 2023
8024cf4
Get both props and SMT2s
msooseth Sep 21, 2023
8db6f53
Better printing of SMT2 queries
msooseth Sep 21, 2023
b4b1232
Fixing generated SMT2
msooseth Sep 22, 2023
920cc2e
Update test/test.hs
msooseth Oct 4, 2023
353f20a
Update test/test.hs
msooseth Oct 4, 2023
cf769b9
Sendline change
msooseth Oct 4, 2023
f751e8a
Revert "Sendline change"
msooseth Oct 4, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions src/EVM/Format.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ module EVM.Format
( formatExpr
, formatSomeExpr
, formatPartial
, formatProp
, contractNamePart
, contractPathPart
, showError
Expand Down
61 changes: 36 additions & 25 deletions src/EVM/SMT.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@ import Language.SMT2.Syntax (Symbol, SpecConstant(..), GeneralRes(..), Term(..),
import Numeric (readHex, readBin)
import Witch (into, unsafeInto)
import Control.Monad.State
import EVM.Format (formatProp)

import EVM.CSE
import EVM.Expr (writeByte, bufLengthEnv, containsNode, bufLength, minLength, inRange)
Expand Down Expand Up @@ -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]
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

what are the extra props for?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

deriving (Eq, Show)

instance Semigroup RefinementEqs where
(RefinementEqs a b) <> (RefinementEqs a2 b2) = RefinementEqs (a <> a2) (b <> b2)

instance Monoid RefinementEqs where
mempty = RefinementEqs mempty mempty

flattenBufs :: SMTCex -> Maybe SMTCex
flattenBufs cex = do
Expand All @@ -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]
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

what are the extra props for?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

See above :)

deriving (Eq, Show)

instance Semigroup SMT2 where
(SMT2 a (RefinementEqs b) c) <> (SMT2 a2 (RefinementEqs b2) c2) = SMT2 (a <> a2) (RefinementEqs (b <> b2)) (c <> c2)
(SMT2 a (RefinementEqs b refps) c d) <> (SMT2 a2 (RefinementEqs b2 refps2) c2 d2) = SMT2 (a <> a2) (RefinementEqs (b <> b2) (refps <> refps2)) (c <> c2) (d <> d2)

instance Monoid SMT2 where
mempty = SMT2 mempty mempty mempty
mempty = SMT2 mempty mempty mempty mempty

formatSMT2 :: SMT2 -> Text
formatSMT2 (SMT2 ls _ _) = T.unlines (fmap toLazyText ls)
formatSMT2 (SMT2 ls _ _ ps) = expr <> smt2
where
expr = T.concat [T.singleton ';', T.replace "\n" "\n;" $ T.pack . TS.unpack $ TS.unlines (fmap formatProp ps)]
smt2 = T.unlines (fmap toLazyText ls)

-- | Reads all intermediate variables from the builder state and produces SMT declaring them as constants
declareIntermediates :: BufEnv -> StoreEnv -> SMT2
Expand All @@ -144,16 +154,16 @@ declareIntermediates bufs stores =
encBs = Map.mapWithKey encodeBuf bufs
sorted = List.sortBy compareFst $ Map.toList $ encSs <> encBs
decls = fmap snd sorted
smt2 = (SMT2 [fromText "; intermediate buffers & stores"] mempty mempty):decls
in foldr (<>) (SMT2[""] mempty mempty) smt2
smt2 = (SMT2 [fromText "; intermediate buffers & stores"] mempty mempty mempty):decls
in foldr (<>) (SMT2[""] mempty mempty mempty) smt2
where
compareFst (l, _) (r, _) = compare l r
encodeBuf n expr =
SMT2 ["(define-const buf" <> (fromString . show $ n) <> " Buf " <> exprToSMT expr <> ")\n"] mempty mempty <> encodeBufLen n expr
SMT2 ["(define-const buf" <> (fromString . show $ n) <> " Buf " <> exprToSMT expr <> ")\n"] mempty mempty mempty <> encodeBufLen n expr
encodeBufLen n expr =
SMT2 ["(define-const buf" <> (fromString . show $ n) <>"_length" <> " (_ BitVec 256) " <> exprToSMT (bufLengthEnv bufs True expr) <> ")"] mempty mempty
SMT2 ["(define-const buf" <> (fromString . show $ n) <>"_length" <> " (_ BitVec 256) " <> exprToSMT (bufLengthEnv bufs True expr) <> ")"] mempty mempty mempty
encodeStore n expr =
SMT2 ["(define-const store" <> (fromString . show $ n) <> " Storage " <> exprToSMT expr <> ")"] mempty mempty
SMT2 ["(define-const store" <> (fromString . show $ n) <> " Storage " <> exprToSMT expr <> ")"] mempty mempty mempty

data AbstState = AbstState
{ words :: Map (Expr EWord) Int
Expand Down Expand Up @@ -190,7 +200,7 @@ abstractAwayProps abstRefineConfig ps = runState (mapM abstrAway ps) (AbstState
pure $ Var (TS.pack ("abst_" ++ show next))

smt2Line :: Builder -> SMT2
smt2Line txt = SMT2 [txt] mempty mempty
smt2Line txt = SMT2 [txt] mempty mempty mempty

assertProps :: AbstRefineConfig -> [Prop] -> SMT2
assertProps conf ps = assertPropsNoSimp conf (Expr.simplifyProps ps)
Expand Down Expand Up @@ -221,9 +231,10 @@ assertPropsNoSimp abstRefineConfig ps =
<> keccakAssumes
<> readAssumes
<> smt2Line ""
<> SMT2 (fmap (\p -> "(assert " <> p <> ")") encs) mempty mempty
<> SMT2 mempty (RefinementEqs $ fmap (\p -> "(assert " <> p <> ")") abstSMT) mempty
<> SMT2 mempty mempty mempty { storeReads = storageReads }
<> SMT2 (fmap (\p -> "(assert " <> p <> ")") encs) mempty mempty mempty
<> SMT2 mempty (RefinementEqs (fmap (\p -> "(assert " <> p <> ")") abstSMT) (psElimAbst <> abstProps)) mempty mempty
<> SMT2 mempty mempty mempty { storeReads = storageReads } mempty
<> SMT2 mempty mempty mempty ps

where
(psElim, bufs, stores) = eliminateProps ps
Expand Down Expand Up @@ -251,13 +262,13 @@ assertPropsNoSimp abstRefineConfig ps =

keccakAssumes
= smt2Line "; keccak assumptions"
<> SMT2 (fmap (\p -> "(assert " <> propToSMT p <> ")") (keccakAssumptions psElim bufVals storeVals)) mempty mempty
<> SMT2 (fmap (\p -> "(assert " <> propToSMT p <> ")") (keccakAssumptions psElim bufVals storeVals)) mempty mempty mempty
<> smt2Line "; keccak computations"
<> SMT2 (fmap (\p -> "(assert " <> propToSMT p <> ")") (keccakCompute psElim bufVals storeVals)) mempty mempty
<> SMT2 (fmap (\p -> "(assert " <> propToSMT p <> ")") (keccakCompute psElim bufVals storeVals)) mempty mempty mempty

readAssumes
= smt2Line "; read assumptions"
<> SMT2 (fmap (\p -> "(assert " <> propToSMT p <> ")") (assertReads psElim bufs stores)) mempty mempty
<> SMT2 (fmap (\p -> "(assert " <> propToSMT p <> ")") (assertReads psElim bufs stores)) mempty mempty mempty

referencedAbstractStores :: TraversableTerm a => a -> Set Builder
referencedAbstractStores term = foldTerm go mempty term
Expand Down Expand Up @@ -395,7 +406,7 @@ discoverMaxReads props benv senv = bufMap

-- | Returns an SMT2 object with all buffers referenced from the input props declared, and with the appropriate cex extraction metadata attached
declareBufs :: [Prop] -> BufEnv -> StoreEnv -> SMT2
declareBufs props bufEnv storeEnv = SMT2 ("; buffers" : fmap declareBuf allBufs <> ("; buffer lengths" : fmap declareLength allBufs)) mempty cexvars
declareBufs props bufEnv storeEnv = SMT2 ("; buffers" : fmap declareBuf allBufs <> ("; buffer lengths" : fmap declareLength allBufs)) mempty cexvars mempty
where
cexvars = (mempty :: CexVars){ buffers = discoverMaxReads props bufEnv storeEnv }
allBufs = fmap fromLazyText $ Map.keys cexvars.buffers
Expand All @@ -404,39 +415,39 @@ declareBufs props bufEnv storeEnv = SMT2 ("; buffers" : fmap declareBuf allBufs

-- Given a list of variable names, create an SMT2 object with the variables declared
declareVars :: [Builder] -> SMT2
declareVars names = SMT2 (["; variables"] <> fmap declare names) mempty cexvars
declareVars names = SMT2 (["; variables"] <> fmap declare names) mempty cexvars mempty
where
declare n = "(declare-const " <> n <> " (_ BitVec 256))"
cexvars = (mempty :: CexVars){ calldata = fmap toLazyText names }

-- Given a list of variable names, create an SMT2 object with the variables declared
declareAddrs :: [Builder] -> SMT2
declareAddrs names = SMT2 (["; symbolic addresseses"] <> fmap declare names) mempty cexvars
declareAddrs names = SMT2 (["; symbolic addresseses"] <> fmap declare names) mempty cexvars mempty
where
declare n = "(declare-const " <> n <> " Addr)"
cexvars = (mempty :: CexVars){ addrs = fmap toLazyText names }

declareFrameContext :: [(Builder, [Prop])] -> SMT2
declareFrameContext names = SMT2 (["; frame context"] <> concatMap declare names) mempty cexvars
declareFrameContext names = SMT2 (["; frame context"] <> concatMap declare names) mempty cexvars mempty
where
declare (n,props) = [ "(declare-const " <> n <> " (_ BitVec 256))" ]
<> fmap (\p -> "(assert " <> propToSMT p <> ")") props
cexvars = (mempty :: CexVars){ txContext = fmap (toLazyText . fst) names }

declareAbstractStores :: [Builder] -> SMT2
declareAbstractStores names = SMT2 (["; abstract base stores"] <> fmap declare names) mempty mempty
declareAbstractStores names = SMT2 (["; abstract base stores"] <> fmap declare names) mempty mempty mempty
where
declare n = "(declare-const " <> n <> " Storage)"

declareBlockContext :: [(Builder, [Prop])] -> SMT2
declareBlockContext names = SMT2 (["; block context"] <> concatMap declare names) mempty cexvars
declareBlockContext names = SMT2 (["; block context"] <> concatMap declare names) mempty cexvars mempty
where
declare (n, props) = [ "(declare-const " <> n <> " (_ BitVec 256))" ]
<> fmap (\p -> "(assert " <> propToSMT p <> ")") props
cexvars = (mempty :: CexVars){ blockContext = fmap (toLazyText . fst) names }

prelude :: SMT2
prelude = SMT2 src mempty mempty
prelude = SMT2 src mempty mempty mempty
where
src = fmap (fromLazyText . T.drop 2) . T.lines $ [i|
; logic
Expand Down
26 changes: 18 additions & 8 deletions src/EVM/Solvers.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -88,6 +88,12 @@ checkSat (SolverGroup taskQueue) script = do
-- collect result
readChan resChan

writeSMT2File :: SMT2 -> Int -> String -> IO ()
writeSMT2File smt2 count abst =
do
let content = formatSMT2 smt2 <> "\n\n(check-sat)"
T.writeFile ("query-" <> (show count) <> "-" <> abst <> ".smt2") content

withSolvers :: Solver -> Natural -> Maybe Natural -> (SolverGroup -> IO a) -> IO a
withSolvers solver count timeout cont = do
-- spawn solvers
Expand All @@ -96,7 +102,7 @@ withSolvers solver count timeout cont = do
taskQueue <- newChan
availableInstances <- newChan
forM_ instances (writeChan availableInstances)
orchestrateId <- forkIO $ orchestrate taskQueue availableInstances
orchestrateId <- forkIO $ orchestrate taskQueue availableInstances 0

-- run continuation with task queue
res <- cont (SolverGroup taskQueue)
Expand All @@ -106,15 +112,17 @@ withSolvers solver count timeout cont = do
killThread orchestrateId
pure res
where
orchestrate queue avail = do
orchestrate :: Chan Task -> Chan SolverInstance -> Int -> IO b
orchestrate queue avail fileCounter = do
task <- readChan queue
inst <- readChan avail
_ <- forkIO $ runTask task inst avail
orchestrate queue avail
_ <- forkIO $ runTask task inst avail fileCounter
orchestrate queue avail (fileCounter + 1)

runTask (Task (SMT2 cmds (RefinementEqs refineEqs) cexvars) r) inst availableInstances = do
runTask (Task smt2@(SMT2 cmds (RefinementEqs refineEqs refps) cexvars ps) r) inst availableInstances fileCounter = do
writeSMT2File smt2 fileCounter "abstracted"
-- reset solver and send all lines of provided script
out <- sendScript inst (SMT2 ("(reset)" : cmds) mempty mempty)
out <- sendScript inst (SMT2 ("(reset)" : cmds) mempty mempty ps)
case out of
-- if we got an error then return it
Left e -> writeChan r (Error ("error while writing SMT to solver: " <> T.toStrict e))
Expand All @@ -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"
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 :(

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Anyway, I'm gonna do it, but I'm sure it's just gonna be wrong. But anyway, let me see.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

_ <- sendScript inst refinedSMT2
sat2 <- sendLine inst "(check-sat)"
case sat2 of
"unsat" -> pure Unsat
Expand Down Expand Up @@ -262,7 +272,7 @@ stopSolver (SolverInstance _ stdin stdout stderr process) = cleanupProcess (Just

-- | Sends a list of commands to the solver. Returns the first error, if there was one.
sendScript :: SolverInstance -> SMT2 -> IO (Either Text ())
sendScript solver (SMT2 cmds _ _) = do
sendScript solver (SMT2 cmds _ _ _) = do
let sexprs = splitSExpr $ fmap toLazyText cmds
go sexprs
where
Expand Down
21 changes: 5 additions & 16 deletions src/EVM/SymExec.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,8 +24,6 @@ import Data.Set qualified as Set
import Data.Text (Text)
import Data.Text qualified as T
import Data.Text.IO qualified as T
import Data.Text.Lazy qualified as TL
import Data.Text.Lazy.IO qualified as TL
import Data.Tree.Zipper qualified as Zipper
import Data.Tuple (swap)
import EVM (makeVm, abstractContract, initialContract, getCodeLocation, isValidJumpDest)
Expand All @@ -34,7 +32,7 @@ import EVM.Fetch qualified as Fetch
import EVM.ABI
import EVM.Expr qualified as Expr
import EVM.Format (formatExpr, formatPartial)
import EVM.SMT (SMTCex(..), SMT2(..), assertProps, formatSMT2)
import EVM.SMT (SMTCex(..), SMT2(..), assertProps)
import EVM.SMT qualified as SMT
import EVM.Solvers
import EVM.Stepper (Stepper)
Expand Down Expand Up @@ -582,11 +580,6 @@ verify solvers opts preState maybepost = do
<> show (length withQueries)
<> " potential property violation(s)"

when opts.debug $ forM_ (zip [(1 :: Int)..] withQueries) $ \(idx, (q, leaf)) -> do
TL.writeFile
("query-" <> show idx <> ".smt2")
("; " <> (TL.pack $ show leaf) <> "\n\n" <> formatSMT2 q <> "\n\n(check-sat)")

-- Dispatch the remaining branches to the solver to check for violations
results <- flip mapConcurrently withQueries $ \(query, leaf) -> do
res <- checkSat solvers query
Expand Down Expand Up @@ -687,13 +680,9 @@ equivalenceCheck' solvers branchesA branchesB opts = do
-- the solver if we can determine unsatisfiability from the cache already
-- the last element of the returned tuple indicates whether the cache was
-- used or not
check :: UnsatCache -> (Set Prop) -> Int -> IO (EquivResult, Bool)
check knownUnsat props idx = do
check :: UnsatCache -> (Set Prop) -> IO (EquivResult, Bool)
check knownUnsat props = do
let smt = assertProps opts.abstRefineConfig (Set.toList props)
-- if debug is on, write the query to a file
let filename = "equiv-query-" <> show idx <> ".smt2"
when opts.debug $ TL.writeFile filename (formatSMT2 smt <> "\n\n(check-sat)")

ku <- readTVarIO knownUnsat
res <- if subsetAny props ku
then pure (True, Unsat)
Expand All @@ -709,7 +698,7 @@ equivalenceCheck' solvers branchesA branchesB opts = do
atomically $ readTVar knownUnsat >>= writeTVar knownUnsat . (props :)
pure (Qed (), False)
(_, EVM.Solvers.Unknown) -> pure (Timeout (), False)
(_, Error txt) -> internalError $ "solver returned: " <> (T.unpack txt) <> if opts.debug then "\n SMT file was: " <> filename <> "" else ""
(_, Error txt) -> internalError $ "solver returned: " <> (T.unpack txt)

-- Allows us to run it in parallel. Note that this (seems to) run it
-- from left-to-right, and with a max of K threads. This is in contrast to
Expand All @@ -718,7 +707,7 @@ equivalenceCheck' solvers branchesA branchesB opts = do
checkAll :: [(Set Prop)] -> UnsatCache -> Int -> IO [(EquivResult, Bool)]
checkAll input cache numproc = do
wrap <- pool numproc
parMapIO (wrap . (uncurry $ check cache)) $ zip input [1..]
parMapIO (wrap . (check cache)) input


-- Takes two branches and returns a set of props that will need to be
Expand Down
4 changes: 2 additions & 2 deletions test/test.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1723,7 +1723,7 @@ tests = testGroup "hevm"
}
}
|]
(_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint16)" [AbiUIntType 16])) [] defaultVeriOpts
(_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint16)" [AbiUIntType 16])) [] debugVeriOpts
msooseth marked this conversation as resolved.
Show resolved Hide resolved
putStrLn "DIV by zero is zero"
,
-- Somewhat tautological since we are asserting the precondition
Expand Down Expand Up @@ -1952,7 +1952,7 @@ tests = testGroup "hevm"
}
}
|]
(_, [Cex (_, a), Cex (_, b)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
(_, [Cex (_, a), Cex (_, b)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] debugVeriOpts
msooseth marked this conversation as resolved.
Show resolved Hide resolved
let ints = map (flip getVar "arg1") [a,b]
assertBool "0 must be one of the Cex-es" $ isJust $ List.elemIndex 0 ints
putStrLn "expected 2 counterexamples found, one Cex is the 0 value"
Expand Down