From 5515db70897689646c51202b879400ddb96343e6 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Mon, 26 Aug 2024 17:19:53 -0700 Subject: [PATCH] feat: replace --symbolic-storage with enableSymbolicStorage(address) cheatcode (#355) Co-authored-by: karmacoma --- .github/workflows/test-external.yml | 11 +-- src/halmos/__main__.py | 5 +- src/halmos/cheatcodes.py | 33 ++++++--- src/halmos/config.py | 5 -- src/halmos/sevm.py | 97 ++++++++++++++----------- tests/lib/halmos-cheatcodes | 2 +- tests/regression/halmos.toml | 3 - tests/regression/test/Counter.t.sol | 9 ++- tests/regression/test/Extcodehash.t.sol | 2 +- tests/regression/test/List.t.sol | 12 ++- tests/regression/test/Storage.t.sol | 8 +- tests/test_config.py | 6 +- tests/test_sevm.py | 1 - tests/test_traces.py | 2 - 14 files changed, 106 insertions(+), 90 deletions(-) diff --git a/.github/workflows/test-external.yml b/.github/workflows/test-external.yml index 597a0918..2081b0ef 100644 --- a/.github/workflows/test-external.yml +++ b/.github/workflows/test-external.yml @@ -20,11 +20,12 @@ jobs: matrix: cache-solver: ["", "--cache-solver"] project: - - repo: "morpho-org/morpho-data-structures" - dir: "morpho-data-structures" - cmd: "--function testProve --loop 4 --symbolic-storage" - branch: "" - profile: "" + # TODO: enable after migrating morpho-data-structures tests to use new cheatcode instead of --symbolic-storage + # - repo: "morpho-org/morpho-data-structures" + # dir: "morpho-data-structures" + # cmd: "--function testProve --loop 4 + # branch: "" + # profile: "" - repo: "a16z/cicada" dir: "cicada" cmd: "--contract LibUint1024Test --function testProve --loop 256" diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py index 6d750a74..a063c096 100644 --- a/src/halmos/__main__.py +++ b/src/halmos/__main__.py @@ -61,6 +61,7 @@ Path, SMTQuery, State, + StorageData, con_addr, jumpid_str, mnemonic, @@ -415,12 +416,11 @@ def deploy_test( ex = sevm.mk_exec( code={this: Contract(b"")}, - storage={this: {}}, + storage={this: StorageData()}, balance=EMPTY_BALANCE, block=mk_block(), context=CallContext(message=message), pgm=None, # to be added - symbolic=False, path=Path(mk_solver(args)), ) @@ -663,7 +663,6 @@ def run( pc=0, st=State(), jumpis={}, - symbolic=args.symbolic_storage, # path=path, alias=setup_ex.alias.copy(), diff --git a/src/halmos/cheatcodes.py b/src/halmos/cheatcodes.py index 556cbee6..333cbc1d 100644 --- a/src/halmos/cheatcodes.py +++ b/src/halmos/cheatcodes.py @@ -203,12 +203,20 @@ def stopPrank(self) -> bool: return True +def symbolic_storage(ex, arg, sevm, stack, step_id): + account = uint160(arg.get_word(4)) + account_alias = sevm.resolve_address_alias( + ex, account, stack, step_id, branching=False + ) + ex.storage[account_alias].symbolic = True + + def create_generic(ex, bits: int, var_name: str, type_name: str) -> BitVecRef: label = f"halmos_{var_name}_{type_name}_{ex.new_symbol_id():>02}" return BitVec(label, BitVecSorts[bits]) -def create_uint(ex, arg): +def create_uint(ex, arg, **kwargs): bits = int_of( extract_bytes(arg, 4, 32), "symbolic bit size for halmos.createUint()" ) @@ -219,12 +227,12 @@ def create_uint(ex, arg): return uint256(create_generic(ex, bits, name, f"uint{bits}")) -def create_uint256(ex, arg): +def create_uint256(ex, arg, **kwargs): name = name_of(extract_string_argument(arg, 0)) return create_generic(ex, 256, name, "uint256") -def create_int(ex, arg): +def create_int(ex, arg, **kwargs): bits = int_of( extract_bytes(arg, 4, 32), "symbolic bit size for halmos.createUint()" ) @@ -235,12 +243,12 @@ def create_int(ex, arg): return int256(create_generic(ex, bits, name, f"int{bits}")) -def create_int256(ex, arg): +def create_int256(ex, arg, **kwargs): name = name_of(extract_string_argument(arg, 0)) return create_generic(ex, 256, name, "int256") -def create_bytes(ex, arg): +def create_bytes(ex, arg, **kwargs): byte_size = int_of( extract_bytes(arg, 4, 32), "symbolic byte size for halmos.createBytes()" ) @@ -249,7 +257,7 @@ def create_bytes(ex, arg): return Concat(con(32), con(byte_size), symbolic_bytes) -def create_string(ex, arg): +def create_string(ex, arg, **kwargs): byte_size = int_of( extract_bytes(arg, 4, 32), "symbolic byte size for halmos.createString()" ) @@ -258,22 +266,22 @@ def create_string(ex, arg): return Concat(con(32), con(byte_size), symbolic_string) -def create_bytes4(ex, arg): +def create_bytes4(ex, arg, **kwargs): name = name_of(extract_string_argument(arg, 0)) return Concat(create_generic(ex, 32, name, "bytes4"), con(0, size_bits=224)) -def create_bytes32(ex, arg): +def create_bytes32(ex, arg, **kwargs): name = name_of(extract_string_argument(arg, 0)) return create_generic(ex, 256, name, "bytes32") -def create_address(ex, arg): +def create_address(ex, arg, **kwargs): name = name_of(extract_string_argument(arg, 0)) return uint256(create_generic(ex, 160, name, "address")) -def create_bool(ex, arg): +def create_bool(ex, arg, **kwargs): name = name_of(extract_string_argument(arg, 0)) return uint256(create_generic(ex, 1, name, "bool")) @@ -313,13 +321,14 @@ class halmos_cheat_code: 0xBF72FA66: create_bytes32, # createBytes32(string) 0x3B0FA01B: create_address, # createAddress(string) 0x6E0BB659: create_bool, # createBool(string) + 0xDC00BA4D: symbolic_storage, # enableSymbolicStorage(address) } @staticmethod - def handle(ex, arg: BitVecRef) -> BitVecRef: + def handle(sevm, ex, arg: BitVecRef, stack, step_id) -> BitVecRef: funsig = int_of(extract_funsig(arg), "symbolic halmos cheatcode") if handler := halmos_cheat_code.handlers.get(funsig): - return ByteVec(handler(ex, arg)) + return ByteVec(handler(ex, arg, sevm=sevm, stack=stack, step_id=step_id)) error_msg = f"Unknown halmos cheat code: function selector = 0x{funsig:0>8x}, calldata = {hexify(arg)}" raise HalmosException(error_msg) diff --git a/src/halmos/config.py b/src/halmos/config.py index d22decdb..defcae5c 100644 --- a/src/halmos/config.py +++ b/src/halmos/config.py @@ -160,11 +160,6 @@ class Config: choices=["solidity", "generic"], ) - symbolic_storage: bool = arg( - help="set default storage values to symbolic", - 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 5d948d52..1752e740 100644 --- a/src/halmos/sevm.py +++ b/src/halmos/sevm.py @@ -757,10 +757,16 @@ def extend_path(self, path): self.extend(path.conditions.keys()) +@dataclass +class StorageData: + symbolic: bool = False + mapping: dict = field(default_factory=dict) + + class Exec: # an execution path # network code: dict[Address, Contract] - storage: dict[Address, dict[int, Any]] # address -> { storage slot -> value } + storage: dict[Address, StorageData] # address -> { storage slot -> value } balance: Any # address -> balance # block @@ -775,7 +781,6 @@ class Exec: # an execution path pc: int st: State # stack and memory jumpis: dict[JumpID, dict[bool, int]] # for loop detection - symbolic: bool # symbolic or concrete storage addresses_to_delete: set[Address] # path @@ -804,7 +809,6 @@ def __init__(self, **kwargs) -> None: self.pc = kwargs["pc"] self.st = kwargs["st"] self.jumpis = kwargs["jumpis"] - self.symbolic = kwargs["symbolic"] self.addresses_to_delete = kwargs.get("addresses_to_delete") or set() # self.path = kwargs["path"] @@ -952,7 +956,9 @@ def check(self, cond: Any) -> Any: return self.path.check(cond) - def select(self, array: Any, key: Word, arrays: dict) -> Word: + def select( + self, array: Any, key: Word, arrays: dict, symbolic: bool = False + ) -> Word: if array in arrays: store = arrays[array] if store.decl().name() == "store" and store.num_args() == 3: @@ -962,11 +968,11 @@ def select(self, array: Any, key: Word, arrays: dict) -> Word: if eq(key, key0): # structural equality return val0 if self.check(key == key0) == unsat: # key != key0 - return self.select(base, key, arrays) + return self.select(base, key, arrays, symbolic) if self.check(key != key0) == unsat: # key == key0 return val0 # empty array - elif not self.symbolic and re.search(r"^(storage_.+|balance)_00$", str(array)): + elif not 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) @@ -1138,23 +1144,23 @@ def init(cls, ex: Exec, addr: Any, slot: int, keys: tuple) -> None: assert_address(addr) num_keys = len(keys) size_keys = cls.bitsize(keys) - if slot not in ex.storage[addr]: - ex.storage[addr][slot] = {} - if num_keys not in ex.storage[addr][slot]: - ex.storage[addr][slot][num_keys] = {} - if size_keys not in ex.storage[addr][slot][num_keys]: + if slot not in ex.storage[addr].mapping: + ex.storage[addr].mapping[slot] = {} + if num_keys not in ex.storage[addr].mapping[slot]: + ex.storage[addr].mapping[slot][num_keys] = {} + if size_keys not in ex.storage[addr].mapping[slot][num_keys]: if size_keys == 0: - if ex.symbolic: + if ex.storage[addr].symbolic: label = f"storage_{id_str(addr)}_{slot}_{num_keys}_{size_keys}_00" - ex.storage[addr][slot][num_keys][size_keys] = BitVec( + ex.storage[addr].mapping[slot][num_keys][size_keys] = BitVec( label, BitVecSort256 ) else: - ex.storage[addr][slot][num_keys][size_keys] = ZERO + ex.storage[addr].mapping[slot][num_keys][size_keys] = ZERO else: # do not use z3 const array `K(BitVecSort(size_keys), ZERO)` when not ex.symbolic # instead use normal smt array, and generate emptyness axiom; see load() - ex.storage[addr][slot][num_keys][size_keys] = cls.empty( + ex.storage[addr].mapping[slot][num_keys][size_keys] = cls.empty( addr, slot, keys ) @@ -1168,15 +1174,18 @@ def load(cls, ex: Exec, addr: Any, loc: Word) -> Word: num_keys = len(keys) size_keys = cls.bitsize(keys) if num_keys == 0: - return ex.storage[addr][slot][num_keys][size_keys] + return ex.storage[addr].mapping[slot][num_keys][size_keys] else: - if not ex.symbolic: + if not ex.storage[addr].symbolic: # generate emptyness axiom for each array index, instead of using quantified formula; see init() ex.path.append( Select(cls.empty(addr, slot, keys), concat(keys)) == ZERO ) return ex.select( - ex.storage[addr][slot][num_keys][size_keys], concat(keys), ex.storages + ex.storage[addr].mapping[slot][num_keys][size_keys], + concat(keys), + ex.storages, + ex.storage[addr].symbolic, ) @classmethod @@ -1189,7 +1198,7 @@ def store(cls, ex: Exec, addr: Any, loc: Any, val: Any) -> None: num_keys = len(keys) size_keys = cls.bitsize(keys) if num_keys == 0: - ex.storage[addr][slot][num_keys][size_keys] = val + ex.storage[addr].mapping[slot][num_keys][size_keys] = val else: new_storage_var = Array( f"storage_{id_str(addr)}_{slot}_{num_keys}_{size_keys}_{1+len(ex.storages):>02}", @@ -1197,10 +1206,10 @@ def store(cls, ex: Exec, addr: Any, loc: Any, val: Any) -> None: BitVecSort256, ) new_storage = Store( - ex.storage[addr][slot][num_keys][size_keys], concat(keys), val + ex.storage[addr].mapping[slot][num_keys][size_keys], concat(keys), val ) ex.path.append(new_storage_var == new_storage) - ex.storage[addr][slot][num_keys][size_keys] = new_storage_var + ex.storage[addr].mapping[slot][num_keys][size_keys] = new_storage_var ex.storages[new_storage_var] = new_storage @classmethod @@ -1279,17 +1288,22 @@ def empty(cls, addr: BitVecRef, loc: BitVecRef) -> ArrayRef: @classmethod def init(cls, ex: Exec, addr: Any, loc: BitVecRef) -> None: assert_address(addr) - if loc.size() not in ex.storage[addr]: - ex.storage[addr][loc.size()] = cls.empty(addr, loc) + if loc.size() not in ex.storage[addr].mapping: + ex.storage[addr].mapping[loc.size()] = cls.empty(addr, loc) @classmethod def load(cls, ex: Exec, addr: Any, loc: Word) -> Word: loc = cls.decode(loc) cls.init(ex, addr, loc) - if not ex.symbolic: + if not ex.storage[addr].symbolic: # generate emptyness axiom for each array index, instead of using quantified formula; see init() ex.path.append(Select(cls.empty(addr, loc), loc) == ZERO) - return ex.select(ex.storage[addr][loc.size()], loc, ex.storages) + return ex.select( + ex.storage[addr].mapping[loc.size()], + loc, + ex.storages, + ex.storage[addr].symbolic, + ) @classmethod def store(cls, ex: Exec, addr: Any, loc: Any, val: Any) -> None: @@ -1300,9 +1314,9 @@ def store(cls, ex: Exec, addr: Any, loc: Any, val: Any) -> None: BitVecSorts[loc.size()], BitVecSort256, ) - new_storage = Store(ex.storage[addr][loc.size()], loc, val) + new_storage = Store(ex.storage[addr].mapping[loc.size()], loc, val) ex.path.append(new_storage_var == new_storage) - ex.storage[addr][loc.size()] = new_storage_var + ex.storage[addr].mapping[loc.size()] = new_storage_var ex.storages[new_storage_var] = new_storage @classmethod @@ -1833,7 +1847,6 @@ def callback(new_ex: Exec, stack, step_id): new_ex.pc = ex.pc new_ex.st = deepcopy(ex.st) new_ex.jumpis = deepcopy(ex.jumpis) - new_ex.symbolic = ex.symbolic # set return data (in memory) effective_ret_size = min(ret_size, new_ex.returndatasize()) @@ -1873,7 +1886,6 @@ def callback(new_ex: Exec, stack, step_id): pc=0, st=State(), jumpis={}, - symbolic=ex.symbolic, # path=ex.path, alias=ex.alias, @@ -1975,7 +1987,7 @@ def call_unknown() -> None: # halmos cheat code elif eq(to, halmos_cheat_code.address): exit_code = ONE - ret = halmos_cheat_code.handle(ex, arg) + ret = halmos_cheat_code.handle(self, ex, arg, stack, step_id) # vm cheat code elif eq(to, hevm_cheat_code.address): @@ -2132,7 +2144,8 @@ def create( # setup new account ex.set_code(new_addr, Contract(b"")) # existing code must be empty - ex.storage[new_addr] = {} # existing storage may not be empty and reset here + # existing storage may not be empty and reset here + ex.storage[new_addr] = StorageData() # transfer value self.transfer_value(ex, pranked_caller, new_addr, value) @@ -2151,7 +2164,6 @@ def callback(new_ex: Exec, stack, step_id): new_ex.pc = ex.pc new_ex.st = deepcopy(ex.st) new_ex.jumpis = deepcopy(ex.jumpis) - new_ex.symbolic = ex.symbolic if subcall.is_stuck(): # internal errors abort the current path, @@ -2192,7 +2204,6 @@ def callback(new_ex: Exec, stack, step_id): pc=0, st=State(), jumpis={}, - symbolic=False, # path=ex.path, alias=ex.alias, @@ -2308,7 +2319,6 @@ def create_branch(self, ex: Exec, cond: BitVecRef, target: int) -> Exec: pc=target, st=deepcopy(ex.st), jumpis=deepcopy(ex.jumpis), - symbolic=ex.symbolic, # path=new_path, alias=ex.alias.copy(), @@ -2521,15 +2531,16 @@ def finalize(ex: Exec): if account_alias is not None: codesize = len(ex.code[account_alias]) - elif ( - eq(account, hevm_cheat_code.address) - or eq(account, halmos_cheat_code.address) - or eq(account, console.address) - ): - # dummy arbitrary value, consistent with foundry - codesize = 1 if eq(account, hevm_cheat_code.address) else 0 else: - codesize = 0 + codesize = ( + 1 # dummy arbitrary value, consistent with foundry + if eq(account, hevm_cheat_code.address) + # NOTE: the codesize of halmos cheatcode should be non-zero to pass the extcodesize check for external calls with non-empty return types. this behavior differs from foundry. + or eq(account, halmos_cheat_code.address) + # the codesize of console is considered zero in foundry + # or eq(account, console.address) + else 0 + ) ex.st.push(codesize) @@ -2837,7 +2848,6 @@ def mk_exec( context: CallContext, # pgm, - symbolic, path, ) -> Exec: return Exec( @@ -2854,7 +2864,6 @@ def mk_exec( pc=0, st=State(), jumpis={}, - symbolic=symbolic, # path=path, alias={}, diff --git a/tests/lib/halmos-cheatcodes b/tests/lib/halmos-cheatcodes index c0d86550..3ca0e11c 160000 --- a/tests/lib/halmos-cheatcodes +++ b/tests/lib/halmos-cheatcodes @@ -1 +1 @@ -Subproject commit c0d865508c0fee0a11b97732c5e90f9cad6b65a5 +Subproject commit 3ca0e11cf6ea5b3f73997a44932ab9c048c5ed57 diff --git a/tests/regression/halmos.toml b/tests/regression/halmos.toml index 916a2bf3..5254d685 100644 --- a/tests/regression/halmos.toml +++ b/tests/regression/halmos.toml @@ -32,9 +32,6 @@ depth = 0 # The generic model should only be necessary for vyper, huff, or unconventional storage patterns in yul. storage-layout = "solidity" -# set default storage values to symbolic -symbolic-storage = false - # allow the usage of FFI to call external functions ffi = false diff --git a/tests/regression/test/Counter.t.sol b/tests/regression/test/Counter.t.sol index 02960bce..0f0ab95b 100644 --- a/tests/regression/test/Counter.t.sol +++ b/tests/regression/test/Counter.t.sol @@ -2,9 +2,14 @@ pragma solidity >=0.8.0 <0.9.0; import "../src/Counter.sol"; +import {SymTest} from "halmos-cheatcodes/SymTest.sol"; + +/// @custom:halmos --loop 4 +contract CounterTest is Counter, SymTest { + function setUp() public { + svm.enableSymbolicStorage(address(this)); + } -/// @custom:halmos --loop 4 --symbolic-storage -contract CounterTest is Counter { function check_set(uint n) public { set(n); assert(cnt == n); diff --git a/tests/regression/test/Extcodehash.t.sol b/tests/regression/test/Extcodehash.t.sol index bdfb80f0..11adff25 100644 --- a/tests/regression/test/Extcodehash.t.sol +++ b/tests/regression/test/Extcodehash.t.sol @@ -258,7 +258,7 @@ contract ExtcodehashTest is Test, SymTest { assertEq(VM_ADDRESS.code.length, 1); assertEq(console.CONSOLE_ADDRESS.code.length, 0); - assertEq(SymTest.SVM_ADDRESS.code.length, 0); + assertEq(SymTest.SVM_ADDRESS.code.length, 1); // different from foundry } function check_extcodehash_cheatcode() external { diff --git a/tests/regression/test/List.t.sol b/tests/regression/test/List.t.sol index 210f4c2b..ae151480 100644 --- a/tests/regression/test/List.t.sol +++ b/tests/regression/test/List.t.sol @@ -3,9 +3,13 @@ pragma solidity >=0.8.0 <0.9.0; import "forge-std/Test.sol"; import "../src/List.sol"; +import {SymTest} from "halmos-cheatcodes/SymTest.sol"; + +contract ListTest is SymTest, Test, List { + function setUp() public { + svm.enableSymbolicStorage(address(this)); + } -/// @custom:halmos --symbolic-storage -contract ListTest is Test, List { function check_add(uint x) public { uint oldSize = arr.length; vm.assume(oldSize < type(uint).max); @@ -32,13 +36,13 @@ contract ListTest is Test, List { } } -/// @custom:halmos --symbolic-storage -contract ListTestTest is Test { +contract ListTestTest is SymTest, Test { List list; function setUp() public { list = new List(); list.add(1); + svm.enableSymbolicStorage(address(list)); } function check_add(uint x) public { diff --git a/tests/regression/test/Storage.t.sol b/tests/regression/test/Storage.t.sol index f8b106d5..97c8d5b2 100644 --- a/tests/regression/test/Storage.t.sol +++ b/tests/regression/test/Storage.t.sol @@ -3,9 +3,13 @@ pragma solidity >=0.8.0 <0.9.0; import "forge-std/Test.sol"; import "../src/Storage.sol"; +import {SymTest} from "halmos-cheatcodes/SymTest.sol"; + +contract StorageTest is Storage, SymTest { + function setUp() public { + svm.enableSymbolicStorage(address(this)); + } -/// @custom:halmos --symbolic-storage -contract StorageTest is Storage { function check_setMap1(uint k, uint v) public { setMap1(k, v); assert(map1[k] == v); diff --git a/tests/test_config.py b/tests/test_config.py index ab564665..cd073e81 100644 --- a/tests/test_config.py +++ b/tests/test_config.py @@ -159,9 +159,7 @@ def test_config_file_snake_case(config, toml_parser): def test_config_e2e(config, parser, toml_parser): # when we apply overrides to the default config - config_file_data = toml_parser.parse_str( - "[global]\nverbose = 42\nsymbolic_storage = true" - ) + config_file_data = toml_parser.parse_str("[global]\nverbose = 42") config = config.with_overrides(source="halmos.toml", **config_file_data) args = parser.parse_args(["-vvv"]) @@ -169,12 +167,10 @@ def test_config_e2e(config, parser, toml_parser): # then the config object should have the expected values assert config.verbose == 3 - assert config.symbolic_storage is True assert config.loop == 2 # and each value should have the expected source assert config.value_with_source("verbose") == (3, "command-line") - assert config.value_with_source("symbolic_storage") == (True, "halmos.toml") assert config.value_with_source("loop") == (2, "default") diff --git a/tests/test_sevm.py b/tests/test_sevm.py index a4bb00eb..7c39ef77 100644 --- a/tests/test_sevm.py +++ b/tests/test_sevm.py @@ -71,7 +71,6 @@ def mk_ex(hexcode, sevm, solver, storage, caller, this): block=mk_block(), context=CallContext(message), pgm=bytecode, - symbolic=True, path=Path(solver), ) diff --git a/tests/test_traces.py b/tests/test_traces.py index 8e31440f..d6dc22d5 100644 --- a/tests/test_traces.py +++ b/tests/test_traces.py @@ -202,7 +202,6 @@ def mk_create_ex( context=CallContext(message=message), this=this, pgm=bytecode, - symbolic=True, path=Path(solver), ) @@ -239,7 +238,6 @@ def mk_ex( context=CallContext(message=message), this=this, pgm=bytecode, - symbolic=True, path=Path(solver), )