diff --git a/src/halmos/cheatcodes.py b/src/halmos/cheatcodes.py index 45d00dc0..b58cfc7b 100644 --- a/src/halmos/cheatcodes.py +++ b/src/halmos/cheatcodes.py @@ -477,7 +477,9 @@ def handle(sevm, ex, arg: ByteVec, stack, step_id) -> Optional[ByteVec]: store_account = uint160(arg.get_word(4)) store_slot = uint256(arg.get_word(36)) store_value = uint256(arg.get_word(68)) - store_account_addr = sevm.resolve_address_alias(ex, store_account, stack, step_id) + store_account_addr = sevm.resolve_address_alias( + ex, store_account, stack, step_id + ) if store_account_addr is None: raise HalmosException(f"uninitialized account: {hexify(store_account)}") @@ -488,7 +490,9 @@ def handle(sevm, ex, arg: ByteVec, stack, step_id) -> Optional[ByteVec]: elif funsig == hevm_cheat_code.load_sig: load_account = uint160(arg.get_word(4)) load_slot = uint256(arg.get_word(36)) - load_account_addr = sevm.resolve_address_alias(ex, load_account, stack, step_id) + load_account_addr = sevm.resolve_address_alias( + ex, load_account, stack, step_id + ) if load_account_addr is None: raise HalmosException(f"uninitialized account: {load_account}") diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py index fc1999f0..5f97059a 100644 --- a/src/halmos/sevm.py +++ b/src/halmos/sevm.py @@ -1517,12 +1517,16 @@ def sstore(self, ex: Exec, addr: Any, loc: Any, val: Any) -> None: self.storage_model.store(ex, addr, loc, val) - def resolve_address_alias(self, ex: Exec, target: Address, stack, step_id) -> Address: + def resolve_address_alias( + self, ex: Exec, target: Address, stack, step_id + ) -> Address: if target in ex.code: return target if self.options.debug: - debug(f"Address {hexify(target)} not in: [{", ".join([hexify(addr) for addr in ex.code])}]") + debug( + f"Address {hexify(target)} not in: [{', '.join([hexify(addr) for addr in ex.code])}]" + ) if is_bv_value(target): if self.options.debug: @@ -1537,10 +1541,12 @@ def resolve_address_alias(self, ex: Exec, target: Address, stack, step_id) -> Ad alias_cond = target == addr if ex.check(alias_cond) != unsat: if self.options.debug: - debug(f"Potential address alias: {hexify(addr)} for {hexify(target)}") + debug( + f"Potential address alias: {hexify(addr)} for {hexify(target)}" + ) potential_aliases.append((addr, alias_cond)) - emptyness_cond = And([ target != addr for addr in ex.code ]) + emptyness_cond = And([target != addr for addr in ex.code]) if ex.check(emptyness_cond) != unsat: if self.options.debug: debug(f"Potential empty address: {hexify(target)}") @@ -1587,12 +1593,7 @@ def transfer_value( ex.balance_update(to, self.arith(ex, EVM.ADD, ex.balance_of(to), value)) def call( - self, - ex: Exec, - op: int, - stack: List[Tuple[Exec, int]], - step_id: int, - to_addr + self, ex: Exec, op: int, stack: List[Tuple[Exec, int]], step_id: int, to_addr ) -> None: gas = ex.st.pop() to = uint160(ex.st.pop()) @@ -1759,7 +1760,9 @@ def call_unknown() -> None: exit_code = con(1) modulus_size = int_of(extract_bytes(arg, 64, 32)) f_modexp = Function( - f"f_modexp_{arg_size}_{modulus_size}", BitVecSorts[arg_size], BitVecSorts[modulus_size] + f"f_modexp_{arg_size}_{modulus_size}", + BitVecSorts[arg_size], + BitVecSorts[modulus_size], ) # TODO: empty returndata in error ret = ByteVec(f_modexp(arg)) @@ -1767,17 +1770,13 @@ def call_unknown() -> None: # ecadd elif eq(to, con_addr(6)): exit_code = con(1) - f_ecadd = Function( - f"f_ecadd", BitVecSorts[1024], BitVecSorts[512] - ) + f_ecadd = Function(f"f_ecadd", BitVecSorts[1024], BitVecSorts[512]) ret = ByteVec(f_ecadd(arg)) # ecmul elif eq(to, con_addr(7)): exit_code = con(1) - f_ecmul = Function( - f"f_ecmul", BitVecSorts[768], BitVecSorts[512] - ) + f_ecmul = Function(f"f_ecmul", BitVecSorts[768], BitVecSorts[512]) ret = ByteVec(f_ecmul(arg)) # ecpairing @@ -1791,9 +1790,7 @@ def call_unknown() -> None: # blake2f elif eq(to, con_addr(9)): exit_code = con(1) - f_blake2f = Function( - f"f_blake2f", BitVecSorts[1704], BitVecSorts[512] - ) + f_blake2f = Function(f"f_blake2f", BitVecSorts[1704], BitVecSorts[512]) ret = ByteVec(f_blake2f(arg)) # point_evaluation @@ -1828,7 +1825,9 @@ def call_unknown() -> None: ret = ByteVec() # push exit code - exit_code_var = BitVec(f"call_exit_code_{ex.new_call_id():>02}", BitVecSort256) + exit_code_var = BitVec( + f"call_exit_code_{ex.new_call_id():>02}", BitVecSort256 + ) ex.path.append(exit_code_var == exit_code) ex.st.push(exit_code if is_bv_value(exit_code) else exit_code_var) @@ -1871,7 +1870,7 @@ def call_unknown() -> None: # precompiles or cheatcodes if ( # precompile - (is_bv_value(to) and to.as_long() in range(1,11)) + (is_bv_value(to) and to.as_long() in range(1, 11)) # cheatcode calls or eq(to, halmos_cheat_code.address) or eq(to, hevm_cheat_code.address) @@ -2346,7 +2345,9 @@ def finalize(ex: Exec): # TODO: define f_extcodesize for known addresses in advance elif opcode == EVM.EXTCODESIZE: account = uint160(ex.st.peek()) - account_addr = self.resolve_address_alias(ex, account, stack, step_id) + account_addr = self.resolve_address_alias( + ex, account, stack, step_id + ) ex.st.pop() if account_addr is not None: @@ -2356,7 +2357,7 @@ def finalize(ex: Exec): or eq(account, halmos_cheat_code.address) or eq(account, console.address) ): - codesize = 777 # dummy arbitrary value + codesize = 777 # dummy arbitrary value else: codesize = 0 @@ -2364,7 +2365,9 @@ def finalize(ex: Exec): elif opcode == EVM.EXTCODECOPY: account: Address = uint160(ex.st.peek()) - account_addr = self.resolve_address_alias(ex, account, stack, step_id) + account_addr = self.resolve_address_alias( + ex, account, stack, step_id + ) ex.st.pop() loc: int = int_of(ex.st.pop(), "symbolic EXTCODECOPY offset") @@ -2390,7 +2393,9 @@ def finalize(ex: Exec): elif opcode == EVM.EXTCODEHASH: account_addr = uint160(ex.st.peek()) - alias_addr = self.resolve_address_alias(ex, account_addr, stack, step_id) + alias_addr = self.resolve_address_alias( + ex, account_addr, stack, step_id + ) ex.st.pop() addr = alias_addr if alias_addr is not None else account_addr