TheDude
/
mythril
mirror of https://github.com/ConsenSys/mythril
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Rename BitVecFunc.input to BitVecFunc.input_

Browse Source
pull/901/head
Nathan 6 years ago
parent 25a7774b12
commit 5bfd7fe392
4 changed files with 50 additions and 41 deletions
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Show Stats Download Patch File Download Diff File
  1. 4
      mythril/laser/ethereum/instructions.py
  2. 35
      mythril/laser/smt/__init__.py
  3. 38
      mythril/laser/smt/bitvec.py
  4. 14
      mythril/laser/smt/bitvecfunc.py

4
mythril/laser/ethereum/instructions.py
Unescape View File

@ -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)))

35
mythril/laser/smt/__init__.py
Unescape View File

@ -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]):

38
mythril/laser/smt/bitvec.py
Unescape View File

@ -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,
)

14
mythril/laser/smt/bitvecfunc.py
Unescape View File

@ -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":

Write Preview
Loading…
Cancel
Save