diff options
Diffstat (limited to 'lib/Solver')
| -rw-r--r-- | lib/Solver/FastCexSolver.cpp | 64 | ||||
| -rw-r--r-- | lib/Solver/IndependentSolver.cpp | 39 | ||||
| -rwxr-xr-x | lib/Solver/Makefile | 3 | ||||
| -rw-r--r-- | lib/Solver/MetaSMTBuilder.h | 18 | ||||
| -rw-r--r-- | lib/Solver/QueryLoggingSolver.cpp | 10 | ||||
| -rw-r--r-- | lib/Solver/QueryLoggingSolver.h | 10 | ||||
| -rw-r--r-- | lib/Solver/STPBuilder.cpp | 108 | ||||
| -rw-r--r-- | lib/Solver/STPBuilder.h | 19 | ||||
| -rw-r--r-- | lib/Solver/Solver.cpp | 17 |
9 files changed, 140 insertions, 148 deletions
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp index 08a9ef7c..57e44806 100644 --- a/lib/Solver/FastCexSolver.cpp +++ b/lib/Solver/FastCexSolver.cpp @@ -18,7 +18,9 @@ // FIXME: Use APInt. #include "klee/Internal/Support/IntEvaluation.h" -#include <iostream> +#define DEBUG_TYPE "cex-solver" +#include "llvm/Support/Debug.h" +#include "llvm/Support/raw_ostream.h" #include <sstream> #include <cassert> #include <map> @@ -109,7 +111,7 @@ public: ValueRange(uint64_t _min, uint64_t _max) : m_min(_min), m_max(_max) {} ValueRange(const ValueRange &b) : m_min(b.m_min), m_max(b.m_max) {} - void print(std::ostream &os) const { + void print(llvm::raw_ostream &os) const { if (isFixed()) { os << m_min; } else { @@ -283,7 +285,8 @@ public: } }; -inline std::ostream &operator<<(std::ostream &os, const ValueRange &vr) { +inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, + const ValueRange &vr) { vr.print(os); return os; } @@ -363,12 +366,12 @@ protected: // value cannot be part of the assignment. if (index >= array.size) return ReadExpr::create(UpdateList(&array, 0), - ConstantExpr::alloc(index, Expr::Int32)); + ConstantExpr::alloc(index, array.getDomain())); std::map<const Array*, CexObjectData*>::iterator it = objects.find(&array); return ConstantExpr::alloc((it == objects.end() ? 127 : it->second->getPossibleValue(index)), - Expr::Int8); + array.getRange()); } public: @@ -384,19 +387,19 @@ protected: // value cannot be part of the assignment. if (index >= array.size) return ReadExpr::create(UpdateList(&array, 0), - ConstantExpr::alloc(index, Expr::Int32)); + ConstantExpr::alloc(index, array.getDomain())); std::map<const Array*, CexObjectData*>::iterator it = objects.find(&array); if (it == objects.end()) return ReadExpr::create(UpdateList(&array, 0), - ConstantExpr::alloc(index, Expr::Int32)); + ConstantExpr::alloc(index, array.getDomain())); CexValueData cvd = it->second->getExactValues(index); if (!cvd.isFixed()) return ReadExpr::create(UpdateList(&array, 0), - ConstantExpr::alloc(index, Expr::Int32)); + ConstantExpr::alloc(index, array.getDomain())); - return ConstantExpr::alloc(cvd.min(), Expr::Int8); + return ConstantExpr::alloc(cvd.min(), array.getRange()); } public: @@ -405,10 +408,6 @@ public: : objects(_objects) {} }; -#if 0 -#define DEBUG -#endif - class CexData { public: std::map<const Array*, CexObjectData*> objects; @@ -442,9 +441,7 @@ public: } void propogatePossibleValues(ref<Expr> e, CexValueData range) { - #ifdef DEBUG - std::cerr << "propogate: " << range << " for\n" << e << "\n"; - #endif + DEBUG(llvm::errs() << "propogate: " << range << " for\n" << e << "\n";); switch (e->getKind()) { case Expr::Constant: @@ -938,27 +935,29 @@ public: } void dump() { - std::cerr << "-- propogated values --\n"; - for (std::map<const Array*, CexObjectData*>::iterator - it = objects.begin(), ie = objects.end(); it != ie; ++it) { + llvm::errs() << "-- propogated values --\n"; + for (std::map<const Array *, CexObjectData *>::iterator + it = objects.begin(), + ie = objects.end(); + it != ie; ++it) { const Array *A = it->first; CexObjectData *COD = it->second; - - std::cerr << A->name << "\n"; - std::cerr << "possible: ["; + + llvm::errs() << A->name << "\n"; + llvm::errs() << "possible: ["; for (unsigned i = 0; i < A->size; ++i) { if (i) - std::cerr << ", "; - std::cerr << COD->getPossibleValues(i); + llvm::errs() << ", "; + llvm::errs() << COD->getPossibleValues(i); } - std::cerr << "]\n"; - std::cerr << "exact : ["; + llvm::errs() << "]\n"; + llvm::errs() << "exact : ["; for (unsigned i = 0; i < A->size; ++i) { if (i) - std::cerr << ", "; - std::cerr << COD->getExactValues(i); + llvm::errs() << ", "; + llvm::errs() << COD->getExactValues(i); } - std::cerr << "]\n"; + llvm::errs() << "]\n"; } } }; @@ -1009,9 +1008,7 @@ static bool propogateValues(const Query& query, CexData &cd, cd.propogateExactValue(query.expr, 0); } -#ifdef DEBUG - cd.dump(); -#endif + DEBUG(cd.dump();); // Check the result. bool hasSatisfyingAssignment = true; @@ -1109,13 +1106,14 @@ FastCexSolver::computeInitialValues(const Query& query, // Propogation found a satisfying assignment, compute the initial values. for (unsigned i = 0; i != objects.size(); ++i) { const Array *array = objects[i]; + assert(array); std::vector<unsigned char> data; data.reserve(array->size); for (unsigned i=0; i < array->size; i++) { ref<Expr> read = ReadExpr::create(UpdateList(array, 0), - ConstantExpr::create(i, Expr::Int32)); + ConstantExpr::create(i, array->getDomain())); ref<Expr> value = cd.evaluatePossible(read); if (ConstantExpr *CE = dyn_cast<ConstantExpr>(value)) { diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index d9fc77dc..46b4ee56 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -15,10 +15,12 @@ #include "klee/util/ExprUtil.h" +#define DEBUG_TYPE "independent-solver" +#include "llvm/Support/Debug.h" +#include "llvm/Support/raw_ostream.h" #include <map> #include <vector> #include <ostream> -#include <iostream> using namespace klee; using namespace llvm; @@ -60,7 +62,7 @@ public: return false; } - void print(std::ostream &os) const { + void print(llvm::raw_ostream &os) const { bool first = true; os << "{"; for (typename set_ty::iterator it = s.begin(), ie = s.end(); @@ -76,8 +78,9 @@ public: } }; -template<class T> -inline std::ostream &operator<<(std::ostream &os, const ::DenseSet<T> &dis) { +template <class T> +inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, + const ::DenseSet<T> &dis) { dis.print(os); return os; } @@ -124,7 +127,7 @@ public: return *this; } - void print(std::ostream &os) const { + void print(llvm::raw_ostream &os) const { os << "{"; bool first = true; for (std::set<const Array*>::iterator it = wholeObjects.begin(), @@ -214,7 +217,8 @@ public: } }; -inline std::ostream &operator<<(std::ostream &os, const IndependentElementSet &ies) { +inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, + const IndependentElementSet &ies) { ies.print(os); return os; } @@ -247,20 +251,21 @@ IndependentElementSet getIndependentConstraints(const Query& query, worklist.swap(newWorklist); } while (!done); - if (0) { +DEBUG( std::set< ref<Expr> > reqset(result.begin(), result.end()); - std::cerr << "--\n"; - std::cerr << "Q: " << query.expr << "\n"; - std::cerr << "\telts: " << IndependentElementSet(query.expr) << "\n"; + errs() << "--\n"; + errs() << "Q: " << query.expr << "\n"; + errs() << "\telts: " << IndependentElementSet(query.expr) << "\n"; int i = 0; - for (ConstraintManager::const_iterator it = query.constraints.begin(), - ie = query.constraints.end(); it != ie; ++it) { - std::cerr << "C" << i++ << ": " << *it; - std::cerr << " " << (reqset.count(*it) ? "(required)" : "(independent)") << "\n"; - std::cerr << "\telts: " << IndependentElementSet(*it) << "\n"; + for (ConstraintManager::const_iterator it = query.constraints.begin(), + ie = query.constraints.end(); it != ie; ++it) { + errs() << "C" << i++ << ": " << *it; + errs() << " " << (reqset.count(*it) ? "(required)" : "(independent)") << "\n"; + errs() << "\telts: " << IndependentElementSet(*it) << "\n"; } - std::cerr << "elts closure: " << eltsClosure << "\n"; - } + errs() << "elts closure: " << eltsClosure << "\n"; + ); + return eltsClosure; } diff --git a/lib/Solver/Makefile b/lib/Solver/Makefile index 2be74c01..a44b4f6e 100755 --- a/lib/Solver/Makefile +++ b/lib/Solver/Makefile @@ -12,6 +12,7 @@ LEVEL=../.. LIBRARYNAME=kleaverSolver DONT_BUILD_RELINKED=1 BUILD_ARCHIVE=1 +NO_INSTALL=1 include $(LEVEL)/Makefile.common @@ -22,4 +23,4 @@ ifeq ($(ENABLE_METASMT),1) CXX.Flags := $(filter-out -fno-rtti,$(CXX.Flags)) CXX.Flags += $(metaSMT_CXXFLAGS) CXX.Flags += $(metaSMT_INCLUDES) -endif \ No newline at end of file +endif diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h index 2b084ac7..b5c99907 100644 --- a/lib/Solver/MetaSMTBuilder.h +++ b/lib/Solver/MetaSMTBuilder.h @@ -187,7 +187,7 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::getInitialArr if (!hashed) { - array_expr = evaluate(_solver, buildArray(8, 32)); + array_expr = evaluate(_solver, buildArray(root->getRange(), root->getDomain())); if (root->isConstantArray()) { for (unsigned i = 0, e = root->size; i != e; ++i) { @@ -599,11 +599,11 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructActu ++stats::queryConstructs; -// std::cerr << "Constructing expression "; -// ExprPPrinter::printSingleExpr(std::cerr, e); -// std::cerr << "\n"; +// llvm::errs() << "Constructing expression "; +// ExprPPrinter::printSingleExpr(llvm::errs(), e); +// llvm::errs() << "\n"; - switch (e->getKind()) { + switch (e->getKind()) { case Expr::Constant: { @@ -614,7 +614,7 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructActu // Coerce to bool if necessary. if (coe_width == 1) { - res = (coe->isTrue()) ? getTrue() : getFalse(); + res = (coe->isTrue()) ? getTrue() : getFalse(); } else if (coe_width <= 32) { res = bvConst32(coe_width, coe->getZExtValue(32)); @@ -624,7 +624,7 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructActu } else { ref<ConstantExpr> tmp = coe; - res = bvConst64(64, tmp->Extract(0, 64)->getZExtValue()); + res = bvConst64(64, tmp->Extract(0, 64)->getZExtValue()); while (tmp->getWidth() > 64) { tmp = tmp->Extract(64, tmp->getWidth() - 64); unsigned min_width = std::min(64U, tmp->getWidth()); @@ -658,9 +658,9 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructActu case Expr::Read: { ReadExpr *re = cast<ReadExpr>(e); - assert(re); + assert(re && re->updates.root); + *width_out = re->updates.root->getRange(); // FixMe call method of Array - *width_out = 8; res = evaluate(_solver, metaSMT::logic::Array::select( getArrayForUpdate(re->updates.root, re->updates.head), diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp index f2e38182..d5598d1d 100644 --- a/lib/Solver/QueryLoggingSolver.cpp +++ b/lib/Solver/QueryLoggingSolver.cpp @@ -18,9 +18,10 @@ QueryLoggingSolver::QueryLoggingSolver(Solver *_solver, std::string path, const std::string& commentSign, int queryTimeToLog) - : solver(_solver), - os(path.c_str(), std::ios::trunc), - logBuffer(""), + : solver(_solver), + os(path.c_str(), ErrorInfo), + BufferString(""), + logBuffer(BufferString), queryCount(0), minQueryTimeToLog(queryTimeToLog), startTime(0.0f), @@ -79,8 +80,7 @@ void QueryLoggingSolver::flushBuffer() { } // prepare the buffer for reuse - logBuffer.clear(); - logBuffer.str(""); + BufferString = ""; } bool QueryLoggingSolver::computeTruth(const Query& query, bool& isValid) { diff --git a/lib/Solver/QueryLoggingSolver.h b/lib/Solver/QueryLoggingSolver.h index 2c7d80e8..ad1722ca 100644 --- a/lib/Solver/QueryLoggingSolver.h +++ b/lib/Solver/QueryLoggingSolver.h @@ -12,6 +12,7 @@ #include "klee/Solver.h" #include "klee/SolverImpl.h" +#include "llvm/Support/raw_ostream.h" #include <fstream> #include <sstream> @@ -25,9 +26,12 @@ class QueryLoggingSolver : public SolverImpl { protected: Solver *solver; - std::ofstream os; - std::ostringstream logBuffer; // buffer to store logs before flushing to - // file + std::string ErrorInfo; + llvm::raw_fd_ostream os; + // @brief Buffer used by logBuffer + std::string BufferString; + // @brief buffer to store logs before flushing to file + llvm::raw_string_ostream logBuffer; unsigned queryCount; int minQueryTimeToLog; // we log to file only those queries // which take longer than the specified time (ms); diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index 90252656..34ce0ede 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -34,7 +34,6 @@ #include <algorithm> // max, min #include <cassert> -#include <iostream> #include <map> #include <sstream> #include <vector> @@ -174,14 +173,13 @@ ExprHandle STPBuilder::eqExpr(ExprHandle a, ExprHandle b) { } // logical right shift -ExprHandle STPBuilder::bvRightShift(ExprHandle expr, unsigned amount, unsigned shiftBits) { +ExprHandle STPBuilder::bvRightShift(ExprHandle expr, unsigned shift) { unsigned width = vc_getBVLength(vc, expr); - unsigned shift = amount & ((1<<shiftBits) - 1); if (shift==0) { return expr; } else if (shift>=width) { - return bvZero(width); + return bvZero(width); // Overshift to zero } else { return vc_bvConcatExpr(vc, bvZero(shift), @@ -190,14 +188,13 @@ ExprHandle STPBuilder::bvRightShift(ExprHandle expr, unsigned amount, unsigned s } // logical left shift -ExprHandle STPBuilder::bvLeftShift(ExprHandle expr, unsigned amount, unsigned shiftBits) { +ExprHandle STPBuilder::bvLeftShift(ExprHandle expr, unsigned shift) { unsigned width = vc_getBVLength(vc, expr); - unsigned shift = amount & ((1<<shiftBits) - 1); if (shift==0) { return expr; } else if (shift>=width) { - return bvZero(width); + return bvZero(width); // Overshift to zero } else { // stp shift does "expr @ [0 x s]" which we then have to extract, // rolling our own gives slightly smaller exprs @@ -208,96 +205,97 @@ ExprHandle STPBuilder::bvLeftShift(ExprHandle expr, unsigned amount, unsigned sh } // left shift by a variable amount on an expression of the specified width -ExprHandle STPBuilder::bvVarLeftShift(ExprHandle expr, ExprHandle amount, unsigned width) { +ExprHandle STPBuilder::bvVarLeftShift(ExprHandle expr, ExprHandle shift) { + unsigned width = vc_getBVLength(vc, expr); ExprHandle res = bvZero(width); - int shiftBits = getShiftBits( width ); - - //get the shift amount (looking only at the bits appropriate for the given width) - ExprHandle shift = vc_bvExtract( vc, amount, shiftBits - 1, 0 ); - //construct a big if-then-elif-elif-... with one case per possible shift amount for( int i=width-1; i>=0; i-- ) { res = vc_iteExpr(vc, - eqExpr(shift, bvConst32(shiftBits, i)), - bvLeftShift(expr, i, shiftBits), + eqExpr(shift, bvConst32(width, i)), + bvLeftShift(expr, i), res); } + + // If overshifting, shift to zero + res = vc_iteExpr(vc, + vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)), + res, + bvZero(width)); return res; } // logical right shift by a variable amount on an expression of the specified width -ExprHandle STPBuilder::bvVarRightShift(ExprHandle expr, ExprHandle amount, unsigned width) { +ExprHandle STPBuilder::bvVarRightShift(ExprHandle expr, ExprHandle shift) { + unsigned width = vc_getBVLength(vc, expr); ExprHandle res = bvZero(width); - int shiftBits = getShiftBits( width ); - - //get the shift amount (looking only at the bits appropriate for the given width) - ExprHandle shift = vc_bvExtract( vc, amount, shiftBits - 1, 0 ); - //construct a big if-then-elif-elif-... with one case per possible shift amount for( int i=width-1; i>=0; i-- ) { res = vc_iteExpr(vc, - eqExpr(shift, bvConst32(shiftBits, i)), - bvRightShift(expr, i, shiftBits), + eqExpr(shift, bvConst32(width, i)), + bvRightShift(expr, i), res); } + // If overshifting, shift to zero + res = vc_iteExpr(vc, + vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)), + res, + bvZero(width)); return res; } // arithmetic right shift by a variable amount on an expression of the specified width -ExprHandle STPBuilder::bvVarArithRightShift(ExprHandle expr, ExprHandle amount, unsigned width) { - int shiftBits = getShiftBits( width ); - - //get the shift amount (looking only at the bits appropriate for the given width) - ExprHandle shift = vc_bvExtract( vc, amount, shiftBits - 1, 0 ); +ExprHandle STPBuilder::bvVarArithRightShift(ExprHandle expr, ExprHandle shift) { + unsigned width = vc_getBVLength(vc, expr); //get the sign bit to fill with ExprHandle signedBool = bvBoolExtract(expr, width-1); //start with the result if shifting by width-1 - ExprHandle res = constructAShrByConstant(expr, width-1, signedBool, shiftBits); + ExprHandle res = constructAShrByConstant(expr, width-1, signedBool); //construct a big if-then-elif-elif-... with one case per possible shift amount // XXX more efficient to move the ite on the sign outside all exprs? // XXX more efficient to sign extend, right shift, then extract lower bits? for( int i=width-2; i>=0; i-- ) { res = vc_iteExpr(vc, - eqExpr(shift, bvConst32(shiftBits,i)), + eqExpr(shift, bvConst32(width,i)), constructAShrByConstant(expr, i, - signedBool, - shiftBits), + signedBool), res); } + // If overshifting, shift to zero + res = vc_iteExpr(vc, + vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)), + res, + bvZero(width)); return res; } ExprHandle STPBuilder::constructAShrByConstant(ExprHandle expr, - unsigned amount, - ExprHandle isSigned, - unsigned shiftBits) { + unsigned shift, + ExprHandle isSigned) { unsigned width = vc_getBVLength(vc, expr); - unsigned shift = amount & ((1<<shiftBits) - 1); if (shift==0) { return expr; } else if (shift>=width-1) { - return vc_iteExpr(vc, isSigned, bvMinusOne(width), bvZero(width)); + return bvZero(width); // Overshift to zero } else { return vc_iteExpr(vc, isSigned, ExprHandle(vc_bvConcatExpr(vc, bvMinusOne(shift), bvExtract(expr, width - 1, shift))), - bvRightShift(expr, shift, shiftBits)); + bvRightShift(expr, shift)); } } ExprHandle STPBuilder::constructMulByConstant(ExprHandle expr, unsigned width, uint64_t x) { - unsigned shiftBits = getShiftBits(width); uint64_t add, sub; ExprHandle res = 0; @@ -313,7 +311,7 @@ ExprHandle STPBuilder::constructMulByConstant(ExprHandle expr, unsigned width, u if ((add&bit) || (sub&bit)) { assert(!((add&bit) && (sub&bit)) && "invalid mult constants"); - ExprHandle op = bvLeftShift(expr, j, shiftBits); + ExprHandle op = bvLeftShift(expr, j); if (add&bit) { if (res) { @@ -367,9 +365,9 @@ ExprHandle STPBuilder::constructUDivByConstant(ExprHandle expr_n, unsigned width // n/d = (((n - t1) >> sh1) + t1) >> sh2; ExprHandle n_minus_t1 = vc_bvMinusExpr( vc, width, expr_n, t1 ); - ExprHandle shift_sh1 = bvVarRightShift( n_minus_t1, expr_sh1, 32 ); + ExprHandle shift_sh1 = bvVarRightShift( n_minus_t1, expr_sh1); ExprHandle plus_t1 = vc_bvPlusExpr( vc, width, shift_sh1, t1 ); - ExprHandle res = bvVarRightShift( plus_t1, expr_sh2, 32 ); + ExprHandle res = bvVarRightShift( plus_t1, expr_sh2); return res; } @@ -407,7 +405,7 @@ ExprHandle STPBuilder::constructSDivByConstant(ExprHandle expr_n, unsigned width // Improved variable arithmetic right shift: sign extend, shift, // extract. ExprHandle extend_npm = vc_bvSignExtend( vc, n_plus_mulsh, 64 ); - ExprHandle shift_npm = bvVarRightShift( extend_npm, expr_shpost, 64 ); + ExprHandle shift_npm = bvVarRightShift( extend_npm, expr_shpost); ExprHandle shift_shpost = vc_bvExtract( vc, shift_npm, 31, 0 ); //lower 32-bits // XSIGN(n) is -1 if n is negative, positive one otherwise @@ -440,7 +438,7 @@ ExprHandle STPBuilder::constructSDivByConstant(ExprHandle expr_n, unsigned width memmove(buf + space, buf, addrlen); // moving the address part to the end memcpy(buf, root->name.c_str(), space); // filling out the name part - array_expr = buildArray(buf, 32, 8); + array_expr = buildArray(buf, root->getDomain(), root->getRange()); if (root->isConstantArray()) { // FIXME: Flush the concrete values into STP. Ideally we would do this @@ -554,7 +552,8 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) { case Expr::Read: { ReadExpr *re = cast<ReadExpr>(e); - *width_out = 8; + assert(re && re->updates.root); + *width_out = re->updates.root->getRange(); return vc_readExpr(vc, getArrayForUpdate(re->updates.root, re->updates.head), construct(re->index, 0)); @@ -659,8 +658,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) { if (bits64::isPowerOfTwo(divisor)) { return bvRightShift(left, - bits64::indexOfSingleBit(divisor), - getShiftBits(*width_out)); + bits64::indexOfSingleBit(divisor)); } else if (optimizeDivides) { if (*width_out == 32) //only works for 32-bit division return constructUDivByConstant( left, *width_out, @@ -810,28 +808,25 @@ 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, (unsigned) CE->getLimitedValue(), - getShiftBits(*width_out)); + return bvLeftShift(left, (unsigned) CE->getLimitedValue()); } else { int shiftWidth; ExprHandle amount = construct(se->right, &shiftWidth); - return bvVarLeftShift( left, amount, *width_out ); + return bvVarLeftShift( left, amount); } } case Expr::LShr: { LShrExpr *lse = cast<LShrExpr>(e); ExprHandle left = construct(lse->left, width_out); - unsigned shiftBits = getShiftBits(*width_out); assert(*width_out!=1 && "uncanonicalized lshr"); if (ConstantExpr *CE = dyn_cast<ConstantExpr>(lse->right)) { - return bvRightShift(left, (unsigned) CE->getLimitedValue(), - shiftBits); + return bvRightShift(left, (unsigned) CE->getLimitedValue()); } else { int shiftWidth; ExprHandle amount = construct(lse->right, &shiftWidth); - return bvVarRightShift( left, amount, *width_out ); + return bvVarRightShift( left, amount); } } @@ -843,12 +838,11 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) { if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ase->right)) { unsigned shift = (unsigned) CE->getLimitedValue(); ExprHandle signedBool = bvBoolExtract(left, *width_out-1); - return constructAShrByConstant(left, shift, signedBool, - getShiftBits(*width_out)); + return constructAShrByConstant(left, shift, signedBool); } else { int shiftWidth; ExprHandle amount = construct(ase->right, &shiftWidth); - return bvVarArithRightShift( left, amount, *width_out ); + return bvVarArithRightShift( left, amount); } } diff --git a/lib/Solver/STPBuilder.h b/lib/Solver/STPBuilder.h index 0a99b753..ef1cd8b3 100644 --- a/lib/Solver/STPBuilder.h +++ b/lib/Solver/STPBuilder.h @@ -79,13 +79,6 @@ class STPBuilder { STPArrayExprHash _arr_hash; private: - unsigned getShiftBits(unsigned amount) { - unsigned bits = 1; - amount--; - while (amount >>= 1) - bits++; - return bits; - } ExprHandle bvOne(unsigned width); ExprHandle bvZero(unsigned width); @@ -100,14 +93,14 @@ private: ExprHandle eqExpr(ExprHandle a, ExprHandle b); //logical left and right shift (not arithmetic) - ExprHandle bvLeftShift(ExprHandle expr, unsigned shift, unsigned shiftBits); - ExprHandle bvRightShift(ExprHandle expr, unsigned amount, unsigned shiftBits); - ExprHandle bvVarLeftShift(ExprHandle expr, ExprHandle amount, unsigned width); - ExprHandle bvVarRightShift(ExprHandle expr, ExprHandle amount, unsigned width); - ExprHandle bvVarArithRightShift(ExprHandle expr, ExprHandle amount, unsigned width); + ExprHandle bvLeftShift(ExprHandle expr, unsigned shift); + ExprHandle bvRightShift(ExprHandle expr, unsigned shift); + ExprHandle bvVarLeftShift(ExprHandle expr, ExprHandle shift); + ExprHandle bvVarRightShift(ExprHandle expr, ExprHandle shift); + ExprHandle bvVarArithRightShift(ExprHandle expr, ExprHandle shift); ExprHandle constructAShrByConstant(ExprHandle expr, unsigned shift, - ExprHandle isSigned, unsigned shiftBits); + ExprHandle isSigned); ExprHandle constructMulByConstant(ExprHandle expr, unsigned width, uint64_t x); ExprHandle constructUDivByConstant(ExprHandle expr_n, unsigned width, uint64_t d); ExprHandle constructSDivByConstant(ExprHandle expr_n, unsigned width, uint64_t d); diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index 22b1545f..229fa234 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -407,11 +407,12 @@ ValidatingSolver::computeInitialValues(const Query& query, std::vector< ref<Expr> > bindings; for (unsigned i = 0; i != values.size(); ++i) { const Array *array = objects[i]; + assert(array); for (unsigned j=0; j<array->size; j++) { unsigned char value = values[i][j]; bindings.push_back(EqExpr::create(ReadExpr::create(UpdateList(array, 0), - ConstantExpr::alloc(j, Expr::Int32)), - ConstantExpr::alloc(value, Expr::Int8))); + ConstantExpr::alloc(j, array->getDomain())), + ConstantExpr::alloc(value, array->getRange()))); } } ConstraintManager tmp(bindings); @@ -493,8 +494,6 @@ Solver *klee::createDummySolver() { class STPSolverImpl : public SolverImpl { private: - /// The solver we are part of, for access to public information. - STPSolver *solver; VC vc; STPBuilder *builder; double timeout; @@ -502,7 +501,7 @@ private: SolverRunStatus runStatusCode; public: - STPSolverImpl(STPSolver *_solver, bool _useForkedSTP, bool _optimizeDivides = true); + STPSolverImpl(bool _useForkedSTP, bool _optimizeDivides = true); ~STPSolverImpl(); char *getConstraintLog(const Query&); @@ -526,9 +525,8 @@ static void stp_error_handler(const char* err_msg) { abort(); } -STPSolverImpl::STPSolverImpl(STPSolver *_solver, bool _useForkedSTP, bool _optimizeDivides) - : solver(_solver), - vc(vc_createValidityChecker()), +STPSolverImpl::STPSolverImpl(bool _useForkedSTP, bool _optimizeDivides) + : vc(vc_createValidityChecker()), builder(new STPBuilder(vc, _optimizeDivides)), timeout(0.0), useForkedSTP(_useForkedSTP), @@ -565,7 +563,7 @@ STPSolverImpl::~STPSolverImpl() { /***/ STPSolver::STPSolver(bool useForkedSTP, bool optimizeDivides) - : Solver(new STPSolverImpl(this, useForkedSTP, optimizeDivides)) + : Solver(new STPSolverImpl(useForkedSTP, optimizeDivides)) { } @@ -773,7 +771,6 @@ static SolverImpl::SolverRunStatus runAndGetCexForked(::VC vc, } } } -#include <iostream> bool STPSolverImpl::computeInitialValues(const Query &query, const std::vector<const Array*> |