Symbolic execution queue

CHANGELOG.md

@@ -14,6 +14,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Replaced RPC mocking by a full block cache support. This allows users to cache responses from an RPC
   node via `--cache-dir dir`.
 - Changed `verify*` methods to always require postcodition.
+- We now use a symbolic execution queue, so as not to run out of resources when there are
+  too many branches to explore.
 
 ## [0.56.0] - 2025-10-13
 

bench/bench.hs

@@ -92,7 +92,7 @@ runBCTest x =
 findPanics :: App m => Solver -> Natural -> Integer -> ByteString -> m ()
 findPanics solver count iters c = do
   _ <- withSolvers solver count 1 Nothing $ \s -> do
-    let opts = defaultVeriOpts { iterConf = defaultIterConf {maxIter = Just iters, askSmtIters = iters + 1 }}
+    let opts = (defaultVeriOpts :: VeriOpts) { iterConf = defaultIterConf {maxIter = Just iters, askSmtIters = iters + 1 }}
     checkAssert s allPanicCodes c Nothing [] opts
   liftIO $ putStrLn "done"
 

cli/cli.hs

@@ -46,7 +46,7 @@ import EVM.Concrete qualified as Concrete
 import GitHash
 import EVM.FeeSchedule (feeSchedule)
 import EVM.Fetch qualified as Fetch
-import EVM.Format (hexByteString, strip0x, formatExpr)
+import EVM.Format (hexByteString, strip0x, formatExpr, indent)
 import EVM.Solidity
 import EVM.Solvers
 import EVM.Stepper qualified
@@ -527,7 +527,7 @@ symbCheck cFileOpts sOpts cExecOpts cOpts = do
       cache <- readMVar sess.sharedCache
       Fetch.saveCache dir block cache
     case res of
-      [Qed] -> do
+      [] -> do
         liftIO $ putStrLn "\nQED: No reachable property violations discovered\n"
         showExtras solvers sOpts calldata expr
       _ -> do
@@ -540,26 +540,29 @@ symbCheck cFileOpts sOpts cExecOpts cOpts = do
                  , ""
                  ] <> fmap (formatCex (fst calldata) Nothing) cexs
         liftIO $ T.putStrLn $ T.unlines counterexamples
-        liftIO $ printWarnings Nothing [expr] res "symbolically"
+        liftIO $ printWarnings Nothing expr res "symbolically"
         showExtras solvers sOpts calldata expr
         liftIO exitFailure
 
-showExtras :: App m => SolverGroup ->SymbolicOptions -> (Expr Buf, [Prop]) -> Expr End -> m ()
+showExtras :: App m => SolverGroup ->SymbolicOptions -> (Expr Buf, [Prop]) -> [Expr End] -> m ()
 showExtras solvers sOpts calldata expr = do
   when sOpts.showTree $ liftIO $ do
-    putStrLn "=== Expression ===\n"
-    T.putStrLn $ formatExpr $ Expr.simplify expr
+    putStrLn "=== Leafs ===\n"
+    printLeafs $ map (formatExpr . Expr.simplify) expr
     putStrLn ""
   when sOpts.showReachableTree $ do
     reached <- reachable solvers expr
     liftIO $ do
-      putStrLn "=== Potentially Reachable Expression ===\n"
-      T.putStrLn (formatExpr . Expr.simplify $ reached)
+      putStrLn "=== Potentially Reachable Leafs ===\n"
+      printLeafs $ map (formatExpr . Expr.simplify) reached
       putStrLn ""
   when sOpts.getModels $ do
-    liftIO $ putStrLn $ "=== Models for " <> show (Expr.numBranches expr) <> " branches ==="
+    liftIO $ putStrLn $ "=== Models for " <> show (length expr) <> " branches ==="
     ms <- produceModels solvers expr
     liftIO $ forM_ ms (showModel (fst calldata))
+  where
+    printLeafs leafs =
+      T.putStrLn $ indent 2 $ T.unlines $ zipWith (\i r -> "Leaf " <> T.pack (show (i :: Integer)) <> ":\n" <> r) [0..] leafs
 
 isTestOrLib :: Text -> Bool
 isTestOrLib file = T.isSuffixOf ".t.sol" file || areAnyPrefixOf ["src/test/", "src/tests/", "lib/"] file

doc/src/architecture.md

