Added support for bitwise not. Replacing "false == " with Not in

the canonical form.



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

1 files changed, 29 insertions, 17 deletions

diff --git a/lib/Expr/ExprBuilder.cpp b/lib/Expr/ExprBuilder.cpp
index 009e621e..d9e20e45 100644
--- a/lib/Expr/ExprBuilder.cpp
+++ b/lib/Expr/ExprBuilder.cpp
@@ -82,6 +82,10 @@ namespace {
       return SRemExpr::alloc(LHS, RHS);
     }
 
+    virtual ref<Expr> Not(const ref<Expr> &LHS) {
+      return NotExpr::alloc(LHS);
+    }
+
     virtual ref<Expr> And(const ref<Expr> &LHS, const ref<Expr> &RHS) {
       return AndExpr::alloc(LHS, RHS);
     }
@@ -227,6 +231,10 @@ namespace {
       return Base->SRem(LHS, RHS);
     }
 
+    ref<Expr> Not(const ref<Expr> &LHS) {
+      return Base->Not(LHS);
+    }
+
     ref<Expr> And(const ref<Expr> &LHS, const ref<Expr> &RHS) {
       return Base->And(LHS, RHS);
     }
@@ -462,6 +470,17 @@ namespace {
                           cast<NonConstantExpr>(RHS));
     }
 
+    virtual ref<Expr> Not(const ref<Expr> &LHS) {
+      // !!X ==> X
+      if (NotExpr *DblNot = dyn_cast<NotExpr>(LHS))
+        return DblNot->getKid(0);
+
+      if (ConstantExpr *CE = dyn_cast<ConstantExpr>(LHS))
+        return CE->Not();
+
+      return Builder.Not(cast<NonConstantExpr>(LHS));
+    }
+
     virtual ref<Expr> And(const ref<Expr> &LHS, const ref<Expr> &RHS) {
       if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) {
         if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS))
@@ -942,18 +961,7 @@ namespace {
           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->Not(RHS);
       }
 
       return Base->Eq(LHS, RHS);
@@ -988,11 +996,7 @@ namespace {
           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->Not(RHS);
       }
 
       return Base->Eq(LHS, RHS);
@@ -1012,6 +1016,14 @@ namespace {
       return Base->Eq(LHS, RHS);
     }
 
+    ref<Expr> Not(const ref<NonConstantExpr> &LHS) {
+      // Transform !(a or b) ==> !a and !b.
+      if (const OrExpr *OE = dyn_cast<OrExpr>(LHS))
+	return Builder->And(Builder->Not(OE->left),
+			    Builder->Not(OE->right));
+      return Base->Not(LHS);
+    }
+
     ref<Expr> Ne(const ref<Expr> &LHS, const ref<Expr> &RHS) {
       // X != Y ==> !(X == Y)
       return Builder->Not(Builder->Eq(LHS, RHS));