Replace specific Z3 hints with broader ExprRef

mythril/laser/ethereum/call.py

@@ -1,6 +1,6 @@
 import logging
 from typing import Union
-from z3 import simplify, BitVecRef, BitVecNumRef, BoolRef, Extract
+from z3 import simplify, ExprRef, Extract
 import mythril.laser.ethereum.util as util
 from mythril.laser.ethereum.state import Account, CalldataType, GlobalState, Calldata
 from mythril.support.loader import DynLoader
@@ -57,7 +57,7 @@ def get_call_parameters(
 
 
 def get_callee_address(
-    global_state: GlobalState, dynamic_loader: DynLoader, symbolic_to_address: BitVecRef
+    global_state: GlobalState, dynamic_loader: DynLoader, symbolic_to_address: ExprRef
 ):
     """
     Gets the address of the callee
@@ -143,8 +143,8 @@ def get_callee_account(
 
 def get_call_data(
     global_state: GlobalState,
-    memory_start: Union[int, BitVecNumRef, BoolRef],
-    memory_size: Union[int, BitVecNumRef, BoolRef],
+    memory_start: Union[int, ExprRef],
+    memory_size: Union[int, ExprRef],
     pad=True,
 ):
     """

mythril/laser/ethereum/instructions.py

@@ -1,7 +1,7 @@
 import binascii
 import logging
 from copy import copy, deepcopy
-from typing import Callable, List
+from typing import Callable, List, Union
 
 from ethereum import utils
 from z3 import (
@@ -886,7 +886,7 @@ class Instruction:
             return self._sload_helper(global_state, str(index))
 
     @staticmethod
-    def _sload_helper(global_state, index, constraints=None):
+    def _sload_helper(global_state: GlobalState, index: Union[int, ExprRef], constraints=None):
         try:
             data = global_state.environment.active_account.storage[index]
         except KeyError:

mythril/laser/ethereum/keccak.py

@@ -1,11 +1,11 @@
-from z3 import ExprRef, BitVecRef
+from z3 import ExprRef
 
 
 class KeccakFunctionManager:
     def __init__(self):
         self.keccak_expression_mapping = {}
 
-    def is_keccak(self, expression: BitVecRef) -> bool:
+    def is_keccak(self, expression: ExprRef) -> bool:
         return str(expression) in self.keccak_expression_mapping.keys()
 
     def get_argument(self, expression: str) -> ExprRef:

mythril/laser/ethereum/natives.py

@@ -3,7 +3,7 @@
 import copy
 import hashlib
 import logging
-from typing import List, Union
+from typing import Union
 
 from ethereum.utils import ecrecover_to_pub
 from py_ecc.secp256k1 import N as secp256k1n

mythril/laser/ethereum/state.py

@@ -149,7 +149,7 @@ class Storage:
         self._storage[item] = BitVec("storage_" + str(item), 256)
         return self._storage[item]
 
-    def __setitem__(self, key: str, value: BitVecRef) -> None:
+    def __setitem__(self, key: str, value: ExprRef) -> None:
         self._storage[key] = value
 
     def keys(self) -> KeysView:
@@ -194,10 +194,10 @@ class Account:
     def __str__(self) -> str:
         return str(self.as_dict)
 
-    def set_balance(self, balance: BitVecRef) -> None:
+    def set_balance(self, balance: ExprRef) -> None:
         self.balance = balance
 
-    def add_balance(self, balance: BitVecRef) -> None:
+    def add_balance(self, balance: ExprRef) -> None:
         self.balance += balance
 
     @property
@@ -218,11 +218,11 @@ class Environment:
     def __init__(
         self,
         active_account: Account,
-        sender: BitVecRef,
+        sender: ExprRef,
         calldata: Calldata,
-        gasprice: BitVecRef,
-        callvalue: BitVecRef,
-        origin: BitVecRef,
+        gasprice: ExprRef,
+        callvalue: ExprRef,
+        origin: ExprRef,
         code=None,
         calldata_type=CalldataType.SYMBOLIC,
     ):

mythril/laser/ethereum/taint_analysis.py

@@ -1,7 +1,7 @@
 import logging
 import copy
 from typing import Union, List, Tuple
-from z3 import BitVecNumRef
+from z3 import ExprRef
 import mythril.laser.ethereum.util as helper
 from mythril.laser.ethereum.cfg import JumpType, Node
 from mythril.laser.ethereum.state import GlobalState, Environment
@@ -238,7 +238,7 @@ class TaintRunner:
         record.stack[l], record.stack[i] = record.stack[i], record.stack[l]
 
     @staticmethod
-    def mutate_mload(record: TaintRecord, op0: BitVecNumRef) -> None:
+    def mutate_mload(record: TaintRecord, op0: ExprRef) -> None:
         _ = record.stack.pop()
         try:
             index = helper.get_concrete_int(op0)
@@ -250,7 +250,7 @@ class TaintRunner:
         record.stack.append(record.memory_tainted(index))
 
     @staticmethod
-    def mutate_mstore(record: TaintRecord, op0: BitVecNumRef) -> None:
+    def mutate_mstore(record: TaintRecord, op0: ExprRef) -> None:
         _, value_taint = record.stack.pop(), record.stack.pop()
         try:
             index = helper.get_concrete_int(op0)
@@ -261,7 +261,7 @@ class TaintRunner:
         record.memory[index] = value_taint
 
     @staticmethod
-    def mutate_sload(record: TaintRecord, op0: BitVecNumRef) -> None:
+    def mutate_sload(record: TaintRecord, op0: ExprRef) -> None:
         _ = record.stack.pop()
         try:
             index = helper.get_concrete_int(op0)
@@ -273,7 +273,7 @@ class TaintRunner:
         record.stack.append(record.storage_tainted(index))
 
     @staticmethod
-    def mutate_sstore(record: TaintRecord, op0: BitVecNumRef) -> None:
+    def mutate_sstore(record: TaintRecord, op0: ExprRef) -> None:
         _, value_taint = record.stack.pop(), record.stack.pop()
         try:
             index = helper.get_concrete_int(op0)

mythril/laser/ethereum/transaction/transaction_models.py

@@ -8,7 +8,7 @@ from mythril.laser.ethereum.state import (
     Account,
     Calldata,
 )
-from z3 import BitVec, BitVecNumRef
+from z3 import BitVec, ExprRef
 import array
 
 _next_transaction_id = 0
@@ -47,7 +47,7 @@ class MessageCallTransaction:
         self,
         world_state: WorldState,
         callee_account: Account,
-        caller: BitVecNumRef,
+        caller: ExprRef,
         call_data=None,
         identifier=None,
         gas_price=None,
@@ -119,7 +119,7 @@ class ContractCreationTransaction:
     def __init__(
         self,
         world_state: WorldState,
-        caller: BitVecNumRef,
+        caller: ExprRef,
         identifier=None,
         callee_account=None,
         code=None,

mythril/laser/ethereum/util.py

@@ -63,7 +63,7 @@ def pop_bitvec(state: "MachineState") -> BitVecVal:
         return simplify(item)
 
 
-def get_concrete_int(item: Union[int, BitVecNumRef, BoolRef]) -> int:
+def get_concrete_int(item: Union[int, ExprRef]) -> int:
     if isinstance(item, int):
         return item
     elif isinstance(item, BitVecNumRef):