From 33dcddad7664cf1d4c939f7337cc0c00ddcd90f8 Mon Sep 17 00:00:00 2001 From: karmacoma Date: Fri, 22 Dec 2023 17:36:34 -0800 Subject: [PATCH] fix: calldata rendering bugfix, large memory offset bugfix (#242) --- src/halmos/__main__.py | 20 +++++++++++++------- src/halmos/sevm.py | 6 ++++++ tests/test_halmos.py | 23 ++++++++++++++++++++++- tests/test_sevm.py | 12 ++++++++++++ 4 files changed, 53 insertions(+), 8 deletions(-) diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py index 919bc161..e4f76141 100644 --- a/src/halmos/__main__.py +++ b/src/halmos/__main__.py @@ -237,6 +237,15 @@ def rendered_trace(context: CallContext) -> str: return output.getvalue() +def rendered_calldata(calldata: List[Byte]) -> str: + if any(is_bv(x) for x in calldata): + # make sure every byte is wrapped + calldata_bv = [x if is_bv(x) else con(x, 8) for x in calldata] + return hexify(simplify(concat(calldata_bv))) + + return "0x" + bytes(calldata).hex() if calldata else "0x" + + def render_trace(context: CallContext, file=sys.stdout) -> None: # TODO: label for known addresses # TODO: decode calldata @@ -261,12 +270,7 @@ def render_trace(context: CallContext, file=sys.stdout) -> None: ) else: - calldata = ( - hexify(simplify(Concat(message.data))) - if any(is_bv(x) for x in message.data) - else bytes(message.data).hex() or "0x" - ) - + calldata = rendered_calldata(message.data) 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}", file=file) @@ -1421,6 +1425,8 @@ def on_exit(exitcode: int) -> MainResult: result = MainResult(exitcode, test_results_map) if args.json_output: + if args.debug: + debug(f"Writing output to {args.json_output}") with open(args.json_output, "w") as json_file: json.dump(asdict(result), json_file, indent=4) @@ -1428,7 +1434,7 @@ def on_exit(exitcode: int) -> MainResult: def on_signal(signum, frame): if args.debug: - debug(f"Signal {signum} received. Dumping {test_results_map}...") + debug(f"Signal {signum} received") exitcode = 128 + signum on_exit(exitcode) sys.exit(exitcode) diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py index b80ad513..d761aab5 100644 --- a/src/halmos/sevm.py +++ b/src/halmos/sevm.py @@ -39,6 +39,8 @@ EMPTY_BYTES = b"" MAX_CALL_DEPTH = 1024 +# TODO: make this configurable +MAX_MEMORY_SIZE = 2**20 # symbolic states # calldataload(index) @@ -170,6 +172,10 @@ def instruction_length(opcode: Any) -> int: def wextend(mem: List[UnionType[int, BitVecRef]], loc: int, size: int) -> None: + new_msize = loc + size + if new_msize > MAX_MEMORY_SIZE: + raise OutOfGasError(f"memory offset {new_msize} exceeds max memory") + mem.extend([0] * (loc + size - len(mem))) diff --git a/tests/test_halmos.py b/tests/test_halmos.py index 746772f5..c99261ea 100644 --- a/tests/test_halmos.py +++ b/tests/test_halmos.py @@ -4,7 +4,8 @@ from typing import Dict from dataclasses import asdict -from halmos.__main__ import _main +from halmos.__main__ import _main, rendered_calldata +from halmos.sevm import con from test_fixtures import halmos_options @@ -76,3 +77,23 @@ def assert_eq(m1: Dict, m2: Dict) -> int: assert r1["name"] == r2["name"] assert r1["exitcode"] == r2["exitcode"], f"{c} {r1['name']}" assert r1["num_models"] == r2["num_models"], f"{c} {r1['name']}" + + +def test_rendered_calldata_symbolic(): + assert rendered_calldata([con(1, 8), con(2, 8), con(3, 8)]) == "0x010203" + + +def test_rendered_calldata_symbolic_singleton(): + assert rendered_calldata([con(0x42, 8)]) == "0x42" + + +def test_rendered_calldata_concrete(): + assert rendered_calldata([1, 2, 3]) == "0x010203" + + +def test_rendered_calldata_mixed(): + assert rendered_calldata([con(1, 8), 2, con(3, 8)]) == "0x010203" + + +def test_rendered_calldata_empty(): + assert rendered_calldata([]) == "0x" diff --git a/tests/test_sevm.py b/tests/test_sevm.py index 9828c8d8..0836be59 100644 --- a/tests/test_sevm.py +++ b/tests/test_sevm.py @@ -2,6 +2,7 @@ from z3 import * +from halmos.exceptions import OutOfGasError from halmos.utils import EVM from halmos.sevm import ( @@ -328,6 +329,17 @@ def test_stack_underflow_pop(sevm: SEVM, solver, storage): list(sevm.run(ex)) +def test_large_memory_offset(sevm: SEVM, solver, storage): + # check that we get an exception when popping from an empty stack + for op in [o(EVM.MLOAD), o(EVM.MSTORE), o(EVM.MSTORE8)]: + ex = mk_ex(op, sevm, solver, storage, caller, this) + ex.st.stack.append(con(42)) # value, ignored by MLOAD + ex.st.stack.append(con(2**64)) # offset too big to fit in memory + + exs = list(sevm.run(ex)) + assert len(exs) == 1 and isinstance(exs[0].context.output.error, OutOfGasError) + + def test_iter_bytes_bv_val(): b = BitVecVal(0x12345678, 32) assert list(iter_bytes(b)) == [0x12, 0x34, 0x56, 0x78]