From 3d0033f099c907bcd5d4d2c2a7562037071ec2bf Mon Sep 17 00:00:00 2001
From: Daniel Schemmel <daniel@schemmel.net>
Date: Thu, 30 Jun 2022 03:59:57 +0100
Subject: Fix memory leak in crosscheck core solver mechanism

---
 lib/Solver/ConstructSolverChain.cpp |  2 +-
 lib/Solver/ValidatingSolver.cpp     | 18 ++++++++++++------
 2 files changed, 13 insertions(+), 7 deletions(-)

(limited to 'lib')

diff --git a/lib/Solver/ConstructSolverChain.cpp b/lib/Solver/ConstructSolverChain.cpp
index 3dab0361..999edda4 100644
--- a/lib/Solver/ConstructSolverChain.cpp
+++ b/lib/Solver/ConstructSolverChain.cpp
@@ -71,7 +71,7 @@ Solver *constructSolverChain(Solver *coreSolver,
   }
   if (DebugCrossCheckCoreSolverWith != NO_SOLVER) {
     Solver *oracleSolver = createCoreSolver(DebugCrossCheckCoreSolverWith);
-    solver = createValidatingSolver(/*s=*/solver, /*oracle=*/oracleSolver);
+    solver = createValidatingSolver(solver, oracleSolver, true);
   }
 
   return solver;
diff --git a/lib/Solver/ValidatingSolver.cpp b/lib/Solver/ValidatingSolver.cpp
index 5d4dab39..d95b8942 100644
--- a/lib/Solver/ValidatingSolver.cpp
+++ b/lib/Solver/ValidatingSolver.cpp
@@ -18,18 +18,24 @@ namespace klee {
 class ValidatingSolver : public SolverImpl {
 private:
   Solver *solver, *oracle;
+  bool ownsOracle;
 
 public:
-  ValidatingSolver(Solver *_solver, Solver *_oracle)
-      : solver(_solver), oracle(_oracle) {}
-  ~ValidatingSolver() { delete solver; }
+  ValidatingSolver(Solver *solver, Solver *oracle, bool ownsOracle = false)
+      : solver(solver), oracle(oracle), ownsOracle(ownsOracle) {}
+  ~ValidatingSolver() {
+    delete solver;
+    if (ownsOracle) {
+      delete oracle;
+    }
+  }
 
   bool computeValidity(const Query &, Solver::Validity &result);
   bool computeTruth(const Query &, bool &isValid);
   bool computeValue(const Query &, ref<Expr> &result);
   bool computeInitialValues(const Query &,
                             const std::vector<const Array *> &objects,
-                            std::vector<std::vector<unsigned char> > &values,
+                            std::vector<std::vector<unsigned char>> &values,
                             bool &hasSolution);
   SolverRunStatus getOperationStatusCode();
   char *getConstraintLog(const Query &);
@@ -136,7 +142,7 @@ void ValidatingSolver::setCoreSolverTimeout(time::Span timeout) {
   solver->impl->setCoreSolverTimeout(timeout);
 }
 
-Solver *createValidatingSolver(Solver *s, Solver *oracle) {
-  return new Solver(new ValidatingSolver(s, oracle));
+Solver *createValidatingSolver(Solver *s, Solver *oracle, bool ownsOracle) {
+  return new Solver(new ValidatingSolver(s, oracle, ownsOracle));
 }
 }
-- 
cgit 1.4.1