Symbolic fallback for EXTCODESIZE and optinally for CALL

cli/cli.hs

@@ -103,6 +103,7 @@ data Command w
       , loopDetectionHeuristic :: w ::: LoopHeuristic <!> "StackBased" <?> "Which heuristic should be used to determine if we are in a loop: StackBased (default) or Naive"
       , noDecompose   :: w ::: Bool               <?> "Don't decompose storage slots into separate arrays"
       , maxBranch     :: w ::: Int                <!> "10" <?> "Max number of branches to explore when encountering a symbolic value (default: 10)"
+      , promiseNoReent:: w ::: Bool               <!> "Promise no reentrancy is possible into the contrct(s) being examined"
       }
   | Equivalence -- prove equivalence between two programs
       { codeA         :: w ::: ByteString       <?> "Bytecode of the first program"
@@ -124,6 +125,7 @@ data Command w
       , loopDetectionHeuristic :: w ::: LoopHeuristic <!> "StackBased" <?> "Which heuristic should be used to determine if we are in a loop: StackBased (default) or Naive"
       , noDecompose   :: w ::: Bool             <?> "Don't decompose storage slots into separate arrays"
       , maxBranch     :: w ::: Int              <!> "10" <?> "Max number of branches to explore when encountering a symbolic value (default: 10)"
+      , promiseNoReent:: w ::: Bool               <!> "Promise no reentrancy is possible into the contrct(s) being examined"
       }
   | Exec -- Execute a given program with specified env & calldata
       { code        :: w ::: Maybe ByteString  <?> "Program bytecode"
@@ -176,6 +178,7 @@ data Command w
       , maxBranch     :: w ::: Int                      <!> "10" <?> "Max number of branches to explore when encountering a symbolic value (default: 10)"
       , numCexFuzz    :: w ::: Integer                  <!> "3" <?> "Number of fuzzing tries to do to generate a counterexample (default: 3)"
       , askSmtIterations :: w ::: Integer               <!> "1" <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 1)"
+      , promiseNoReent:: w ::: Bool               <!> "Promise no reentrancy is possible into the contrct(s) being examined"
       }
   | Version
 
@@ -263,6 +266,7 @@ equivalence cmd = do
                             , askSmtIters = cmd.askSmtIterations
                             , loopHeuristic = cmd.loopDetectionHeuristic
                             , rpcInfo = Nothing
+                            , promiseNoReent = cmd.promiseNoReent
                             }
     calldata <- liftIO $ buildCalldata cmd
     solver <- liftIO $ getSolver cmd

src/EVM.hs

@@ -25,6 +25,7 @@ import EVM.Sign qualified
 import EVM.Concrete qualified as Concrete
 import EVM.CheatsTH
 import EVM.Expr (maybeLitByteSimp, maybeLitWordSimp, maybeLitAddrSimp)
+import EVM.Effects (Config (..))
 
 import Control.Monad (unless, when)
 import Control.Monad.ST (ST)
@@ -288,20 +289,9 @@ getOpW8 state = case state.code of
 getOpName :: forall (t :: VMType) s . FrameState t s -> [Char]
 getOpName state = intToOpName $ fromEnum $ getOpW8 state
 
