feat(symbolic): support symbolic vm.deal values

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

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

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