accept review suggestions

src/halmos/calldata.py

@@ -127,9 +127,9 @@ def get_dyn_sizes(self, name: str, typ: Type) -> tuple[list[int], BitVecRef]:
         The candidates are derived from --array_lengths if provided; otherwise, default values are used.
         """
 
-        if name in self.arrlen:
-            sizes = self.arrlen[name]
-        else:
+        sizes = self.arrlen.get(name)
+
+        if sizes is None:
             sizes = (
                 list(range(self.args.loop + 1))
                 if isinstance(typ, DynamicArrayType)
@@ -152,7 +152,7 @@ def create(self, abi: dict, fun_info: FunctionInfo) -> ByteVec:
 
         # function selector
         calldata = ByteVec()
-        calldata.append(int(fun_info.selector, 16).to_bytes(4, "big"))
+        calldata.append(bytes.fromhex(fun_info.selector))
 
         # list of parameter types
         fun_abi = abi[fun_info.sig]

src/halmos/cheatcodes.py

@@ -226,7 +226,7 @@ def symbolic_storage(ex, arg, sevm, stack, step_id):
 
 def create_calldata_contract(ex, arg, sevm, stack, step_id):
     contract_name = name_of(extract_string_argument(arg, 0))
-    return create_calldata_generic(ex, arg, sevm, stack, step_id, contract_name)
+    return create_calldata_generic(ex, sevm, contract_name)
 
 
 def create_calldata_contract_bool(ex, arg, sevm, stack, step_id):
@@ -236,15 +236,15 @@ def create_calldata_contract_bool(ex, arg, sevm, stack, step_id):
         "symbolic boolean flag for SVM.createCalldata()",
     )
     return create_calldata_generic(
-        ex, arg, sevm, stack, step_id, contract_name, include_view=bool(include_view)
+        ex, sevm, contract_name, include_view=bool(include_view)
     )
 
 
 def create_calldata_file_contract(ex, arg, sevm, stack, step_id):
     filename = name_of(extract_string_argument(arg, 0))
     contract_name = name_of(extract_string_argument(arg, 1))
     return create_calldata_generic(
-        ex, arg, sevm, stack, step_id, contract_name, filename
+        ex, sevm, contract_name, filename
     )
 
 
@@ -256,12 +256,12 @@ def create_calldata_file_contract_bool(ex, arg, sevm, stack, step_id):
         "symbolic boolean flag for SVM.createCalldata()",
     )
     return create_calldata_generic(
-        ex, arg, sevm, stack, step_id, contract_name, filename, bool(include_view)
+        ex, sevm, contract_name, filename, bool(include_view)
     )
 
 
 def create_calldata_generic(
-    ex, arg, sevm, stack, step_id, contract_name, filename=None, include_view=False
+    ex, sevm, contract_name, filename=None, include_view=False
 ):
     """
     Generate arbitrary symbolic calldata for the given contract.

src/halmos/mapper.py

@@ -116,9 +116,9 @@ def get_by_name(self, contract_name: str, filename: str = None) -> dict:
 
         if filename is None:
             if len(mapping) > 1:
-                err_msg = f"{contract_name} exists in multiple files: {mapping.keys()}"
+                err_msg = f"{contract_name} exists in multiple files: {list(mapping.keys())}"
                 raise HalmosException(err_msg)
-            filename = list(mapping.keys())[0]
+            [filename] = mapping.keys()
 
         result = mapping.get(filename)
 

src/halmos/sevm.py

@@ -2115,10 +2115,11 @@ def call_unknown() -> None:
 
             ret_lst = ret if isinstance(ret, list) else [ret]
 
+            last_idx = len(ret_lst) - 1
             for idx, ret_ in enumerate(ret_lst):
                 new_ex = (
                     self.create_branch(ex, BoolVal(True), ex.pc)
-                    if idx < len(ret_lst) - 1
+                    if idx < last_idx
                     else ex
                 )
 

tests/regression/test/HalmosCheatCode.t.sol

@@ -141,7 +141,7 @@ contract HalmosCheatCodeTest is SymTest, Test {
 
     function check_createCalldata_Beep_1_excluding_pure() public {
         bytes memory data = svm.createCalldata("HalmosCheatCode.t.sol", "Beep");
-        _check_createCalldata_Beep(data); // fail // not reachable, no calldata generated above
+        _check_createCalldata_Beep(data); // fail because the only function in Beep is pure, which is excluded in createCalldata()
     }
 
     function check_createCalldata_Beep_1() public {
@@ -151,7 +151,7 @@ contract HalmosCheatCodeTest is SymTest, Test {
 
     function check_createCalldata_Beep_2_excluding_pure() public {
         bytes memory data = svm.createCalldata("Beep");
-        _check_createCalldata_Beep(data); // fail // not reachable, no calldata generated above
+        _check_createCalldata_Beep(data); // fail because the only function in Beep is pure, which is excluded in createCalldata()
     }
 
     function check_createCalldata_Beep_2() public {
@@ -162,6 +162,7 @@ contract HalmosCheatCodeTest is SymTest, Test {
     function _check_createCalldata_Beep(bytes memory data) public {
         Beep beep = new Beep();
         (bool success, bytes memory retdata) = address(beep).call(data);
+        vm.assume(success);
         uint ret = abi.decode(retdata, (uint256));
         assertEq(ret, 42);
     }
@@ -209,6 +210,7 @@ contract HalmosCheatCodeTest is SymTest, Test {
     function _check_createCalldata_Mock(bytes memory data) public {
         Mock mock = new Mock();
         (bool success, bytes memory retdata) = address(mock).call(data);
+        vm.assume(success);
 
         bytes4 ret = abi.decode(retdata, (bytes4));
         bytes4 expected = bytes4(bytes.concat(data[0], data[1], data[2], data[3]));