about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--include/klee/Expr.h1
-rw-r--r--include/klee/Solver.h2
-rw-r--r--lib/Core/Executor.cpp12
-rw-r--r--lib/Core/TimingSolver.cpp2
-rw-r--r--lib/Expr/Expr.cpp26
-rw-r--r--lib/Expr/ExprPPrinter.cpp4
-rw-r--r--lib/Expr/Parser.cpp9
-rw-r--r--lib/Solver/CachingSolver.cpp2
-rw-r--r--lib/Solver/CexCachingSolver.cpp4
-rw-r--r--lib/Solver/Solver.cpp2
10 files changed, 30 insertions, 34 deletions
diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index 6e55cdd3..fe6388de 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -221,7 +221,6 @@ public:
 
   /* Utility creation functions */
   static ref<Expr> createCoerceToPointerType(ref<Expr> e);
-  static ref<Expr> createNot(ref<Expr> e);
   static ref<Expr> createImplies(ref<Expr> hyp, ref<Expr> conc);
   static ref<Expr> createIsZero(ref<Expr> e);
 
diff --git a/include/klee/Solver.h b/include/klee/Solver.h
index f1e18f12..dc787ad6 100644
--- a/include/klee/Solver.h
+++ b/include/klee/Solver.h
@@ -40,7 +40,7 @@ namespace klee {
 
     /// negateExpr - Return a copy of the query with the expression negated.
     Query negateExpr() const {
-      return withExpr(Expr::createNot(expr));
+      return withExpr(Expr::createIsZero(expr));
     }
   };
 
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 79b2040b..62f033be 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -728,7 +728,7 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
           addConstraint(current, condition);
         } else  {
           res = Solver::False;
-          addConstraint(current, Expr::createNot(condition));
+          addConstraint(current, Expr::createIsZero(condition));
         }
       }
     } else if (res==Solver::Unknown) {
@@ -753,7 +753,7 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
           addConstraint(current, condition);
           res = Solver::True;        
         } else {
-          addConstraint(current, Expr::createNot(condition));
+          addConstraint(current, Expr::createIsZero(condition));
           res = Solver::False;
         }
       }
@@ -786,7 +786,7 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
       assert(trueSeed || falseSeed);
       
       res = trueSeed ? Solver::True : Solver::False;
-      addConstraint(current, trueSeed ? condition : Expr::createNot(condition));
+      addConstraint(current, trueSeed ? condition : Expr::createIsZero(condition));
     }
   }
 
@@ -880,7 +880,7 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
     }
 
     addConstraint(*trueState, condition);
-    addConstraint(*falseState, Expr::createNot(condition));
+    addConstraint(*falseState, Expr::createIsZero(condition));
 
     // Kinda gross, do we even really still want this option?
     if (MaxDepth && MaxDepth<=trueState->depth) {
@@ -1389,7 +1389,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
       for (unsigned i=1; i<cases; ++i) {
         ref<Expr> value = evalConstant(si->getCaseValue(i));
         ref<Expr> match = EqExpr::create(cond, value);
-        isDefault = AndExpr::create(isDefault, Expr::createNot(match));
+        isDefault = AndExpr::create(isDefault, Expr::createIsZero(match));
         bool result;
         bool success = solver->mayBeTrue(state, match, result);
         assert(success && "FIXME: Unhandled solver failure");
@@ -3119,7 +3119,7 @@ bool Executor::getSymbolicSolution(const ExecutionState &state,
         mo->cexPreferences.begin(), pie = mo->cexPreferences.end();
       for (; pi != pie; ++pi) {
         bool mustBeTrue;
-        bool success = solver->mustBeTrue(tmp, Expr::createNot(*pi), 
+        bool success = solver->mustBeTrue(tmp, Expr::createIsZero(*pi), 
                                           mustBeTrue);
         if (!success) break;
         if (!mustBeTrue) tmp.addConstraint(*pi);
diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp
index 0154ddcf..542a3c8e 100644
--- a/lib/Core/TimingSolver.cpp
+++ b/lib/Core/TimingSolver.cpp
@@ -72,7 +72,7 @@ bool TimingSolver::mustBeTrue(const ExecutionState& state, ref<Expr> expr,
 
 bool TimingSolver::mustBeFalse(const ExecutionState& state, ref<Expr> expr,
                                bool &result) {
-  return mustBeTrue(state, Expr::createNot(expr), result);
+  return mustBeTrue(state, Expr::createIsZero(expr), result);
 }
 
 bool TimingSolver::mayBeTrue(const ExecutionState& state, ref<Expr> expr, 
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);
diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp
index d353e485..c0b77429 100644
--- a/lib/Solver/CachingSolver.cpp
+++ b/lib/Solver/CachingSolver.cpp
@@ -89,7 +89,7 @@ public:
     the canonicalization process. */
 ref<Expr> CachingSolver::canonicalizeQuery(ref<Expr> originalQuery,
                                            bool &negationUsed) {
-  ref<Expr> negatedQuery = Expr::createNot(originalQuery);
+  ref<Expr> negatedQuery = Expr::createIsZero(originalQuery);
 
   // select the "smaller" query to the be canonical representation
   if (originalQuery.compare(negatedQuery) < 0) {
diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp
index 373f42d9..2bdc7418 100644
--- a/lib/Solver/CexCachingSolver.cpp
+++ b/lib/Solver/CexCachingSolver.cpp
@@ -137,7 +137,7 @@ bool CexCachingSolver::searchForAssignment(KeyType &key, Assignment *&result) {
 bool CexCachingSolver::lookupAssignment(const Query &query, 
                                         Assignment *&result) {
   KeyType key(query.constraints.begin(), query.constraints.end());
-  ref<Expr> neg = Expr::createNot(query.expr);
+  ref<Expr> neg = Expr::createIsZero(query.expr);
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(neg)) {
     if (CE->isFalse()) {
       result = (Assignment*) 0;
@@ -152,7 +152,7 @@ bool CexCachingSolver::lookupAssignment(const Query &query,
 
 bool CexCachingSolver::getAssignment(const Query& query, Assignment *&result) {
   KeyType key(query.constraints.begin(), query.constraints.end());
-  ref<Expr> neg = Expr::createNot(query.expr);
+  ref<Expr> neg = Expr::createIsZero(query.expr);
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(neg)) {
     if (CE->isFalse()) {
       result = (Assignment*) 0;
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index f8f9d690..abff5743 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -349,7 +349,7 @@ ValidatingSolver::computeInitialValues(const Query& query,
       }
     }
     ConstraintManager tmp(bindings);
-    ref<Expr> constraints = Expr::createNot(query.expr);
+    ref<Expr> constraints = Expr::createIsZero(query.expr);
     for (ConstraintManager::const_iterator it = query.constraints.begin(), 
            ie = query.constraints.end(); it != ie; ++it)
       constraints = AndExpr::create(constraints, *it);
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-27 00:27:12 +0000