Update

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
@@ -1736,10 +1737,12 @@ cheat gas (inOffset, inSize) (outOffset, outSize) xs = do
       Nothing -> partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) "symbolic cheatcode selector" (wrap [abi])
     Just concAbi -> runCheat concAbi input
   where
-    runCheat abi input =  do
-      let abi' = unsafeInto abi
+    runCheat concAbi input =  do
+      let abi' = unsafeInto concAbi
       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 ()
@@ -1911,9 +1914,11 @@ cheatActions = Map.fromList
       \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
-            doStop
+            frameReturn $ AbiUInt 256 (fromIntegral blockNo)
         _ -> vmError (BadCheatCode "createSelectFork(string,uint256) parameter decoding failed" sig)
 
   , action "activeFork()" $

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
@@ -239,9 +240,12 @@ oracle solvers info q = do
              internalError $ "oracle error: " ++ show q
 
     PleaseFetchBlock url blockNo continue -> do
-         liftIO $ fetchBlockFrom (EVM.Fetch.BlockNumber blockNo) (pack url) >>= \case
-           Just block  -> pure (continue block)
-           Nothing -> internalError $ "oracle error: " ++ show q
+      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

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

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 {