lint

src/halmos/calldata.py

@@ -2,7 +2,7 @@
 
 import re
 from collections.abc import Callable
-from dataclasses import dataclass, field
+from dataclasses import dataclass
 from functools import reduce
 
 from z3 import (
@@ -126,7 +126,8 @@ def get_dyn_sizes(self, name: str, typ: Type) -> tuple[list[int], BitVecRef]:
             sizes = (
                 list(range(self.args.loop + 1))
                 if isinstance(typ, DynamicArrayType)
-                else [0, 32, 1024, 65]  # bytes/string sizes # 65 is ECDSA signature size
+                # typ is bytes or string
+                else [0, 32, 1024, 65]  # 65 is ECDSA signature size
             )
             if self.args.debug:
                 print(
@@ -194,9 +195,7 @@ def encode(self, name: str, typ: Type) -> EncodingResult:
             items = [self.encode(f"{name}[{i}]", typ.base) for i in range(max(sizes))]
             encoded = self.encode_tuple(items)
             # generalized encoding for multiple sizes
-            return EncodingResult(
-                [size_var] + encoded.data, 32 + encoded.size, False
-            )
+            return EncodingResult([size_var] + encoded.data, 32 + encoded.size, False)
 
         if isinstance(typ, BaseType):
             new_symbol = f"p_{name}_{typ.typ}_{self.new_symbol_id():>02}"

src/halmos/cheatcodes.py

@@ -25,8 +25,6 @@
 from .assertions import assert_cheatcode_handler
 from .bytevec import ByteVec
 from .calldata import (
-    DynamicArrayType,
-    DynamicParam,
     FunctionInfo,
     find_abi,
     mk_calldata,
@@ -232,10 +230,13 @@ def create_calldata_contract(ex, arg, sevm, stack, step_id):
 
 def create_calldata_contract_bool(ex, arg, sevm, stack, step_id):
     contract_name = name_of(extract_string_argument(arg, 0))
-    include_view_functions = bool(int_of(
-        extract_bytes(arg, 4+32, 32), "symbolic boolean flag for SVM.createCalldata()"
-    ))
-    return create_calldata_generic(ex, arg, sevm, stack, step_id, contract_name, include_view_functions=include_view_functions)
+    include_view = int_of(
+        extract_bytes(arg, 4 + 32 * 1, 32),
+        "symbolic boolean flag for SVM.createCalldata()",
+    )
+    return create_calldata_generic(
+        ex, arg, sevm, stack, step_id, contract_name, include_view=bool(include_view)
+    )
 
 
 def create_calldata_file_contract(ex, arg, sevm, stack, step_id):
@@ -249,16 +250,17 @@ def create_calldata_file_contract(ex, arg, sevm, stack, step_id):
 def create_calldata_file_contract_bool(ex, arg, sevm, stack, step_id):
     filename = name_of(extract_string_argument(arg, 0))
     contract_name = name_of(extract_string_argument(arg, 1))
-    include_view_functions = bool(int_of(
-        extract_bytes(arg, 4+32*2, 32), "symbolic boolean flag for SVM.createCalldata()"
-    ))
+    include_view = int_of(
+        extract_bytes(arg, 4 + 32 * 2, 32),
+        "symbolic boolean flag for SVM.createCalldata()",
+    )
     return create_calldata_generic(
-        ex, arg, sevm, stack, step_id, contract_name, filename, include_view_functions
+        ex, arg, sevm, stack, step_id, contract_name, filename, bool(include_view)
     )
 
 
 def create_calldata_generic(
-    ex, arg, sevm, stack, step_id, contract_name, filename=None, include_view_functions=False
+    ex, arg, sevm, stack, step_id, contract_name, filename=None, include_view=False
 ):
     """
     Generate arbitrary symbolic calldata for the given contract.
@@ -280,7 +282,7 @@ def create_calldata_generic(
         funselector = methodIdentifiers[funsig]
         funinfo = FunctionInfo(funname, funsig, funselector)
 
-        if not include_view_functions:
+        if not include_view:
             fun_abi = find_abi(abi, funinfo)
             if fun_abi["stateMutability"] in ["pure", "view"]:
                 continue

src/halmos/sevm.py

@@ -42,12 +42,12 @@
     Xor,
     ZeroExt,
     eq,
+    is_eq,
     is_false,
     is_true,
     sat,
     simplify,
     unsat,
-    is_eq,
 )
 from z3.z3util import is_expr_var