diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 03f0f9ee..cc718e4d 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -906,7 +906,7 @@ class Instruction: if data.symbolic: argument_str = str(state.memory[index]).replace(" ", "_") result = symbol_factory.BitVecFuncSym( - "KECCAC[{}]".format(argument_str), "keccak256", 256, input=data + "KECCAC[{}]".format(argument_str), "keccak256", 256, input_=data ) log.debug("Created BitVecFunc hash.") @@ -914,7 +914,7 @@ class Instruction: else: keccak = utils.sha3(data.value.to_bytes(length, byteorder="big")) result = symbol_factory.BitVecFuncVal( - "keccak256", util.concrete_int_from_bytes(keccak, 0), 256, input=data + util.concrete_int_from_bytes(keccak, 0), "keccak256", 256, input_=data ) log.debug("Computed SHA3 Hash: " + str(binascii.hexlify(keccak))) diff --git a/mythril/laser/smt/__init__.py b/mythril/laser/smt/__init__.py index 0f7ee8e2..e2f055e2 100644 --- a/mythril/laser/smt/__init__.py +++ b/mythril/laser/smt/__init__.py @@ -66,32 +66,39 @@ class SymbolFactory(Generic[T, U]): @staticmethod def BitVecFuncVal( - func_name: str, value: int, + func_name: str, size: int, annotations: Annotations = None, - input: Union[int, "BitVec"] = None, + input_: Union[int, "BitVec"] = None, ) -> BitVecFunc: - """Creates a new bit vector function with a concrete value. + """Creates a new bit vector function with a symbolic value. - :param func_name: The name of the function :param value: The concrete value to set the bit vector to + :param func_name: The name of the bit vector function :param size: The size of the bit vector :param annotations: The annotations to initialize the bit vector with - :return: The freshly created bit vector + :param input_: The input to the bit vector function + :return: The freshly created bit vector function """ raise NotImplementedError() @staticmethod def BitVecFuncSym( - name: str, func_name: str, size: int, annotations: Annotations = None - ) -> U: - """Creates a new bit vector with a symbolic value. + name: str, + func_name: str, + size: int, + annotations: Annotations = None, + input_: Union[int, "BitVec"] = None, + ) -> BitVecFunc: + """Creates a new bit vector function with a symbolic value. :param name: The name of the symbolic bit vector + :param func_name: The name of the bit vector function :param size: The size of the bit vector :param annotations: The annotations to initialize the bit vector with - :return: The freshly created bit vector + :param input_: The input to the bit vector function + :return: The freshly created bit vector function """ raise NotImplementedError() @@ -127,15 +134,15 @@ class _SmtSymbolFactory(SymbolFactory[bool.Bool, BitVec]): @staticmethod def BitVecFuncVal( - func_name: str, value: int, + func_name: str, size: int, annotations: Annotations = None, - input: Union[int, "BitVec"] = None, + input_: Union[int, "BitVec"] = None, ) -> BitVecFunc: """Creates a new bit vector function with a concrete value.""" raw = z3.BitVecVal(value, size) - return BitVecFunc(raw, func_name, input, annotations) + return BitVecFunc(raw, func_name, input_, annotations) @staticmethod def BitVecFuncSym( @@ -143,11 +150,11 @@ class _SmtSymbolFactory(SymbolFactory[bool.Bool, BitVec]): func_name: str, size: int, annotations: Annotations = None, - input: Union[int, "BitVec"] = None, + input_: Union[int, "BitVec"] = None, ) -> BitVecFunc: """Creates a new bit vector function with a symbolic value.""" raw = z3.BitVec(name, size) - return BitVecFunc(raw, func_name, input, annotations) + return BitVecFunc(raw, func_name, input_, annotations) class _Z3SymbolFactory(SymbolFactory[z3.BoolRef, z3.BitVecRef]): diff --git a/mythril/laser/smt/bitvec.py b/mythril/laser/smt/bitvec.py index c111fae8..c936bad4 100644 --- a/mythril/laser/smt/bitvec.py +++ b/mythril/laser/smt/bitvec.py @@ -228,13 +228,13 @@ def UGT(a: BitVec, b: BitVec) -> Bool: if ( not isinstance(b, BitVecFunc) or not a.func_name - or not a.input + or not a.input_ or not a.func_name == b.func_name ): return Bool(z3.BoolVal(False), annotations=annotations) return And( - Bool(z3.UGT(a.raw, b.raw), annotations=annotations), a.input != b.input + Bool(z3.UGT(a.raw, b.raw), annotations=annotations), a.input_ != b.input_ ) return Bool(z3.UGT(a.raw, b.raw), annotations) @@ -255,13 +255,13 @@ def UGE(a: BitVec, b: BitVec) -> Bool: if ( not isinstance(b, BitVecFunc) or not a.func_name - or not a.input + or not a.input_ or not a.func_name == b.func_name ): return Bool(z3.BoolVal(False), annotations=annotations) return And( - Bool(z3.UGE(a.raw, b.raw), annotations=annotations), a.input != b.input + Bool(z3.UGE(a.raw, b.raw), annotations=annotations), a.input_ != b.input_ ) return Bool(z3.UGE(a.raw, b.raw), annotations) @@ -282,13 +282,13 @@ def ULT(a: BitVec, b: BitVec) -> Bool: if ( not isinstance(b, BitVecFunc) or not a.func_name - or not a.input + or not a.input_ or not a.func_name == b.func_name ): return Bool(z3.BoolVal(False), annotations=annotations) return And( - Bool(z3.ULT(a.raw, b.raw), annotations=annotations), a.input != b.input + Bool(z3.ULT(a.raw, b.raw), annotations=annotations), a.input_ != b.input_ ) return Bool(z3.ULT(a.raw, b.raw), annotations) @@ -324,7 +324,7 @@ def Concat(*args: Union[BitVec, List[BitVec]]) -> BitVec: if bitvecfunc: # Is there a better value to set func_name and input to in this case? - return BitVecFunc(raw=nraw, func_name=None, input=None, annotations=annotations) + return BitVecFunc(raw=nraw, func_name=None, input_=None, annotations=annotations) return BitVec(nraw, annotations) @@ -340,7 +340,7 @@ def Extract(high: int, low: int, bv: BitVec) -> BitVec: raw = z3.Extract(high, low, bv.raw) if isinstance(bv, BitVecFunc): # Is there a better value to set func_name and input to in this case? - return BitVecFunc(raw=raw, func_name=None, input=None, annotations=bv.annotations) + return BitVecFunc(raw=raw, func_name=None, input_=None, annotations=bv.annotations) return BitVec(raw, annotations=bv.annotations) @@ -356,11 +356,11 @@ def URem(a: BitVec, b: BitVec) -> BitVec: union = a.annotations + b.annotations if isinstance(a, BitVecFunc) and isinstance(b, BitVecFunc): - return BitVecFunc(raw=raw, func_name=None, input=None, annotations=union) + return BitVecFunc(raw=raw, func_name=None, input_=None, annotations=union) elif isinstance(a, BitVecFunc): - return BitVecFunc(raw=raw, func_name=a.func_name, input=a.input, annotations=union) + return BitVecFunc(raw=raw, func_name=a.func_name, input_=a.input_, annotations=union) elif isinstance(b, BitVecFunc): - return BitVecFunc(raw=raw, func_name=b.func_name, input=b.input, annotations=union) + return BitVecFunc(raw=raw, func_name=b.func_name, input_=b.input_, annotations=union) return BitVec(raw, annotations=union) @@ -376,11 +376,11 @@ def SRem(a: BitVec, b: BitVec) -> BitVec: union = a.annotations + b.annotations if isinstance(a, BitVecFunc) and isinstance(b, BitVecFunc): - return BitVecFunc(raw=raw, func_name=None, input=None, annotations=union) + return BitVecFunc(raw=raw, func_name=None, input_=None, annotations=union) elif isinstance(a, BitVecFunc): - return BitVecFunc(raw=raw, func_name=a.func_name, input=a.input, annotations=union) + return BitVecFunc(raw=raw, func_name=a.func_name, input_=a.input_, annotations=union) elif isinstance(b, BitVecFunc): - return BitVecFunc(raw=raw, func_name=b.func_name, input=b.input, annotations=union) + return BitVecFunc(raw=raw, func_name=b.func_name, input_=b.input_, annotations=union) return BitVec(raw, annotations=union) @@ -396,11 +396,11 @@ def UDiv(a: BitVec, b: BitVec) -> BitVec: union = a.annotations + b.annotations if isinstance(a, BitVecFunc) and isinstance(b, BitVecFunc): - return BitVecFunc(raw=raw, func_name=None, input=None, annotations=union) + return BitVecFunc(raw=raw, func_name=None, input_=None, annotations=union) elif isinstance(a, BitVecFunc): - return BitVecFunc(raw=raw, func_name=a.func_name, input=a.input, annotations=union) + return BitVecFunc(raw=raw, func_name=a.func_name, input_=a.input_, annotations=union) elif isinstance(b, BitVecFunc): - return BitVecFunc(raw=raw, func_name=b.func_name, input=b.input, annotations=union) + return BitVecFunc(raw=raw, func_name=b.func_name, input_=b.input_, annotations=union) return BitVec(raw, annotations=union) @@ -420,12 +420,12 @@ def Sum(*args: BitVec) -> BitVec: bitvecfuncs.append(bv) if len(bitvecfuncs) >= 2: - return BitVecFunc(raw=raw, func_name=None, input=None, annotations=annotations) + return BitVecFunc(raw=raw, func_name=None, input_=None, annotations=annotations) elif len(bitvecfuncs) == 1: return BitVecFunc( raw=raw, func_name=bitvecfuncs[0].func_name, - input=bitvecfuncs[0].input, + input_=bitvecfuncs[0].input_, annotations=annotations, ) diff --git a/mythril/laser/smt/bitvecfunc.py b/mythril/laser/smt/bitvecfunc.py index dabf9d56..e1ff3525 100644 --- a/mythril/laser/smt/bitvecfunc.py +++ b/mythril/laser/smt/bitvecfunc.py @@ -27,9 +27,11 @@ def _arithmetic_helper( if isinstance(b, BitVecFunc): # TODO: Find better value to set input and name to in this case? - return BitVecFunc(raw=raw, func_name=None, input=None, annotations=union) + return BitVecFunc(raw=raw, func_name=None, input_=None, annotations=union) - return BitVecFunc(raw=raw, func_name=a.func_name, input=a.input, annotations=union) + return BitVecFunc( + raw=raw, func_name=a.func_name, input_=a.input_, annotations=union + ) def _comparison_helper( @@ -59,14 +61,14 @@ def _comparison_helper( if ( not isinstance(b, BitVecFunc) or not a.func_name - or not a.input + or not a.input_ or not a.func_name == b.func_name ): return Bool(z3.BoolVal(default_value), annotations=union) return And( Bool(cast(z3.BoolRef, operation(a.raw, b.raw)), annotations=union), - a.input == b.input if inputs_equal else a.input != b.input, + a.input_ == b.input_ if inputs_equal else a.input_ != b.input_, ) @@ -77,7 +79,7 @@ class BitVecFunc(BitVec): self, raw: z3.BitVecRef, func_name: Optional[str], - input: Union[int, "BitVec"] = None, + input_: Union[int, "BitVec"] = None, annotations: Optional[Annotations] = None, ): """ @@ -89,7 +91,7 @@ class BitVecFunc(BitVec): """ self.func_name = func_name - self.input = input + self.input_ = input_ super().__init__(raw, annotations) def __add__(self, other: Union[int, "BitVec"]) -> "BitVecFunc":