Add basic constant folding / simplification for Eq.

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

3 files changed, 88 insertions, 0 deletions

diff --git a/lib/Expr/ExprBuilder.cpp b/lib/Expr/ExprBuilder.cpp
index aaddb3e3..68a7fefd 100644
--- a/lib/Expr/ExprBuilder.cpp
+++ b/lib/Expr/ExprBuilder.cpp
@@ -931,6 +931,43 @@ namespace {
                   const ref<NonConstantExpr> &RHS) {
       return Base->Xor(LHS, RHS);
     }
+
+    ref<Expr> Eq(const ref<ConstantExpr> &LHS, 
+                 const ref<NonConstantExpr> &RHS) {
+      Expr::Width Width = LHS->getWidth();
+      
+      if (Width == Expr::Bool) {
+        // true == X ==> X
+        if (LHS->isTrue())
+          return RHS;
+
+        // false == ... (not)
+
+        // Eliminate double negation.
+        if (const EqExpr *EE = dyn_cast<EqExpr>(RHS)) {
+          if (EE->left->getWidth() == Expr::Bool) {
+            // false == (false == X) ==> X
+            if (EE->left->isFalse())
+              return EE->right;
+            // false == (X == false) ==> X
+            if (EE->right->isFalse())
+              return EE->left;
+          }
+        }
+      }
+
+      return Base->Eq(LHS, RHS);
+    }
+
+    ref<Expr> Eq(const ref<NonConstantExpr> &LHS, 
+                 const ref<ConstantExpr> &RHS) {
+      return Eq(RHS, LHS);
+    }
+
+    ref<Expr> Eq(const ref<NonConstantExpr> &LHS, 
+                 const ref<NonConstantExpr> &RHS) {
+      return Base->Eq(LHS, RHS);
+    }
   };
 
   typedef ConstantSpecializedExprBuilder<ConstantFoldingBuilder>
@@ -941,6 +978,40 @@ namespace {
     SimplifyingBuilder(ExprBuilder *Builder, ExprBuilder *Base)
       : ChainedBuilder(Builder, Base) {}
 
+    ref<Expr> Eq(const ref<ConstantExpr> &LHS, 
+                 const ref<NonConstantExpr> &RHS) {
+      Expr::Width Width = LHS->getWidth();
+      
+      if (Width == Expr::Bool) {
+        // true == X ==> X
+        if (LHS->isTrue())
+          return RHS;
+
+        // false == X (not)
+
+        // Transform !(a or b) ==> !a and !b.
+        if (const OrExpr *OE = dyn_cast<OrExpr>(RHS))
+          return Builder->And(Builder->Not(OE->left),
+                              Builder->Not(OE->right));
+      }
+
+      return Base->Eq(LHS, RHS);
+    }
+
+    ref<Expr> Eq(const ref<NonConstantExpr> &LHS, 
+                 const ref<ConstantExpr> &RHS) {
+      return Eq(RHS, LHS);
+    }
+
+    ref<Expr> Eq(const ref<NonConstantExpr> &LHS, 
+                 const ref<NonConstantExpr> &RHS) {
+      // X == X ==> true
+      if (LHS == RHS)
+          return Builder->True();
+
+      return Base->Eq(LHS, RHS);
+    }
+
     ref<Expr> Ne(const ref<Expr> &LHS, const ref<Expr> &RHS) {
       // X != Y ==> !(X == Y)
       return Builder->Not(Builder->Eq(LHS, RHS));
diff --git a/test/Expr/Parser/ConstantFolding.pc b/test/Expr/Parser/ConstantFolding.pc
index bce6d5bb..56895e53 100644
--- a/test/Expr/Parser/ConstantFolding.pc
+++ b/test/Expr/Parser/ConstantFolding.pc
@@ -180,3 +180,13 @@ array a[64] : w32 -> w8 = symbolic
 # 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))])
+
+# Check -- true == X ==> X
+# RUN: grep -A 2 \"# Query 35$\" %t > %t2
+# RUN: grep \"(query .. false .(Eq 0 (Read w8 0 a)).\" %t2
+(query [] false [(Eq true (Eq 0 (Read w8 0 a)))])
+
+# Check -- !!X ==> X
+# RUN: grep -A 2 \"# Query 36$\" %t > %t2
+# RUN: grep \"(query .. false .(Eq 0 (Read w8 0 a)).\" %t2
+(query [] false [(Not (Not (Eq 0 (Read w8 0 a))))])
diff --git a/test/Expr/Parser/Simplify.pc b/test/Expr/Parser/Simplify.pc
index cf6d90ab..e89d79ff 100644
--- a/test/Expr/Parser/Simplify.pc
+++ b/test/Expr/Parser/Simplify.pc
@@ -26,3 +26,10 @@ array a[64] : w32 -> w8 = symbolic
 # RUN: grep -A 2 \"# Query 5\" %t > %t2
 # RUN: grep \"(query .. false .(Not (Eq (Read w8 0 a) (Read w8 1 a))).)\" %t2
 (query [] false [(Ne (Read w8 0 a) (Read w8 1 a))])
+
+# Check -- !(X or Y) ==> !X and !Y
+# RUN: grep -A 3 \"# Query 6$\" %t > %t2
+# RUN: grep \"(query .. false .(And (Not (Eq 0 (Read w8 0 a)))\" %t2
+# RUN: grep                       \"(Not (Eq 1 (Read w8 1 a))))\" %t2
+(query [] false [(Not (Or (Eq 0 (Read w8 0 a))
+                          (Eq 1 (Read w8 1 a))))])