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/smtlib/constraints.py

@@ -1,9 +1,10 @@
 import itertools
 import sys
-
+from typing import Optional
 from ...utils.helpers import PickleSerializer
 from ...exceptions import SmtlibError
 from .expression import (
+    Expression,
     BitVecVariable,
     BoolVariable,
     ArrayVariable,
@@ -115,7 +116,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: Optional[Expression] = None):
         # 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 +128,57 @@ 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 related_to is None:
+            return self
+        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))
+
+        # 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=True):
+        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 +188,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/solver.py

@@ -435,7 +435,7 @@ def can_be_true(self, constraints: ConstraintSet, expression: Union[bool, Bool]
 
         with constraints as temp_cs:
             temp_cs.add(expression)
-            self._reset(temp_cs.to_string(related_to=expression))
+            self._reset(temp_cs.to_string())
             return self._is_sat()
 
     # get-all-values min max minmax
@@ -454,7 +454,7 @@ def get_all_values(self, constraints, expression, maxcnt=None, silent=False):
                 maxcnt = 2
                 silent = True
 
-        with constraints as temp_cs:
+        with constraints.related_to(expression) as temp_cs:
             if isinstance(expression, Bool):
                 var = temp_cs.new_bool()
             elif isinstance(expression, BitVec):
@@ -471,7 +471,7 @@ def get_all_values(self, constraints, expression, maxcnt=None, silent=False):
                 )
 
             temp_cs.add(var == expression)
-            self._reset(temp_cs.to_string(related_to=var))
+            self._reset(temp_cs.related_to(var).to_string())
             result = []
             start = time.time()
             while self._is_sat():
@@ -490,11 +490,20 @@ def get_all_values(self, constraints, expression, maxcnt=None, silent=False):
                 if time.time() - start > consts.timeout:
                     if silent:
                         logger.info("Timeout searching for all solutions")
-                        return result
+                        return (
+                            result
+                            / home
+                            / felipe
+                            / Projects
+                            / manticore
+                            / tests
+                            / other
+                            / test_smtlibv2.py
+                        )
                     raise SolverError("Timeout")
                 # Sometimes adding a new contraint after a check-sat eats all the mem
                 temp_cs.add(var != value)
-                self._reset(temp_cs.to_string(related_to=var))
+                self._reset(temp_cs.to_string())
                 # self._assert(var != value)
             return list(result)
 
@@ -516,8 +525,8 @@ def optimize(self, constraints: ConstraintSet, x: BitVec, goal: str, max_iter=10
             X = temp_cs.new_bitvec(x.size)
             temp_cs.add(X == x)
             aux = temp_cs.new_bitvec(X.size, name="optimized_")
-            self._reset(temp_cs.to_string(related_to=X))
-            self._send(aux.declaration)
+            self._reset(temp_cs.to_string())
+            # self._send(aux.declaration)
 
             start = time.time()
             if consts.optimize and getattr(self, f"support_{goal}", False):

manticore/core/smtlib/visitors.py

@@ -285,7 +285,6 @@ def __init__(self, **kw):
         BitVecAdd: operator.__add__,
         BitVecSub: operator.__sub__,
         BitVecMul: operator.__mul__,
-        BitVecDiv: operator.__floordiv__,
         BitVecShiftLeft: operator.__lshift__,
         BitVecShiftRight: operator.__rshift__,
         BitVecAnd: operator.__and__,
@@ -301,13 +300,29 @@ def __init__(self, **kw):
         BoolAnd: operator.__and__,
         BoolOr: operator.__or__,
         BoolNot: operator.__not__,
-        BitVecUnsignedDiv: lambda x, y: (x & UNSIGN_MASK) // (y & UNSIGN_MASK),
+        BitVecUnsignedDiv: lambda x, y: 0 if (y & UNSIGN_MASK) == 0 else (x & UNSIGN_MASK) // (y & UNSIGN_MASK),
         UnsignedLessThan: lambda x, y: (x & UNSIGN_MASK) < (y & UNSIGN_MASK),
         UnsignedLessOrEqual: lambda x, y: (x & UNSIGN_MASK) <= (y & UNSIGN_MASK),
         UnsignedGreaterThan: lambda x, y: (x & UNSIGN_MASK) > (y & UNSIGN_MASK),
         UnsignedGreaterOrEqual: lambda x, y: (x & UNSIGN_MASK) >= (y & UNSIGN_MASK),
     }
 
+    def visit_BitVecDiv(self, expression, *operands):
+        if all(isinstance(o, Constant) for o in operands):
+            signmask = operands[0].signmask
+            mask = operands[0].mask
+            numeral = operands[0].value
+            dividend = operands[1].value
+            if numeral & signmask:
+                numeral = -(mask - numeral - 1)
+            if dividend & signmask:
+                dividend = -(mask - dividend - 1)
+            if dividend == 0:
+                result = 0
+            else:
+                result = int(numeral / dividend)
+            return BitVecConstant(expression.size, result, taint=expression.taint)
+
     def visit_BitVecConcat(self, expression, *operands):
         if all(isinstance(o, Constant) for o in operands):
             result = 0

