diff --git a/.git-blame-ignore-revs b/.git-blame-ignore-revs index b4350210..699095e0 100644 --- a/.git-blame-ignore-revs +++ b/.git-blame-ignore-revs @@ -1,2 +1,3 @@ # Migrate code style to Black 449404c7a2b318b8203dbccbeac11c87d20c422f +00cc14c20659cbf717594451dfc7906b295dca98 diff --git a/examples/tokens/ERC20/remappings.txt b/examples/tokens/ERC20/remappings.txt index 5a2d0833..acf3e02d 100644 --- a/examples/tokens/ERC20/remappings.txt +++ b/examples/tokens/ERC20/remappings.txt @@ -1 +1,2 @@ openzeppelin/=../../../tests/lib/openzeppelin-contracts/contracts/ +ds-test/=../../../tests/lib/forge-std/lib/ds-test/src/ diff --git a/examples/tokens/ERC721/remappings.txt b/examples/tokens/ERC721/remappings.txt index 5a2d0833..acf3e02d 100644 --- a/examples/tokens/ERC721/remappings.txt +++ b/examples/tokens/ERC721/remappings.txt @@ -1 +1,2 @@ openzeppelin/=../../../tests/lib/openzeppelin-contracts/contracts/ +ds-test/=../../../tests/lib/forge-std/lib/ds-test/src/ diff --git a/pyproject.toml b/pyproject.toml index 3fc4ab65..fcf94529 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -34,3 +34,7 @@ halmos = "halmos.__main__:main" [tool.black] target-versions = ["py38", "py39", "py310", "py311"] + +[tool.pytest.ini_options] +# TODO: re-add test_traces.py when we have a better way to support it in CI +addopts = "--ignore=tests/lib/solady/ext/woke --ignore=tests/test_traces.py" diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py index 7a39e3c5..dbd21864 100644 --- a/src/halmos/__main__.py +++ b/src/halmos/__main__.py @@ -12,9 +12,24 @@ from dataclasses import dataclass, asdict from importlib import metadata -from .pools import thread_pool, process_pool +from concurrent.futures import ProcessPoolExecutor, ThreadPoolExecutor + from .sevm import * -from .utils import color_good, color_warn, hexify, NamedTimer +from .utils import ( + hexify, + indent_text, + NamedTimer, + yellow, + cyan, + green, + red, + error, + info, + color_good, + color_warn, + color_info, + color_error, +) from .warnings import * from .parser import mk_arg_parser from .calldata import Calldata @@ -28,10 +43,22 @@ if hasattr(sys, "set_int_max_str_digits"): sys.set_int_max_str_digits(0) +# we need to be able to process at least the max message depth (1024) +sys.setrecursionlimit(1024 * 4) + # sometimes defaults to cp1252 on Windows, which can cause UnicodeEncodeError if sys.stdout.encoding != "utf-8": sys.stdout.reconfigure(encoding="utf-8") +# Panic(1) +# bytes4(keccak256("Panic(uint256)")) + bytes32(1) +ASSERT_FAIL = 0x4E487B710000000000000000000000000000000000000000000000000000000000000001 + +VERBOSITY_TRACE_COUNTEREXAMPLE = 2 +VERBOSITY_TRACE_SETUP = 3 +VERBOSITY_TRACE_PATHS = 4 +VERBOSITY_TRACE_CONSTRUCTOR = 5 + @dataclass(frozen=True) class FunctionInfo: @@ -135,29 +162,137 @@ def mk_solver(args: Namespace): return solver -def run_bytecode(hexcode: str, args: Namespace) -> List[Exec]: - contract = Contract.from_hexcode(hexcode) +def rendered_initcode(context: CallContext) -> str: + message = context.message + data = message.data - storage = {} + initcode_str = "" + args_str = "" - solver = mk_solver(args) + if ( + isinstance(data, BitVecRef) + and is_app(data) + and data.decl().kind() == Z3_OP_CONCAT + ): + children = [arg for arg in data.children()] + if isinstance(children[0], BitVecNumRef): + initcode_str = hex(children[0].as_long()) + args_str = ", ".join(map(str, children[1:])) + else: + initcode_str = hexify(data) + + return f"{initcode_str}({color_info(args_str)})" + + +def render_output(context: CallContext) -> None: + output = context.output + returndata_str = "0x" + failed = output.error is not None + + if not failed and context.is_stuck(): + return + + if output.data is not None: + is_create = context.message.is_create() + + returndata_str = ( + f"<{byte_length(output.data)} bytes of code>" + if (is_create and not failed) + else hexify(output.data) + ) + + ret_scheme = context.output.return_scheme + ret_scheme_str = f"{cyan(mnemonic(ret_scheme))} " if ret_scheme is not None else "" + error_str = f" (error: {repr(output.error)})" if failed else "" + + color = red if failed else green + indent = context.depth * " " + print( + f"{indent}{color('↩ ')}{ret_scheme_str}{color(returndata_str)}{color(error_str)}" + ) + + +def rendered_log(log: EventLog) -> str: + opcode_str = f"LOG{len(log.topics)}" + topics = [ + f"{color_info(f'topic{i}')}={hexify(topic)}" + for i, topic in enumerate(log.topics) + ] + data_str = f"{color_info('data')}={hexify(log.data)}" + args_str = ", ".join(topics + [data_str]) + + return f"{opcode_str}({args_str})" + + +def render_trace(context: CallContext) -> None: + # TODO: label for known addresses + # TODO: decode calldata + # TODO: decode logs + + message = context.message + addr = unbox_int(message.target) + addr_str = str(addr) if is_bv(addr) else hex(addr) + value = unbox_int(message.value) + value_str = f" (value: {value})" if is_bv(value) or value > 0 else "" + + call_scheme_str = f"{cyan(mnemonic(message.call_scheme))} " + indent = context.depth * " " + + if message.is_create(): + # TODO: select verbosity level to render full initcode + # initcode_str = rendered_initcode(context) + initcode_str = f"<{byte_length(message.data)} bytes of initcode>" + print(f"{indent}{call_scheme_str}{addr_str}::{initcode_str}{value_str}") + + else: + calldata = ( + hexify(simplify(Concat(message.data))) + if any(is_bv(x) for x in message.data) + else bytes(message.data).hex() or "0x" + ) + + call_str = f"{addr_str}::{calldata}" + static_str = yellow(" [static]") if message.is_static else "" + print(f"{indent}{call_scheme_str}{call_str}{static_str}{value_str}") + + log_indent = (context.depth + 1) * " " + for trace_element in context.trace: + if isinstance(trace_element, CallContext): + render_trace(trace_element) + elif isinstance(trace_element, EventLog): + print(f"{log_indent}{rendered_log(trace_element)}") + else: + raise HalmosException(f"unexpected trace element: {trace_element}") + + render_output(context) + + if context.depth == 1: + print() + + +def run_bytecode(hexcode: str, args: Namespace) -> List[Exec]: + solver = mk_solver(args) + contract = Contract.from_hexcode(hexcode) balance = mk_balance() block = mk_block() - callvalue = mk_callvalue() - caller = mk_caller(args) - this = mk_this() options = mk_options(args) + this = mk_this() + + message = Message( + target=this, + caller=mk_caller(args), + value=mk_callvalue(), + data=[], + ) sevm = SEVM(options) ex = sevm.mk_exec( code={this: contract}, - storage={this: storage}, + storage={this: {}}, balance=balance, block=block, - calldata=[], - callvalue=callvalue, - caller=caller, + context=CallContext(message=message), this=this, pgm=contract, symbolic=args.symbolic_storage, @@ -167,13 +302,20 @@ def run_bytecode(hexcode: str, args: Namespace) -> List[Exec]: for idx, ex in enumerate(exs): opcode = ex.current_opcode() - if opcode in [EVM.STOP, EVM.RETURN, EVM.REVERT, EVM.INVALID]: - model_with_context = gen_model(args, idx, ex) - print( - f"Final opcode: {mnemonic(opcode)} | Return data: {ex.output} | Input example: {model_with_context.model}" + error = ex.context.output.error + returndata = ex.context.output.data + + if error: + warn( + INTERNAL_ERROR, + f"{mnemonic(opcode)} failed, error={error}, returndata={returndata}", ) else: - warn(INTERNAL_ERROR, f"{mnemonic(opcode)} failed: {ex.error}") + print(f"Final opcode: {mnemonic(opcode)})") + print(f"Return data: {returndata}") + model_with_context = gen_model(args, idx, ex) + print(f"Input example: {model_with_context.model}") + if args.print_states: print(f"# {idx+1} / {len(exs)}") print(ex) @@ -189,15 +331,19 @@ def deploy_test( libs: Dict, ) -> Exec: this = mk_this() + message = Message( + target=this, + caller=mk_caller(args), + value=con(0), + data=[], + ) ex = sevm.mk_exec( code={this: Contract(b"")}, storage={this: {}}, balance=mk_balance(), block=mk_block(), - calldata=[], - callvalue=con(0), - caller=mk_caller(args), + context=CallContext(message=message), this=this, pgm=None, # to be added symbolic=False, @@ -226,22 +372,28 @@ def deploy_test( # sanity check if len(exs) != 1: raise ValueError(f"constructor: # of paths: {len(exs)}") + ex = exs[0] - if ex.failed: - raise ValueError(f"constructor: failed: {ex.error}") - if ex.current_opcode() not in [EVM.STOP, EVM.RETURN]: - raise ValueError(f"constructor: failed: {ex.current_opcode()}: {ex.error}") + + if args.verbose >= VERBOSITY_TRACE_CONSTRUCTOR: + print("Constructor trace:") + render_trace(ex.context) + + error = ex.context.output.error + returndata = ex.context.output.data + if error: + raise ValueError(f"constructor failed, error={error} returndata={returndata}") # deployed bytecode - deployed_bytecode = Contract(ex.output) + deployed_bytecode = Contract(returndata) ex.code[this] = deployed_bytecode ex.pgm = deployed_bytecode # reset vm state ex.pc = 0 ex.st = State() + ex.context.output = CallOutput() ex.jumpis = {} - ex.output = None ex.prank = Prank() return ex @@ -259,23 +411,25 @@ def setup( setup_timer.create_subtimer("decode") sevm = SEVM(mk_options(args)) - setup_ex = deploy_test(creation_hexcode, deployed_hexcode, sevm, args, libs) setup_timer.create_subtimer("run") - setup_sig, setup_name, setup_selector = ( - setup_info.sig, - setup_info.name, - setup_info.selector, - ) + setup_sig, setup_selector = (setup_info.sig, setup_info.selector) if setup_sig: - if args.verbose >= 1: - print(f"Running {setup_sig}") - - wstore(setup_ex.calldata, 0, 4, BitVecVal(int(setup_selector, 16), 32)) + calldata = [] + wstore(calldata, 0, 4, BitVecVal(int(setup_selector, 16), 32)) dyn_param_size = [] # TODO: propagate to run - mk_calldata(abi, setup_info, setup_ex.calldata, dyn_param_size, args) + mk_calldata(abi, setup_info, calldata, dyn_param_size, args) + + setup_ex.context = CallContext( + message=Message( + target=setup_ex.message().target, + caller=setup_ex.message().caller, + value=con(0), + data=calldata, + ), + ) (setup_exs_all, setup_steps, setup_logs) = sevm.run(setup_ex) @@ -290,27 +444,47 @@ def setup( setup_exs = [] for idx, setup_ex in enumerate(setup_exs_all): + if args.verbose >= VERBOSITY_TRACE_SETUP: + num_traces = len(setup_exs_all) + print( + f"{setup_sig} trace #{idx+1}/{num_traces}:" + if num_traces > 1 + else f"{setup_sig} trace:" + ) + render_trace(setup_ex.context) + opcode = setup_ex.current_opcode() - if opcode in [EVM.STOP, EVM.RETURN]: + error = setup_ex.context.output.error + + if error is None: setup_ex.solver.set(timeout=args.solver_timeout_assertion) res = setup_ex.solver.check() if res != unsat: setup_exs.append(setup_ex) - elif opcode not in [EVM.REVERT, EVM.INVALID]: - print( - color_warn( - f"Warning: {setup_sig} execution encountered an issue at {mnemonic(opcode)}: {setup_ex.error}" + else: + if opcode not in [EVM.REVERT, EVM.INVALID]: + warn( + INTERNAL_ERROR, + f"Warning: {setup_sig} execution encountered an issue at {mnemonic(opcode)}: {error}", ) - ) + + # only render the trace if we didn't already do it + if ( + args.verbose < VERBOSITY_TRACE_SETUP + and args.verbose >= VERBOSITY_TRACE_COUNTEREXAMPLE + ): + print(f"{setup_sig} trace:") + render_trace(setup_ex.context) if len(setup_exs) == 0: - raise ValueError(f"No successful path found in {setup_sig}") + raise HalmosException(f"No successful path found in {setup_sig}") + if len(setup_exs) > 1: - print( - color_warn( - f"Warning: multiple paths were found in {setup_sig}; an arbitrary path has been selected for the following tests." - ) + info( + f"Warning: multiple paths were found in {setup_sig}; " + "an arbitrary path has been selected for the following tests." ) + if args.debug: print("\n".join(map(str, setup_exs))) @@ -351,6 +525,11 @@ class TestResult: num_bounded_loops: int = None # number of incomplete loops +def is_global_fail_set(context: CallContext) -> bool: + hevm_fail = isinstance(context.output.error, FailCheatcode) + return hevm_fail or any(is_global_fail_set(x) for x in context.subcalls()) + + def run( setup_ex: Exec, abi: List, @@ -366,17 +545,17 @@ def run( # cd = [] - wstore(cd, 0, 4, BitVecVal(int(funselector, 16), 32)) dyn_param_size = [] mk_calldata(abi, fun_info, cd, dyn_param_size, args) - # - # callvalue - # - - callvalue = mk_callvalue() + message = Message( + target=setup_ex.this, + caller=setup_ex.caller(), + value=con(0), + data=cd, + ) # # run @@ -400,16 +579,13 @@ def run( # block=deepcopy(setup_ex.block), # - calldata=cd, - callvalue=callvalue, - caller=setup_ex.caller, + context=CallContext(message=message), this=setup_ex.this, # pgm=setup_ex.code[setup_ex.this], pc=0, st=State(), jumpis={}, - output=None, symbolic=args.symbolic_storage, prank=Prank(), # prank is reset after setUp() # @@ -417,14 +593,11 @@ def run( path=setup_ex.path.copy(), alias=setup_ex.alias.copy(), # - log=setup_ex.log.copy(), cnts=deepcopy(setup_ex.cnts), sha3s=setup_ex.sha3s.copy(), storages=setup_ex.storages.copy(), balances=setup_ex.balances.copy(), calls=setup_ex.calls.copy(), - failed=setup_ex.failed, - error=setup_ex.error, ) ) @@ -437,21 +610,30 @@ def run( stuck = [] for idx, ex in enumerate(exs): - opcode = ex.current_opcode() - if opcode in [EVM.STOP, EVM.RETURN]: - normal += 1 - elif opcode in [EVM.REVERT, EVM.INVALID]: - # Panic(1) - # bytes4(keccak256("Panic(uint256)")) + bytes32(1) - if ( - unbox_int(ex.output) - == 0x4E487B710000000000000000000000000000000000000000000000000000000000000001 - ): + if args.verbose >= VERBOSITY_TRACE_PATHS: + print(f"Path #{idx+1}/{len(exs)}:") + print(indent_text(ex.str_path())) + + print("\nTrace:") + render_trace(ex.context) + + error = ex.context.output.error + + if isinstance(error, Revert): + returndata = ex.context.output.data + if unbox_int(returndata) == ASSERT_FAIL: execs_to_model.append((idx, ex)) - elif ex.failed: + continue + + if is_global_fail_set(ex.context): execs_to_model.append((idx, ex)) - else: - stuck.append((opcode, idx, ex)) + continue + + if ex.context.is_stuck(): + stuck.append((idx, ex, ex.context.get_stuck_reason())) + + elif not error: + normal += 1 if len(execs_to_model) > 0 and args.dump_smt_queries: dirname = f"/tmp/{funname}.{uuid.uuid4().hex}" @@ -476,7 +658,8 @@ def run( fn_args = [ GenModelArgs(args, idx, ex.solver.to_smt2()) for idx, ex in execs_to_model ] - models = [m for m in thread_pool.map(gen_model_from_sexpr, fn_args)] + with ThreadPoolExecutor() as thread_pool: + models = list(thread_pool.map(gen_model_from_sexpr, fn_args)) else: models = [gen_model(args, idx, ex) for idx, ex in execs_to_model] @@ -504,7 +687,7 @@ def run( # model could be an empty dict here if model is not None: if is_valid: - print(color_warn(f"Counterexample: {render_model(model)}")) + print(red(f"Counterexample: {render_model(model)}")) counterexamples.append(model) elif args.print_potential_counterexample: warn( @@ -524,11 +707,19 @@ def run( print(f"# {idx+1} / {len(exs)}") print(ex) - for opcode, idx, ex in stuck: - warn(INTERNAL_ERROR, f"{mnemonic(opcode)} failed: {ex.error}") + if args.verbose >= VERBOSITY_TRACE_COUNTEREXAMPLE: + print( + f"Trace #{idx+1}/{len(exs)}:" + if args.verbose == VERBOSITY_TRACE_PATHS + else "Trace:" + ) + render_trace(ex.context) + + for idx, ex, err in stuck: + warn(INTERNAL_ERROR, f"Encountered {err}") if args.print_blocked_states: - print(f"# {idx+1} / {len(exs)}") - print(ex) + print(f"\nPath #{idx+1}/{len(exs)}") + render_trace(ex.context) if logs.bounded_loops: warn( @@ -597,11 +788,8 @@ def setup_and_run_single(fn_args: SetupAndRunSingleArgs) -> List[TestResult]: fn_args.libs, ) except Exception as err: - print( - color_warn( - f"Error: {fn_args.setup_info.sig} failed: {type(err).__name__}: {err}" - ) - ) + error(f"Error: {fn_args.setup_info.sig} failed: {type(err).__name__}: {err}") + if args.debug: traceback.print_exc() return [] @@ -614,8 +802,8 @@ def setup_and_run_single(fn_args: SetupAndRunSingleArgs) -> List[TestResult]: fn_args.args, ) except Exception as err: - print(f"{color_warn('[SKIP]')} {fn_args.fun_info.sig}") - print(color_warn(f"{type(err).__name__}: {err}")) + print(f"{yellow('[SKIP]')} {fn_args.fun_info.sig}") + error(f"{type(err).__name__}: {err}") if args.debug: traceback.print_exc() return [TestResult(fn_args.fun_info.sig, 2)] @@ -688,7 +876,8 @@ def run_parallel(run_args: RunArgs) -> List[TestResult]: ] # dispatch to the shared process pool - test_results = list(process_pool.map(setup_and_run_single, single_run_args)) + with ProcessPoolExecutor() as process_pool: + test_results = list(process_pool.map(setup_and_run_single, single_run_args)) test_results = sum(test_results, []) # flatten lists return test_results diff --git a/src/halmos/cheatcodes.py b/src/halmos/cheatcodes.py index b2f2aa41..a81e20f4 100644 --- a/src/halmos/cheatcodes.py +++ b/src/halmos/cheatcodes.py @@ -159,6 +159,6 @@ class console: # address constant CONSOLE_ADDRESS = address(0x000000000000000000636F6e736F6c652e6c6f67); address: BitVecRef = con_addr(0x000000000000000000636F6E736F6C652E6C6F67) - log_uint: int = 0xF5B1BBA9 # bytes4(keccak256("log(uint)")) + log_uint256: int = 0xF82C50F1 # bytes4(keccak256("log(uint256)")) log_string: int = 0x41304FAC # bytes4(keccak256("log(string)")) diff --git a/src/halmos/exceptions.py b/src/halmos/exceptions.py new file mode 100644 index 00000000..8e5dde08 --- /dev/null +++ b/src/halmos/exceptions.py @@ -0,0 +1,138 @@ +""" +Ethereum Virtual Machine (EVM) Exceptions +======================================== + +Exceptions thrown during EVM execution. + +Note: this is a modified version execution-specs' src/ethereum//vm/exceptions.pyd +""" + + +class EvmException(Exception): + """ + Base class for all EVM exceptions. + """ + + pass + + +class Revert(EvmException): + """ + Raised by the `REVERT` opcode. + + Unlike other EVM exceptions this does not result in the consumption of all gas. + """ + + pass + + +class ExceptionalHalt(EvmException): + """ + Indicates that the EVM has experienced an exceptional halt. This causes + execution to immediately end with all gas being consumed. + """ + + pass + + +class StackUnderflowError(ExceptionalHalt): + """ + Occurs when a pop is executed on an empty stack. + """ + + pass + + +class StackOverflowError(ExceptionalHalt): + """ + Occurs when a push is executed on a stack at max capacity. + """ + + pass + + +class OutOfGasError(ExceptionalHalt): + """ + Occurs when an operation costs more than the amount of gas left in the + frame. + """ + + pass + + +class InvalidOpcode(ExceptionalHalt): + """ + Raised when an invalid opcode is encountered. + """ + + pass + + +class InvalidJumpDestError(ExceptionalHalt): + """ + Occurs when the destination of a jump operation doesn't meet any of the + following criteria: + + * The jump destination is less than the length of the code. + * The jump destination should have the `JUMPDEST` opcode (0x5B). + * The jump destination shouldn't be part of the data corresponding to + `PUSH-N` opcodes. + """ + + +class MessageDepthLimitError(ExceptionalHalt): + """ + Raised when the message depth is greater than `1024` + """ + + pass + + +class WriteInStaticContext(ExceptionalHalt): + """ + Raised when an attempt is made to modify the state while operating inside + of a STATICCALL context. + """ + + pass + + +class OutOfBoundsRead(ExceptionalHalt): + """ + Raised when an attempt was made to read data beyond the + boundaries of the buffer. + """ + + pass + + +class InvalidParameter(ExceptionalHalt): + """ + Raised when invalid parameters are passed. + """ + + pass + + +class InvalidContractPrefix(ExceptionalHalt): + """ + Raised when the new contract code starts with 0xEF. + """ + + pass + + +class FailCheatcode(ExceptionalHalt): + """ + Raised when invoking hevm's vm.fail() cheatcode + """ + + pass + + +class AddressCollision(ExceptionalHalt): + """ + Raised when trying to deploy into a non-empty address + """ + + pass diff --git a/src/halmos/pools.py b/src/halmos/pools.py index e0983edf..12d1f44f 100644 --- a/src/halmos/pools.py +++ b/src/halmos/pools.py @@ -1,5 +1,5 @@ from concurrent.futures import ProcessPoolExecutor, ThreadPoolExecutor # defined as globals so that they can be imported from anywhere but instantiated only once -process_pool = ProcessPoolExecutor() -thread_pool = ThreadPoolExecutor() +# process_pool = ProcessPoolExecutor() +# thread_pool = ThreadPoolExecutor() diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py index 875de16b..95eaedf9 100644 --- a/src/halmos/sevm.py +++ b/src/halmos/sevm.py @@ -4,24 +4,27 @@ import math import re -from subprocess import Popen, PIPE - from copy import deepcopy from collections import defaultdict +from dataclasses import dataclass, field +from functools import reduce +from subprocess import Popen, PIPE from typing import ( + Any, + Dict, + Iterator, List, + Optional, Set, - Dict, - Union as UnionType, Tuple, - Any, - Optional, - TypeVar, Type, + TypeVar, + Union as UnionType, ) -from functools import reduce - from z3 import * + +from .cheatcodes import halmos_cheat_code, hevm_cheat_code, console, Prank +from .exceptions import * from .utils import ( EVM, sha3_inv, @@ -32,8 +35,8 @@ con_addr, bv_value_to_bytes, hexify, + color_info, ) -from .cheatcodes import halmos_cheat_code, hevm_cheat_code, console, Prank from .warnings import ( warn, UNSUPPORTED_OPCODE, @@ -49,6 +52,9 @@ Steps = Dict[int, Dict[str, Any]] # execution tree +EMPTY_BYTES = b"" +MAX_CALL_DEPTH = 1024 + # dynamic BitVecSort sizes class BitVecSortCache: @@ -133,14 +139,6 @@ def __getitem__(self, size: int) -> BitVecSort: new_address_offset: int = 1 -def id_str(x: Any) -> str: - return hexify(x).replace(" ", "") - - -def name_of(x: str) -> str: - return re.sub(r"\s+", "_", x) - - class Instruction: pc: int opcode: int @@ -157,7 +155,7 @@ def __str__(self) -> str: if self.operand is not None: operand = self.operand if isinstance(operand, bytes): - operand = con(int.from_bytes(self.operand, "big"), len(operand) * 8) + operand = con(int.from_bytes(operand, "big"), len(operand) * 8) expected_operand_length = instruction_length(self.opcode) - 1 actual_operand_length = operand.size() // 8 @@ -175,10 +173,33 @@ def __len__(self) -> int: return instruction_length(self.opcode) -class NotConcreteError(Exception): +class HalmosException(Exception): + pass + + +class NotConcreteError(HalmosException): pass +def id_str(x: Any) -> str: + return hexify(x).replace(" ", "") + + +def name_of(x: str) -> str: + return re.sub(r"\s+", "_", x) + + +def padded_slice(lst: List, start: int, size: int, default=0) -> List: + """ + Return a slice of lst, starting at start and with size elements. If the slice + is out of bounds, pad with default. + """ + + end = start + size + n = len(lst) + return [lst[i] if i < n else default for i in range(start, end)] + + def unbox_int(x: Any) -> Any: """Convert int-like objects to int""" if isinstance(x, bytes): @@ -350,7 +371,7 @@ def wstore_partial( return if not datasize >= offset + size: - raise ValueError(datasize, offset, size) + raise OutOfBoundsRead(datasize, offset, size) if is_bv(data): sub_data = Extract( @@ -469,6 +490,100 @@ def stringified_bytes_to_bytes(string_bytes: str): return BitVecVal(int.from_bytes(ret_bytes, "big"), ret_len * 8) +@dataclass(frozen=True) +class EventLog: + """ + Data record produced during the execution of a transaction. + """ + + address: Address + topics: List[Word] + data: Optional[Bytes] + + +@dataclass(frozen=True) +class Message: + target: Address + caller: Address + value: Word + data: List[Byte] + is_static: bool = False + call_scheme: int = EVM.CALL + gas: Optional[Word] = None + + def is_create(self) -> bool: + return self.call_scheme == EVM.CREATE or self.call_scheme == EVM.CREATE2 + + +@dataclass +class CallOutput: + """ + Data record produced during the execution of a call. + """ + + data: Optional[Bytes] = None + accounts_to_delete: Set[Address] = field(default_factory=set) + error: Optional[UnionType[EvmException, HalmosException]] = None + return_scheme: Optional[int] = None + + # TODO: + # - touched_accounts + # not modeled: + # - gas_refund + # - gas_left + + +TraceElement = UnionType["CallContext", EventLog] + + +@dataclass +class CallContext: + message: Message + output: CallOutput = field(default_factory=CallOutput) + depth: int = 1 + trace: List[TraceElement] = field(default_factory=list) + + def subcalls(self) -> Iterator["CallContext"]: + return iter(t for t in self.trace if isinstance(t, CallContext)) + + def last_subcall(self) -> Optional["CallContext"]: + """ + Returns the last subcall or None if there are no subcalls. + """ + + for c in reversed(self.trace): + if isinstance(c, CallContext): + return c + + return None + + def logs(self) -> Iterator[EventLog]: + return iter(t for t in self.trace if isinstance(t, EventLog)) + + def is_stuck(self) -> bool: + """ + When called after execution, this method returns True if the call is stuck, + i.e. it encountered an internal error and has no output. + + This is meaningless during execution, because the call may not yet have an output + """ + return self.output.data is None + + def get_stuck_reason(self) -> Optional[HalmosException]: + """ + Returns the first internal error encountered during the execution of the call. + """ + if isinstance(self.output.error, HalmosException): + return self.output.error + + if self.output.data is not None: + # if this context has output data (including empty bytes), it is not stuck + return None + + if (last_subcall := self.last_subcall()) is not None: + return last_subcall.get_stuck_reason() + + class State: stack: List[Word] memory: List[Byte] @@ -535,10 +650,7 @@ def mload(self) -> None: def ret(self) -> Bytes: loc: int = self.mloc() size: int = int_of(self.pop(), "symbolic return data size") # size in bytes - if size > 0: - return wload(self.memory, loc, size, prefer_concrete=True) - else: - return None + return wload(self.memory, loc, size, prefer_concrete=True) if size else b"" class Block: @@ -570,11 +682,18 @@ class Contract: # (typically a Concat() of concrete and symbolic values) _rawcode: UnionType[bytes, BitVecRef] - def __init__(self, rawcode: UnionType[bytes, BitVecRef]) -> None: + def __init__(self, rawcode: UnionType[bytes, BitVecRef, str]) -> None: + if rawcode is None: + raise HalmosException("invalid contract code: None") + if is_bv_value(rawcode): if rawcode.size() % 8 != 0: raise ValueError(rawcode) rawcode = rawcode.as_long().to_bytes(rawcode.size() // 8, "big") + + if isinstance(rawcode, str): + rawcode = bytes.fromhex(rawcode) + self._rawcode = rawcode def __init_jumpdests(self): @@ -638,7 +757,9 @@ def __getslice__(self, slice): return extracted # concrete - return self._rawcode[slice.start : slice.stop] + size = slice.stop - slice.start + data = padded_slice(self._rawcode, slice.start, size, default=0) + return bytes(data) def __getitem__(self, key) -> UnionType[int, BitVecRef]: """Returns the byte at the given offset.""" @@ -702,34 +823,34 @@ class Exec: # an execution path code: Dict[Address, Contract] storage: Dict[Address, Dict[int, Any]] # address -> { storage slot -> value } balance: Any # address -> balance + # block block: Block + # tx - calldata: List[Byte] # msg.data - callvalue: Word # msg.value - caller: Address # msg.sender - this: Address # current account address + context: CallContext + # vm state + this: Address # current account address pgm: Contract pc: int st: State # stack and memory jumpis: Dict[str, Dict[bool, int]] # for loop detection - output: Any # returndata symbolic: bool # symbolic or concrete storage prank: Prank + addresses_to_delete: Set[Address] + # path solver: Solver path: List[Any] # path conditions alias: Dict[Address, Address] # address aliases - # logs - log: List[Tuple[List[Word], Any]] # event logs emitted + + # internal bookkeeping cnts: Dict[str, Dict[int, int]] # opcode -> frequency; counters sha3s: Dict[Word, int] # sha3 hashes generated storages: Dict[Any, Any] # storage updates balances: Dict[Any, Any] # balance updates calls: List[Any] # external calls - failed: bool - error: str def __init__(self, **kwargs) -> None: self.code = kwargs["code"] @@ -737,36 +858,64 @@ def __init__(self, **kwargs) -> None: self.balance = kwargs["balance"] # self.block = kwargs["block"] + self.context = kwargs["context"] # - self.calldata = kwargs["calldata"] - self.callvalue = kwargs["callvalue"] - self.caller = kwargs["caller"] self.this = kwargs["this"] - # self.pgm = kwargs["pgm"] self.pc = kwargs["pc"] self.st = kwargs["st"] self.jumpis = kwargs["jumpis"] - self.output = kwargs["output"] self.symbolic = kwargs["symbolic"] self.prank = kwargs["prank"] + self.addresses_to_delete = kwargs.get("addresses_to_delete") or set() # self.solver = kwargs["solver"] self.path = kwargs["path"] self.alias = kwargs["alias"] # - self.log = kwargs["log"] self.cnts = kwargs["cnts"] self.sha3s = kwargs["sha3s"] self.storages = kwargs["storages"] self.balances = kwargs["balances"] self.calls = kwargs["calls"] - self.failed = kwargs["failed"] - self.error = kwargs["error"] - assert_address(self.caller) + assert_address(self.context.message.target) + assert_address(self.context.message.caller) assert_address(self.this) + def context_str(self) -> str: + opcode = self.current_opcode() + return f"addr={hexify(self.this)} pc={self.pc} insn={mnemonic(opcode)}" + + def halt( + self, + data: Bytes = EMPTY_BYTES, + error: Optional[EvmException] = None, + ) -> None: + output = self.context.output + if output.data is not None: + raise HalmosException("output already set") + + output.data = data + output.error = error + output.return_scheme = self.current_opcode() + + def emit_log(self, log: EventLog): + self.context.trace.append(log) + + def calldata(self) -> List[Byte]: + message = self.message() + return [] if message.is_create() else message.data + + def caller(self): + return self.message().caller + + def callvalue(self): + return self.message().value + + def message(self): + return self.context.message + def current_opcode(self) -> UnionType[int, BitVecRef]: return unbox_int(self.pgm[self.pc]) @@ -793,6 +942,7 @@ def str_path(self) -> str: ) def __str__(self) -> str: + output = self.context.output.data return hexify( "".join( [ @@ -806,14 +956,10 @@ def __str__(self) -> str: self.storage, ) ), - # f"Solver:\n{self.str_solver()}\n", f"Path:\n{self.str_path()}", f"Aliases:\n", "".join([f"- {k}: {v}\n" for k, v in self.alias.items()]), - f"Output: {self.output.hex() if isinstance(self.output, bytes) else self.output}\n", - f"Log: {self.log}\n", - # f"Opcodes:\n{self.str_cnts()}", - # f"Memsize: {len(self.st.memory)}\n", + f"Output: {output.hex() if isinstance(output, bytes) else output}\n", f"Balance updates:\n", "".join( map( @@ -832,7 +978,6 @@ def __str__(self) -> str: "".join(map(lambda x: f"- {self.sha3s[x]}: {x}\n", self.sha3s)), f"External calls:\n", "".join(map(lambda x: f"- {x}\n", self.calls)), - # f"Calldata: {self.calldata}\n", ] ) ) @@ -944,8 +1089,25 @@ def new_symbol_id(self) -> int: self.cnts["fresh"]["symbol"] += 1 return self.cnts["fresh"]["symbol"] + def returndata(self) -> Optional[Bytes]: + """ + Return data from the last executed sub-context or the empty bytes sequence + """ + + last_subcall = self.context.last_subcall() + + if not last_subcall: + return EMPTY_BYTES + + output = last_subcall.output + if last_subcall.message.is_create() and not output.error: + return EMPTY_BYTES + + return output.data + def returndatasize(self) -> int: - return 0 if self.output is None else byte_length(self.output) + returndata = self.returndata() + return byte_length(returndata) if returndata is not None else 0 def is_jumpdest(self, x: Word) -> bool: if not is_concrete(x): @@ -1272,7 +1434,7 @@ def is_power_of_two(x: int) -> bool: return False -class Logs: +class HalmosLogs: bounded_loops: List[str] unknown_calls: Dict[str, Dict[str, Set[str]]] # funsig -> to -> set(arg) @@ -1280,7 +1442,7 @@ def __init__(self) -> None: self.bounded_loops = [] self.unknown_calls = defaultdict(lambda: defaultdict(set)) - def extend(self, logs) -> None: + def extend(self, logs: "HalmosLogs") -> None: self.bounded_loops.extend(logs.bounded_loops) for funsig in logs.unknown_calls: for to in logs.unknown_calls[funsig]: @@ -1291,12 +1453,12 @@ def add_uninterpreted_unknown_call(self, funsig, to, arg): self.unknown_calls[funsig][to].add(arg) def print_unknown_calls(self): - for funsig in logs.unknown_calls: + for funsig in self.unknown_calls: print(f"{funsig}:") - for to in logs.unknown_calls[funsig]: + for to in self.unknown_calls[funsig]: print(f"- {to}:") print( - "\n".join([f" - {arg}" for arg in logs.unknown_calls[funsig][to]]) + "\n".join([f" - {arg}" for arg in self.unknown_calls[funsig][to]]) ) @@ -1513,6 +1675,9 @@ def sload(self, ex: Exec, addr: Any, loc: Word) -> Word: return self.storage_model.load(ex, addr, loc) def sstore(self, ex: Exec, addr: Any, loc: Any, val: Any) -> None: + if ex.message().is_static: + raise WriteInStaticContext(ex.context_str()) + if is_bool(val): val = If(val, con(1), con(0)) @@ -1567,21 +1732,16 @@ def call( stack: List[Tuple[Exec, int]], step_id: int, out: List[Exec], - logs: Logs, + logs: HalmosLogs, ) -> None: gas = ex.st.pop() - to = uint160(ex.st.pop()) + fund = con(0) if op in [EVM.STATICCALL, EVM.DELEGATECALL] else ex.st.pop() - if op == EVM.STATICCALL or op == EVM.DELEGATECALL: - fund = con(0) - else: - fund = ex.st.pop() arg_loc: int = ex.st.mloc() - # size (in bytes) arg_size: int = int_of(ex.st.pop(), "symbolic CALL input data size") + ret_loc: int = ex.st.mloc() - # size (in bytes) ret_size: int = int_of(ex.st.pop(), "symbolic CALL return data size") if not arg_size >= 0: @@ -1590,12 +1750,12 @@ def call( raise ValueError(ret_size) arg = wload(ex.st.memory, arg_loc, arg_size) if arg_size > 0 else None - caller = ex.prank.lookup(ex.this, to) def send_callvalue(condition=None) -> None: # no balance update for CALLCODE which transfers to itself if op == EVM.CALL: + # TODO: revert if context is static self.transfer_value(ex, caller, to, fund, condition) def call_known(to: Address) -> None: @@ -1603,7 +1763,6 @@ def call_known(to: Address) -> None: orig_code = ex.code.copy() orig_storage = deepcopy(ex.storage) orig_balance = ex.balance - orig_log = ex.log.copy() # transfer msg.value send_callvalue() @@ -1615,6 +1774,17 @@ def call_known(to: Address) -> None: calldata, 0, arg_size, ex.st.memory[arg_loc : arg_loc + arg_size] ) + message = Message( + target=to if op in [EVM.CALL, EVM.STATICCALL] else ex.this, + caller=caller if op != EVM.DELEGATECALL else ex.caller(), + value=fund if op != EVM.DELEGATECALL else ex.callvalue(), + data=calldata, + is_static=(ex.context.message.is_static or op == EVM.STATICCALL), + call_scheme=op, + ) + + # TODO: check max call depth + # execute external calls (new_exs, new_steps, new_logs) = self.run( Exec( @@ -1624,16 +1794,13 @@ def call_known(to: Address) -> None: # block=ex.block, # - calldata=calldata, - callvalue=fund if op != EVM.DELEGATECALL else ex.callvalue, - caller=caller if op != EVM.DELEGATECALL else ex.caller, - this=to if op in [EVM.CALL, EVM.STATICCALL] else ex.this, + context=CallContext(message=message, depth=ex.context.depth + 1), + this=message.target, # pgm=ex.code[to], pc=0, st=State(), jumpis={}, - output=None, symbolic=ex.symbolic, prank=Prank(), # @@ -1641,35 +1808,38 @@ def call_known(to: Address) -> None: path=ex.path, alias=ex.alias, # - log=ex.log, cnts=ex.cnts, sha3s=ex.sha3s, storages=ex.storages, balances=ex.balances, calls=ex.calls, - failed=ex.failed, - error=ex.error, ) ) logs.extend(new_logs) # process result - for idx, new_ex in enumerate(new_exs): - opcode = new_ex.current_opcode() - - # restore tx msg - new_ex.calldata = ex.calldata - new_ex.callvalue = ex.callvalue - new_ex.caller = ex.caller + for new_ex in new_exs: + # continue execution in the context of the parent + # pessimistic copy because the subcall results may diverge + subcall = new_ex.context + + # restore context + new_ex.context = deepcopy(ex.context) + new_ex.context.trace.append(subcall) new_ex.this = ex.this + if subcall.is_stuck(): + # internal errors abort the current path, + # so we don't need to add it to the worklist + out.append(new_ex) + continue + # restore vm state new_ex.pgm = ex.pgm new_ex.pc = ex.pc new_ex.st = deepcopy(ex.st) new_ex.jumpis = deepcopy(ex.jumpis) - # new_ex.output is passed into the caller new_ex.symbolic = ex.symbolic new_ex.prank = deepcopy(ex.prank) @@ -1680,30 +1850,23 @@ def call_known(to: Address) -> None: ret_loc, 0, min(ret_size, actual_ret_size), - new_ex.output, + subcall.output.data, actual_ret_size, ) - # set status code (in stack) - if opcode in [EVM.STOP, EVM.RETURN, EVM.REVERT, EVM.INVALID]: - if opcode in [EVM.STOP, EVM.RETURN]: - new_ex.st.push(con(1)) - else: - new_ex.st.push(con(0)) + # set status code on the stack + subcall_success = subcall.output.error is None + new_ex.st.push(con(1) if subcall_success else con(0)) - # revert network states - new_ex.code = orig_code - new_ex.storage = orig_storage - new_ex.balance = orig_balance - new_ex.log = orig_log + if not subcall_success: + # revert network states + new_ex.code = orig_code + new_ex.storage = orig_storage + new_ex.balance = orig_balance - # add to worklist even if it reverted during the external call - new_ex.next_pc() - stack.append((new_ex, step_id)) - else: - # got stuck during external call - new_ex.error = f"External call encountered an issue at {mnemonic(opcode)}: {new_ex.error}" - out.append(new_ex) + # add to worklist even if it reverted during the external call + new_ex.next_pc() + stack.append((new_ex, step_id)) def call_unknown() -> None: call_id = len(ex.calls) @@ -1774,6 +1937,9 @@ def call_unknown() -> None: extract_funsig(arg), "symbolic halmos cheatcode function selector" ) + if self.options.get("debug"): + print(f"Executing halmos cheat code: {hex(funsig)}") + # createUint(uint256,string) returns (uint256) if funsig == halmos_cheat_code.create_uint: bit_size = int_of( @@ -1785,9 +1951,7 @@ def call_unknown() -> None: label = f"halmos_{name}_uint{bit_size}_{ex.new_symbol_id():>02}" ret = uint256(BitVec(label, BitVecSorts[bit_size])) else: - ex.error = f"bitsize larger than 256: {bit_size}" - out.append(ex) - return + raise HalmosException(f"bitsize larger than 256: {bit_size}") # createBytes(uint256,string) returns (bytes) elif funsig == halmos_cheat_code.create_bytes: @@ -1825,9 +1989,8 @@ def call_unknown() -> None: ret = uint256(BitVec(label, BitVecSort1)) else: - ex.error = f"Unknown halmos cheat code: function selector = 0x{funsig:0>8x}, calldata = {hexify(arg)}" - out.append(ex) - return + error_msg = f"Unknown halmos cheat code: function selector = 0x{funsig:0>8x}, calldata = {hexify(arg)}" + raise HalmosException(error_msg) # vm cheat code if eq(to, hevm_cheat_code.address): @@ -1835,9 +1998,8 @@ def call_unknown() -> None: # vm.fail() # BitVecVal(hevm_cheat_code.fail_payload, 800) if arg == hevm_cheat_code.fail_payload: - ex.failed = True - out.append(ex) - return + raise FailCheatcode() + # vm.assume(bool) elif ( eq(arg.sort(), BitVecSorts[(4 + 32) * 8]) @@ -1846,6 +2008,7 @@ def call_unknown() -> None: assume_cond = simplify(is_non_zero(Extract(255, 0, arg))) ex.solver.add(assume_cond) ex.path.append(str(assume_cond)) + # vm.getCode(string) elif ( simplify(Extract(arg_size * 8 - 1, arg_size * 8 - 32, arg)) @@ -1878,9 +2041,8 @@ def call_unknown() -> None: ): result = ex.prank.prank(uint160(Extract(255, 0, arg))) if not result: - ex.error = "You have an active prank already." - out.append(ex) - return + raise HalmosException("You have an active prank already.") + # vm.startPrank(address) elif ( eq(arg.sort(), BitVecSorts[(4 + 32) * 8]) @@ -1889,9 +2051,8 @@ def call_unknown() -> None: ): result = ex.prank.startPrank(uint160(Extract(255, 0, arg))) if not result: - ex.error = "You have an active prank already." - out.append(ex) - return + raise HalmosException("You have an active prank already.") + # vm.stopPrank() elif ( eq(arg.sort(), BitVecSorts[4 * 8]) @@ -1918,9 +2079,8 @@ def call_unknown() -> None: if store_account_addr is not None: self.sstore(ex, store_account_addr, store_slot, store_value) else: - ex.error = f"uninitialized account: {store_account}" - out.append(ex) - return + raise HalmosException(f"uninitialized account: {store_account}") + # vm.load(address,bytes32) elif ( eq(arg.sort(), BitVecSorts[(4 + 32 * 2) * 8]) @@ -1932,9 +2092,8 @@ def call_unknown() -> None: if load_account_addr is not None: ret = self.sload(ex, load_account_addr, load_slot) else: - ex.error = f"uninitialized account: {load_account}" - out.append(ex) - return + raise HalmosException(f"uninitialized account: {store_account}") + # vm.fee(uint256) elif ( eq(arg.sort(), BitVecSorts[(4 + 32) * 8]) @@ -1978,9 +2137,8 @@ def call_unknown() -> None: # who must be concrete if not is_bv_value(who): - ex.error = f"vm.etch(address who, bytes code) must have concrete argument `who` but received {who}" - out.append(ex) - return + error_msg = f"vm.etch(address who, bytes code) must have concrete argument `who` but received {who}" + raise HalmosException(error_msg) # code must be concrete try: @@ -1993,18 +2151,15 @@ def call_unknown() -> None: ex.code[who] = Contract(code_bytes) except Exception as e: - ex.error = f"vm.etch(address who, bytes code) must have concrete argument `code` but received calldata {arg}" - out.append(ex) - return + error_msg = f"vm.etch(address who, bytes code) must have concrete argument `code` but received calldata {arg}" + raise HalmosException(error_msg) from e # ffi(string[]) returns (bytes) elif extract_funsig(arg) == hevm_cheat_code.ffi_sig: if not self.options.get("ffi"): - ex.error = "ffi cheatcode is disabled. Run again with `--ffi` if you want to enable it" - out.append(ex) - return - process = Popen( - extract_string_array_argument(arg, 0), stdout=PIPE, stderr=PIPE - ) + error_msg = "ffi cheatcode is disabled. Run again with `--ffi` if you want to enable it" + raise HalmosException(error_msg) + cmd = extract_string_array_argument(arg, 0) + process = Popen(cmd, stdout=PIPE, stderr=PIPE) (stdout, stderr) = process.communicate() @@ -2025,9 +2180,8 @@ def call_unknown() -> None: else: # TODO: support other cheat codes - ex.error = f"Unsupported cheat code: calldata = {hexify(arg)}" - out.append(ex) - return + msg = f"Unsupported cheat code: calldata = {hexify(arg)}" + raise HalmosException(msg) # console if eq(to, console.address): @@ -2037,25 +2191,43 @@ def call_unknown() -> None: extract_funsig(arg), "symbolic console function selector" ) - if funsig == console.log_uint: + if funsig == console.log_uint256: print(extract_bytes(arg, 4, 32)) # elif funsig == console.log_string: else: # TODO: support other console functions - ex.error = f"Unsupported console function: function selector = 0x{funsig:0>8x}, calldata = {hexify(arg)}" - out.append(ex) - return + print( + color_info( + f"Unsupported console function: selector = 0x{funsig:0>8x}, " + f"calldata = {hexify(arg)}" + ) + ) # store return value if ret_size > 0: wstore(ex.st.memory, ret_loc, ret_size, ret) - # propagate callee's output to caller, which could be None - ex.output = ret + ex.context.trace.append( + CallContext( + message=Message( + target=to, + caller=caller, + value=fund, + data=ex.st.memory[arg_loc : arg_loc + arg_size], + call_scheme=op, + ), + output=CallOutput( + data=ret, + error=None, + ), + depth=ex.context.depth + 1, + ) + ) - ex.calls.append((exit_code_var, exit_code, ex.output)) + # TODO: check if still needed + ex.calls.append((exit_code_var, exit_code, ex.context.output.data)) ex.next_pc() stack.append((ex, step_id)) @@ -2091,8 +2263,10 @@ def call_unknown() -> None: call_unknown() return - ex.error = f"Unknown contract call: to = {hexify(to)}; calldata = {hexify(arg)}; callvalue = {hexify(fund)}" - out.append(ex) + raise HalmosException( + f"Unknown contract call: to = {hexify(to)}; " + f"calldata = {hexify(arg)}; callvalue = {hexify(fund)}" + ) def create( self, @@ -2101,8 +2275,11 @@ def create( stack: List[Tuple[Exec, int]], step_id: int, out: List[Exec], - logs: Logs, + logs: HalmosLogs, ) -> None: + if ex.message().is_static: + raise WriteInStaticContext(ex.context_str()) + value: Word = ex.st.pop() loc: int = int_of(ex.st.pop(), "symbolic CREATE offset") size: int = int_of(ex.st.pop(), "symbolic CREATE size") @@ -2120,7 +2297,7 @@ def create( # new account address if op == EVM.CREATE: new_addr = ex.new_address() - else: # EVM.CREATE2 + elif op == EVM.CREATE2: # EVM.CREATE2 if isinstance(create_hexcode, bytes): create_hexcode = con( int.from_bytes(create_hexcode, "big"), len(create_hexcode) * 8 @@ -2128,15 +2305,40 @@ def create( code_hash = ex.sha3_data(create_hexcode, create_hexcode.size() // 8) hash_data = simplify(Concat(con(0xFF, 8), caller, salt, code_hash)) new_addr = uint160(ex.sha3_data(hash_data, 85)) + else: + raise HalmosException(f"Unknown CREATE opcode: {op}") + + message = Message( + target=new_addr, + caller=caller, + value=value, + data=create_hexcode, + is_static=False, + call_scheme=op, + ) if new_addr in ex.code: - ex.error = f"existing address: {hexify(new_addr)}" - out.append(ex) + # address conflicts don't revert, they push 0 on the stack and continue + ex.st.push(con(0)) + ex.next_pc() + + # add a virtual subcontext to the trace for debugging purposes + subcall = CallContext(message=message, depth=ex.context.depth + 1) + subcall.output.data = b"" + subcall.output.error = AddressCollision() + ex.context.trace.append(subcall) + + stack.append((ex, step_id)) return for addr in ex.code: ex.solver.add(new_addr != addr) # ensure new address is fresh + # backup current state + orig_code = ex.code.copy() + orig_storage = deepcopy(ex.storage) + orig_balance = ex.balance + # setup new account ex.code[new_addr] = Contract(b"") # existing code must be empty ex.storage[new_addr] = {} # existing storage may not be empty and reset here @@ -2153,16 +2355,13 @@ def create( # block=ex.block, # - calldata=[], - callvalue=value, - caller=caller, + context=CallContext(message=message, depth=ex.context.depth + 1), this=new_addr, # pgm=create_code, pc=0, st=State(), jumpis={}, - output=None, symbolic=False, prank=Prank(), # @@ -2170,61 +2369,66 @@ def create( path=ex.path, alias=ex.alias, # - log=ex.log, cnts=ex.cnts, sha3s=ex.sha3s, storages=ex.storages, balances=ex.balances, calls=ex.calls, - failed=ex.failed, - error=ex.error, ) ) logs.extend(new_logs) # process result - for idx, new_ex in enumerate(new_exs): - # sanity checks - if new_ex.failed: - raise ValueError(new_ex) - - opcode = new_ex.current_opcode() - if opcode in [EVM.STOP, EVM.RETURN]: - # new contract code - new_ex.code[new_addr] = Contract(new_ex.output) - - # restore tx msg - new_ex.calldata = ex.calldata - new_ex.callvalue = ex.callvalue - new_ex.caller = ex.caller - new_ex.this = ex.this + for new_ex in new_exs: + subcall = new_ex.context + + # continue execution in the context of the parent + # pessimistic copy because the subcall results may diverge + new_ex.context = deepcopy(ex.context) + new_ex.context.trace.append(subcall) + + new_ex.this = ex.this + + # restore vm state + new_ex.pgm = ex.pgm + new_ex.pc = ex.pc + new_ex.st = deepcopy(ex.st) + new_ex.jumpis = deepcopy(ex.jumpis) + new_ex.symbolic = ex.symbolic + new_ex.prank = deepcopy(ex.prank) + + if subcall.is_stuck(): + # internal errors abort the current path, + out.append(new_ex) + continue - # restore vm state - new_ex.pgm = ex.pgm - new_ex.pc = ex.pc - new_ex.st = deepcopy(ex.st) - new_ex.jumpis = deepcopy(ex.jumpis) - new_ex.output = None # output is reset, not restored - new_ex.symbolic = ex.symbolic - new_ex.prank = deepcopy(ex.prank) + elif subcall.output.error is None: + # new contract code, will revert if data is None + new_ex.code[new_addr] = Contract(subcall.output.data) # push new address to stack new_ex.st.push(uint256(new_addr)) - # add to worklist - new_ex.next_pc() - stack.append((new_ex, step_id)) else: # creation failed - out.append(new_ex) + new_ex.st.push(con(0)) + + # revert network states + new_ex.code = orig_code + new_ex.storage = orig_storage + new_ex.balance = orig_balance + + # add to worklist + new_ex.next_pc() + stack.append((new_ex, step_id)) def jumpi( self, ex: Exec, stack: List[Tuple[Exec, int]], step_id: int, - logs: Logs, + logs: HalmosLogs, ) -> None: jid = ex.jumpi_id() @@ -2324,16 +2528,13 @@ def create_branch(self, ex: Exec, cond: BitVecRef, target: int) -> Exec: # block=deepcopy(ex.block), # - calldata=ex.calldata, - callvalue=ex.callvalue, - caller=ex.caller, + context=deepcopy(ex.context), this=ex.this, # pgm=ex.pgm, pc=target, st=deepcopy(ex.st), jumpis=deepcopy(ex.jumpis), - output=ex.output, symbolic=ex.symbolic, prank=deepcopy(ex.prank), # @@ -2341,14 +2542,11 @@ def create_branch(self, ex: Exec, cond: BitVecRef, target: int) -> Exec: path=new_path, alias=ex.alias.copy(), # - log=ex.log.copy(), cnts=deepcopy(ex.cnts), sha3s=ex.sha3s.copy(), storages=ex.storages.copy(), balances=ex.balances.copy(), calls=ex.calls.copy(), - failed=ex.failed, - error=ex.error, ) return new_ex @@ -2368,24 +2566,24 @@ def gen_nested_ite(curr: int) -> BitVecRef: # If(idx == 0, Extract(255, 248, w), If(idx == 1, Extract(247, 240, w), ..., If(idx == 31, Extract(7, 0, w), 0)...)) return ZeroExt(248, gen_nested_ite(0)) - def run(self, ex0: Exec) -> Tuple[List[Exec], Steps]: + def run(self, ex0: Exec) -> Tuple[List[Exec], Steps, HalmosLogs]: out: List[Exec] = [] - logs = Logs() + logs = HalmosLogs() steps: Steps = {} step_id: int = 0 stack: List[Tuple[Exec, int]] = [(ex0, 0)] while stack: try: - if ( - "max_width" in self.options - and len(out) >= self.options["max_width"] - ): + if len(out) >= self.options.get("max_width", 2**64): break (ex, prev_step_id) = stack.pop() step_id += 1 + if ex.context.depth > MAX_CALL_DEPTH: + raise MessageDepthLimitError(ex.context) + insn = ex.current_instruction() opcode = insn.opcode ex.cnts["opcode"][opcode] += 1 @@ -2409,22 +2607,22 @@ def run(self, ex0: Exec) -> Tuple[List[Exec], Steps]: print(ex) if opcode == EVM.STOP: - ex.output = None + ex.halt() out.append(ex) continue elif opcode == EVM.INVALID: - ex.output = None + ex.halt(error=InvalidOpcode(opcode)) out.append(ex) continue elif opcode == EVM.REVERT: - ex.output = ex.st.ret() + ex.halt(data=ex.st.ret(), error=Revert()) out.append(ex) continue elif opcode == EVM.RETURN: - ex.output = ex.st.ret() + ex.halt(data=ex.st.ret()) out.append(ex) continue @@ -2507,28 +2705,25 @@ def run(self, ex0: Exec) -> Tuple[List[Exec], Steps]: ex.st.push(SignExt(256 - bl, Extract(bl - 1, 0, ex.st.pop()))) elif opcode == EVM.CALLDATALOAD: - if ex.calldata is None: + calldata = ex.calldata() + if calldata is None: ex.st.push(f_calldataload(ex.st.pop())) else: - offset: int = int_of( - ex.st.pop(), "symbolic CALLDATALOAD offset" - ) - ex.st.push( - Concat( - (ex.calldata + [BitVecVal(0, 8)] * 32)[ - offset : offset + 32 - ] - ) - ) + err_msg = "symbolic CALLDATALOAD offset" + offset: int = int_of(ex.st.pop(), err_msg) + data = padded_slice(calldata, offset, 32, default=con(0, 8)) + ex.st.push(Concat(data)) + elif opcode == EVM.CALLDATASIZE: - if ex.calldata is None: - ex.st.push(f_calldatasize()) - else: - ex.st.push(con(len(ex.calldata))) + cd = ex.calldata() + + # TODO: is optional calldata necessary? + ex.st.push(f_calldatasize() if cd is None else con(len(cd))) + elif opcode == EVM.CALLVALUE: - ex.st.push(ex.callvalue) + ex.st.push(ex.callvalue()) elif opcode == EVM.CALLER: - ex.st.push(uint256(ex.caller)) + ex.st.push(uint256(ex.caller())) elif opcode == EVM.ORIGIN: ex.st.push(uint256(f_origin())) elif opcode == EVM.ADDRESS: @@ -2552,10 +2747,11 @@ def run(self, ex0: Exec) -> Tuple[List[Exec], Steps]: elif opcode == EVM.EXTCODEHASH: account = uint160(ex.st.pop()) account_addr = self.resolve_address_alias(ex, account) - if account_addr is not None: - codehash = f_extcodehash(account_addr) - else: - codehash = f_extcodehash(account) + codehash = ( + f_extcodehash(account_addr) + if account_addr is not None + else f_extcodehash(account) + ) ex.st.push(codehash) elif opcode == EVM.CODESIZE: ex.st.push(con(len(ex.pgm))) @@ -2633,8 +2829,15 @@ def run(self, ex0: Exec) -> Tuple[List[Exec], Steps]: offset: int = int_of(ex.st.pop(), "symbolic RETURNDATACOPY offset") # size (in bytes) size: int = int_of(ex.st.pop(), "symbolic RETURNDATACOPY size") + + # TODO: do we need to pass returndatasize here? wstore_partial( - ex.st.memory, loc, offset, size, ex.output, ex.returndatasize() + ex.st.memory, + loc, + offset, + size, + ex.returndata(), + ex.returndatasize(), ) elif opcode == EVM.CALLDATACOPY: @@ -2643,7 +2846,8 @@ def run(self, ex0: Exec) -> Tuple[List[Exec], Steps]: # size (in bytes) size: int = int_of(ex.st.pop(), "symbolic CALLDATACOPY size") if size > 0: - if ex.calldata is None: + calldata = ex.message().data + if calldata is None: f_calldatacopy = Function( "calldatacopy_" + str(size * 8), BitVecSort256, @@ -2652,23 +2856,8 @@ def run(self, ex0: Exec) -> Tuple[List[Exec], Steps]: data = f_calldatacopy(offset) wstore(ex.st.memory, loc, size, data) else: - if offset + size <= len(ex.calldata): - wstore_bytes( - ex.st.memory, - loc, - size, - ex.calldata[offset : offset + size], - ) - elif offset == len(ex.calldata): - # copy zero bytes - wstore_bytes( - ex.st.memory, - loc, - size, - [con(0, 8) for _ in range(size)], - ) - else: - raise ValueError(offset, size, len(ex.calldata)) + data = padded_slice(calldata, offset, size, con(0, 8)) + wstore_bytes(ex.st.memory, loc, size, data) elif opcode == EVM.CODECOPY: loc: int = ex.st.mloc() @@ -2678,6 +2867,13 @@ def run(self, ex0: Exec) -> Tuple[List[Exec], Steps]: wextend(ex.st.memory, loc, size) codeslice = ex.pgm[offset : offset + size] + + actual_size = byte_length(codeslice) + if actual_size != size: + raise HalmosException( + f"CODECOPY: expected {size} bytes but got {actual_size}" + ) + ex.st.memory[loc : loc + size] = iter_bytes(codeslice) elif opcode == EVM.BYTE: @@ -2703,16 +2899,16 @@ def run(self, ex0: Exec) -> Tuple[List[Exec], Steps]: ex.st.push(self.sym_byte_of(idx, w)) elif EVM.LOG0 <= opcode <= EVM.LOG4: - num_keys: int = opcode - EVM.LOG0 + if ex.message().is_static: + raise WriteInStaticContext(ex.context_str()) + + num_topics: int = opcode - EVM.LOG0 loc: int = ex.st.mloc() - # size (in bytes) size: int = int_of(ex.st.pop(), "symbolic LOG data size") - keys = [] - for _ in range(num_keys): - keys.append(ex.st.pop()) - ex.log.append( - (keys, wload(ex.st.memory, loc, size) if size > 0 else None) - ) + topics = list(ex.st.pop() for _ in range(num_topics)) + data = wload(ex.st.memory, loc, size) if size > 0 else None + + ex.emit_log(EventLog(ex.this, topics, data)) elif opcode == EVM.PUSH0: ex.st.push(con(0)) @@ -2736,25 +2932,24 @@ def run(self, ex0: Exec) -> Tuple[List[Exec], Steps]: ex.st.swap(opcode - EVM.SWAP1 + 1) else: - warn( - UNSUPPORTED_OPCODE, - f"Unsupported opcode {hex(opcode)} ({str_opcode.get(opcode, '?')})", - ) - out.append(ex) - continue + # TODO: switch to InvalidOpcode when we have full opcode coverage + # this halts the path, but we should only halt the current context + raise HalmosException(f"Unsupported opcode {hex(opcode)}") ex.next_pc() stack.append((ex, step_id)) - except NotConcreteError as err: - ex.error = f"{err}" + except EvmException as err: + ex.halt(error=err) out.append(ex) continue - except Exception as err: + except HalmosException as err: if self.options["debug"]: - print(ex) - raise + print(err) + ex.halt(data=None, error=err) + out.append(ex) + continue return (out, steps, logs) @@ -2767,31 +2962,13 @@ def mk_exec( # block, # - calldata, - callvalue, - caller, + context: CallContext, + # this, # pgm, - # pc, - # st, - # jumpis, - # output, symbolic, - # prank, - # solver, - # path, - # alias, - # - # log, - # cnts, - # sha3s, - # storages, - # balances, - # calls, - # failed, - # error, ) -> Exec: return Exec( code=code, @@ -2800,16 +2977,13 @@ def mk_exec( # block=block, # - calldata=calldata, - callvalue=callvalue, - caller=caller, - this=this, + context=context, # + this=this, pgm=pgm, pc=0, st=State(), jumpis={}, - output=None, symbolic=symbolic, prank=Prank(), # @@ -2823,6 +2997,4 @@ def mk_exec( storages={}, balances={}, calls=[], - failed=False, - error="", ) diff --git a/src/halmos/utils.py b/src/halmos/utils.py index a926ee94..d41ea33c 100644 --- a/src/halmos/utils.py +++ b/src/halmos/utils.py @@ -47,12 +47,52 @@ def con_addr(n: int) -> BitVecRef: return BitVecVal(n, 160) +def green(text: str) -> str: + return f"\033[32m{text}\033[0m" + + +def red(text: str) -> str: + return f"\033[31m{text}\033[0m" + + +def yellow(text: str) -> str: + return f"\033[33m{text}\033[0m" + + +def cyan(text: str) -> str: + return f"\033[36m{text}\033[0m" + + def color_good(text: str) -> str: - return "\033[32m" + text + "\033[0m" + return green(text) + + +def color_error(text: str) -> str: + return red(text) def color_warn(text: str) -> str: - return "\033[31m" + text + "\033[0m" + return red(text) + + +def color_info(text: str) -> str: + return cyan(text) + + +def error(text: str) -> None: + print(color_error(text)) + + +def warn(text: str) -> None: + print(color_warn(text)) + + +def info(text: str) -> None: + print(color_info(text)) + + +def indent_text(text: str, n: int = 4) -> str: + return "\n".join(" " * n + line for line in text.splitlines()) class EVM: diff --git a/tests/expected/all.json b/tests/expected/all.json index 225f9682..64acca97 100644 --- a/tests/expected/all.json +++ b/tests/expected/all.json @@ -41,20 +41,20 @@ "num_bounded_loops": null } ], - "test/AssertTest.sol:CTest": [ + "test/AssertTest.t.sol:AssertTest": [ { - "name": "check_bar()", - "exitcode": 1, - "num_models": 1, + "name": "check_assert_not_propagated()", + "exitcode": 0, + "num_models": 0, "models": null, "num_paths": null, "time": null, "num_bounded_loops": null }, { - "name": "check_foo()", - "exitcode": 0, - "num_models": 0, + "name": "check_fail_propagated()", + "exitcode": 1, + "num_models": 1, "models": null, "num_paths": null, "time": null, @@ -117,6 +117,44 @@ "num_bounded_loops": null } ], + "test/Buffers.t.sol:BuffersTest": [ + { + "name": "check_calldatacopy_large_offset()", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_calldataload_large_offset()", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_codecopy_large_offset()", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_codecopy_offset_across_boundary()", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], "test/Byte.t.sol:ByteTest": [ { "name": "check_byte(uint256,uint256)", @@ -286,6 +324,98 @@ "num_bounded_loops": null } ], + "test/Context.t.sol:ContextTest": [ + { + "name": "check_call0_fail()", + "exitcode": 1, + "num_models": 1, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_call0_halmos_exception()", + "exitcode": 1, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_call0_normal(uint256)", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_call1_fail(uint256)", + "exitcode": 1, + "num_models": 2, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_call1_halmos_exception(uint256)", + "exitcode": 1, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_call1_normal(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_create()", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_create_halmos_exception()", + "exitcode": 1, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_returndata()", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_setup()", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], "test/Counter.t.sol:CounterTest": [ { "name": "check_div_1(uint256,uint256)", @@ -481,18 +611,27 @@ "num_bounded_loops": null }, { - "name": "check_create2_collision(uint256,uint256,bytes32)", + "name": "check_create2_collision_alias(uint256,uint256,bytes32)", "exitcode": 1, - "num_models": 0, + "num_models": 1, "models": null, "num_paths": null, "time": null, "num_bounded_loops": null }, { - "name": "check_create2_collision_alias(uint256,uint256,bytes32)", + "name": "check_create2_collision_basic(uint256,uint256,bytes32)", "exitcode": 1, - "num_models": 1, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_create2_collision_lowlevel(uint256,uint256,bytes32)", + "exitcode": 0, + "num_models": 0, "models": null, "num_paths": null, "time": null, @@ -602,6 +741,15 @@ "num_paths": null, "time": null, "num_bounded_loops": null + }, + { + "name": "check_externalGetter(uint256)", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null } ], "test/HalmosCheatCode.t.sol:HalmosCheatCodeTest": [ @@ -1293,6 +1441,44 @@ "num_bounded_loops": null } ], + "test/StaticContexts.t.sol:StaticContextsTest": [ + { + "name": "check_create2_fails()", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_create_fails()", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_log_fails()", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_sstore_fails()", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], "test/Storage.t.sol:StorageTest": [ { "name": "check_addArr1(uint256)", @@ -1536,7 +1722,7 @@ ], "test/UnsupportedOpcode.t.sol:X": [ { - "name": "check_foo()", + "name": "check_unsupported_opcode()", "exitcode": 1, "num_models": 0, "models": null, @@ -1547,7 +1733,7 @@ ], "test/UnsupportedOpcode.t.sol:Y": [ { - "name": "check_foo()", + "name": "check_unsupported_opcode()", "exitcode": 1, "num_models": 0, "models": null, @@ -1558,7 +1744,7 @@ ], "test/UnsupportedOpcode.t.sol:Z": [ { - "name": "check_foo()", + "name": "check_unsupported_opcode()", "exitcode": 1, "num_models": 0, "models": null, @@ -1633,4 +1819,4 @@ } ] } -} \ No newline at end of file +} diff --git a/tests/remappings.txt b/tests/remappings.txt index 9c9b6d20..166c39da 100644 --- a/tests/remappings.txt +++ b/tests/remappings.txt @@ -1 +1,2 @@ openzeppelin/=lib/openzeppelin-contracts/contracts/ +ds-test/=lib/forge-std/lib/ds-test/src/ diff --git a/tests/test/AssertTest.sol b/tests/test/AssertTest.t.sol similarity index 80% rename from tests/test/AssertTest.sol rename to tests/test/AssertTest.t.sol index 6fd996a1..c63386c9 100644 --- a/tests/test/AssertTest.sol +++ b/tests/test/AssertTest.t.sol @@ -13,18 +13,18 @@ contract C is Test { } } -contract CTest is Test { +contract AssertTest is Test { C c; function setUp() public { c = new C(); } - function check_foo() public { + function check_assert_not_propagated() public { address(c).call(abi.encodeWithSelector(C.foo.selector, bytes(""))); // pass } - function check_bar() public { + function check_fail_propagated() public { address(c).call(abi.encodeWithSelector(C.bar.selector, bytes(""))); // fail } } diff --git a/tests/test/Buffers.t.sol b/tests/test/Buffers.t.sol new file mode 100644 index 00000000..f377dbe9 --- /dev/null +++ b/tests/test/Buffers.t.sol @@ -0,0 +1,62 @@ +// SPDX-License-Identifier: AGPL-3.0 +pragma solidity >=0.8.0 <0.9.0; +import "forge-std/Test.sol"; + +contract BuffersTest is Test { + function check_calldatacopy_large_offset() public { + uint256 index = 1 ether; + uint256 value; + assembly { + calldatacopy(0, index, 32) + value := mload(0) + } + + assertEq(value, 0); + } + + function check_calldataload_large_offset() public { + uint256 index = 1 ether; + uint256 value; + assembly { + value := calldataload(index) + } + + assertEq(value, 0); + } + + function check_codecopy_large_offset() public { + uint256 index = 1 ether; + uint256 value; + assembly { + codecopy(0, index, 32) + value := mload(0) + } + + assertEq(value, 0); + } + + function check_codecopy_offset_across_boundary() public { + uint256 index = address(this).code.length - 16; + uint256 value; + assembly { + codecopy(0, index, 32) + value := mload(0) + } + + assertNotEq(value, 0); + } + + // TODO: uncomment when we support extcodecopy + // function check_extcodecopy_boundary() public { + // address target = address(this); + // uint256 index = target.code.length - 16; + // uint256 value; + // assembly { + // extcodecopy(target, 0, index, 32) + // value := mload(0) + // } + + // console2.log("value:", value); + // assertNotEq(value, 0); + // } +} diff --git a/tests/test/Call.t.sol b/tests/test/Call.t.sol index 40a72c2e..229f6015 100644 --- a/tests/test/Call.t.sol +++ b/tests/test/Call.t.sol @@ -111,11 +111,11 @@ contract CallTest is Test { (address msg_sender, uint msg_value, address target) = abi.decode(retdata, (address, uint, address)); // delegatecall is executed in the caller's context - assert(msg_sender == address(this)); - assert(msg_value == fund); - assert(target == address(d)); + assertEq(msg_sender, address(this)); + assertEq(msg_value, fund); + assertEq(target, address(d)); - assert(d.num() == x); // delegatecall updates the caller's state + assert(d.num() == x); // delegatecall updates the caller's state assert(d.c().num() == 0); assert(address(this).balance == 0); diff --git a/tests/test/Context.t.sol b/tests/test/Context.t.sol new file mode 100644 index 00000000..0733ecc5 --- /dev/null +++ b/tests/test/Context.t.sol @@ -0,0 +1,281 @@ +// SPDX-License-Identifier: AGPL-3.0 +pragma solidity >=0.8.0 <0.9.0; + +import "forge-std/Test.sol"; + +contract Context is Test { + bool public flag; + + function call0(uint mode) external { + flag = true; + + if (mode == 1) { + assembly { + stop() + } + } else if (mode == 2) { + assembly { + invalid() + } + } else if (mode == 3) { + assembly { + revert(0, 0) + } + } else if (mode == 4) { + revert("blah"); // revert(Error("blah")) + } else if (mode == 5) { + assert(false); // revert(Panic(1)) + } else if (mode == 6) { + assembly { + return(0, 0) + } + } else if (mode == 7) { + assembly { + return(0, 32) + } + } else if (mode == 8) { + assembly { + let p := mload(0x40) + returndatacopy(p, returndatasize(), 32) // OutOfBoundsRead + } + } else if (mode == 9) { + vm.prank(address(0)); + vm.prank(address(0)); // HalmosException + } else if (mode == 10) { + fail(); + } + } + + function call1(uint mode1, address ctx0, uint mode0) external returns (bool success, bytes memory retdata) { + flag = true; + + (success, retdata) = ctx0.call(abi.encodeWithSelector(Context.call0.selector, mode0)); + + if (mode1 == 0) { + bytes memory result = abi.encode(success, retdata); + assembly { + revert(add(32, result), mload(result)) + } + } + } +} + +contract ConstructorContext { + constructor(Context ctx, uint mode, bool fail) { + assert(returndatasize() == 0); // empty initial returndata + assert(msg.data.length == 0); // no calldata for constructor + + ctx.call0(mode); + + if (fail) revert("fail"); + } + + function returndatasize() internal pure returns (uint size) { + assembly { + size := returndatasize() + } + } +} + +contract ContextTest is Test { + address internal testDeployer; + address internal testAddress; + + Context internal ctx; + + constructor() payable { + assertEq(returndatasize(), 0); // empty initial returndata + assertEq(msg.data.length, 0); // no calldata for test constructor + assertEq(msg.value, 0); // no callvalue + testDeployer = msg.sender; + testAddress = address(this); + } + + function ensure_test_context() internal { + assertEq(address(this), testAddress); + assertEq(msg.sender, testDeployer); + assertEq(msg.value, 0); // no callvalue + assertGt(msg.data.length, 0); // non-empty calldata + } + + function setUp() public payable { + assertEq(returndatasize(), 0); // empty initial returndata + ensure_test_context(); + + ctx = new Context(); + + assertEq(returndatasize(), 0); // empty returndata after create + } + + function check_setup() public payable { + assert(returndatasize() == 0); // empty initial returndata + ensure_test_context(); + } + + function check_returndata() public payable { + assert(returndatasize() == 0); // empty initial returndata + ensure_test_context(); + + address(ctx).call(abi.encodeWithSelector(Context.call0.selector, 1)); + assert(returndatasize() == 0); + ensure_test_context(); + + address(ctx).call(abi.encodeWithSelector(Context.call0.selector, 2)); + assert(returndatasize() == 0); + ensure_test_context(); + + address(ctx).call(abi.encodeWithSelector(Context.call0.selector, 3)); + assert(returndatasize() == 0); + ensure_test_context(); + + address(ctx).call(abi.encodeWithSelector(Context.call0.selector, 4)); + assert(returndatasize() == 100); + ensure_test_context(); + + address(ctx).call(abi.encodeWithSelector(Context.call0.selector, 5)); + assert(returndatasize() == 36); + ensure_test_context(); + + address(ctx).call(abi.encodeWithSelector(Context.call0.selector, 6)); + assert(returndatasize() == 0); + ensure_test_context(); + + address(ctx).call(abi.encodeWithSelector(Context.call0.selector, 7)); + assert(returndatasize() == 32); + ensure_test_context(); + + address(ctx).call(abi.encodeWithSelector(Context.call0.selector, 8)); + assert(returndatasize() == 0); + ensure_test_context(); + + new Context(); + assert(returndatasize() == 0); // empty returndata after create + ensure_test_context(); + } + + function check_create() public payable { + assertEq(returndatasize(), 0); // empty initial returndata + ensure_test_context(); + + Context ctx1 = new Context(); + ConstructorContext cc1 = new ConstructorContext(ctx1, 7, false); + cc1; // silence unused warning + assertEq(returndatasize(), 0); // empty returndata after create + ensure_test_context(); + + assertTrue(ctx1.flag()); + assertEq(returndatasize(), 32); + ensure_test_context(); + + Context ctx2 = new Context(); + try new ConstructorContext(ctx2, 7, true) returns (ConstructorContext cc2) { + cc2; // silence unused warning + } catch {} + assertEq(returndatasize(), 100); // returndata for create failure + ensure_test_context(); + + assertFalse(ctx2.flag()); + assertEq(returndatasize(), 32); + ensure_test_context(); + } + + function check_create_halmos_exception() public payable { + assert(returndatasize() == 0); // empty initial returndata + ensure_test_context(); + + try new ConstructorContext(ctx, 9, false) returns (ConstructorContext cc) { + cc; // silence unused warning + } catch {} + + assert(false); // shouldn't reach here + } + + function check_call0_normal(uint mode0) public payable { + require(mode0 < 9); + _check_call0(mode0); + } + + function check_call0_halmos_exception() public payable { + _check_call0(9); + } + + function check_call0_fail() public payable { + _check_call0(10); + } + + function _check_call0(uint mode0) public payable { + assert(returndatasize() == 0); // empty initial returndata + ensure_test_context(); + + Context ctx0 = ctx; + + (bool success0, bytes memory retdata0) = address(ctx0).call(abi.encodeWithSelector(Context.call0.selector, mode0)); + assert(returndatasize() == retdata0.length); + ensure_test_context(); + + ensure_call0_result(mode0, success0, retdata0); + + assert(ctx0.flag() == success0); // revert state + assert(returndatasize() == 32); + ensure_test_context(); + } + + function check_call1_normal(uint mode1, uint mode0) public payable { + require(mode0 < 9); + _check_call1(mode1, mode0); + } + + function check_call1_halmos_exception(uint mode1) public payable { + _check_call1(mode1, 9); + } + + function check_call1_fail(uint mode1) public payable { + _check_call1(mode1, 10); + } + + function _check_call1(uint mode1, uint mode0) public payable { + assert(returndatasize() == 0); // empty initial returndata + ensure_test_context(); + + Context ctx1 = new Context(); + Context ctx0 = ctx; + + (bool success1, bytes memory retdata1) = address(ctx1).call(abi.encodeWithSelector(Context.call1.selector, mode1, ctx0, mode0)); + assert(returndatasize() == retdata1.length); + ensure_test_context(); + + assert(success1 == (mode1 > 0)); + (bool success0, bytes memory retdata0) = abi.decode(retdata1, (bool, bytes)); + ensure_test_context(); + + ensure_call0_result(mode0, success0, retdata0); + + // revert state + assert(ctx1.flag() == success1); + assert(returndatasize() == 32); + ensure_test_context(); + + assert(ctx0.flag() == (success1 && success0)); + assert(returndatasize() == 32); + ensure_test_context(); + } + + function ensure_call0_result(uint mode, bool success, bytes memory retdata) internal { + if (mode == 1) assert( success && retdata.length == 0); + else if (mode == 2) assert(!success && retdata.length == 0); + else if (mode == 3) assert(!success && retdata.length == 0); + else if (mode == 4) assert(!success && retdata.length > 0); + else if (mode == 5) assert(!success && retdata.length == 36); + else if (mode == 6) assert( success && retdata.length == 0); + else if (mode == 7) assert( success && retdata.length == 32); + else if (mode == 8) assert(!success && retdata.length == 0); + else if (mode == 9) assert(!success && retdata.length == 0); + else if (mode == 10) assert(!success && retdata.length == 0); + } + + function returndatasize() internal pure returns (uint size) { + assembly { + size := returndatasize() + } + } +} diff --git a/tests/test/Create2.t.sol b/tests/test/Create2.t.sol index 101fff9b..2dc27586 100644 --- a/tests/test/Create2.t.sol +++ b/tests/test/Create2.t.sol @@ -77,10 +77,36 @@ contract Create2Test is Test { assert(C(c2).num2() == x); } - function check_create2_collision(uint x, uint y, bytes32 salt) public { + function check_create2_collision_basic(uint x, uint y, bytes32 salt) public { C c1 = new C{salt: salt}(x, y); - C c2 = new C{salt: salt}(x, y); // expected to fail - assert(c1 == c2); // deadcode + C c2 = new C{salt: salt}(x, y); // expected to fail (Solidity reverts) + c1; c2; // silence warnings + } + + function check_create2_collision_lowlevel(uint x, uint y, bytes32 salt) public { + bytes memory deploymentBytecode = abi.encodePacked(type(C).creationCode, abi.encode(x, y)); + + address addr1; + address addr2; + + assembly { + addr1 := create2( + 0, // value + add(deploymentBytecode, 32), // data offset + mload(deploymentBytecode), // data length + salt + ) + + addr2 := create2( + 0, // value + add(deploymentBytecode, 32), // data offset + mload(deploymentBytecode), // data length + salt + ) + } + + assert(addr1 != address(0)); + assert(addr2 == address(0)); // expected to fail without reverting } function check_create2_no_collision_1(uint x, uint y, bytes32 salt1, bytes32 salt2) public { diff --git a/tests/test/Foundry.t.sol b/tests/test/Foundry.t.sol index a97c25c0..556d4d3d 100644 --- a/tests/test/Foundry.t.sol +++ b/tests/test/Foundry.t.sol @@ -6,6 +6,21 @@ import "forge-std/StdCheats.sol"; import "../src/Counter.sol"; +contract DeepFailer is Test { + function do_test(uint256 x) external { + if (x >= 6) { + fail(); + } else { + (bool success, ) = address(this).call(abi.encodeWithSelector(this.do_test.selector, x + 1)); + success; // silence warnings + } + } + + function test_fail_cheatcode() public { + DeepFailer(address(this)).do_test(0); + } +} + contract FoundryTest is Test { /* TODO: support checkFail prefix function checkFail() public { @@ -51,6 +66,8 @@ contract FoundryTest is Test { assertEq(uint256(uint8(retval[0])), 0xAA); } + + /// @notice etching to a symbolic address is not supported // function check_etch_SymbolicAddr(address who) public { // vm.etch(who, hex"60425f526001601ff3"); diff --git a/tests/test/Getter.t.sol b/tests/test/Getter.t.sol index ba069e3a..9eb9bdcf 100644 --- a/tests/test/Getter.t.sol +++ b/tests/test/Getter.t.sol @@ -5,10 +5,14 @@ pragma solidity >=0.8.0 <0.9.0; /// @custom:halmos --storage-layout=generic contract GetterTest { - uint256[3] v; + uint256[3] public v; uint w; function check_Getter(uint256 i) public view { assert(v[i] >= 0); } + + function check_externalGetter(uint256 i) public view { + assert(this.v(i) >= 0); + } } diff --git a/tests/test/Math.t.sol b/tests/test/Math.t.sol index c05737d3..b24deab3 100644 --- a/tests/test/Math.t.sol +++ b/tests/test/Math.t.sol @@ -21,7 +21,7 @@ contract MathTest { assert(A1 * S2 <= A2 * S1); // no counterexample } - /// @custom:halmos --smt-div + /// @custom:halmos --smt-div --solver-timeout-assertion=0 function check_mint(uint s, uint A1, uint S1) public pure { uint a = (s * A1) / S1; diff --git a/tests/test/SignedDiv.t.sol b/tests/test/SignedDiv.t.sol index 583b19cd..84742735 100644 --- a/tests/test/SignedDiv.t.sol +++ b/tests/test/SignedDiv.t.sol @@ -69,7 +69,6 @@ abstract contract TestMulWad is Test { SolidityWadMul solidityWadMul = new SolidityWadMul(); function setUp() external { - solidityWadMul = new SolidityWadMul(); wadMul = createWadMul(); } diff --git a/tests/test/StaticContexts.t.sol b/tests/test/StaticContexts.t.sol new file mode 100644 index 00000000..d63f3da1 --- /dev/null +++ b/tests/test/StaticContexts.t.sol @@ -0,0 +1,72 @@ +// SPDX-License-Identifier: AGPL-3.0 +pragma solidity >=0.8.0 <0.9.0; + +import "forge-std/Test.sol"; + +contract Dummy {} + +contract StaticContextsTest is Test { + event Log(uint256 x); + + uint256 x; + + function do_sstore() public { + unchecked { + x += 1; + } + } + + function do_log() public { + emit Log(x); + } + + function do_create() public { + new Dummy(); + } + + function do_create2() public { + new Dummy{salt: 0}(); + } + + function do_call_with_value() public { + vm.deal(address(this), 1 ether); + (bool success, ) = payable(address(this)).call{value: 1 ether}(""); + success; // silence warnings + } + + function do_selfdestruct() public { + selfdestruct(payable(address(0))); + } + + function check_sstore_fails() public { + (bool success, ) = address(this).staticcall(abi.encodeWithSignature("do_sstore()")); + assertFalse(success); + } + + function check_log_fails() public { + (bool success, ) = address(this).staticcall(abi.encodeWithSignature("do_log()")); + assertFalse(success); + } + + function check_create_fails() public { + (bool success, ) = address(this).staticcall(abi.encodeWithSignature("do_create()")); + assertFalse(success); + } + + function check_create2_fails() public { + (bool success, ) = address(this).staticcall(abi.encodeWithSignature("do_create2()")); + assertFalse(success); + } + + // TODO: value check not implemented yet + // function check_call_with_value_fails() public { + // (bool success, ) = address(this).staticcall(abi.encodeWithSignature("do_call_with_value()")); + // assertFalse(success); + // } + + // TODO: selfdestruct not implemented yet + // function check_selfdestruct_fails() public { + // (bool success, ) = address(this).staticcall(abi.encodeWithSignature("do_selfdestruct()")); + // assertFalse(success); + // } +} diff --git a/tests/test/UnsupportedOpcode.t.sol b/tests/test/UnsupportedOpcode.t.sol index 9fbb9f31..b3981571 100644 --- a/tests/test/UnsupportedOpcode.t.sol +++ b/tests/test/UnsupportedOpcode.t.sol @@ -1,18 +1,20 @@ // SPDX-License-Identifier: AGPL-3.0 pragma solidity >=0.8.0 <0.9.0; +// no hop contract X { - function foo() public { + function foo() internal { assembly { selfdestruct(0) // unsupported opcode } } - function check_foo() public { + function check_unsupported_opcode() public { foo(); // unsupported error } } +// 1 hop contract Y { X x; @@ -20,11 +22,12 @@ contract Y { x = new X(); } - function check_foo() public { - x.foo(); // unsupported error + function check_unsupported_opcode() public { + x.check_unsupported_opcode(); // unsupported error } } +// 2 hops contract Z { Y y; @@ -33,7 +36,7 @@ contract Z { y.setUp(); } - function check_foo() public { - y.check_foo(); // unsupported error + function check_unsupported_opcode() public { + y.check_unsupported_opcode(); // unsupported error } } diff --git a/tests/test_sevm.py b/tests/test_sevm.py index 5f115e41..0f1c61cb 100644 --- a/tests/test_sevm.py +++ b/tests/test_sevm.py @@ -13,6 +13,8 @@ f_smod, f_exp, f_origin, + CallContext, + Message, SEVM, Exec, int_of, @@ -52,14 +54,13 @@ def storage(): def mk_ex(hexcode, sevm, solver, storage, caller, this): bytecode = Contract(hexcode) + message = Message(target=this, caller=caller, value=callvalue, data=[]) return sevm.mk_exec( code={this: bytecode}, storage={this: storage}, balance=balance, block=mk_block(), - calldata=[], - callvalue=callvalue, - caller=caller, + context=CallContext(message), this=this, pgm=bytecode, symbolic=True, diff --git a/tests/test_traces.py b/tests/test_traces.py new file mode 100644 index 00000000..ebd3ea1e --- /dev/null +++ b/tests/test_traces.py @@ -0,0 +1,892 @@ +import json +import pytest +import subprocess + +from dataclasses import dataclass +from typing import Dict, List, Any, Optional + +from z3 import * + +from halmos.__main__ import mk_block, render_trace +from halmos.exceptions import * +from halmos.sevm import ( + CallContext, + CallOutput, + Contract, + EventLog, + Exec, + Message, + NotConcreteError, + SEVM, + byte_length, + con, + int_of, + wstore, +) +from halmos.utils import EVM +from test_fixtures import args, options, sevm + +import halmos.sevm + +# keccak256("FooEvent()") +FOO_EVENT_SIG = 0x34E21A9428B1B47E73C4E509EABEEA7F2B74BECA07D82AAC87D4DD28B74C2A4A + +# keccak256("Log(uint256)") +LOG_U256_SIG = 0x909C57D5C6AC08245CF2A6DE3900E2B868513FA59099B92B27D8DB823D92DF9C + +# bytes4(keccak256("Panic(uint256)")) + bytes32(1) +PANIC_1 = 0x4E487B710000000000000000000000000000000000000000000000000000000000000001 + +DEFAULT_EMPTY_CONSTRUCTOR = """ +contract Foo {} +""" + + +FAILED_CREATE = """ +contract Bar { + uint256 immutable x; + + constructor(uint256 _x) { + assert(_x != 42); + x = _x; + } +} + +contract Foo { + function go() public returns(bool success) { + bytes memory creationCode = abi.encodePacked( + type(Bar).creationCode, + uint256(42) + ); + + address addr; + bytes memory returndata; + + assembly { + addr := create(0, add(creationCode, 0x20), mload(creationCode)) + + // advance free mem pointer to allocate `size` bytes + let free_mem_ptr := mload(0x40) + mstore(0x40, add(free_mem_ptr, returndatasize())) + + returndata := free_mem_ptr + mstore(returndata, returndatasize()) + + let offset := add(returndata, 32) + returndatacopy( + offset, + 0, // returndata offset + returndatasize() + ) + } + + success = (addr != address(0)); + // assert(returndata.length == 36); + } +} +""" + + +caller = BitVec("msg_sender", 160) +this = BitVec("this_address", 160) +balance = Array("balance_0", BitVecSort(160), BitVecSort(256)) + +# 0x0f59f83a is keccak256("go()") +default_calldata = list(con(x, size_bits=8) for x in bytes.fromhex("0f59f83a")) + +go_uint256_selector = BitVecVal(0xB20E7344, 32) # keccak256("go(uint256)") +p_x_uint256 = BitVec("p_x_uint256", 256) +go_uint256_calldata: List[BitVecRef] = [] +wstore(go_uint256_calldata, 0, 4, go_uint256_selector) +wstore(go_uint256_calldata, 4, 32, p_x_uint256) + + +@pytest.fixture +def solver(args): + solver = SolverFor( + "QF_AUFBV" + ) # quantifier-free bitvector + array theory; https://smtlib.cs.uiowa.edu/logics.shtml + solver.set(timeout=args.solver_timeout_branching) + return solver + + +@pytest.fixture +def storage(): + return {} + + +@dataclass(frozen=True) +class SingleResult: + is_single: bool + value: Optional[Any] + + # allows tuple-like unpacking + def __iter__(self): + return iter((self.is_single, self.value)) + + +NO_SINGLE_RESULT = SingleResult(False, None) + + +def single(iterable) -> SingleResult: + """ + Returns (True, element) if the iterable has exactly one element + or (False, None) otherwise. + + Note: + - if the iterable has a single None element, this returns (True, None) + """ + iterator = iter(iterable) + element = None + try: + element = next(iterator) + except StopIteration: + return NO_SINGLE_RESULT + + try: + next(iterator) + return NO_SINGLE_RESULT + except StopIteration: + return SingleResult(True, element) + + +def is_single(iterable) -> bool: + """ + Returns True if the iterable has exactly one element, False otherwise. + """ + + return single(iterable).is_single + + +def empty(iterable) -> bool: + """ + Returns True if the iterable is empty, False otherwise. + """ + iterator = iter(iterable) + try: + next(iterator) + return False + except StopIteration: + return True + + +def render_path(ex: Exec) -> None: + path = list(dict.fromkeys(ex.path)) + path.remove("True") + print(f"Path: {', '.join(path)}") + + +def mk_create_ex( + hexcode, sevm, solver, caller=caller, value=con(0), this=this, storage={} +) -> Exec: + bytecode = Contract(hexcode) + storage[this] = {} + + message = Message( + target=this, + caller=caller, + value=value, + data=[], + is_static=False, + ) + + return sevm.mk_exec( + code={}, + storage=storage, + balance=balance, + block=mk_block(), + context=CallContext(message=message), + this=this, + pgm=bytecode, + symbolic=True, + solver=solver, + ) + + +def mk_ex( + hexcode, + sevm, + solver, + caller=caller, + value=con(0), + this=this, + storage={}, + data=default_calldata, +) -> Exec: + bytecode = Contract(hexcode) + storage[this] = {} + + message = Message( + target=this, + caller=caller, + value=value, + data=data, + is_static=False, + ) + + return sevm.mk_exec( + code={this: bytecode}, + storage=storage, + balance=balance, + block=mk_block(), + context=CallContext(message=message), + this=this, + pgm=bytecode, + symbolic=True, + solver=solver, + ) + + +BuildOutput = Dict + + +def compile(source: str) -> BuildOutput: + proc = subprocess.Popen( + ["solc", "--combined-json", "bin,bin-runtime", "--no-cbor-metadata", "-"], + stdin=subprocess.PIPE, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + ) + (stdout, stderr) = proc.communicate(input=source.encode("utf-8")) + if proc.returncode != 0: + raise Exception("solc failed: " + stderr.decode("utf-8")) + return json.loads(stdout) + + +def find_contract(contract_name: str, build_output: BuildOutput) -> Dict: + for name in build_output["contracts"]: + if name.endswith(f":{contract_name}"): + return build_output["contracts"][name] + + raise Exception(f"Contract {contract_name} not found in {build_output}") + + +def get_bytecode(source: str, contract_name: str = "Foo"): + build_output = compile(source) + contract_object = find_contract(contract_name, build_output) + return contract_object["bin"], contract_object["bin-runtime"] + + +def test_deploy_basic(sevm, solver): + deploy_hexcode, runtime_hexcode = get_bytecode(DEFAULT_EMPTY_CONSTRUCTOR) + exec: Exec = mk_create_ex(deploy_hexcode, sevm, solver) + + # before execution + assert exec.context.output.data is None + + sevm.run(exec) + render_trace(exec.context) + + # after execution + assert exec.context.output.error is None + assert exec.context.output.data == bytes.fromhex(runtime_hexcode) + assert len(exec.context.trace) == 0 + + +def test_deploy_nonpayable_reverts(sevm, solver): + deploy_hexcode, _ = get_bytecode(DEFAULT_EMPTY_CONSTRUCTOR) + exec: Exec = mk_create_ex(deploy_hexcode, sevm, solver, value=con(1)) + + sevm.run(exec) + render_trace(exec.context) + + assert isinstance(exec.context.output.error, Revert) + assert not exec.context.output.data + assert len(exec.context.trace) == 0 + + +def test_deploy_payable(sevm, solver): + deploy_hexcode, runtime_hexcode = get_bytecode( + """ + contract Foo { + constructor() payable {} + } + """ + ) + exec: Exec = mk_create_ex(deploy_hexcode, sevm, solver, value=con(1)) + + sevm.run(exec) + render_trace(exec.context) + + assert exec.context.output.error is None + assert exec.context.output.data == bytes.fromhex(runtime_hexcode) + assert len(exec.context.trace) == 0 + + +def test_deploy_event_in_constructor(sevm, solver): + deploy_hexcode, _ = get_bytecode( + """ + contract Foo { + event FooEvent(); + + constructor() { + emit FooEvent(); + } + } + """ + ) + exec: Exec = mk_create_ex(deploy_hexcode, sevm, solver) + + sevm.run(exec) + render_trace(exec.context) + + assert exec.context.output.error is None + assert len(exec.context.trace) == 1 + + event: EventLog = exec.context.trace[0] + assert len(event.topics) == 1 + assert int_of(event.topics[0]) == FOO_EVENT_SIG + assert not event.data + + +def test_simple_call(sevm: SEVM, solver): + _, runtime_hexcode = get_bytecode( + """ + contract Foo { + function view_func() public pure returns (uint) { + return 42; + } + + function go() public view returns (bool success) { + (success, ) = address(this).staticcall(abi.encodeWithSignature("view_func()")); + } + } + """ + ) + input_exec: Exec = mk_ex(runtime_hexcode, sevm, solver) + + execs = sevm.run(input_exec)[0] + (is_single_exec, output_exec) = single(execs) + assert is_single_exec + + render_trace(output_exec.context) + + assert output_exec.context.output is not None + assert output_exec.context.output.error is None + + # go() returns success=true + assert int_of(output_exec.context.output.data) == 1 + + # view_func() returns 42 + (is_single_call, subcall) = single(output_exec.context.subcalls()) + assert is_single_call + assert subcall.output.error is None + assert int_of(subcall.output.data) == 42 + + +def test_failed_call(sevm: SEVM, solver): + _, runtime_hexcode = get_bytecode( + """ + contract Foo { + function just_fails() public pure returns (uint) { + assert(false); + } + + function go() public view returns (bool success) { + (success, ) = address(this).staticcall(abi.encodeWithSignature("just_fails()")); + } + } + """ + ) + input_exec: Exec = mk_ex(runtime_hexcode, sevm, solver) + + execs = sevm.run(input_exec)[0] + (is_single_exec, output_exec) = single(execs) + assert is_single_exec + + render_trace(output_exec.context) + + # go() does not revert, it returns success=false + assert output_exec.context.output.error is None + assert int_of(output_exec.context.output.data) == 0 + + # the just_fails() subcall fails + (is_single_call, subcall) = single(output_exec.context.subcalls()) + assert is_single_call + assert isinstance(subcall.output.error, Revert) + assert int_of(subcall.output.data) == PANIC_1 + + +def test_failed_static_call(sevm: SEVM, solver): + _, runtime_hexcode = get_bytecode( + """ + contract Foo { + uint256 x; + + function do_sstore() public returns (uint) { + unchecked { + x += 1; + } + } + + function go() public view returns (bool success) { + (success, ) = address(this).staticcall(abi.encodeWithSignature("do_sstore()")); + } + } + """ + ) + input_exec: Exec = mk_ex(runtime_hexcode, sevm, solver) + + execs = sevm.run(input_exec)[0] + (is_single_exec, output_exec) = single(execs) + assert is_single_exec + + render_trace(output_exec.context) + + # go() does not revert, it returns success=false + assert output_exec.context.output.error is None + assert int_of(output_exec.context.output.data) == 0 + + # the do_sstore() subcall fails + (is_single_call, subcall) = single(output_exec.context.subcalls()) + assert is_single_call + assert subcall.message.is_static is True + assert isinstance(subcall.output.error, WriteInStaticContext) + + +def test_symbolic_subcall(sevm: SEVM, solver): + _, runtime_hexcode = get_bytecode( + """ + contract Foo { + function may_fail(uint256 x) public pure returns (uint) { + assert(x != 42); + } + + function go(uint256 x) public view returns (bool success) { + (success, ) = address(this).staticcall(abi.encodeWithSignature("may_fail(uint256)", x)); + } + } + """ + ) + input_exec: Exec = mk_ex(runtime_hexcode, sevm, solver, data=go_uint256_calldata) + + execs = sevm.run(input_exec)[0] + + # we get 2 executions, one for x == 42 and one for x != 42 + assert len(execs) == 2 + render_trace(execs[0].context) + render_trace(execs[1].context) + + # all executions have exactly one subcall and the outer call does not revert + assert all(is_single(x.context.subcalls()) for x in execs) + assert all(x.context.output.error is None for x in execs) + + # in one of the executions, the subcall succeeds + subcalls = list(single(x.context.subcalls()).value for x in execs) + assert any(subcall.output.error is None for subcall in subcalls) + + # in one of the executions, the subcall reverts + assert any(isinstance(subcall.output.error, Revert) for subcall in subcalls) + + +def test_symbolic_create(sevm: SEVM, solver): + _, runtime_hexcode = get_bytecode( + """ + contract Bar { + uint256 immutable x; + + constructor(uint256 _x) { + assert(_x != 42); + x = _x; + } + } + + contract Foo { + function go(uint256 x) public returns (bool success) { + try new Bar(x) { + success = true; + } catch { + success = false; + } + } + } + """ + ) + input_exec: Exec = mk_ex(runtime_hexcode, sevm, solver, data=go_uint256_calldata) + + execs = sevm.run(input_exec)[0] + + # we get 2 executions, one for x == 42 and one for x != 42 + assert len(execs) == 2 + render_trace(execs[0].context) + render_trace(execs[1].context) + + # all executions have exactly one subcall and the outer call does not revert + assert all(is_single(x.context.subcalls()) for x in execs) + assert all(x.context.output.error is None for x in execs) + + # in one of the executions, the subcall succeeds + subcalls = list(single(x.context.subcalls()).value for x in execs) + assert any(subcall.output.error is None for subcall in subcalls) + + # in one of the executions, the subcall reverts + assert any(isinstance(subcall.output.error, Revert) for subcall in subcalls) + + +def test_failed_create(sevm: SEVM, solver): + _, runtime_hexcode = get_bytecode(FAILED_CREATE) + input_exec: Exec = mk_ex(runtime_hexcode, sevm, solver) + + execs = sevm.run(input_exec)[0] + (is_single_exec, output_exec) = single(execs) + assert is_single_exec + + render_trace(output_exec.context) + + # go() does not revert, it returns success=false + assert output_exec.context.output.error is None + assert int_of(output_exec.context.output.data) == 0 + + # the create() subcall fails + (is_single_call, subcall) = single(output_exec.context.subcalls()) + assert is_single_call + assert isinstance(subcall.output.error, Revert) + assert int_of(subcall.output.data) == PANIC_1 + + +def test_event_conditional_on_symbol(sevm: SEVM, solver): + _, runtime_hexcode = get_bytecode( + """ + contract Foo { + event Log(uint256 x); + + function may_log(uint256 x) public returns (uint) { + if (x == 42) { + emit Log(x); + } + } + + function go(uint256 x) public returns (bool success) { + (success, ) = address(this).staticcall(abi.encodeWithSignature("may_log(uint256)", x)); + if (x != 42) { + emit Log(x); + } + } + } + """ + ) + input_exec: Exec = mk_ex(runtime_hexcode, sevm, solver, data=go_uint256_calldata) + + execs = sevm.run(input_exec)[0] + + for e in execs: + render_path(e) + render_trace(e.context) + + assert len(execs) == 2 + + # all executions have a single subcall + assert all(is_single(x.context.subcalls()) for x in execs) + + all_subcalls = list(single(x.context.subcalls()).value for x in execs) + + # one execution has a single subcall that reverts + assert any( + isinstance(subcall.output.error, WriteInStaticContext) + for subcall in all_subcalls + ) + + # one execution has a single subcall that succeeds and emits an event + assert any( + single(x.context.subcalls()).value.output.error is None + and is_single(x.context.logs()) + for x in execs + ) + + +def test_symbolic_event_data(sevm: SEVM, solver): + _, runtime_hexcode = get_bytecode( + """ + contract Foo { + event Log(uint256 x); + + function go(uint256 x) public returns (bool success) { + emit Log(x); + } + } + """ + ) + + input_exec: Exec = mk_ex(runtime_hexcode, sevm, solver, data=go_uint256_calldata) + execs = sevm.run(input_exec)[0] + (is_single_exec, output_exec) = single(execs) + assert is_single_exec + + (is_single_event, event) = single(output_exec.context.logs()) + assert is_single_event + assert len(event.topics) == 1 + assert int_of(event.topics[0]) == LOG_U256_SIG + assert is_bv(event.data) and event.data.decl().name() == "p_x_uint256" + + +def test_symbolic_event_topic(sevm: SEVM, solver): + _, runtime_hexcode = get_bytecode( + """ + contract Foo { + event Log(uint256 indexed x); + + function go(uint256 x) public returns (bool success) { + emit Log(x); + } + } + """ + ) + + input_exec: Exec = mk_ex(runtime_hexcode, sevm, solver, data=go_uint256_calldata) + execs = sevm.run(input_exec)[0] + (is_single_exec, output_exec) = single(execs) + assert is_single_exec + + (is_single_event, event) = single(output_exec.context.logs()) + assert is_single_event + assert len(event.topics) == 2 + assert int_of(event.topics[0]) == LOG_U256_SIG + assert is_bv(event.topics[1]) and event.topics[1].decl().name() == "p_x_uint256" + assert not event.data + + +def test_trace_ordering(sevm: SEVM, solver): + _, runtime_hexcode = get_bytecode( + """ + contract Foo { + event FooEvent(); + + function view_func1() public view returns (uint) { + return gasleft(); + } + + function view_func2() public view returns (uint) { + return 42; + } + + function go(uint256 x) public returns (bool success) { + (bool succ1, ) = address(this).staticcall(abi.encodeWithSignature("view_func1()")); + emit FooEvent(); + (bool succ2, ) = address(this).staticcall(abi.encodeWithSignature("view_func2()")); + success = succ1 && succ2; + } + } + """ + ) + + input_exec: Exec = mk_ex(runtime_hexcode, sevm, solver, data=go_uint256_calldata) + execs = sevm.run(input_exec)[0] + (is_single_exec, output_exec) = single(execs) + assert is_single_exec + + top_level_call = output_exec.context + render_trace(top_level_call) + + assert len(list(top_level_call.subcalls())) == 2 + call1, call2 = tuple(top_level_call.subcalls()) + + (is_single_event, event) = single(top_level_call.logs()) + assert is_single_event + + # the trace must preserve the ordering + assert top_level_call.trace == [call1, event, call2] + assert int_of(call2.output.data) == 42 + + +def test_static_context_propagates(sevm: SEVM, solver): + _, runtime_hexcode = get_bytecode( + """ + contract Foo { + event FooEvent(); + + function logFoo() public returns (uint) { + emit FooEvent(); + return 42; + } + + function view_func() public returns (bool succ) { + (succ, ) = address(this).call(abi.encodeWithSignature("logFoo()")); + } + + function go(uint256 x) public view { + (bool outerSucc, bytes memory ret) = address(this).staticcall(abi.encodeWithSignature("view_func()")); + assert(outerSucc); + + bool innerSucc = abi.decode(ret, (bool)); + assert(!innerSucc); + } + } + """ + ) + + input_exec: Exec = mk_ex(runtime_hexcode, sevm, solver, data=go_uint256_calldata) + + execs = sevm.run(input_exec)[0] + (is_single_exec, output_exec) = single(execs) + assert is_single_exec + + top_level_call = output_exec.context + render_trace(top_level_call) + + (is_single_call, outer_call) = single(top_level_call.subcalls()) + assert is_single_call + + assert outer_call.message.call_scheme == EVM.STATICCALL + assert outer_call.message.is_static is True + assert outer_call.output.error is None + + assert len(list(outer_call.subcalls())) == 1 + inner_call = next(outer_call.subcalls()) + + assert inner_call.message.call_scheme == EVM.CALL + assert inner_call.message.is_static is True + assert isinstance(inner_call.output.error, WriteInStaticContext) + assert next(inner_call.logs(), None) is None + + +def test_halmos_exception_halts_path(sevm: SEVM, solver): + _, runtime_hexcode = get_bytecode( + """ + contract Foo { + function sload(uint256 x) public view returns (uint256 value) { + assembly { + value := sload(x) + } + } + + function go(uint256 x) public view { + this.sload(x); + } + } + """ + ) + + input_exec: Exec = mk_ex(runtime_hexcode, sevm, solver, data=go_uint256_calldata) + + execs = sevm.run(input_exec)[0] + (is_single_exec, output_exec) = single(execs) + assert is_single_exec + + outer_call = output_exec.context + render_trace(outer_call) + + # outer call does not return because of NotConcreteError + assert outer_call.output.error is None + assert outer_call.output.return_scheme == None + + (is_single_call, inner_call) = single(outer_call.subcalls()) + assert is_single_call + + assert inner_call.message.call_scheme == EVM.STATICCALL + assert isinstance(inner_call.output.error, NotConcreteError) + assert not inner_call.output.data + assert inner_call.output.return_scheme == EVM.SLOAD + + +def test_deploy_symbolic_bytecode(sevm: SEVM, solver): + _, runtime_hexcode = get_bytecode( + """ + contract Foo { + function go(uint256 x) public { + assembly { + mstore(0, x) + let addr := create(0, 0, 32) + } + } + } + """ + ) + + input_exec: Exec = mk_ex(runtime_hexcode, sevm, solver, data=go_uint256_calldata) + + execs = sevm.run(input_exec)[0] + (is_single_exec, output_exec) = single(execs) + assert is_single_exec + + outer_call = output_exec.context + render_trace(outer_call) + + # outer call does not return because of NotConcreteError + assert outer_call.output.error is None + assert outer_call.output.return_scheme == None + + (is_single_call, inner_call) = single(outer_call.subcalls()) + assert is_single_call + assert inner_call.message.call_scheme == EVM.CREATE + + assert isinstance(inner_call.output.error, NotConcreteError) + assert not inner_call.output.data + assert is_bv(inner_call.output.return_scheme) + + +def test_deploy_empty_runtime_bytecode(sevm: SEVM, solver): + for creation_bytecode_len in (0, 1): + _, runtime_hexcode = get_bytecode( + f""" + contract Foo {{ + function go() public {{ + assembly {{ + let addr := create(0, 0, {creation_bytecode_len}) + }} + }} + }} + """ + ) + + input_exec: Exec = mk_ex(runtime_hexcode, sevm, solver, data=default_calldata) + + execs = sevm.run(input_exec)[0] + (is_single_exec, output_exec) = single(execs) + assert is_single_exec + + outer_call = output_exec.context + render_trace(outer_call) + + (is_single_call, inner_call) = single(outer_call.subcalls()) + assert is_single_call + assert inner_call.message.call_scheme == EVM.CREATE + assert len(inner_call.message.data) == creation_bytecode_len + + assert inner_call.output.error is None + assert len(inner_call.output.data) == 0 + assert inner_call.output.return_scheme == EVM.STOP + + +def test_call_limit_with_create(monkeypatch, sevm: SEVM, solver): + _, runtime_hexcode = get_bytecode( + """ + contract Foo { + function go() public { + // bytecode for: + // codecopy(0, 0, codesize()) + // create(0, 0, codesize()) + bytes memory creationCode = hex"386000803938600080f050"; + assembly { + let addr := create(0, add(creationCode, 0x20), mload(creationCode)) + } + } + } + """ + ) + + input_exec: Exec = mk_ex(runtime_hexcode, sevm, solver, data=default_calldata) + + # override the call depth limit to 3 (the test runs faster) + MAX_CALL_DEPTH_OVERRIDE = 3 + monkeypatch.setattr(halmos.sevm, "MAX_CALL_DEPTH", MAX_CALL_DEPTH_OVERRIDE) + + execs = sevm.run(input_exec)[0] + (is_single_exec, output_exec) = single(execs) + assert is_single_exec + + outer_call = output_exec.context + render_trace(outer_call) + + assert outer_call.output.error is None + assert byte_length(outer_call.output.data) == 0 + assert not outer_call.is_stuck() + + # peel the layer of the call stack onion until we get to the innermost call + inner_call = outer_call + for _ in range(MAX_CALL_DEPTH_OVERRIDE): + (is_single_call, inner_call) = single(inner_call.subcalls()) + assert is_single_call + assert inner_call.message.call_scheme == EVM.CREATE + assert byte_length(inner_call.output.data) == 0 + + assert isinstance(inner_call.output.error, MessageDepthLimitError)