Skip to content

Commit be6cf4e

Browse files
msoosethmsooseth
committed
Also have abort for Solvers
Now immediate crash No deadlocks? Now it works Fixing test Update Cleanup Cleanup Cleanup
1 parent 3df93f2 commit be6cf4e

File tree

4 files changed

+101
-53
lines changed

4 files changed

+101
-53
lines changed

‎src/EVM/Solvers.hs‎

Lines changed: 91 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,9 @@ import Prelude hiding (LT, GT)
99
import GHC.Natural
1010
import GHC.IO.Handle (Handle, hFlush, hSetBuffering, BufferMode(..))
1111
import Control.Concurrent.Chan (Chan, newChan, writeChan, readChan)
12-
import Control.Concurrent (forkIO, killThread)
13-
import Control.Concurrent.STM (writeTChan, newTChan, TChan, tryReadTChan, atomically)
12+
import Control.Concurrent (forkIO, killThread, ThreadId, myThreadId)
13+
import Control.Concurrent.STM (writeTChan, newTChan, TChan, tryReadTChan, atomically, readTVar, readTVarIO, modifyTVar', check)
14+
import Control.Concurrent.STM.TVar (TVar, newTVarIO)
1415
import Control.Monad
1516
import Control.Monad.State.Strict
1617
import Control.Monad.IO.Unlift
@@ -61,7 +62,10 @@ data SolverInstance = SolverInstance
6162
}
6263

6364
-- | A channel representing a group of solvers
64-
newtype SolverGroup = SolverGroup (Chan Task)
65+
data SolverGroup = SolverGroup
66+
{ taskQueue :: Chan Task
67+
, shouldAbort :: TVar Bool
68+
}
6569

