Fix constant folding & constraint set slicing

examples/script/concolic.py

@@ -22,6 +22,8 @@
 from manticore.core.plugin import ExtendedTracer, Follower, Plugin
 from manticore.core.smtlib.constraints import ConstraintSet
 from manticore.core.smtlib.solver import Z3Solver
+from manticore.core.smtlib.visitors import GetDeclarations
+
 from manticore.utils import config
 
 import copy
@@ -136,8 +138,17 @@ def perm(lst, func):
 
 
 def constraints_to_constraintset(constupl):
+    # originally those constraints belonged to a different ConstraintSet
+    # This is a hack
     x = ConstraintSet()
-    x._constraints = list(constupl)
+
+    declarations = GetDeclarations()
+    for a in constupl:
+        declarations.visit(a)
+        x.add(a)
+    for d in declarations.result:
+        x._declare(d)
+
     return x
 
 

manticore/core/manticore.py

@@ -525,7 +525,7 @@ def verbosity(level):
         set_verbosity(level)
 
     # State storage
-    @Eventful.will_did("save_state")
+    @Eventful.will_did("save_state", can_raise=False)
     def _save(self, state, state_id=None):
         """ Store or update a state in secondary storage under state_id.
             Use a fresh id is None is provided.
@@ -538,7 +538,7 @@ def _save(self, state, state_id=None):
         state._id = self._workspace.save_state(state, state_id=state_id)
         return state.id
 
-    @Eventful.will_did("load_state")
+    @Eventful.will_did("load_state", can_raise=False)
     def _load(self, state_id):
         """ Load the state from the secondary storage
 
@@ -557,7 +557,7 @@ def _load(self, state_id):
         self.stcache[state_id] = state
         return state
 
-    @Eventful.will_did("remove_state")
+    @Eventful.will_did("remove_state", can_raise=False)
     def _remove(self, state_id):
         """ Remove a state from secondary storage
 

manticore/core/smtlib/constraints.py

@@ -1,9 +1,11 @@
 import itertools
 import sys
-
+import copy
+from typing import Optional
 from ...utils.helpers import PickleSerializer
 from ...exceptions import SmtlibError
 from .expression import (
+    Expression,
     BitVecVariable,
     BoolVariable,
     ArrayVariable,
@@ -16,19 +18,19 @@
     Variable,
     Constant,
 )
-from .visitors import GetDeclarations, TranslatorSmtlib, get_variables, simplify, replace
+from .visitors import (
+    GetDeclarations,
+    TranslatorSmtlib,
+    get_variables,
+    simplify,
+    replace,
+    pretty_print,
+)
 from ...utils import config
 import logging
 
 logger = logging.getLogger(__name__)
 
-consts = config.get_group("smt")
-consts.add(
-    "related_constraints",
-    default=False,
-    description="Try slicing the current path constraint to contain only related items",
-)
-
 
 class ConstraintException(SmtlibError):
     """
@@ -115,7 +117,7 @@ def _get_sid(self) -> int:
         self._sid += 1
         return self._sid
 
-    def __get_related(self, related_to=None):
+    def related_to(self, *related_to) -> "ConstraintSet":
         # sam.moelius: There is a flaw in how __get_related works: when called on certain
         # unsatisfiable sets, it can return a satisfiable one. The flaw arises when:
         #   * self consists of a single constraint C
@@ -127,49 +129,59 @@ def __get_related(self, related_to=None):
         # set. Thus, __get_related was called on an unsatisfiable set, {C}, but it returned a
         # satisfiable one, {}.
         #   In light of the above, the core __get_related logic is currently disabled.
-        # if related_to is not None:
-        # feliam: This assumes the previous constraints are already SAT (normal SE forking)
-        if consts.related_constraints and related_to is not None:
-            number_of_constraints = len(self.constraints)
-            remaining_constraints = set(self.constraints)
-            related_variables = get_variables(related_to)
-            related_constraints = set()
-
-            added = True
-            while added:
-                added = False
-                logger.debug("Related variables %r", [x.name for x in related_variables])
-                for constraint in list(remaining_constraints):
-                    if isinstance(constraint, BoolConstant):
-                        if constraint.value:
-                            continue
-                        else:
-                            related_constraints = {constraint}
-                            break
-
-                    variables = get_variables(constraint)
-                    if related_variables & variables or not (variables):
-                        remaining_constraints.remove(constraint)
-                        related_constraints.add(constraint)
-                        related_variables |= variables
-                        added = True
-
-            logger.debug(
-                "Reduced %d constraints!!", number_of_constraints - len(related_constraints)
-            )
-        else:
-            related_variables = set()
-            for constraint in self.constraints:
-                related_variables |= get_variables(constraint)
-            related_constraints = set(self.constraints)
-        return related_variables, related_constraints
-
-    def to_string(self, related_to=None, replace_constants=False):
-        related_variables, related_constraints = self.__get_related(related_to)
+        """
+        Slices this ConstraintSet keeping only the related constraints.
+        Two constraints are independient if they can be expressed full using a
+        disjoint set of variables.
+        Todo: Research. constraints refering differen not overlapping parts of the same array
+        should be considered independient.
+        :param related_to: An expression
+        :return:
+        """
+
+        if not related_to:
+            return copy.copy(self)
+        number_of_constraints = len(self.constraints)
+        remaining_constraints = set(self.constraints)
+        related_variables = set()
+        for expression in related_to:
+            related_variables |= get_variables(expression)
+        related_constraints = set()
+
+        added = True
+        while added:
+            added = False
+            logger.debug("Related variables %r", [x.name for x in related_variables])
+            for constraint in list(remaining_constraints):
+                if isinstance(constraint, BoolConstant):
+                    if constraint.value:
+                        continue
+                    else:
+                        related_constraints = {constraint}
+                        break
+
+                variables = get_variables(constraint)
+                if related_variables & variables or not (variables):
+                    remaining_constraints.remove(constraint)
+                    related_constraints.add(constraint)
+                    related_variables |= variables
+                    added = True
+
+        logger.debug("Reduced %d constraints!!", number_of_constraints - len(related_constraints))
+        # related_variables, related_constraints
+        cs = ConstraintSet()
+        for var in related_variables:
+            cs._declare(var)
+        for constraint in related_constraints:
+            cs.add(constraint)
+        return cs
+
+    def to_string(self, replace_constants: bool = False) -> str:
+        variables, constraints = self.get_declared_variables(), self.constraints
 
         if replace_constants:
             constant_bindings = {}
