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

8 files changed, 124 insertions, 27 deletions

diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index fe6388de..a14cb43e 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -49,10 +49,10 @@ The general rules are:
 
 <li> Booleans:
     <ol type="a">
-    <li> Boolean not is written as <tt>(false == ?)</tt> </li>
      <li> \c Ne, \c Ugt, \c Uge, \c Sgt, \c Sge are not used </li>
-     <li> The only acceptable operations with boolean arguments are \c And, 
-          \c Or, \c Xor, \c Eq, as well as \c SExt, \c ZExt,
+     <li> The only acceptable operations with boolean arguments are 
+          \c Not \c And, \c Or, \c Xor, \c Eq, 
+	  as well as \c SExt, \c ZExt,
           \c Select and \c NotOptimized. </li>
      <li> The only boolean operation which may involve a constant is boolean not (<tt>== false</tt>). </li>
      </ol>
@@ -134,6 +134,7 @@ public:
     SRem,
 
     // Bit
+    Not,
     And,
     Or,
     Xor,
@@ -840,6 +841,55 @@ public:
 };
 
 
+/** 
+    Bitwise Not 
+*/
+class NotExpr : public NonConstantExpr { 
+public:
+  static const Kind kind = Not;
+  static const unsigned numKids = 1;
+  
+  ref<Expr> expr;
+
+public:  
+  static ref<Expr> alloc(const ref<Expr> &e) {
+    ref<Expr> r(new NotExpr(e));
+    r->computeHash();
+    return r;
+  }
+  
+  static ref<Expr> create(const ref<Expr> &e);
+
+  Width getWidth() const { return expr->getWidth(); }
+  Kind getKind() const { return Not; }
+
+  unsigned getNumKids() const { return numKids; }
+  ref<Expr> getKid(unsigned i) const { return expr; }
+
+  int compareContents(const Expr &b) const {
+    const NotExpr &eb = static_cast<const NotExpr&>(b);
+    if (expr != eb.expr) return expr < eb.expr ? -1 : 1;
+    return 0;
+  }
+
+  virtual ref<Expr> rebuild(ref<Expr> kids[]) const { 
+    return create(kids[0]);
+  }
+
+  virtual unsigned computeHash();
+
+public:
+  static bool classof(const Expr *E) {
+    return E->getKind() == Expr::Not;
+  }
+  static bool classof(const NotExpr *) { return true; }
+
+private:
+  NotExpr(const ref<Expr> &e) : expr(e) {}
+};
+
+
+
 // Casting
 
 class CastExpr : public NonConstantExpr {
diff --git a/include/klee/ExprBuilder.h b/include/klee/ExprBuilder.h
index 2bbcf545..f7a6653d 100644
--- a/include/klee/ExprBuilder.h
+++ b/include/klee/ExprBuilder.h
@@ -41,6 +41,7 @@ namespace klee {
     virtual ref<Expr> SDiv(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
     virtual ref<Expr> URem(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
     virtual ref<Expr> SRem(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
+    virtual ref<Expr> Not(const ref<Expr> &LHS) = 0;
     virtual ref<Expr> And(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
     virtual ref<Expr> Or(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
     virtual ref<Expr> Xor(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
@@ -64,10 +65,6 @@ namespace klee {
 
     ref<Expr> True() { return ConstantExpr::alloc(0, Expr::Bool); }
 
-    ref<Expr> Not(const ref<Expr> &LHS) {
-      return Eq(False(), LHS);
-    }
-
     ref<Expr> Constant(uint64_t Value, Expr::Width W) {
       return Constant(llvm::APInt(W, Value));
     }
diff --git a/include/klee/util/ExprVisitor.h b/include/klee/util/ExprVisitor.h
index d17cb4d8..1fae4505 100644
--- a/include/klee/util/ExprVisitor.h
+++ b/include/klee/util/ExprVisitor.h
@@ -62,6 +62,7 @@ namespace klee {
     virtual Action visitSDiv(const SDivExpr&);
     virtual Action visitURem(const URemExpr&);
     virtual Action visitSRem(const SRemExpr&);
+    virtual Action visitNot(const NotExpr&);
     virtual Action visitAnd(const AndExpr&);
     virtual Action visitOr(const OrExpr&);
     virtual Action visitXor(const XorExpr&);
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);