New queue idea

Cleanup

More generic interpret

Update

Making progress

Making progress

Update

Update

Update

Making progress

Update

Now typecheck

Update

Making progress

Update

Better now

Making progress

Update

Typechecks now

Update

Better

Some improvement?

Better I think

Update

Update

Making progress

Update to fix changes

Fixing

Update

Better

Let's hope this works

Cleaner

Update

Update

Less noise

Update

Much better

Update

Fixing

Update

Update

Update

QED change

Qed fixing still

Fixed Qed

Update to fix cli

Ooops, fixing bug

Better printing

Cleanup

Cleanup

Cleanup

Cleanup

Trying to rebase on top of main

Add changelog

Less braces

Less change

Author: msooseth

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
 

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

src/EVM.hs

@@ -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 ()
@@ -3092,7 +3090,7 @@ instance VMOps Symbolic where
         assign (#iterations % at loc) (Just (iteration + 1, stack))
         continue v
       -- Both paths are possible; we ask for more input
-      runBothPaths loc exploreDepth UnknownBranch =
+      runBothPaths loc exploreDepth UnknownBranch = do
         (runBoth depthLimit exploreDepth ) . PleaseRunBoth condSimp $ (runBothPaths loc exploreDepth) . Case
 
   -- numBytes allows us to specify how many bytes of the returned value is relevant

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