Skip to content

Commit 54eb53a

Browse files
msoosethmsooseth
authored
Merge pull request #652 from ethereum/fast-multi-sol
Faster multi-solution system
2 parents 7763256 + 24cdf3e commit 54eb53a

File tree

6 files changed

+153
-82
lines changed

6 files changed

+153
-82
lines changed

‎CHANGELOG.md

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
1616
and continue running, whenever possible
1717
- STATICCALL abstraction is now performed in case of symbolic arguments
1818
- Better error messages for JSON parsing
19-
- Multiple solutions are allowed for a single symbolic expression
19+
- Multiple solutions are allowed for a single symbolic expression, and they are
20+
generated via iterative calls to the SMT solver for quicker solving
2021
- Aliasing works much better for symbolic and concrete addresses
2122
- Constant propagation for symbolic values
2223

‎cli/cli.hs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -102,7 +102,7 @@ data Command w
102102
, solverThreads :: w ::: Maybe Natural <?> "Number of threads for each solver instance. Only respected for Z3 (default: 1)"
103103
, loopDetectionHeuristic :: w ::: LoopHeuristic <!> "StackBased" <?> "Which heuristic should be used to determine if we are in a loop: StackBased (default) or Naive"
104104
, noDecompose :: w ::: Bool <?> "Don't decompose storage slots into separate arrays"
105-
, maxBranch :: w ::: Int <!> "10" <?> "Max number of branches to explore when encountering a symbolic value (default: 10)"
105+
, maxBranch :: w ::: Int <!> "100" <?> "Max number of branches to explore when encountering a symbolic value (default: 100)"
106106
}
107107
| Equivalence -- prove equivalence between two programs
108108
{ codeA :: w ::: ByteString <?> "Bytecode of the first program"
@@ -123,7 +123,7 @@ data Command w
123123
, solverThreads :: w ::: Maybe Natural <?> "Number of threads for each solver instance. Only respected for Z3 (default: 1)"
124124
, loopDetectionHeuristic :: w ::: LoopHeuristic <!> "StackBased" <?> "Which heuristic should be used to determine if we are in a loop: StackBased (default) or Naive"
125125
, noDecompose :: w ::: Bool <?> "Don't decompose storage slots into separate arrays"
126-
, maxBranch :: w ::: Int <!> "10" <?> "Max number of branches to explore when encountering a symbolic value (default: 10)"
126+
, maxBranch :: w ::: Int <!> "100" <?> "Max number of branches to explore when encountering a symbolic value (default: 100)"
127127
}
128128
| Exec -- Execute a given program with specified env & calldata
129129
{ code :: w ::: Maybe ByteString <?> "Program bytecode"
@@ -173,7 +173,7 @@ data Command w
173173
, maxIterations :: w ::: Maybe Integer <?> "Number of times we may revisit a particular branching point. For no bound, set -1 (default: 5)"
174174
, loopDetectionHeuristic :: w ::: LoopHeuristic <!> "StackBased" <?> "Which heuristic should be used to determine if we are in a loop: StackBased (default) or Naive"
175175
, noDecompose :: w ::: Bool <?> "Don't decompose storage slots into separate arrays"
176-
, maxBranch :: w ::: Int <!> "10" <?> "Max number of branches to explore when encountering a symbolic value (default: 10)"
176+
, maxBranch :: w ::: Int <!> "100" <?> "Max number of branches to explore when encountering a symbolic value (default: 100)"
177177
, numCexFuzz :: w ::: Integer <!> "3" <?> "Number of fuzzing tries to do to generate a counterexample (default: 3)"
178178
, askSmtIterations :: w ::: Integer <!> "1" <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 1)"
179179
}
@@ -219,7 +219,7 @@ main = withUtf8 $ do
219219
, numCexFuzz = cmd.numCexFuzz
220220
, dumpTrace = cmd.trace
221221
, decomposeStorage = Prelude.not cmd.noDecompose
222-
, maxNumBranch = cmd.maxBranch
222+
, maxBranch = cmd.maxBranch
223223
} }
224224
case cmd of
225225
Version {} ->putStrLn getFullVersion

‎src/EVM.hs

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3021,7 +3021,9 @@ instance VMOps Symbolic where
30213021
Just concVals -> do
30223022
assign #result Nothing
30233023
case (length concVals) of
3024-
0 -> continue Nothing
3024+
-- zero solutions means that we are in a branch that's not possible. Revert.
3025+
-- TODO: stop execution of the EVM completely
3026+
0 -> finishFrame (FrameReverted (ConcreteBuf ""))
30253027
1 -> runOne $ head concVals
30263028
_ -> runBoth . PleaseRunBoth ewordExpr $ runMore concVals
30273029
Nothing -> do