--- If the address is already in the cache, or can be obtained via API, return True
--- otherwise, return False
-canFetchAccount :: forall (t :: VMType) s . VMOps t => Expr EAddr -> EVM t s (Bool)
-canFetchAccount addr = do
-  use (#env % #contracts % at addr) >>= \case
-    Just _ -> pure True
-    Nothing -> case addr of
-      LitAddr _ -> pure True
-      SymAddr _ -> pure False
-      GVar _ -> internalError "GVar not allowed here"
-
 -- | Executes the EVM one step
-exec1 :: forall (t :: VMType) s. VMOps t => EVM t s ()
-exec1 = do
+exec1 :: forall (t :: VMType) s. (VMOps t) => Config ->  EVM t s ()
+exec1 conf = do
   vm <- get
 
   let
@@ -459,7 +449,7 @@ exec1 = do
 
         OpBalance ->
           case stk of
-            x:xs -> forceAddr x "BALANCE" $ \a ->
+            x:xs -> forceAddr x (defaultFallback "BALANCE") $ \a ->
               accessAndBurn a $
                 fetchAccount a $ \c -> do
                   next
@@ -519,9 +509,9 @@ exec1 = do
 
         OpExtcodesize ->
           case stk of
-            x':xs -> forceAddr x' "EXTCODESIZE" $ \x -> do
+            x':xs -> forceAddr x' (symbolicFallback xs) $ \x -> do
               let impl = accessAndBurn x $
-                           fetchAccount x $ \c -> do
+                           fetchAccountWithFallback x (symbolicFallback xs) $ \c -> do
                              next
                              assign (#state % #stack) xs
                              case view bytecode c of
@@ -541,7 +531,7 @@ exec1 = do
         OpExtcodecopy ->
           case stk of
             extAccount':memOffset:codeOffset:codeSize:xs ->
-              forceAddr extAccount' "EXTCODECOPY" $ \extAccount -> do
+              forceAddr extAccount' (defaultFallback "EXTCODECOPY") $ \extAccount -> do
                 burnExtcodecopy extAccount codeSize $
                   accessMemoryRange memOffset codeSize $
                     fetchAccount extAccount $ \c -> do
@@ -580,7 +570,7 @@ exec1 = do
 
         OpExtcodehash ->
           case stk of
-            x':xs -> forceAddr x' "EXTCODEHASH" $ \x ->
+            x':xs -> forceAddr x' (defaultFallback "EXTCODEHASH") $ \x ->
               accessAndBurn x $ do
                 next
                 assign (#state % #stack) xs
@@ -881,13 +871,17 @@ exec1 = do
           case stk of
             xGas:xTo':xValue:xInOffset:xInSize:xOutOffset:xOutSize:xs ->
               branch (Expr.gt xValue (Lit 0)) $ \gt0 -> do
+                let addrFallback = if conf.promiseNoReent then const fallback
+                                   else defaultFallback "unable to determine a call target"
                 (if gt0 then notStatic else id) $
-                  forceAddr xTo' "unable to determine a call target" $ \xTo ->
+                  forceAddr xTo' addrFallback $ \xTo ->
                     case gasTryFrom xGas of
                       Left _ -> vmError IllegalOverflow
                       Right gas -> do
                         overrideC <- use $ #state % #overrideCaller
-                        delegateCall this gas xTo xTo xValue xInOffset xInSize xOutOffset xOutSize xs unknownCodeFallback $
+                        let delegateFallback = if conf.promiseNoReent then const fallback
+                                               else unknownCodeFallback
+                        delegateCall this gas xTo xTo xValue xInOffset xInSize xOutOffset xOutSize xs delegateFallback $
                           \callee -> do
                             let from' = fromMaybe self overrideC
                             zoom #state $ do
@@ -897,13 +891,13 @@ exec1 = do
                             touchAccount from'
                             touchAccount callee
                             transfer from' callee xValue
-            _ ->
-              underrun
+              where fallback = genericFreshFallback "CALL" xs
+            _ -> underrun
 
         OpCallcode ->
           case stk of
             xGas:xTo':xValue:xInOffset:xInSize:xOutOffset:xOutSize:xs ->
-              forceAddr xTo' "unable to determine a call target" $ \xTo ->
+              forceAddr xTo' (defaultFallback "unable to determine a call target") $ \xTo ->
                 case gasTryFrom xGas of
                   Left _ -> vmError IllegalOverflow
                   Right gas -> do
@@ -998,39 +992,25 @@ exec1 = do
                 Just xTo' -> do
                   case gasTryFrom xGas of
                     Left _ -> vmError IllegalOverflow
-                    Right gas -> canFetchAccount xTo' >>= \case
-                      False -> fallback
-                      True -> do
-                        overrideC <- use $ #state % #overrideCaller
-                        delegateCall this gas xTo' xTo' (Lit 0) xInOffset xInSize xOutOffset xOutSize xs (const fallback) $
-                          \callee -> do
-                            zoom #state $ do
-                              assign #callvalue (Lit 0)
-                              assign #caller $ fromMaybe self overrideC
-                              assign #contract callee
-                              assign #static True
-                            touchAccount self
-                            touchAccount callee
-              where
-                fallback :: EVM t s ()
-                fallback = do
-                  -- Reset caller if needed
-                  resetCaller <- use $ #state % #resetCaller
-                  when resetCaller $ assign (#state % #overrideCaller) Nothing
-                  -- overapproximate by returning a symbolic value
-                  freshVar <- use #freshVar
-                  assign #freshVar (freshVar + 1)
-                  let freshVarExpr = Var ("staticcall-result-stack-" <> (pack . show) freshVar)
-                  modifying #constraints ((:) (PLEq freshVarExpr (Lit 1) ))
-                  assign (#state % #returndata) (AbstractBuf ("staticall-result-data-" <> (pack . show) freshVar))
-                  next >> assign (#state % #stack) (freshVarExpr:xs)
+                    Right gas -> do
+                      overrideC <- use $ #state % #overrideCaller
+                      delegateCall this gas xTo' xTo' (Lit 0) xInOffset xInSize xOutOffset xOutSize xs (const fallback) $
+                        \callee -> do
+                          zoom #state $ do
+                            assign #callvalue (Lit 0)
+                            assign #caller $ fromMaybe self overrideC
+                            assign #contract callee
+                            assign #static True
+                          touchAccount self
+                          touchAccount callee
+              where fallback = genericFreshFallback "STATICCALL" xs
             _ -> underrun
 
         OpSelfdestruct ->
           notStatic $
           case stk of
             [] -> underrun
-            (xTo':_) -> forceAddr xTo' "SELFDESTRUCT" $ \case
+            (xTo':_) -> forceAddr xTo' (defaultFallback "SELFDESTRUCT") $ \case
               xTo@(LitAddr _) -> do
                 cc <- gets (.tx.subState.createdContracts)
                 let createdThisTr = self `member` cc
@@ -1407,16 +1387,18 @@ query q = assign #result $ Just $ HandleEffect (Query q)
 runBoth :: RunBoth s -> EVM Symbolic s ()
 runBoth c = assign #result $ Just $ HandleEffect (RunBoth c)
 
--- | Construct RPC Query and halt execution until resolved
-fetchAccount :: VMOps t => Expr EAddr -> (Contract -> EVM t s ()) -> EVM t s ()
+fetchAccount  :: VMOps t => Expr EAddr -> (Contract -> EVM t s ()) -> EVM t s ()
 fetchAccount addr continue =
+  let fallback = defaultFallback "trying to access a symbolic address that isn't already present in storage"
+  in fetchAccountWithFallback addr fallback continue
+
+-- | Construct RPC Query and halt execution until resolved
+fetchAccountWithFallback :: VMOps t => Expr EAddr -> (Expr EAddr -> EVM t s ()) -> (Contract -> EVM t s ()) -> EVM t s ()
+fetchAccountWithFallback addr fallback continue =
   use (#env % #contracts % at addr) >>= \case
     Just c -> continue c
     Nothing -> case addr of
-      SymAddr _ -> do
-        pc <- use (#state % #pc)
-        state <- use #state
-        partial $ UnexpectedSymbolicArg pc (getOpName state) "trying to access a symbolic address that isn't already present in storage" (wrap [addr])
+      SymAddr _ -> fallback addr
       LitAddr a -> do
         use (#cache % #fetched % at a) >>= \case
           Just c -> do
@@ -1614,15 +1596,43 @@ notStatic continue = do
     then vmError StateChangeWhileStatic
     else continue
 
-forceAddr :: VMOps t => Expr EWord -> String -> (Expr EAddr -> EVM t s ()) -> EVM t s ()
-forceAddr n msg continue = case wordToAddr n of
+forceAddr :: VMOps t =>
+  Expr EWord
+  -> (Expr EWord -> EVM t s ())
+  -> (Expr EAddr -> EVM t s ())
+  -> EVM t s ()
+forceAddr n fallback continue = case wordToAddr n of
   Nothing -> manySolutions n 20 $ \case
     Just sol -> continue $ LitAddr (truncateToAddr sol)
-    Nothing -> fallback
+    Nothing -> fallback n
   Just c -> continue c
-  where fallback = do
-          vm <- get
-          partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) msg (wrap [n])
+
+defaultFallback :: (Typeable a, VMOps t) => String -> Expr a -> EVM t s ()
+defaultFallback msg n = do
+  vm <- get
+  partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) msg (wrap [n])
+
+genericFreshFallback :: (VMOps t, ?op :: Word8) => String -> [Expr EWord] -> EVM t s ()
+genericFreshFallback str xs = do
+  -- Reset caller if needed
+  resetCaller <- use $ #state % #resetCaller
+  when resetCaller $ assign (#state % #overrideCaller) Nothing
+  -- overapproximate by returning a symbolic value
+  freshVar <- use #freshVar
+  assign #freshVar (freshVar + 1)
+  let freshVarExpr = Var ("staticcall-result-stack-" <> (pack . show) freshVar)
+  modifying #constraints ((:) (PLEq freshVarExpr (Lit 1) ))
+  assign (#state % #returndata) (AbstractBuf ((pack str) <> "-result-data-" <> (pack . show) freshVar))
+  next >> assign (#state % #stack) (freshVarExpr:xs)
+
+symbolicFallback:: (VMOps t, ?op :: Word8) => [Expr EWord] -> Expr a -> EVM t s ()
+symbolicFallback xs _ = do
+  next
+  freshVar <- use #freshVar
+  assign #freshVar (freshVar + 1)
+  let freshVarExpr = Var ("symbolicFallback-" <> (pack . show) freshVar)
+  assign (#state % #stack) xs
+  pushSym freshVarExpr
 
 forceConcrete :: VMOps t => Expr EWord -> String -> (W256 -> EVM t s ()) -> EVM t s ()
 forceConcrete n = forceConcreteLimitSz n 32
@@ -1789,7 +1799,7 @@ cheatActions = Map.fromList
   , action "deal(address,uint256)" $
       \sig input -> case decodeStaticArgs 0 2 input of
         [a, amt] ->
-          forceAddr a "vm.deal: cannot decode target into an address" $ \usr ->
+          forceAddr a (defaultFallback "vm.deal: cannot decode target into an address") $ \usr ->
             fetchAccount usr $ \_ -> do
               assign (#env % #contracts % ix usr % #balance) amt
               doStop
@@ -2100,7 +2110,7 @@ delegateCall this gasGiven xTo xContext xValue xInOffset xInSize xOutOffset xOut
           resetCaller <- use $ #state % #resetCaller
           when resetCaller $ assign (#state % #overrideCaller) Nothing
           vm0 <- get
-          fetchAccount xTo $ \target -> case target.code of
+          fetchAccountWithFallback xTo fallback $ \target -> case target.code of
               UnknownCode _ -> fallback xTo
               _ -> do
                 burn' xGas $ do

src/EVM/Effects.hs

@@ -44,6 +44,7 @@ data Config = Config
   , onlyCexFuzz      :: Bool
   , decomposeStorage :: Bool
   , maxNumBranch     :: Int
+  , promiseNoReent   :: Bool
   }
   deriving (Show, Eq)
 
@@ -58,6 +59,7 @@ defaultConfig = Config
   , onlyCexFuzz  = False
   , decomposeStorage = True
   , maxNumBranch = 10
+  , promiseNoReent = False
   }
 
 -- Write to the console

src/EVM/Exec.hs

@@ -10,6 +10,7 @@ import Data.ByteString (ByteString)
 import Data.Maybe (isNothing)
 import Optics.Core
 import Control.Monad.ST (ST)
+import EVM.Effects (Config)
 
 ethrunAddress :: Addr
 ethrunAddress = Addr 0x00a329c0648769a73afac7f9381e08fb43dbea72
@@ -46,18 +47,18 @@ vmForEthrunCreation creationCode =
     }) <&> set (#env % #contracts % at (LitAddr ethrunAddress))
              (Just (initialContract (RuntimeCode (ConcreteRuntimeCode ""))))
 
-exec :: VMOps t => EVM t s (VMResult t s)
-exec = do
+exec :: (VMOps t) => Config -> EVM t s (VMResult t s)
+exec conf = do
   vm <- get
   case vm.result of
-    Nothing -> exec1 >> exec
+    Nothing -> exec1 conf >> exec conf
     Just r -> pure r
 
-run :: VMOps t => EVM t s (VM t s)
-run = do
+run :: (VMOps t) => Config -> EVM t s (VM t s)
+run conf = do
   vm <- get
   case vm.result of
-    Nothing -> exec1 >> run
+    Nothing -> exec1 conf >> run conf
     Just _ -> pure vm
 
 execWhile :: (VM t s -> Bool) -> State (VM t s) Int

src/EVM/Stepper.hs

@@ -108,7 +108,8 @@ interpret fetcher vm = eval . view
     eval (action :>>= k) =
       case action of
         Exec -> do
-          (r, vm') <- liftIO $ stToIO $ runStateT EVM.Exec.exec vm
+          conf <- readConfig
+          (r, vm') <- liftIO $ stToIO $ runStateT (EVM.Exec.exec conf) vm
           interpret fetcher vm' (k r)
         Wait q -> do
           m <- fetcher q

src/EVM/SymExec.hs

@@ -313,7 +313,8 @@ interpret fetcher maxIter askSmtIters heuristic vm =
   eval (action Operational.:>>= k) =
     case action of
       Stepper.Exec -> do
-        (r, vm') <- liftIO $ stToIO $ runStateT exec vm
+        conf <- readConfig
+        (r, vm') <- liftIO $ stToIO $ runStateT (exec conf) vm
         interpret fetcher maxIter askSmtIters heuristic vm' (k r)
       Stepper.Fork (PleaseRunBoth cond continue) -> do
         frozen <- liftIO $ stToIO $ freezeVM vm

test/EVM/Test/Tracing.hs

@@ -17,7 +17,7 @@ import Control.Monad.Operational qualified as Operational
 import Control.Monad.ST (RealWorld, ST, stToIO)
 import Control.Monad.State.Strict (StateT(..))
 import Control.Monad.State.Strict qualified as State
-import Control.Monad.Reader (ReaderT)
+import Control.Monad.Reader (ReaderT, lift)
 import Data.Aeson ((.:), (.:?))
 import Data.Aeson qualified as JSON
 import Data.ByteString (ByteString)
@@ -542,11 +542,12 @@ runWithTrace :: App m => StateT (TraceState RealWorld) m (VM Concrete RealWorld)
 runWithTrace = do
   -- This is just like `exec` except for every instruction evaluated,
   -- we also increment a counter indexed by the current code location.
+  conf <- lift readConfig
   vm0 <- use _1
   case vm0.result of
     Nothing -> do
       State.modify' (\(a, b) -> (a, b ++ [vmtrace vm0]))
-      vm' <- liftIO $ stToIO $ State.execStateT exec1 vm0
+      vm' <- liftIO $ stToIO $ State.execStateT (exec1 conf) vm0
       assign _1 vm'
       runWithTrace
     Just (VMFailure _) -> do