From 0dc60f758a4921522e55fa57ab5a5062d14139d8 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Tue, 7 Jan 2025 15:36:59 +0100 Subject: [PATCH 1/9] Use a SAT solver to try to force values to be concrete --- src/EVM.hs | 41 ++++++++++++++++++++++++++++++++--------- src/EVM/Fetch.hs | 36 ++++++++++++++++++++++++++++++++++++ src/EVM/Types.hs | 6 ++++++ 3 files changed, 74 insertions(+), 9 deletions(-) diff --git a/src/EVM.hs b/src/EVM.hs index 5750ea84f..3dcf4bbfa 100644 --- a/src/EVM.hs +++ b/src/EVM.hs @@ -67,6 +67,7 @@ import Witch (into, tryFrom, unsafeInto, tryInto) import Crypto.Hash (Digest, SHA256, RIPEMD160) import Crypto.Hash qualified as Crypto import Crypto.Number.ModArithmetic (expFast) +import Debug.Trace (traceM) blankState :: VMOps t => ST s (FrameState t s) blankState = do @@ -330,7 +331,7 @@ exec1 = do else do let ?op = getOpW8 vm.state let opName = getOpName vm.state - + -- traceM $ "Executing " ++ opName ++ " at " ++ show (vm.state.pc) case getOp (?op) of OpPush0 -> do @@ -802,7 +803,9 @@ exec1 = do burn g_mid $ forceConcrete x "JUMP: symbolic jumpdest" $ \x' -> case tryInto x' of Left _ -> vmError BadJumpDestination - Right i -> checkJump i xs + Right i -> do + traceM $ "Jumping to " ++ show i + checkJump i xs _ -> underrun OpJumpi -> @@ -1380,7 +1383,7 @@ getCodeLocation :: VM t s -> CodeLocation getCodeLocation vm = (vm.state.contract, vm.state.pc) query :: Query t s -> EVM t s () -query = assign #result . Just . HandleEffect . Query +query q = assign #result $ Just $ HandleEffect (Query q) choose :: Choose s -> EVM Symbolic s () choose = assign #result . Just . HandleEffect . Choose @@ -1585,17 +1588,21 @@ notStatic continue = do forceAddr :: VMOps t => Expr EWord -> String -> (Expr EAddr -> EVM t s ()) -> EVM t s () forceAddr n msg continue = case wordToAddr n of - Nothing -> do - vm <- get - partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) msg (wrap [n]) + Nothing -> oneSolution n $ \case + Just sol -> maybe fallback continue (wordToAddr (Lit sol)) + Nothing -> fallback Just c -> continue c + where fallback = do + vm <- get + partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) msg (wrap [n]) forceConcrete :: VMOps t => Expr EWord -> String -> (W256 -> EVM t s ()) -> EVM t s () forceConcrete n msg continue = case maybeLitWordSimp n of - Nothing -> do - vm <- get - partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) msg (wrap [n]) + Nothing -> oneSolution n $ maybe fallback continue Just c -> continue c + where fallback = do + vm <- get + partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) msg (wrap [n]) forceConcreteAddr :: VMOps t => Expr EAddr -> String -> (Addr -> EVM t s ()) -> EVM t s () forceConcreteAddr n msg continue = case maybeLitAddrSimp n of @@ -2622,6 +2629,7 @@ checkJump x xs = noJumpIntoInitData x $ do True -> do #state % #stack .= xs #state % #pc .= x + traceM $ "setting PC to " <> show x False -> vmError BadJumpDestination -- fails with partial if we're trying to jump into the symbolic region of an `InitCode` @@ -2954,6 +2962,21 @@ instance VMOps Symbolic where choosePath loc Unknown = choose . PleaseChoosePath condSimp $ choosePath loc . Case + oneSolution symAddr continue = do + pathconds <- use #constraints + pc <- zoom #state $ use #pc + traceM $ "oneSolution at pc: " ++ show pc + query $ PleaseGetSol symAddr pathconds calcAddr + where + calcAddr (Just concAddr) = do + assign #result Nothing + traceM $ "oneSolution concAddrs: " ++ show concAddr + pushTo #constraints $ Expr.simplifyProp (symAddr .== (Lit concAddr)) + continue (Just concAddr) + calcAddr Nothing = do + traceM "oneSolution symAddr" + continue Nothing + instance VMOps Concrete where burn' n continue = do available <- use (#state % #gas) diff --git a/src/EVM/Fetch.hs b/src/EVM/Fetch.hs index 81c2ab2be..8fc258e73 100644 --- a/src/EVM/Fetch.hs +++ b/src/EVM/Fetch.hs @@ -28,6 +28,7 @@ import System.Environment (lookupEnv, getEnvironment) import System.Process import Control.Monad.IO.Class import EVM.Effects +import Debug.Trace (traceM) -- | Abstract representation of an RPC fetch request data RpcQuery a where @@ -212,6 +213,11 @@ oracle solvers info q = do -- Is is possible to satisfy the condition? continue <$> checkBranch solvers (branchcondition ./= (Lit 0)) pathconds + PleaseGetSol symAddr pathconditions continue -> do + let pathconds = foldl' PAnd (PBool True) pathconditions + -- traceM $ "Getting solution for " ++ show symAddr + continue <$> getSolution solvers symAddr pathconds + PleaseFetchContract addr base continue -> do contract <- case info of Nothing -> let @@ -239,6 +245,36 @@ oracle solvers info q = do type Fetcher t m s = App m => Query t s -> m (EVM t s ()) +getSolution :: forall m . App m => SolverGroup -> Expr EWord -> Prop -> m (Maybe W256) +getSolution solvers symAddr pathconditions = do + conf <- readConfig + liftIO $ do + ret <- collectSolutions [] 2 pathconditions conf + case ret of + Nothing -> pure Nothing + Just r -> case length r of + 0 -> pure Nothing + -- Temporary, a future improvement can deal with more than one solution + 1 -> pure $ Just (r !! 0) + _ -> pure Nothing + where + collectSolutions :: [W256] -> Int -> Prop -> Config -> IO (Maybe [W256]) + collectSolutions addrs maxSols conds conf = do + if (length addrs >= maxSols) then pure Nothing + else + checkSat solvers (assertProps conf [(PEq (Var "addrQuery") symAddr) .&& conds]) >>= \case + Sat (SMTCex vars _ _ _ _ _) -> case (Map.lookup (Var "addrQuery") vars) of + Just addr -> do + traceM $ "Model: " ++ show addr + let newConds = PAnd conds (symAddr ./= (Lit addr)) + collectSolutions (addr:addrs) maxSols newConds conf + _ -> pure $ Just addrs + Unsat -> do + traceM "No (more) solution(s) found" + pure $ Just addrs + -- Error or timeout, we need to be conservative + _ -> pure Nothing + -- | Checks which branches are satisfiable, checking the pathconditions for consistency -- if the third argument is true. -- When in debug mode, we do not want to be able to navigate to dead paths, diff --git a/src/EVM/Types.hs b/src/EVM/Types.hs index ca6e9212b..f7f6a9116 100644 --- a/src/EVM/Types.hs +++ b/src/EVM/Types.hs @@ -594,6 +594,7 @@ data Query t s where PleaseFetchContract :: Addr -> BaseState -> (Contract -> EVM t s ()) -> Query t s PleaseFetchSlot :: Addr -> W256 -> (W256 -> EVM t s ()) -> Query t s PleaseAskSMT :: Expr EWord -> [Prop] -> (BranchCondition -> EVM Symbolic s ()) -> Query Symbolic s + PleaseGetSol :: Expr EWord -> [Prop] -> (Maybe W256 -> EVM Symbolic s ()) -> Query Symbolic s PleaseDoFFI :: [String] -> Map String String -> (ByteString -> EVM t s ()) -> Query t s PleaseReadEnv :: String -> (String -> EVM t s ()) -> Query t s @@ -617,6 +618,10 @@ instance Show (Query t s) where (("") ++) + PleaseGetSol addr constraints _ -> + (("") ++) PleaseDoFFI cmd env _ -> ((" @@ -854,6 +859,7 @@ class VMOps (t :: VMType) where partial :: PartialExec -> EVM t s () branch :: Expr EWord -> (Bool -> EVM t s ()) -> EVM t s () + oneSolution :: Expr EWord -> (Maybe W256 -> EVM t s ()) -> EVM t s () -- Bytecode Representations ------------------------------------------------------------------------ From 443cc3daeedfba3270acf1301836e7a139ab5adb Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Wed, 8 Jan 2025 15:52:11 +0100 Subject: [PATCH 2/9] Fixing up --- src/EVM.hs | 42 ++++++++++++++++-------------------------- src/EVM/Fetch.hs | 4 ---- 2 files changed, 16 insertions(+), 30 deletions(-) diff --git a/src/EVM.hs b/src/EVM.hs index 3dcf4bbfa..de08f3457 100644 --- a/src/EVM.hs +++ b/src/EVM.hs @@ -67,7 +67,6 @@ import Witch (into, tryFrom, unsafeInto, tryInto) import Crypto.Hash (Digest, SHA256, RIPEMD160) import Crypto.Hash qualified as Crypto import Crypto.Number.ModArithmetic (expFast) -import Debug.Trace (traceM) blankState :: VMOps t => ST s (FrameState t s) blankState = do @@ -331,7 +330,6 @@ exec1 = do else do let ?op = getOpW8 vm.state let opName = getOpName vm.state - -- traceM $ "Executing " ++ opName ++ " at " ++ show (vm.state.pc) case getOp (?op) of OpPush0 -> do @@ -803,9 +801,7 @@ exec1 = do burn g_mid $ forceConcrete x "JUMP: symbolic jumpdest" $ \x' -> case tryInto x' of Left _ -> vmError BadJumpDestination - Right i -> do - traceM $ "Jumping to " ++ show i - checkJump i xs + Right i -> checkJump i xs _ -> underrun OpJumpi -> @@ -1386,7 +1382,7 @@ query :: Query t s -> EVM t s () query q = assign #result $ Just $ HandleEffect (Query q) choose :: Choose s -> EVM Symbolic s () -choose = assign #result . Just . HandleEffect . Choose +choose c = assign #result $ Just $ HandleEffect (Choose c) -- | Construct RPC Query and halt execution until resolved fetchAccount :: VMOps t => Expr EAddr -> (Contract -> EVM t s ()) -> EVM t s () @@ -1706,8 +1702,13 @@ cheat gas (inOffset, inSize) (outOffset, outSize) xs = do , context = newContext } case maybeLitWordSimp abi of - Nothing -> partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) "symbolic cheatcode selector" (wrap [abi]) - Just (unsafeInto -> abi') -> + Nothing -> oneSolution abi $ \case + Just concAbi -> runCheat concAbi input + Nothing -> partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) "symbolic cheatcode selector" (wrap [abi]) + Just concAbi -> runCheat concAbi input + where + runCheat abi input = do + let abi' = unsafeInto abi case Map.lookup abi' cheatActions of Nothing -> vmError (BadCheatCode "Cannot understand cheatcode." abi') Just action -> action input @@ -2629,7 +2630,6 @@ checkJump x xs = noJumpIntoInitData x $ do True -> do #state % #stack .= xs #state % #pc .= x - traceM $ "setting PC to " <> show x False -> vmError BadJumpDestination -- fails with partial if we're trying to jump into the symbolic region of an `InitCode` @@ -2962,20 +2962,14 @@ instance VMOps Symbolic where choosePath loc Unknown = choose . PleaseChoosePath condSimp $ choosePath loc . Case - oneSolution symAddr continue = do + oneSolution ewordExpr continue = do pathconds <- use #constraints - pc <- zoom #state $ use #pc - traceM $ "oneSolution at pc: " ++ show pc - query $ PleaseGetSol symAddr pathconds calcAddr - where - calcAddr (Just concAddr) = do + query $ PleaseGetSol ewordExpr pathconds $ \case + Just concAddr -> do assign #result Nothing - traceM $ "oneSolution concAddrs: " ++ show concAddr - pushTo #constraints $ Expr.simplifyProp (symAddr .== (Lit concAddr)) - continue (Just concAddr) - calcAddr Nothing = do - traceM "oneSolution symAddr" - continue Nothing + pushTo #constraints $ Expr.simplifyProp (ewordExpr .== (Lit concAddr)) + continue $ Just concAddr + Nothing -> continue Nothing instance VMOps Concrete where burn' n continue = do @@ -3099,16 +3093,12 @@ instance VMOps Concrete where push (into vm.state.gas) enoughGas cost gasCap = cost <= gasCap - subGas gasCap cost = gasCap - cost - toGas = id - whenSymbolicElse _ a = a - partial _ = internalError "won't happen during concrete exec" - branch (forceLit -> cond) continue = continue (cond > 0) + oneSolution _ _ = internalError "SMT solver should never be needed in concrete mode" -- Create symbolic VM from concrete VM symbolify :: VM Concrete s -> VM Symbolic s diff --git a/src/EVM/Fetch.hs b/src/EVM/Fetch.hs index 8fc258e73..257a87d4b 100644 --- a/src/EVM/Fetch.hs +++ b/src/EVM/Fetch.hs @@ -28,7 +28,6 @@ import System.Environment (lookupEnv, getEnvironment) import System.Process import Control.Monad.IO.Class import EVM.Effects -import Debug.Trace (traceM) -- | Abstract representation of an RPC fetch request data RpcQuery a where @@ -215,7 +214,6 @@ oracle solvers info q = do PleaseGetSol symAddr pathconditions continue -> do let pathconds = foldl' PAnd (PBool True) pathconditions - -- traceM $ "Getting solution for " ++ show symAddr continue <$> getSolution solvers symAddr pathconds PleaseFetchContract addr base continue -> do @@ -265,12 +263,10 @@ getSolution solvers symAddr pathconditions = do checkSat solvers (assertProps conf [(PEq (Var "addrQuery") symAddr) .&& conds]) >>= \case Sat (SMTCex vars _ _ _ _ _) -> case (Map.lookup (Var "addrQuery") vars) of Just addr -> do - traceM $ "Model: " ++ show addr let newConds = PAnd conds (symAddr ./= (Lit addr)) collectSolutions (addr:addrs) maxSols newConds conf _ -> pure $ Just addrs Unsat -> do - traceM "No (more) solution(s) found" pure $ Just addrs -- Error or timeout, we need to be conservative _ -> pure Nothing From 03dbaecd60ecf74e7bfcd2c66a2e357e15d2b816 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Wed, 8 Jan 2025 16:04:32 +0100 Subject: [PATCH 3/9] More & cleaner use of solution getting --- src/EVM.hs | 15 ++++++++------- src/EVM/Types.hs | 6 +++--- 2 files changed, 11 insertions(+), 10 deletions(-) diff --git a/src/EVM.hs b/src/EVM.hs index de08f3457..660c7df2a 100644 --- a/src/EVM.hs +++ b/src/EVM.hs @@ -1585,7 +1585,7 @@ notStatic continue = do forceAddr :: VMOps t => Expr EWord -> String -> (Expr EAddr -> EVM t s ()) -> EVM t s () forceAddr n msg continue = case wordToAddr n of Nothing -> oneSolution n $ \case - Just sol -> maybe fallback continue (wordToAddr (Lit sol)) + Just sol -> continue $ LitAddr (truncateToAddr sol) Nothing -> fallback Just c -> continue c where fallback = do @@ -1602,10 +1602,11 @@ forceConcrete n msg continue = case maybeLitWordSimp n of forceConcreteAddr :: VMOps t => Expr EAddr -> String -> (Addr -> EVM t s ()) -> EVM t s () forceConcreteAddr n msg continue = case maybeLitAddrSimp n of - Nothing -> do - vm <- get - partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) msg (wrap [n]) + Nothing -> oneSolution (WAddr n) $ maybe fallback $ \c -> continue $ unsafeInto c Just c -> continue c + where fallback = do + vm <- get + partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) msg (wrap [n]) forceConcreteAddr2 :: VMOps t => (Expr EAddr, Expr EAddr) -> String -> ((Addr, Addr) -> EVM t s ()) -> EVM t s () forceConcreteAddr2 (n,m) msg continue = case (maybeLitAddrSimp n, maybeLitAddrSimp m) of @@ -2965,10 +2966,10 @@ instance VMOps Symbolic where oneSolution ewordExpr continue = do pathconds <- use #constraints query $ PleaseGetSol ewordExpr pathconds $ \case - Just concAddr -> do + Just concVal -> do assign #result Nothing - pushTo #constraints $ Expr.simplifyProp (ewordExpr .== (Lit concAddr)) - continue $ Just concAddr + pushTo #constraints $ Expr.simplifyProp (ewordExpr .== (Lit concVal)) + continue $ Just concVal Nothing -> continue Nothing instance VMOps Concrete where diff --git a/src/EVM/Types.hs b/src/EVM/Types.hs index f7f6a9116..bd12c0fbc 100644 --- a/src/EVM/Types.hs +++ b/src/EVM/Types.hs @@ -618,9 +618,9 @@ instance Show (Query t s) where (("") ++) - PleaseGetSol addr constraints _ -> - ((" + (("") ++) PleaseDoFFI cmd env _ -> ((" Date: Wed, 8 Jan 2025 16:26:57 +0100 Subject: [PATCH 4/9] More debug when possible --- src/EVM/Fetch.hs | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/EVM/Fetch.hs b/src/EVM/Fetch.hs index 257a87d4b..3b9f1a155 100644 --- a/src/EVM/Fetch.hs +++ b/src/EVM/Fetch.hs @@ -27,6 +27,7 @@ import Numeric.Natural (Natural) import System.Environment (lookupEnv, getEnvironment) import System.Process import Control.Monad.IO.Class +import Control.Monad (when) import EVM.Effects -- | Abstract representation of an RPC fetch request @@ -264,12 +265,16 @@ getSolution solvers symAddr pathconditions = do Sat (SMTCex vars _ _ _ _ _) -> case (Map.lookup (Var "addrQuery") vars) of Just addr -> do let newConds = PAnd conds (symAddr ./= (Lit addr)) + when conf.debug $ putStrLn $ "Got one solution to symbolic query:" <> show addr collectSolutions (addr:addrs) maxSols newConds conf _ -> pure $ Just addrs Unsat -> do + when conf.debug $ putStrLn "No more solution(s) to symbolic query." pure $ Just addrs -- Error or timeout, we need to be conservative - _ -> pure Nothing + res -> do + when conf.debug $ putStrLn $ "Symbolic query result is neither SAT nor UNSAT:" <> show res + pure Nothing -- | Checks which branches are satisfiable, checking the pathconditions for consistency -- if the third argument is true. From c9e58b91ae21481034d9623b509efdf701ba7f29 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Wed, 8 Jan 2025 16:37:18 +0100 Subject: [PATCH 5/9] Update changelog --- CHANGELOG.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 8b94dfe36..644984ee1 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -9,6 +9,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 - JoinBytes simplification rule - New simplification rule to help deal with abi.encodeWithSelector - More simplification rules for Props +- Using the SMT solver to get a single concrete value for a symbolic expression + and continue running, whenever possible ## Fixed - We now try to simplify expressions fully before trying to cast them to a concrete value From a2a115cb52b0c65dce97c248bcf471fe8166e827 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Wed, 8 Jan 2025 17:05:23 +0100 Subject: [PATCH 6/9] This should be an error, there must be a valuation for the addrQuery --- src/EVM/Fetch.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/EVM/Fetch.hs b/src/EVM/Fetch.hs index 3b9f1a155..7eac0a3d3 100644 --- a/src/EVM/Fetch.hs +++ b/src/EVM/Fetch.hs @@ -267,7 +267,7 @@ getSolution solvers symAddr pathconditions = do let newConds = PAnd conds (symAddr ./= (Lit addr)) when conf.debug $ putStrLn $ "Got one solution to symbolic query:" <> show addr collectSolutions (addr:addrs) maxSols newConds conf - _ -> pure $ Just addrs + _ -> internalError "No solution to symbolic query" Unsat -> do when conf.debug $ putStrLn "No more solution(s) to symbolic query." pure $ Just addrs From 620f5f8e776db39f767428da76a85b3150f42579 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Thu, 9 Jan 2025 12:56:04 +0100 Subject: [PATCH 7/9] Just some cleanup --- src/EVM.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/EVM.hs b/src/EVM.hs index 660c7df2a..43f942e93 100644 --- a/src/EVM.hs +++ b/src/EVM.hs @@ -2942,7 +2942,7 @@ instance VMOps Symbolic where toGas _ = () whenSymbolicElse a _ = a - partial e = assign #result (Just (Unfinished e)) + partial e = assign #result $ Just (Unfinished e) branch cond continue = do loc <- codeloc pathconds <- use #constraints From 6221b77a5191f91aefb71354d142c46c5c4b5e8b Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Thu, 9 Jan 2025 14:12:06 +0100 Subject: [PATCH 8/9] Better debug message --- src/EVM/Fetch.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/EVM/Fetch.hs b/src/EVM/Fetch.hs index 7eac0a3d3..449cfd0e7 100644 --- a/src/EVM/Fetch.hs +++ b/src/EVM/Fetch.hs @@ -265,7 +265,7 @@ getSolution solvers symAddr pathconditions = do Sat (SMTCex vars _ _ _ _ _) -> case (Map.lookup (Var "addrQuery") vars) of Just addr -> do let newConds = PAnd conds (symAddr ./= (Lit addr)) - when conf.debug $ putStrLn $ "Got one solution to symbolic query:" <> show addr + when conf.debug $ putStrLn $ "Got one solution to symbolic query:" <> show addr <> " now have " <> show (length addrs + 1) <> " solution(s)." collectSolutions (addr:addrs) maxSols newConds conf _ -> internalError "No solution to symbolic query" Unsat -> do From f8857accb842297ef99992d240ac52b4a7eb9bfe Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Thu, 9 Jan 2025 15:04:18 +0100 Subject: [PATCH 9/9] Cleaner implementation --- src/EVM.hs | 20 ++++++++++---------- src/EVM/Fetch.hs | 6 +++--- 2 files changed, 13 insertions(+), 13 deletions(-) diff --git a/src/EVM.hs b/src/EVM.hs index 43f942e93..e5a3033f8 100644 --- a/src/EVM.hs +++ b/src/EVM.hs @@ -1402,11 +1402,11 @@ fetchAccount addr continue = Nothing -> do base <- use (#config % #baseState) assign (#result) . Just . HandleEffect . Query $ - PleaseFetchContract a base - (\c -> do assign (#cache % #fetched % at a) (Just c) - assign (#env % #contracts % at addr) (Just c) - assign #result Nothing - continue c) + PleaseFetchContract a base $ \c -> do + assign (#cache % #fetched % at a) (Just c) + assign (#env % #contracts % at addr) (Just c) + assign #result Nothing + continue c GVar _ -> internalError "Unexpected GVar" accessStorage @@ -1445,13 +1445,11 @@ accessStorage addr slot continue = do else do modifying (#env % #contracts % ix addr % #storage) (writeStorage slot (Lit 0)) continue $ Lit 0 - mkQuery a s = query $ - PleaseFetchSlot a s - (\x -> do + mkQuery a s = query $ PleaseFetchSlot a s $ \x -> do modifying (#cache % #fetched % ix a % #storage) (writeStorage (Lit s) (Lit x)) modifying (#env % #contracts % ix (LitAddr a) % #storage) (writeStorage (Lit s) (Lit x)) assign #result Nothing - continue (Lit x)) + continue $ Lit x accessTStorage :: VMOps t => Expr EAddr @@ -2970,7 +2968,9 @@ instance VMOps Symbolic where assign #result Nothing pushTo #constraints $ Expr.simplifyProp (ewordExpr .== (Lit concVal)) continue $ Just concVal - Nothing -> continue Nothing + Nothing -> do + assign #result Nothing + continue Nothing instance VMOps Concrete where burn' n continue = do diff --git a/src/EVM/Fetch.hs b/src/EVM/Fetch.hs index 449cfd0e7..f6c23cc91 100644 --- a/src/EVM/Fetch.hs +++ b/src/EVM/Fetch.hs @@ -248,7 +248,7 @@ getSolution :: forall m . App m => SolverGroup -> Expr EWord -> Prop -> m (Maybe getSolution solvers symAddr pathconditions = do conf <- readConfig liftIO $ do - ret <- collectSolutions [] 2 pathconditions conf + ret <- collectSolutions [] 1 pathconditions conf case ret of Nothing -> pure Nothing Just r -> case length r of @@ -259,13 +259,13 @@ getSolution solvers symAddr pathconditions = do where collectSolutions :: [W256] -> Int -> Prop -> Config -> IO (Maybe [W256]) collectSolutions addrs maxSols conds conf = do - if (length addrs >= maxSols) then pure Nothing + if (length addrs > maxSols) then pure Nothing else checkSat solvers (assertProps conf [(PEq (Var "addrQuery") symAddr) .&& conds]) >>= \case Sat (SMTCex vars _ _ _ _ _) -> case (Map.lookup (Var "addrQuery") vars) of Just addr -> do let newConds = PAnd conds (symAddr ./= (Lit addr)) - when conf.debug $ putStrLn $ "Got one solution to symbolic query:" <> show addr <> " now have " <> show (length addrs + 1) <> " solution(s)." + when conf.debug $ putStrLn $ "Got one solution to symbolic query:" <> show addr <> " now have " <> show (length addrs + 1) <> " solution(s), max is: " <> show maxSols collectSolutions (addr:addrs) maxSols newConds conf _ -> internalError "No solution to symbolic query" Unsat -> do