fix(symbolic): include the cheatcode address in EXTCODE* candidates

crates/cheatcodes/src/inspector.rs

@@ -1174,18 +1174,7 @@ impl<FEN: FoundryEvmNetwork> Cheatcodes<FEN> {
         gas: &mut GasTracker,
         executor: &mut dyn CheatcodesExecutor<FEN>,
     ) -> Result {
-        // decode the cheatcode call
-        let decoded = Vm::VmCalls::abi_decode(&message.input).map_err(|e| {
-            if let alloy_sol_types::Error::UnknownSelector { name: _, selector } = e {
-                let msg = format!(
-                    "unknown cheatcode with selector {selector}; \
-                     you may have a mismatch between the `Vm` interface (likely in `forge-std`) \
-                     and the `forge` version"
-                );
-                return alloy_sol_types::Error::Other(std::borrow::Cow::Owned(msg));
-            }
-            e
-        })?;
+        let decoded = decode_cheatcode_call(&message.input)?;
 
         let caller = message.caller;
 
@@ -3713,6 +3702,21 @@ const fn cheatcode_signature(cheat: &spec::Cheatcode<'static>) -> &'static str {
 }
 
 /// Dispatches the cheatcode call to the appropriate function.
+/// Decodes a cheatcode call, reporting an unknown selector as a `Vm` interface mismatch.
+pub fn decode_cheatcode_call(input: &[u8]) -> alloy_sol_types::Result<Vm::VmCalls> {
+    Vm::VmCalls::abi_decode(input).map_err(|e| {
+        if let alloy_sol_types::Error::UnknownSelector { name: _, selector } = e {
+            let msg = format!(
+                "unknown cheatcode with selector {selector}; \
+                 you may have a mismatch between the `Vm` interface (likely in `forge-std`) \
+                 and the `forge` version"
+            );
+            return alloy_sol_types::Error::Other(std::borrow::Cow::Owned(msg));
+        }
+        e
+    })
+}
+
 fn apply_dispatch<FEN: FoundryEvmNetwork>(
     calls: &Vm::VmCalls,
     ccx: &mut CheatsCtxt<'_, '_, FEN>,

crates/cheatcodes/src/lib.rs

@@ -31,7 +31,7 @@ pub use config::CheatsConfig;
 pub use error::{Error, ErrorKind, Result};
 pub use inspector::{
     BroadcastableTransaction, BroadcastableTransactions, Cheatcodes, CheatcodesExecutor,
-    StorageHook, message_result, revert_frame,
+    StorageHook, decode_cheatcode_call, message_result, revert_frame,
 };
 pub use spec::{CheatcodeDef, Vm};
 

crates/evm/symbolic/Cargo.toml

@@ -16,6 +16,7 @@ workspace = true
 [dependencies]
 foundry-common.workspace = true
 foundry-config.workspace = true
+foundry-cheatcodes.workspace = true
 foundry-cheatcodes-spec.workspace = true
 foundry-evm.workspace = true
 

crates/evm/symbolic/src/executor/calls.rs

@@ -1,4 +1,5 @@
 use super::*;
+use foundry_cheatcodes_spec::Vm::VmCalls;
 
 impl SymbolicExecutor {
     pub(super) fn call(
@@ -1575,9 +1576,20 @@ impl SymbolicExecutor {
                 SymBoolExpr::eq(&mut self.cx, target.clone(), address)
             })
             .collect::<Vec<_>>();
+        // The cheatcode addresses have code, so an unconstrained target may alias them. They are
+        // not call candidates: Forge fails a call to them that its cheatcode decoder rejects.
+        let cheatcode_constraints =
+            [CHEATCODE_ADDRESS, SYMBOLIC_VM_COMPAT_ADDRESS].map(|address| {
+                let address = SymExpr::constant(&mut self.cx, address_word(address));
+                SymBoolExpr::eq(&mut self.cx, target.clone(), address)
+            });
         let mut outside_constraints = state.constraints.clone();
         outside_constraints.extend(
-            candidate_constraints.iter().cloned().map(|condition| condition.not(&mut self.cx)),
+            candidate_constraints
+                .iter()
+                .chain(&cheatcode_constraints)
+                .cloned()
+                .map(|condition| condition.not(&mut self.cx)),
         );
         let outside_sat = self.is_sat_with_state(state, &outside_constraints)?;
 
@@ -1674,6 +1686,38 @@ impl SymbolicExecutor {
         }
 
         let call_input = in_size.read_from_memory(&mut self.cx, &state.memory, in_offset.clone());
+        let mut cheatcode_branch = state.clone();
+        let is_cheatcode = SymBoolExpr::or(&mut self.cx, cheatcode_constraints.to_vec());
+        cheatcode_branch.constraints.push(is_cheatcode);
+        if self.is_sat_with_state(&cheatcode_branch, &cheatcode_branch.constraints)? {
+            // The decoder error only depends on the selector, except for shorter calldata.
+            let input = if call_input.len() < 4 {
+                call_input.clone()
+            } else {
+                call_input.slice_concrete(&mut self.cx, 0, 4)
+            };
+            let input = input.concrete_bytes(&mut self.cx, "symbolic cheatcode selector")?;
+            if let Ok(selector) = <[u8; 4]>::try_from(input.as_slice())
+                && VmCalls::signature_by_selector(selector).is_some()
+            {
+                return Err(SymbolicError::Unsupported("symbolic cheatcode CALL target"));
+            }
+            let Err(error) = decode_cheatcode_call(&input) else {
+                return Err(SymbolicError::Unsupported("symbolic cheatcode CALL target"));
+            };
+            // Like Forge, a cheatcode call leaves `vm.expectRevert` and `vm.assumeNoRevert`
+            // pending.
+            let return_data = error_string_return_data(&mut self.cx, &error.to_string());
+            revert_cheatcode_call(
+                &mut self.cx,
+                &mut cheatcode_branch,
+                out_offset.clone(),
+                &out_size,
+                return_data,
+            )?;
+            parents.push_back(cheatcode_branch);
+        }
+
         for (to, constraint) in candidates.into_iter().zip(candidate_constraints) {
             let mut branch = state.clone();
             branch.constraints.push(constraint);

crates/evm/symbolic/src/lib.rs

@@ -26,6 +26,7 @@ use evm2::{
         secp256k1, secp256r1,
     },
 };
+use foundry_cheatcodes::decode_cheatcode_call;
 use foundry_cheatcodes_spec::{SymbolicVm, Vm};
 use foundry_common::FoundryTransactionBuilder;
 use foundry_config::{SymbolicConfig, SymbolicExplorationOrder, SymbolicStorageLayout};

crates/evm/symbolic/src/runtime/cheatcodes.rs

@@ -408,6 +408,22 @@ pub(crate) fn complete_cheatcode_call(
     Ok(())
 }
 
+/// Completes a cheatcode call that reverts with `return_data`, which can be the reverter of a
+/// pending `vm.expectRevert`.
+pub(crate) fn revert_cheatcode_call(
+    cx: &mut SymCx,
+    state: &mut PathState,
+    out_offset: SymExpr,
+    out_size: &BoundedCopySize,
+    return_data: SymReturnData,
+) -> Result<(), SymbolicError> {
+    state.first_failed_callee.get_or_insert(CHEATCODE_ADDRESS);
+    state.return_data = return_data;
+    state.copy_call_output_offset(cx, out_offset, out_size)?;
+    state.stack.push(SymExpr::zero(cx))?;
+    Ok(())
+}
+
 pub(crate) fn storage_slots_abi_array(cx: &mut SymCx, slots: Vec<SymExpr>) -> SymbolicAbiValue {
     SymbolicAbiValue::Array {
         elements: slots

crates/evm/symbolic/src/runtime/state.rs

@@ -2184,9 +2184,7 @@ impl SymbolicWorld {
         let expr = address_expr;
         let representative = expr.representative_symbolic_address();
         let mut result = self.balance_word_for_address(cx, executor, representative);
-        // Cheatcode accounts can hold balances even though they are not code candidates.
-        let cheatcode_addresses = [CHEATCODE_ADDRESS, SYMBOLIC_VM_COMPAT_ADDRESS];
-        for address in self.known_addresses(executor).into_iter().chain(cheatcode_addresses) {
+        for address in self.known_addresses(executor) {
             let balance = self.balance_word_for_address(cx, executor, address);
             let address = SymExpr::constant(cx, address_word(address));
             let condition = SymBoolExpr::eq(cx, expr.clone(), address);
@@ -2538,7 +2536,10 @@ impl SymbolicWorld {
     ) -> Result<Vec<Address>, SymbolicError> {
         let mut targets = Vec::new();
         for address in self.known_addresses(executor) {
-            if is_precompile_for_spec(address, executor.spec_id) {
+            if is_precompile_for_spec(address, executor.spec_id)
+                || address == CHEATCODE_ADDRESS
+                || address == SYMBOLIC_VM_COMPAT_ADDRESS
+            {
                 continue;
             }
             if !self.extcode(cx, executor, address)?.is_empty() {
@@ -2551,7 +2552,8 @@ impl SymbolicWorld {
     /// Returns the concrete accounts a symbolic address may alias, in address order.
     ///
     /// Includes accounts that exist only in the backend, such as contracts deployed in `setUp`,
-    /// which the world caches only once touched. Cheatcode addresses are excluded.
+    /// which the world caches only once touched, and the cheatcode addresses, which have code
+    /// and can hold balances.
     fn known_addresses(&self, executor: &ExecutorView<'_>) -> Vec<Address> {
         let mut addresses = self
             .code_cache
@@ -2560,9 +2562,7 @@ impl SymbolicWorld {
             .chain(&self.existing_accounts)
             .chain(&executor.account_addresses)
             .copied()
-            .filter(|address| {
-                *address != CHEATCODE_ADDRESS && *address != SYMBOLIC_VM_COMPAT_ADDRESS
-            })
+            .chain([CHEATCODE_ADDRESS, SYMBOLIC_VM_COMPAT_ADDRESS])
             .collect::<Vec<_>>();
         addresses.sort_unstable();
         addresses.dedup();

crates/forge/tests/cli/test_cmd/symbolic_cheatcodes.rs

@@ -292,10 +292,11 @@ import "forge-std/Test.sol";
 contract SymbolicExtcodeSize is Test {
     function checkSymbolicCodeLength(address who) public {
         address coded = address(0xC0DE);
-        vm.assume(who == coded || who == address(0xDEAD));
+        vm.assume(who == coded || who == address(0xDEAD) || who == address(vm));
         vm.etch(coded, hex"60006000");
 
-        uint256 expected = who == coded ? 4 : 0;
+        // Forge gives the cheatcode address the one-byte code 0x00.
+        uint256 expected = who == coded ? 4 : who == address(vm) ? 1 : 0;
         assertEq(who.code.length, expected);
     }
 }
@@ -339,10 +340,12 @@ import "forge-std/Test.sol";
 contract SymbolicExtcodeHash is Test {
     function checkSymbolicCodeHash(address who) public {
         address coded = address(0xC0DE);
-        vm.assume(who == coded || who == address(0xDEAD));
+        vm.assume(who == coded || who == address(0xDEAD) || who == address(vm));
         vm.etch(coded, hex"60006000");
 
-        bytes32 expected = who == coded ? keccak256(hex"60006000") : bytes32(0);
+        bytes32 expected = who == coded
+            ? keccak256(hex"60006000")
+            : who == address(vm) ? keccak256(hex"00") : bytes32(0);
         assertEq(who.codehash, expected);
     }
 }
@@ -438,13 +441,21 @@ contract Pinger {
     function ping() external {}
 }
 
+contract RevertingPinger {
+    function ping() external pure {
+        revert("ping");
+    }
+}
+
 contract SymbolicSetupAccounts is Test {
     Pinger a;
     Pinger b;
+    RevertingPinger reverter;
 
     function setUp() public {
         a = new Pinger();
         b = new Pinger();
+        reverter = new RevertingPinger();
         vm.deal(address(a), 1 ether);
         vm.deal(address(b), 1 ether);
     }
@@ -487,10 +498,26 @@ contract SymbolicSetupAccounts is Test {
         assert(false);
     }
 
+    // The first counterexample is the cheatcode address: its unknown-selector error bubbles up.
     function checkUnconstrainedHighLevelCall(address target) public {
         Pinger(target).ping();
         assert(false);
     }
+
+    // Forge fails an unknown-selector call to the cheatcode address with its decoder error.
+    function checkCheatcodeCallRevertData(address target) public {
+        vm.assume(target == address(vm) || target == address(a));
+        (, bytes memory data) = target.call(abi.encodeWithSignature("ping()"));
+        assert(data.length == 0);
+    }
+
+    // A cheatcode call leaves `vm.expectRevert` pending, so the later successful call fails.
+    function checkCheatcodeCallKeepsExpectRevert(address target) public {
+        vm.assume(target == address(vm) || target == address(reverter));
+        vm.expectRevert();
+        target.call(abi.encodeWithSignature("ping()"));
+        a.ping();
+    }
 }
 "#,
     );
@@ -504,15 +531,17 @@ contract SymbolicSetupAccounts is Test {
     .failure()
     .stdout_eq(str![[r#"
 ...
-Ran 7 tests for test/SymbolicSetupAccounts.t.sol:SymbolicSetupAccounts
+Ran 9 tests for test/SymbolicSetupAccounts.t.sol:SymbolicSetupAccounts
 [FAIL: panic: assertion failed (0x01); counterexample: 		[SENDER] [SENDER] [CALLDATA] [ARGS]] checkBalance(address) ([METRICS])
 [FAIL: panic: assertion failed (0x01); counterexample: 		[SENDER] [SENDER] [CALLDATA] [ARGS]] checkCheatcodeBalance(address) ([METRICS])
+[FAIL: next call did not revert as expected; counterexample: 		[SENDER] [SENDER] [CALLDATA] [ARGS]] checkCheatcodeCallKeepsExpectRevert(address) ([METRICS])
+[FAIL: panic: assertion failed (0x01); counterexample: 		[SENDER] [SENDER] [CALLDATA] [ARGS]] checkCheatcodeCallRevertData(address) ([METRICS])
 [FAIL: panic: assertion failed (0x01); counterexample: 		[SENDER] [SENDER] [CALLDATA] [ARGS]] checkCodeCopy(address) ([METRICS])
 [FAIL: panic: assertion failed (0x01); counterexample: 		[SENDER] [SENDER] [CALLDATA] [ARGS]] checkCodeHash(address) ([METRICS])
 [FAIL: panic: assertion failed (0x01); counterexample: 		[SENDER] [SENDER] [CALLDATA] [ARGS]] checkCodeLength(address) ([METRICS])
 [FAIL: panic: assertion failed (0x01); counterexample: 		[SENDER] [SENDER] [CALLDATA] [ARGS]] checkHighLevelCall(address,bool) ([METRICS])
-[FAIL: panic: assertion failed (0x01); counterexample: 		[SENDER] [SENDER] [CALLDATA] [ARGS]] checkUnconstrainedHighLevelCall(address) ([METRICS])
-Suite result: FAILED. 0 passed; 7 failed; 0 skipped; [ELAPSED]
+[FAIL: unknown cheatcode with selector 0x5c36b186; you may have a mismatch between the `Vm` interface (likely in `forge-std`) and the `forge` version; counterexample: 		[SENDER] [SENDER] [CALLDATA] [ARGS]] checkUnconstrainedHighLevelCall(address) ([METRICS])
+Suite result: FAILED. 0 passed; 9 failed; 0 skipped; [ELAPSED]
 ...
 "#]]);
 }