diff options
author | Daniel Dunbar <daniel@zuster.org> | 2009-06-14 06:07:30 +0000 |
---|---|---|
committer | Daniel Dunbar <daniel@zuster.org> | 2009-06-14 06:07:30 +0000 |
commit | 7c27c8a6a7c233c3c6162d9b86942351fe5f42b3 (patch) | |
tree | 876b610183e2e4d470139b8544cd6cdbf22a6982 /lib/Solver | |
parent | d15a30cc0ce2579747ae4c2e919af54c6b06af70 (diff) | |
download | klee-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.cpp | 4 | ||||
-rw-r--r-- | lib/Solver/IndependentSolver.cpp | 2 | ||||
-rw-r--r-- | lib/Solver/STPBuilder.cpp | 91 | ||||
-rw-r--r-- | lib/Solver/Solver.cpp | 2 |
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; |