From d992ea3ec20bc015d51946a3172d0793419e8803 Mon Sep 17 00:00:00 2001 From: Dickson Date: Tue, 1 Sep 2026 01:55:39 +0000 Subject: [PATCH] fix invariant msg.value balance accounting --- src/halmos/__main__.py | 23 +- src/halmos/sevm.py | 41 ++- tests/expected/all.json | 22 +- tests/regression/test/InvariantMsgValue.t.sol | 54 ++++ tests/test_cli.py | 10 +- tests/test_sevm.py | 262 ++++++++++++++++++ 6 files changed, 401 insertions(+), 11 deletions(-) create mode 100644 tests/regression/test/InvariantMsgValue.t.sol diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py index d768243d2..605a95ddf 100644 --- a/src/halmos/__main__.py +++ b/src/halmos/__main__.py @@ -567,11 +567,8 @@ def run_target_contract( else None ) - # create a symbolic msg.value - msg_value = BitVec( - f"halmos_msg_value_{id_str(addr)}_{uid()}_{ex.new_symbol_id():>02}", - BitVecSort256, - ) + state_mutability = abi[fun_sig]["stateMutability"] + msg_value = mk_invariant_msg_value(ex, addr, state_mutability) yield from run_target_function( args, @@ -592,6 +589,22 @@ def run_target_contract( continue +def mk_invariant_msg_value( + ex: Exec, addr: Address, state_mutability: str +) -> Word: + """Return the call value modeled for an invariant target transaction.""" + # Solidity dispatchers reject value before entering nonpayable functions. + # Model that value as zero up front so rejected calls do not create spurious + # balance histories in the invariant frontier. + if state_mutability != "payable": + return ZERO + + return BitVec( + f"halmos_msg_value_{id_str(addr)}_{uid()}_{ex.new_symbol_id():>02}", + BitVecSort256, + ) + + def _compute_frontier(ctx: ContractContext, depth: int) -> Iterator[Exec]: """ Computes the frontier states at a given depth. diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py index 3d2ead175..99722db47 100644 --- a/src/halmos/sevm.py +++ b/src/halmos/sevm.py @@ -2310,22 +2310,29 @@ def transfer_value( if value.is_concrete and value.value == 0: return + caller = uint160(caller).as_z3() + to = uint160(to).as_z3() caller_balance: BitVecRef = ex.balance_of(caller) # assume balance is enough; otherwise ignore this path # note: evm requires enough balance even for self-transfer balance_cond = simplify(UGE(caller_balance, value.as_z3())) - if is_false(balance_cond): + if is_false(balance_cond) or ex.check(balance_cond) == unsat: raise InfeasiblePath("transfer_value: balance is not enough") ex.path.append(balance_cond) + # A self-transfer still requires sufficient funds, but has no net state + # change. Check both structural equality and equality established by + # the current path before creating balance-array identities. + if eq(caller, to) or ex.check(caller != to) == unsat: + return + # conditional transfer if condition is not None: value = If(condition, value, Z3_ZERO) ex.balance_update(caller, BV(caller_balance).sub(value)) - # NOTE: ex.balance_of(to) must be called **after** updating the caller's balance above, to correctly handle the self-transfer case ex.balance_update(to, BV(ex.balance_of(to)).add(value)) def call( @@ -3009,11 +3016,14 @@ def run_message(self, pre_ex: Exec, message: Message, path: Path) -> Iterator[Ex Executes the given transaction from the given input state. Note: As this involves executing a new transaction, the transient storage is reset to empty instead of being inherited from the input state. + Failed top-level calls yield an error state with persistent network state + restored to the input transaction state. Transient storage remains at its + fresh transaction-start state. """ ex0 = Exec( code=pre_ex.code.copy(), # shallow copy storage=deepcopy(pre_ex.storage), - transient_storage=self.fresh_transient_storage(pre_ex), # empty + transient_storage=self.fresh_transient_storage(pre_ex), balance=pre_ex.balance, # block=deepcopy(pre_ex.block), @@ -3035,7 +3045,30 @@ def run_message(self, pre_ex: Exec, message: Message, path: Path) -> Iterator[Ex storages=pre_ex.storages.copy(), balances=pre_ex.balances.copy(), ) - yield from self.run(ex0) + + # Apply the top-level CALL value transfer to the copied transaction state. + # An underfunded transaction is invalid and therefore has no output state. + if message.call_scheme == OP_CALL: + try: + self.transfer_value( + ex0, + message.caller, + message.target, + uint256(message.value), + ) + except InfeasiblePath: + return + + for post_ex in self.run(ex0): + if isinstance(post_ex.context.output.error, EvmException): + post_ex.code = pre_ex.code.copy() + post_ex.storage = deepcopy(pre_ex.storage) + post_ex.transient_storage = self.fresh_transient_storage(pre_ex) + post_ex.balance = pre_ex.balance + post_ex.storages = pre_ex.storages.copy() + post_ex.balances = pre_ex.balances.copy() + + yield post_ex def run(self, ex0: Exec) -> Iterator[Exec]: next_ex: Exec | None = ex0 diff --git a/tests/expected/all.json b/tests/expected/all.json index b9cb7594a..72881baf9 100644 --- a/tests/expected/all.json +++ b/tests/expected/all.json @@ -2329,6 +2329,26 @@ "num_bounded_loops": null } ], + "test/InvariantMsgValue.t.sol:InvariantMsgValueTest": [ + { + "name": "invariant_msg_value_can_be_positive()", + "exitcode": 1, + "num_models": 1, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "invariant_msg_value_transfer()", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], "test/InvariantProbes.t.sol:InvariantProbesTest": [ { "name": "invariant_probes_found()", @@ -6734,4 +6754,4 @@ } ] } -} \ No newline at end of file +} diff --git a/tests/regression/test/InvariantMsgValue.t.sol b/tests/regression/test/InvariantMsgValue.t.sol new file mode 100644 index 000000000..3636481e2 --- /dev/null +++ b/tests/regression/test/InvariantMsgValue.t.sol @@ -0,0 +1,54 @@ +// SPDX-License-Identifier: AGPL-3.0 +pragma solidity >=0.8.0 <0.9.0; + +import "forge-std/Test.sol"; + +contract InvariantMsgValueTarget { + uint256 public totalMsgValue; + uint256 public nonpayableCalls; + + function deposit() external payable { + totalMsgValue += msg.value; + } + + function touch() external { + nonpayableCalls++; + } +} + +contract InvariantMsgValueTest is Test { + address constant SENDER = address(0xbeef); + uint256 constant SENDER_INITIAL_BALANCE = 2 ether; + uint256 constant TARGET_INITIAL_BALANCE = 1 ether; + + InvariantMsgValueTarget target; + + function setUp() public { + target = new InvariantMsgValueTarget(); + + vm.deal(SENDER, SENDER_INITIAL_BALANCE); + vm.deal(address(target), TARGET_INITIAL_BALANCE); + + targetContract(address(target)); + targetSender(SENDER); + } + + /// @custom:halmos --invariant-depth 1 + function invariant_msg_value_transfer() public view { + // At depth one, this is the msg.value observed by the target call. + uint256 totalMsgValue = target.totalMsgValue(); + + assertLe(totalMsgValue, SENDER_INITIAL_BALANCE); + assertEq(SENDER.balance + totalMsgValue, SENDER_INITIAL_BALANCE); + assertEq( + address(target).balance, + TARGET_INITIAL_BALANCE + totalMsgValue + ); + } + + /// @custom:halmos --invariant-depth 1 + function invariant_msg_value_can_be_positive() public view { + // Expected counterexample: deposit receives a positive, funded msg.value. + assertEq(target.totalMsgValue(), 0); + } +} diff --git a/tests/test_cli.py b/tests/test_cli.py index edde7ecdd..7c12fec1b 100644 --- a/tests/test_cli.py +++ b/tests/test_cli.py @@ -8,12 +8,20 @@ eq, ) -from halmos.bitvec import HalmosBitVec as BV +from halmos.__main__ import mk_invariant_msg_value +from halmos.bitvec import ZERO, HalmosBitVec as BV from halmos.calldata import str_abi from halmos.sevm import Contract, Instruction from halmos.utils import EVM, hexify +@pytest.mark.parametrize("state_mutability", ["nonpayable", "view", "pure"]) +def test_nonpayable_invariant_target_has_zero_msg_value(state_mutability): + # Neither address formatting nor symbol allocation should be reached for a + # target that the ABI says cannot accept value. + assert mk_invariant_msg_value(None, None, state_mutability) is ZERO + + @pytest.fixture def setup_abi(): return json.loads( diff --git a/tests/test_sevm.py b/tests/test_sevm.py index ef05c2af0..e72bae04c 100644 --- a/tests/test_sevm.py +++ b/tests/test_sevm.py @@ -10,16 +10,20 @@ LShR, Select, SignExt, + Store, + UGE, ZeroExt, ) from halmos.__main__ import mk_block from halmos.bitvec import HalmosBitVec as BV from halmos.bytevec import ByteVec +from halmos.config import ConfigSource from halmos.exceptions import ( InvalidJumpDestError, InvalidOpcode, OutOfGasError, + Revert, StackUnderflowError, ) from halmos.sevm import ( @@ -82,6 +86,264 @@ def mk_ex(hexcode, sevm, solver, storage, caller, this): ) +RUN_MESSAGE_CALLER = BitVecVal(0xCA11E2, 160) +RUN_MESSAGE_TARGET = BitVecVal(0x7A26E7, 160) + + +def mk_run_message_ex( + sevm, + solver, + *, + caller_balance, + target_balance, + value, + caller=RUN_MESSAGE_CALLER, + target=RUN_MESSAGE_TARGET, + hexcode="00", +): + bytecode = Contract.from_hexcode(hexcode) + caller = uint160(caller).as_z3() + target = uint160(target).as_z3() + initial_balance = Store(balance, caller, uint256(caller_balance).as_z3()) + if not caller.eq(target): + initial_balance = Store( + initial_balance, target, uint256(target_balance).as_z3() + ) + + message = Message( + target=target, + caller=caller, + origin=caller, + value=uint256(value).as_z3(), + data=ByteVec(), + call_scheme=EVM.CALL, + ) + pre_ex = sevm.mk_exec( + code={target: bytecode}, + storage={target: sevm.mk_storagedata()}, + transient_storage={target: sevm.mk_storagedata()}, + balance=initial_balance, + block=mk_block(), + context=CallContext(message), + pgm=bytecode, + path=Path(solver), + ) + path = Path(solver) + path.extend_path(pre_ex.path) + return pre_ex, message, path + + +def concrete_balance(ex, address): + value = BV(ex.balance_of(address)) + assert value.is_concrete + return value.value + + +def test_run_message_transfers_positive_value(sevm, solver): + pre_ex, message, path = mk_run_message_ex( + sevm, + solver, + caller_balance=10, + target_balance=4, + value=3, + ) + + post_exs = list(sevm.run_message(pre_ex, message, path)) + + assert len(post_exs) == 1 + post_ex = post_exs[0] + assert post_ex.context.output.error is None + assert concrete_balance(post_ex, RUN_MESSAGE_CALLER) == 7 + assert concrete_balance(post_ex, RUN_MESSAGE_TARGET) == 7 + + +def test_run_message_zero_value_reuses_balance_state(sevm, solver): + pre_ex, message, path = mk_run_message_ex( + sevm, + solver, + caller_balance=10, + target_balance=4, + value=0, + ) + + post_exs = list(sevm.run_message(pre_ex, message, path)) + + assert len(post_exs) == 1 + post_ex = post_exs[0] + assert post_ex.balance is pre_ex.balance + assert post_ex.balances == pre_ex.balances == {} + assert concrete_balance(post_ex, RUN_MESSAGE_CALLER) == 10 + assert concrete_balance(post_ex, RUN_MESSAGE_TARGET) == 4 + + +def test_run_message_rejects_definitely_insufficient_value_without_mutating_pre_ex( + sevm, solver +): + pre_ex, message, path = mk_run_message_ex( + sevm, + solver, + caller_balance=2, + target_balance=4, + value=3, + ) + pre_balance = pre_ex.balance + pre_balances = pre_ex.balances.copy() + pre_conditions = pre_ex.path.conditions.copy() + + post_exs = list(sevm.run_message(pre_ex, message, path)) + + assert post_exs == [] + assert pre_ex.balance is pre_balance + assert pre_ex.balances == pre_balances + assert pre_ex.path.conditions == pre_conditions + assert pre_ex.context.output.data is None + + +def test_run_message_rejects_solver_proven_insufficient_value(sevm, solver): + symbolic_value = BitVec("run_message_value", 256) + pre_ex, message, path = mk_run_message_ex( + sevm, + solver, + caller_balance=2, + target_balance=4, + value=symbolic_value, + ) + # This implies insufficient funds without being the syntactic negation of + # the funding condition, forcing the solver-backed feasibility check. + path.append(UGE(symbolic_value, con(3))) + + post_exs = list(sevm.run_message(pre_ex, message, path)) + + assert post_exs == [] + + +@pytest.mark.parametrize( + "caller_balance,value,expected_outputs", + [(5, 5, 1), (4, 5, 0)], +) +def test_run_message_self_transfer_preserves_balance_but_requires_funds( + sevm, solver, caller_balance, value, expected_outputs +): + pre_ex, message, path = mk_run_message_ex( + sevm, + solver, + caller_balance=caller_balance, + target_balance=caller_balance, + value=value, + target=RUN_MESSAGE_CALLER, + ) + + post_exs = list(sevm.run_message(pre_ex, message, path)) + + assert len(post_exs) == expected_outputs + if post_exs: + post_ex = post_exs[0] + assert post_ex.balance is pre_ex.balance + assert concrete_balance(post_ex, RUN_MESSAGE_CALLER) == caller_balance + + +def test_run_message_path_equal_self_transfer_reuses_balance_state(sevm, solver): + symbolic_caller = BitVec("run_message_caller", 160) + pre_ex, message, path = mk_run_message_ex( + sevm, + solver, + caller_balance=5, + target_balance=5, + value=3, + caller=symbolic_caller, + ) + path.append(symbolic_caller == RUN_MESSAGE_TARGET) + + [post_ex] = list(sevm.run_message(pre_ex, message, path)) + + assert post_ex.balance is pre_ex.balance + assert concrete_balance(post_ex, RUN_MESSAGE_TARGET) == 5 + + +def test_run_message_success_does_not_mutate_pre_ex_balance_history(sevm, solver): + pre_ex, message, path = mk_run_message_ex( + sevm, + solver, + caller_balance=9, + target_balance=1, + value=2, + ) + pre_balance = pre_ex.balance + pre_balances = pre_ex.balances.copy() + pre_conditions = pre_ex.path.conditions.copy() + + [post_ex] = list(sevm.run_message(pre_ex, message, path)) + + assert concrete_balance(post_ex, RUN_MESSAGE_CALLER) == 7 + assert concrete_balance(post_ex, RUN_MESSAGE_TARGET) == 3 + assert pre_ex.balance is pre_balance + assert pre_ex.balances == pre_balances + assert pre_ex.path.conditions == pre_conditions + assert pre_ex.context.output.data is None + + +def test_run_message_marks_reverted_top_level_call(sevm, solver): + pre_ex, message, path = mk_run_message_ex( + sevm, + solver, + caller_balance=9, + target_balance=1, + value=2, + hexcode="60006000fd", + ) + + [post_ex] = list(sevm.run_message(pre_ex, message, path)) + + assert isinstance(post_ex.context.output.error, Revert) + assert not post_ex.context.output.data + assert post_ex.balance is pre_ex.balance + assert concrete_balance(post_ex, RUN_MESSAGE_CALLER) == 9 + assert concrete_balance(post_ex, RUN_MESSAGE_TARGET) == 1 + + +def test_run_message_exceptional_halt_restores_transaction_state( + args, fun_info, solver +): + generic_args = args.with_overrides( + ConfigSource.function_annotation, storage_layout="generic" + ) + sevm = SEVM(generic_args, fun_info) + + # TSTORE(0, 1); SSTORE(0, 1); INVALID -- the exceptional halt must roll + # back the storage writes and the top-level value transfer. + pre_ex, message, path = mk_run_message_ex( + sevm, + solver, + caller_balance=9, + target_balance=1, + value=2, + hexcode="600160005d6001600055fe", + ) + prior_transient_storage = pre_ex.transient_storage[RUN_MESSAGE_TARGET] + prior_transient_storage[8] = BitVecVal(123, 256) + prior_transient_digest = prior_transient_storage.digest() + empty_transient_digest = sevm.mk_storagedata().digest() + + [post_ex] = list(sevm.run_message(pre_ex, message, path)) + + assert isinstance(post_ex.context.output.error, InvalidOpcode) + assert ( + post_ex.storage[RUN_MESSAGE_TARGET].digest() + == pre_ex.storage[RUN_MESSAGE_TARGET].digest() + ) + assert post_ex.transient_storage[RUN_MESSAGE_TARGET].digest() == ( + empty_transient_digest + ) + assert post_ex.transient_storage[RUN_MESSAGE_TARGET].digest() != ( + prior_transient_digest + ) + assert post_ex.balance is pre_ex.balance + assert post_ex.storages == pre_ex.storages == {} + assert post_ex.balances == pre_ex.balances == {} + assert concrete_balance(post_ex, RUN_MESSAGE_CALLER) == 9 + assert concrete_balance(post_ex, RUN_MESSAGE_TARGET) == 1 + + x = BV("x") y = BV("y") z = BV("z")