@@ -68,16 +68,13 @@ Expressions in this language can have the following types:
 - `Logs`: EVM logs
 
 ## Control Flow
-An EVM program is represented by an `Expr End`, which is either a single end
-state for a program without branches, or a series of nested if-then-else terms,
-where each leaf is an end state. Some end states (e.g. `Return`) contain copies
-of any externally observable data (i.e. returndata and post call storage).
-
-As an example the following Expr encodes a program that branches based on the
-equality of two symbolic words ("a" and "b"), and returns if they are equal and
-reverts if they are not:
+An EVM program is represented by an `[Expr End]`, which is a list of all
+possible end states for a program. As an example the following
+two `Expr End`-s encode a program that branches based on the equality of two symbolic
+words ("a" and "b"), and returns if they are equal and reverts if they are not:
 ```haskell
-(ITE (Eq (Var "a") (Var "b")) (Success ...) (Failure ...))
+[ Success [PEq (Var "a") (Var "b")] ...,
+, Failure [PNeg (PEq (Var "a") (Var "b"))] ...]
 ```
 
 ## Buffers

src/EVM.hs

@@ -1621,7 +1621,7 @@ onlyDeployed addrExpr fallback continue = do
     else case eqT @t @Symbolic of
       Just Refl -> do
         let deployedAddrs = map forceEAddrToEWord $ mapMaybe (codeMustExist vm) $ Map.keys vm.env.contracts
-        runAll (?conf.maxDepth) vm.exploreDepth $ PleaseRunAll addrExpr deployedAddrs runAllPaths
+        runAll (?conf.maxDepth) vm.exploreDepth $ PleaseRunAll deployedAddrs runAllPaths
       _ -> internalError "Unknown address in Concrete mode"
   where
     codeMustExist :: (VM t s) -> Expr EAddr -> Maybe (Expr EAddr)
@@ -2669,14 +2669,12 @@ traceForest' :: Expr End -> Forest Trace
 traceForest' (Success _ (TraceContext f _ _) _ _) = f
 traceForest' (Partial _ (TraceContext f _ _) _) = f
 traceForest' (Failure _ (TraceContext f _ _) _) = f
-traceForest' (ITE {}) = internalError"Internal Error: ITE does not contain a trace"
 traceForest' (GVar {}) = internalError"Internal Error: Unexpected GVar"
 
 traceContext :: Expr End -> TraceContext
 traceContext (Success _ c _ _) = c
 traceContext (Partial _ c _) = c
 traceContext (Failure _ c _) = c
-traceContext (ITE {}) = internalError"Internal Error: ITE does not contain a trace"
 traceContext (GVar {}) = internalError"Internal Error: Unexpected GVar"
 
 traceTopLog :: [Expr Log] -> EVM t s ()
@@ -3080,20 +3078,18 @@ instance VMOps Symbolic where
     vm <- get
     query $ PleaseAskSMT cond pathconds (runBothPaths loc vm.exploreDepth)
     where
-      condSimp = Expr.simplify cond
-      condSimpConc = Expr.concKeccakSimpExpr condSimp
       runBothPaths loc _ (Case v) = do
         assign #result Nothing
