From 2256fb3d5c2944a5ffd3dfaccb23aeacb64444fe Mon Sep 17 00:00:00 2001
From: Daejun Park <daejunpark@gmail.com>
Date: Fri, 13 Sep 2024 09:54:59 -0700
Subject: [PATCH] refactor: explicitly return dyn_params + todo comment arrlen

---
 src/halmos/__main__.py   |  7 +++----
 src/halmos/calldata.py   | 30 ++++++++++++++++--------------
 src/halmos/cheatcodes.py |  4 +---
 3 files changed, 20 insertions(+), 21 deletions(-)

diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py
index e7df3941..9979393c 100644
--- a/src/halmos/__main__.py
+++ b/src/halmos/__main__.py
@@ -428,8 +428,8 @@ def setup(
 
     setup_sig = setup_info.sig
     if setup_sig:
-        dyn_params = []  # TODO: propagate to run
-        calldata = mk_calldata(abi, setup_info, dyn_params, args)
+        # TODO: dyn_params may need to be passed to mk_calldata in run()
+        calldata, dyn_params = mk_calldata(abi, setup_info, args)
         setup_ex.path.process_dyn_params(dyn_params, legacy=True)
 
         parent_message = setup_ex.message()
@@ -568,8 +568,7 @@ def run(
     path = Path(solver)
     path.extend_path(setup_ex.path)
 
-    dyn_params = []  # to be populated by mk_calldata
-    cd = mk_calldata(abi, fun_info, dyn_params, args)
+    cd, dyn_params = mk_calldata(abi, fun_info, args)
     path.process_dyn_params(dyn_params, legacy=True)
 
     message = Message(
diff --git a/src/halmos/calldata.py b/src/halmos/calldata.py
index e601d57f..d33fca1b 100644
--- a/src/halmos/calldata.py
+++ b/src/halmos/calldata.py
@@ -104,20 +104,26 @@ class FunctionInfo:
 
 class Calldata:
     args: HalmosConfig
+
+    # `arrlen` holds the parsed value of --array-lengths, specifying the sizes for certain dynamic parameters.
+    # For dynamic parameters not listed in --array-lengths, default sizes are applied.
+    # `dyn_params` contains the fully resolved size information for all dynamic parameters.
+    # TODO: Extend `args` to include `arrlen` to avoid re-parsing --array-lengths multiple times.
     arrlen: dict[str, list[int]]
-    dyn_params: list[DynamicParam]  # to be updated
+    dyn_params: list[DynamicParam]
+
+    # Counter for generating unique symbol names.
+    # Required for create_calldata cheatcodes, which may be called multiple times.
     new_symbol_id: Callable
 
     def __init__(
         self,
         args: HalmosConfig,
-        arrlen: dict[str, list[int]],
-        dyn_params: list[DynamicParam],
         new_symbol_id: Callable | None,
     ) -> None:
         self.args = args
-        self.arrlen = arrlen
-        self.dyn_params = dyn_params
+        self.arrlen = mk_arrlen(args)
+        self.dyn_params = []
         self.new_symbol_id = new_symbol_id if new_symbol_id else lambda: ""
 
     def get_dyn_sizes(self, name: str, typ: Type) -> tuple[list[int], BitVecRef]:
@@ -147,7 +153,7 @@ def get_dyn_sizes(self, name: str, typ: Type) -> tuple[list[int], BitVecRef]:
 
         return (sizes, size_var)
 
-    def create(self, abi: dict, fun_info: FunctionInfo) -> ByteVec:
+    def create(self, abi: dict, fun_info: FunctionInfo) -> tuple[ByteVec, list[DynamicParam]]:
         """Create calldata of the given function"""
 
         # function selector
@@ -160,7 +166,7 @@ def create(self, abi: dict, fun_info: FunctionInfo) -> ByteVec:
 
         # no parameters
         if not tuple_type.items:
-            return calldata
+            return calldata, self.dyn_params
 
         starting_size = len(calldata)
 
@@ -174,7 +180,7 @@ def create(self, abi: dict, fun_info: FunctionInfo) -> ByteVec:
         if calldata_size != encoded.size:
             raise ValueError(encoded)
 
-        return calldata
+        return calldata, self.dyn_params
 
     def encode(self, name: str, typ: Type) -> EncodingResult:
         """Create symbolic ABI encoded calldata
@@ -317,14 +323,10 @@ def get_abi(contract_json: dict) -> dict:
 def mk_calldata(
     abi: dict,
     fun_info: FunctionInfo,
-    dyn_params: list[DynamicParam],
     args: HalmosConfig,
-    arrlen: dict[str, list[int]] = None,
     new_symbol_id: Callable = None,
-) -> None:
-    arrlen = mk_arrlen(args) if arrlen is None else arrlen
-    calldata = Calldata(args, arrlen, dyn_params, new_symbol_id)
-    return calldata.create(abi, fun_info)
+) -> tuple[ByteVec, list[DynamicParam]]:
+    return Calldata(args, new_symbol_id).create(abi, fun_info)
 
 
 def mk_arrlen(args: HalmosConfig) -> dict[str, list[int]]:
diff --git a/src/halmos/cheatcodes.py b/src/halmos/cheatcodes.py
index 251e8d13..a6b3afd9 100644
--- a/src/halmos/cheatcodes.py
+++ b/src/halmos/cheatcodes.py
@@ -312,11 +312,9 @@ def create_calldata_generic(ex, sevm, contract_name, filename=None, include_view
             if fun_abi["stateMutability"] in ["pure", "view"]:
                 continue
 
-        dyn_params = []  # to be populated by mk_calldata
-        calldata = mk_calldata(
+        calldata, dyn_params = mk_calldata(
             abi,
             funinfo,
-            dyn_params,
             sevm.options,
             new_symbol_id=ex.new_symbol_id,
         )