-            for expression in related_constraints:
+            for expression in constraints:
                 if (
                     isinstance(expression, BoolEqual)
                     and isinstance(expression.operands[0], Variable)
@@ -179,16 +191,17 @@ def to_string(self, related_to=None, replace_constants=False):
 
         tmp = set()
         result = ""
-        for var in related_variables:
+        for var in variables:
             # FIXME
             # band aid hack around the fact that we are double declaring stuff :( :(
             if var.declaration in tmp:
                 logger.warning("Variable '%s' was copied twice somewhere", var.name)
                 continue
             tmp.add(var.declaration)
             result += var.declaration + "\n"
+
         translator = TranslatorSmtlib(use_bindings=True)
-        for constraint in related_constraints:
+        for constraint in constraints:
             if replace_constants:
                 constraint = simplify(replace(constraint, constant_bindings))
                 # if no variables then it is a constant

manticore/core/smtlib/expression.py

@@ -504,6 +504,13 @@ def __hash__(self):
     def value(self):
         return self._value
 
+    @property
+    def signed_value(self):
+        if self._value & self.signmask:
+            return self._value - (1 << self.size)
+        else:
+            return self._value
+
 
 class BitVecOperation(BitVec):
     __slots__ = ["_operands"]
@@ -960,50 +967,45 @@ def value(self):
         return self.operands[2]
 
 
-class ArraySlice(Array):
+class ArraySlice(ArrayOperation):
     def __init__(
         self, array: Union["Array", "ArrayProxy"], offset: int, size: int, *args, **kwargs
     ):
         if not isinstance(array, Array):
             raise ValueError("Array expected")
         if isinstance(array, ArrayProxy):
             array = array._array
-        super().__init__(array.index_bits, array.index_max, array.value_bits, *args, **kwargs)
+        super().__init__(array, **kwargs)
 
-        self._array = array
         self._slice_offset = offset
         self._slice_size = size
 
     @property
-    def underlying_variable(self):
-        return self._array.underlying_variable
+    def array(self):
+        return self.operands[0]
 
     @property
-    def operands(self):
-        return self._array.operands
+    def underlying_variable(self):
+        return self.array.underlying_variable
 
     @property
     def index_bits(self):
-        return self._array.index_bits
+        return self.array.index_bits
 
     @property
     def index_max(self):
         return self._slice_size
 
     @property
     def value_bits(self):
-        return self._array.value_bits
-
-    @property
-    def taint(self):
-        return self._array.taint
+        return self.array.value_bits
 
     def select(self, index):
-        return self._array.select(index + self._slice_offset)
+        return self.array.select(index + self._slice_offset)
 
     def store(self, index, value):
         return ArraySlice(
-            self._array.store(index + self._slice_offset, value),
+            self.array.store(index + self._slice_offset, value),
             self._slice_offset,
             self._slice_size,
         )
@@ -1048,7 +1050,7 @@ def name(self):
 
     @property
     def operands(self):
-        return self._array.operands
+        return (self._array,)
 
     @property
     def index_bits(self):
@@ -1145,13 +1147,13 @@ def written(self):
             # take out Proxy sleve
             array = self._array
             offset = 0
-            while isinstance(array, ArraySlice):
-                # if it is a proxy over a slice take out the slice too
-                offset += array._slice_offset
-                array = array._array
             while not isinstance(array, ArrayVariable):
-                # The index written to underlaying Array are displaced when sliced
-                written.add(array.index - offset)
+                if isinstance(array, ArraySlice):
+                    # if it is a proxy over a slice take out the slice too
+                    offset += array._slice_offset
+                else:
+                    # The index written to underlaying Array are displaced when sliced
+                    written.add(array.index - offset)
                 array = array.array
             assert isinstance(array, ArrayVariable)
             self._written = written