diff options
Diffstat (limited to 'lib/Solver')
| -rw-r--r-- | lib/Solver/AssignmentValidatingSolver.cpp | 158 | ||||
| -rw-r--r-- | lib/Solver/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | lib/Solver/CoreSolver.cpp | 66 | ||||
| -rw-r--r-- | lib/Solver/MetaSMTSolver.cpp | 34 | ||||
| -rw-r--r-- | lib/Solver/MetaSMTSolver.h | 32 | ||||
| -rw-r--r-- | lib/Solver/QueryLoggingSolver.cpp | 8 | ||||
| -rw-r--r-- | lib/Solver/STPSolver.cpp | 1 | ||||
| -rw-r--r-- | lib/Solver/STPSolver.h | 39 | ||||
| -rw-r--r-- | lib/Solver/Z3Builder.cpp | 46 | ||||
| -rw-r--r-- | lib/Solver/Z3Builder.h | 14 | ||||
| -rw-r--r-- | lib/Solver/Z3Solver.cpp | 160 | ||||
| -rw-r--r-- | lib/Solver/Z3Solver.h | 34 |
12 files changed, 512 insertions, 81 deletions
diff --git a/lib/Solver/AssignmentValidatingSolver.cpp b/lib/Solver/AssignmentValidatingSolver.cpp new file mode 100644 index 00000000..a4d97f54 --- /dev/null +++ b/lib/Solver/AssignmentValidatingSolver.cpp @@ -0,0 +1,158 @@ +//===-- AssignmentValidatingSolver.cpp ------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// +#include "klee/util/Assignment.h" +#include "klee/Constraints.h" +#include "klee/Solver.h" +#include "klee/SolverImpl.h" +#include <vector> + +namespace klee { + +class AssignmentValidatingSolver : public SolverImpl { +private: + Solver *solver; + void dumpAssignmentQuery(const Query &query, const Assignment &assignment); + +public: + AssignmentValidatingSolver(Solver *_solver) : solver(_solver) {} + ~AssignmentValidatingSolver() { delete solver; } + + bool computeValidity(const Query &, Solver::Validity &result); + bool computeTruth(const Query &, bool &isValid); + bool computeValue(const Query &, ref<Expr> &result); + bool computeInitialValues(const Query &, + const std::vector<const Array *> &objects, + std::vector<std::vector<unsigned char> > &values, + bool &hasSolution); + SolverRunStatus getOperationStatusCode(); + char *getConstraintLog(const Query &); + void setCoreSolverTimeout(double timeout); +}; + +// TODO: use computeInitialValues for all queries for more stress testing +bool AssignmentValidatingSolver::computeValidity(const Query &query, + Solver::Validity &result) { + return solver->impl->computeValidity(query, result); +} +bool AssignmentValidatingSolver::computeTruth(const Query &query, + bool &isValid) { + return solver->impl->computeTruth(query, isValid); +} +bool AssignmentValidatingSolver::computeValue(const Query &query, + ref<Expr> &result) { + return solver->impl->computeValue(query, result); +} + +bool AssignmentValidatingSolver::computeInitialValues( + const Query &query, const std::vector<const Array *> &objects, + std::vector<std::vector<unsigned char> > &values, bool &hasSolution) { + bool success = + solver->impl->computeInitialValues(query, objects, values, hasSolution); + if (!hasSolution) + return success; + + // Use `_allowFreeValues` so that if we are missing an assignment + // we can't compute a constant and flag this as a problem. + Assignment assignment(objects, values, /*_allowFreeValues=*/true); + // Check computed assignment satisfies query + for (ConstraintManager::const_iterator it = query.constraints.begin(), + ie = query.constraints.end(); + it != ie; ++it) { + ref<Expr> constraint = *it; + ref<Expr> constraintEvaluated = assignment.evaluate(constraint); + ConstantExpr *CE = dyn_cast<ConstantExpr>(constraintEvaluated); + if (CE == NULL) { + llvm::errs() << "Constraint did not evalaute to a constant:\n"; + llvm::errs() << "Constraint:\n" << constraint << "\n"; + llvm::errs() << "Evaluated Constraint:\n" << constraintEvaluated << "\n"; + llvm::errs() << "Assignment:\n"; + assignment.dump(); + dumpAssignmentQuery(query, assignment); + abort(); + } + if (CE->isFalse()) { + llvm::errs() << "Constraint evaluated to false when using assignment\n"; + llvm::errs() << "Constraint:\n" << constraint << "\n"; + llvm::errs() << "Assignment:\n"; + assignment.dump(); + dumpAssignmentQuery(query, assignment); + abort(); + } + } + + ref<Expr> queryExprEvaluated = assignment.evaluate(query.expr); + ConstantExpr *CE = dyn_cast<ConstantExpr>(queryExprEvaluated); + if (CE == NULL) { + llvm::errs() << "Query expression did not evalaute to a constant:\n"; + llvm::errs() << "Expression:\n" << query.expr << "\n"; + llvm::errs() << "Evaluated expression:\n" << queryExprEvaluated << "\n"; + llvm::errs() << "Assignment:\n"; + assignment.dump(); + dumpAssignmentQuery(query, assignment); + abort(); + } + // KLEE queries are validity queries. A counter example to + // ∀ x constraints(x) → query(x) + // exists therefore + // ¬∀ x constraints(x) → query(x) + // Which is equivalent to + // ∃ x constraints(x) ∧ ¬ query(x) + // This means for the assignment we get back query expression should evaluate + // to false. + if (CE->isTrue()) { + llvm::errs() + << "Query Expression evaluated to true when using assignment\n"; + llvm::errs() << "Expression:\n" << query.expr << "\n"; + llvm::errs() << "Assignment:\n"; + assignment.dump(); + dumpAssignmentQuery(query, assignment); + abort(); + } + + return success; +} + +void AssignmentValidatingSolver::dumpAssignmentQuery( + const Query &query, const Assignment &assignment) { + // Create a Query that is augmented with constraints that + // enforce the given assignment. + std::vector<ref<Expr> > constraints; + assignment.createConstraintsFromAssignment(constraints); + // Add Constraints from `query` + for (ConstraintManager::const_iterator it = query.constraints.begin(), + ie = query.constraints.end(); + it != ie; ++it) { + constraints.push_back(*it); + } + ConstraintManager augmentedConstraints(constraints); + Query augmentedQuery(augmentedConstraints, query.expr); + + // Ask the solver for the log for this query. + char *logText = solver->getConstraintLog(augmentedQuery); + llvm::errs() << "Query with assignment as constraints:\n" << logText << "\n"; + free(logText); +} + +SolverImpl::SolverRunStatus +AssignmentValidatingSolver::getOperationStatusCode() { + return solver->impl->getOperationStatusCode(); +} + +char *AssignmentValidatingSolver::getConstraintLog(const Query &query) { + return solver->impl->getConstraintLog(query); +} + +void AssignmentValidatingSolver::setCoreSolverTimeout(double timeout) { + return solver->impl->setCoreSolverTimeout(timeout); +} + +Solver *createAssignmentValidatingSolver(Solver *s) { + return new Solver(new AssignmentValidatingSolver(s)); +} +} diff --git a/lib/Solver/CMakeLists.txt b/lib/Solver/CMakeLists.txt index 1302db38..d9c393fb 100644 --- a/lib/Solver/CMakeLists.txt +++ b/lib/Solver/CMakeLists.txt @@ -7,6 +7,7 @@ # #===------------------------------------------------------------------------===# klee_add_component(kleaverSolver + AssignmentValidatingSolver.cpp CachingSolver.cpp CexCachingSolver.cpp ConstantDivision.cpp diff --git a/lib/Solver/CoreSolver.cpp b/lib/Solver/CoreSolver.cpp index 783047f8..438f38f6 100644 --- a/lib/Solver/CoreSolver.cpp +++ b/lib/Solver/CoreSolver.cpp @@ -7,90 +7,48 @@ // //===----------------------------------------------------------------------===// +#include "STPSolver.h" +#include "Z3Solver.h" +#include "MetaSMTSolver.h" #include "klee/CommandLine.h" +#include "klee/Internal/Support/ErrorHandling.h" #include "klee/Solver.h" #include "llvm/Support/ErrorHandling.h" #include "llvm/Support/raw_ostream.h" #include <string> -#ifdef ENABLE_METASMT - -#include <metaSMT/DirectSolver_Context.hpp> -#include <metaSMT/backend/Z3_Backend.hpp> -#include <metaSMT/backend/Boolector.hpp> - -#define Expr VCExpr -#define Type VCType -#define STP STP_Backend -#include <metaSMT/backend/STP.hpp> -#undef Expr -#undef Type -#undef STP - -using namespace klee; -using namespace metaSMT; -using namespace metaSMT::solver; - -static klee::Solver *handleMetaSMT() { - Solver *coreSolver = NULL; - std::string backend; - switch (MetaSMTBackend) { - case METASMT_BACKEND_STP: - backend = "STP"; - coreSolver = new MetaSMTSolver<DirectSolver_Context<STP_Backend> >( - UseForkedCoreSolver, CoreSolverOptimizeDivides); - break; - case METASMT_BACKEND_Z3: - backend = "Z3"; - coreSolver = new MetaSMTSolver<DirectSolver_Context<Z3_Backend> >( - UseForkedCoreSolver, CoreSolverOptimizeDivides); - break; - case METASMT_BACKEND_BOOLECTOR: - backend = "Boolector"; - coreSolver = new MetaSMTSolver<DirectSolver_Context<Boolector> >( - UseForkedCoreSolver, CoreSolverOptimizeDivides); - break; - default: - llvm_unreachable("Unrecognised metasmt backend"); - break; - }; - llvm::errs() << "Starting MetaSMTSolver(" << backend << ") ...\n"; - return coreSolver; -} -#endif /* ENABLE_METASMT */ - namespace klee { Solver *createCoreSolver(CoreSolverType cst) { switch (cst) { case STP_SOLVER: #ifdef ENABLE_STP - llvm::errs() << "Using STP solver backend\n"; + klee_message("Using STP solver backend"); return new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides); #else - llvm::errs() << "Not compiled with STP support\n"; + klee_message("Not compiled with STP support"); return NULL; #endif case METASMT_SOLVER: #ifdef ENABLE_METASMT - llvm::errs() << "Using MetaSMT solver backend\n"; - return handleMetaSMT(); + klee_message("Using MetaSMT solver backend"); + return createMetaSMTSolver(); #else - llvm::errs() << "Not compiled with MetaSMT support\n"; + klee_message("Not compiled with MetaSMT support"); return NULL; #endif case DUMMY_SOLVER: return createDummySolver(); case Z3_SOLVER: #ifdef ENABLE_Z3 - llvm::errs() << "Using Z3 solver backend\n"; + klee_message("Using Z3 solver backend"); return new Z3Solver(); #else - llvm::errs() << "Not compiled with Z3 support\n"; + klee_message("Not compiled with Z3 support"); return NULL; #endif case NO_SOLVER: - llvm::errs() << "Invalid solver\n"; + klee_message("Invalid solver"); return NULL; default: llvm_unreachable("Unsupported CoreSolverType"); diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp index a453de40..9b49f995 100644 --- a/lib/Solver/MetaSMTSolver.cpp +++ b/lib/Solver/MetaSMTSolver.cpp @@ -9,6 +9,7 @@ #include "klee/Config/config.h" #ifdef ENABLE_METASMT +#include "MetaSMTSolver.h" #include "MetaSMTBuilder.h" #include "klee/Constraints.h" #include "klee/Internal/Support/ErrorHandling.h" @@ -17,6 +18,8 @@ #include "klee/util/Assignment.h" #include "klee/util/ExprUtil.h" +#include "llvm/Support/ErrorHandling.h" + #include <metaSMT/DirectSolver_Context.hpp> #include <metaSMT/backend/Z3_Backend.hpp> #include <metaSMT/backend/Boolector.hpp> @@ -405,5 +408,36 @@ void MetaSMTSolver<SolverContext>::setCoreSolverTimeout(double timeout) { template class MetaSMTSolver<DirectSolver_Context<metaSMT::solver::Boolector> >; template class MetaSMTSolver<DirectSolver_Context<metaSMT::solver::Z3_Backend> >; template class MetaSMTSolver<DirectSolver_Context<metaSMT::solver::STP_Backend> >; + +Solver *createMetaSMTSolver() { + using metaSMT::DirectSolver_Context; + using namespace metaSMT::solver; + + Solver *coreSolver = NULL; + std::string backend; + switch (MetaSMTBackend) { + case METASMT_BACKEND_STP: + backend = "STP"; + coreSolver = new MetaSMTSolver<DirectSolver_Context<STP_Backend> >( + UseForkedCoreSolver, CoreSolverOptimizeDivides); + break; + case METASMT_BACKEND_Z3: + backend = "Z3"; + coreSolver = new MetaSMTSolver<DirectSolver_Context<Z3_Backend> >( + UseForkedCoreSolver, CoreSolverOptimizeDivides); + break; + case METASMT_BACKEND_BOOLECTOR: + backend = "Boolector"; + coreSolver = new MetaSMTSolver<DirectSolver_Context<Boolector> >( + UseForkedCoreSolver, CoreSolverOptimizeDivides); + break; + default: + llvm_unreachable("Unrecognised MetaSMT backend"); + break; + }; + klee_message("Starting MetaSMTSolver(%s)", backend.c_str()); + return coreSolver; +} + } #endif // ENABLE_METASMT diff --git a/lib/Solver/MetaSMTSolver.h b/lib/Solver/MetaSMTSolver.h new file mode 100644 index 00000000..60d72383 --- /dev/null +++ b/lib/Solver/MetaSMTSolver.h @@ -0,0 +1,32 @@ +//===-- MetaSMTSolver.h +//---------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_METASMTSOLVER_H +#define KLEE_METASMTSOLVER_H + +#include "klee/Solver.h" + +namespace klee { + +template <typename SolverContext> class MetaSMTSolver : public Solver { +public: + MetaSMTSolver(bool useForked, bool optimizeDivides); + virtual ~MetaSMTSolver(); + + virtual char *getConstraintLog(const Query &); + virtual void setCoreSolverTimeout(double timeout); +}; + +/// createMetaSMTSolver - Create a solver using the metaSMT backend set by +/// the option MetaSMTBackend. +Solver *createMetaSMTSolver(); +} + +#endif /* KLEE_METASMTSOLVER_H */ diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp index a858a7d7..cf4966cd 100644 --- a/lib/Solver/QueryLoggingSolver.cpp +++ b/lib/Solver/QueryLoggingSolver.cpp @@ -42,7 +42,13 @@ QueryLoggingSolver::QueryLoggingSolver(Solver *_solver, std::string path, #ifdef HAVE_ZLIB_H if (!CreateCompressedQueryLog) { #endif -#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 6) + std::error_code ec; + os = new llvm::raw_fd_ostream(path.c_str(), ec, + llvm::sys::fs::OpenFlags::F_Text); + if (ec) + ErrorInfo = ec.message(); +#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) os = new llvm::raw_fd_ostream(path.c_str(), ErrorInfo, llvm::sys::fs::OpenFlags::F_Text); #else diff --git a/lib/Solver/STPSolver.cpp b/lib/Solver/STPSolver.cpp index 5893c28e..d1b8cbdc 100644 --- a/lib/Solver/STPSolver.cpp +++ b/lib/Solver/STPSolver.cpp @@ -8,6 +8,7 @@ //===----------------------------------------------------------------------===// #include "klee/Config/config.h" #ifdef ENABLE_STP +#include "STPSolver.h" #include "STPBuilder.h" #include "klee/Solver.h" #include "klee/SolverImpl.h" diff --git a/lib/Solver/STPSolver.h b/lib/Solver/STPSolver.h new file mode 100644 index 00000000..cb68ed91 --- /dev/null +++ b/lib/Solver/STPSolver.h @@ -0,0 +1,39 @@ +//===-- STPSolver.h +//---------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_STPSOLVER_H +#define KLEE_STPSOLVER_H + +#include "klee/Solver.h" + +namespace klee { +/// STPSolver - A complete solver based on STP. +class STPSolver : public Solver { +public: + /// STPSolver - Construct a new STPSolver. + /// + /// \param useForkedSTP - Whether STP should be run in a separate process + /// (required for using timeouts). + /// \param optimizeDivides - Whether constant division operations should + /// be optimized into add/shift/multiply operations. + STPSolver(bool useForkedSTP, bool optimizeDivides = true); + + /// getConstraintLog - Return the constraint log for the given state in CVC + /// format. + virtual char *getConstraintLog(const Query &); + + /// setCoreSolverTimeout - Set constraint solver timeout delay to the given + /// value; 0 + /// is off. + virtual void setCoreSolverTimeout(double timeout); +}; +} + +#endif /* KLEE_STPSOLVER_H */ diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp index fc826c07..6c0653e8 100644 --- a/lib/Solver/Z3Builder.cpp +++ b/lib/Solver/Z3Builder.cpp @@ -11,10 +11,10 @@ #include "Z3Builder.h" #include "klee/Expr.h" +#include "klee/Internal/Support/ErrorHandling.h" #include "klee/Solver.h" -#include "klee/util/Bits.h" -#include "ConstantDivision.h" #include "klee/SolverStats.h" +#include "klee/util/Bits.h" #include "llvm/ADT/StringExtras.h" #include "llvm/Support/CommandLine.h" @@ -26,6 +26,21 @@ llvm::cl::opt<bool> UseConstructHashZ3( "use-construct-hash-z3", llvm::cl::desc("Use hash-consing during Z3 query construction."), llvm::cl::init(true)); + +// FIXME: This should be std::atomic<bool>. Need C++11 for that. +bool Z3InterationLogOpen = false; +} + +namespace klee { + +// Declared here rather than `Z3Builder.h` so they can be called in gdb. +template <> void Z3NodeHandle<Z3_sort>::dump() { + llvm::errs() << "Z3SortHandle:\n" << ::Z3_sort_to_string(context, node) + << "\n"; +} +template <> void Z3NodeHandle<Z3_ast>::dump() { + llvm::errs() << "Z3ASTHandle:\n" << ::Z3_ast_to_string(context, as_ast()) + << "\n"; } void custom_z3_error_handler(Z3_context ctx, Z3_error_code ec) { @@ -45,6 +60,9 @@ void custom_z3_error_handler(Z3_context ctx, Z3_error_code ec) { } llvm::errs() << "Error: Incorrect use of Z3. [" << ec << "] " << errorMsg << "\n"; + // NOTE: The current implementation of `Z3_close_log()` can be safely + // called even if the log isn't open. + Z3_close_log(); abort(); } @@ -55,8 +73,17 @@ void Z3ArrayExprHash::clear() { _array_hash.clear(); } -Z3Builder::Z3Builder(bool autoClearConstructCache) - : autoClearConstructCache(autoClearConstructCache) { +Z3Builder::Z3Builder(bool autoClearConstructCache, const char* z3LogInteractionFileArg) + : autoClearConstructCache(autoClearConstructCache), z3LogInteractionFile("") { + if (z3LogInteractionFileArg) + this->z3LogInteractionFile = std::string(z3LogInteractionFileArg); + if (z3LogInteractionFile.length() > 0) { + klee_message("Logging Z3 API interaction to \"%s\"", + z3LogInteractionFile.c_str()); + assert(!Z3InterationLogOpen && "interaction log should not already be open"); + Z3_open_log(z3LogInteractionFile.c_str()); + Z3InterationLogOpen = true; + } // FIXME: Should probably let the client pass in a Z3_config instead Z3_config cfg = Z3_mk_config(); // It is very important that we ask Z3 to let us manage memory so that @@ -75,6 +102,10 @@ Z3Builder::~Z3Builder() { clearConstructCache(); _arr_hash.clear(); Z3_del_context(ctx); + if (z3LogInteractionFile.length() > 0) { + Z3_close_log(); + Z3InterationLogOpen = false; + } } Z3SortHandle Z3Builder::getBvSort(unsigned width) { @@ -529,6 +560,7 @@ Z3ASTHandle Z3Builder::constructActual(ref<Expr> e, int *width_out) { if (srcWidth == 1) { return iteExpr(src, bvOne(*width_out), bvZero(*width_out)); } else { + assert(*width_out > srcWidth && "Invalid width_out"); return Z3ASTHandle(Z3_mk_concat(ctx, bvZero(*width_out - srcWidth), src), ctx); } @@ -621,12 +653,15 @@ Z3ASTHandle Z3Builder::constructActual(ref<Expr> e, int *width_out) { uint64_t divisor = CE->getZExtValue(); if (bits64::isPowerOfTwo(divisor)) { - unsigned bits = bits64::indexOfSingleBit(divisor); + // FIXME: This should be unsigned but currently needs to be signed to + // avoid signed-unsigned comparison in assert. + int bits = bits64::indexOfSingleBit(divisor); // special case for modding by 1 or else we bvExtract -1:0 if (bits == 0) { return bvZero(*width_out); } else { + assert(*width_out > bits && "invalid width_out"); return Z3ASTHandle(Z3_mk_concat(ctx, bvZero(*width_out - bits), bvExtract(left, bits - 1, 0)), ctx); @@ -816,4 +851,5 @@ Z3ASTHandle Z3Builder::constructActual(ref<Expr> e, int *width_out) { return getTrue(); } } +} #endif // ENABLE_Z3 diff --git a/lib/Solver/Z3Builder.h b/lib/Solver/Z3Builder.h index f3b2732b..a3473f82 100644 --- a/lib/Solver/Z3Builder.h +++ b/lib/Solver/Z3Builder.h @@ -81,19 +81,13 @@ template <> inline ::Z3_ast Z3NodeHandle<Z3_sort>::as_ast() { // instead to simplify our implementation but this seems cleaner. return ::Z3_sort_to_ast(context, node); } -template <> inline void Z3NodeHandle<Z3_sort>::dump() { - llvm::errs() << "Z3SortHandle:\n" << ::Z3_sort_to_string(context, node) - << "\n"; -} typedef Z3NodeHandle<Z3_sort> Z3SortHandle; +template <> void Z3NodeHandle<Z3_sort>::dump() __attribute__((used)); // Specialise for Z3_ast template <> inline ::Z3_ast Z3NodeHandle<Z3_ast>::as_ast() { return node; } -template <> inline void Z3NodeHandle<Z3_ast>::dump() { - llvm::errs() << "Z3ASTHandle:\n" << ::Z3_ast_to_string(context, as_ast()) - << "\n"; -} typedef Z3NodeHandle<Z3_ast> Z3ASTHandle; +template <> void Z3NodeHandle<Z3_ast>::dump() __attribute__((used)); class Z3ArrayExprHash : public ArrayExprHash<Z3ASTHandle> { @@ -171,11 +165,11 @@ private: Z3SortHandle getBvSort(unsigned width); Z3SortHandle getArraySort(Z3SortHandle domainSort, Z3SortHandle rangeSort); bool autoClearConstructCache; + std::string z3LogInteractionFile; public: Z3_context ctx; - - Z3Builder(bool autoClearConstructCache = true); + Z3Builder(bool autoClearConstructCache, const char *z3LogInteractionFile); ~Z3Builder(); Z3ASTHandle getTrue(); diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp index 1cbca566..985c143d 100644 --- a/lib/Solver/Z3Solver.cpp +++ b/lib/Solver/Z3Solver.cpp @@ -8,13 +8,37 @@ //===----------------------------------------------------------------------===// #include "klee/Config/config.h" #include "klee/Internal/Support/ErrorHandling.h" +#include "klee/Internal/Support/FileHandling.h" #ifdef ENABLE_Z3 +#include "Z3Solver.h" #include "Z3Builder.h" #include "klee/Constraints.h" #include "klee/Solver.h" #include "klee/SolverImpl.h" #include "klee/util/Assignment.h" #include "klee/util/ExprUtil.h" +#include "llvm/Support/CommandLine.h" +#include "llvm/Support/raw_ostream.h" + +namespace { +// NOTE: Very useful for debugging Z3 behaviour. These files can be given to +// the z3 binary to replay all Z3 API calls using its `-log` option. +llvm::cl::opt<std::string> Z3LogInteractionFile( + "debug-z3-log-api-interaction", llvm::cl::init(""), + llvm::cl::desc("Log API interaction with Z3 to the specified path")); + +llvm::cl::opt<std::string> Z3QueryDumpFile( + "debug-z3-dump-queries", llvm::cl::init(""), + llvm::cl::desc("Dump Z3's representation of the query to the specified path")); + +llvm::cl::opt<bool> Z3ValidateModels( + "debug-z3-validate-models", llvm::cl::init(false), + llvm::cl::desc("When generating Z3 models validate these against the query")); + +llvm::cl::opt<unsigned> + Z3VerbosityLevel("debug-z3-verbosity", llvm::cl::init(0), + llvm::cl::desc("Z3 verbosity level (default=0)")); +} #include "llvm/Support/ErrorHandling.h" @@ -25,6 +49,7 @@ private: Z3Builder *builder; double timeout; SolverRunStatus runStatusCode; + llvm::raw_fd_ostream* dumpedQueriesFile; ::Z3_params solverParameters; // Parameter symbols ::Z3_symbol timeoutParamStrSymbol; @@ -33,6 +58,7 @@ private: const std::vector<const Array *> *objects, std::vector<std::vector<unsigned char> > *values, bool &hasSolution); +bool validateZ3Model(::Z3_solver &theSolver, ::Z3_model &theModel); public: Z3SolverImpl(); @@ -65,18 +91,47 @@ public: }; Z3SolverImpl::Z3SolverImpl() - : builder(new Z3Builder(/*autoClearConstructCache=*/false)), timeout(0.0), - runStatusCode(SOLVER_RUN_STATUS_FAILURE) { + : builder(new Z3Builder( + /*autoClearConstructCache=*/false, + /*z3LogInteractionFileArg=*/Z3LogInteractionFile.size() > 0 + ? Z3LogInteractionFile.c_str() + : NULL)), + timeout(0.0), runStatusCode(SOLVER_RUN_STATUS_FAILURE), + dumpedQueriesFile(0) { assert(builder && "unable to create Z3Builder"); solverParameters = Z3_mk_params(builder->ctx); Z3_params_inc_ref(builder->ctx, solverParameters); timeoutParamStrSymbol = Z3_mk_string_symbol(builder->ctx, "timeout"); setCoreSolverTimeout(timeout); + + if (!Z3QueryDumpFile.empty()) { + std::string error; + dumpedQueriesFile = klee_open_output_file(Z3QueryDumpFile, error); + if (!error.empty()) { + klee_error("Error creating file for dumping Z3 queries: %s", + error.c_str()); + } + klee_message("Dumping Z3 queries to \"%s\"", Z3QueryDumpFile.c_str()); + } + + // Set verbosity + if (Z3VerbosityLevel > 0) { + std::string underlyingString; + llvm::raw_string_ostream ss(underlyingString); + ss << Z3VerbosityLevel; + ss.flush(); + Z3_global_param_set("verbose", underlyingString.c_str()); + } } Z3SolverImpl::~Z3SolverImpl() { Z3_params_dec_ref(builder->ctx, solverParameters); delete builder; + + if (dumpedQueriesFile) { + dumpedQueriesFile->close(); + delete dumpedQueriesFile; + } } Z3Solver::Z3Solver() : Solver(new Z3SolverImpl()) {} @@ -91,10 +146,18 @@ void Z3Solver::setCoreSolverTimeout(double timeout) { char *Z3SolverImpl::getConstraintLog(const Query &query) { std::vector<Z3ASTHandle> assumptions; + // We use a different builder here because we don't want to interfere + // with the solver's builder because it may change the solver builder's + // cache. + // NOTE: The builder does not set `z3LogInteractionFile` to avoid conflicting + // with whatever the solver's builder is set to do. + Z3Builder temp_builder(/*autoClearConstructCache=*/false, + /*z3LogInteractionFile=*/NULL); + for (std::vector<ref<Expr> >::const_iterator it = query.constraints.begin(), ie = query.constraints.end(); it != ie; ++it) { - assumptions.push_back(builder->construct(*it)); + assumptions.push_back(temp_builder.construct(*it)); } ::Z3_ast *assumptionsArray = NULL; int numAssumptions = query.constraints.size(); @@ -111,10 +174,11 @@ char *Z3SolverImpl::getConstraintLog(const Query &query) { // the negation of the equivalent i.e. // ∃ X Constraints(X) ∧ ¬ query(X) Z3ASTHandle formula = Z3ASTHandle( - Z3_mk_not(builder->ctx, builder->construct(query.expr)), builder->ctx); + Z3_mk_not(temp_builder.ctx, temp_builder.construct(query.expr)), + temp_builder.ctx); ::Z3_string result = Z3_benchmark_to_smtlib_string( - builder->ctx, + temp_builder.ctx, /*name=*/"Emited by klee::Z3SolverImpl::getConstraintLog()", /*logic=*/"", /*status=*/"unknown", @@ -125,6 +189,12 @@ char *Z3SolverImpl::getConstraintLog(const Query &query) { if (numAssumptions) free(assumptionsArray); + + // We need to trigger a dereference before the `temp_builder` gets destroyed. + // We do this indirectly by emptying `assumptions` and assigning to + // `formula`. + assumptions.clear(); + formula = Z3ASTHandle(NULL, temp_builder.ctx); // Client is responsible for freeing the returned C-string return strdup(result); } @@ -165,12 +235,15 @@ bool Z3SolverImpl::computeInitialValues( bool Z3SolverImpl::internalRunSolver( const Query &query, const std::vector<const Array *> *objects, std::vector<std::vector<unsigned char> > *values, bool &hasSolution) { + TimerStatIncrementer t(stats::queryTime); - // TODO: Does making a new solver for each query have a performance - // impact vs making one global solver and using push and pop? - // TODO: is the "simple_solver" the right solver to use for - // best performance? - Z3_solver theSolver = Z3_mk_simple_solver(builder->ctx); + // NOTE: Z3 will switch to using a slower solver internally if push/pop are + // used so for now it is likely that creating a new solver each time is the + // right way to go until Z3 changes its behaviour. + // + // TODO: Investigate using a custom tactic as described in + // https://github.com/klee/klee/issues/653 + Z3_solver theSolver = Z3_mk_solver(builder->ctx); Z3_solver_inc_ref(builder->ctx, theSolver); Z3_solver_set_params(builder->ctx, theSolver, solverParameters); @@ -197,6 +270,15 @@ bool Z3SolverImpl::internalRunSolver( builder->ctx, theSolver, Z3ASTHandle(Z3_mk_not(builder->ctx, z3QueryExpr), builder->ctx)); + if (dumpedQueriesFile) { + *dumpedQueriesFile << "; start Z3 query\n"; + *dumpedQueriesFile << Z3_solver_to_string(builder->ctx, theSolver); + *dumpedQueriesFile << "(check-sat)\n"; + *dumpedQueriesFile << "(reset)\n"; + *dumpedQueriesFile << "; end Z3 query\n\n"; + dumpedQueriesFile->flush(); + } + ::Z3_lbool satisfiable = Z3_solver_check(builder->ctx, theSolver); runStatusCode = handleSolverResponse(theSolver, satisfiable, objects, values, hasSolution); @@ -271,6 +353,13 @@ SolverImpl::SolverRunStatus Z3SolverImpl::handleSolverResponse( values->push_back(data); } + // Validate the model if requested + if (Z3ValidateModels) { + bool success = validateZ3Model(theSolver, theModel); + if (!success) + abort(); + } + Z3_model_dec_ref(builder->ctx, theModel); return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE; } @@ -280,7 +369,8 @@ SolverImpl::SolverRunStatus Z3SolverImpl::handleSolverResponse( case Z3_L_UNDEF: { ::Z3_string reason = ::Z3_solver_get_reason_unknown(builder->ctx, theSolver); - if (strcmp(reason, "timeout") == 0 || strcmp(reason, "canceled") == 0) { + if (strcmp(reason, "timeout") == 0 || strcmp(reason, "canceled") == 0 || + strcmp(reason, "(resource limits reached)") == 0) { return SolverImpl::SOLVER_RUN_STATUS_TIMEOUT; } if (strcmp(reason, "unknown") == 0) { @@ -294,6 +384,54 @@ SolverImpl::SolverRunStatus Z3SolverImpl::handleSolverResponse( } } +bool Z3SolverImpl::validateZ3Model(::Z3_solver &theSolver, ::Z3_model &theModel) { + bool success = true; + ::Z3_ast_vector constraints = + Z3_solver_get_assertions(builder->ctx, theSolver); + Z3_ast_vector_inc_ref(builder->ctx, constraints); + + unsigned size = Z3_ast_vector_size(builder->ctx, constraints); + + for (unsigned index = 0; index < size; ++index) { + Z3ASTHandle constraint = Z3ASTHandle( + Z3_ast_vector_get(builder->ctx, constraints, index), builder->ctx); + + ::Z3_ast rawEvaluatedExpr; + bool successfulEval = + Z3_model_eval(builder->ctx, theModel, constraint, + /*model_completion=*/Z3_TRUE, &rawEvaluatedExpr); + assert(successfulEval && "Failed to evaluate model"); + + // Use handle to do ref-counting. + Z3ASTHandle evaluatedExpr(rawEvaluatedExpr, builder->ctx); + + Z3SortHandle sort = + Z3SortHandle(Z3_get_sort(builder->ctx, evaluatedExpr), builder->ctx); + assert(Z3_get_sort_kind(builder->ctx, sort) == Z3_BOOL_SORT && + "Evaluated expression has wrong sort"); + + Z3_lbool evaluatedValue = + Z3_get_bool_value(builder->ctx, evaluatedExpr); + if (evaluatedValue != Z3_L_TRUE) { + llvm::errs() << "Validating model failed:\n" + << "The expression:\n"; + constraint.dump(); + llvm::errs() << "evaluated to \n"; + evaluatedExpr.dump(); + llvm::errs() << "But should be true\n"; + success = false; + } + } + + if (!success) { + llvm::errs() << "Solver state:\n" << Z3_solver_to_string(builder->ctx, theSolver) << "\n"; + llvm::errs() << "Model:\n" << Z3_model_to_string(builder->ctx, theModel) << "\n"; + } + + Z3_ast_vector_dec_ref(builder->ctx, constraints); + return success; +} + SolverImpl::SolverRunStatus Z3SolverImpl::getOperationStatusCode() { return runStatusCode; } diff --git a/lib/Solver/Z3Solver.h b/lib/Solver/Z3Solver.h new file mode 100644 index 00000000..8dc97e06 --- /dev/null +++ b/lib/Solver/Z3Solver.h @@ -0,0 +1,34 @@ +//===-- Z3Solver.h +//---------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_Z3SOLVER_H +#define KLEE_Z3SOLVER_H + +#include "klee/Solver.h" + +namespace klee { +/// Z3Solver - A solver complete solver based on Z3 +class Z3Solver : public Solver { +public: + /// Z3Solver - Construct a new Z3Solver. + Z3Solver(); + + /// Get the query in SMT-LIBv2 format. + /// \return A C-style string. The caller is responsible for freeing this. + virtual char *getConstraintLog(const Query &); + + /// setCoreSolverTimeout - Set constraint solver timeout delay to the given + /// value; 0 + /// is off. + virtual void setCoreSolverTimeout(double timeout); +}; +} + +#endif /* KLEE_Z3SOLVER_H */ |