Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
figtracer wants to merge 4 commits into
base: mablr/evm2-migration
Choose a base branch
from
+195 −35
Open

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

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
925ef66
fix(symbolic): include the cheatcode address in EXTCODE* candidates
figtracer Nov 9, 2026
56106c7
fix(symbolic): revert symbolic calls that alias the cheatcode address
figtracer Nov 9, 2026
40506a5
fix(symbolic): use Forge's decoder error for cheatcode-alias calls
figtracer Nov 10, 2026
c4f9c74
fix(symbolic): model compatibility calls
figtracer Nov 10, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
46 changes: 45 additions & 1 deletion crates/evm/symbolic/src/executor/calls.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
use super::*;
use foundry_cheatcodes_spec::Vm::VmCalls;

impl SymbolicExecutor {
pub(super) fn call(
Expand Down Expand Up @@ -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 reverts a call to them with an unknown selector.
let cheatcode_constraints =
[CHEATCODE_ADDRESS, SYMBOLIC_VM_COMPAT_ADDRESS].map(|address| {

@mattsse mattsse Nov 10, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Separate compatibility aliases from Forge cheatcode decoding

SYMBOLIC_VM_COMPAT_ADDRESS is not intercepted by the concrete Forge cheatcode inspector: in an ordinary unforked test it has no code, so a low-level ping() call succeeds. Grouping it with CHEATCODE_ADDRESS sends it through decode_cheatcode_call and forces a revert instead. For example, constrain target to the compatibility address or a deployed contract with a reverting fallback, call target.call(abi.encodeWithSignature("ping()")), and assert !success: both branches now revert symbolically, while the compatibility-address input concretely succeeds and violates the assertion. The existing engine with --symbolic-call-targets finds and replays exactly that counterexample. Please split the compatibility-address handling and report incomplete if its semantics cannot be modeled, rather than fabricating a Forge decoder revert.

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)?;

Expand Down Expand Up @@ -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();

@stevencartavia stevencartavia Nov 10, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The cheatcode branch doesn't check the call kind. Forge only intercepts when destination == CHEATCODE_ADDRESS, so DELEGATECALL and CALLCODE to address(vm) run its 0x00 code and succeed. Modelling them as a decoder revert makes assert(!ok) falsely pass. With --symbolic-call-targets, base reported a correct counterexample here. Build this branch only for Call/StaticCall.

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)? {
let selector = call_input
.slice_concrete(&mut self.cx, 0, 4)
.concrete_bytes(&mut self.cx, "symbolic cheatcode selector")?;
if let Ok(selector) = <[u8; 4]>::try_from(selector)
&& VmCalls::signature_by_selector(selector).is_some()
{
return Err(SymbolicError::Unsupported("symbolic cheatcode CALL target"));
}
let return_data = SymReturnData::empty(&mut self.cx);

@mattsse mattsse Nov 10, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Preserve the unknown-selector revert payload

Concrete Forge returns ABI-encoded CheatcodeError(...) for an unknown selector (apply_cheatcode constructs the error and the inspector ABI-encodes it), rather than empty bytes. For example, constrain target to address(vm) or a deployed Pinger, perform target.call(abi.encodeWithSignature("ping()")), and assert that the returned bytes have length zero. The normal Pinger.ping() returns no bytes, and this new branch also supplies no bytes, so the symbolic model can prove that assertion even though the concrete VM case fails it. Please preserve the concrete error payload, or report incomplete for this case until it is modeled.

match self.finish_codeless_call(

@mattsse mattsse Nov 10, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Keep revert expectations pending across cheatcode calls

finish_codeless_call consumes a pending ordinary vm.expectRevert, but concrete Forge explicitly skips cheatcode calls in ExpectedRevert::needs_processing. Consider vm.expectRevert(); target.call(abi.encodeWithSignature("ping()")); pinger.ping();, with target constrained to the VM address or a contract whose fallback reverts. This branch treats the VM's unknown-selector revert as satisfying the expectation, so the subsequent successful ping() passes. Concrete Forge leaves the expectation pending and fails that subsequent call with next call did not revert as expected. Please retain the cheatcode-specific handling here; the same helper also incorrectly consumes pending assumeNoRevert state for this branch.

executor,
&mut cheatcode_branch,
kind,
CallStatus::Revert,
return_data,
CHEATCODE_ADDRESS,
out_offset.clone(),
&out_size,
)? {
StepOutcome::Continue => parents.push_back(cheatcode_branch),
StepOutcome::AssumeRejected => {}
outcome => {
*state = cheatcode_branch;
return Ok(outcome);
}
}
}

for (to, constraint) in candidates.into_iter().zip(candidate_constraints) {
let mut branch = state.clone();
branch.constraints.push(constraint);
Expand Down
16 changes: 8 additions & 8 deletions crates/evm/symbolic/src/runtime/state.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down Expand Up @@ -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() {
Expand All @@ -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
Expand All @@ -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])

@mattsse mattsse Nov 9, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Update the high-level CALL regression for the new candidates

Including these addresses makes Solidity's EXTCODESIZE guard admit cheatcode targets, but symbolic_call_targets still excludes them. With the default symbolic_call_targets = false, checkUnconstrainedHighLevelCall(address) therefore returns incomplete symbolic execution (Stuck): unsupported symbolic execution feature: symbolic CALL target instead of the replayed assertion failure still expected by symbolic_account_queries_see_setup_accounts. This snapshot fails on all three attempts in test / test all. Please reconcile the CALL handling or update that regression's expectation in this PR so the required suite passes.

.collect::<Vec<_>>();
addresses.sort_unstable();
addresses.dedup();
Expand Down
11 changes: 7 additions & 4 deletions crates/forge/tests/cli/test_cmd/symbolic_cheatcodes.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
}
Expand Down Expand Up @@ -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);
}
}
Expand Down
Loading