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

3 files changed, 55 insertions, 7 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&);