Having a go at implementing createSelectFork

CHANGELOG.md

@@ -16,6 +16,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   and continue running, whenever possible
 - STATICCALL abstraction is now performed in case of symbolic arguments
 - Better error messages for JSON parsing
+- Added support for createSelectFork(string,uint256)
 
 ## Fixed
 - We now try to simplify expressions fully before trying to cast them to a concrete value

src/EVM.hs

@@ -67,6 +67,7 @@ import Witch (into, tryFrom, unsafeInto, tryInto)
 import Crypto.Hash (Digest, SHA256, RIPEMD160)
 import Crypto.Hash qualified as Crypto
 import Crypto.Number.ModArithmetic (expFast)
+import Debug.Trace (traceM)
 
 blankState :: VMOps t => ST s (FrameState t s)
 blankState = do
@@ -1407,6 +1408,13 @@ query q = assign #result $ Just $ HandleEffect (Query q)
 choose :: Choose s -> EVM Symbolic s ()
 choose c = assign #result $ Just $ HandleEffect (Choose c)
 
+fetchBlockFrom :: VMOps t => String -> W256 -> (Block -> EVM t s ()) -> EVM t s ()
+fetchBlockFrom url blockNo continue = do
+      assign (#result) . Just . HandleEffect . Query $
+        PleaseFetchBlock url blockNo $ \c -> do
+          assign #result Nothing
+          continue c
+
 -- | Construct RPC Query and halt execution until resolved
 fetchAccount :: VMOps t => Expr EAddr -> (Contract -> EVM t s ()) -> EVM t s ()
 fetchAccount addr continue =
@@ -1732,7 +1740,9 @@ cheat gas (inOffset, inSize) (outOffset, outSize) xs = do
     runCheat abi input =  do
       let abi' = unsafeInto abi
       case Map.lookup abi' cheatActions of
-        Nothing -> vmError (BadCheatCode "Cannot understand cheatcode." abi')
+        Nothing -> do
+          vm <- get
+          partial $ CheatCodeMissing vm.state.pc abi'
         Just action -> action input
 
 type CheatAction t s = Expr Buf -> EVM t s ()
@@ -1900,6 +1910,17 @@ cheatActions = Map.fromList
                 vmError (NonexistentFork forkId')
         _ -> vmError (BadCheatCode "selectFork(uint256) parameter decoding failed" sig)
 
+  , action "createSelectFork(string,uint256)" $
+      \sig input -> case decodeBuf [AbiStringType, AbiUIntType 256] input of
+        CAbi [AbiString url, AbiUInt 256 blockNo] -> do
+          let blockNo' = fromIntegral blockNo
+          -- doStop
+          fetchBlockFrom (BS8.unpack url) blockNo' $ \block -> do
+            traceM $ "here, continuing with block:" <> show  block
+            assign #block block
+            frameReturn $ AbiUInt 256 (fromIntegral blockNo)
+        _ -> vmError (BadCheatCode "createSelectFork(string,uint256) parameter decoding failed" sig)
+
   , action "activeFork()" $
       \_ _ -> do
         vm <- get

src/EVM/Fetch.hs

@@ -29,6 +29,7 @@ import System.Process
 import Control.Monad.IO.Class
 import Control.Monad (when)
 import EVM.Effects
+import Debug.Trace (traceM)
 
 -- | Abstract representation of an RPC fetch request
 data RpcQuery a where
@@ -238,6 +239,14 @@ oracle solvers info q = do
            Nothing ->
              internalError $ "oracle error: " ++ show q
 
+    PleaseFetchBlock url blockNo continue -> do
+      traceM $ "Fetching block " <> show blockNo <> " from " <> show url
+      liftIO $ fetchBlockFrom (EVM.Fetch.BlockNumber blockNo) (pack url) >>= \case
+        Just block  -> do
+          putStrLn $ "Fetched block " <> show blockNo <> " from " <> show url <> " block:  " <> show block
+          pure (continue block)
+        Nothing -> internalError $ "oracle error: " ++ show q
+
     PleaseReadEnv variable continue -> do
       value <- liftIO $ lookupEnv variable
       pure . continue $ fromMaybe "" value

src/EVM/Format.hs

@@ -465,7 +465,7 @@ formatError = \case
 
 formatPartial :: PartialExec -> Text
 formatPartial = \case
-  (UnexpectedSymbolicArg pc opcode msg args) -> T.unlines
+  UnexpectedSymbolicArg pc opcode msg args -> T.unlines
     [ "Unexpected Symbolic Arguments to Opcode"
     , indent 2 $ T.unlines
       [ "msg: " <> T.pack (show msg)
@@ -477,6 +477,11 @@ formatPartial = \case
     ]
   MaxIterationsReached pc addr -> "Max Iterations Reached in contract: " <> formatAddr addr <> " pc: " <> pack (show pc) <> " To increase the maximum, set a fixed large (or negative) value for `--max-iterations` on the command line"
   JumpIntoSymbolicCode pc idx -> "Encountered a jump into a potentially symbolic code region while executing initcode. pc: " <> pack (show pc) <> " jump dst: " <> pack (show idx)
+  CheatCodeMissing pc selector ->T.unlines
+    [ "Cheat code not recognized"
+    , "program counter: " <> T.pack (show pc)
+    , "selector: " <> T.pack (show selector)
+    ]
 
 formatSomeExpr :: SomeExpr -> Text
 formatSomeExpr (SomeExpr e) = formatExpr $ Expr.simplify e

src/EVM/Types.hs

@@ -581,6 +581,7 @@ data PartialExec
   = UnexpectedSymbolicArg { pc :: Int, opcode :: String, msg  :: String, args  :: [SomeExpr] }
   | MaxIterationsReached  { pc :: Int, addr :: Expr EAddr }
   | JumpIntoSymbolicCode  { pc :: Int, jumpDst :: Int }
+  | CheatCodeMissing      { pc :: Int, selector :: FunctionSelector }
   deriving (Show, Eq, Ord)
 
 -- | Effect types used by the vm implementation for side effects & control flow
@@ -593,6 +594,7 @@ deriving instance Show (Effect t s)
 data Query t s where
   PleaseFetchContract :: Addr -> BaseState -> (Contract -> EVM t s ()) -> Query t s
   PleaseFetchSlot     :: Addr -> W256 -> (W256 -> EVM t s ()) -> Query t s
+  PleaseFetchBlock    :: String -> W256 -> (Block -> EVM t s ()) -> Query t s
   PleaseAskSMT        :: Expr EWord -> [Prop] -> (BranchCondition -> EVM Symbolic s ()) -> Query Symbolic s
   PleaseGetSol        :: Expr EWord -> [Prop] -> (Maybe W256 -> EVM Symbolic s ()) -> Query Symbolic s
   PleaseDoFFI         :: [String] -> Map String String -> (ByteString -> EVM t s ()) -> Query t s
@@ -609,11 +611,15 @@ data BranchCondition = Case Bool | Unknown
 instance Show (Query t s) where
   showsPrec _ = \case
     PleaseFetchContract addr base _ ->
-      (("<EVM.Query: fetch contract " ++ show addr ++ show base ++ ">") ++)
+      (("<EVM.Query: fetch from contract " ++ show addr ++ show base ++ ">") ++)
     PleaseFetchSlot addr slot _ ->
       (("<EVM.Query: fetch slot "
         ++ show slot ++ " for "
         ++ show addr ++ ">") ++)
+    PleaseFetchBlock url block _ ->
+      (("<EVM.Query: fetch from url "
+        ++ show url ++ " block "
+        ++ show block ++ ">") ++)
     PleaseAskSMT condition constraints _ ->
       (("<EVM.Query: ask SMT about "
         ++ show condition ++ " in context "

test/test.hs

@@ -1310,8 +1310,23 @@ tests = testGroup "hevm"
             |]
         r <- allBranchesFail c Nothing
         assertBoolM "all branches must fail" (isRight r)
-      ,
-      test "cheatcode-with-selector" $ do
+      , test "cheatcode-nonexistent" $ do
+        Just c <- solcRuntime "C"
+            [i|
+              interface Vm {
+                function nonexistent(uint) external;
+              }
+            contract C {
+              function fun(uint a) public {
+                  Vm vm = Vm(0x7109709ECfa91a80626fF3989D68f67F5b1DD12D);
+                  vm.nonexistent(a);
+                  assert(1 == 1);
+              }
+            }
+            |]
+        let sig = Just (Sig "fun(uint256)" [AbiUIntType 256])
+        (e, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
+        assertBoolM "The expression must contain Partial." $ Expr.containsNode isPartial e
         Just c <- solcRuntime "C"
             [i|
             contract C {