Unsigned div constant folding simplification (#1530)

* Unsigned div constant folding simp * blkn * Precalculate unsign mask
trailofbits · Oct 2, 2019 · 5e5f5bd · 5e5f5bd
1 parent 1ec9032
commit 5e5f5bd
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 0 deletions.
diff --git a/manticore/core/smtlib/visitors.py b/manticore/core/smtlib/visitors.py
@@ -5,6 +5,7 @@
 import operator
 
 logger = logging.getLogger(__name__)
+UNSIGN_MASK = (1 << 256) - 1
 
 
 class Visitor:
@@ -281,6 +282,7 @@ def __init__(self, **kw):
         BoolAnd: operator.__and__,
         BoolOr: operator.__or__,
         BoolNot: operator.__not__,
+        BitVecUnsignedDiv: lambda x, y: (x & UNSIGN_MASK) // (y & UNSIGN_MASK),
     }
 
     def visit_BitVecConcat(self, expression, *operands):

diff --git a/tests/other/test_smtlibv2.py b/tests/other/test_smtlibv2.py
@@ -533,6 +533,14 @@ def test_arithmetic_simplify_extract(self):
         )
         self.assertEqual(translate_to_smtlib(simplify(c)), "((_ extract 23 8) VARA)")
 
+    def test_constant_folding_udiv(self):
+        cs = ConstraintSet()
+        x = BitVecConstant(32, 0xFFFFFFFF, taint=("important",))
+        y = BitVecConstant(32, 2, taint=("stuff",))
+        z = constant_folder(x.udiv(y))
+        self.assertItemsEqual(z.taint, ("important", "stuff"))
+        self.assertEqual(z.value, 0x7FFFFFFF)
+
     def testBasicReplace(self):
         """ Add """
         a = BitVecConstant(32, 100)