feat: support for new cheatcode of generating calldata

examples/simple/test/SimpleState.t.sol

@@ -0,0 +1,48 @@
+// SPDX-License-Identifier: AGPL-3.0
+pragma solidity >=0.8.0 <0.9.0;
+
+import "forge-std/Test.sol";
+import {SymTest} from "halmos-cheatcodes/SymTest.sol";
+
+//
+// Example from ItyFuzz paper (Figure 2): https://arxiv.org/pdf/2306.17135
+//
+
+contract SimpleState {
+    uint counter = 0;
+
+    function incr(uint x) public {
+        require(x <= counter);
+        counter += 1;
+    }
+
+    function decr(uint x) public {
+        require(x >= counter);
+        counter -= 1;
+    }
+}
+
+contract SimpleStateTest is SymTest, Test {
+    address target;
+
+    function setUp() public {
+        target = address(new SimpleState());
+    }
+
+    function buggy() public returns (bool) {
+        uint counter = uint(vm.load(target, bytes32(0)));
+        return counter == 10;
+    }
+
+    function check_buggy() public {
+        bool success;
+
+        // note: a total of 253 feasible paths are generated, of which only 10 unique states exist
+        for (uint i = 0; i < 10; i++) {
+            (success,) = target.call(svm.createCalldata("SimpleState"));
+            vm.assume(success);
+        }
+
+        assertFalse(buggy());
+    }
+}

examples/tokens/ERC721/test/ERC721Test.sol

@@ -14,7 +14,7 @@ abstract contract ERC721Test is SymTest, Test {
 
     function setUp() public virtual;
 
-    function check_NoBackdoor(bytes4 selector) public virtual {
+    function _check_NoBackdoor(bytes memory _calldata) public virtual {
         // consider caller and other that are distinct
         address caller = svm.createAddress('caller');
         address other = svm.createAddress('other');
@@ -34,13 +34,7 @@ abstract contract ERC721Test is SymTest, Test {
 
         // consider an arbitrary function call to the token from the caller
         vm.prank(caller);
-        bool success;
-        if (uint32(selector) == 0xb88d4fde) { // TODO: support parameters of type bytes or dynamic arrays
-            (success,) = address(token).call(abi.encodeWithSelector(selector, svm.createAddress('from'), svm.createAddress('to'), svm.createUint256('tokenId'), svm.createBytes(96, 'data')));
-        } else {
-            bytes memory args = svm.createBytes(1024, 'args');
-            (success,) = address(token).call(abi.encodePacked(selector, args));
-        }
+        (bool success,) = address(token).call(_calldata);
         vm.assume(success);
 
         // ensure that the caller cannot spend other's tokens

examples/tokens/ERC721/test/OpenZeppelinERC721.t.sol

@@ -41,4 +41,9 @@ contract OpenZeppelinERC721Test is ERC721Test {
         vm.prank(accounts[1]);
         token_.setApprovalForAll(accounts[2], true);
     }
+
+    function check_NoBackdoor() public {
+        bytes memory _calldata = svm.createCalldata("OpenZeppelinERC721");
+        _check_NoBackdoor(_calldata);
+    }
 }

examples/tokens/ERC721/test/SoladyERC721.t.sol

@@ -43,4 +43,9 @@ contract SoladyERC721Test is ERC721Test {
         vm.prank(accounts[1]);
         token_.setApprovalForAll(accounts[2], true);
     }
+
+    function check_NoBackdoor() public {
+        bytes memory _calldata = svm.createCalldata("SoladyERC721");
+        _check_NoBackdoor(_calldata);
+    }
 }

examples/tokens/ERC721/test/SolmateERC721.t.sol

@@ -43,4 +43,9 @@ contract SolmateERC721Test is ERC721Test {
         vm.prank(accounts[1]);
         token_.setApprovalForAll(accounts[2], true);
     }
+
+    function check_NoBackdoor() public {
+        bytes memory _calldata = svm.createCalldata("SolmateERC721");
+        _check_NoBackdoor(_calldata);
+    }
 }

src/halmos/__main__.py

@@ -35,11 +35,11 @@
 )
 
 from .bytevec import ByteVec
-from .calldata import Calldata
+from .calldata import DynamicParams, FunctionInfo, mk_calldata
 from .config import Config as HalmosConfig
 from .config import arg_parser, default_config, resolve_config_files, toml_parser
 from .exceptions import HalmosException
