Correctly propagate annotations in sha3 (from indexed memory)

pull/1029/head
Bernhard Mueller 6 years ago
parent 982cb8ee74
commit c35b6b35bd
  1. 1
      mythril/analysis/modules/dependence_on_predictable_vars.py
  2. 10
      mythril/laser/ethereum/instructions.py

@ -118,6 +118,7 @@ def _analyze_states(state: GlobalState) -> list:
issues.append(issue)
elif opcode == "JUMPI":
for annotation in state.mstate.stack[-2].annotations:
if isinstance(annotation, PredictableValueAnnotation):
state.annotate(

@ -913,9 +913,7 @@ class Instruction:
if isinstance(op0, Expression):
op0 = simplify(op0)
state.stack.append(
symbol_factory.BitVecSym(
"KECCAC_mem[" + str(op0) + "]", 256, op0.annotations
)
symbol_factory.BitVecSym("KECCAC_mem[" + str(op0) + "]", 256)
)
gas_tuple = cast(Tuple, OPCODE_GAS["SHA3"])
state.min_gas_used += gas_tuple[0]
@ -947,7 +945,7 @@ class Instruction:
"keccak256",
256,
input_=data,
annotations=op0.annotations,
annotations=state.memory[index].annotations,
)
log.debug("Created BitVecFunc hash.")
@ -959,9 +957,9 @@ class Instruction:
"keccak256",
256,
input_=data,
annotations=op0.annotations,
annotations=state.memory[index].annotations,
)
log.debug("Computed SHA3 Hash: " + str(binascii.hexlify(keccak)))
log.info("Computed SHA3 Hash: " + str(binascii.hexlify(keccak)))
state.stack.append(result)
return [global_state]

Loading…
Cancel
Save