From d1402277ada6e996b43a505cf7eaf06a29a6a551 Mon Sep 17 00:00:00 2001 From: Gustavo Figueiredo Date: Thu, 28 May 2026 09:37:06 +0100 Subject: [PATCH] feat(symbolic): support symbolic vm.deal values Co-authored-by: Amp Amp-Thread-ID: https://ampcode.com/threads/T-019e645e-97a2-757f-adc7-2c765700d18d --- .../evm/symbolic/src/executor/cheatcodes.rs | 9 +- crates/evm/symbolic/src/runtime/state.rs | 5 - .../tests/cli/test_cmd/symbolic_cheatcodes.rs | 103 ++++++++++++++++++ 3 files changed, 109 insertions(+), 8 deletions(-) diff --git a/crates/evm/symbolic/src/executor/cheatcodes.rs b/crates/evm/symbolic/src/executor/cheatcodes.rs index 4fd3e92cc4aa9..c5577695b0b1a 100644 --- a/crates/evm/symbolic/src/executor/cheatcodes.rs +++ b/crates/evm/symbolic/src/executor/cheatcodes.rs @@ -1237,9 +1237,12 @@ impl SymbolicExecutor { } if selector == selector!("deal(address,uint256)") { let target = read_abi_address_or_symbolic_slot_arg(state, args_offset, 0)?; - let value = - read_abi_constrained_word_arg(state, args_offset, 1, "symbolic vm.deal value")?; - state.world.set_balance(target, value); + let value = read_abi_word_arg(&state.memory, args_offset, 1)?; + if value.contains_gasleft() { + return Err(SymbolicError::Unsupported("GAS/gasleft() not modeled")); + } + let value = state.constrained_word(&value).map(SymWord::Concrete).unwrap_or(value); + state.world.set_balance_word(target, value); return Ok(CheatcodeOutcome::Continue(Vec::new())); } if selector == selector!("setNonce(address,uint64)") diff --git a/crates/evm/symbolic/src/runtime/state.rs b/crates/evm/symbolic/src/runtime/state.rs index 894001f37841a..174b39162ef6b 100644 --- a/crates/evm/symbolic/src/runtime/state.rs +++ b/crates/evm/symbolic/src/runtime/state.rs @@ -1238,11 +1238,6 @@ impl SymbolicWorld { Ok(SymWord::Expr(result)) } - /// Applies the `set_balance` symbolic state helper. - pub(crate) fn set_balance(&mut self, address: Address, value: U256) { - self.set_balance_word(address, SymWord::Concrete(value)); - } - /// Applies the `set_balance_word` symbolic state helper. pub(crate) fn set_balance_word(&mut self, address: Address, value: SymWord) { self.balances.insert(address, value.clone()); diff --git a/crates/forge/tests/cli/test_cmd/symbolic_cheatcodes.rs b/crates/forge/tests/cli/test_cmd/symbolic_cheatcodes.rs index 6f823c5c1946f..f116ebc5b1458 100644 --- a/crates/forge/tests/cli/test_cmd/symbolic_cheatcodes.rs +++ b/crates/forge/tests/cli/test_cmd/symbolic_cheatcodes.rs @@ -3,6 +3,7 @@ use foundry_common::sh_eprintln; use foundry_test_utils::{forgetest_init, util::OutputExt}; use super::symbolic_helpers::z3_available; +use crate::skip_unless_z3; forgetest_init!(symbolic_cheatcodes_accept_symbolic_address_targets, |prj, cmd| { if !z3_available() { @@ -1676,6 +1677,32 @@ contract SymbolicConstrainedCheatcodes is Test { assertEq(address(0xbeef).balance, 7); } + function checkSymbolicDealValueFundsCall(uint256 amount) public { + address recipient = address(0xbeef); + + vm.deal(address(this), amount); + assertEq(address(this).balance, amount); + + (bool ok,) = recipient.call{value: amount}(""); + + assertTrue(ok); + assertEq(recipient.balance, amount); + assertEq(address(this).balance, 0); + } + + function checkSymbolicDealInsufficientFunds(uint256 amount) public { + vm.assume(amount < type(uint256).max); + address recipient = address(0xbeef); + + vm.deal(address(this), amount); + + (bool ok,) = recipient.call{value: amount + 1}(""); + + assertFalse(ok); + assertEq(address(this).balance, amount); + assertEq(recipient.balance, 0); + } + function checkConstrainedRandomBytes(uint16 len) public { vm.assume(len == 3); @@ -1697,6 +1724,18 @@ contract SymbolicConstrainedCheatcodes is Test { &stdout, foundry_test_utils::str![[r#" [PASS] checkConstrainedDeal(address,uint256) +"#]], + ); + assert_relevant_lines( + &stdout, + foundry_test_utils::str![[r#" +[PASS] checkSymbolicDealValueFundsCall(uint256) +"#]], + ); + assert_relevant_lines( + &stdout, + foundry_test_utils::str![[r#" +[PASS] checkSymbolicDealInsufficientFunds(uint256) "#]], ); assert_relevant_lines( @@ -1710,6 +1749,70 @@ contract SymbolicConstrainedCheatcodes is Test { assert!(!stdout.contains("symbolic randomBytes len"), "{stdout}"); }); +forgetest_init!(symbolic_cheatcodes_reject_gas_deal_value, |prj, cmd| { + skip_unless_z3!("symbolic_cheatcodes_reject_gas_deal_value"); + + prj.add_test( + "SymbolicDealGasValue.t.sol", + r#" +import "forge-std/Test.sol"; + +contract SymbolicDealGasValue is Test { + function checkGasDealValue() public { + vm.deal(address(this), gasleft()); + } + + function checkDerivedGasDealValue() public { + vm.deal(address(this), gasleft() + 1); + } +} +"#, + ); + + let stdout = cmd + .args(["test", "--symbolic", "--match-test", "checkGasDealValue"]) + .assert_failure() + .get_output() + .stdout_lossy(); + + assert_relevant_lines( + &stdout, + foundry_test_utils::str![[r#" +incomplete symbolic execution (Stuck): unsupported symbolic execution feature: GAS/gasleft() not modeled +"#]], + ); +}); + +forgetest_init!(symbolic_cheatcodes_reject_derived_gas_deal_value, |prj, cmd| { + skip_unless_z3!("symbolic_cheatcodes_reject_derived_gas_deal_value"); + + prj.add_test( + "SymbolicDerivedDealGasValue.t.sol", + r#" +import "forge-std/Test.sol"; + +contract SymbolicDerivedDealGasValue is Test { + function checkDerivedGasDealValue() public { + vm.deal(address(this), gasleft() + 1); + } +} +"#, + ); + + let stdout = cmd + .args(["test", "--symbolic", "--match-test", "checkDerivedGasDealValue"]) + .assert_failure() + .get_output() + .stdout_lossy(); + + assert_relevant_lines( + &stdout, + foundry_test_utils::str![[r#" +incomplete symbolic execution (Stuck): unsupported symbolic execution feature: GAS/gasleft() not modeled +"#]], + ); +}); + forgetest_init!(symbolic_cheatcodes_accept_bounded_symbolic_input_size, |prj, cmd| { if !z3_available() { let _ = sh_eprintln!(