Replaced createNot() by createIsZero() and "Not" macro by "Nz".

Not will become bitwise not.



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

3 files changed, 18 insertions, 21 deletions

diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index fc450d76..2f9e04a0 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -289,7 +289,7 @@ Expr::Width Expr::getWidthForLLVMType(const llvm::Type *t) {
 }
 
 ref<Expr> Expr::createImplies(ref<Expr> hyp, ref<Expr> conc) {
-  return OrExpr::create(Expr::createNot(hyp), conc);
+  return OrExpr::create(Expr::createIsZero(hyp), conc);
 }
 
 ref<Expr> Expr::createIsZero(ref<Expr> e) {
@@ -300,10 +300,6 @@ ref<Expr> Expr::createCoerceToPointerType(ref<Expr> e) {
   return ZExtExpr::create(e, kMachinePointerType);
 }
 
-ref<Expr> Expr::createNot(ref<Expr> e) {
-  return createIsZero(e);
-}
-
 ref<ConstantExpr> Expr::createPointer(uint64_t v) {
   return ConstantExpr::create(v, kMachinePointerType);
 }
@@ -527,11 +523,11 @@ ref<Expr> SelectExpr::create(ref<Expr> c, ref<Expr> t, ref<Expr> f) {
       if (CE->isTrue()) {
         return OrExpr::create(c, f);
       } else {
-        return AndExpr::create(Expr::createNot(c), f);
+        return AndExpr::create(Expr::createIsZero(c), f);
       }
     } else if (ConstantExpr *CE = dyn_cast<ConstantExpr>(f)) {
       if (CE->isTrue()) {
-        return OrExpr::create(Expr::createNot(c), t);
+        return OrExpr::create(Expr::createIsZero(c), t);
       } else {
         return AndExpr::create(c, t);
       }
@@ -868,7 +864,7 @@ static ref<Expr> SRemExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
 
 static ref<Expr> ShlExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
   if (l->getWidth() == Expr::Bool) { // l & !r
-    return AndExpr::create(l, Expr::createNot(r));
+    return AndExpr::create(l, Expr::createIsZero(r));
   } else{
     return ShlExpr::alloc(l, r);
   }
@@ -876,7 +872,7 @@ static ref<Expr> ShlExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
 
 static ref<Expr> LShrExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
   if (l->getWidth() == Expr::Bool) { // l & !r
-    return AndExpr::create(l, Expr::createNot(r));
+    return AndExpr::create(l, Expr::createIsZero(r));
   } else{
     return LShrExpr::alloc(l, r);
   }
@@ -1014,8 +1010,8 @@ static ref<Expr> EqExpr_createPartialR(const ref<ConstantExpr> &cl, Expr *r) {
         const OrExpr *roe = cast<OrExpr>(r);
 
         // transform not(or(a,b)) to and(not a, not b)
-        return AndExpr::create(Expr::createNot(roe->left),
-                               Expr::createNot(roe->right));
+        return AndExpr::create(Expr::createIsZero(roe->left),
+                               Expr::createIsZero(roe->right));
       }
     }
   } else if (rk == Expr::SExt) {
@@ -1093,7 +1089,7 @@ ref<Expr> SgeExpr::create(const ref<Expr> &l, const ref<Expr> &r) {
 static ref<Expr> UltExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
   Expr::Width t = l->getWidth();
   if (t == Expr::Bool) { // !l && r
-    return AndExpr::create(Expr::createNot(l), r);
+    return AndExpr::create(Expr::createIsZero(l), r);
   } else {
     return UltExpr::alloc(l, r);
   }
@@ -1101,7 +1097,7 @@ static ref<Expr> UltExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
 
 static ref<Expr> UleExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
   if (l->getWidth() == Expr::Bool) { // !(l && !r)
-    return OrExpr::create(Expr::createNot(l), r);
+    return OrExpr::create(Expr::createIsZero(l), r);
   } else {
     return UleExpr::alloc(l, r);
   }
@@ -1109,7 +1105,7 @@ static ref<Expr> UleExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
 
 static ref<Expr> SltExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
   if (l->getWidth() == Expr::Bool) { // l && !r
-    return AndExpr::create(l, Expr::createNot(r));
+    return AndExpr::create(l, Expr::createIsZero(r));
   } else {
     return SltExpr::alloc(l, r);
   }
@@ -1117,7 +1113,7 @@ static ref<Expr> SltExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
 
 static ref<Expr> SleExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
   if (l->getWidth() == Expr::Bool) { // !(!l && r)
-    return OrExpr::create(l, Expr::createNot(r));
+    return OrExpr::create(l, Expr::createIsZero(r));
   } else {
     return SleExpr::alloc(l, r);
   }
diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index 6eb15c7c..691ccd89 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -408,11 +408,11 @@ public:
           bindings.insert(std::make_pair(e, counter++));
         }
 
-        // Detect Not.
+        // Detect Nz
         // FIXME: This should be in common code.
         if (const EqExpr *ee = dyn_cast<EqExpr>(e)) {
           if (ee->left == ConstantExpr::alloc(false, Expr::Bool)) {
-            PC << "(Not";
+            PC << "(Nz";
             printWidth(PC, e);
             PC << ' ';
             print(ee->right, PC);
diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
index 42e8af03..52fba4a6 100644
--- a/lib/Expr/Parser.cpp
+++ b/lib/Expr/Parser.cpp
@@ -776,7 +776,7 @@ ExprResult ParserImpl::ParseExpr(TypeResult ExpectedType) {
 
 // Additional kinds for macro forms.
 enum MacroKind {
-  eMacroKind_Not = Expr::LastKind + 1,     // false == x
+  eMacroKind_Nz = Expr::LastKind + 1,      // false == x
   eMacroKind_Neg,                          // 0 - x
   eMacroKind_ReadLSB,                      // Multibyte read
   eMacroKind_ReadMSB,                      // Multibyte write
@@ -806,6 +806,9 @@ static bool LookupExprInfo(const Token &Tok, unsigned &Kind,
       return SetOK(Expr::Eq, false, 2);
     if (memcmp(Tok.start, "Ne", 2) == 0)
       return SetOK(Expr::Ne, false, 2);
+    
+    if (memcmp(Tok.start, "Nz", 2) == 0)
+      return SetOK(eMacroKind_Nz, true, 1);
 
     if (memcmp(Tok.start, "Or", 2) == 0)
       return SetOK(Expr::Or, true, 2);
@@ -826,8 +829,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, "Not", 3) == 0)
-      return SetOK(eMacroKind_Not, true, 1);
     if (memcmp(Tok.start, "Neg", 3) == 0)
       return SetOK(eMacroKind_Neg, true, 1);
     if (memcmp(Tok.start, "Ult", 3) == 0)
@@ -1015,7 +1016,7 @@ ExprResult ParserImpl::ParseUnaryParenExpr(const Token &Name,
   ExpectRParen("unexpected argument in unary expression.");  
   ExprHandle E = Arg.get();
   switch (Kind) {
-  case eMacroKind_Not:
+  case eMacroKind_Nz:
     return Builder->Eq(Builder->Constant(0, E->getWidth()), E);
   case eMacroKind_Neg:
     return Builder->Sub(Builder->Constant(0, E->getWidth()), E);