Add a constraint class with solver

mythril/analysis/modules/dependence_on_predictable_vars.py

@@ -62,7 +62,7 @@ def execute(statespace):
 
         # Second check: blockhash
 
-        for constraint in call.node.constraints + [call.to]:
+        for constraint in call.node.constraints[:] + [call.to]:
             if "blockhash" in str(constraint):
                 description = "In the function `" + call.node.function_name + "` "
                 if "number" in str(constraint):

mythril/analysis/solver.py

@@ -2,15 +2,13 @@ from z3 import Solver, simplify, sat, unknown
 from mythril.exceptions import UnsatError
 import logging
 
+
 def get_model(constraints):
-    s = Solver()
-    s.set("timeout", 100000)
 
-    for constraint in constraints:
-        s.add(constraint)
-    result = s.check()
+    constraints.solver.set("timeout", 10000)
+    result = constraints.solver.check()
     if result == sat:
-        return s.model()
+        return constraints.solver.model()
     elif result == unknown:
         logging.info("Timeout encountered while solving expression using z3")
     raise UnsatError

mythril/laser/ethereum/instructions.py

@@ -951,6 +951,7 @@ class Instruction:
                 states.append(new_state)
             else:
                 logging.debug("Pruned unreachable states.")
+        del global_state
         return states
 
     @StateTransition()

mythril/laser/ethereum/state.py

@@ -1,4 +1,4 @@
-from z3 import BitVec, BitVecVal, Solver, ExprRef, sat
+from z3 import BitVec, BitVecVal, Solver, ExprRef, sat, unsat
 from mythril.disassembler.disassembly import Disassembly
 from copy import copy, deepcopy
 from enum import Enum
@@ -127,18 +127,64 @@ class Environment:
                     calldata_type=self.calldata_type)
 
 
+class Constraints(list):
+    def __init__(self, constraint_list=[], solver=None, possibility=None):
+        super(Constraints, self).__init__(constraint_list)
+        self.solver = solver or Solver()
+        self.solver.set("timeout", 1)
+        self.__possibility = possibility
+        if solver is None:
+            for constraint in constraint_list:
+                self.solver.add(constraint)
+
+    def check_possibility(self):
+        if self.__possibility is None:
+            self.__possibility = (self.solver.check() != unsat)
+        return self.__possibility
+
+    def append(self, constraint):
+        self.__possibility = None
+        super(Constraints, self).append(constraint)
+        self.solver.add(constraint)
+
+    def pop(self, index=-1):
+        raise NotImplementedError
+
+    def __copy__(self):
+        constraint_list = super(Constraints, self).copy()
+        solver = self.solver.translate(self.solver.ctx)
+        return Constraints(constraint_list, solver, self.__possibility)
+
+    def __deepcopy__(self, memodict={}):
+        constraint_list = super(Constraints, self).copy()
+        solver = self.solver.translate(self.solver.ctx)
+        return Constraints(constraint_list, solver)
+
+    def __add__(self, constraints):
+        """
+        Implement constraint concatenation if needed
+        """
+        raise NotImplementedError
+
+    def __iadd__(self, other):
+        """
+        Implement constraint concatenation if needed
+        """
+        raise NotImplementedError
+
+
 class MachineState:
     """
     MachineState represents current machine state also referenced to as \mu
     """
-    def __init__(self, gas):
+    def __init__(self, gas, pc=0, stack=[], memory=[], constraints=None, depth=0):
         """ Constructor for machineState """
-        self.pc = 0
-        self.stack = []
-        self.memory = []
+        self.pc = pc
+        self.stack = stack
+        self.memory = memory
         self.gas = gas
-        self.constraints = []
-        self.depth = 0
+        self.constraints = constraints or Constraints()
+        self.depth = depth
 
     def mem_extend(self, start, size):
         """
@@ -165,6 +211,10 @@ class MachineState:
 
         return values[0] if amount == 1 else values
 
+    def __deepcopy__(self, memodict={}):
+        return MachineState(gas=self.gas, pc=self.pc, stack=copy(self.stack), memory=copy(self.memory),
+                            constraints=copy(self.constraints), depth=self.depth)
+
     def __str__(self):
         return str(self.as_dict)
 

mythril/laser/ethereum/svm.py

@@ -102,7 +102,7 @@ class LaserEVM:
             except NotImplementedError:
                 logging.info("Encountered unimplemented instruction")
                 continue
-
+            new_states = [state for state in new_states if state.mstate.constraints.check_possibility()]
             self.manage_cfg(op_code, new_states)
 
             self.work_list += new_states