Add SMT simplifications for bitvec subtraction (#2504)

* Add SMT simplifications for bitvec subtraction

* Replace operator SUB by built-in '-'

* Use '==' instead of 'is' to test bitvector equality

* Lint

* Use custom exception when __bool__ fails to evaluate expression

manticore/core/smtlib/expression.py

@@ -15,6 +15,14 @@ class ExpressionException(SmtlibError):
     pass
 
 
+class ExpressionEvalError(SmtlibError):
+    """Exception raised when an expression can't be concretized, typically
+    when calling __bool__() fails to produce a True/False boolean result
+    """
+
+    pass
+
+
 class XSlotted(type):
     """
     Metaclass that will propagate slots on multi-inheritance classes
@@ -65,7 +73,7 @@ def __new__(cls, clsname, bases, attrs, abstract=False):
 
 
 class Expression(object, metaclass=XSlotted, abstract=True):
-    """ Abstract taintable Expression. """
+    """Abstract taintable Expression."""
 
     __xslots__: Tuple[str, ...] = ("_taint",)
 
@@ -214,7 +222,7 @@ def __bool__(self):
         x = simplify(self)
         if isinstance(x, Constant):
             return x.value
-        raise NotImplementedError("__bool__ for Bool")
+        raise ExpressionEvalError("__bool__ for Bool")
 
 
 class BoolVariable(Bool):
@@ -259,7 +267,7 @@ def value(self):
 
 
 class BoolOperation(Bool, abstract=True):
-    """ An operation that results in a Bool """
+    """An operation that results in a Bool"""
 
     __xslots__: Tuple[str, ...] = ("_operands",)
 
@@ -302,7 +310,7 @@ def __init__(self, *, cond: "Bool", true: "Bool", false: "Bool", **kwargs):
 
 
 class BitVec(Expression, abstract=True):
-    """ BitVector expressions have a fixed bit size """
+    """BitVector expressions have a fixed bit size"""
 
     __xslots__: Tuple[str, ...] = ("size",)
 
@@ -564,7 +572,7 @@ def signed_value(self):
 
 
 class BitVecOperation(BitVec, abstract=True):
-    """ An operation that results in a BitVec """
+    """An operation that results in a BitVec"""
 
     __xslots__: Tuple[str, ...] = ("_operands",)
 

manticore/core/smtlib/visitors.py

@@ -395,7 +395,7 @@ def visit_BoolAnd(self, expression, a, b):
             return a
 
     def _visit_operation(self, expression, *operands):
-        """ constant folding, if all operands of an expression are a Constant do the math """
+        """constant folding, if all operands of an expression are a Constant do the math"""
         operation = self.operations.get(type(expression), None)
         if operation is not None and all(isinstance(o, Constant) for o in operands):
             value = operation(*(x.value for x in operands))
@@ -438,7 +438,7 @@ def _changed(expression, operands):
         return any(operands[i] is not expression.operands[i] for i in range(arity))
 
     def _visit_operation(self, expression, *operands):
-        """ constant folding, if all operands of an expression are a Constant do the math """
+        """constant folding, if all operands of an expression are a Constant do the math"""
         if all(isinstance(o, Constant) for o in operands):
             expression = constant_folder(expression)
         if self._changed(expression, operands):
@@ -716,9 +716,10 @@ def visit_BitVecAdd(self, expression, *operands):
                 return right
 
     def visit_BitVecSub(self, expression, *operands):
-        """a - 0 ==> 0
+        """a - 0 ==> a
         (a + b) - b  ==> a
         (b + a) - b  ==> a
+        a - a ==> 0
         """
         left = operands[0]
         right = operands[1]
@@ -739,6 +740,16 @@ def visit_BitVecSub(self, expression, *operands):
                         taint=subright.taint | right.taint,
                     ),
                 )
+        elif isinstance(right, Constant) and right.value == 0:
+            return left
+        else:
+            # If equality can not be computed because of symbolic
+            # variables '==' will raise an exception
+            try:
+                if left == right:
+                    return BitVecConstant(size=left.size, value=0)
+            except ExpressionEvalError:
+                pass
 
     def visit_BitVecOr(self, expression, *operands):
         """a | 0 => a
@@ -1007,7 +1018,7 @@ def translate_to_smtlib(expression, **kwargs):
 
 
 class Replace(Visitor):
-    """ Simple visitor to replaces expressions """
+    """Simple visitor to replaces expressions"""
 
     def __init__(self, bindings=None, **kwargs):
         super().__init__(**kwargs)

tests/other/test_smtlibv2.py

@@ -848,6 +848,13 @@ def test_simplify_OR(self):
         cs.add(simplify(Operators.OR(var, bt)) == bt)
         self.assertTrue(self.solver.check(cs))
 
+    def test_simplify_SUB(self):
+        cs = ConstraintSet()
+        var = cs.new_bitvec(size=32)
+        cs.add(simplify(var - var) == 0)
+        cs.add(simplify(var - 0) == var)
+        self.assertTrue(self.solver.check(cs))
+
     def testBasicReplace(self):
         """ Add """
         a = BitVecConstant(size=32, value=100)