-from .mapper import DeployAddressMapper, Mapper
+from .mapper import BuildOut, DeployAddressMapper, Mapper
 from .sevm import (
     EMPTY_BALANCE,
     EVM,
@@ -168,61 +168,6 @@ def load_config(_args) -> HalmosConfig:
     return config
 
 
-@dataclass(frozen=True)
-class FunctionInfo:
-    name: str | None = None
-    sig: str | None = None
-    selector: str | None = None
-
-
-def str_abi(item: dict) -> str:
-    def str_tuple(args: list) -> str:
-        ret = []
-        for arg in args:
-            typ = arg["type"]
-            match = re.search(r"^tuple((\[[0-9]*\])*)$", typ)
-            if match:
-                ret.append(str_tuple(arg["components"]) + match.group(1))
-            else:
-                ret.append(typ)
-        return "(" + ",".join(ret) + ")"
-
-    if item["type"] != "function":
-        raise ValueError(item)
-    return item["name"] + str_tuple(item["inputs"])
-
-
-def find_abi(abi: list, fun_info: FunctionInfo) -> dict:
-    funname, funsig = fun_info.name, fun_info.sig
-    for item in abi:
-        if (
-            item["type"] == "function"
-            and item["name"] == funname
-            and str_abi(item) == funsig
-        ):
-            return item
-    raise ValueError(f"No {funsig} found in {abi}")
-
-
-def mk_calldata(
-    abi: list,
-    fun_info: FunctionInfo,
-    cd: ByteVec,
-    dyn_param_size: list[str],
-    args: HalmosConfig,
-) -> None:
-    # find function abi
-    fun_abi = find_abi(abi, fun_info)
-
-    # no parameters
-    if len(fun_abi["inputs"]) == 0:
-        return
-
-    # generate symbolic ABI calldata
-    calldata = Calldata(args, mk_arrlen(args), dyn_param_size)
-    calldata.create(fun_abi, cd)
-
-
 def mk_block() -> Block:
     # foundry default values
     block = Block(
@@ -486,7 +431,7 @@ def setup(
         calldata = ByteVec()
         calldata.append(int(setup_selector, 16).to_bytes(4, "big"))
 
-        dyn_param_size = []  # TODO: propagate to run
+        dyn_param_size = DynamicParams()  # TODO: propagate to run
         mk_calldata(abi, setup_info, calldata, dyn_param_size, args)
 
         parent_message = setup_ex.message()
@@ -623,7 +568,7 @@ def run(
     cd = ByteVec()
     cd.append(int(funselector, 16).to_bytes(4, "big"))
 
-    dyn_param_size = []
+    dyn_param_size = DynamicParams()
     mk_calldata(abi, fun_info, cd, dyn_param_size, args)
 
     message = Message(
@@ -807,7 +752,7 @@ def future_callback(future_model):
 
     # print result
     print(
-        f"{passfail} {funsig} (paths: {len(result_exs)}, {time_info}, bounds: [{', '.join(dyn_param_size)}])"
+        f"{passfail} {funsig} (paths: {len(result_exs)}, {time_info}, bounds: [{dyn_param_size}])"
     )
 
     for idx, _, err in stuck:
@@ -860,9 +805,12 @@ class SetupAndRunSingleArgs:
     setup_args: HalmosConfig
     args: HalmosConfig
     libs: dict
+    build_out_map: dict
 
 
 def setup_and_run_single(fn_args: SetupAndRunSingleArgs) -> list[TestResult]:
+    BuildOut().set_build_out(fn_args.build_out_map)
+
     args = fn_args.args
     try:
         setup_ex = setup(
@@ -930,6 +878,8 @@ class RunArgs:
     contract_json: dict
     libs: dict
 
+    build_out_map: dict
+
 
 def run_parallel(run_args: RunArgs) -> list[TestResult]:
     args = run_args.args
@@ -958,6 +908,7 @@ def run_parallel(run_args: RunArgs) -> list[TestResult]:
             setup_config,
             with_devdoc(args, fun_info.sig, run_args.contract_json),
             libs,
+            run_args.build_out_map,
         )
         for fun_info in fun_infos
     ]
@@ -971,6 +922,8 @@ def run_parallel(run_args: RunArgs) -> list[TestResult]:
 
 
 def run_sequential(run_args: RunArgs) -> list[TestResult]:
+    BuildOut().set_build_out(run_args.build_out_map)
+
     args = run_args.args
     setup_info = extract_setup(run_args.methodIdentifiers)
 
@@ -1261,16 +1214,6 @@ def render_model(model: StrModel | str) -> str:
     return "".join(sorted(formatted)) if formatted else "∅"
 
 
-def mk_arrlen(args: HalmosConfig) -> dict[str, int]:
-    arrlen = {}
-    if args.array_lengths:
-        for assign in [x.split("=") for x in args.array_lengths.split(",")]:
-            name = assign[0].strip()
-            size = assign[1].strip()
-            arrlen[name] = int(size)
-    return arrlen
-
-
 def get_contract_type(
     ast_nodes: list, contract_name: str
 ) -> tuple[str | None, str | None]:
@@ -1592,6 +1535,7 @@ def on_signal(signum, frame):
             contract_args,
             contract_json,
             libs,
+            build_out_map,
         )
 
         enable_parallel = args.test_parallel and num_found > 1