SymExec: default symbolic values when displaying calldata

CHANGELOG.md

@@ -11,6 +11,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 - CopySlice wraparound issue especially during CopyCallBytesToMemory
 - EVM.Solidity.toCode to include contractName in error string
+- Better cex reconstruction in cases where branches do not refer to all input variables in calldata
 
 ## Changed
 

src/EVM/SymExec.hs

@@ -812,7 +812,7 @@ formatCex cd m@(SMTCex _ _ store blockContext txContext) = T.unlines $
     -- it for branches that do not refer to calldata at all (e.g. the top level
     -- callvalue check inserted by solidity in contracts that don't have any
     -- payable functions).
-    cd' = prettyBuf $ Expr.simplify $ subModel m cd
+    cd' = prettyBuf . Expr.simplify . defaultSymbolicValues $ subModel m cd
 
     storeCex :: [Text]
     storeCex
@@ -871,23 +871,55 @@ formatCex cd m@(SMTCex _ _ store blockContext txContext) = T.unlines $
     prettyBuf :: Expr Buf -> Text
     prettyBuf (ConcreteBuf "") = "Empty"
     prettyBuf (ConcreteBuf bs) = formatBinary bs
-    prettyBuf _ = "Any"
-
--- | Takes a buffer and a Cex and replaces all abstract values in the buf with
+    prettyBuf b = internalError $ "Unexpected symbolic buffer:\n" <> T.unpack (formatExpr b)
+
+-- | If the expression contains any symbolic values, default them to some
+-- concrete value The intuition here is that if we still have symbolic values
+-- in our calldata expression after substituing in our cex, then they can have
+-- any value and we can safely pick a random value. This is a bit unsatisfying,
+-- we should really be doing smth like: https://github.com/ethereum/hevm/issues/334
+-- but it's probably good enough for now
+defaultSymbolicValues :: Expr a -> Expr a
+defaultSymbolicValues e = subBufs (foldTerm symbufs mempty e)
+                        . subVars (foldTerm symwords mempty e) $ e
+  where
+    symbufs :: Expr a -> Map (Expr Buf) ByteString
+    symbufs = \case
+      a@(AbstractBuf _) -> Map.singleton a ""
+      _ -> mempty
+    symwords :: Expr a -> Map (Expr EWord) W256
+    symwords = \case
+      a@(Var _) -> Map.singleton a 0
+      a@Origin -> Map.singleton a 0
+      a@Coinbase -> Map.singleton a 0
+      a@Timestamp -> Map.singleton a 0
+      a@BlockNumber -> Map.singleton a 0
+      a@PrevRandao -> Map.singleton a 0
+      a@GasLimit -> Map.singleton a 0
+      a@ChainId -> Map.singleton a 0
+      a@BaseFee -> Map.singleton a 0
+      _ -> mempty
+
+-- | Takes an expression and a Cex and replaces all abstract values in the buf with
 -- concrete ones from the Cex.
 subModel :: SMTCex -> Expr a -> Expr a
-subModel c expr =
-  subBufs (fmap forceFlattened c.buffers) . subVars c.vars . subStore c.store
-  . subVars c.blockContext . subVars c.txContext $ expr
+subModel c
+  = subBufs (fmap forceFlattened c.buffers)
+  . subStore c.store
+  . subVars c.vars
+  . subVars c.blockContext
+  . subVars c.txContext
   where
     forceFlattened (SMT.Flat bs) = bs
     forceFlattened b@(SMT.Comp _) = forceFlattened $
       fromMaybe (internalError $ "cannot flatten buffer: " <> show b)
                 (SMT.collapse b)
 
-    subVars model b = Map.foldlWithKey subVar b model
+subVars :: Map (Expr EWord) W256 -> Expr a -> Expr a
+subVars model b = Map.foldlWithKey subVar b model
+  where
     subVar :: Expr a -> Expr EWord -> W256 -> Expr a
-    subVar b var val = mapExpr go b
+    subVar a var val = mapExpr go a
       where
         go :: Expr a -> Expr a
         go = \case
@@ -896,9 +928,11 @@ subModel c expr =
                       else v
           e -> e
 
-    subBufs model b = Map.foldlWithKey subBuf b model
+subBufs :: Map (Expr Buf) ByteString -> Expr a -> Expr a
+subBufs model b = Map.foldlWithKey subBuf b model
+  where
     subBuf :: Expr a -> Expr Buf -> ByteString -> Expr a
-    subBuf b var val = mapExpr go b
+    subBuf x var val = mapExpr go x
       where
         go :: Expr a -> Expr a
         go = \case
@@ -907,10 +941,10 @@ subModel c expr =
                       else a
           e -> e
 
-    subStore :: Map W256 (Map W256 W256) -> Expr a -> Expr a
-    subStore m b = mapExpr go b
-      where
-        go :: Expr a -> Expr a
-        go = \case
-          AbstractStore -> ConcreteStore m
-          e -> e
+subStore :: Map W256 (Map W256 W256) -> Expr a -> Expr a
+subStore model b = mapExpr go b
+  where
+    go :: Expr a -> Expr a
+    go = \case
+      AbstractStore -> ConcreteStore model
+      e -> e

src/EVM/UnitTest.hs

@@ -19,7 +19,7 @@ import EVM.FeeSchedule qualified as FeeSchedule
 import EVM.Fetch qualified as Fetch
 import EVM.Format
 import EVM.Solidity
-import EVM.SymExec (defaultVeriOpts, symCalldata, verify, isQed, extractCex, runExpr, subModel, VeriOpts(..))
+import EVM.SymExec (defaultVeriOpts, symCalldata, verify, isQed, extractCex, runExpr, subModel, defaultSymbolicValues, VeriOpts(..))
 import EVM.Types
 import EVM.Transaction (initTx)
 import EVM.RLP
@@ -777,7 +777,7 @@ prettyCalldata cex buf sig types = head (Text.splitOn "(" sig) <> showCalldata c
 showCalldata :: (?context :: DappContext) => SMTCex -> [AbiType] -> Expr Buf -> Text
 showCalldata cex tps buf = "(" <> intercalate "," (fmap showVal vals) <> ")"
   where
-    argdata = Expr.drop 4 $ simplify $ subModel cex buf
+    argdata = Expr.drop 4 . simplify . defaultSymbolicValues $ subModel cex buf
     vals = case decodeBuf tps argdata of
              CAbi v -> v
              _ -> internalError $ "unable to abi decode function arguments:\n" <> (Text.unpack $ formatExpr argdata)

test/test.hs

@@ -57,7 +57,7 @@ import EVM.SMT hiding (one)
 import EVM.Solidity
 import EVM.Solvers
 import EVM.Stepper qualified as Stepper
-import EVM.SymExec
+import EVM.SymExec hiding (subStore)
 import EVM.Test.Tracing qualified as Tracing
 import EVM.Test.Utils
 import EVM.Traversals