6670
data MultiSol = MultiSol
6771
{ maxSols :: Int
@@ -92,13 +96,13 @@ supersetAny :: Set Prop -> [Set Prop] -> Bool
9296
supersetAny a bs = any (`isSubsetOf` a) bs
9397

9498
checkMulti :: SolverGroup -> Err SMT2 -> MultiSol -> IO (Maybe [W256])
95-
checkMulti (SolverGroup taskq) smt2 multiSol = do
99+
checkMulti sg smt2 multiSol = do
96100
if isLeft smt2 then pure Nothing
97101
else do
98102
-- prepare result channel
99103
resChan <- newChan
100104
-- send task to solver group
101-
writeChan taskq (TaskMulti (MultiData (getNonError smt2) multiSol resChan))
105+
writeChan sg.taskQueue (TaskMulti (MultiData (getNonError smt2) multiSol resChan))
102106
-- collect result
103107
readChan resChan
104108

@@ -115,13 +119,13 @@ checkSatWithProps sg props = do
115119

116120
-- When props is Nothing, the cache will not be filled or used
117121
checkSat :: SolverGroup -> Maybe [Prop] -> Err SMT2 -> IO SMTResult
118-
checkSat (SolverGroup taskq) props smt2 = do
122+
checkSat sg props smt2 = do
119123
if isLeft smt2 then pure $ Error $ getError smt2
120124
else do
121125
-- prepare result channel
122126
resChan <- newChan
123127
-- send task to solver group
124-
writeChan taskq (TaskSingle (SingleData (getNonError smt2) props resChan))
128+
writeChan sg.taskQueue (TaskSingle (SingleData (getNonError smt2) props resChan))
125129
-- collect result
126130
readChan resChan
127131

@@ -139,44 +143,91 @@ withSolvers solver count threads timeout cont = do
139143
taskq <- liftIO newChan
140144
cacheq <- liftIO . atomically $ newTChan
141145
availableInstances <- liftIO newChan
146+
shouldAbort <- liftIO $ newTVarIO False
147+
runningThreads <- liftIO $ newTVarIO ([] :: [(ThreadId, Task)])
142148
liftIO $ forM_ instances (writeChan availableInstances)
143-
orchestrate' <- toIO $ orchestrate taskq cacheq availableInstances [] 0
149+
150+
-- Spawn orchestration thread
151+
orchestrate' <- toIO $ orchestrate taskq cacheq availableInstances shouldAbort runningThreads [] 0
144152
orchestrateId <- liftIO $ forkIO orchestrate'
145153

154+
-- Spawn watcher thread that kills solver threads when abort flag is set
155+
abortWatcher' <- toIO $ abortWatcher shouldAbort runningThreads
156+
abortWatcherId <- liftIO $ forkIO abortWatcher'
157+
146158
-- run continuation with task queue
147-
res <- cont (SolverGroup taskq)
159+
res <- cont (SolverGroup taskq shouldAbort)
148160

149161
-- cleanup and return results
150162
liftIO $ mapM_ (stopSolver) instances
151163
liftIO $ killThread orchestrateId
164+
liftIO $ killThread abortWatcherId
152165
pure res
153166
where
154-
orchestrate :: App m => Chan Task -> TChan CacheEntry -> Chan SolverInstance -> [Set Prop] -> Int -> m b
155-
orchestrate taskq cacheq avail knownUnsat fileCounter = do
167+
-- Watcher thread that blocks until abort flag is set, then kills all solver threads
168+
abortWatcher :: App m => TVar Bool -> TVar [(ThreadId, Task)] -> m ()
169+
abortWatcher abortFlag runningThreads = do
156170
conf <- readConfig
157-
mx <- liftIO . atomically $ tryReadTChan cacheq
158-
case mx of
159-
Just (CacheEntry props) -> do
160-
let knownUnsat' = (fromList props):knownUnsat
161-
when conf.debug $ liftIO $ putStrLn " adding UNSAT cache"
162-
orchestrate taskq cacheq avail knownUnsat' fileCounter
163-
Nothing -> do
164-
task <- liftIO $ readChan taskq
171+
when conf.earlyAbort $ do
172+
-- Block until abort flag becomes True
173+
liftIO . atomically $ do
174+
abort <- readTVar abortFlag
175+
check abort
176+
-- Kill all running solver threads immediately and write errors to their result channels
177+
tidTasks <- liftIO $ readTVarIO runningThreads
178+
liftIO $ forM_ tidTasks $ \(tid, task) -> do
179+
killThread tid
180+
-- Write error result to the task's result channel
165181
case task of
166-
TaskSingle (SingleData _ props r) | isJust props && supersetAny (fromList (fromJust props)) knownUnsat -> do
167-
liftIO $ writeChan r Qed
168-
when conf.debug $ liftIO $ putStrLn " Qed found via cache!"
169-
orchestrate taskq cacheq avail knownUnsat fileCounter
170-
_ -> do
171-
inst <- liftIO $ readChan avail
172-
runTask' <- case task of
173-
TaskSingle (SingleData smt2 props r) -> toIO $ getOneSol smt2 props r cacheq inst avail fileCounter
174-
TaskMulti (MultiData smt2 multiSol r) -> toIO $ getMultiSol smt2 multiSol r inst avail fileCounter
175-
_ <- liftIO $ forkIO runTask'
176-
orchestrate taskq cacheq avail knownUnsat (fileCounter + 1)
177-
178-
getMultiSol :: forall m. (MonadIO m, ReadConfig m) => SMT2 -> MultiSol -> (Chan (Maybe [W256])) -> SolverInstance -> Chan SolverInstance -> Int -> m ()
179-
getMultiSol smt2@(SMT2 cmds cexvars _) multiSol r inst availableInstances fileCounter = do
182+
TaskSingle (SingleData _ _ r) -> writeChan r (Error "Aborted due to early abort")
183+
TaskMulti (MultiData _ _ r) -> writeChan r Nothing
184+
liftIO . atomically $ modifyTVar' runningThreads (const [])
185+
when conf.debug $ liftIO $ putStrLn $ " [Abort Watcher] Killed " <> show (length tidTasks) <> " running solver thread(s) due to early abort"
186+
187+
orchestrate :: App m => Chan Task -> TChan CacheEntry -> Chan SolverInstance -> TVar Bool -> TVar [(ThreadId, Task)] -> [Set Prop] -> Int -> m b
188+
orchestrate taskq cacheq avail abortFlag runningThreads knownUnsat fileCounter = do
189+
conf <- readConfig
190+
-- Check if we should abort early
191+
abort <- liftIO $ readTVarIO abortFlag
192+
if (conf.earlyAbort && abort) then drainTasks taskq
193+
else do
194+
mx <- liftIO . atomically $ tryReadTChan cacheq
195+
case mx of
196+
Just (CacheEntry props) -> do
197+
let knownUnsat' = (fromList props):knownUnsat
198+
when conf.debug $ liftIO $ putStrLn " adding UNSAT cache"
199+
orchestrate taskq cacheq avail abortFlag runningThreads knownUnsat' fileCounter
200+
Nothing -> do
201+
task <- liftIO $ readChan taskq
202+
case task of
203+
TaskSingle (SingleData _ props r) | isJust props && supersetAny (fromList (fromJust props)) knownUnsat -> do
204+
liftIO $ writeChan r Qed
205+
when conf.debug $ liftIO $ putStrLn " Qed found via cache!"
206+
orchestrate taskq cacheq avail abortFlag runningThreads knownUnsat fileCounter
207+
_ -> do
208+
inst <- liftIO $ readChan avail
209+
runTask' <- case task of
210+
TaskSingle (SingleData smt2 props r) -> toIO $ getOneSol smt2 props r cacheq inst avail runningThreads fileCounter
211+
TaskMulti (MultiData smt2 multiSol r) -> toIO $ getMultiSol smt2 multiSol r inst avail runningThreads fileCounter
212+
tid <- liftIO $ forkIO runTask'
213+
liftIO . atomically $ modifyTVar' runningThreads ((tid, task):)
214+
orchestrate taskq cacheq avail abortFlag runningThreads knownUnsat (fileCounter + 1)
215+
216+
-- Drain any pending tasks from the queue and return error results
217+
drainTasks :: App m => Chan Task -> m b
218+
drainTasks taskq = do
219+
conf <- readConfig
220+
when conf.debug $ liftIO $ putStrLn " [Orchestrate] Draining pending tasks due to early abort"
221+
forever $ do
222+
task <- liftIO $ readChan taskq
223+
case task of
224+
TaskSingle (SingleData _ _ r) -> liftIO $ writeChan r (Error "Aborted due to early abort")
225+
TaskMulti (MultiData _ _ r) -> liftIO $ writeChan r Nothing
226+
227+
getMultiSol :: forall m. (MonadIO m, ReadConfig m) => SMT2 -> MultiSol -> (Chan (Maybe [W256])) -> SolverInstance -> Chan SolverInstance -> TVar [(ThreadId, Task)] -> Int -> m ()
228+
getMultiSol smt2@(SMT2 cmds cexvars _) multiSol r inst availableInstances runningThreads fileCounter = do
229+
tid <- liftIO myThreadId
230+
let cleanup = liftIO . atomically $ modifyTVar' runningThreads (filter (\(t, _) -> t /= tid))
180231
conf <- readConfig
181232
when conf.dumpQueries $ liftIO $ writeSMT2File smt2 "." (show fileCounter)
182233
-- reset solver and send all lines of provided script
@@ -195,6 +246,8 @@ getMultiSol smt2@(SMT2 cmds cexvars _) multiSol r inst availableInstances fileCo
195246
subRun [] smt2 sat
196247
-- put the instance back in the list of available instances
197248
liftIO $ writeChan availableInstances inst
249+
-- remove thread from running threads list
250+
cleanup
198251
where
199252
maskFromBytesCount k
200253
| k <= 32 = (2 ^ (8 * k) - 1)
@@ -243,9 +296,10 @@ getMultiSol smt2@(SMT2 cmds cexvars _) multiSol r inst availableInstances fileCo
243296
when conf.debug $ putStrLn $ "Unable to write SMT to solver: " <> (T.unpack err)
244297
writeChan r Nothing
245298

246-
getOneSol :: (MonadIO m, ReadConfig m) => SMT2 -> Maybe [Prop] -> Chan SMTResult -> TChan CacheEntry -> SolverInstance -> Chan SolverInstance -> Int -> m ()
247-
getOneSol smt2@(SMT2 cmds cexvars _) props r cacheq inst availableInstances fileCounter = do
299+
getOneSol :: (MonadIO m, ReadConfig m) => SMT2 -> Maybe [Prop] -> Chan SMTResult -> TChan CacheEntry -> SolverInstance -> Chan SolverInstance -> TVar [(ThreadId, Task)] -> Int -> m ()
300+
getOneSol smt2@(SMT2 cmds cexvars _) props r cacheq inst availableInstances runningThreads fileCounter = do
248301
conf <- readConfig
302+
tid <- liftIO myThreadId
249303
liftIO $ do
250304
when (conf.dumpQueries) $ writeSMT2File smt2 "." (show fileCounter)
251305
-- reset solver and send all lines of provided script
@@ -275,6 +329,8 @@ getOneSol smt2@(SMT2 cmds cexvars _) props r cacheq inst availableInstances file
275329

276330
-- put the instance back in the list of available instances
277331
writeChan availableInstances inst
332+
-- remove thread from running threads list
333+
liftIO . atomically $ modifyTVar' runningThreads (filter (\(t, _) -> t /= tid))
278334

279335
dumpUnsolved :: SMT2 -> Int -> Maybe FilePath -> IO ()
280336
dumpUnsolved fullSmt fileCounter dump = do

‎src/EVM/SymExec.hs‎

Lines changed: 7 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -630,8 +630,7 @@ getExprEmptyStore solvers c signature' concreteArgs opts = do
630630
conf <- readConfig
631631
calldata <- mkCalldata signature' concreteArgs
632632
preState <- liftIO $ stToIO $ loadEmptySymVM (RuntimeCode (ConcreteRuntimeCode c)) (Lit 0) calldata
633-
shouldAbort <- liftIO $ newTVarIO False
634-
paths <- interpret (Fetch.oracle solvers Nothing opts.rpcInfo) opts.iterConf preState shouldAbort runExpr pure
633+
paths <- interpret (Fetch.oracle solvers Nothing opts.rpcInfo) opts.iterConf preState solvers.shouldAbort runExpr pure
635634
if conf.simp then (pure $ map Expr.simplify paths) else pure paths
636635

637636
-- Used only in testing
@@ -647,8 +646,7 @@ getExpr solvers c signature' concreteArgs opts = do
647646
conf <- readConfig
648647
calldata <- mkCalldata signature' concreteArgs
649648
preState <- liftIO $ stToIO $ abstractVM calldata c Nothing False
650-
shouldAbort <- liftIO $ newTVarIO False
651-
paths <- interpret (Fetch.oracle solvers Nothing opts.rpcInfo) opts.iterConf preState shouldAbort runExpr pure
649+
paths <- interpret (Fetch.oracle solvers Nothing opts.rpcInfo) opts.iterConf preState solvers.shouldAbort runExpr pure
652650
if conf.simp then (pure $ map Expr.simplify paths) else pure paths
653651

654652
{- | Checks if an assertion violation has been encountered
@@ -733,8 +731,7 @@ exploreContract solvers theCode signature' concreteArgs opts maybepre = do
733731
calldata <- mkCalldata signature' concreteArgs
734732
preState <- liftIO $ stToIO $ abstractVM calldata theCode maybepre False
735733
let fetcher = Fetch.oracle solvers Nothing opts.rpcInfo
736-
shouldAbort <- liftIO $ newTVarIO False
737-
executeVM fetcher opts.iterConf preState shouldAbort pure
734+
executeVM fetcher opts.iterConf preState solvers.shouldAbort pure
738735

739736
-- | Stepper that parses the result of Stepper.runFully into an Expr End
740737
runExpr :: Stepper.Stepper Symbolic (Expr End)
@@ -844,8 +841,7 @@ verifyInputsWithHandler solvers opts fetcher preState post cexHandler = do
844841
putStrLn $ " Keccak preimages in state: " <> (show $ length preState.keccakPreImgs)
845842
putStrLn $ " Exploring call " <> call
846843

847-
shouldAbort <- liftIO $ newTVarIO False
848-
results <- executeVM fetcher opts.iterConf preState shouldAbort $ \leaf -> do
844+
results <- executeVM fetcher opts.iterConf preState solvers.shouldAbort $ \leaf -> do
849845
-- Extract partial if applicable
850846
let mPartial = case leaf of
851847
Partial _ _ p -> Just (p, leaf)
@@ -861,8 +857,8 @@ verifyInputsWithHandler solvers opts fetcher preState post cexHandler = do
861857
case (cexHandler, res) of
862858
(Just handler, cex@(Cex _)) -> do
863859
handler preState cex leaf
864-
when conf.earlyAbort $ liftIO $ atomically $ writeTVar shouldAbort True
865-
(_, (Cex _)) -> when conf.earlyAbort $ liftIO $ atomically $ writeTVar shouldAbort True
860+
when conf.earlyAbort $ liftIO $ atomically $ writeTVar solvers.shouldAbort True
861+
(_, (Cex _)) -> when conf.earlyAbort $ liftIO $ atomically $ writeTVar solvers.shouldAbort True
866862
_ -> pure ()
867863
pure (res, leaf)
868864
else pure (Qed, leaf)
@@ -960,8 +956,7 @@ equivalenceCheck solvers sess bytecodeA bytecodeB opts calldata create = do
960956
getBranches bs = do
961957
let bytecode = if BS.null bs then BS.pack [0] else bs
962958
prestate <- liftIO $ stToIO $ abstractVM calldata bytecode Nothing create
963-
shouldAbort <- liftIO $ newTVarIO False
964-
interpret (Fetch.oracle solvers sess Fetch.noRpc) opts.iterConf prestate shouldAbort runExpr pure
959+
interpret (Fetch.oracle solvers sess Fetch.noRpc) opts.iterConf prestate solvers.shouldAbort runExpr pure
965960
filterQeds (EqIssues res partials) = EqIssues (filter (\(r, _) -> not . isQed $ r) res) partials
966961

967962
rewriteFresh :: Text -> [Expr a] -> [Expr a]

‎test/EVM/Test/FuzzSymExec.hs‎

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,6 @@ concretely through Expr.simplify, then check that against evmtool's output.
1212
-}
1313
module EVM.Test.FuzzSymExec where
1414

15-
import Control.Concurrent.STM.TVar (newTVarIO)
1615
import Control.Monad (when)
1716
import Control.Monad.IO.Unlift
1817
import Control.Monad.ST (ST, stToIO, RealWorld)
@@ -408,9 +407,7 @@ runCodeWithTrace rpcinfo evmEnv alloc txn fromAddr toAddress = withSolvers Z3 0
408407
code' = alloc.code
409408
iterConf = IterConfig { maxIter = Nothing, askSmtIters = 1, loopHeuristic = Naive }
410409
fetcherSym = Fetch.oracle solvers Nothing rpcinfo
411-
buildExpr vm = do
412-
abortFlag <- liftIO $ newTVarIO False
413-
interpret fetcherSym iterConf vm abortFlag runExpr pure
410+
buildExpr vm = interpret fetcherSym iterConf vm solvers.shouldAbort runExpr pure
414411
origVM <- liftIO $ stToIO $ vmForRuntimeCode code' calldata' evmEnv alloc txn fromAddr toAddress
415412
expr <- buildExpr $ symbolify origVM
416413

‎test/test.hs‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1930,7 +1930,7 @@ tests = testGroup "hevm"
19301930
let calldata = (WriteWord (Lit 0x0) (Var "u") (ConcreteBuf ""), [])
19311931
initVM <- liftIO $ stToIO $ abstractVM calldata initCode Nothing True
19321932
let iterConf = IterConfig {maxIter=Nothing, askSmtIters=1, loopHeuristic=StackBased }
1933-
paths <- interpret (Fetch.noRpcFetcher s) iterConf initVM runExpr pure
1933+
paths <- interpret (Fetch.noRpcFetcher s) iterConf initVM s.shouldAbort runExpr pure
19341934
let exprSimp = map Expr.simplify paths
19351935
assertBoolM "unexptected partial execution" (not $ any isPartial exprSimp)
19361936
, test "mixed-concrete-symbolic-args" $ do
@@ -2022,7 +2022,7 @@ tests = testGroup "hevm"
20222022
withDefaultSolver $ \s -> do
20232023
vm <- liftIO $ stToIO $ loadSymVM runtimecode (Lit 0) initCode False
20242024
let iterConf = IterConfig {maxIter=Nothing, askSmtIters=1, loopHeuristic=StackBased }
2025-
paths <- interpret (Fetch.noRpcFetcher s) iterConf vm runExpr pure
2025+
paths <- interpret (Fetch.noRpcFetcher s) iterConf vm s.shouldAbort runExpr pure
20262026
let exprSimp = map Expr.simplify paths
20272027
assertBoolM "expected partial execution" (any isPartial exprSimp)
20282028
]

0 commit comments

Comments
 (0)