aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/Solver
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Solver')
-rw-r--r--lib/Solver/AssignmentValidatingSolver.cpp9
-rw-r--r--lib/Solver/CachingSolver.cpp4
-rw-r--r--lib/Solver/CexCachingSolver.cpp4
-rw-r--r--lib/Solver/IncompleteSolver.cpp2
-rw-r--r--lib/Solver/IndependentSolver.cpp4
-rw-r--r--lib/Solver/MetaSMTSolver.cpp11
-rw-r--r--lib/Solver/MetaSMTSolver.h2
-rw-r--r--lib/Solver/QueryLoggingSolver.cpp2
-rw-r--r--lib/Solver/QueryLoggingSolver.h2
-rw-r--r--lib/Solver/STPSolver.cpp11
-rw-r--r--lib/Solver/STPSolver.h2
-rw-r--r--lib/Solver/Solver.cpp2
-rw-r--r--lib/Solver/ValidatingSolver.cpp4
-rw-r--r--lib/Solver/Z3Solver.cpp29
-rw-r--r--lib/Solver/Z3Solver.h2
15 files changed, 40 insertions, 50 deletions
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<std::vector<unsigned char> > &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<unsigned char> > &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<unsigned char> > &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<SolverContext> *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<SolverContext>::MetaSMTSolverImpl(
}
template <typename SolverContext>
-char *MetaSMTSolverImpl<SolverContext>::getConstraintLog(const Query &) {
- const char *msg = "Not supported";
- char *buf = new char[strlen(msg) + 1];
- strcpy(buf, msg);
- return buf;
+std::string MetaSMTSolverImpl<SolverContext>::getConstraintLog(const Query &) {
+ return {"Not supported"};
}
template <typename SolverContext>
@@ -409,7 +406,7 @@ template <typename SolverContext>
MetaSMTSolver<SolverContext>::~MetaSMTSolver() {}
template <typename SolverContext>
-char *MetaSMTSolver<SolverContext>::getConstraintLog(const Query &query) {
+std::string MetaSMTSolver<SolverContext>::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<std::vector<unsigned char> > &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<STPSolverImpl>(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<SolverImpl> 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<std::vector<unsigned char>> &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<Z3SolverImpl>()) {}
-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<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
@@ -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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-19 19:46:09 +0000