Unsound symbolication - A general approach to handle symbolic imprecisions

examples/evm/minimal.py

@@ -1,4 +1,4 @@
-from manticore.ethereum import ManticoreEVM
+from manticore import ManticoreEVM
 
 ################ Script #######################
 

examples/script/concolic.py

@@ -72,6 +72,8 @@ def flip(constraint):
     assert len(equal.operands) == 2
     # assume they are the equal -> ite form that we produce on standard branches
     ite, forcepc = equal.operands
+    if not (isinstance(ite, BitVecITE) and isinstance(forcepc, BitVecConstant)):
+        return constraint
     assert isinstance(ite, BitVecITE) and isinstance(forcepc, BitVecConstant)
     assert len(ite.operands) == 3
     cond, iifpc, eelsepc = ite.operands

manticore/core/manticore.py

@@ -549,6 +549,31 @@ def _kill_state(self, state_id, delete=False):
         # wake up everyone waiting for a change in the state lists
         self._lock.notify_all()
 
+    @sync
+    def kill_state(self, state, delete=False):
+        """ Kill a state.
+             A state is moved from any list to the kill list or fully
+             removed from secondary storage
+
+            :param state_id: a estate id
+            :type state_id: int
+            :param delete: if true remove the state from the secondary storage
+            :type delete: bool
+        """
+        state_id = state.id
+        if state_id in self._busy_states:
+            self._busy_states.remove(state_id)
+        if state_id in self._terminated_states:
+            self._terminated_states.remove(state_id)
+        if state_id in self._ready_states:
+            self._ready_states.remove(state_id)
+
+        if delete:
+            self._remove(state_id)
+        else:
+            # add the state_id to the terminated list
+            self._killed_states.append(state_id)
+
     @property
     @sync
     def ready_states(self):
@@ -561,7 +586,8 @@ def ready_states(self):
 
         This means it is not possible to change the state used by Manticore with `states = list(m.ready_states)`.
         """
-        for state_id in self._ready_states:
+        _ready_states = self._ready_states
+        for state_id in _ready_states:
             state = self._load(state_id)
             yield state
             # Re-save the state in case the user changed its data
@@ -610,9 +636,9 @@ def _all_states(self):
         """ Only allowed at not running.
             (At running we can have states at busy)
         """
-        return (
-            tuple(self._ready_states) + tuple(self._terminated_states) + tuple(self._killed_states)
-        )
+        return tuple(self._ready_states) + tuple(
+            self._terminated_states
+        )  # + tuple(self._killed_states)
 
     @property
     @sync
@@ -634,6 +660,11 @@ def count_states(self):
         """ Total states count """
         return len(self._all_states)
 
+    @sync
+    def count_all_states(self):
+        """ Total states count """
+        return len(self._all_states)
+
     @sync
     def count_ready_states(self):
         """ Ready states count """
@@ -866,11 +897,9 @@ def kill_timeout(self, timeout=None):
             timer.cancel()
 
     @at_not_running
-    def run(self, timeout=None):
+    def run(self):
         """
         Runs analysis.
