Add (very) basic constant folding for And,Or,Xor.

 - Lots more important goodness can be done here.


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

2 files changed, 117 insertions, 31 deletions

diff --git a/lib/Expr/ExprBuilder.cpp b/lib/Expr/ExprBuilder.cpp
index bb6f28ec..aaddb3e3 100644
--- a/lib/Expr/ExprBuilder.cpp
+++ b/lib/Expr/ExprBuilder.cpp
@@ -856,8 +856,8 @@ namespace {
         return LHS;
       if (LHS->isOne())
         return RHS;
-      // FIXME: Unbalance muls, fold constants through {sub,add}-with-constant,
-      // etc.
+      // FIXME: Unbalance nested muls, fold constants through
+      // {sub,add}-with-constant, etc.
       return Base->Mul(LHS, RHS);
     }
 
@@ -870,6 +870,67 @@ namespace {
                   const ref<NonConstantExpr> &RHS) {
       return Base->Mul(LHS, RHS);
     }
+
+    ref<Expr> And(const ref<ConstantExpr> &LHS,
+                  const ref<NonConstantExpr> &RHS) {
+      if (LHS->isZero())
+        return LHS;
+      if (LHS->isAllOnes())
+        return RHS;
+      // FIXME: Unbalance nested ands, fold constants through
+      // {and,or}-with-constant, etc.
+      return Base->And(LHS, RHS);
+    }
+
+    ref<Expr> And(const ref<NonConstantExpr> &LHS,
+                  const ref<ConstantExpr> &RHS) {
+      return And(RHS, LHS);
+    }
+
+    ref<Expr> And(const ref<NonConstantExpr> &LHS,
+                  const ref<NonConstantExpr> &RHS) {
+      return Base->And(LHS, RHS);
+    }
+
+    ref<Expr> Or(const ref<ConstantExpr> &LHS,
+                  const ref<NonConstantExpr> &RHS) {
+      if (LHS->isZero())
+        return RHS;
+      if (LHS->isAllOnes())
+        return LHS;
+      // FIXME: Unbalance nested ors, fold constants through
+      // {and,or}-with-constant, etc.
+      return Base->Or(LHS, RHS);
+    }
+
+    ref<Expr> Or(const ref<NonConstantExpr> &LHS,
+                 const ref<ConstantExpr> &RHS) {
+      return Or(RHS, LHS);
+    }
+
+    ref<Expr> Or(const ref<NonConstantExpr> &LHS,
+                 const ref<NonConstantExpr> &RHS) {
+      return Base->Or(LHS, RHS);
+    }
+
+    ref<Expr> Xor(const ref<ConstantExpr> &LHS,
+                  const ref<NonConstantExpr> &RHS) {
+      if (LHS->isZero())
+        return RHS;
+      // FIXME: Unbalance nested ors, fold constants through
+      // {and,or}-with-constant, etc.
+      return Base->Xor(LHS, RHS);
+    }
+
+    ref<Expr> Xor(const ref<NonConstantExpr> &LHS,
+                  const ref<ConstantExpr> &RHS) {
+      return Xor(RHS, LHS);
+    }
+
+    ref<Expr> Xor(const ref<NonConstantExpr> &LHS,
+                  const ref<NonConstantExpr> &RHS) {
+      return Base->Xor(LHS, RHS);
+    }
   };
 
   typedef ConstantSpecializedExprBuilder<ConstantFoldingBuilder>
diff --git a/test/Expr/Parser/ConstantFolding.pc b/test/Expr/Parser/ConstantFolding.pc
index 3a311a60..bce6d5bb 100644
--- a/test/Expr/Parser/ConstantFolding.pc
+++ b/test/Expr/Parser/ConstantFolding.pc
@@ -2,156 +2,181 @@
 
 array a[64] : w32 -> w8 = symbolic
 
-# RUN: grep -A 2 \"# Query 1\" %t > %t2
+# RUN: grep -A 2 \"# Query 1$\" %t > %t2
 # RUN: grep \"(query .. false)\" %t2
 (query [] (Not (Ult (w32 0) (w32 1))))
 
 # Check -- 0 + X ==> X
-# RUN: grep -A 2 \"# Query 2\" %t > %t2
+# RUN: grep -A 2 \"# Query 2$\" %t > %t2
 # RUN: grep \"(query .. false .(Read w8 0 a).)\" %t2
 (query [] false [(Add w8 0 (Read w8 0 a))])
