about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--include/klee/Expr.h32
-rw-r--r--include/klee/util/Assignment.h7
-rw-r--r--lib/Core/Executor.cpp20
-rw-r--r--lib/Core/TimingSolver.cpp4
-rw-r--r--lib/Expr/Constraints.cpp2
-rw-r--r--lib/Expr/Expr.cpp63
-rw-r--r--lib/Expr/ExprEvaluator.cpp2
-rw-r--r--lib/Expr/ExprPPrinter.cpp2
-rw-r--r--lib/Solver/CexCachingSolver.cpp6
-rw-r--r--lib/Solver/STPBuilder.cpp11
-rw-r--r--lib/Solver/Solver.cpp4
11 files changed, 75 insertions, 78 deletions
diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index 192be985..9851d122 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -354,6 +354,28 @@ public:
   }
   static bool classof(const ConstantExpr *) { return true; }
 
+  /* Utility Functions */
+
+  /// isZero - Is this a constant zero.
+  bool isZero() const { return getConstantValue() == 0; }
+  
+  /// isTrue - Is this the true expression.
+  bool isTrue() const { 
+    assert(getWidth() == Expr::Bool && "Invalid isTrue() call!");
+    return getConstantValue() == 1;
+  }
+
+  /// isFalse - Is this the false expression.
+  bool isFalse() const {
+    assert(getWidth() == Expr::Bool && "Invalid isTrue() call!");
+    return getConstantValue() == 0;
+  }
+
+  /// isAllOnes - Is this constant all ones.
+  bool isAllOnes() const {
+    return getConstantValue() == bits64::maxValueOfNBits(getWidth());
+  }
+
   /* Constant Operations */
 
   ref<ConstantExpr> Concat(const ref<ConstantExpr> &RHS);
@@ -936,21 +958,21 @@ COMPARISON_EXPR_CLASS(Sge)
 
 inline bool Expr::isZero() const {
   if (const ConstantExpr *CE = dyn_cast<ConstantExpr>(this))
-    return CE->getConstantValue() == 0;
+    return CE->isZero();
   return false;
 }
   
 inline bool Expr::isTrue() const {
+  assert(getWidth() == Expr::Bool && "Invalid isTrue() call!");
   if (const ConstantExpr *CE = dyn_cast<ConstantExpr>(this))
-    return (CE->getWidth() == Expr::Bool &&
-            CE->getConstantValue() == 1);
+    return CE->isTrue();
   return false;
 }
   
 inline bool Expr::isFalse() const {
+  assert(getWidth() == Expr::Bool && "Invalid isFalse() call!");
   if (const ConstantExpr *CE = dyn_cast<ConstantExpr>(this))
-    return (CE->getWidth() == Expr::Bool &&
-            CE->getConstantValue() == 0);
+    return CE->isFalse();
   return false;
 }
 
diff --git a/include/klee/util/Assignment.h b/include/klee/util/Assignment.h
index 458b8d8d..838d03bd 100644
--- a/include/klee/util/Assignment.h
+++ b/include/klee/util/Assignment.h
@@ -88,12 +88,9 @@ namespace klee {
   template<typename InputIterator>
   inline bool Assignment::satisfies(InputIterator begin, InputIterator end) {
     AssignmentEvaluator v(*this);
-    for (; begin!=end; ++begin) {
-      ref<Expr> res = v.visit(*begin);
-      ConstantExpr *CE = dyn_cast<ConstantExpr>(res);
-      if (!CE || !CE->getConstantValue())
+    for (; begin!=end; ++begin)
+      if (!v.visit(*begin)->isTrue())
         return false;
-    }
     return true;
   }
 }
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 2aae57c9..f12aec08 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -630,7 +630,7 @@ void Executor::branch(ExecutionState &state,
                            res);
         assert(success && "FIXME: Unhandled solver failure");
         (void) success;
-        if (res->getConstantValue())
+        if (res->isTrue())
           break;
       }
       
@@ -766,15 +766,13 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
         solver->getValue(current, siit->assignment.evaluate(condition), res);
       assert(success && "FIXME: Unhandled solver failure");
       (void) success;