‎src/EVM/Effects.hs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,7 @@ data Config = Config
4343
-- Returns Unknown if the Cex cannot be found via fuzzing
4444
, onlyCexFuzz :: Bool
4545
, decomposeStorage :: Bool
46-
, maxNumBranch :: Int
46+
, maxBranch :: Int
4747
}
4848
deriving (Show, Eq)
4949

@@ -57,7 +57,7 @@ defaultConfig = Config
5757
, numCexFuzz = 10
5858
, onlyCexFuzz = False
5959
, decomposeStorage = True
60-
, maxNumBranch = 10
60+
, maxBranch = 100
6161
}
6262

6363
-- Write to the console

‎src/EVM/Fetch.hs

Lines changed: 6 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -27,11 +27,8 @@ import Numeric.Natural (Natural)
2727
import System.Environment (lookupEnv, getEnvironment)
2828
import System.Process
2929
import Control.Monad.IO.Class
30-
import Control.Monad (when)
3130
import EVM.Effects
3231
import qualified EVM.Expr as Expr
33-
import Numeric (showHex,readHex)
34-
import Data.Bits ((.&.))
3532

3633
-- | Abstract representation of an RPC fetch request
3734
data RpcQuery a where
@@ -252,40 +249,18 @@ getSolutions solvers symExprPreSimp numBytes pathconditions = do
252249
conf <- readConfig
253250
liftIO $ do
254251
let symExpr = Expr.concKeccakSimpExpr symExprPreSimp
255-
when conf.debug $ putStrLn $ "Collecting solutions to symbolic query: " <> show symExpr
256-
ret <- collectSolutions [] conf.maxNumBranch symExpr pathconditions conf
252+
-- when conf.debug $ putStrLn $ "Collecting solutions to symbolic query: " <> show symExpr
253+
ret <- collectSolutions symExpr pathconditions conf
257254
case ret of
258255
Nothing -> pure Nothing
259256
Just r -> case length r of
260257
0 -> pure Nothing
261258
_ -> pure $ Just r
262259
where
263-
createHexValue k =
264-
let hexString = concat (replicate k "ff")
265-
in fst . head $ readHex hexString
266-
collectSolutions :: [W256] -> Int -> Expr EWord -> Prop -> Config -> IO (Maybe [W256])
267-
collectSolutions vals maxSols symExpr conds conf = do
268-
if (length vals > maxSols) then pure Nothing
269-
else
270-
checkSat solvers (assertProps conf [(PEq (Var "addrQuery") symExpr) .&& conds]) >>= \case
271-
Sat (SMTCex vars _ _ _ _ _) -> case (Map.lookup (Var "addrQuery") vars) of
272-
Just v -> do
273-
let hexMask = createHexValue numBytes
274-
maskedVal = v .&. hexMask
275-
cond = (And symExpr (Lit hexMask)) ./= Lit maskedVal
276-
newConds = Expr.simplifyProp $ PAnd conds cond
277-
showedVal = "val: 0x" <> (showHex maskedVal "")
278-
when conf.debug $ putStrLn $ "Got one solution to symbolic query," <> showedVal <> " now have " <>
279-
show (length vals + 1) <> " solution(s), max is: " <> show maxSols
280-
collectSolutions (maskedVal:vals) maxSols symExpr newConds conf
281-
_ -> internalError "No solution to symbolic query"
282-
Unsat -> do
283-
when conf.debug $ putStrLn "No more solution(s) to symbolic query."
284-
pure $ Just vals
285-
-- Error or timeout, we need to be conservative
286-
res -> do
287-
when conf.debug $ putStrLn $ "Symbolic query result is neither SAT nor UNSAT:" <> show res
288-
pure Nothing
260+
collectSolutions :: Expr EWord -> Prop -> Config -> IO (Maybe [W256])
261+
collectSolutions symExpr conds conf = do
262+
let smt2 = assertProps conf [(PEq (Var "multiQueryVar") symExpr) .&& conds]
263+
checkMulti solvers smt2 $ MultiSol { maxSols = conf.maxBranch , numBytes = numBytes , var = "multiQueryVar" }
289264

290265
-- | Checks which branches are satisfiable, checking the pathconditions for consistency
291266
-- if the third argument is true.