-# RUN: grep -A 2 \"# Query 3\" %t > %t2
+# RUN: grep -A 2 \"# Query 3$\" %t > %t2
 # RUN: grep \"(query .. false .(Read w8 0 a).)\" %t2
 (query [] false [(Add w8 (Read w8 0 a) 0)])
 
 # Check -- C_0 + (C_1 + X) ==> (C_0 + C_1) + X
-# RUN: grep -A 2 \"# Query 4\" %t > %t2
+# RUN: grep -A 2 \"# Query 4$\" %t > %t2
 # RUN: grep \"(query .. false .(Add w8 30 (Read w8 0 a)).)\" %t2
 (query [] false [(Add w8 10 (Add w8 20 (Read w8 0 a)))])
 
 # Check -- C_0 + (X + C_1) ==> (C_0 + C_1) + X
-# RUN: grep -A 2 \"# Query 5\" %t > %t2
+# RUN: grep -A 2 \"# Query 5$\" %t > %t2
 # RUN: grep \"(query .. false .(Add w8 30 (Read w8 0 a)).)\" %t2
 (query [] false [(Add w8 10 (Add w8 (Read w8 0 a) 20))])
 
 # Check -- C_0 + (C_1 - X) ==> (C_0 + C_1) - X
-# RUN: grep -A 2 \"# Query 6\" %t > %t2
+# RUN: grep -A 2 \"# Query 6$\" %t > %t2
 # RUN: grep \"(query .. false .(Sub w8 30 (Read w8 0 a)).)\" %t2
 (query [] false [(Add w8 10 (Sub w8 20 (Read w8 0 a)))])
 
 # Check -- C_0 + (X - C_1) ==> (C_0 - C_1) + X
-# RUN: grep -A 2 \"# Query 7\" %t > %t2
+# RUN: grep -A 2 \"# Query 7$\" %t > %t2
 # RUN: grep \"(query .. false .(Add w8 246 (Read w8 0 a)).)\" %t2
 (query [] false [(Add w8 10 (Sub w8 (Read w8 0 a) 20))])
 
 # Check -- (X + Y) + Z ==> X + (Y + Z)
-# RUN: grep -A 3 \"# Query 8\" %t > %t2
+# RUN: grep -A 3 \"# Query 8$\" %t > %t2
 # RUN: grep \"(query .. false .(Add w8 (Read w8 0 a)\" %t2
 # RUN: grep                          \"(Add w8 (Read w8 1 a) (Read w8 2 a)\" %t2
 (query [] false [(Add w8 (Add w8 (Read w8 0 a) (Read w8 1 a)) (Read w8 2 a))])
 
 # Check -- (X - Y) + Z ==> X + (Z - Y)
-# RUN: grep -A 3 \"# Query 9\" %t > %t2
+# RUN: grep -A 3 \"# Query 9$\" %t > %t2
 # RUN: grep \"(query .. false .(Add w8 (Read w8 0 a)\" %t2
 # RUN: grep                          \"(Sub w8 (Read w8 2 a) (Read w8 1 a)\" %t2
 (query [] false [(Add w8 (Sub w8 (Read w8 0 a) (Read w8 1 a)) (Read w8 2 a))])
 
 # Check -- X + (C + Y) ==> C + (X + Y)
-# RUN: grep -A 3 \"# Query 10\" %t > %t2
+# RUN: grep -A 3 \"# Query 10$\" %t > %t2
 # RUN: grep \"(query .. false .(Add w8 10\" %t2
 # RUN: grep                          \"(Add w8 (Read w8 0 a) (Read w8 1 a)\" %t2
 (query [] false [(Add w8 (Read w8 0 a) (Add w8 10 (Read w8 1 a)))])
 
 # Check -- X + (Y + C) ==> C + (X + Y)
-# RUN: grep -A 3 \"# Query 11\" %t > %t2
+# RUN: grep -A 3 \"# Query 11$\" %t > %t2
 # RUN: grep \"(query .. false .(Add w8 10\" %t2
 # RUN: grep                          \"(Add w8 (Read w8 0 a) (Read w8 1 a)\" %t2
 (query [] false [(Add w8 (Read w8 0 a) (Add w8 (Read w8 1 a) 10))])
 
 # Check -- X + (C - Y) ==> C + (X - Y)
