From 15b675ecb70e0c9a7bce3868d9b5855f00739f05 Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Mon, 27 Jan 2025 16:15:45 +0100
Subject: [PATCH] Fixing partial for missing cheatcode

---
 CHANGELOG.md      |  1 +
 src/EVM.hs        |  4 +++-
 src/EVM/Format.hs |  7 ++++++-
 src/EVM/Types.hs  |  1 +
 test/test.hs      | 21 +++++++++++++++++++--
 5 files changed, 30 insertions(+), 4 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 0bebb07a8..cb892ddf8 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -24,6 +24,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Not all testcases ran due to incorrect filtering, fixed
 - Removed dead code related to IOAct in the now deprecated and removed debugger
 - Dumping of END states (.prop) files is now default for `--debug`
+- When cheatcode is missing, we produce a partial execution warning
 
 ## [0.54.2] - 2024-12-12
 
diff --git a/src/EVM.hs b/src/EVM.hs
index 4279fd273..f658fd187 100644
--- a/src/EVM.hs
+++ b/src/EVM.hs
@@ -1732,7 +1732,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 ()
diff --git a/src/EVM/Format.hs b/src/EVM/Format.hs
index bfedd55f3..edfbf5219 100644
--- a/src/EVM/Format.hs
+++ b/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)
+    , "function selector: " <> T.pack (show selector)
+    ]
 
 formatSomeExpr :: SomeExpr -> Text
 formatSomeExpr (SomeExpr e) = formatExpr $ Expr.simplify e
diff --git a/src/EVM/Types.hs b/src/EVM/Types.hs
index 13aac47f3..8198a21fe 100644
--- a/src/EVM/Types.hs
+++ b/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
diff --git a/test/test.hs b/test/test.hs
index 24c884075..ab1c1af75 100644
--- a/test/test.hs
+++ b/test/test.hs
@@ -1310,8 +1310,25 @@ 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_cheatcode(uint) external;
+              }
+            contract C {
+              function fun(uint a) public {
+                  // Cheatcode address
+                  Vm vm = Vm(0x7109709ECfa91a80626fF3989D68f67F5b1DD12D);
+                  vm.nonexistent_cheatcode(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
+      , test "cheatcode-with-selector" $ do
         Just c <- solcRuntime "C"
             [i|
             contract C {