tests/other/test_smtlibv2.py

@@ -1,4 +1,5 @@
 import unittest
+import os
 
 from manticore.core.smtlib import (
     ConstraintSet,
@@ -11,15 +12,55 @@
     arithmetic_simplify,
     constant_folder,
     replace,
+    BitVecConstant,
 )
 from manticore.core.smtlib.solver import Z3Solver
 from manticore.core.smtlib.expression import *
 from manticore.utils.helpers import pickle_dumps
+from manticore import config
 
 # logging.basicConfig(filename = "test.log",
 #                format = "%(asctime)s: %(name)s:%(levelname)s: %(message)s",
 #                level = logging.DEBUG)
 
+DIRPATH = os.path.dirname(__file__)
+
+
+class RegressionTest(unittest.TestCase):
+    def test_related_to(self):
+        import gzip
+        import pickle, sys
+
+        filename = os.path.abspath(os.path.join(DIRPATH, "data", "ErrRelated.pkl.gz"))
+
+        constraints, constraint = pickle.loads(gzip.open(filename, "rb").read())
+
+        consts = config.get_group("smt")
+        consts.related_constraints = False
+
+        Z3Solver.instance().can_be_true.cache_clear()
+        ground_truth = Z3Solver.instance().can_be_true(constraints, constraint)
+        self.assertEqual(ground_truth, False)
+
+        consts.related_constraints = True
+        Z3Solver.instance().can_be_true.cache_clear()
+        self.assertEqual(ground_truth, Z3Solver.instance().can_be_true(constraints, constraint))
+
+        # Replace
+        new_constraint = Operators.UGE(
+            Operators.SEXTEND(BitVecConstant(256, 0x1A), 256, 512) * BitVecConstant(512, 1),
+            0x00000000000000000000000000000000000000000000000000000000000000010000000000000000000000000000000000000000000000000000000000000000,
+        )
+        self.assertEqual(translate_to_smtlib(constraint), translate_to_smtlib(new_constraint))
+
+        consts.related_constraints = False
+        Z3Solver.instance().can_be_true.cache_clear()
+        self.assertEqual(ground_truth, Z3Solver.instance().can_be_true(constraints, new_constraint))
+
+        consts.related_constraints = True
+        Z3Solver.instance().can_be_true.cache_clear()
+        self.assertEqual(ground_truth, Z3Solver.instance().can_be_true(constraints, new_constraint))
+
 
 class ExpressionTest(unittest.TestCase):
     _multiprocess_can_split_ = True
@@ -905,9 +946,8 @@ def test_SDIV(self):
         cs.add(b == 0x86)  # -122
         cs.add(c == 0x11)  # 17
         cs.add(a == Operators.SDIV(b, c))
-        cs.add(d == b / c)
+        cs.add(d == (b // c))
         cs.add(a == d)
-
         self.assertTrue(solver.check(cs))
         self.assertEqual(solver.get_value(cs, a), -7 & 0xFF)
 
@@ -986,6 +1026,33 @@ def test_check_solver_undefined(self):
         )
         self.assertTrue(self.solver._solver_version() > Version(major=4, minor=4, patch=1))
 
+    def testRelated(self):
+        cs = ConstraintSet()
+        aa1 = cs.new_bool(name="AA1")
+        aa2 = cs.new_bool(name="AA2")
+        bb1 = cs.new_bool(name="BB1")
+        bb2 = cs.new_bool(name="BB2")
+        cs.add(Operators.OR(aa1, aa2))
+        cs.add(Operators.OR(bb1, bb2))
+        self.assertTrue(self.solver.check(cs))
+        # No BB variables related to AA
+        self.assertNotIn("BB", cs.related_to(aa1).to_string())
+        self.assertNotIn("BB", cs.related_to(aa2).to_string())
+        self.assertNotIn("BB", cs.related_to(aa1 == aa2).to_string())
+        self.assertNotIn("BB", cs.related_to(aa1 == False).to_string())
+        # No AA variables related to BB
+        self.assertNotIn("AA", cs.related_to(bb1).to_string())
+        self.assertNotIn("AA", cs.related_to(bb2).to_string())
+        self.assertNotIn("AA", cs.related_to(bb1 == bb2).to_string())
+        self.assertNotIn("AA", cs.related_to(bb1 == False).to_string())
+
+        # Nothing is related to tautologies?
+        self.assertEqual("", cs.related_to(simplify(bb1 == bb1)).to_string())
+
+        # But if the tautollogy can not get simplified we have to ask the solver
+        # and send in all the other stuff
+        self.assertNotIn("AA", cs.related_to(bb1 == bb1).to_string())
+
     def test_API(self):
         """
         As we've split up the Constant, Variable, and Operation classes to avoid using multiple inheritance,