Add reacheability check and check if the expression is used in a requires statement

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