about summary refs log tree commit diff homepage
path: root/lib/Solver
diff options
context:
space:
mode:
authorDaniel Dunbar <daniel@zuster.org>2009-06-03 15:40:42 +0000
committerDaniel Dunbar <daniel@zuster.org>2009-06-03 15:40:42 +0000
commit32461e170b16d2f6cbcd04830bf68ce2a6372db5 (patch)
tree59c8813624c9072d2ecd14526658d6751e5a9674 /lib/Solver
parentd55171601a0537506ddd05d37a1dabe372454a6d (diff)
downloadklee-32461e170b16d2f6cbcd04830bf68ce2a6372db5.tar.gz
Kill off specialized ref<> forwarding methods, in the interest of making it a
more standard reference counting wrapper.
 - The only interesting changes here are in Ref.h, everything else is just
   updating foo.method to use foo->method instead.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72777 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'lib/Solver')
-rw-r--r--lib/Solver/CachingSolver.cpp4
-rw-r--r--lib/Solver/CexCachingSolver.cpp6
-rw-r--r--lib/Solver/FastCexSolver.cpp22
-rw-r--r--lib/Solver/IndependentSolver.cpp2
-rw-r--r--lib/Solver/STPBuilder.cpp24
-rw-r--r--lib/Solver/Solver.cpp16
6 files changed, 37 insertions, 37 deletions
diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp
index 517e133b..d353e485 100644
--- a/lib/Solver/CachingSolver.cpp
+++ b/lib/Solver/CachingSolver.cpp
@@ -49,11 +49,11 @@ private:
   
   struct CacheEntryHash {
     unsigned operator()(const CacheEntry &ce) const {
-      unsigned result = ce.query.hash();
+      unsigned result = ce.query->hash();
       
       for (ConstraintManager::constraint_iterator it = ce.constraints.begin();
            it != ce.constraints.end(); ++it)
-        result ^= it->hash();
+        result ^= (*it)->hash();
       
       return result;
     }
diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp
index 79bc985d..db15632b 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 (neg.isConstant()) {
-    if (!neg.getConstantValue()) {
+    if (!neg->getConstantValue()) {
       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 (neg.isConstant()) {
-    if (!neg.getConstantValue()) {
+    if (!neg->getConstantValue()) {
       result = (Assignment*) 0;
       return true;
     }
@@ -219,7 +219,7 @@ bool CexCachingSolver::computeValidity(const Query& query,
   ref<Expr> q = a->evaluate(query.expr);
   assert(q.isConstant() && "assignment evaluation did not result in constant");
 
-  if (q.getConstantValue()) {
+  if (q->getConstantValue()) {
     if (!getAssignment(query, a))
       return false;
     result = !a ? Solver::True : Solver::Unknown;
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp
index b6f676aa..88f34c99 100644
--- a/lib/Solver/FastCexSolver.cpp
+++ b/lib/Solver/FastCexSolver.cpp
@@ -398,7 +398,7 @@ public:
 #ifdef LOG
     //    *theLog << "force: " << e << " to " << range << "\n";
 #endif
-    switch (e.getKind()) {
+    switch (e->getKind()) {
     case Expr::Constant: {
       // rather a pity if the constant isn't in the range, but how can
       // we use this?
@@ -417,8 +417,8 @@ public:
       // XXX we need to respect the version here and object state chain
 
       if (re->index.isConstant() && 
-          re->index.getConstantValue() < array->size) {
-        CexValueData &cvd = cod.values[re->index.getConstantValue()];
+          re->index->getConstantValue() < array->size) {
+        CexValueData &cvd = cod.values[re->index->getConstantValue()];
         CexValueData tmp = cvd.set_intersection(range);
         
         if (tmp.isEmpty()) {
@@ -522,7 +522,7 @@ public:
       // possible input range.
     case Expr::ZExt: {
       CastExpr *ce = static_ref_cast<CastExpr>(e);
-      unsigned inBits = ce->src.getWidth();
+      unsigned inBits = ce->src->getWidth();
       ValueRange input = range.set_intersection(ValueRange(0, bits64::maxValueOfNBits(inBits)));
       forceExprToRange(ce->src, input);
       break;
@@ -531,7 +531,7 @@ public:
       // minus the impossible values. This is nicer since it is a single interval.
     case Expr::SExt: {
       CastExpr *ce = static_ref_cast<CastExpr>(e);
-      unsigned inBits = ce->src.getWidth();
+      unsigned inBits = ce->src->getWidth();
       unsigned outBits = ce->width;
       ValueRange output = range.set_difference(ValueRange(1<<(inBits-1),
                                                           (bits64::maxValueOfNBits(outBits)-
@@ -614,7 +614,7 @@ public:
       BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
       if (range.isFixed()) {
         if (be->left.isConstant()) {
-          uint64_t value = be->left.getConstantValue();
+          uint64_t value = be->left->getConstantValue();
           if (range.min()) {
             forceExprToValue(be->right, value);
           } else {
@@ -622,7 +622,7 @@ public:
               forceExprToRange(be->right, 
                                CexValueData(1,
                                             ints::sext(1, 
-                                                       be->right.getWidth(),
+                                                       be->right->getWidth(),
                                                        1)));
             } else {
               // XXX heuristic / lossy, could be better to pick larger range?
@@ -645,7 +645,7 @@ public:
         ValueRange left = evalRangeForExpr(be->left);
         ValueRange right = evalRangeForExpr(be->right);
 
-        uint64_t maxValue = bits64::maxValueOfNBits(be->right.getWidth());
+        uint64_t maxValue = bits64::maxValueOfNBits(be->right->getWidth());
 
         // XXX should deal with overflow (can lead to empty range)
 
@@ -678,7 +678,7 @@ public:
 
         // XXX should deal with overflow (can lead to empty range)
 
-        uint64_t maxValue = bits64::maxValueOfNBits(be->right.getWidth());
+        uint64_t maxValue = bits64::maxValueOfNBits(be->right->getWidth());
         if (left.isFixed()) {
           if (range.min()) {
             forceExprToRange(be->right, CexValueData(left.min(), maxValue));
@@ -732,7 +732,7 @@ public:
     if (!v.isConstant()) return false;
     // XXX reenable once all reads and vars are fixed
     //    assert(v.isConstant() && "not all values have been fixed");
-    return v.getConstantValue()==value;
+    return v->getConstantValue() == value;
   }
 };
 
@@ -940,7 +940,7 @@ FastCexSolver::computeInitialValues(const Query& query,
                                                        kMachinePointerType)));
       
       if (value.isConstant()) {
-        data.push_back(value.getConstantValue());
+        data.push_back(value->getConstantValue());
       } else {
         // FIXME: When does this happen?
         return false;
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index c966aff6..18e5c84d 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -99,7 +99,7 @@ public:
         if (!wholeObjects.count(array)) {
           if (re->index.isConstant()) {
             DenseSet<unsigned> &dis = elements[array];
-            dis.add((unsigned) re->index.getConstantValue());
+            dis.add((unsigned) re->index->getConstantValue());
           } else {
             elements_ty::iterator it2 = elements.find(array);
             if (it2!=elements.end())
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index a1b6e99a..1d27c655 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -447,11 +447,10 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
 
   ++stats::queryConstructs;
 
-  switch(e.getKind()) {
-
+  switch (e->getKind()) {
   case Expr::Constant: {
-    uint64_t asUInt64 = e.getConstantValue();
-    *width_out = e.getWidth();
+    uint64_t asUInt64 = e->getConstantValue();
+    *width_out = e->getWidth();
 
     if (*width_out > 64)
       assert(0 && "constructActual: width > 64");
@@ -557,7 +556,8 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     assert(*width_out!=1 && "uncanonicalized mul");
 
     if (me->left.isConstant()) {
-      return constructMulByConstant(right, *width_out, me->left.getConstantValue());
+      return constructMulByConstant(right, *width_out, 
+                                    me->left->getConstantValue());
     } else {
       ExprHandle left = construct(me->left, width_out);
       return vc_bvMultExpr(vc, *width_out, left, right);
@@ -570,7 +570,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     assert(*width_out!=1 && "uncanonicalized udiv");
     
     if (de->right.isConstant()) {
-      uint64_t divisor = de->right.getConstantValue();
+      uint64_t divisor = de->right->getConstantValue();
       
       if (bits64::isPowerOfTwo(divisor)) {
         return bvRightShift(left,
@@ -592,7 +592,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     assert(*width_out!=1 && "uncanonicalized sdiv");
 
     if (de->right.isConstant()) {
-      uint64_t divisor = de->right.getConstantValue();
+      uint64_t divisor = de->right->getConstantValue();
  
       if (optimizeDivides) {
 	if (*width_out == 32) //only works for 32-bit division
@@ -612,7 +612,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     assert(*width_out!=1 && "uncanonicalized urem");
     
     if (de->right.isConstant()) {
-      uint64_t divisor = de->right.getConstantValue();
+      uint64_t divisor = de->right->getConstantValue();
 
       if (bits64::isPowerOfTwo(divisor)) {
         unsigned bits = bits64::indexOfSingleBit(divisor);
@@ -711,7 +711,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     assert(*width_out!=1 && "uncanonicalized shl");
 
     if (se->right.isConstant()) {
-      return bvLeftShift(left, se->right.getConstantValue(), getShiftBits(*width_out));
+      return bvLeftShift(left, se->right->getConstantValue(), getShiftBits(*width_out));
     } else {
       int shiftWidth;
       ExprHandle amount = construct(se->right, &shiftWidth);
@@ -726,7 +726,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     assert(*width_out!=1 && "uncanonicalized lshr");
 
     if (lse->right.isConstant()) {
-      return bvRightShift(left, (unsigned) lse->right.getConstantValue(), shiftBits);
+      return bvRightShift(left, (unsigned) lse->right->getConstantValue(), shiftBits);
     } else {
       int shiftWidth;
       ExprHandle amount = construct(lse->right, &shiftWidth);
@@ -740,7 +740,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     assert(*width_out!=1 && "uncanonicalized ashr");
     
     if (ase->right.isConstant()) {
-      unsigned shift = (unsigned) ase->right.getConstantValue();
+      unsigned shift = (unsigned) ase->right->getConstantValue();
       ExprHandle signedBool = bvBoolExtract(left, *width_out-1);
       return constructAShrByConstant(left, shift, signedBool, getShiftBits(*width_out));
     } else {
@@ -758,7 +758,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     ExprHandle right = construct(ee->right, width_out);
     if (*width_out==1) {
       if (ee->left.isConstant()) {
-        assert(!ee->left.getConstantValue() && "uncanonicalized eq");
+        assert(!ee->left->getConstantValue() && "uncanonicalized eq");
         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 ae378ac1..8990e3b9 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -53,11 +53,11 @@ SolverImpl::~SolverImpl() {
 }
 
 bool Solver::evaluate(const Query& query, Validity &result) {
-  assert(query.expr.getWidth() == Expr::Bool && "Invalid expression type!");
+  assert(query.expr->getWidth() == Expr::Bool && "Invalid expression type!");
 
-  // Maintain invariants implementation expect.
+  // Maintain invariants implementations expect.
   if (query.expr.isConstant()) {
-    result = query.expr.getConstantValue() ? True : False;
+    result = query.expr->getConstantValue() ? True : False;
     return true;
   }
 
@@ -79,11 +79,11 @@ bool SolverImpl::computeValidity(const Query& query, Solver::Validity &result) {
 }
 
 bool Solver::mustBeTrue(const Query& query, bool &result) {
-  assert(query.expr.getWidth() == Expr::Bool && "Invalid expression type!");
+  assert(query.expr->getWidth() == Expr::Bool && "Invalid expression type!");
 
-  // Maintain invariants implementation expect.
+  // Maintain invariants implementations expect.
   if (query.expr.isConstant()) {
-    result = query.expr.getConstantValue() ? true : false;
+    result = query.expr->getConstantValue() ? true : false;
     return true;
   }
 
@@ -136,7 +136,7 @@ Solver::getInitialValues(const Query& query,
 
 std::pair< ref<Expr>, ref<Expr> > Solver::getRange(const Query& query) {
   ref<Expr> e = query.expr;
-  Expr::Width width = e.getWidth();
+  Expr::Width width = e->getWidth();
   uint64_t min, max;
 
   if (width==1) {
@@ -152,7 +152,7 @@ std::pair< ref<Expr>, ref<Expr> > Solver::getRange(const Query& query) {
       min = 0, max = 1; break;
     }
   } else if (e.isConstant()) {
-    min = max = e.getConstantValue();
+    min = max = e->getConstantValue();
   } else {
     // binary search for # of useful bits
     uint64_t lo=0, hi=width, mid, bits=0;