Skip to content

Commit d5f2d0e

Browse files
msoosethmsooseth
committed
Move unsat cache to Solver.hs in a central location
1 parent 9554b54 commit d5f2d0e

File tree

3 files changed

+73
-71
lines changed

3 files changed

+73
-71
lines changed

‎CHANGELOG.md

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -51,6 +51,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
5151
currently executed branch is in fact impossible. In these cases, unwind all
5252
frames and return a Revert with empty returndata.
5353
- More rewrite rules for PEq, PNeg, missing eqByte call, and distributivity for And
54+
- UNSAT cache is now in `Solvers.hs` and is therefore shared across all threads.
55+
Hence, it is now active even during branch queries.
5456

5557
## Fixed
5658
- We now try to simplify expressions fully before trying to cast them to a concrete value

‎src/EVM/Solvers.hs

Lines changed: 45 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ import Control.Monad.IO.Unlift
1616
import Data.Char (isSpace)
1717
import Data.Map (Map)
1818
import Data.Map qualified as Map
19+
import Data.Set (Set, isSubsetOf, fromList)
1920
import Data.Maybe (fromMaybe, isJust, fromJust)
2021
import Data.Either (isLeft)
2122
import Data.Text qualified as TStrict
@@ -67,7 +68,7 @@ data MultiSol = MultiSol
6768
}
6869

6970
-- | A script to be executed, a list of models to be extracted in the case of a sat result, and a channel where the result should be written
70-
data Task = TaskSingle SingleData | TaskMulti MultiData
71+
data Task = TaskSingle SingleData | TaskMulti MultiData | TaskAddCache [Prop]
7172

