Merge pull request #640 from ethereum/fix-partial

Fixing partial warning for missing cheatcode

CHANGELOG.md

@@ -26,6 +26,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Base case of exponentiation to 0 was not handled, leading to infinite loop
 - Better exponential simplification
 - 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
 

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 ()

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

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,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 {