lint

a16z · Aug 20, 2024 · 22e8334 · 22e8334
1 parent 9df14bc
commit 22e8334
Show file tree

Hide file tree

Showing 2 changed files with 37 additions and 28 deletions.
diff --git a/src/halmos/cheatcodes.py b/src/halmos/cheatcodes.py
@@ -477,7 +477,9 @@ def handle(sevm, ex, arg: ByteVec, stack, step_id) -> Optional[ByteVec]:
             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, stack, step_id)
+            store_account_addr = sevm.resolve_address_alias(
+                ex, store_account, stack, step_id
+            )
             if store_account_addr is None:
                 raise HalmosException(f"uninitialized account: {hexify(store_account)}")
 
@@ -488,7 +490,9 @@ def handle(sevm, ex, arg: ByteVec, stack, step_id) -> Optional[ByteVec]:
         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, stack, step_id)
+            load_account_addr = sevm.resolve_address_alias(
+                ex, load_account, stack, step_id
+            )
             if load_account_addr is None:
                 raise HalmosException(f"uninitialized account: {load_account}")
 

diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py
@@ -1517,12 +1517,16 @@ def sstore(self, ex: Exec, addr: Any, loc: Any, val: Any) -> None:
 
         self.storage_model.store(ex, addr, loc, val)
 
-    def resolve_address_alias(self, ex: Exec, target: Address, stack, step_id) -> Address:
+    def resolve_address_alias(
+        self, ex: Exec, target: Address, stack, step_id
+    ) -> Address:
         if target in ex.code:
             return target
 
         if self.options.debug:
-            debug(f"Address {hexify(target)} not in: [{", ".join([hexify(addr) for addr in ex.code])}]")
+            debug(
+                f"Address {hexify(target)} not in: [{', '.join([hexify(addr) for addr in ex.code])}]"
+            )
 
         if is_bv_value(target):
             if self.options.debug:
@@ -1537,10 +1541,12 @@ def resolve_address_alias(self, ex: Exec, target: Address, stack, step_id) -> Ad
             alias_cond = target == addr
             if ex.check(alias_cond) != unsat:
                 if self.options.debug:
-                    debug(f"Potential address alias: {hexify(addr)} for {hexify(target)}")
+                    debug(
+                        f"Potential address alias: {hexify(addr)} for {hexify(target)}"
+                    )
                 potential_aliases.append((addr, alias_cond))
 
-        emptyness_cond = And([ target != addr for addr in ex.code ])
+        emptyness_cond = And([target != addr for addr in ex.code])
         if ex.check(emptyness_cond) != unsat:
             if self.options.debug:
                 debug(f"Potential empty address: {hexify(target)}")