‎src/EVM/Solvers.hs

Lines changed: 136 additions & 43 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ import Data.Map (Map)
1818
import Data.Map qualified as Map
1919
import Data.Maybe (fromMaybe, isJust, fromJust)
2020
import Data.Either (isLeft)
21+
import Data.Text qualified as TStrict
2122
import Data.Text.Lazy (Text)
2223
import Data.Text.Lazy qualified as T
2324
import Data.Text.Lazy.IO qualified as T
@@ -26,9 +27,12 @@ import System.Process (createProcess, cleanupProcess, proc, ProcessHandle, std_i
2627
import Witch (into)
2728
import EVM.Effects
2829
import EVM.Fuzz (tryCexFuzz)
30+
import Numeric (readHex)
31+
import Data.Bits ((.&.))
32+
import Numeric (showHex)
2933

3034
import EVM.SMT
31-
import EVM.Types (W256, Expr(AbstractBuf), internalError, Err, getError, getNonError)
35+
import EVM.Types
3236

3337
-- | Supported solvers
3438
data Solver
@@ -55,9 +59,23 @@ data SolverInstance = SolverInstance
5559
-- | A channel representing a group of solvers
5660
newtype SolverGroup = SolverGroup (Chan Task)
5761

62+
data MultiSol = MultiSol
63+
{ maxSols :: Int
64+
, numBytes :: Int
65+
, var :: String
66+
}
67+
5868
-- | 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
59-
data Task = Task
60-
{ script :: SMT2
69+
data Task = TaskSingle SingleData | TaskMulti MultiData
70+
71+
data MultiData = MultiData
72+
{ smt2 :: SMT2
73+
, multiSol :: MultiSol
74+
, resultChan :: Chan (Maybe [W256])
75+
}
76+
77+
data SingleData = SingleData
78+
{ smt2 :: SMT2
6179
, resultChan :: Chan CheckSatResult
6280
}
6381

@@ -77,21 +95,32 @@ isUnsat :: CheckSatResult -> Bool
7795
isUnsat Unsat = True
7896
isUnsat _ = False
7997

98+
checkMulti :: SolverGroup -> Err SMT2 -> MultiSol -> IO (Maybe [W256])
99+
checkMulti (SolverGroup taskQueue) smt2 multiSol = do
100+
if isLeft smt2 then pure Nothing
101+
else do
102+
-- prepare result channel
103+
resChan <- newChan
104+
-- send task to solver group
105+
writeChan taskQueue (TaskMulti (MultiData (getNonError smt2) multiSol resChan))
106+
-- collect result
107+
readChan resChan
108+
80109
checkSat :: SolverGroup -> Err SMT2 -> IO CheckSatResult
81-
checkSat (SolverGroup taskQueue) script = do
82-
if isLeft script then pure $ Error $ getError script
110+
checkSat (SolverGroup taskQueue) smt2 = do
111+
if isLeft smt2 then pure $ Error $ getError smt2
83112
else do
84113
-- prepare result channel
85114
resChan <- newChan
86115
-- send task to solver group
87-
writeChan taskQueue (Task (getNonError script) resChan)
116+
writeChan taskQueue (TaskSingle (SingleData (getNonError smt2) resChan))
88117
-- collect result
89118
readChan resChan
90119

91-
writeSMT2File :: SMT2 -> Int -> IO ()
92-
writeSMT2File smt2 count =
120+
writeSMT2File :: SMT2 -> String -> IO ()
121+
writeSMT2File smt2 postfix =
93122
let content = formatSMT2 smt2 <> "\n\n(check-sat)"
94-
in T.writeFile ("query-" <> (show count) <> ".smt2") content
123+
in T.writeFile ("query-" <> postfix <> ".smt2") content
95124

96125
withSolvers :: App m => Solver -> Natural -> Natural -> Maybe Natural -> (SolverGroup -> m a) -> m a
97126
withSolvers solver count threads timeout cont = do
@@ -116,43 +145,107 @@ withSolvers solver count threads timeout cont = do
116145
orchestrate queue avail fileCounter = do
117146
task <- liftIO $ readChan queue
118147
inst <- liftIO $ readChan avail
119-
runTask' <- toIO $ runTask task inst avail fileCounter
148+
runTask' <- case task of
149+
TaskSingle (SingleData smt2 r) -> toIO $ getOneSol smt2 r inst avail fileCounter
150+
TaskMulti (MultiData smt2 multiSol r) -> toIO $ getMultiSol smt2 multiSol r inst avail fileCounter
120151
_ <- liftIO $ forkIO runTask'
121152
orchestrate queue avail (fileCounter + 1)
122153

123-
runTask :: (MonadIO m, ReadConfig m) => Task -> SolverInstance -> Chan SolverInstance -> Int -> m ()
124-
runTask (Task smt2@(SMT2 cmds cexvars ps) r) inst availableInstances fileCounter = do
154+
getMultiSol :: forall m. (MonadIO m, ReadConfig m) => SMT2 -> MultiSol -> (Chan (Maybe [W256])) -> SolverInstance -> Chan SolverInstance -> Int -> m ()
155+
getMultiSol smt2@(SMT2 cmds cexvars _) multiSol r inst availableInstances fileCounter = do
156+
conf <- readConfig
157+
when conf.dumpQueries $ liftIO $ writeSMT2File smt2 (show fileCounter)
158+
-- reset solver and send all lines of provided script
159+
out <- liftIO $ sendScript inst ("(reset)" : cmds)
160+
case out of
161+
Left err -> liftIO $ do
162+
when conf.debug $ putStrLn $ "Unable to write SMT to solver: " <> (T.unpack err)
163+
writeChan r Nothing
164+
Right _ -> do
165+
sat <- liftIO $ sendLine inst "(check-sat)"
166+
subRun [] smt2 sat
167+
-- put the instance back in the list of available instances
168+
liftIO $ writeChan availableInstances inst
169+
where
170+
createHexValue k =
171+
let hexString = concat (replicate k "ff")
172+
in fst . head $ readHex hexString
173+
subRun :: (MonadIO m, ReadConfig m) => [W256] -> SMT2 -> Text -> m ()
174+
subRun vals fullSmt sat = do
125175
conf <- readConfig
126-
let fuzzResult = tryCexFuzz ps conf.numCexFuzz
127-
liftIO $ do
128-
when (conf.dumpQueries) $ writeSMT2File smt2 fileCounter
129-
if (isJust fuzzResult)
130-
then do
131-
when (conf.debug) $ putStrLn $ " Cex found via fuzzing:" <> (show fuzzResult)
132-
writeChan r (Sat $ fromJust fuzzResult)
133-
else if not conf.onlyCexFuzz then do
134-
-- reset solver and send all lines of provided script
135-
out <- sendScript inst (SMT2 ("(reset)" : cmds) mempty ps)
136-
case out of
137-
-- if we got an error then return it
138-
Left e -> writeChan r (Error $ "Error while writing SMT to solver: " <> T.unpack e)
139-
-- otherwise call (check-sat), parse the result, and send it down the result channel
140-
Right () -> do
141-
sat <- sendLine inst "(check-sat)"
142-
res <- do
143-
case sat of
144-
"unsat" -> pure Unsat
145-
"timeout" -> pure $ Unknown "Result timeout by SMT solver"
146-
"unknown" -> pure $ Unknown "Result unknown by SMT solver"
147-
"sat" -> Sat <$> getModel inst cexvars
148-
_ -> pure . Error $ "Unable to parse SMT solver output: " <> T.unpack sat
149-
writeChan r res
176+
case sat of
177+
"unsat" -> liftIO $ do
178+
when conf.debug $ putStrLn $ "No more solutions to query, returning: " <> show vals
179+
liftIO $ writeChan r (Just vals)
180+
"timeout" -> liftIO $ do
181+
when conf.debug $ putStrLn "Timeout inside SMT solver."
182+
writeChan r Nothing
183+
"unknown" -> liftIO $ do
184+
when conf.debug $ putStrLn "Unknown result by SMT solver."
185+
writeChan r Nothing
186+
"sat" -> do
187+
if length vals >= multiSol.maxSols then liftIO $ do
188+
when conf.debug $ putStrLn "Too many solutions to symbolic query."
189+
writeChan r Nothing
150190
else do
151-
when (conf.debug) $ putStrLn "Fuzzing failed to find a Cex, not trying SMT due to onlyCexFuzz"
152-
writeChan r $ Error "Option onlyCexFuzz enabled, not running SMT"
153-
154-
-- put the instance back in the list of available instances
155-
writeChan availableInstances inst
191+
cex <- liftIO $ getModel inst cexvars
192+
case Map.lookup (Var (TStrict.pack multiSol.var)) cex.vars of
193+
Just v -> do
194+
let hexMask = createHexValue multiSol.numBytes
195+
maskedVal = v .&. hexMask
196+
toSMT n = show (into n :: Integer)
197+
maskedVar = "(bvand " <> multiSol.var <> " (_ bv" <> toSMT hexMask <> " 256))"
198+
restrict = "(assert (not (= " <> maskedVar <> " (_ bv" <> toSMT maskedVal <> " 256))))"
199+
newSmt = fullSmt <> SMT2 [(fromString restrict)] mempty mempty
200+
when conf.debug $ liftIO $ putStrLn $ "Got one solution to symbolic query, val: 0x" <> (showHex maskedVal "") <>
201+
" now have " <> show (length vals + 1) <> " solution(s), max is: " <> show multiSol.maxSols
202+
when conf.dumpQueries $ liftIO $ writeSMT2File newSmt (show fileCounter <> "-sol" <> show (length vals))
203+
out <- liftIO $ sendLine inst (T.pack restrict)
204+
case out of
205+
"success" -> do
206+
out2 <- liftIO $ sendLine inst (T.pack "(check-sat)")
207+
subRun (maskedVal:vals) newSmt out2
208+
err -> liftIO $ do
209+
when conf.debug $ putStrLn $ "Unable to write SMT to solver: " <> (T.unpack err)
210+
writeChan r Nothing
211+
Nothing -> internalError $ "variable " <> multiSol.var <> " not part of model (i.e. cex) ... that's not possible"
212+
err -> liftIO $ do
213+
when conf.debug $ putStrLn $ "Unable to write SMT to solver: " <> (T.unpack err)
214+
writeChan r Nothing
215+
216+
getOneSol :: (MonadIO m, ReadConfig m) => SMT2 -> (Chan CheckSatResult) -> SolverInstance -> Chan SolverInstance -> Int -> m ()
217+
getOneSol smt2@(SMT2 cmds cexvars ps) r inst availableInstances fileCounter = do
218+
conf <- readConfig
219+
let fuzzResult = tryCexFuzz ps conf.numCexFuzz
220+
liftIO $ do
221+
when (conf.dumpQueries) $ writeSMT2File smt2 (show fileCounter)
222+
if (isJust fuzzResult)
223+
then do
224+
when (conf.debug) $ putStrLn $ " Cex found via fuzzing:" <> (show fuzzResult)
225+
writeChan r (Sat $ fromJust fuzzResult)
226+
else if Prelude.not conf.onlyCexFuzz then do
227+
-- reset solver and send all lines of provided script
228+
out <- sendScript inst ("(reset)" : cmds)
229+
case out of
230+
-- if we got an error then return it
231+
Left e -> writeChan r (Error $ "Error while writing SMT to solver: " <> T.unpack e)
232+
-- otherwise call (check-sat), parse the result, and send it down the result channel
233+
Right () -> do
234+
sat <- sendLine inst "(check-sat)"
235+
res <- do
236+
case sat of
237+
"unsat" -> pure Unsat
238+
"timeout" -> pure $ EVM.Solvers.Unknown "Result timeout by SMT solver"
239+
"unknown" -> pure $ EVM.Solvers.Unknown "Result unknown by SMT solver"
240+
"sat" -> Sat <$> getModel inst cexvars
241+
_ -> pure . Error $ "Unable to parse SMT solver output: " <> T.unpack sat
242+
writeChan r res
243+
else do
244+
when (conf.debug) $ putStrLn "Fuzzing failed to find a Cex, not trying SMT due to onlyCexFuzz"
245+
writeChan r $ Error "Option onlyCexFuzz enabled, not running SMT"
246+
247+
-- put the instance back in the list of available instances
248+
writeChan availableInstances inst
156249

157250
getModel :: SolverInstance -> CexVars -> IO SMTCex
158251
getModel inst cexvars = do
@@ -291,8 +384,8 @@ stopSolver :: SolverInstance -> IO ()
291384
stopSolver (SolverInstance _ stdin stdout process) = cleanupProcess (Just stdin, Just stdout, Nothing, process)
292385

293386
-- | Sends a list of commands to the solver. Returns the first error, if there was one.
294-
sendScript :: SolverInstance -> SMT2 -> IO (Either Text ())
295-
sendScript solver (SMT2 cmds _ _) = do
387+
sendScript :: SolverInstance -> [Builder] -> IO (Either Text ())
388+
sendScript solver cmds = do
296389
let sexprs = splitSExpr $ fmap toLazyText cmds
297390
go sexprs
298391
where

0 commit comments

Comments
 (0)