-# RUN: grep -A 3 \"# Query 12\" %t > %t2
+# RUN: grep -A 3 \"# Query 12$\" %t > %t2
 # RUN: grep \"(query .. false .(Add w8 10\" %t2
 # RUN: grep                          \"(Sub w8 (Read w8 0 a) (Read w8 1 a)\" %t2
 (query [] false [(Add w8 (Read w8 0 a) (Sub w8 10 (Read w8 1 a)))])
 
 # Check -- X + (Y - C) ==> -C + (X + Y)
-# RUN: grep -A 3 \"# Query 13\" %t > %t2
+# RUN: grep -A 3 \"# Query 13$\" %t > %t2
 # RUN: grep \"(query .. false .(Add w8 246\" %t2
 # RUN: grep                          \"(Add w8 (Read w8 0 a) (Read w8 1 a)\" %t2
 (query [] false [(Add w8 (Read w8 0 a) (Sub w8 (Read w8 1 a) 10))])
 
 # Check -- C_0 - (C_1 + X) ==> (C_0 - C1) - X
-# RUN: grep -A 2 \"# Query 14\" %t > %t2
+# RUN: grep -A 2 \"# Query 14$\" %t > %t2
 # RUN: grep \"(query .. false .(Sub w8 10 (Read w8 0 a))\" %t2
 (query [] false [(Sub w8 20 (Add w8 10 (Read w8 0 a)))])
 
 # Check -- C_0 - (X + C_1) ==> (C_0 + C1) + X
-# RUN: grep -A 2 \"# Query 15\" %t > %t2
+# RUN: grep -A 2 \"# Query 15$\" %t > %t2
 # RUN: grep \"(query .. false .(Sub w8 10 (Read w8 0 a))\" %t2
 (query [] false [(Sub w8 20 (Add w8 (Read w8 0 a) 10))])
 
 # Check -- C_0 - (C_1 - X) ==> (C_0 - C1) + X
-# RUN: grep -A 2 \"# Query 16\" %t > %t2
+# RUN: grep -A 2 \"# Query 16$\" %t > %t2
 # RUN: grep \"(query .. false .(Add w8 10 (Read w8 0 a))\" %t2
 (query [] false [(Sub w8 20 (Sub w8 10 (Read w8 0 a)))])
 
 # Check -- C_0 - (X - C_1) ==> (C_0 + C1) - X
-# RUN: grep -A 2 \"# Query 17\" %t > %t2
+# RUN: grep -A 2 \"# Query 17$\" %t > %t2
 # RUN: grep \"(query .. false .(Sub w8 30 (Read w8 0 a))\" %t2
 (query [] false [(Sub w8 20 (Sub w8 (Read w8 0 a) 10))])
 
 # Check -- (C_0 + X) - C_1 ==> (C_0 - C1) + X
-# RUN: grep -A 2 \"# Query 18\" %t > %t2
+# RUN: grep -A 2 \"# Query 18$\" %t > %t2
 # RUN: grep \"(query .. false .(Add w8 246 (Read w8 0 a))\" %t2
 (query [] false [(Sub w8 (Add w8 10 (Read w8 0 a)) 20)])
 
 # Check -- (X + C_0) - C_1 ==> (C_0 - C1) + X
-# RUN: grep -A 2 \"# Query 19\" %t > %t2
+# RUN: grep -A 2 \"# Query 19$\" %t > %t2
 # RUN: grep \"(query .. false .(Add w8 246 (Read w8 0 a))\" %t2
 (query [] false [(Sub w8 (Add w8 (Read w8 0 a) 10) 20)])
 
 # Check -- (C_0 - X) - C_1 ==> (C_0 - C1) - X
-# RUN: grep -A 2 \"# Query 20\" %t > %t2
+# RUN: grep -A 2 \"# Query 20$\" %t > %t2
 # RUN: grep \"(query .. false .(Sub w8 246 (Read w8 0 a))\" %t2
 (query [] false [(Sub w8 (Sub w8 10 (Read w8 0 a)) 20)])
 
 # Check -- (X - C_0) - C_1 ==> -(C_0 + C1) + X
-# RUN: grep -A 2 \"# Query 21\" %t > %t2
+# RUN: grep -A 2 \"# Query 21$\" %t > %t2
 # RUN: grep \"(query .. false .(Add w8 226 (Read w8 0 a))\" %t2
 (query [] false [(Sub w8 (Sub w8 (Read w8 0 a) 10) 20)])
 
 # Check -- (X + Y) - Z ==> X + (Y - Z)
