Merge branch 'develop' into enhance/941

mythril/analysis/modules/integer.py

@@ -2,12 +2,15 @@
 underflows."""
 
 import json
+
+from math import log2, ceil
 from typing import Dict, cast, List
 from mythril.analysis import solver
 from mythril.analysis.report import Issue
 from mythril.analysis.swc_data import INTEGER_OVERFLOW_AND_UNDERFLOW
 from mythril.exceptions import UnsatError
 from mythril.laser.ethereum.state.global_state import GlobalState
+from mythril.laser.ethereum.util import get_concrete_int
 from mythril.laser.ethereum.state.annotation import StateAnnotation
 from mythril.analysis.modules.base import DetectionModule
 
@@ -19,6 +22,8 @@ from mythril.laser.smt import (
     symbol_factory,
     Not,
     Expression,
+    Bool,
+    And,
 )
 
 import logging
@@ -31,7 +36,7 @@ class OverUnderflowAnnotation:
     """ Symbol Annotation used if a BitVector can overflow"""
 
     def __init__(
-        self, overflowing_state: GlobalState, operator: str, constraint
+        self, overflowing_state: GlobalState, operator: str, constraint: Bool
     ) -> None:
         self.overflowing_state = overflowing_state
         self.operator = operator
@@ -42,7 +47,7 @@ class OverUnderflowStateAnnotation(StateAnnotation):
     """ State Annotation used if an overflow is both possible and used in the annotated path"""
 
     def __init__(
-        self, overflowing_state: GlobalState, operator: str, constraint
+        self, overflowing_state: GlobalState, operator: str, constraint: Bool
     ) -> None:
         self.overflowing_state = overflowing_state
         self.operator = operator
@@ -63,7 +68,7 @@ class IntegerOverflowUnderflowModule(DetectionModule):
                 "there's a possible state where op1 + op0 > 2^32 - 1"
             ),
             entrypoint="callback",
-            pre_hooks=["ADD", "MUL", "SUB", "SSTORE", "JUMPI", "STOP", "RETURN"],
+            pre_hooks=["ADD", "MUL", "EXP", "SUB", "SSTORE", "JUMPI", "STOP", "RETURN"],
         )
         self._overflow_cache = {}  # type: Dict[int, bool]
         self._underflow_cache = {}  # type: Dict[int, bool]
@@ -88,25 +93,30 @@ class IntegerOverflowUnderflowModule(DetectionModule):
         has_underflow = self._underflow_cache.get(address, False)
         if has_overflow or has_underflow:
             return
-        if state.get_current_instruction()["opcode"] == "ADD":
+        opcode = state.get_current_instruction()["opcode"]
-            self._handle_add(state)
+        funcs = {
-        elif state.get_current_instruction()["opcode"] == "MUL":
+            "ADD": [self._handle_add],
-            self._handle_mul(state)
+            "SUB": [self._handle_sub],
-        elif state.get_current_instruction()["opcode"] == "SUB":
+            "MUL": [self._handle_mul],
-            self._handle_sub(state)
+            "SSTORE": [self._handle_sstore],
-        elif state.get_current_instruction()["opcode"] == "SSTORE":
+            "JUMPI": [self._handle_jumpi],
-            self._handle_sstore(state)
+            "RETURN": [self._handle_return, self._handle_transaction_end],
-        elif state.get_current_instruction()["opcode"] == "JUMPI":
+            "STOP": [self._handle_transaction_end],
-            self._handle_jumpi(state)
+            "EXP": [self._handle_exp],
-        elif state.get_current_instruction()["opcode"] in ("RETURN", "STOP"):
+        }
-            self._handle_transaction_end(state)
+        for func in funcs[opcode]:
-
+            func(state)
-    def _handle_add(self, state):
+
+    def _get_args(self, state):
         stack = state.mstate.stack
         op0, op1 = (
             self._make_bitvec_if_not(stack, -1),
             self._make_bitvec_if_not(stack, -2),
         )
+        return op0, op1
+
+    def _handle_add(self, state):
+        op0, op1 = self._get_args(state)
         c = Not(BVAddNoOverflow(op0, op1, False))
 
         # Check satisfiable
@@ -118,12 +128,7 @@ class IntegerOverflowUnderflowModule(DetectionModule):
         op0.annotate(annotation)
 
     def _handle_mul(self, state):
-        stack = state.mstate.stack
+        op0, op1 = self._get_args(state)
-        op0, op1 = (
-            self._make_bitvec_if_not(stack, -1),
-            self._make_bitvec_if_not(stack, -2),
-        )
-
         c = Not(BVMulNoOverflow(op0, op1, False))
 
         # Check satisfiable
@@ -135,11 +140,7 @@ class IntegerOverflowUnderflowModule(DetectionModule):
         op0.annotate(annotation)
 
     def _handle_sub(self, state):
-        stack = state.mstate.stack
+        op0, op1 = self._get_args(state)
-        op0, op1 = (
-            self._make_bitvec_if_not(stack, -1),
-            self._make_bitvec_if_not(stack, -2),
-        )
         c = Not(BVSubNoUnderflow(op0, op1, False))
 
         # Check satisfiable
@@ -150,6 +151,33 @@ class IntegerOverflowUnderflowModule(DetectionModule):
         annotation = OverUnderflowAnnotation(state, "subtraction", c)
         op0.annotate(annotation)
 
+    def _handle_exp(self, state):
+        op0, op1 = self._get_args(state)
+        if op0.symbolic and op1.symbolic:
+            constraint = And(
+                op1 > symbol_factory.BitVecVal(256, 256),
+                op0 > symbol_factory.BitVecVal(1, 256),
+            )
+        elif op1.symbolic:
+            if op0.value < 2:
+                return
+            constraint = op1 >= symbol_factory.BitVecVal(
+                ceil(256 / log2(op0.value)), 256
+            )
+        elif op0.symbolic:
+            if op1.value == 0:
+                return
+            constraint = op0 >= symbol_factory.BitVecVal(
+                2 ** ceil(256 / op1.value), 256
+            )
+        else:
+            constraint = op0.value ** op1.value >= 2 ** 256
+        model = self._try_constraints(state.node.constraints, [constraint])
+        if model is None:
+            return
+        annotation = OverUnderflowAnnotation(state, "exponentiation", constraint)
+        op0.annotate(annotation)
+
     @staticmethod
     def _make_bitvec_if_not(stack, index):
         value = stack[index]
@@ -185,7 +213,6 @@ class IntegerOverflowUnderflowModule(DetectionModule):
     def _handle_sstore(state: GlobalState) -> None:
         stack = state.mstate.stack
         value = stack[-2]
-
         if not isinstance(value, Expression):
             return
         for annotation in value.annotations:
@@ -215,6 +242,31 @@ class IntegerOverflowUnderflowModule(DetectionModule):
                 )
             )
 
+    @staticmethod
+    def _handle_return(state: GlobalState) -> None:
+        """
+        Adds all the annotations into the state which correspond to the
+        locations in the memory returned by RETURN opcode.
+        :param state: The Global State
+        """
+        stack = state.mstate.stack
+        try:
+            offset, length = get_concrete_int(stack[-1]), get_concrete_int(stack[-2])
+        except TypeError:
+            return
+        for element in state.mstate.memory[offset : offset + length]:
+            if not isinstance(element, Expression):
+                continue
+            for annotation in element.annotations:
+                if isinstance(annotation, OverUnderflowAnnotation):
+                    state.annotate(
+                        OverUnderflowStateAnnotation(
+                            annotation.overflowing_state,
+                            annotation.operator,
+                            annotation.constraint,
+                        )
+                    )
+
     def _handle_transaction_end(self, state: GlobalState) -> None:
         for annotation in cast(
             List[OverUnderflowStateAnnotation],

mythril/laser/ethereum/instructions.py

@@ -519,16 +519,22 @@ class Instruction:
         base, exponent = util.pop_bitvec(state), util.pop_bitvec(state)
 
         if base.symbolic or exponent.symbolic:
+
             state.stack.append(
                 global_state.new_bitvec(
                     "(" + str(simplify(base)) + ")**(" + str(simplify(exponent)) + ")",
                     256,
+                    base.annotations + exponent.annotations,
                 )
             )
         else:
 
             state.stack.append(
-                symbol_factory.BitVecVal(pow(base.value, exponent.value, 2 ** 256), 256)
+                symbol_factory.BitVecVal(
+                    pow(base.value, exponent.value, 2 ** 256),
+                    256,
+                    annotations=base.annotations + exponent.annotations,
+                )
             )
 
         return [global_state]
@@ -1296,7 +1302,7 @@ class Instruction:
 
         try:
             value_to_write = (
-                util.get_concrete_int(value) ^ 0xFF
+                util.get_concrete_int(value) % 256
             )  # type: Union[int, BitVec]
         except TypeError:  # BitVec
             value_to_write = Extract(7, 0, value)

mythril/laser/ethereum/state/global_state.py

@@ -111,7 +111,7 @@ class GlobalState:
         """
         return self.get_current_instruction()
 
-    def new_bitvec(self, name: str, size=256) -> BitVec:
+    def new_bitvec(self, name: str, size=256, annotations=None) -> BitVec:
         """
 
         :param name:
@@ -119,7 +119,9 @@ class GlobalState:
         :return:
         """
         transaction_id = self.current_transaction.id
-        return symbol_factory.BitVecSym("{}_{}".format(transaction_id, name), size)
+        return symbol_factory.BitVecSym(
+            "{}_{}".format(transaction_id, name), size, annotations=annotations
+        )
 
     def annotate(self, annotation: StateAnnotation) -> None:
         """

mythril/laser/ethereum/state/world_state.py

@@ -117,7 +117,7 @@ class WorldState:
         :return:
         """
         while True:
-            address = "0x" + "".join([str(hex(randint(0, 16)))[-1] for _ in range(20)])
+            address = "0x" + "".join([str(hex(randint(0, 16)))[-1] for _ in range(40)])
             if address not in self.accounts.keys():
                 return address