feat: branching over symbolic call addresses (#349)

Co-authored-by: karmacoma <[email protected]>

.github/workflows/test.yml

@@ -54,4 +54,4 @@ jobs:
         run: python -m pip install -e .
 
       - name: Run pytest
-        run: pytest -v -k "not long and not ffi" --ignore=tests/lib --halmos-options="--debug -st ${{ matrix.parallel }} --storage-layout ${{ matrix.storage-layout }} ${{ matrix.cache-solver }} --solver-timeout-assertion 0 ${{ inputs.halmos-options }}" ${{ inputs.pytest-options }}
+        run: pytest -v -k "not long and not ffi" --ignore=tests/lib --halmos-options="-st ${{ matrix.parallel }} --solver-threads 1 --storage-layout ${{ matrix.storage-layout }} ${{ matrix.cache-solver }} --solver-timeout-assertion 0 ${{ inputs.halmos-options }}" ${{ inputs.pytest-options }}

src/halmos/__main__.py

@@ -196,7 +196,10 @@ def mk_caller(args: HalmosConfig) -> Address:
 
 
 def mk_this() -> Address:
-    return magic_address + 1
+    # NOTE: Do NOT remove the `con_addr()` wrapper.
+    #       The return type should be BitVecSort(160) as it is used as a key for ex.code.
+    #       The keys of ex.code are compared using structural equality with other BitVecRef addresses.
+    return con_addr(magic_address + 1)
 
 
 def mk_solver(args: HalmosConfig, logic="QF_AUFBV", ctx=None, assertion=False):
@@ -440,7 +443,7 @@ def deploy_test(
     # use the given deployed bytecode if --no-test-constructor is enabled
     if args.no_test_constructor:
         deployed_bytecode = Contract.from_hexcode(deployed_hexcode)
-        ex.code[this] = deployed_bytecode
+        ex.set_code(this, deployed_bytecode)
         ex.pgm = deployed_bytecode
         return ex
 
@@ -465,7 +468,7 @@ def deploy_test(
         )
 
     deployed_bytecode = Contract(returndata)
-    ex.code[this] = deployed_bytecode
+    ex.set_code(this, deployed_bytecode)
     ex.pgm = deployed_bytecode
 
     # reset vm state
@@ -582,7 +585,7 @@ def setup(
         for assign in [x.split("=") for x in args.reset_bytecode.split(",")]:
             addr = con_addr(int(assign[0].strip(), 0))
             new_hexcode = assign[1].strip()
-            setup_ex.code[addr] = Contract.from_hexcode(new_hexcode)
+            setup_ex.set_code(addr, Contract.from_hexcode(new_hexcode))
 
     if args.statistics:
         print(setup_timer.report())
@@ -692,7 +695,6 @@ def run(
             sha3s=setup_ex.sha3s.copy(),
             storages=setup_ex.storages.copy(),
             balances=setup_ex.balances.copy(),
-            calls=setup_ex.calls.copy(),
         )
     )
 
@@ -848,14 +850,6 @@ def future_callback(future_model):
         if args.debug:
             print("\n".join(jumpid_str(x) for x in logs.bounded_loops))
 
-    if logs.unknown_calls:
-        warn_code(
-            UNINTERPRETED_UNKNOWN_CALLS,
-            f"{funsig}: unknown calls have been assumed to be static: {', '.join(logs.unknown_calls)}",
-        )
-        if args.debug:
-            logs.print_unknown_calls()
-
     # print post-states
     if args.print_states:
         for idx, ex in enumerate(result_exs):
@@ -1094,7 +1088,7 @@ def solve(
             )
 
         with open(dump_filename, "w") as f:
-            if args.verbose >= 1:
+            if args.debug:
                 print(f"Writing SMT query to {dump_filename}")
             if args.cache_solver:
                 f.write("(set-option :produce-unsat-cores true)\n")
@@ -1108,7 +1102,7 @@ def solve(
                 f.write("(get-unsat-core)\n")
 
     if args.solver_command:
-        if args.verbose >= 1:
+        if args.debug:
             print(f"  Checking with external solver process")
             print(f"    {args.solver_command} {dump_filename} >{dump_filename}.out")
 
@@ -1128,7 +1122,7 @@ def solve(
             with open(f"{dump_filename}.out", "w") as f:
                 f.write(res_str)
 
-            if args.verbose >= 1:
+            if args.debug:
                 print(f"    {res_str_head}")
 
             if res_str_head == "unsat":

src/halmos/cheatcodes.py

@@ -477,22 +477,22 @@ def handle(sevm, ex, arg: ByteVec, stack, step_id) -> ByteVec | None:
             store_account = uint160(arg.get_word(4))
             store_slot = uint256(arg.get_word(36))
             store_value = uint256(arg.get_word(68))
-            store_account_addr = sevm.resolve_address_alias(ex, store_account)
-            if store_account_addr is None:
-                raise HalmosException(f"uninitialized account: {hexify(store_account)}")
+            store_account_alias = sevm.resolve_address_alias(
+                ex, store_account, stack, step_id, branching=False
+            )
 
-            sevm.sstore(ex, store_account_addr, store_slot, store_value)
+            sevm.sstore(ex, store_account_alias, store_slot, store_value)
             return ret
 
         # vm.load(address,bytes32)
         elif funsig == hevm_cheat_code.load_sig:
             load_account = uint160(arg.get_word(4))
             load_slot = uint256(arg.get_word(36))
-            load_account_addr = sevm.resolve_address_alias(ex, load_account)
-            if load_account_addr is None:
-                raise HalmosException(f"uninitialized account: {load_account}")
+            load_account_alias = sevm.resolve_address_alias(
+                ex, load_account, stack, step_id, branching=False
+            )
 
-            return ByteVec(sevm.sload(ex, load_account_addr, load_slot))
+            return ByteVec(sevm.sload(ex, load_account_alias, load_slot))
 
         # vm.fee(uint256)
         elif funsig == hevm_cheat_code.fee_sig:

src/halmos/config.py

@@ -153,23 +153,6 @@ class Config:
         metavar="NAME1=LENGTH1,NAME2=LENGTH2,...",
     )
 
-    # default set of selectors:
-    # - IERC721.onERC721Received
-    # - IERC1271.isValidSignature
-    # - IERC1155.onERC1155Received
-    # - IERC1155.onERC1155BatchReceived
-    uninterpreted_unknown_calls: str = arg(
-        help="use uninterpreted abstractions for unknown external calls with the given function signatures",
-        global_default="0x150b7a02,0x1626ba7e,0xf23a6e61,0xbc197c81",
-        metavar="SELECTOR1,SELECTOR2,...",
-    )
-
-    return_size_of_unknown_calls: int = arg(
-        help="set the byte size of return data from uninterpreted unknown external calls",
-        global_default=32,
-        metavar="BYTE_SIZE",
-    )
-
     storage_layout: str = arg(
         help="Select one of the available storage layout models. The generic model should only be necessary for vyper, huff, or unconventional storage patterns in yul.",
         global_default="solidity",
@@ -390,6 +373,25 @@ class Config:
         group=deprecated,
     )
 
+    # default set of selectors:
+    # - IERC721.onERC721Received
+    # - IERC1271.isValidSignature
+    # - IERC1155.onERC1155Received
+    # - IERC1155.onERC1155BatchReceived
+    uninterpreted_unknown_calls: str = arg(
+        help="(Deprecated; no-op) use uninterpreted abstractions for unknown external calls with the given function signatures",
+        global_default="0x150b7a02,0x1626ba7e,0xf23a6e61,0xbc197c81",
+        metavar="SELECTOR1,SELECTOR2,...",
+        group=deprecated,
+    )
+
+    return_size_of_unknown_calls: int = arg(
+        help="(Deprecated; no-op) set the byte size of return data from uninterpreted unknown external calls",
+        global_default=32,
+        metavar="BYTE_SIZE",
+        group=deprecated,
+    )
+
     ### Methods
 
     def __getattribute__(self, name):