-        pushTo #constraints $ if v then Expr.simplifyProp (Lit 0 ./= condSimpConc)
-                                   else Expr.simplifyProp (Lit 0 .== condSimpConc)
+        pushTo #constraints $ if v then PNeg (PEq (Lit 0) cond)
+                                   else (PEq (Lit 0) cond)
         (iteration, _) <- use (#iterations % at loc % non (0,[]))
         stack <- use (#state % #stack)
         assign (#pathsVisited % at (loc, iteration)) (Just v)
         assign (#iterations % at loc) (Just (iteration + 1, stack))
         continue v
       -- Both paths are possible; we ask for more input
       runBothPaths loc exploreDepth UnknownBranch =
-        (runBoth depthLimit exploreDepth ) . PleaseRunBoth condSimp $ (runBothPaths loc exploreDepth) . Case
+        (runBoth depthLimit exploreDepth ) . PleaseRunBoth $ (runBothPaths loc exploreDepth) . Case
 
   -- numBytes allows us to specify how many bytes of the returned value is relevant
   -- if it's e.g.a JUMP, only 2 bytes can be relevant. This allows us to avoid
@@ -3112,7 +3108,7 @@ instance VMOps Symbolic where
             assign #result Nothing
             pushTo #constraints $ Expr.simplifyProp (ewordExpr .== (Lit val))
             continue $ Just val
-          _ -> runAll maxDepth vm.exploreDepth $ PleaseRunAll ewordExpr (map Lit concVals) runAllPaths
+          _ -> runAll maxDepth vm.exploreDepth $ PleaseRunAll (map Lit concVals) runAllPaths
       Nothing -> do
         assign #result Nothing
         continue Nothing

src/EVM/Expr.hs

@@ -1076,11 +1076,6 @@ simplifyNoLitToKeccak e = untilFixpoint (mapExpr go) e
       | a == b = Lit 1
       | otherwise = eq a b
 
-    -- redundant ITE
-    go (ITE (Lit x) a b)
-      | x == 0 = b
-      | otherwise = a
-
     -- Masking as as per Solidity bit-packing of e.g. function parameters
     go (And (Lit mask1) (Or (And (Lit mask2) _) x)) | (mask1 .&. mask2 == 0)
          = And (Lit mask1) x
@@ -1228,13 +1223,6 @@ simplifyNoLitToKeccak e = untilFixpoint (mapExpr go) e
       | b == (Lit 0) = a
       | otherwise = EVM.Expr.or a b
 
-    -- If x is ever non zero the Or will always evaluate to some non zero value and the false branch will be unreachable
-    -- NOTE: with AND this does not work, because and(0x8, 0x4) = 0
-    go (ITE (Or (Lit x) a) t f)
-      | x == 0 = ITE a t f
-      | otherwise = t
-    go (ITE (Or a b@(Lit _)) t f) = ITE (Or b a) t f
-
     -- we write at least 32, so if x <= 32, it's FALSE
     go o@(EVM.Types.LT (BufLength (WriteWord {})) (Lit x))
       | x <= 32 = Lit 0
@@ -1672,10 +1660,6 @@ max (Lit 0) y = y
 max x (Lit 0) = x
 max x y = normArgs Max Prelude.max x y
 
-numBranches :: Expr End -> Int
-numBranches (ITE _ t f) = numBranches t + numBranches f
-numBranches _ = 1
-
 allLit :: [Expr Byte] -> Bool
 allLit = all isLitByte
 

src/EVM/Format.hs

@@ -16,6 +16,7 @@ module EVM.Format
   , showTraceTree'
   , showValues
   , prettyvmresult
+  , prettyvmresults
   , showCall
   , showWordExact
   , showWordExplanation
@@ -201,7 +202,6 @@ showTraceTree dapp vm =
   in pack $ concatMap showTree traces
 
 showTraceTree' :: DappInfo -> Expr End -> Text
-showTraceTree' _ (ITE {}) = internalError "ITE does not contain a trace"
 showTraceTree' dapp leaf =
   let ?context = DappContext { info = dapp, contracts, labels }
   in let forest = traceForest' leaf
@@ -453,6 +453,10 @@ prettyvmresult (Failure _ _ err) = prettyError err
 prettyvmresult (Partial _ _ p) = T.unpack $ formatPartial p
 prettyvmresult r = internalError $ "Invalid result: " <> show r
 
+prettyvmresults :: [Expr End] -> String
+prettyvmresults results =
+  T.unpack $ indent 2 $ T.unlines $ zipWith (\i r -> T.pack ("Result " <> show (i :: Integer) <> ": " <> prettyvmresult r)) [0..] results
+
 indent :: Int -> Text -> Text
 indent n = rstrip . T.unlines . fmap (T.replicate n (T.pack [' ']) <>) . T.lines
 
@@ -565,14 +569,6 @@ formatExpr = go
       (GVar v) -> "(GVar " <> T.pack (show v) <> ")"
       LitByte w -> T.pack $ show w
 
-      ITE c t f -> T.unlines
-        [ "(ITE"
-        , indent 2 $ T.unlines
-          [ formatExpr c
-          , formatExpr t
-          , formatExpr f
-          ]
-        , ")"]
       Success asserts _ buf store -> T.unlines
         [ "(Success"
         , indent 2 $ T.unlines

src/EVM/Stepper.hs

@@ -98,6 +98,7 @@ runFully = do
 enter :: Text -> Stepper t s ()
 enter t = evm (EVM.pushTrace (EntryTrace t))
 
+-- Concrete interpretation
 interpret
   :: forall m a . (App m)
   => Fetch.Fetcher Concrete m RealWorld