From 2e12c5326edde78b1344cc9df1a51db902e41bd5 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 24 May 2017 18:37:50 +0100 Subject: [Z3] In `getConstraintLog()` use a separate builder from that of the solver. This is to avoid tampering with the cache of the builder the solver is using. --- lib/Solver/Z3Solver.cpp | 21 ++++++++++++++++++--- 1 file changed, 18 insertions(+), 3 deletions(-) (limited to 'lib/Solver/Z3Solver.cpp') diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp index 2b2e63b8..f32860f7 100644 --- a/lib/Solver/Z3Solver.cpp +++ b/lib/Solver/Z3Solver.cpp @@ -132,10 +132,18 @@ void Z3Solver::setCoreSolverTimeout(double timeout) { char *Z3SolverImpl::getConstraintLog(const Query &query) { std::vector 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 >::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(); @@ -152,10 +160,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", @@ -166,6 +175,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); } -- cgit 1.4.1