-# RUN: grep -A 3 \"# Query 22\" %t > %t2
+# RUN: grep -A 3 \"# Query 22$\" %t > %t2
 # RUN: grep \"(query .. false .(Add w8 (Read w8 0 a)\" %t2
 # RUN: grep                          \"(Sub w8 (Read w8 1 a) (Read w8 2 a)\" %t2
 (query [] false [(Sub w8 (Add w8 (Read w8 0 a) (Read w8 1 a)) (Read w8 2 a))])
 
 # Check -- (X - Y) - Z ==> X - (Y + Z)
-# RUN: grep -A 3 \"# Query 23\" %t > %t2
+# RUN: grep -A 3 \"# Query 23$\" %t > %t2
 # RUN: grep \"(query .. false .(Sub w8 (Read w8 0 a)\" %t2
 # RUN: grep                          \"(Add w8 (Read w8 1 a) (Read w8 2 a)\" %t2
 (query [] false [(Sub w8 (Sub w8 (Read w8 0 a) (Read w8 1 a)) (Read w8 2 a))])
 
 # Check -- X - (C + Y) ==> -C + (X - Y)
-# RUN: grep -A 3 \"# Query 24\" %t > %t2
+# RUN: grep -A 3 \"# Query 24$\" %t > %t2
 # RUN: grep \"(query .. false .(Add w8 246\" %t2
 # RUN: grep                          \"(Sub w8 (Read w8 0 a) (Read w8 1 a)\" %t2
 (query [] false [(Sub w8 (Read w8 0 a) (Add w8 10 (Read w8 1 a)))])
 
 # Check -- X - (Y + C) ==> -C + (X - Y)
-# RUN: grep -A 3 \"# Query 25\" %t > %t2
+# RUN: grep -A 3 \"# Query 25$\" %t > %t2
 # RUN: grep \"(query .. false .(Add w8 246\" %t2
 # RUN: grep                          \"(Sub w8 (Read w8 0 a) (Read w8 1 a)\" %t2
 (query [] false [(Sub w8 (Read w8 0 a) (Add w8 (Read w8 1 a) 10))])
 
 # Check -- X - (C - Y) ==> -C + (X + Y)
-# RUN: grep -A 3 \"# Query 26\" %t > %t2
+# RUN: grep -A 3 \"# Query 26$\" %t > %t2
 # RUN: grep \"(query .. false .(Add w8 246\" %t2
 # RUN: grep                          \"(Add w8 (Read w8 0 a) (Read w8 1 a)\" %t2
 (query [] false [(Sub w8 (Read w8 0 a) (Sub w8 10 (Read w8 1 a)))])
 
 # Check -- X - (Y - C) ==> C + (X - Y)
-# RUN: grep -A 3 \"# Query 27\" %t > %t2
+# RUN: grep -A 3 \"# Query 27$\" %t > %t2
 # 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 -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 -A 2 \"# Query 29$\" %t > %t2
 # RUN: grep \"(query .. false .(Read w8 0 a).\" %t2
 (query [] false [(Mul w8 1 (Read w8 0 a))])
+
+# Check -- X & 0 ==> 0
+# RUN: grep -A 2 \"# Query 30$\" %t > %t2
+# RUN: grep \"(query .. false .(w8 0).\" %t2
+(query [] false [(And w8 0 (Read w8 0 a))])
+
+# Check -- X & 0b1...1 ==> X
+# RUN: grep -A 2 \"# Query 31$\" %t > %t2
+# RUN: grep \"(query .. false .(Read w8 0 a).\" %t2
+(query [] false [(And w8 255 (Read w8 0 a))])
+
+# Check -- X | 0 ==> X
+# RUN: grep -A 2 \"# Query 32$\" %t > %t2
+# RUN: grep \"(query .. false .(Read w8 0 a).\" %t2
+(query [] false [(Or w8 0 (Read w8 0 a))])
+
+# Check -- X | 0b1...1 ==> X
+# RUN: grep -A 2 \"# Query 33$\" %t > %t2
+# RUN: grep \"(query .. false .(w8 255).\" %t2
+(query [] false [(Or w8 255 (Read w8 0 a))])
+
+# Check -- X ^ 0b1...1 ==> X
+# RUN: grep -A 2 \"# Query 34$\" %t > %t2
+# RUN: grep \"(query .. false .(Read w8 0 a).\" %t2
+(query [] false [(Xor w8 0 (Read w8 0 a))])