about summary refs log tree commit diff homepage
path: root/lib/Solver
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Solver')
-rw-r--r--lib/Solver/CexCachingSolver.cpp8
-rw-r--r--lib/Solver/FastCexSolver.cpp27
-rw-r--r--lib/Solver/IndependentSolver.cpp4
-rw-r--r--lib/Solver/STPBuilder.cpp37
-rw-r--r--lib/Solver/Solver.cpp12
5 files changed, 46 insertions, 42 deletions
diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp
index 49db74e8..1eaec4d9 100644
--- a/lib/Solver/CexCachingSolver.cpp
+++ b/lib/Solver/CexCachingSolver.cpp
@@ -138,8 +138,8 @@ bool CexCachingSolver::lookupAssignment(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 (ConstantExpr *CE = dyn_cast<ConstantExpr>(neg)) {
+    if (!CE->getConstantValue()) {
       result = (Assignment*) 0;
       return true;
     }
@@ -153,8 +153,8 @@ 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);
-  if (neg->isConstant()) {
-    if (!neg->getConstantValue()) {
+  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(neg)) {
+    if (!CE->getConstantValue()) {
       result = (Assignment*) 0;
       return true;
     }
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp
index a0d943d3..1a1cfe62 100644
--- a/lib/Solver/FastCexSolver.cpp
+++ b/lib/Solver/FastCexSolver.cpp
@@ -416,16 +416,17 @@ 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()];
-        CexValueData tmp = cvd.set_intersection(range);
+      if (ConstantExpr *CE = dyn_cast<ConstantExpr>(re->index)) {
+        if (CE->getConstantValue() < array->size) {
+          CexValueData &cvd = cod.values[CE->getConstantValue()];
+          CexValueData tmp = cvd.set_intersection(range);
         
-        if (tmp.isEmpty()) {
-          if (range.isFixed()) // ranges conflict, if new one is fixed use that
-            cvd = range;
-        } else {
-          cvd = tmp;
+          if (tmp.isEmpty()) {
+            if (range.isFixed()) // ranges conflict, if new one is fixed use that
+              cvd = range;
+          } else {
+            cvd = tmp;
+          }
         }
       } else {
         // XXX        fatal("XXX not implemented");
@@ -613,8 +614,8 @@ public:
     case Expr::Eq: {
       BinaryExpr *be = cast<BinaryExpr>(e);
       if (range.isFixed()) {
-        if (be->left->isConstant()) {
-          uint64_t value = be->left->getConstantValue();
+        if (ConstantExpr *CE = dyn_cast<ConstantExpr>(be->left)) {
+          uint64_t value = CE->getConstantValue();
           if (range.min()) {
             forceExprToValue(be->right, value);
           } else {
@@ -939,8 +940,8 @@ FastCexSolver::computeInitialValues(const Query& query,
                                   ConstantExpr::create(i,
                                                        kMachinePointerType)));
       
-      if (value->isConstant()) {
-        data.push_back(value->getConstantValue());
+      if (ConstantExpr *CE = dyn_cast<ConstantExpr>(value)) {
+        data.push_back(CE->getConstantValue());
       } else {
         // FIXME: When does this happen?
         return false;
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index 4e004fd8..455e9240 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -97,9 +97,9 @@ public:
       if (re->updates.isRooted) {
         const Array *array = re->updates.root;
         if (!wholeObjects.count(array)) {
-          if (re->index->isConstant()) {
+          if (ConstantExpr *CE = dyn_cast<ConstantExpr>(re->index)) {
             DenseSet<unsigned> &dis = elements[array];
-            dis.add((unsigned) re->index->getConstantValue());
+            dis.add((unsigned) CE->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 00fd8e4a..88bdd2b0 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -555,9 +555,9 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     ExprHandle right = construct(me->right, width_out);
     assert(*width_out!=1 && "uncanonicalized mul");
 
-    if (me->left->isConstant()) {
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(me->left)) {
       return constructMulByConstant(right, *width_out, 
-                                    me->left->getConstantValue());
+                                    CE->getConstantValue());
     } else {
       ExprHandle left = construct(me->left, width_out);
       return vc_bvMultExpr(vc, *width_out, left, right);
@@ -569,8 +569,8 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     ExprHandle left = construct(de->left, width_out);
     assert(*width_out!=1 && "uncanonicalized udiv");
     
-    if (de->right->isConstant()) {
-      uint64_t divisor = de->right->getConstantValue();
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right)) {
+      uint64_t divisor = CE->getConstantValue();
       
       if (bits64::isPowerOfTwo(divisor)) {
         return bvRightShift(left,
@@ -591,8 +591,8 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     ExprHandle left = construct(de->left, width_out);
     assert(*width_out!=1 && "uncanonicalized sdiv");
 
-    if (de->right->isConstant()) {
-      uint64_t divisor = de->right->getConstantValue();
+    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
@@ -611,8 +611,8 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     ExprHandle left = construct(de->left, width_out);
     assert(*width_out!=1 && "uncanonicalized urem");
     
-    if (de->right->isConstant()) {
-      uint64_t divisor = de->right->getConstantValue();
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right)) {
+      uint64_t divisor = CE->getConstantValue();
 
       if (bits64::isPowerOfTwo(divisor)) {
         unsigned bits = bits64::indexOfSingleBit(divisor);
@@ -710,8 +710,9 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     ExprHandle left = construct(se->left, width_out);
     assert(*width_out!=1 && "uncanonicalized shl");
 
-    if (se->right->isConstant()) {
-      return bvLeftShift(left, se->right->getConstantValue(), getShiftBits(*width_out));
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(se->right)) {
+      return bvLeftShift(left, CE->getConstantValue(), 
+                         getShiftBits(*width_out));
     } else {
       int shiftWidth;
       ExprHandle amount = construct(se->right, &shiftWidth);
@@ -725,8 +726,9 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     unsigned shiftBits = getShiftBits(*width_out);
     assert(*width_out!=1 && "uncanonicalized lshr");
 
-    if (lse->right->isConstant()) {
-      return bvRightShift(left, (unsigned) lse->right->getConstantValue(), shiftBits);
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(lse->right)) {
+      return bvRightShift(left, (unsigned) CE->getConstantValue(), 
+                          shiftBits);
     } else {
       int shiftWidth;
       ExprHandle amount = construct(lse->right, &shiftWidth);
@@ -739,10 +741,11 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     ExprHandle left = construct(ase->left, width_out);
     assert(*width_out!=1 && "uncanonicalized ashr");
     
-    if (ase->right->isConstant()) {
-      unsigned shift = (unsigned) ase->right->getConstantValue();
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ase->right)) {
+      unsigned shift = (unsigned) CE->getConstantValue();
       ExprHandle signedBool = bvBoolExtract(left, *width_out-1);
-      return constructAShrByConstant(left, shift, signedBool, getShiftBits(*width_out));
+      return constructAShrByConstant(left, shift, signedBool, 
+                                     getShiftBits(*width_out));
     } else {
       int shiftWidth;
       ExprHandle amount = construct(ase->right, &shiftWidth);
@@ -757,8 +760,8 @@ 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 (ee->left->isConstant()) {
-        assert(!ee->left->getConstantValue() && "uncanonicalized eq");
+      if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ee->left)) {
+        assert(!CE->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 6cbf6ac0..3db049cd 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -56,8 +56,8 @@ bool Solver::evaluate(const Query& query, Validity &result) {
   assert(query.expr->getWidth() == Expr::Bool && "Invalid expression type!");
 
   // Maintain invariants implementations expect.
-  if (query.expr->isConstant()) {
-    result = query.expr->getConstantValue() ? True : False;
+  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(query.expr)) {
+    result = CE->getConstantValue() ? True : False;
     return true;
   }
 
@@ -82,8 +82,8 @@ bool Solver::mustBeTrue(const Query& query, bool &result) {
   assert(query.expr->getWidth() == Expr::Bool && "Invalid expression type!");
 
   // Maintain invariants implementations expect.
-  if (query.expr->isConstant()) {
-    result = query.expr->getConstantValue() ? true : false;
+  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(query.expr)) {
+    result = CE->getConstantValue() ? true : false;
     return true;
   }
 
@@ -151,8 +151,8 @@ std::pair< ref<Expr>, ref<Expr> > Solver::getRange(const Query& query) {
     default:
       min = 0, max = 1; break;
     }
-  } else if (e->isConstant()) {
-    min = max = e->getConstantValue();
+  } else if (ConstantExpr *CE = dyn_cast<ConstantExpr>(e)) {
+    min = max = CE->getConstantValue();
   } else {
     // binary search for # of useful bits
     uint64_t lo=0, hi=width, mid, bits=0;
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-26 15:08:26 +0000