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

5 files changed, 69 insertions, 20 deletions

diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index 2f9e04a0..763a4be1 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -122,6 +122,7 @@ void Expr::printKind(std::ostream &os, Kind k) {
     X(SDiv);
     X(URem);
     X(SRem);
+    X(Not);
     X(And);
     X(Or);
     X(Xor);
@@ -188,6 +189,11 @@ unsigned ReadExpr::computeHash() {
   return hashValue;
 }
 
+unsigned NotExpr::computeHash() {
+  unsigned hashValue = expr->hash() * Expr::MAGIC_HASH_CONSTANT * Expr::Not;
+  return hashValue;
+}
+
 ref<Expr> Expr::createFromKind(Kind k, std::vector<CreateArg> args) {
   unsigned numArgs = args.size();
   (void) numArgs;
@@ -621,6 +627,16 @@ ref<Expr> ExtractExpr::create(ref<Expr> expr, unsigned off, Width w) {
 
 /***/
 
+ref<Expr> NotExpr::create(const ref<Expr> &e) {
+  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(e))
+    return CE->Not();
+  
+  return NotExpr::alloc(e);
+}
+
+
+/***/
+
 ref<Expr> ZExtExpr::create(const ref<Expr> &e, Width w) {
   unsigned kBits = e->getWidth();
   if (w == kBits) {
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));
diff --git a/lib/Expr/ExprVisitor.cpp b/lib/Expr/ExprVisitor.cpp
index cf75974a..3eced3bf 100644
--- a/lib/Expr/ExprVisitor.cpp
+++ b/lib/Expr/ExprVisitor.cpp
@@ -69,6 +69,7 @@ ref<Expr> ExprVisitor::visitActual(const ref<Expr> &e) {
     case Expr::SDiv: res = visitSDiv(static_cast<SDivExpr&>(ep)); break;
     case Expr::URem: res = visitURem(static_cast<URemExpr&>(ep)); break;
     case Expr::SRem: res = visitSRem(static_cast<SRemExpr&>(ep)); break;
+    case Expr::Not: res = visitNot(static_cast<NotExpr&>(ep)); break;
     case Expr::And: res = visitAnd(static_cast<AndExpr&>(ep)); break;
     case Expr::Or: res = visitOr(static_cast<OrExpr&>(ep)); break;
     case Expr::Xor: res = visitXor(static_cast<XorExpr&>(ep)); break;
@@ -187,6 +188,10 @@ ExprVisitor::Action ExprVisitor::visitSRem(const SRemExpr&) {
   return Action::doChildren(); 
 }
 
+ExprVisitor::Action ExprVisitor::visitNot(const NotExpr&) {
+  return Action::doChildren(); 
+}
+
 ExprVisitor::Action ExprVisitor::visitAnd(const AndExpr&) {
   return Action::doChildren(); 
 }
diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
index 52fba4a6..85a9a1ac 100644
--- a/lib/Expr/Parser.cpp
+++ b/lib/Expr/Parser.cpp
@@ -822,6 +822,8 @@ static bool LookupExprInfo(const Token &Tok, unsigned &Kind,
     if (memcmp(Tok.start, "Mul", 3) == 0)
       return SetOK(Expr::Mul, true, 2);
 
+    if (memcmp(Tok.start, "Not", 3) == 0)
+      return SetOK(Expr::Not, true, 1);
     if (memcmp(Tok.start, "And", 3) == 0)
       return SetOK(Expr::And, true, 2);
     if (memcmp(Tok.start, "Shl", 3) == 0)
@@ -829,8 +831,6 @@ static bool LookupExprInfo(const Token &Tok, unsigned &Kind,
     if (memcmp(Tok.start, "Xor", 3) == 0)
       return SetOK(Expr::Xor, true, 2);
 
-    if (memcmp(Tok.start, "Neg", 3) == 0)
-      return SetOK(eMacroKind_Neg, true, 1);
     if (memcmp(Tok.start, "Ult", 3) == 0)
       return SetOK(Expr::Ult, false, 2);
     if (memcmp(Tok.start, "Ule", 3) == 0)
@@ -849,6 +849,8 @@ static bool LookupExprInfo(const Token &Tok, unsigned &Kind,
       return SetOK(Expr::Sge, false, 2);
     break;
 
+    
+
   case 4:
     if (memcmp(Tok.start, "Read", 4) == 0)
       return SetOK(Expr::Read, true, -1);
@@ -1020,6 +1022,9 @@ ExprResult ParserImpl::ParseUnaryParenExpr(const Token &Name,
     return Builder->Eq(Builder->Constant(0, E->getWidth()), E);
   case eMacroKind_Neg:
     return Builder->Sub(Builder->Constant(0, E->getWidth()), E);
+  case Expr::Not:
+    // FIXME: Type check arguments.
+    return Builder->Not(E);
   case Expr::SExt:
     // FIXME: Type check arguments.
     return Builder->SExt(E, ResTy);
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 65ef24d1..4e091600 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -700,7 +700,17 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     return vc_sbvModExpr(vc, *width_out, left, right);
   }
 
-    // Binary
+    // Bitwise
+
+  case Expr::Not: {
+    NotExpr *ne = cast<NotExpr>(e);
+    ExprHandle expr = construct(ne->expr, width_out);
+    if (*width_out==1) {
+      return vc_notExpr(vc, expr);
+    } else {
+      return vc_bvNotExpr(vc, expr);
+    }
+  }    
 
   case Expr::And: {
     AndExpr *ae = cast<AndExpr>(e);
@@ -712,6 +722,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
       return vc_bvAndExpr(vc, left, right);
     }
   }
+
   case Expr::Or: {
     OrExpr *oe = cast<OrExpr>(e);
     ExprHandle left = construct(oe->left, width_out);