From 998b28235b49e2dec771efd5a23467096558499a Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Mon, 26 Aug 2024 14:55:04 -0700 Subject: [PATCH] feat: empty initial network state (#352) --- .github/workflows/test-external.yml | 2 +- .github/workflows/test-long.yml | 2 +- src/halmos/__main__.py | 59 ++++++++++------------------- src/halmos/cheatcodes.py | 11 ++++-- src/halmos/config.py | 10 ----- src/halmos/sevm.py | 18 ++++++--- tests/expected/all.json | 45 ++++++++++++++++++++++ tests/regression/halmos.toml | 15 -------- tests/regression/test/Block.t.sol | 10 +++++ tests/regression/test/Deal.t.sol | 4 ++ tests/regression/test/Foundry.t.sol | 12 ++++++ 11 files changed, 113 insertions(+), 75 deletions(-) diff --git a/.github/workflows/test-external.yml b/.github/workflows/test-external.yml index f9f4a497..597a0918 100644 --- a/.github/workflows/test-external.yml +++ b/.github/workflows/test-external.yml @@ -87,7 +87,7 @@ jobs: run: docker run halmos-image --version - name: Test external repo - run: docker run -v .:/workspace halmos-image ${{ matrix.project.cmd }} --statistics --solver-timeout-assertion 0 --solver-threads 4 --solver-command yices-smt2 ${{ matrix.cache-solver }} ${{ inputs.halmos-options }} + run: docker run -v .:/workspace halmos-image ${{ matrix.project.cmd }} --statistics --solver-timeout-assertion 0 --solver-threads 3 --solver-command yices-smt2 ${{ matrix.cache-solver }} ${{ inputs.halmos-options }} working-directory: ${{ matrix.project.dir }} env: FOUNDRY_PROFILE: ${{ matrix.project.profile }} diff --git a/.github/workflows/test-long.yml b/.github/workflows/test-long.yml index 59455b7a..ccb222ff 100644 --- a/.github/workflows/test-long.yml +++ b/.github/workflows/test-long.yml @@ -48,4 +48,4 @@ jobs: - name: Run pytest run: | - docker run -v .:/workspace --entrypoint pytest halmos-image -x -v tests/test_halmos.py -k ${{ matrix.testname }} --halmos-options='-st --solver-timeout-assertion 0 --solver-threads 4 --solver-command yices-smt2 ${{ matrix.cache-solver }} ${{ inputs.halmos-options }}' -s --log-cli-level= + docker run -v .:/workspace --entrypoint pytest halmos-image -x -v tests/test_halmos.py -k ${{ matrix.testname }} --halmos-options='-st --solver-timeout-assertion 0 --solver-threads 3 --solver-command yices-smt2 ${{ matrix.cache-solver }} ${{ inputs.halmos-options }}' -s --log-cli-level= diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py index 29c49836..6d750a74 100644 --- a/src/halmos/__main__.py +++ b/src/halmos/__main__.py @@ -19,16 +19,13 @@ from z3 import ( Z3_OP_CONCAT, - Array, BitVec, BitVecNumRef, BitVecRef, - BitVecSort, Bool, CheckSatResult, Context, ModelRef, - ZeroExt, is_app, is_bv, sat, @@ -44,8 +41,14 @@ from .exceptions import HalmosException from .mapper import DeployAddressMapper, Mapper from .sevm import ( + EMPTY_BALANCE, EVM, + FOUNDRY_CALLER, + FOUNDRY_ORIGIN, + FOUNDRY_TEST, + ONE, SEVM, + ZERO, Address, Block, CallContext, @@ -58,14 +61,13 @@ Path, SMTQuery, State, - Word, con_addr, jumpid_str, - magic_address, mnemonic, ) from .utils import ( NamedTimer, + address, byte_length, color_error, con, @@ -221,25 +223,17 @@ def mk_calldata( calldata.create(fun_abi, cd) -def mk_callvalue() -> Word: - return BitVec("msg_value", 256) - - -def mk_balance() -> Word: - return Array("balance_0", BitVecSort(160), BitVecSort(256)) - - def mk_block() -> Block: + # foundry default values block = Block( - basefee=ZeroExt(160, BitVec("block_basefee", 96)), # practical limit 96 bit - chainid=ZeroExt(192, BitVec("block_chainid", 64)), # chainid 64 bit - coinbase=mk_addr("block_coinbase"), # address 160 bit - difficulty=BitVec("block_difficulty", 256), - gaslimit=ZeroExt(160, BitVec("block_gaslimit", 96)), # practical limit 96 bit - number=ZeroExt(192, BitVec("block_number", 64)), # practical limit 64 bit - timestamp=ZeroExt(192, BitVec("block_timestamp", 64)), # practical limit 64 bit + basefee=ZERO, + chainid=con(31337), + coinbase=address(0), + difficulty=ZERO, + gaslimit=con(2**63 - 1), + number=ONE, + timestamp=ONE, ) - block.chainid = con(1) # for ethereum return block @@ -247,15 +241,11 @@ def mk_addr(name: str) -> Address: return BitVec(name, 160) -def mk_caller(args: HalmosConfig) -> Address: - return mk_addr("msg_sender") if args.symbolic_msg_sender else magic_address - - def mk_this() -> Address: # NOTE: Do NOT remove the `con_addr()` wrapper. # The return type should be BitVecSort(160) as it is used as a key for ex.code. # The keys of ex.code are compared using structural equality with other BitVecRef addresses. - return con_addr(magic_address + 1) + return con_addr(FOUNDRY_TEST) def mk_solver(args: HalmosConfig, logic="QF_AUFBV", ctx=None, assertion=False): @@ -416,8 +406,8 @@ def deploy_test( this = mk_this() message = Message( target=this, - caller=mk_caller(args), - origin=mk_addr("tx_origin"), + caller=FOUNDRY_CALLER, + origin=FOUNDRY_ORIGIN, value=0, data=ByteVec(), call_scheme=EVM.CREATE, @@ -426,7 +416,7 @@ def deploy_test( ex = sevm.mk_exec( code={this: Contract(b"")}, storage={this: {}}, - balance=mk_balance(), + balance=EMPTY_BALANCE, block=mk_block(), context=CallContext(message=message), pgm=None, # to be added @@ -443,13 +433,6 @@ def deploy_test( creation_bytecode = Contract.from_hexcode(creation_hexcode) ex.pgm = creation_bytecode - # use the given deployed bytecode if --no-test-constructor is enabled - if args.no_test_constructor: - deployed_bytecode = Contract.from_hexcode(deployed_hexcode) - ex.set_code(this, deployed_bytecode) - ex.pgm = deployed_bytecode - return ex - # create test contract exs = list(sevm.run(ex)) @@ -1597,8 +1580,8 @@ def on_signal(signum, frame): contract_path = f"{contract_json['ast']['absolutePath']}:{contract_name}" print(f"\nRunning {num_found} tests for {contract_path}") - # Set 0xaaaa0001 in DeployAddressMapper - DeployAddressMapper().add_deployed_contract("0xaaaa0001", contract_name) + # Set the test contract address in DeployAddressMapper + DeployAddressMapper().add_deployed_contract(hexify(mk_this()), contract_name) # support for `/// @custom:halmos` annotations contract_args = with_natspec(args, contract_name, natspec) diff --git a/src/halmos/cheatcodes.py b/src/halmos/cheatcodes.py index 5785e008..556cbee6 100644 --- a/src/halmos/cheatcodes.py +++ b/src/halmos/cheatcodes.py @@ -409,7 +409,7 @@ class hevm_cheat_code: label_sig: int = 0xC657C718 # bytes4(keccak256("getBlockNumber()")) - get_block_nunber_sig: int = 0x42CBB15C + get_block_number_sig: int = 0x42CBB15C @staticmethod def handle(sevm, ex, arg: ByteVec, stack, step_id) -> ByteVec | None: @@ -581,7 +581,7 @@ def handle(sevm, ex, arg: ByteVec, stack, step_id) -> ByteVec | None: return ret - # ffi(string[]) returns (bytes) + # vm.ffi(string[]) returns (bytes) elif funsig == hevm_cheat_code.ffi_sig: if not sevm.options.ffi: error_msg = "ffi cheatcode is disabled. Run again with `--ffi` if you want to enable it" @@ -615,6 +615,7 @@ def handle(sevm, ex, arg: ByteVec, stack, step_id) -> ByteVec | None: return stringified_bytes_to_bytes(out_str) + # vm.addr(uint256 privateKey) returns (address keyAddr) elif funsig == hevm_cheat_code.addr_sig: private_key = uint256(extract_bytes(arg, 4, 32)) @@ -630,6 +631,7 @@ def handle(sevm, ex, arg: ByteVec, stack, step_id) -> ByteVec | None: ret.append(uint256(addr)) return ret + # vm.sign(uint256 privateKey, bytes32 digest) returns (uint8 v, bytes32 r, bytes32 s) elif funsig == hevm_cheat_code.sign_sig: key = extract_bytes(arg, 4, 32) digest = extract_bytes(arg, 4 + 32, 32) @@ -679,6 +681,7 @@ def handle(sevm, ex, arg: ByteVec, stack, step_id) -> ByteVec | None: ret.append(s) return ret + # vm.label(address account, string calldata newLabel) elif funsig == hevm_cheat_code.label_sig: addr = extract_bytes(arg, 4, 32) @@ -687,8 +690,8 @@ def handle(sevm, ex, arg: ByteVec, stack, step_id) -> ByteVec | None: return ret - # getBlockNumber() return (uint256) - elif funsig == hevm_cheat_code.get_block_nunber_sig: + # vm.getBlockNumber() return (uint256) + elif funsig == hevm_cheat_code.get_block_number_sig: ret.append(uint256(ex.block.number)) return ret diff --git a/src/halmos/config.py b/src/halmos/config.py index b963fde2..d22decdb 100644 --- a/src/halmos/config.py +++ b/src/halmos/config.py @@ -165,16 +165,6 @@ class Config: global_default=False, ) - symbolic_msg_sender: bool = arg( - help="set msg.sender symbolic", - global_default=False, - ) - - no_test_constructor: bool = arg( - help="do not run the constructor of test contracts", - global_default=False, - ) - ffi: bool = arg( help="allow the usage of FFI to call external functions", global_default=False, diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py index 435e0c4f..5d948d52 100644 --- a/src/halmos/sevm.py +++ b/src/halmos/sevm.py @@ -122,19 +122,21 @@ ZERO, ONE = con(0), con(1) MAX_CALL_DEPTH = 1024 +EMPTY_BALANCE = Array("balance_00", BitVecSort160, BitVecSort256) + # TODO: make this configurable MAX_MEMORY_SIZE = 2**20 +FOUNDRY_CALLER = 0x1804C8AB1F12E6BBF3894D4083F33E07309D1F38 +FOUNDRY_ORIGIN = FOUNDRY_CALLER +FOUNDRY_TEST = 0x7FA9385BE102AC3EAC297483DD6233D62B3E1496 + # (pc, (jumpdest, ...)) # the jumpdests are stored as strings to avoid the cost of converting bv values JumpID = tuple[int, tuple[str]] # symbolic states -# extcodesize(target address) -f_extcodesize = Function("f_extcodesize", BitVecSort160, BitVecSort256) -# extcodehash(target address) -f_extcodehash = Function("f_extcodehash", BitVecSort160, BitVecSort256) # blockhash(block number) f_blockhash = Function("f_blockhash", BitVecSort256, BitVecSort256) # gas(cnt) @@ -964,14 +966,17 @@ def select(self, array: Any, key: Word, arrays: dict) -> Word: if self.check(key != key0) == unsat: # key == key0 return val0 # empty array - elif not self.symbolic and re.search(r"^storage_.+_00$", str(array)): + elif not self.symbolic and re.search(r"^(storage_.+|balance)_00$", str(array)): # note: simplifying empty array access might have a negative impact on solver performance return ZERO return Select(array, key) def balance_of(self, addr: Word) -> Word: assert_address(addr) - value = self.select(self.balance, uint160(addr), self.balances) + addr = uint160(addr) + value = self.select(self.balance, addr, self.balances) + # generate emptyness axiom for each array index, instead of using quantified formula + self.path.append(Select(EMPTY_BALANCE, addr) == ZERO) # practical assumption on the max balance per account self.path.append(ULT(value, con(2**96))) return value @@ -979,6 +984,7 @@ def balance_of(self, addr: Word) -> Word: def balance_update(self, addr: Word, value: Word) -> None: assert_address(addr) assert_uint256(value) + addr = uint160(addr) new_balance_var = Array( f"balance_{1+len(self.balances):>02}", BitVecSort160, BitVecSort256 ) diff --git a/tests/expected/all.json b/tests/expected/all.json index 2d9291df..ac918d8a 100644 --- a/tests/expected/all.json +++ b/tests/expected/all.json @@ -125,6 +125,15 @@ "time": null, "num_bounded_loops": null }, + { + "name": "check_gaslimit()", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, { "name": "check_roll(uint256)", "exitcode": 0, @@ -820,6 +829,15 @@ "num_paths": null, "time": null, "num_bounded_loops": null + }, + { + "name": "check_initial_balance(address)", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null } ], "test/Extcodehash.t.sol:ExtcodehashTest": [ @@ -1018,6 +1036,15 @@ "time": null, "num_bounded_loops": null }, + { + "name": "check_caller()", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, { "name": "check_deployCode(uint256)", "exitcode": 0, @@ -1053,6 +1080,24 @@ "num_paths": null, "time": null, "num_bounded_loops": null + }, + { + "name": "check_origin()", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_this()", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null } ], "test/Getter.t.sol:GetterTest": [ diff --git a/tests/regression/halmos.toml b/tests/regression/halmos.toml index 3d851260..916a2bf3 100644 --- a/tests/regression/halmos.toml +++ b/tests/regression/halmos.toml @@ -28,12 +28,6 @@ depth = 0 # set the length of dynamic-sized arrays including bytes and string (default: loop unrolling bound) # array-lengths = NAME1=LENGTH1,NAME2=LENGTH2,... -# use uninterpreted abstractions for unknown external calls with the given function signatures -uninterpreted-unknown-calls = "0x150b7a02,0x1626ba7e,0xf23a6e61,0xbc197c81" - -# set the byte size of return data from uninterpreted unknown external calls -return-size-of-unknown-calls = 32 - # Select one of the available storage layout models # The generic model should only be necessary for vyper, huff, or unconventional storage patterns in yul. storage-layout = "solidity" @@ -41,12 +35,6 @@ storage-layout = "solidity" # set default storage values to symbolic symbolic-storage = false -# set msg.sender symbolic -symbolic-msg-sender = false - -# do not run the constructor of test contracts -no-test-constructor = false - # allow the usage of FFI to call external functions ffi = false @@ -125,9 +113,6 @@ solver-max-memory = 0 # use the given command when invoking the solver # solver-command = COMMAND -# run assertion solvers in parallel -solver-parallel = false - # set the number of threads for parallel solvers # solver-threads = N diff --git a/tests/regression/test/Block.t.sol b/tests/regression/test/Block.t.sol index ebb7097d..1f70eaa4 100644 --- a/tests/regression/test/Block.t.sol +++ b/tests/regression/test/Block.t.sol @@ -5,31 +5,41 @@ import "forge-std/Test.sol"; contract BlockCheatCodeTest is Test { function check_fee(uint x) public { + assertEq(block.basefee, 0); // foundry default value vm.fee(x); assert(block.basefee == x); } function check_chainId(uint64 x) public { + assertEq(block.chainid, 31337); // foundry default value vm.chainId(x); assert(block.chainid == x); } function check_coinbase(address x) public { + assertEq(block.coinbase, address(0)); // foundry default value vm.coinbase(x); assert(block.coinbase == x); } function check_difficulty(uint x) public { + assertEq(block.difficulty, 0); // foundry default value vm.difficulty(x); assert(block.difficulty == x); } + function check_gaslimit() public { + assertEq(block.gaslimit, 2**63 - 1); // foundry default value + } + function check_roll(uint x) public { + assertEq(block.number, 1); // foundry default value vm.roll(x); assert(block.number == x); } function check_warp(uint x) public { + assertEq(block.timestamp, 1); // foundry default value vm.warp(x); assert(block.timestamp == x); } diff --git a/tests/regression/test/Deal.t.sol b/tests/regression/test/Deal.t.sol index d26e4066..116b2c11 100644 --- a/tests/regression/test/Deal.t.sol +++ b/tests/regression/test/Deal.t.sol @@ -6,6 +6,10 @@ import "forge-std/Test.sol"; contract DealTest is Test { C c; + function check_initial_balance(address addr) public { + assertEq(addr.balance, 0); + } + function check_deal_1(address payable receiver, uint amount) public { vm.deal(receiver, amount); assert(receiver.balance == amount); diff --git a/tests/regression/test/Foundry.t.sol b/tests/regression/test/Foundry.t.sol index a9cc4202..f6d390f4 100644 --- a/tests/regression/test/Foundry.t.sol +++ b/tests/regression/test/Foundry.t.sol @@ -46,6 +46,18 @@ contract FoundryTest is Test { } */ + function check_caller() public { + assertEq(msg.sender, address(0x1804c8AB1F12E6bbf3894d4083f33e07309d1f38)); + } + + function check_origin() public { + assertEq(tx.origin, address(0x1804c8AB1F12E6bbf3894d4083f33e07309d1f38)); + } + + function check_this() public { + assertEq(address(this), address(0x7FA9385bE102ac3EAc297483Dd6233D62b3e1496)); + } + function check_assume(uint x) public { vm.assume(x < 10); assertLt(x, 100);