SymExec: default symbolic values when displaying calldata

Sometimes we get back a model that does not mention all variables that
are present in the input calldata buffer. This can happen if those
variables are not relevant to the branch that we are producing a model
for.

In this case we can simply set the values that remain symbolic afters
subsituting in our cex to some default value. We will still have issues
here if we have lost some constraints over those variables during
simplification, but it's better than what we're doing now (i.e. just
printing "Any" if we can't get a fully concrete model for calldata out).

A fully general (and hopefully correct) approach could look like:
#334

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)