From 3ca81c2dc3881aec0bbf94646c73a148d706c76d Mon Sep 17 00:00:00 2001 From: Daniel Schemmel Date: Sun, 29 Oct 2023 16:00:02 +0000 Subject: Change `GetConstraintLog` to work with `std::string`s instead of `char*`s --- include/klee/Solver/IncompleteSolver.h | 2 +- include/klee/Solver/Solver.h | 3 ++- include/klee/Solver/SolverImpl.h | 6 +++--- lib/Core/Executor.cpp | 4 +--- lib/Core/TimingSolver.h | 3 ++- lib/Solver/AssignmentValidatingSolver.cpp | 9 ++++----- lib/Solver/CachingSolver.cpp | 4 ++-- lib/Solver/CexCachingSolver.cpp | 4 ++-- lib/Solver/IncompleteSolver.cpp | 2 +- lib/Solver/IndependentSolver.cpp | 4 ++-- lib/Solver/MetaSMTSolver.cpp | 11 ++++------- lib/Solver/MetaSMTSolver.h | 2 +- lib/Solver/QueryLoggingSolver.cpp | 2 +- lib/Solver/QueryLoggingSolver.h | 2 +- lib/Solver/STPSolver.cpp | 11 +++++++---- lib/Solver/STPSolver.h | 2 +- lib/Solver/Solver.cpp | 2 +- lib/Solver/ValidatingSolver.cpp | 4 ++-- lib/Solver/Z3Solver.cpp | 29 ++++++++++------------------- lib/Solver/Z3Solver.h | 2 +- unittests/Solver/Z3SolverTest.cpp | 6 +++--- 21 files changed, 52 insertions(+), 62 deletions(-) diff --git a/include/klee/Solver/IncompleteSolver.h b/include/klee/Solver/IncompleteSolver.h index 8bcf7f88..f026743b 100644 --- a/include/klee/Solver/IncompleteSolver.h +++ b/include/klee/Solver/IncompleteSolver.h @@ -104,7 +104,7 @@ public: std::vector< std::vector > &values, bool &hasSolution); SolverRunStatus getOperationStatusCode(); - char *getConstraintLog(const Query&); + std::string getConstraintLog(const Query&) override; void setCoreSolverTimeout(time::Span timeout); }; diff --git a/include/klee/Solver/Solver.h b/include/klee/Solver/Solver.h index c50b17d8..8679cb87 100644 --- a/include/klee/Solver/Solver.h +++ b/include/klee/Solver/Solver.h @@ -15,6 +15,7 @@ #include "klee/Solver/SolverCmdLine.h" #include +#include #include namespace klee { @@ -202,7 +203,7 @@ namespace klee { // FIXME: This should go into a helper class, and should handle failure. virtual std::pair< ref, ref > getRange(const Query&); - virtual char *getConstraintLog(const Query& query); + virtual std::string getConstraintLog(const Query& query); virtual void setCoreSolverTimeout(time::Span timeout); }; diff --git a/include/klee/Solver/SolverImpl.h b/include/klee/Solver/SolverImpl.h index b73370b9..a8b4f8e4 100644 --- a/include/klee/Solver/SolverImpl.h +++ b/include/klee/Solver/SolverImpl.h @@ -101,9 +101,9 @@ namespace klee { /// status code static const char* getOperationStatusString(SolverRunStatus statusCode); - virtual char *getConstraintLog(const Query& query) { - // dummy - return nullptr; + virtual std::string getConstraintLog(const Query &query) { + // dummy + return {}; } virtual void setCoreSolverTimeout(time::Span timeout) {}; diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 49df9790..eccdf9eb 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -4734,9 +4734,7 @@ void Executor::getConstraintLog(const ExecutionState &state, std::string &res, switch (logFormat) { case STP: { Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool)); - char *log = solver->getConstraintLog(query); - res = std::string(log); - free(log); + res = solver->getConstraintLog(query); } break; case KQUERY: { diff --git a/lib/Core/TimingSolver.h b/lib/Core/TimingSolver.h index 0b88be3c..4042c724 100644 --- a/lib/Core/TimingSolver.h +++ b/lib/Core/TimingSolver.h @@ -16,6 +16,7 @@ #include "klee/System/Time.h" #include +#include #include #include @@ -41,7 +42,7 @@ public: void setTimeout(time::Span t) { solver->setCoreSolverTimeout(t); } - char *getConstraintLog(const Query &query) { + std::string getConstraintLog(const Query &query) { return solver->getConstraintLog(query); } diff --git a/lib/Solver/AssignmentValidatingSolver.cpp b/lib/Solver/AssignmentValidatingSolver.cpp index d90cf6b2..891abfb2 100644 --- a/lib/Solver/AssignmentValidatingSolver.cpp +++ b/lib/Solver/AssignmentValidatingSolver.cpp @@ -35,7 +35,7 @@ public: std::vector > &values, bool &hasSolution); SolverRunStatus getOperationStatusCode(); - char *getConstraintLog(const Query &); + std::string getConstraintLog(const Query &) override; void setCoreSolverTimeout(time::Span timeout); }; @@ -132,9 +132,8 @@ void AssignmentValidatingSolver::dumpAssignmentQuery( Query augmentedQuery(constraints, 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); + llvm::errs() << "Query with assignment as constraints:\n" + << solver->getConstraintLog(augmentedQuery) << "\n"; } SolverImpl::SolverRunStatus @@ -142,7 +141,7 @@ AssignmentValidatingSolver::getOperationStatusCode() { return solver->impl->getOperationStatusCode(); } -char *AssignmentValidatingSolver::getConstraintLog(const Query &query) { +std::string AssignmentValidatingSolver::getConstraintLog(const Query &query) { return solver->impl->getConstraintLog(query); } diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp index 751e81c1..41b95316 100644 --- a/lib/Solver/CachingSolver.cpp +++ b/lib/Solver/CachingSolver.cpp @@ -85,7 +85,7 @@ public: hasSolution); } SolverRunStatus getOperationStatusCode(); - char *getConstraintLog(const Query&); + std::string getConstraintLog(const Query&) override; void setCoreSolverTimeout(time::Span timeout); }; @@ -246,7 +246,7 @@ SolverImpl::SolverRunStatus CachingSolver::getOperationStatusCode() { return solver->impl->getOperationStatusCode(); } -char *CachingSolver::getConstraintLog(const Query& query) { +std::string CachingSolver::getConstraintLog(const Query& query) { return solver->impl->getConstraintLog(query); } diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp index 87e6169c..993a1633 100644 --- a/lib/Solver/CexCachingSolver.cpp +++ b/lib/Solver/CexCachingSolver.cpp @@ -95,7 +95,7 @@ public: std::vector< std::vector > &values, bool &hasSolution); SolverRunStatus getOperationStatusCode(); - char *getConstraintLog(const Query& query); + std::string getConstraintLog(const Query& query) override; void setCoreSolverTimeout(time::Span timeout); }; @@ -357,7 +357,7 @@ SolverImpl::SolverRunStatus CexCachingSolver::getOperationStatusCode() { return solver->impl->getOperationStatusCode(); } -char *CexCachingSolver::getConstraintLog(const Query& query) { +std::string CexCachingSolver::getConstraintLog(const Query& query) { return solver->impl->getConstraintLog(query); } diff --git a/lib/Solver/IncompleteSolver.cpp b/lib/Solver/IncompleteSolver.cpp index 7aef05c9..f8899cde 100644 --- a/lib/Solver/IncompleteSolver.cpp +++ b/lib/Solver/IncompleteSolver.cpp @@ -134,7 +134,7 @@ SolverImpl::SolverRunStatus StagedSolverImpl::getOperationStatusCode() { return secondary->impl->getOperationStatusCode(); } -char *StagedSolverImpl::getConstraintLog(const Query& query) { +std::string StagedSolverImpl::getConstraintLog(const Query& query) { return secondary->impl->getConstraintLog(query); } diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index c05fa6bb..3d73b067 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -404,7 +404,7 @@ public: std::vector< std::vector > &values, bool &hasSolution); SolverRunStatus getOperationStatusCode(); - char *getConstraintLog(const Query&); + std::string getConstraintLog(const Query&) override; void setCoreSolverTimeout(time::Span timeout); }; @@ -550,7 +550,7 @@ SolverImpl::SolverRunStatus IndependentSolver::getOperationStatusCode() { return solver->impl->getOperationStatusCode(); } -char *IndependentSolver::getConstraintLog(const Query& query) { +std::string IndependentSolver::getConstraintLog(const Query& query) { return solver->impl->getConstraintLog(query); } diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp index c3c6dfaa..197b89c3 100644 --- a/lib/Solver/MetaSMTSolver.cpp +++ b/lib/Solver/MetaSMTSolver.cpp @@ -88,7 +88,7 @@ public: MetaSMTSolverImpl(MetaSMTSolver *solver, bool useForked, bool optimizeDivides); - char *getConstraintLog(const Query &); + std::string getConstraintLog(const Query &) override; void setCoreSolverTimeout(time::Span timeout) { _timeout = timeout; } bool computeTruth(const Query &, bool &isValid); @@ -135,11 +135,8 @@ MetaSMTSolverImpl::MetaSMTSolverImpl( } template -char *MetaSMTSolverImpl::getConstraintLog(const Query &) { - const char *msg = "Not supported"; - char *buf = new char[strlen(msg) + 1]; - strcpy(buf, msg); - return buf; +std::string MetaSMTSolverImpl::getConstraintLog(const Query &) { + return {"Not supported"}; } template @@ -409,7 +406,7 @@ template MetaSMTSolver::~MetaSMTSolver() {} template -char *MetaSMTSolver::getConstraintLog(const Query &query) { +std::string MetaSMTSolver::getConstraintLog(const Query &query) { return impl->getConstraintLog(query); } diff --git a/lib/Solver/MetaSMTSolver.h b/lib/Solver/MetaSMTSolver.h index 64c56c57..eab2f789 100644 --- a/lib/Solver/MetaSMTSolver.h +++ b/lib/Solver/MetaSMTSolver.h @@ -22,7 +22,7 @@ public: MetaSMTSolver(bool useForked, bool optimizeDivides); virtual ~MetaSMTSolver(); - virtual char *getConstraintLog(const Query &); + std::string getConstraintLog(const Query &) override; virtual void setCoreSolverTimeout(time::Span timeout); }; diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp index 911fa067..df57a7db 100644 --- a/lib/Solver/QueryLoggingSolver.cpp +++ b/lib/Solver/QueryLoggingSolver.cpp @@ -208,7 +208,7 @@ SolverImpl::SolverRunStatus QueryLoggingSolver::getOperationStatusCode() { return solver->impl->getOperationStatusCode(); } -char *QueryLoggingSolver::getConstraintLog(const Query &query) { +std::string QueryLoggingSolver::getConstraintLog(const Query &query) { return solver->impl->getConstraintLog(query); } diff --git a/lib/Solver/QueryLoggingSolver.h b/lib/Solver/QueryLoggingSolver.h index 8149342f..0c975276 100644 --- a/lib/Solver/QueryLoggingSolver.h +++ b/lib/Solver/QueryLoggingSolver.h @@ -71,7 +71,7 @@ public: std::vector > &values, bool &hasSolution); SolverRunStatus getOperationStatusCode(); - char *getConstraintLog(const Query &); + std::string getConstraintLog(const Query &) override; void setCoreSolverTimeout(time::Span timeout); }; diff --git a/lib/Solver/STPSolver.cpp b/lib/Solver/STPSolver.cpp index 8858e83e..7df61834 100644 --- a/lib/Solver/STPSolver.cpp +++ b/lib/Solver/STPSolver.cpp @@ -95,7 +95,7 @@ public: explicit STPSolverImpl(bool useForkedSTP, bool optimizeDivides = true); ~STPSolverImpl() override; - char *getConstraintLog(const Query &) override; + std::string getConstraintLog(const Query &) override; void setCoreSolverTimeout(time::Span timeout) override { this->timeout = timeout; } bool computeTruth(const Query &, bool &isValid) override; @@ -195,7 +195,7 @@ STPSolverImpl::~STPSolverImpl() { /***/ -char *STPSolverImpl::getConstraintLog(const Query &query) { +std::string STPSolverImpl::getConstraintLog(const Query &query) { vc_push(vc); for (const auto &constraint : query.constraints) @@ -208,7 +208,10 @@ char *STPSolverImpl::getConstraintLog(const Query &query) { vc_printQueryStateToBuffer(vc, builder->getFalse(), &buffer, &length, false); vc_pop(vc); - return buffer; + std::string result = buffer; + std::free(buffer); + + return result; } bool STPSolverImpl::computeTruth(const Query &query, bool &isValid) { @@ -432,7 +435,7 @@ SolverImpl::SolverRunStatus STPSolverImpl::getOperationStatusCode() { STPSolver::STPSolver(bool useForkedSTP, bool optimizeDivides) : Solver(std::make_unique(useForkedSTP, optimizeDivides)) {} -char *STPSolver::getConstraintLog(const Query &query) { +std::string STPSolver::getConstraintLog(const Query &query) { return impl->getConstraintLog(query); } diff --git a/lib/Solver/STPSolver.h b/lib/Solver/STPSolver.h index 494a30db..fa13d457 100644 --- a/lib/Solver/STPSolver.h +++ b/lib/Solver/STPSolver.h @@ -27,7 +27,7 @@ public: /// getConstraintLog - Return the constraint log for the given state in CVC /// format. - virtual char *getConstraintLog(const Query &); + std::string getConstraintLog(const Query &) override; /// setCoreSolverTimeout - Set constraint solver timeout delay to the given /// value; 0 diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index bb6ed105..b3c70788 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -27,7 +27,7 @@ const char *Solver::validity_to_str(Validity v) { Solver::Solver(std::unique_ptr impl) : impl(std::move(impl)) {} Solver::~Solver() = default; -char *Solver::getConstraintLog(const Query& query) { +std::string Solver::getConstraintLog(const Query& query) { return impl->getConstraintLog(query); } diff --git a/lib/Solver/ValidatingSolver.cpp b/lib/Solver/ValidatingSolver.cpp index 8e9886d1..e836e8e6 100644 --- a/lib/Solver/ValidatingSolver.cpp +++ b/lib/Solver/ValidatingSolver.cpp @@ -38,7 +38,7 @@ public: std::vector> &values, bool &hasSolution); SolverRunStatus getOperationStatusCode(); - char *getConstraintLog(const Query &); + std::string getConstraintLog(const Query &) override; void setCoreSolverTimeout(time::Span timeout); }; @@ -134,7 +134,7 @@ SolverImpl::SolverRunStatus ValidatingSolver::getOperationStatusCode() { return solver->impl->getOperationStatusCode(); } -char *ValidatingSolver::getConstraintLog(const Query &query) { +std::string ValidatingSolver::getConstraintLog(const Query &query) { return solver->impl->getConstraintLog(query); } diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp index 180b32f6..c4a5d878 100644 --- a/lib/Solver/Z3Solver.cpp +++ b/lib/Solver/Z3Solver.cpp @@ -77,7 +77,7 @@ public: Z3SolverImpl(); ~Z3SolverImpl(); - char *getConstraintLog(const Query &); + std::string getConstraintLog(const Query &) override; void setCoreSolverTimeout(time::Span _timeout) { timeout = _timeout; @@ -141,7 +141,7 @@ Z3SolverImpl::~Z3SolverImpl() { Z3Solver::Z3Solver() : Solver(std::make_unique()) {} -char *Z3Solver::getConstraintLog(const Query &query) { +std::string Z3Solver::getConstraintLog(const Query &query) { return impl->getConstraintLog(query); } @@ -149,7 +149,7 @@ void Z3Solver::setCoreSolverTimeout(time::Span timeout) { impl->setCoreSolverTimeout(timeout); } -char *Z3SolverImpl::getConstraintLog(const Query &query) { +std::string 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 @@ -183,35 +183,26 @@ char *Z3SolverImpl::getConstraintLog(const Query &query) { } } - ::Z3_ast *assumptionsArray = NULL; - int numAssumptions = assumptions.size(); - if (numAssumptions) { - assumptionsArray = (::Z3_ast *)malloc(sizeof(::Z3_ast) * numAssumptions); - for (int index = 0; index < numAssumptions; ++index) { - assumptionsArray[index] = (::Z3_ast)assumptions[index]; - } - } - + std::vector<::Z3_ast> raw_assumptions{assumptions.cbegin(), + assumptions.cend()}; ::Z3_string result = Z3_benchmark_to_smtlib_string( temp_builder.ctx, /*name=*/"Emited by klee::Z3SolverImpl::getConstraintLog()", /*logic=*/"", /*status=*/"unknown", /*attributes=*/"", - /*num_assumptions=*/numAssumptions, - /*assumptions=*/assumptionsArray, + /*num_assumptions=*/raw_assumptions.size(), + /*assumptions=*/raw_assumptions.size() ? raw_assumptions.data() : nullptr, /*formula=*/formula); - 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`. + raw_assumptions.clear(); assumptions.clear(); formula = Z3ASTHandle(NULL, temp_builder.ctx); - // Client is responsible for freeing the returned C-string - return strdup(result); + + return {result}; } bool Z3SolverImpl::computeTruth(const Query &query, bool &isValid) { diff --git a/lib/Solver/Z3Solver.h b/lib/Solver/Z3Solver.h index 9688ccff..38b3e1bf 100644 --- a/lib/Solver/Z3Solver.h +++ b/lib/Solver/Z3Solver.h @@ -22,7 +22,7 @@ public: /// Get the query in SMT-LIBv2 format. /// \return A C-style string. The caller is responsible for freeing this. - virtual char *getConstraintLog(const Query &); + std::string getConstraintLog(const Query &) override; /// setCoreSolverTimeout - Set constraint solver timeout delay to the given /// value; 0 diff --git a/unittests/Solver/Z3SolverTest.cpp b/unittests/Solver/Z3SolverTest.cpp index 0eba3d0e..9f4a4786 100644 --- a/unittests/Solver/Z3SolverTest.cpp +++ b/unittests/Solver/Z3SolverTest.cpp @@ -63,9 +63,9 @@ TEST_F(Z3SolverTest, GetConstraintLog) { // Ensure this is not buggy as fixed in https://github.com/klee/klee/pull/1235 // If the bug is still present this fail due to an internal assertion - char *ConstraintsString = Z3Solver_->getConstraintLog(TheQuery); + std::string ConstraintsString = Z3Solver_->getConstraintLog(TheQuery); const char *ExpectedArraySelection = "(= (select const_array_0"; - const char *Occurence = std::strstr(ConstraintsString, ExpectedArraySelection); + const char *Occurence = + std::strstr(ConstraintsString.c_str(), ExpectedArraySelection); ASSERT_STRNE(Occurence, nullptr); - free(ConstraintsString); } -- cgit 1.4.1