diff options
Diffstat (limited to 'lib/Solver')
-rw-r--r-- | lib/Solver/QueryLoggingSolver.cpp | 42 | ||||
-rw-r--r-- | lib/Solver/QueryLoggingSolver.h | 2 | ||||
-rw-r--r-- | lib/Solver/STPBuilder.cpp | 92 | ||||
-rw-r--r-- | lib/Solver/STPBuilder.h | 2 |
4 files changed, 91 insertions, 47 deletions
diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp index f93bec3c..fb957b65 100644 --- a/lib/Solver/QueryLoggingSolver.cpp +++ b/lib/Solver/QueryLoggingSolver.cpp @@ -7,8 +7,13 @@ // //===----------------------------------------------------------------------===// #include "QueryLoggingSolver.h" +#include "klee/Config/config.h" #include "klee/Internal/System/Time.h" #include "klee/Statistics.h" +#ifdef HAVE_ZLIB_H +#include "klee/Internal/Support/CompressionStream.h" +#include "klee/Internal/Support/ErrorHandling.h" +#endif #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) #include "llvm/Support/FileSystem.h" @@ -20,30 +25,49 @@ namespace { llvm::cl::opt<bool> DumpPartialQueryiesEarly( "log-partial-queries-early", llvm::cl::init(false), llvm::cl::desc("Log queries before calling the solver (default=off)")); + +#ifdef HAVE_ZLIB_H +llvm::cl::opt<bool> CreateCompressedQueryLog( + "compress-query-log", llvm::cl::init(false), + llvm::cl::desc("Compress query log files (default=off)")); +#endif } QueryLoggingSolver::QueryLoggingSolver(Solver *_solver, std::string path, const std::string &commentSign, int queryTimeToLog) - : solver(_solver), + : solver(_solver), os(0), BufferString(""), logBuffer(BufferString), + queryCount(0), minQueryTimeToLog(queryTimeToLog), startTime(0.0f), + lastQueryTime(0.0f), queryCommentSign(commentSign) { + if (!CreateCompressedQueryLog) { #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) - os(path.c_str(), ErrorInfo, llvm::sys::fs::OpenFlags::F_Text), + os = new llvm::raw_fd_ostream(path.c_str(), ErrorInfo, + llvm::sys::fs::OpenFlags::F_Text); #else - os(path.c_str(), ErrorInfo), + os = new llvm::raw_fd_ostream(path.c_str(), ErrorInfo); +#endif + } +#ifdef HAVE_ZLIB_H + else { + os = new compressed_fd_ostream((path + ".gz").c_str(), ErrorInfo); + } + if (ErrorInfo != "") { + klee_error("Could not open file %s : %s", path.c_str(), ErrorInfo.c_str()); + } #endif - BufferString(""), logBuffer(BufferString), queryCount(0), - minQueryTimeToLog(queryTimeToLog), startTime(0.0f), lastQueryTime(0.0f), - queryCommentSign(commentSign) { assert(0 != solver); } -QueryLoggingSolver::~QueryLoggingSolver() { delete solver; } +QueryLoggingSolver::~QueryLoggingSolver() { + delete solver; + delete os; +} void QueryLoggingSolver::flushBufferConditionally(bool writeToFile) { logBuffer.flush(); if (writeToFile) { - os << logBuffer.str(); - os.flush(); + *os << logBuffer.str(); + os->flush(); } // prepare the buffer for reuse BufferString = ""; diff --git a/lib/Solver/QueryLoggingSolver.h b/lib/Solver/QueryLoggingSolver.h index bb266c67..7ac783d1 100644 --- a/lib/Solver/QueryLoggingSolver.h +++ b/lib/Solver/QueryLoggingSolver.h @@ -26,7 +26,7 @@ class QueryLoggingSolver : public SolverImpl { protected: Solver *solver; std::string ErrorInfo; - llvm::raw_fd_ostream os; + llvm::raw_ostream *os; // @brief Buffer used by logBuffer std::string BufferString; // @brief buffer to store logs before flushing to file diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index 307ae0fb..8ec35762 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -152,6 +152,7 @@ ExprHandle STPBuilder::bvExtract(ExprHandle expr, unsigned top, unsigned bottom) return vc_bvExtract(vc, expr, top, bottom); } ExprHandle STPBuilder::eqExpr(ExprHandle a, ExprHandle b) { + assert((vc_getBVLength(vc, a) == vc_getBVLength(vc, b)) && "a and b should be same type"); return vc_eqExpr(vc, a, b); } @@ -187,76 +188,93 @@ ExprHandle STPBuilder::bvLeftShift(ExprHandle expr, unsigned shift) { } } +ExprHandle STPBuilder::extractPartialShiftValue(ExprHandle shift, + unsigned width, + unsigned &shiftBits) { + // Assuming width is power of 2 + llvm::APInt sw(32, width); + shiftBits = sw.getActiveBits(); + + // get the shift amount (looking only at the bits appropriate for the given + // width) + return vc_bvExtract(vc, shift, shiftBits - 1, 0); +} + // left shift by a variable amount on an expression of the specified width ExprHandle STPBuilder::bvVarLeftShift(ExprHandle expr, ExprHandle shift) { unsigned width = vc_getBVLength(vc, expr); ExprHandle res = bvZero(width); - //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(width, i)), - bvLeftShift(expr, i), - res); + unsigned shiftBits = 0; + ExprHandle shift_ext = extractPartialShiftValue(shift, width, shiftBits); + + // 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_ext, bvConst32(shiftBits, i)), + bvLeftShift(expr, i), res); } // If overshifting, shift to zero - ExprHandle ex = vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)); + ExprHandle ex = + vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc, shift), width)); res = vc_iteExpr(vc, ex, res, bvZero(width)); return res; } -// logical right shift by a variable amount on an expression of the specified width +// logical right shift by a variable amount on an expression of the specified +// width ExprHandle STPBuilder::bvVarRightShift(ExprHandle expr, ExprHandle shift) { unsigned width = vc_getBVLength(vc, expr); ExprHandle res = bvZero(width); - //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(width, i)), - bvRightShift(expr, i), - res); + unsigned shiftBits = 0; + ExprHandle shift_ext = extractPartialShiftValue(shift, width, shiftBits); + + // 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_ext, bvConst32(shiftBits, i)), + bvRightShift(expr, i), res); } // If overshifting, shift to zero - ExprHandle ex = vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)); - res = vc_iteExpr(vc, - ex, - res, - bvZero(width)); + // If overshifting, shift to zero + ExprHandle ex = + vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc, shift), width)); + res = vc_iteExpr(vc, ex, res, bvZero(width)); + return res; } -// arithmetic right shift by a variable amount on an expression of the specified width +// arithmetic right shift by a variable amount on an expression of the specified +// width 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); + unsigned shiftBits = 0; + ExprHandle shift_ext = extractPartialShiftValue(shift, width, shiftBits); - //start with the result if shifting by width-1 - ExprHandle res = constructAShrByConstant(expr, width-1, signedBool); + // get the sign bit to fill with + ExprHandle signedBool = bvBoolExtract(expr, width - 1); - //construct a big if-then-elif-elif-... with one case per possible shift amount + // start with the result if shifting by width-1 + 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(width,i)), - constructAShrByConstant(expr, - i, - signedBool), - res); + for (int i = width - 2; i >= 0; i--) { + res = vc_iteExpr(vc, eqExpr(shift_ext, bvConst32(shiftBits, i)), + constructAShrByConstant(expr, i, signedBool), res); } // If overshifting, shift to zero - ExprHandle ex = vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)); - res = vc_iteExpr(vc, - ex, - res, - bvZero(width)); + ExprHandle ex = + vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc, shift), width)); + res = vc_iteExpr(vc, ex, res, bvZero(width)); return res; } diff --git a/lib/Solver/STPBuilder.h b/lib/Solver/STPBuilder.h index 3b17ccf1..5be34029 100644 --- a/lib/Solver/STPBuilder.h +++ b/lib/Solver/STPBuilder.h @@ -93,6 +93,8 @@ private: ExprHandle bvVarLeftShift(ExprHandle expr, ExprHandle shift); ExprHandle bvVarRightShift(ExprHandle expr, ExprHandle shift); ExprHandle bvVarArithRightShift(ExprHandle expr, ExprHandle shift); + ExprHandle extractPartialShiftValue(ExprHandle shift, unsigned width, + unsigned &shiftBits); ExprHandle constructAShrByConstant(ExprHandle expr, unsigned shift, ExprHandle isSigned); |