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/FastCexSolver.cpp4
-rw-r--r--lib/Solver/IndependentSolver.cpp2
-rw-r--r--lib/Solver/STPBuilder.cpp91
-rw-r--r--lib/Solver/Solver.cpp2
4 files changed, 52 insertions, 47 deletions
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp
index af2666ab..8c2fcfe6 100644
--- a/lib/Solver/FastCexSolver.cpp
+++ b/lib/Solver/FastCexSolver.cpp
@@ -346,7 +346,7 @@ public:
     if (array.isConstantArray() && 
         index.isFixed() && 
         index.min() < array.size)
-      return ValueRange(array.constantValues[index.min()]->getConstantValue());
+      return ValueRange(array.constantValues[index.min()]->getZExtValue(8));
 
     return ValueRange(0, 255);
   }
@@ -1037,7 +1037,7 @@ FastCexSolver::computeInitialValues(const Query& query,
       ref<Expr> value = cd.evaluatePossible(read);
       
       if (ConstantExpr *CE = dyn_cast<ConstantExpr>(value)) {
-        data.push_back((unsigned char) CE->getConstantValue());
+        data.push_back((unsigned char) CE->getZExtValue(8));
       } else {
         // FIXME: When does this happen?
         return false;
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index 1f3ea798..3e19dbc6 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -104,7 +104,7 @@ public:
       if (!wholeObjects.count(array)) {
         if (ConstantExpr *CE = dyn_cast<ConstantExpr>(re->index)) {
           DenseSet<unsigned> &dis = elements[array];
-          dis.add((unsigned) CE->getConstantValue());
+          dis.add((unsigned) CE->getZExtValue(32));
         } 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 8680d0a8..3d6f789e 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -571,13 +571,13 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     ExprHandle right = construct(me->right, width_out);
     assert(*width_out!=1 && "uncanonicalized mul");
 
-    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(me->left)) {
-      return constructMulByConstant(right, *width_out, 
-                                    CE->getConstantValue());
-    } else {
-      ExprHandle left = construct(me->left, width_out);
-      return vc_bvMultExpr(vc, *width_out, left, right);
-    }
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(me->left))
+      if (CE->getWidth() <= 64)
+        return constructMulByConstant(right, *width_out, 
+                                      CE->getZExtValue());
+
+    ExprHandle left = construct(me->left, width_out);
+    return vc_bvMultExpr(vc, *width_out, left, right);
   }
 
   case Expr::UDiv: {
@@ -586,15 +586,18 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     assert(*width_out!=1 && "uncanonicalized udiv");
     
     if (ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right)) {
-      uint64_t divisor = CE->getConstantValue();
+      if (CE->getWidth() <= 64) {
+        uint64_t divisor = CE->getConstantValue();
       
-      if (bits64::isPowerOfTwo(divisor)) {
-        return bvRightShift(left,
-                            bits64::indexOfSingleBit(divisor),
-                            getShiftBits(*width_out));
-      } else if (optimizeDivides) {
-        if (*width_out == 32) //only works for 32-bit division
-          return constructUDivByConstant( left, *width_out, (uint32_t)divisor );
+        if (bits64::isPowerOfTwo(divisor)) {
+          return bvRightShift(left,
+                              bits64::indexOfSingleBit(divisor),
+                              getShiftBits(*width_out));
+        } else if (optimizeDivides) {
+          if (*width_out == 32) //only works for 32-bit division
+            return constructUDivByConstant( left, *width_out, 
+                                            (uint32_t) divisor);
+        }
       }
     } 
 
@@ -607,13 +610,11 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     ExprHandle left = construct(de->left, width_out);
     assert(*width_out!=1 && "uncanonicalized sdiv");
 
-    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right)) {
-      if (optimizeDivides) {
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right))
+      if (optimizeDivides)
 	if (*width_out == 32) //only works for 32-bit division
 	  return constructSDivByConstant( left, *width_out, 
-                                          CE->getConstantValue());
-      }
-    } 
+                                          CE->getZExtValue(32));
 
     // XXX need to test for proper handling of sign, not sure I
     // trust STP