-
-        :param timeout: Analysis timeout, in seconds
         """
         # Delete state cache
         # The cached version of a state may get out of sync if a worker in a

manticore/core/smtlib/constraints.py

@@ -11,7 +11,7 @@
     BitVec,
     BoolConstant,
     ArrayProxy,
-    BoolEq,
+    BoolEqual,
     Variable,
     Constant,
 )
@@ -141,15 +141,16 @@ def __get_related(self, related_to=None):
         return related_variables, related_constraints
 
     def to_string(self, related_to=None, replace_constants=True):
+        replace_constants = False
         related_variables, related_constraints = self.__get_related(related_to)
 
         if replace_constants:
             constant_bindings = {}
-            for expression in self.constraints:
+            for expression in related_constraints:
                 if (
-                    isinstance(expression, BoolEq)
+                    isinstance(expression, BoolEqual)
                     and isinstance(expression.operands[0], Variable)
-                    and isinstance(expression.operands[1], Constant)
+                    and isinstance(expression.operands[1], (Variable, Constant))
                 ):
                     constant_bindings[expression.operands[0]] = expression.operands[1]
 
@@ -163,21 +164,19 @@ def to_string(self, related_to=None, replace_constants=True):
                 continue
             tmp.add(var.declaration)
             result += var.declaration + "\n"
-
         translator = TranslatorSmtlib(use_bindings=True)
         for constraint in related_constraints:
             if replace_constants:
-                if (
-                    isinstance(constraint, BoolEq)
-                    and isinstance(constraint.operands[0], Variable)
-                    and isinstance(constraint.operands[1], Constant)
-                ):
-                    var = constraint.operands[0]
-                    expression = constraint.operands[1]
-                    expression = simplify(replace(expression, constant_bindings))
-                    constraint = var == expression
+                constraint = simplify(replace(constraint, constant_bindings))
+                # if no variables then it is a constant
+                if isinstance(constraint, Constant) and constraint.value == True:
+                    continue
 
             translator.visit(constraint)
+        if replace_constants:
+            for k, v in constant_bindings.items():
+                translator.visit(k == v)
+
         for name, exp, smtlib in translator.bindings:
             if isinstance(exp, BitVec):
                 result += f"(declare-fun {name} () (_ BitVec {exp.size}))"

manticore/core/smtlib/expression.py

@@ -178,7 +178,7 @@ def __invert__(self):
         return BoolNot(self)
 
     def __eq__(self, other):
-        return BoolEq(self, self.cast(other))
+        return BoolEqual(self, self.cast(other))
 
     def __hash__(self):
         return object.__hash__(self)
@@ -236,7 +236,7 @@ def __init__(self, value, **kwargs):
         super().__init__(value, **kwargs)
 
 
-class BoolEq(BoolOperation):
+class BoolEqual(BoolOperation):
     def __init__(self, a, b, **kwargs):
         super().__init__(a, b, **kwargs)
 
@@ -403,13 +403,13 @@ def __le__(self, other):
         return LessOrEqual(self, self.cast(other))
 
     def __eq__(self, other):
-        return Equal(self, self.cast(other))
+        return BoolEqual(self, self.cast(other))
 
     def __hash__(self):
         return object.__hash__(self)
 
     def __ne__(self, other):
-        return BoolNot(Equal(self, self.cast(other)))
+        return BoolNot(BoolEqual(self, self.cast(other)))
 
     def __gt__(self, other):
         return GreaterThan(self, self.cast(other))
@@ -591,9 +591,10 @@ def __init__(self, a, b, *args, **kwargs):
         super().__init__(a, b, *args, **kwargs)
 
 
-class Equal(BoolOperation):
+class BoolEqual(BoolOperation):
     def __init__(self, a, b, *args, **kwargs):
-        assert a.size == b.size
+        if isinstance(a, BitVec) or isinstance(b, BitVec):
+            assert a.size == b.size
         super().__init__(a, b, *args, **kwargs)
 
 
@@ -1001,16 +1002,7 @@ def taint(self):
         return self._array.taint
 
     def select(self, index):
-        index = self.cast_index(index)
-        if self.index_max is not None:
-            from .visitors import simplify
-
-            index = simplify(
-                BitVecITE(self.index_bits, index < 0, self.index_max + index + 1, index)
-            )
-        if isinstance(index, Constant) and index.value in self._concrete_cache:
-            return self._concrete_cache[index.value]
-        return self._array.select(index)
+        return self.get(index)
 
     def store(self, index, value):
         if not isinstance(index, Expression):
@@ -1040,6 +1032,9 @@ def __getitem__(self, index):
             for k, v in self._concrete_cache.items():
                 if k >= start and k < start + size:
                     array_proxy_slice._concrete_cache[k - start] = v
+
+            for i in self.written:
+                array_proxy_slice.written.add(i - start)
             return array_proxy_slice
         else:
             if self.index_max is not None:
@@ -1084,9 +1079,9 @@ def written(self):
             # take out Proxy sleve
             array = self._array
             offset = 0
-            if isinstance(array, ArraySlice):
+            while isinstance(array, ArraySlice):
                 # if it is a proxy over a slice take out the slice too
-                offset = array._slice_offset
+                offset += array._slice_offset
                 array = array._array
             while not isinstance(array, ArrayVariable):
                 # The index written to underlaying Array are displaced when sliced
@@ -1113,7 +1108,17 @@ def get(self, index, default=None):
         if default is None:
             default = self._default
         index = self.cast_index(index)
-        value = self.select(index)
+
+        if self.index_max is not None:
+            from .visitors import simplify
+
+            index = simplify(
+                BitVecITE(self.index_bits, index < 0, self.index_max + index + 1, index)
+            )
+        if isinstance(index, Constant) and index.value in self._concrete_cache:
+            return self._concrete_cache[index.value]
+
+        value = self._array.select(index)
         if default is None:
             return value
 

manticore/core/smtlib/operators.py

@@ -71,13 +71,6 @@ def OR(a, b, *others):
     return result
 
 
-def XOR(a, b):
-    result = a ^ b
-    if isinstance(result, (BitVec, int)):
-        result = ITE(result != 0, True, False)
-    return result
-
-
 def UGT(a, b):
     if isinstance(a, BitVec):
         return a.ugt(b)
@@ -208,6 +201,9 @@ def ITEBV(size, cond, true_value, false_value):
     assert isinstance(false_value, (BitVec, int))
     assert isinstance(size, int)
 
+    if isinstance(cond, BoolConstant) and not cond.taint:
+        cond = cond.value
+
     if isinstance(cond, bool):
         if cond:
             return true_value
@@ -263,12 +259,6 @@ def UREM(a, b):
     return a % b
 
 
-def simplify(value):
-    if issymbolic(value):
-        return value.simplify()
-    return value
-
-
 def SAR(size, a, b):
     assert isinstance(size, int)
     if isinstance(b, BitVec) and b.size != size: