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(
@@ -824,7 +825,27 @@ impl SymbolicExecutor {
         out_offset: SymExpr,
         out_size: BoundedCopySize,
     ) -> Result<StepOutcome, SymbolicError> {
-        if to == CHEATCODE_ADDRESS || to == SYMBOLIC_VM_COMPAT_ADDRESS {
+        let compatibility_cheatcode = if to == SYMBOLIC_VM_COMPAT_ADDRESS {
+            let (_, max_input_size, _) = in_size.parts(&mut self.cx);
+            if max_input_size < 4 {
+                false
+            } else if let Some(offset) = in_offset.as_const() {
+                let offset = usize::try_from(offset).map_err(|_| {
+                    SymbolicError::Unsupported("symbolic compatibility CALL input offset")
+                })?;
+                let selector = state.memory.read_concrete(&mut self.cx, offset, 4)?;
+                let selector: [u8; 4] = selector
+                    .try_into()
+                    .map_err(|_| SymbolicError::Unsupported("symbolic compatibility selector"))?;
+                SymbolicVmCheatcode::from_selector(selector).is_some()
+            } else {
+                // The existing symbolic-offset path checks whether the selector is pinned.
+                true
+            }
+        } else {
+            false
+        };
+        if to == CHEATCODE_ADDRESS || compatibility_cheatcode {
             if !state.constrained_word(&mut self.cx, &value).is_some_and(|value| value.is_zero()) {
                 return Err(SymbolicError::Unsupported("value-bearing cheatcode CALL"));
             }
@@ -1559,14 +1580,10 @@ impl SymbolicExecutor {
         out_size: BoundedCopySize,
     ) -> Result<StepOutcome, SymbolicError> {
         let mut candidates = state.world.symbolic_call_targets(&mut self.cx, executor)?;
+        candidates.push(SYMBOLIC_VM_COMPAT_ADDRESS);
         candidates.extend(active_precompiles(executor.spec_id).as_map().addresses());
         candidates.sort();
         candidates.dedup();
-        if candidates.is_empty() {
-            return Err(SymbolicError::Unsupported(
-                "symbolic CALL target has no known contract candidates",
-            ));
-        }
 
         let candidate_constraints = candidates
             .iter()
@@ -1575,9 +1592,17 @@ impl SymbolicExecutor {
                 SymBoolExpr::eq(&mut self.cx, target.clone(), address)
             })
             .collect::<Vec<_>>();
+        // Only the real cheatcode address uses Forge's decoder. The compatibility address is an
+        // ordinary call target unless its selector names a symbolic-VM operation.
+        let cheatcode_address = SymExpr::constant(&mut self.cx, address_word(CHEATCODE_ADDRESS));
+        let cheatcode_condition = SymBoolExpr::eq(&mut self.cx, target.clone(), cheatcode_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_condition])
+                .cloned()
+                .map(|condition| condition.not(&mut self.cx)),
         );
         let outside_sat = self.is_sat_with_state(state, &outside_constraints)?;
 
@@ -1674,6 +1699,37 @@ impl SymbolicExecutor {
         }
 
         let call_input = in_size.read_from_memory(&mut self.cx, &state.memory, in_offset.clone());
+        let mut cheatcode_branch = state.clone();
+        cheatcode_branch.constraints.push(cheatcode_condition);
+        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_calls.rs

@@ -1055,6 +1055,58 @@ Suite result: FAILED. 0 passed; 1 failed; 0 skipped; [ELAPSED]
 "#]]);
 }
 
+#[forgetest_init]
+fn symbolic_compatibility_address_is_not_forge_cheatcode(prj: _, cmd: _) {
+    skip_unless_z3!("symbolic_compatibility_address_is_not_forge_cheatcode");
+
+    prj.add_test(
+        "SymbolicCompatibilityTarget.t.sol",
+        r#"
+import "forge-std/Test.sol";
+
+contract RevertingTarget {
+    fallback() external { revert(); }
+}
+
+contract SymbolicCompatibilityTarget is Test {
+    address constant COMPAT = 0xF3993A62377BCd56AE39D773740A5390411E8BC9;
+    RevertingTarget reverter;
+
+    function setUp() public { reverter = new RevertingTarget(); }
+
+    function testCompatibilityCallSucceeds() public {
+        (bool ok,) = COMPAT.call(abi.encodeWithSignature("ping()"));
+        assertTrue(ok);
+    }
+
+    /// forge-config: default.symbolic.symbolic_call_targets = true
+    function checkCompatibilityAlias(address target) public {
+        vm.assume(target == COMPAT || target == address(reverter));
+        (bool ok,) = target.call(abi.encodeWithSignature("ping()"));
+        assertFalse(ok);
+    }
+}
+"#,
+    );
+
+    cmd.args(["test", "--match-test", "testCompatibilityCallSucceeds"]).assert_success().stdout_eq(
+        str![[r#"
+...
+[PASS] testCompatibilityCallSucceeds() ([..])
+...
+"#]],
+    );
+    assert_symbolic(cmd.forge_fuse().args(["test", "--symbolic", "--match-test", "checkCompatibilityAlias"]))
+        .failure()
+        .stdout_eq(str![[r#"
+...
+Ran 1 test for test/SymbolicCompatibilityTarget.t.sol:SymbolicCompatibilityTarget
+[FAIL: assertion failed; counterexample: [..]args=[0xF3993A62377BCd56AE39D773740A5390411E8BC9]] checkCompatibilityAlias(address) ([METRICS])
+Suite result: FAILED. 0 passed; 1 failed; 0 skipped; [ELAPSED]
+...
+"#]]);
+}
+
 #[forgetest_init]
 fn symbolic_external_call_with_empty_unknown_target_is_modeled(prj: _, cmd: _) {
     if !z3_available() {