@@ -627,30 +628,34 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     assert(*width_out!=1 && "uncanonicalized urem");
     
     if (ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right)) {
-      uint64_t divisor = CE->getConstantValue();
+      if (CE->getWidth() <= 64) {
+        uint64_t divisor = CE->getConstantValue();
+
+        if (bits64::isPowerOfTwo(divisor)) {
+          unsigned bits = bits64::indexOfSingleBit(divisor);
+
+          // special case for modding by 1 or else we bvExtract -1:0
+          if (bits == 0) {
+            return bvZero(*width_out);
+          } else {
+            return vc_bvConcatExpr(vc,
+                                   bvZero(*width_out - bits),
+                                   bvExtract(left, bits - 1, 0));
+          }
+        }
 
-      if (bits64::isPowerOfTwo(divisor)) {
-        unsigned bits = bits64::indexOfSingleBit(divisor);
+      // Use fast division to compute modulo without explicit division for
+      // constant divisor.
 
-        // special case for modding by 1 or else we bvExtract -1:0
-        if (bits == 0) {
-          return bvZero(*width_out);
-        } else {
-          return vc_bvConcatExpr(vc,
-                                 bvZero(*width_out - bits),
-                                 bvExtract(left, bits - 1, 0));
+        if (optimizeDivides) {
+          if (*width_out == 32) { //only works for 32-bit division
+            ExprHandle quotient = constructUDivByConstant( left, *width_out, (uint32_t)divisor );
+            ExprHandle quot_times_divisor = constructMulByConstant( quotient, *width_out, divisor );
+            ExprHandle rem = vc_bvMinusExpr( vc, *width_out, left, quot_times_divisor );
+            return rem;
+          }
         }
       }
-
-      //use fast division to compute modulo without explicit division for constant divisor
-      if (optimizeDivides) {
-	if (*width_out == 32) { //only works for 32-bit division
-	  ExprHandle quotient = constructUDivByConstant( left, *width_out, (uint32_t)divisor );
-	  ExprHandle quot_times_divisor = constructMulByConstant( quotient, *width_out, divisor );
-          ExprHandle rem = vc_bvMinusExpr( vc, *width_out, left, quot_times_divisor );
-	  return rem;
-	}
-      }
     }
     
     ExprHandle right = construct(de->right, width_out);
@@ -726,7 +731,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     assert(*width_out!=1 && "uncanonicalized shl");
 
     if (ConstantExpr *CE = dyn_cast<ConstantExpr>(se->right)) {
-      return bvLeftShift(left, CE->getConstantValue(), 
+      return bvLeftShift(left, (unsigned) CE->getLimitedValue(), 
                          getShiftBits(*width_out));
     } else {
       int shiftWidth;
@@ -742,7 +747,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     assert(*width_out!=1 && "uncanonicalized lshr");
 
     if (ConstantExpr *CE = dyn_cast<ConstantExpr>(lse->right)) {
-      return bvRightShift(left, (unsigned) CE->getConstantValue(), 
+      return bvRightShift(left, (unsigned) CE->getLimitedValue(), 
                           shiftBits);
     } else {
       int shiftWidth;
@@ -757,7 +762,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     assert(*width_out!=1 && "uncanonicalized ashr");
     
     if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ase->right)) {
-      unsigned shift = (unsigned) CE->getConstantValue();
+      unsigned shift = (unsigned) CE->getLimitedValue();
       ExprHandle signedBool = bvBoolExtract(left, *width_out-1);
       return constructAShrByConstant(left, shift, signedBool, 
                                      getShiftBits(*width_out));
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 9e8e37bf..f8f9d690 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -158,7 +158,7 @@ std::pair< ref<Expr>, ref<Expr> > Solver::getRange(const Query& query) {
       min = 0, max = 1; break;
     }
   } else if (ConstantExpr *CE = dyn_cast<ConstantExpr>(e)) {
-    min = max = CE->getConstantValue();
+    min = max = CE->getZExtValue();
   } 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-30 23:27:14 +0000