-      if (ConstantExpr *CE = dyn_cast<ConstantExpr>(res)) {
-        if (CE->getConstantValue()) {
-          trueSeed = true;
-        } else {
-          falseSeed = true;
-        }
-        if (trueSeed && falseSeed)
-          break;
+      if (res->isTrue()) {
+        trueSeed = true;
+      } else {
+        falseSeed = true;
       }
+      if (trueSeed && falseSeed)
+        break;
     }
     if (!(trueSeed && falseSeed)) {
       assert(trueSeed || falseSeed);
@@ -832,7 +830,7 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
           solver->getValue(current, siit->assignment.evaluate(condition), res);
         assert(success && "FIXME: Unhandled solver failure");
         (void) success;
-        if (res->getConstantValue()) {
+        if (res->isTrue()) {
           trueSeeds.push_back(*siit);
         } else {
           falseSeeds.push_back(*siit);
@@ -889,7 +887,7 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
 
 void Executor::addConstraint(ExecutionState &state, ref<Expr> condition) {
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(condition)) {
-    assert(CE->getConstantValue() && "attempt to add invalid constraint");
+    assert(CE->isTrue() && "attempt to add invalid constraint");
     return;
   }
 
diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp
index 339c33b2..0154ddcf 100644
--- a/lib/Core/TimingSolver.cpp
+++ b/lib/Core/TimingSolver.cpp
@@ -26,7 +26,7 @@ bool TimingSolver::evaluate(const ExecutionState& state, ref<Expr> expr,
                             Solver::Validity &result) {
   // Fast path, to avoid timer and OS overhead.
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(expr)) {
-    result = CE->getConstantValue() ? Solver::True : Solver::False;
+    result = CE->isTrue() ? Solver::True : Solver::False;
     return true;
   }
 
@@ -50,7 +50,7 @@ bool TimingSolver::mustBeTrue(const ExecutionState& state, ref<Expr> expr,
                               bool &result) {
   // Fast path, to avoid timer and OS overhead.
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(expr)) {
-    result = CE->getConstantValue() ? true : false;
+    result = CE->isTrue() ? true : false;
     return true;
   }
 
diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp
index 8f89f88a..9c09e643 100644
--- a/lib/Expr/Constraints.cpp
+++ b/lib/Expr/Constraints.cpp
@@ -122,7 +122,7 @@ void ConstraintManager::addConstraintInternal(ref<Expr> e) {
 
   switch (e->getKind()) {
   case Expr::Constant:
-    assert(cast<ConstantExpr>(e)->getConstantValue() && 
+    assert(cast<ConstantExpr>(e)->isTrue() && 
            "attempt to add invalid (false) constraint");
     break;
     
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index 597d1e08..72514aec 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -539,7 +539,7 @@ ref<Expr> ReadExpr::create(const UpdateList &ul, ref<Expr> index) {
     ref<Expr> cond = EqExpr::create(index, un->index);
     
     if (ConstantExpr *CE = dyn_cast<ConstantExpr>(cond)) {
-      if (CE->getConstantValue())
+      if (CE->isTrue())
         return un->value;
     } else {
       break;
@@ -560,18 +560,18 @@ ref<Expr> SelectExpr::create(ref<Expr> c, ref<Expr> t, ref<Expr> f) {
   assert(kt==f->getWidth() && "type mismatch");
 
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(c)) {
-    return CE->getConstantValue() ? t : f;
+    return CE->isTrue() ? t : f;
   } else if (t==f) {
     return t;
   } else if (kt==Expr::Bool) { // c ? t : f  <=> (c and t) or (not c and f)
     if (ConstantExpr *CE = dyn_cast<ConstantExpr>(t)) {      
-      if (CE->getConstantValue()) {
+      if (CE->isTrue()) {
         return OrExpr::create(c, f);
       } else {
         return AndExpr::create(Expr::createNot(c), f);
       }
     } else if (ConstantExpr *CE = dyn_cast<ConstantExpr>(f)) {
-      if (CE->getConstantValue()) {
+      if (CE->isTrue()) {
         return OrExpr::create(Expr::createNot(c), t);
       } else {
         return AndExpr::create(c, t);
@@ -708,12 +708,11 @@ static ref<Expr> SubExpr_createPartialR(const ref<ConstantExpr> &cl, Expr *r);
 static ref<Expr> XorExpr_createPartialR(const ref<ConstantExpr> &cl, Expr *r);
 
 static ref<Expr> AddExpr_createPartialR(const ref<ConstantExpr> &cl, Expr *r) {
-  uint64_t value = cl->getConstantValue();
   Expr::Width type = cl->getWidth();
 
   if (type==Expr::Bool) {
     return XorExpr_createPartialR(cl, r);
-  } else if (!value) {
+  } else if (cl->isZero()) {
     return r;
   } else {
     Expr::Kind rk = r->getKind();
@@ -775,11 +774,9 @@ static ref<Expr> SubExpr_createPartialR(const ref<ConstantExpr> &cl, Expr *r) {
   }
 }
 static ref<Expr> SubExpr_createPartial(Expr *l, const ref<ConstantExpr> &cr) {
-  uint64_t value = cr->getConstantValue();
-  Expr::Width width = cr->getWidth();
-  uint64_t nvalue = ints::sub(0, value, width);
-
-  return AddExpr_createPartial(l, ConstantExpr::create(nvalue, width));
+  // l - c => l + (-c)
+  return AddExpr_createPartial(l, 
+                               ConstantExpr::alloc(0, cr->getWidth())->Sub(cr));
 }
 static ref<Expr> SubExpr_create(Expr *l, Expr *r) {
   Expr::Width type = l->getWidth();
@@ -809,14 +806,13 @@ static ref<Expr> SubExpr_create(Expr *l, Expr *r) {
 }
 
 static ref<Expr> MulExpr_createPartialR(const ref<ConstantExpr> &cl, Expr *r) {
-  uint64_t value = cl->getConstantValue();
   Expr::Width type = cl->getWidth();
 
   if (type == Expr::Bool) {
     return AndExpr_createPartialR(cl, r);
-  } else if (value == 1) {
+  } else if (cl->getConstantValue() == 1) {
     return r;
-  } else if (!value) {
+  } else if (cl->isZero()) {
     return cl;
   } else {
     return MulExpr::alloc(cl, r);
@@ -836,12 +832,9 @@ static ref<Expr> MulExpr_create(Expr *l, Expr *r) {
 }
 
 static ref<Expr> AndExpr_createPartial(Expr *l, const ref<ConstantExpr> &cr) {
-  uint64_t value = cr->getConstantValue();
-  Expr::Width width = cr->getWidth();
-
-  if (value==ints::sext(1, width, 1)) {
+  if (cr->isAllOnes()) {
     return l;
-  } else if (!value) {
+  } else if (cr->isZero()) {
     return cr;
   } else {
     return AndExpr::alloc(l, cr);
@@ -855,12 +848,9 @@ static ref<Expr> AndExpr_create(Expr *l, Expr *r) {
 }
 
 static ref<Expr> OrExpr_createPartial(Expr *l, const ref<ConstantExpr> &cr) {
-  uint64_t value = cr->getConstantValue();
-  Expr::Width width = cr->getWidth();
-
-  if (value == ints::sext(1, width, 1)) {
+  if (cr->isAllOnes()) {
     return cr;
-  } else if (!value) {
+  } else if (cr->isZero()) {
     return l;
   } else {
     return OrExpr::alloc(l, cr);
@@ -874,17 +864,10 @@ static ref<Expr> OrExpr_create(Expr *l, Expr *r) {
 }
 
 static ref<Expr> XorExpr_createPartialR(const ref<ConstantExpr> &cl, Expr *r) {
-  uint64_t value = cl->getConstantValue();
-  Expr::Width type = cl->getWidth();
-
-  if (type==Expr::Bool) {
-    if (value) {
-      return EqExpr_createPartial(r, ConstantExpr::create(0, Expr::Bool));
-    } else {
-      return r;
-    }
-  } else if (!value) {
+  if (cl->isZero()) {
     return r;
+  } else if (cl->getWidth() == Expr::Bool) {
+    return EqExpr_createPartial(r, ConstantExpr::create(0, Expr::Bool));
   } else {
     return XorExpr::alloc(cl, r);
   }
@@ -1028,8 +1011,6 @@ static ref<Expr> EqExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
 /// returns the initial equality expression. 
 static ref<Expr> TryConstArrayOpt(const ref<ConstantExpr> &cl, 
 				  ReadExpr *rd) {
-  uint64_t ct = cl->getConstantValue();
-
   if (rd->updates.root->isSymbolicArray() || rd->updates.getSize())
     return EqExpr_create(cl, rd);
 
@@ -1040,7 +1021,7 @@ static ref<Expr> TryConstArrayOpt(const ref<ConstantExpr> &cl,
   // where the concrete array has one update for each index, in order
   ref<Expr> res = ConstantExpr::alloc(0, Expr::Bool);
   for (unsigned i = 0, e = rd->updates.root->size; i != e; ++i) {
-    if (ct == rd->updates.root->constantValues[i]->getConstantValue()) {
+    if (cl == rd->updates.root->constantValues[i]) {
       // Arbitrary maximum on the size of disjunction.
       if (++numMatches > 100)
         return EqExpr_create(cl, rd);
@@ -1064,17 +1045,17 @@ static ref<Expr> EqExpr_createPartialR(const ref<ConstantExpr> &cl, Expr *r) {
     if (value) {
       return r;
     } else {
-      // 0 != ...
+      // 0 == ...
       
       if (rk == Expr::Eq) {
         const EqExpr *ree = cast<EqExpr>(r);
 
         // eliminate double negation
         if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ree->left)) {
-          if (CE->getWidth() == Expr::Bool) {
-            assert(!CE->getConstantValue());
+          // 0 == (0 == A) => A
+          if (CE->getWidth() == Expr::Bool &&
+              CE->isFalse())
             return ree->right;
-          }
         }
       } else if (rk == Expr::Or) {
         const OrExpr *roe = cast<OrExpr>(r);
diff --git a/lib/Expr/ExprEvaluator.cpp b/lib/Expr/ExprEvaluator.cpp
index 41cb7c48..efb0d658 100644
--- a/lib/Expr/ExprEvaluator.cpp
+++ b/lib/Expr/ExprEvaluator.cpp
@@ -75,7 +75,7 @@ ExprVisitor::Action ExprEvaluator::protectedDivOperation(const BinaryExpr &e) {
                         visit(e.right) };
 
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(kids[1]))
-    if (!CE->getConstantValue())
+    if (CE->isZero())
       kids[1] = e.right;
 
   if (kids[0]!=e.left || kids[1]!=e.right) {
diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index 6ad5fffd..d7c77fb0 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -374,7 +374,7 @@ public:
   void printConst(const ref<ConstantExpr> &e, PrintContext &PC, 
                   bool printWidth) {
     if (e->getWidth() == Expr::Bool)
-      PC << (e->getConstantValue() ? "true" : "false");
+      PC << (e->isTrue() ? "true" : "false");
     else {
       if (PCAllConstWidths)
 	printWidth = true;
diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp
index 9c233530..373f42d9 100644
--- a/lib/Solver/CexCachingSolver.cpp
+++ b/lib/Solver/CexCachingSolver.cpp
@@ -139,7 +139,7 @@ bool CexCachingSolver::lookupAssignment(const Query &query,
   KeyType key(query.constraints.begin(), query.constraints.end());
   ref<Expr> neg = Expr::createNot(query.expr);
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(neg)) {
-    if (!CE->getConstantValue()) {
+    if (CE->isFalse()) {
       result = (Assignment*) 0;
       return true;
     }
@@ -154,7 +154,7 @@ bool CexCachingSolver::getAssignment(const Query& query, Assignment *&result) {
   KeyType key(query.constraints.begin(), query.constraints.end());
   ref<Expr> neg = Expr::createNot(query.expr);
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(neg)) {
-    if (!CE->getConstantValue()) {
+    if (CE->isFalse()) {
       result = (Assignment*) 0;
       return true;
     }
@@ -220,7 +220,7 @@ bool CexCachingSolver::computeValidity(const Query& query,
   assert(isa<ConstantExpr>(q) && 
          "assignment evaluation did not result in constant");
 
-  if (cast<ConstantExpr>(q)->getConstantValue()) {
+  if (cast<ConstantExpr>(q)->isTrue()) {
     if (!getAssignment(query, a))
       return false;
     result = !a ? Solver::True : Solver::Unknown;
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index ab65f254..8680d0a8 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -608,11 +608,10 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     assert(*width_out!=1 && "uncanonicalized sdiv");
 
     if (ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right)) {
-      uint64_t divisor = CE->getConstantValue();
- 
       if (optimizeDivides) {
 	if (*width_out == 32) //only works for 32-bit division
-	  return constructSDivByConstant( left, *width_out, divisor);
+	  return constructSDivByConstant( left, *width_out, 
+                                          CE->getConstantValue());
       }
     } 
 
@@ -776,9 +775,9 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     ExprHandle left = construct(ee->left, width_out);
     ExprHandle right = construct(ee->right, width_out);
     if (*width_out==1) {
-      if (isa<ConstantExpr>(ee->left)) {
-        assert(!cast<ConstantExpr>(ee->left)->getConstantValue() && 
-               "uncanonicalized eq");
+      if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ee->left)) {
+        if (CE->isTrue())
+          return right;
         return vc_notExpr(vc, right);
       } else {
         return vc_iffExpr(vc, left, right);
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 7a1b356c..9e8e37bf 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -57,7 +57,7 @@ bool Solver::evaluate(const Query& query, Validity &result) {
 
   // Maintain invariants implementations expect.
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(query.expr)) {
-    result = CE->getConstantValue() ? True : False;
+    result = CE->isTrue() ? True : False;
     return true;
   }
 
@@ -83,7 +83,7 @@ bool Solver::mustBeTrue(const Query& query, bool &result) {
 
   // Maintain invariants implementations expect.
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(query.expr)) {
-    result = CE->getConstantValue() ? true : false;
+    result = CE->isTrue() ? true : false;
     return true;
   }
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-11 03:48:32 +0000