7273
data MultiData = MultiData
7374
{ smt2 :: SMT2
@@ -77,9 +78,14 @@ data MultiData = MultiData
7778

7879
data SingleData = SingleData
7980
{ smt2 :: SMT2
81+
, props :: [Prop]
8082
, resultChan :: Chan SMTResult
8183
}
8284

85+
-- returns True if a is a subset of any of the sets in b
86+
subsetAny :: [Prop] -> [Set Prop] -> Bool
87+
subsetAny a b = let s = fromList a in foldr (\bp acc -> acc || isSubsetOf s bp) False b
88+
8389
checkMulti :: SolverGroup -> Err SMT2 -> MultiSol -> IO (Maybe [W256])
8490
checkMulti (SolverGroup taskQueue) smt2 multiSol = do
8591
if isLeft smt2 then pure Nothing
@@ -92,7 +98,7 @@ checkMulti (SolverGroup taskQueue) smt2 multiSol = do
9298
readChan resChan
9399

94100
checkSatWithProps :: App m => SolverGroup -> [Prop] -> m (SMTResult, Err SMT2)
95-
checkSatWithProps (SolverGroup taskQueue) props = do
101+
checkSatWithProps sg props = do
96102
conf <- readConfig
97103
let psSimp = simplifyProps props
98104
if psSimp == [PBool False] then pure (Qed, Right mempty)
@@ -101,19 +107,20 @@ checkSatWithProps (SolverGroup taskQueue) props = do
101107
if isLeft smt2 then
102108
let err = getError smt2 in pure (Error err, Left err)
103109
else do
104-
res <- liftIO $ checkSat (SolverGroup taskQueue) smt2
110+
res <- liftIO $ checkSat sg smt2
105111
pure (res, Right (getNonError smt2))
106112

107-
checkSat :: SolverGroup -> Err SMT2 -> IO SMTResult
108-
checkSat (SolverGroup taskQueue) smt2 = do
109-
if isLeft smt2 then pure $ Error $ getError smt2
110-
else do
111-
-- prepare result channel
112-
resChan <- newChan
113-
-- send task to solver group
114-
writeChan taskQueue (TaskSingle (SingleData (getNonError smt2) resChan))
115-
-- collect result
116-
readChan resChan
113+
where
114+
checkSat :: SolverGroup -> Err SMT2 -> IO SMTResult
115+
checkSat (SolverGroup taskQueue) smt2 = do
116+
if isLeft smt2 then pure $ Error $ getError smt2
117+
else do
118+
-- prepare result channel
119+
resChan <- newChan
120+
-- send task to solver group
121+
writeChan taskQueue (TaskSingle (SingleData (getNonError smt2) props resChan))
122+
-- collect result
123+
readChan resChan
117124

118125
writeSMT2File :: SMT2 -> String -> IO ()
119126
writeSMT2File smt2 postfix =
@@ -128,7 +135,7 @@ withSolvers solver count threads timeout cont = do
128135
taskQueue <- liftIO newChan
129136
availableInstances <- liftIO newChan
130137
liftIO $ forM_ instances (writeChan availableInstances)
131-
orchestrate' <- toIO $ orchestrate taskQueue availableInstances 0
138+
orchestrate' <- toIO $ orchestrate taskQueue availableInstances [] 0
132139
orchestrateId <- liftIO $ forkIO orchestrate'
133140

134141
-- run continuation with task queue
@@ -139,15 +146,26 @@ withSolvers solver count threads timeout cont = do
139146
liftIO $ killThread orchestrateId
140147
pure res
141148
where
142-
orchestrate :: App m => Chan Task -> Chan SolverInstance -> Int -> m b
143-
orchestrate queue avail fileCounter = do
149+
orchestrate :: App m => Chan Task -> Chan SolverInstance -> [Set Prop] -> Int -> m b
150+
orchestrate queue avail knownUnsat fileCounter = do
151+
conf <- readConfig
144152
task <- liftIO $ readChan queue
145-
inst <- liftIO $ readChan avail
146-
runTask' <- case task of
147-
TaskSingle (SingleData smt2 r) -> toIO $ getOneSol smt2 r inst avail fileCounter
148-
TaskMulti (MultiData smt2 multiSol r) -> toIO $ getMultiSol smt2 multiSol r inst avail fileCounter
149-
_ <- liftIO $ forkIO runTask'
150-
orchestrate queue avail (fileCounter + 1)
153+
case task of
154+
TaskAddCache props -> do
155+
let knownUnsat' = (fromList props):knownUnsat
156+
when conf.debug $ liftIO $ putStrLn " adding UNSAT cache"
157+
orchestrate queue avail knownUnsat' fileCounter
158+
TaskSingle (SingleData _ props r) | subsetAny props knownUnsat -> do
159+
liftIO $ writeChan r Qed
160+
when conf.debug $ liftIO $ putStrLn " Qed found via cache!"
161+
orchestrate queue avail knownUnsat fileCounter
162+
_ -> do
163+
inst <- liftIO $ readChan avail
164+
runTask' <- case task of
165+
TaskSingle (SingleData smt2 props r) -> toIO $ getOneSol smt2 props r inst avail queue fileCounter
166+
TaskMulti (MultiData smt2 multiSol r) -> toIO $ getMultiSol smt2 multiSol r inst avail fileCounter
167+
_ <- liftIO $ forkIO runTask'
168+
orchestrate queue avail knownUnsat (fileCounter + 1)
151169

152170
getMultiSol :: forall m. (MonadIO m, ReadConfig m) => SMT2 -> MultiSol -> (Chan (Maybe [W256])) -> SolverInstance -> Chan SolverInstance -> Int -> m ()
153171
getMultiSol smt2@(SMT2 cmds cexvars _) multiSol r inst availableInstances fileCounter = do
@@ -211,8 +229,8 @@ getMultiSol smt2@(SMT2 cmds cexvars _) multiSol r inst availableInstances fileCo
211229
when conf.debug $ putStrLn $ "Unable to write SMT to solver: " <> (T.unpack err)
212230
writeChan r Nothing
213231

214-
getOneSol :: (MonadIO m, ReadConfig m) => SMT2 -> (Chan SMTResult) -> SolverInstance -> Chan SolverInstance -> Int -> m ()
215-
getOneSol smt2@(SMT2 cmds cexvars ps) r inst availableInstances fileCounter = do
232+
getOneSol :: (MonadIO m, ReadConfig m) => SMT2 -> [Prop] -> Chan SMTResult -> SolverInstance -> Chan SolverInstance -> (Chan Task) -> Int -> m ()
233+
getOneSol smt2@(SMT2 cmds cexvars ps) props r inst availableInstances task fileCounter = do
216234
conf <- readConfig
217235
let fuzzResult = tryCexFuzz ps conf.numCexFuzz
218236
liftIO $ do
@@ -232,7 +250,9 @@ getOneSol smt2@(SMT2 cmds cexvars ps) r inst availableInstances fileCounter = do
232250
sat <- sendLine inst "(check-sat)"
233251
res <- do
234252
case sat of
235-
"unsat" -> pure Qed
253+
"unsat" -> do
254+
writeChan task (TaskAddCache props)
255+
pure Qed
236256
"timeout" -> pure $ Unknown "Result timeout by SMT solver"
237257
"unknown" -> pure $ Unknown "Result unknown by SMT solver"
238258
"sat" -> Cex <$> getModel inst cexvars

‎src/EVM/SymExec.hs

Lines changed: 26 additions & 46 deletions
Original file line numberDiff line numberDiff line change
@@ -5,13 +5,12 @@ module EVM.SymExec where
55

66
import Control.Concurrent.Async (concurrently, mapConcurrently)
77
import Control.Concurrent.Spawn (parMapIO, pool)
8-
import Control.Concurrent.STM (TVar, readTVarIO, newTVarIO)
98
import Control.Monad (when, forM_, forM)
109
import Control.Monad.IO.Unlift
1110
import Control.Monad.Operational qualified as Operational
1211
import Control.Monad.ST (RealWorld, stToIO, ST)
1312
import Control.Monad.State.Strict (runStateT)
14-
import Data.Bifunctor (second, first)
13+
import Data.Bifunctor (second)
1514
import Data.ByteString (ByteString)
1615
import Data.ByteString qualified as BS
1716
import Data.Containers.ListUtils (nubOrd)
@@ -22,7 +21,7 @@ import Data.Maybe (fromMaybe, listToMaybe, mapMaybe)
2221
import Data.Map.Strict (Map)
2322
import Data.Map.Strict qualified as Map
2423
import Data.Map.Merge.Strict qualified as Map
25-
import Data.Set (Set, isSubsetOf)
24+
import Data.Set (Set)
2625
import Data.Set qualified as Set
2726
import Data.Text (Text)
2827
import Data.Text qualified as T
@@ -676,34 +675,33 @@ verify solvers opts preState maybepost = do
676675

677676
exprInter <- interpret (Fetch.oracle solvers opts.rpcInfo) opts.iterConf preState runExpr
678677
when conf.dumpExprs $ liftIO $ T.writeFile "unsimplified.expr" (formatExpr exprInter)
679-
liftIO $ do
680-
when conf.debug $ putStrLn " Simplifying expression"
678+
do
679+
when conf.debug $ liftIO $ putStrLn " Simplifying expression"
681680
let expr = if opts.simp then (Expr.simplify exprInter) else exprInter
682-
when conf.dumpExprs $ T.writeFile "simplified.expr" (formatExpr expr)
683-
when conf.dumpExprs $ T.writeFile "simplified-conc.expr" (formatExpr $ Expr.simplify $ mapExpr Expr.concKeccakOnePass expr)
681+
when conf.dumpExprs $ liftIO $ T.writeFile "simplified.expr" (formatExpr expr)
682+
when conf.dumpExprs $ liftIO $ T.writeFile "simplified-conc.expr" (formatExpr $ Expr.simplify $ mapExpr Expr.concKeccakOnePass expr)
684683
let flattened = flattenExpr expr
685-
when conf.debug $ do
684+
when conf.debug $ liftIO $ do
686685
printPartialIssues flattened ("the call " <> call)
687686
putStrLn $ " Exploration finished, " <> show (Expr.numBranches expr) <> " branch(es) to check in call " <> call
688687

689688
case maybepost of
690689
Nothing -> pure (expr, [Qed])
691-
Just post -> liftIO $ do
690+
Just post -> do
692691
let
693692
-- Filter out any leaves from `flattened` that can be statically shown to be safe
694693
tocheck = flip map flattened $ \leaf -> (toPropsFinal leaf preState.constraints post, leaf)
695-
withQueries = filter canBeSat tocheck <&> first (SMT.assertProps conf)
696-
when conf.debug $
697-
putStrLn $ " Checking for reachability of " <> show (length withQueries)
698-
<> " potential property violation(s) in call " <> call
694+
withQueries = filter canBeSat tocheck
695+
when conf.debug $ liftIO $ putStrLn $ " Checking for reachability of " <> show (length withQueries) <> " potential property violation(s) in call " <> call
699696

700697
-- Dispatch the remaining branches to the solver to check for violations
701-
results <- flip mapConcurrently withQueries $ \(query, leaf) -> do
702-
res <- checkSat solvers query
703-
when conf.debug $ putStrLn $ " SMT result: " <> show res
704-
pure (res, leaf)
705-
let cexs = filter (\(res, _) -> not . isQed $ res) results
706-
when conf.debug $ putStrLn $ " Found " <> show (length cexs) <> " potential counterexample(s) in call " <> call
698+
--
699+
results <- withRunInIO $ \env -> flip mapConcurrently withQueries $ \(query, leaf) -> do
700+
res <- env $ checkSatWithProps solvers query
701+
when conf.debug $ putStrLn $ " SMT result: " <> show (fst res)
702+
pure (fst res, leaf)
703+
let cexs = filter (not . isQed . fst) results
704+
when conf.debug $ liftIO $ putStrLn $ " Found " <> show (length cexs) <> " potential counterexample(s) in call " <> call
707705
pure $ if Prelude.null cexs then (expr, [Qed]) else (expr, fmap toVRes cexs)
708706
where
709707
getCallPrefix :: Expr Buf -> String
@@ -715,7 +713,7 @@ verify solvers opts preState maybepost = do
715713
canBeSat (a, _) = case a of
716714
[PBool False] -> False
717715
_ -> True
718-
toVRes :: (SMTResult, Expr End) -> VerifyResult
716+
toVRes :: (SMTResult , Expr End) -> VerifyResult
719717
toVRes (res, leaf) = case res of
720718
Cex model -> Cex (leaf, expandCex preState model)
721719
Unknown reason -> Unknown (reason, leaf)
@@ -732,8 +730,6 @@ expandCex prestate c = c { store = Map.union c.store concretePreStore }
732730
ConcreteStore _ -> True
733731
_ -> False
734732

735-
type UnsatCache = TVar [Set Prop]
736-
737733
data EqIssues = EqIssues
738734
{ res :: [(EquivResult, String)]
739735
, partials :: [Expr End]
@@ -835,43 +831,28 @@ equivalenceCheck' solvers branchesA branchesB create = do
835831
when conf.dumpEndStates $ forM_ (zip differingEndStates [(1::Integer)..]) (\(x, i) ->
836832
liftIO $ T.writeFile ("prop-checked-" <> show i <> ".prop") (T.pack $ show x))
837833

838-
knownUnsat <- liftIO $ newTVarIO []
839834
procs <- liftIO getNumProcessors
840-
newDifferences <- checkAll differingEndStates knownUnsat procs
835+
newDifferences <- checkAll differingEndStates procs
841836
let additionalIssues = EqIssues newDifferences mempty
842837
pure $ knownIssues <> additionalIssues
843838

844839
where
845-
-- we order the sets by size because this gives us more cache hits when
840+
-- we order the sets by size because this gives us more UNSAT cache hits when
846841
-- running our queries later on (since we rely on a subset check)
847842
sortBySize :: [(Set a, b)] -> [(Set a, b)]
848843
sortBySize = sortBy (\(a, _) (b, _) -> if Set.size a > Set.size b then Prelude.LT else Prelude.GT)
849844

850-
-- returns True if a is a subset of any of the sets in b
851-
subsetAny :: Set Prop -> [Set Prop] -> Bool
852-
subsetAny a b = foldr (\bp acc -> acc || isSubsetOf a bp) False b
853-
854-
-- checks for satisfiability of all the props in the provided set. skips
855-
-- the solver if we can determine unsatisfiability from the cache already
856-
-- the last element of the returned tuple indicates whether the cache was
857-
-- used or not
858-
check :: App m => UnsatCache -> Set Prop -> m EquivResult
859-
check knownUnsat props = do
860-
ku <- liftIO $ readTVarIO knownUnsat
861-
if subsetAny props ku then pure Qed
862-
else fst <$> checkSatWithProps solvers (Set.toList props)
863-
864845
-- Allows us to run the queries in parallel. Note that this (seems to) run it
865846
-- from left-to-right, and with a max of K threads. This is in contrast to
866847
-- mapConcurrently which would spawn as many threads as there are jobs, and
867848
-- run them in a random order. We ordered them correctly, though so that'd be bad
868-
checkAll :: (App m, MonadUnliftIO m) => [(Set Prop, String)] -> UnsatCache -> Int -> m [(EquivResult, String)]
869-
checkAll input cache numproc = withRunInIO $ \env -> do
849+
checkAll :: (App m, MonadUnliftIO m) => [(Set Prop, String)] -> Int -> m [(EquivResult, String)]
850+
checkAll input numproc = withRunInIO $ \env -> do
870851
wrap <- pool numproc
871852
parMapIO (runOne env wrap) input
872853
where
873854
runOne env wrap (props, meaning) = do
874-
res <- wrap (env $ check cache props)
855+
res <- wrap (env $ fst <$> checkSatWithProps solvers (Set.toList props))
875856
pure (res, meaning)
876857

877858
-- Takes two branches and returns a set of props that will need to be
@@ -996,10 +977,9 @@ both' f (x, y) = (f x, f y)
996977
produceModels :: App m => SolverGroup -> Expr End -> m [(Expr End, SMTResult)]
997978
produceModels solvers expr = do
998979
let flattened = flattenExpr expr
999-
withQueries conf = fmap (\e -> ((SMT.assertProps conf) . extractProps $ e, e)) flattened
1000-
conf <- readConfig
1001-
results <- liftIO $ (flip mapConcurrently) (withQueries conf) $ \(query, leaf) -> do
1002-
res <- checkSat solvers query
980+
withQueries = fmap (\e -> (extractProps e, e)) flattened
981+
results <- withRunInIO $ \runInIO -> (flip mapConcurrently) withQueries $ \(query, leaf) -> do
982+
(res, _) <- runInIO $ checkSatWithProps solvers query
1003983
pure (res, leaf)
1004984
pure $ fmap swap $ filter (\(res, _) -> not . isQed $ res) results
1005985

0 commit comments

Comments
 (0)