fix: calldata rendering bugfix, large memory offset bugfix (#242)

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,14 +1425,16 @@ 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)
 
         return result
 
     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)

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)))
 
 

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"

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]