Add boolean simplifications (#2563)

* Add boolean simplifications

* Fix typo

* Lint tests

* Test remove simplifications

* Comment simplification tests to check eth bench tests

* Re-enable BoolEqual simplifications

* Fix BoolNot

* Fix tests

* Fix more tests

* Re-enable other boolean simplifications and tests

* Fix tests

* Fix tests

* Add multiplication simplification

* Fix tests

* Lint

* Improve docstrings

Co-authored-by: Eric Kilmer <eric.d.kilmer@gmail.com>

Co-authored-by: Eric Kilmer <eric.d.kilmer@gmail.com>

manticore/core/smtlib/visitors.py

@@ -503,13 +503,31 @@ def visit_BoolAnd(self, expression, *operands):
                         ) == BitVecExtract(operand=value1, offset=beg, size=end - beg + 1)
 
     def visit_BoolNot(self, expression, *operands):
+        """
+        !!a -> a
+        !(a&&b) -> !a || !b
+        !(a||b) -> !a && !b
+        """
         if isinstance(operands[0], BoolNot):
             return operands[0].operands[0]
 
+        if isinstance(operands[0], BoolAnd):
+            return BoolOr(
+                a=BoolNot(value=operands[0].operands[0]), b=BoolNot(value=operands[0].operands[1])
+            )
+
+        if isinstance(operands[0], BoolOr):
+            return BoolAnd(
+                a=BoolNot(value=operands[0].operands[0]), b=BoolNot(value=operands[0].operands[1])
+            )
+
     def visit_BoolEqual(self, expression, *operands):
         """(EQ, ITE(cond, constant1, constant2), constant1) -> cond
         (EQ, ITE(cond, constant1, constant2), constant2) -> NOT cond
         (EQ (extract a, b, c) (extract a, b, c))
+
+        EQ (a) True -> a
+        EQ (a) False -> !a
         """
         if isinstance(operands[0], BitVecITE) and isinstance(operands[1], Constant):
             if isinstance(operands[0].operands[1], Constant) and isinstance(
@@ -537,6 +555,9 @@ def visit_BoolEqual(self, expression, *operands):
 
                 return BoolConstant(value=True, taint=expression.taint)
 
+        if isinstance(operands[1], BoolConstant):
+            return operands[0] if operands[1].value else BoolNot(value=operands[0])
+
     def visit_BoolOr(self, expression, a, b):
         if isinstance(a, Constant):
             if a.value == False:
@@ -715,6 +736,18 @@ def visit_BitVecAdd(self, expression, *operands):
             if left.value == 0:
                 return right
 
+    def visit_BitVecMul(self, expression, *operands):
+        """
+        a * 1  ==> a
+        1 * a  ==> a
+        """
+        left = operands[0]
+        right = operands[1]
+        if isinstance(right, BitVecConstant) and right.value == 1:
+            return left
+        if isinstance(left, BitVecConstant) and left.value == 1:
+            return right
+
     def visit_BitVecSub(self, expression, *operands):
         """a - 0 ==> a
         (a + b) - b  ==> a

tests/other/test_smtlibv2.py

@@ -834,6 +834,39 @@ def test_arithmetic_simplify_extract(self):
         )
         self.assertEqual(translate_to_smtlib(simplify(c)), "((_ extract 23 8) VARA)")
 
+    def test_arithmetic_simplify_bool(self):
+        cs = ConstraintSet()
+        a = cs.new_bool(name="A")
+        b = cs.new_bool(name="B")
+
+        x = BoolEqual(a=a, b=BoolConstant(value=False))
+        self.assertEqual(translate_to_smtlib(simplify(x)), translate_to_smtlib(BoolNot(value=a)))
+
+        x = BoolEqual(a=a, b=BoolConstant(value=True))
+        self.assertEqual(translate_to_smtlib(simplify(x)), translate_to_smtlib(a))
+
+        x = BoolNot(value=BoolAnd(a=a, b=b))
+        expected = BoolOr(a=BoolNot(value=a), b=BoolNot(value=b))
+        self.assertEqual(translate_to_smtlib(simplify(x)), translate_to_smtlib(expected))
+
+        x = BoolNot(value=BoolOr(a=a, b=b))
+        expected = BoolAnd(a=BoolNot(value=a), b=BoolNot(value=b))
+        self.assertEqual(translate_to_smtlib(simplify(x)), translate_to_smtlib(expected))
+
+        x = BoolNot(value=BoolNot(value=a))
+        self.assertEqual(translate_to_smtlib(simplify(x)), translate_to_smtlib(a))
+
+    def test_arithmetic_simplify_mul(self):
+        cs = ConstraintSet()
+        a = cs.new_bitvec(32, name="A")
+        one = BitVecConstant(size=32, value=1)
+
+        x = BitVecMul(a=one, b=a)
+        self.assertEqual(translate_to_smtlib(simplify(x)), translate_to_smtlib(a))
+
+        x = BitVecMul(a=a, b=one)
+        self.assertEqual(translate_to_smtlib(simplify(x)), translate_to_smtlib(a))
+
     def test_constant_folding_extract(self):
         cs = ConstraintSet()
         x = BitVecConstant(size=32, value=0xAB123456, taint=("important",))