Add (very) basic constant folding for Mul.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73460 91177308-0d34-0410-b5e6-96231b3b80d8

3 files changed, 33 insertions, 2 deletions

diff --git a/lib/Expr/ExprBuilder.cpp b/lib/Expr/ExprBuilder.cpp
index 098da6ea..bb6f28ec 100644
--- a/lib/Expr/ExprBuilder.cpp
+++ b/lib/Expr/ExprBuilder.cpp
@@ -829,7 +829,7 @@ namespace {
         // X - (C + Y) ==> -C + (X - Y)
         if (ConstantExpr *CE = dyn_cast<ConstantExpr>(BE->left))
           return Builder->Add(CE->Neg(), Builder->Sub(LHS, BE->right));
-        // X - (Y + C) ==> -C + (X + Y);
+        // X - (Y + C) ==> -C + (X + Y)
         if (ConstantExpr *CE = dyn_cast<ConstantExpr>(BE->right))
           return Builder->Add(CE->Neg(), Builder->Sub(LHS, BE->left));
         break;
@@ -849,6 +849,27 @@ namespace {
 
       return Base->Sub(LHS, RHS);
     }
+
+    ref<Expr> Mul(const ref<ConstantExpr> &LHS,
+                  const ref<NonConstantExpr> &RHS) {
+      if (LHS->isZero())
+        return LHS;
+      if (LHS->isOne())
+        return RHS;
+      // FIXME: Unbalance muls, fold constants through {sub,add}-with-constant,
+      // etc.
+      return Base->Mul(LHS, RHS);
+    }
+
+    ref<Expr> Mul(const ref<NonConstantExpr> &LHS,
+                  const ref<ConstantExpr> &RHS) {
+      return Mul(RHS, LHS);
+    }
+
+    ref<Expr> Mul(const ref<NonConstantExpr> &LHS,
+                  const ref<NonConstantExpr> &RHS) {
+      return Base->Mul(LHS, RHS);
+    }
   };
 
   typedef ConstantSpecializedExprBuilder<ConstantFoldingBuilder>
diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index c78791ef..a2103b99 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -569,7 +569,7 @@ void ExprPPrinter::printQuery(std::ostream &os,
     p.printSeparator(PC, q->isFalse(), indent-1);
     PC << '[';
     for (const ref<Expr> *it = evalExprsBegin; it != evalExprsEnd; ++it) {
-      p.print(*it, PC);
+      p.print(*it, PC, /*printConstWidth*/true);
       if (it + 1 != evalExprsEnd)
         PC.breakLine(indent);
     }
diff --git a/test/Expr/Parser/ConstantFolding.pc b/test/Expr/Parser/ConstantFolding.pc
index 95bc361a..3a311a60 100644
--- a/test/Expr/Parser/ConstantFolding.pc
+++ b/test/Expr/Parser/ConstantFolding.pc
@@ -145,3 +145,13 @@ array a[64] : w32 -> w8 = symbolic
 # RUN: grep \"(query .. false .(Add w8 10\" %t2
 # RUN: grep                          \"(Sub w8 (Read w8 0 a) (Read w8 1 a)\" %t2
 (query [] false [(Sub w8 (Read w8 0 a) (Sub w8 (Read w8 1 a) 10))])
+
+# Check -- X * 0 ==> 0
+# RUN: grep -A 2 \"# Query 28\" %t > %t2
+# RUN: grep \"(query .. false .(w8 0).\" %t2
+(query [] false [(Mul w8 0 (Read w8 0 a))])
+
+# Check -- X * 1 ==> X
+# RUN: grep -A 2 \"# Query 29\" %t > %t2
+# RUN: grep \"(query .. false .(Read w8 0 a).\" %t2
+(query [] false [(Mul w8 1 (Read w8 0 a))])