From a0b91da20afed481c77de4d612385ac46a7bb0f0 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Mon, 30 Apr 2018 20:57:16 +0200 Subject: [PATCH] Add reacheability check and check if the expression is used in a requires statement --- mythril/analysis/modules/integer.py | 25 ++++++++++++++----------- 1 file changed, 14 insertions(+), 11 deletions(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index f0ec4a7c..3b33a1b7 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -30,7 +30,7 @@ def execute(statespace): for state in node.states: logging.debug("Checking for integer underflow") - issues += _check_integer_underflow(statespace, state, node) + # issues += _check_integer_underflow(statespace, state, node) logging.debug("Checking for integer overflow") issues += _check_integer_overflow(statespace, state, node) @@ -270,14 +270,19 @@ def _search_children(statespace, node, expression, constraint=[], index=0, depth current_state = node.states[j] current_instruction = current_state.get_current_instruction() if current_instruction['opcode'] in ('JUMPI', 'SSTORE'): - results += _check_usage(current_state, expression) - - # Recursively search children + element = _check_usage(current_state, expression) + if len(element) < 1: + continue + if _check_requires(element[0], node, statespace, constraint): + continue + results += element + + # Recursively search children children = \ [ statespace.nodes[edge.node_to] for edge in statespace.edges - if edge.node_from == node.uid and _try_constraints(node.constraints, constraint) + if edge.node_from == node.uid and _try_constraints(statespace.nodes[edge.node_to].constraints, constraint) is not None ] for child in children: @@ -289,17 +294,15 @@ def _search_children(statespace, node, expression, constraint=[], index=0, depth def _check_requires(state, node, statespace, constraint): """Checks if usage of overflowed statement results in a revert statement""" instruction = state.get_current_instruction() - if instruction['opcode'] != 'JUMPI': + if instruction['opcode'] is not "JUMPI": return False - - children = \ - [ + children = [ statespace.nodes[edge.node_to] for edge in statespace.edges - if edge.node_from == node.uid and _try_constraints(node.constraints, [constraint]) + if edge.node_from == node.uid and _try_constraints(statespace.nodes[edge.node_to].constraints, constraint) is not None ] for child in children: opcodes = [s.get_current_instruction()['opcode'] for s in child.states] - if "REVERT" in opcodes: + if "REVERT" in opcodes or "ASSERT_FAIL" in opcodes: return True return False