diff --git a/src/EVM/Format.hs b/src/EVM/Format.hs index 7b24a6fe9..c8b8db08c 100644 --- a/src/EVM/Format.hs +++ b/src/EVM/Format.hs @@ -5,6 +5,7 @@ module EVM.Format ( formatExpr , formatSomeExpr , formatPartial + , formatProp , contractNamePart , contractPathPart , showError diff --git a/src/EVM/SMT.hs b/src/EVM/SMT.hs index b199031e2..2e5d46e7a 100644 --- a/src/EVM/SMT.hs +++ b/src/EVM/SMT.hs @@ -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) @@ -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] + 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 @@ -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] 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 @@ -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 @@ -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) @@ -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 @@ -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 @@ -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 @@ -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 diff --git a/src/EVM/Solvers.hs b/src/EVM/Solvers.hs index 310f1743f..23dbd83b3 100644 --- a/src/EVM/Solvers.hs +++ b/src/EVM/Solvers.hs @@ -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 @@ -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) @@ -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)) @@ -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" + _ <- sendScript inst refinedSMT2 sat2 <- sendLine inst "(check-sat)" case sat2 of "unsat" -> pure Unsat @@ -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 diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs index 5a02a45d9..d198a891a 100644 --- a/src/EVM/SymExec.hs +++ b/src/EVM/SymExec.hs @@ -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) @@ -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) @@ -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 @@ -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) @@ -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 @@ -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