@@ -1587,12 +1593,7 @@ def transfer_value(
         ex.balance_update(to, self.arith(ex, EVM.ADD, ex.balance_of(to), value))
 
     def call(
-        self,
-        ex: Exec,
-        op: int,
-        stack: List[Tuple[Exec, int]],
-        step_id: int,
-        to_addr
+        self, ex: Exec, op: int, stack: List[Tuple[Exec, int]], step_id: int, to_addr
     ) -> None:
         gas = ex.st.pop()
         to = uint160(ex.st.pop())
@@ -1759,25 +1760,23 @@ def call_unknown() -> None:
                 exit_code = con(1)
                 modulus_size = int_of(extract_bytes(arg, 64, 32))
                 f_modexp = Function(
-                    f"f_modexp_{arg_size}_{modulus_size}", BitVecSorts[arg_size], BitVecSorts[modulus_size]
+                    f"f_modexp_{arg_size}_{modulus_size}",
+                    BitVecSorts[arg_size],
+                    BitVecSorts[modulus_size],
                 )
                 # TODO: empty returndata in error
                 ret = ByteVec(f_modexp(arg))
 
             # ecadd
             elif eq(to, con_addr(6)):
                 exit_code = con(1)
-                f_ecadd = Function(
-                    f"f_ecadd", BitVecSorts[1024], BitVecSorts[512]
-                )
+                f_ecadd = Function(f"f_ecadd", BitVecSorts[1024], BitVecSorts[512])
                 ret = ByteVec(f_ecadd(arg))
 
             # ecmul
             elif eq(to, con_addr(7)):
                 exit_code = con(1)
-                f_ecmul = Function(
-                    f"f_ecmul", BitVecSorts[768], BitVecSorts[512]
-                )
+                f_ecmul = Function(f"f_ecmul", BitVecSorts[768], BitVecSorts[512])
                 ret = ByteVec(f_ecmul(arg))
 
             # ecpairing
@@ -1791,9 +1790,7 @@ def call_unknown() -> None:
             # blake2f
             elif eq(to, con_addr(9)):
                 exit_code = con(1)
-                f_blake2f = Function(
-                    f"f_blake2f", BitVecSorts[1704], BitVecSorts[512]
-                )
+                f_blake2f = Function(f"f_blake2f", BitVecSorts[1704], BitVecSorts[512])
                 ret = ByteVec(f_blake2f(arg))
 
             # point_evaluation
@@ -1828,7 +1825,9 @@ def call_unknown() -> None:
                 ret = ByteVec()
 
             # push exit code
-            exit_code_var = BitVec(f"call_exit_code_{ex.new_call_id():>02}", BitVecSort256)
+            exit_code_var = BitVec(
+                f"call_exit_code_{ex.new_call_id():>02}", BitVecSort256
+            )
             ex.path.append(exit_code_var == exit_code)
             ex.st.push(exit_code if is_bv_value(exit_code) else exit_code_var)
 
@@ -1871,7 +1870,7 @@ def call_unknown() -> None:
         # precompiles or cheatcodes
         if (
             # precompile
-            (is_bv_value(to) and to.as_long() in range(1,11))
+            (is_bv_value(to) and to.as_long() in range(1, 11))
             # cheatcode calls
             or eq(to, halmos_cheat_code.address)
             or eq(to, hevm_cheat_code.address)
@@ -2346,7 +2345,9 @@ def finalize(ex: Exec):
                 # TODO: define f_extcodesize for known addresses in advance
                 elif opcode == EVM.EXTCODESIZE:
                     account = uint160(ex.st.peek())
-                    account_addr = self.resolve_address_alias(ex, account, stack, step_id)
+                    account_addr = self.resolve_address_alias(
+                        ex, account, stack, step_id
+                    )
                     ex.st.pop()
 
                     if account_addr is not None:
@@ -2356,15 +2357,17 @@ def finalize(ex: Exec):
                         or eq(account, halmos_cheat_code.address)
                         or eq(account, console.address)
                     ):
-                        codesize = 777 # dummy arbitrary value
+                        codesize = 777  # dummy arbitrary value
                     else:
                         codesize = 0
 
                     ex.st.push(codesize)
 
                 elif opcode == EVM.EXTCODECOPY:
                     account: Address = uint160(ex.st.peek())
-                    account_addr = self.resolve_address_alias(ex, account, stack, step_id)
+                    account_addr = self.resolve_address_alias(
+                        ex, account, stack, step_id
+                    )
                     ex.st.pop()
 
                     loc: int = int_of(ex.st.pop(), "symbolic EXTCODECOPY offset")
@@ -2390,7 +2393,9 @@ def finalize(ex: Exec):
 
                 elif opcode == EVM.EXTCODEHASH:
                     account_addr = uint160(ex.st.peek())
-                    alias_addr = self.resolve_address_alias(ex, account_addr, stack, step_id)
+                    alias_addr = self.resolve_address_alias(
+                        ex, account_addr, stack, step_id
+                    )
                     ex.st.pop()
 
                     addr = alias_addr if alias_addr is not None else account_addr