aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/Solver
diff options
context:
space:
mode:
authorDaniel Dunbar <daniel@zuster.org>2009-06-14 06:07:30 +0000
committerDaniel Dunbar <daniel@zuster.org>2009-06-14 06:07:30 +0000
commit7c27c8a6a7c233c3c6162d9b86942351fe5f42b3 (patch)
tree876b610183e2e4d470139b8544cd6cdbf22a6982 /lib/Solver
parentd15a30cc0ce2579747ae4c2e919af54c6b06af70 (diff)
downloadklee-7c27c8a6a7c233c3c6162d9b86942351fe5f42b3.tar.gz
Add ConstantExpr::{getLimitedValue,getZExtValue}.
- For use in situations where the range of the constant is known to fit in a uint64 (or smaller), or the extra bits don't matter. - No (intended) functionality change. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73326 91177308-0d34-0410-b5e6-96231b3b80d8
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;