pull/1220/head
Nikhil 5 years ago
parent 9d9da324be
commit aee3e7b0ff
  1. 4
      mythril/laser/ethereum/instructions.py
  2. 8
      mythril/laser/ethereum/keccak_function_manager.py
  3. 2
      mythril/laser/ethereum/state/constraints.py

@ -1001,9 +1001,7 @@ class Instruction:
# length is 0; this only matters for input of the BitVecFuncVal # length is 0; this only matters for input of the BitVecFuncVal
data = symbol_factory.BitVecVal(0, 1) data = symbol_factory.BitVecVal(0, 1)
result, constraints = keccak_function_manager.create_keccak( result, constraints = keccak_function_manager.create_keccak(data, global_state)
data, length, global_state
)
state.stack.append(result) state.stack.append(result)
state.constraints += constraints state.constraints += constraints

@ -47,9 +47,9 @@ class KeccakFunctionManager:
self.keccak_vals[func(data)] = keccak self.keccak_vals[func(data)] = keccak
return keccak return keccak
def create_keccak(self, data: BitVec, length: int, global_state): def create_keccak(self, data: BitVec, global_state):
length = length * 8 length = data.size()
data = simplify(data) data = simplify(data)
if data.symbolic and simplify(data) not in global_state.topo_keys: if data.symbolic and simplify(data) not in global_state.topo_keys:
if data.size() != 512: if data.size() != 512:
@ -60,7 +60,7 @@ class KeccakFunctionManager:
if p1.symbolic and p1 not in global_state.topo_keys: if p1.symbolic and p1 not in global_state.topo_keys:
global_state.topo_keys.append(p1) global_state.topo_keys.append(p1)
self.keccak_parent[p1] = None self.keccak_parent[p1] = None
assert length == data.size()
constraints = [] constraints = []
try: try:
func, inverse = self.sizes[length] func, inverse = self.sizes[length]
@ -78,7 +78,7 @@ class KeccakFunctionManager:
self.size_values[length].append(keccak) self.size_values[length].append(keccak)
constraints.append(func(data) == keccak) constraints.append(func(data) == keccak)
constraints.append(flag_var) constraints.append(flag_var)
return func(data), constraints return keccak, constraints
if simplify(func(data)) not in global_state.topo_keys: if simplify(func(data)) not in global_state.topo_keys:
self.keccak_parent[simplify(func(data))] = data self.keccak_parent[simplify(func(data))] = data

@ -30,7 +30,7 @@ class Constraints(list):
super(Constraints, self).__init__(constraint_list) super(Constraints, self).__init__(constraint_list)
self._default_timeout = 100 self._default_timeout = 100
self._is_possible = is_possible self._is_possible = is_possible
self.weighted = [] # type: List[Bool] self.weighted = [] # type: List[Bool]
@property @property
def is_possible(self) -> bool: def is_possible(self) -> bool:

Loading…
Cancel
Save