about summary refs log tree commit diff homepage
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-pink 1.4.1 (git 2.36.1) at 2024-11-21 20:19:41 +0000