From c35b6b35bdc02c26ad401f809d8d3645d74efdb9 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Tue, 14 May 2019 05:40:02 +0200 Subject: [PATCH] Correctly propagate annotations in sha3 (from indexed memory) --- .../analysis/modules/dependence_on_predictable_vars.py | 1 + mythril/laser/ethereum/instructions.py | 10 ++++------ 2 files changed, 5 insertions(+), 6 deletions(-) diff --git a/mythril/analysis/modules/dependence_on_predictable_vars.py b/mythril/analysis/modules/dependence_on_predictable_vars.py index 532682de..49b3a73c 100644 --- a/mythril/analysis/modules/dependence_on_predictable_vars.py +++ b/mythril/analysis/modules/dependence_on_predictable_vars.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( diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index c8090400..dcea0d20 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -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]