diff options
Diffstat (limited to 'lib/Solver/Z3Solver.cpp')
| -rw-r--r-- | lib/Solver/Z3Solver.cpp | 160 |
1 files changed, 149 insertions, 11 deletions
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; } |