diff options
29 files changed, 213 insertions, 167 deletions
diff --git a/include/klee/Solver/Common.h b/include/klee/Solver/Common.h index 7b244158..626ea55a 100644 --- a/include/klee/Solver/Common.h +++ b/include/klee/Solver/Common.h @@ -24,13 +24,10 @@ namespace klee { const char ALL_QUERIES_KQUERY_FILE_NAME[]="all-queries.kquery"; const char SOLVER_QUERIES_KQUERY_FILE_NAME[]="solver-queries.kquery"; - Solver *constructSolverChain(Solver *coreSolver, - std::string querySMT2LogPath, - std::string baseSolverQuerySMT2LogPath, - std::string queryKQueryLogPath, - std::string baseSolverQueryKQueryLogPath); -} - - +std::unique_ptr<Solver> constructSolverChain( + std::unique_ptr<Solver> coreSolver, std::string querySMT2LogPath, + std::string baseSolverQuerySMT2LogPath, std::string queryKQueryLogPath, + std::string baseSolverQueryKQueryLogPath); +} // namespace klee #endif /* KLEE_COMMON_H */ diff --git a/include/klee/Solver/IncompleteSolver.h b/include/klee/Solver/IncompleteSolver.h index b8ef1929..8bcf7f88 100644 --- a/include/klee/Solver/IncompleteSolver.h +++ b/include/klee/Solver/IncompleteSolver.h @@ -91,10 +91,11 @@ class StagedSolverImpl : public SolverImpl { private: std::unique_ptr<IncompleteSolver> primary; std::unique_ptr<Solver> secondary; - + public: - StagedSolverImpl(IncompleteSolver *_primary, Solver *_secondary); - + StagedSolverImpl(std::unique_ptr<IncompleteSolver> primary, + std::unique_ptr<Solver> secondary); + bool computeTruth(const Query&, bool &isValid); bool computeValidity(const Query&, Solver::Validity &result); bool computeValue(const Query&, ref<Expr> &result); diff --git a/include/klee/Solver/Solver.h b/include/klee/Solver/Solver.h index 2689d19c..c50b17d8 100644 --- a/include/klee/Solver/Solver.h +++ b/include/klee/Solver/Solver.h @@ -71,7 +71,7 @@ namespace klee { std::unique_ptr<SolverImpl> impl; - Solver(SolverImpl *impl); + Solver(std::unique_ptr<SolverImpl> impl); virtual ~Solver(); /// evaluate - Determine for a particular state if the query @@ -215,19 +215,22 @@ namespace klee { /// /// \param s - The primary underlying solver to use. /// \param oracle - The solver to check query results against. - Solver *createValidatingSolver(Solver *s, Solver *oracle, bool ownsOracle = false); + std::unique_ptr<Solver> createValidatingSolver(std::unique_ptr<Solver> s, + Solver *oracle, + bool ownsOracle); /// createAssignmentValidatingSolver - Create a solver that when requested /// for an assignment will check that the computed assignment satisfies /// the Query. /// \param s - The underlying solver to use. - Solver *createAssignmentValidatingSolver(Solver *s); + std::unique_ptr<Solver> + createAssignmentValidatingSolver(std::unique_ptr<Solver> s); /// createCachingSolver - Create a solver which will cache the queries in /// memory (without eviction). /// /// \param s - The underlying solver to use. - Solver *createCachingSolver(Solver *s); + std::unique_ptr<Solver> createCachingSolver(std::unique_ptr<Solver> s); /// createCexCachingSolver - Create a counterexample caching solver. This is a /// more sophisticated cache which records counterexamples for a constraint @@ -235,41 +238,40 @@ namespace klee { /// quickly find satisfying assignments. /// /// \param s - The underlying solver to use. - Solver *createCexCachingSolver(Solver *s); + std::unique_ptr<Solver> createCexCachingSolver(std::unique_ptr<Solver> s); /// createFastCexSolver - Create a "fast counterexample solver", which tries /// to quickly compute a satisfying assignment for a constraint set using /// value propogation and range analysis. /// /// \param s - The underlying solver to use. - Solver *createFastCexSolver(Solver *s); + std::unique_ptr<Solver> createFastCexSolver(std::unique_ptr<Solver> s); /// createIndependentSolver - Create a solver which will eliminate any /// unnecessary constraints before propogating the query to the underlying /// solver. /// /// \param s - The underlying solver to use. - Solver *createIndependentSolver(Solver *s); - + std::unique_ptr<Solver> createIndependentSolver(std::unique_ptr<Solver> s); + /// createKQueryLoggingSolver - Create a solver which will forward all queries /// after writing them to the given path in .kquery format. - Solver *createKQueryLoggingSolver(Solver *s, std::string path, - time::Span minQueryTimeToLog, - bool logTimedOut); + std::unique_ptr<Solver> + createKQueryLoggingSolver(std::unique_ptr<Solver> s, std::string path, + time::Span minQueryTimeToLog, bool logTimedOut); /// createSMTLIBLoggingSolver - Create a solver which will forward all queries /// after writing them to the given path in .smt2 format. - Solver *createSMTLIBLoggingSolver(Solver *s, std::string path, - time::Span minQueryTimeToLog, - bool logTimedOut); - + std::unique_ptr<Solver> + createSMTLIBLoggingSolver(std::unique_ptr<Solver> s, std::string path, + time::Span minQueryTimeToLog, bool logTimedOut); /// createDummySolver - Create a dummy solver implementation which always /// fails. - Solver *createDummySolver(); + std::unique_ptr<Solver> createDummySolver(); // Create a solver based on the supplied ``CoreSolverType``. - Solver *createCoreSolver(CoreSolverType cst); -} + std::unique_ptr<Solver> createCoreSolver(CoreSolverType cst); + } // namespace klee #endif /* KLEE_SOLVER_H */ diff --git a/include/klee/Solver/SolverImpl.h b/include/klee/Solver/SolverImpl.h index f03db964..b73370b9 100644 --- a/include/klee/Solver/SolverImpl.h +++ b/include/klee/Solver/SolverImpl.h @@ -23,12 +23,12 @@ namespace klee { /// SolverImpl - Abstract base clase for solver implementations. class SolverImpl { - // DO NOT IMPLEMENT. - SolverImpl(const SolverImpl&); - void operator=(const SolverImpl&); - public: - SolverImpl() {} + SolverImpl() = default; + + SolverImpl(const SolverImpl&) = delete; + SolverImpl& operator=(const SolverImpl&) = delete; + virtual ~SolverImpl(); enum SolverRunStatus { SOLVER_RUN_STATUS_SUCCESS_SOLVABLE, diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index b13afb6a..0b28d608 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -481,19 +481,19 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts, coreSolverTimeout = time::Span{MaxCoreSolverTime}; if (coreSolverTimeout) UseForkedCoreSolver = true; - Solver *coreSolver = klee::createCoreSolver(CoreSolverToUse); + std::unique_ptr<Solver> coreSolver = klee::createCoreSolver(CoreSolverToUse); if (!coreSolver) { klee_error("Failed to create core solver\n"); } - Solver *solver = constructSolverChain( - coreSolver, + std::unique_ptr<Solver> solver = constructSolverChain( + std::move(coreSolver), interpreterHandler->getOutputFilename(ALL_QUERIES_SMT2_FILE_NAME), interpreterHandler->getOutputFilename(SOLVER_QUERIES_SMT2_FILE_NAME), interpreterHandler->getOutputFilename(ALL_QUERIES_KQUERY_FILE_NAME), interpreterHandler->getOutputFilename(SOLVER_QUERIES_KQUERY_FILE_NAME)); - this->solver = new TimingSolver(solver, EqualitySubstitution); + this->solver = std::make_unique<TimingSolver>(std::move(solver), EqualitySubstitution); memory = new MemoryManager(&arrayCache); initializeSearchOptions(); @@ -593,7 +593,6 @@ Executor::~Executor() { delete externalDispatcher; delete specialFunctionHandler; delete statsTracker; - delete solver; } /***/ @@ -1236,7 +1235,7 @@ void Executor::addConstraint(ExecutionState &state, ref<Expr> condition) { assert(success && "FIXME: Unhandled solver failure"); (void) success; if (res) { - siit->patchSeed(state, condition, solver); + siit->patchSeed(state, condition, solver.get()); warn = true; } } @@ -3895,7 +3894,7 @@ void Executor::callExternalFunction(ExecutionState &state, // Checking to see if the argument is a pointer to something if (ce->getWidth() == Context::get().getPointerWidth() && state.addressSpace.resolveOne(ce, op)) { - op.second->flushToConcreteStore(solver, state); + op.second->flushToConcreteStore(solver.get(), state); } wordIndex += (ce->getWidth()+63)/64; } else { @@ -4234,7 +4233,7 @@ void Executor::resolveExact(ExecutionState &state, p = optimizer.optimizeExpr(p, true); // XXX we may want to be capping this? ResolutionList rl; - state.addressSpace.resolve(state, solver, p, rl); + state.addressSpace.resolve(state, solver.get(), p, rl); ExecutionState *unbound = &state; for (ResolutionList::iterator it = rl.begin(), ie = rl.end(); @@ -4294,7 +4293,7 @@ void Executor::executeMemoryOperation(ExecutionState &state, ObjectPair op; bool success; solver->setTimeout(coreSolverTimeout); - if (!state.addressSpace.resolveOne(state, solver, address, op, success)) { + if (!state.addressSpace.resolveOne(state, solver.get(), address, op, success)) { address = toConstant(state, address, "resolveOne failure"); success = state.addressSpace.resolveOne(cast<ConstantExpr>(address), op); } @@ -4351,7 +4350,7 @@ void Executor::executeMemoryOperation(ExecutionState &state, address = optimizer.optimizeExpr(address, true); ResolutionList rl; solver->setTimeout(coreSolverTimeout); - bool incomplete = state.addressSpace.resolve(state, solver, address, rl, + bool incomplete = state.addressSpace.resolve(state, solver.get(), address, rl, 0, coreSolverTimeout); solver->setTimeout(time::Span()); diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 28a7d56d..40111af9 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -110,7 +110,7 @@ private: Searcher *searcher; ExternalDispatcher *externalDispatcher; - TimingSolver *solver; + std::unique_ptr<TimingSolver> solver; MemoryManager *memory; std::set<ExecutionState*, ExecutionStateIDCompare> states; StatsTracker *statsTracker; diff --git a/lib/Core/TimingSolver.h b/lib/Core/TimingSolver.h index 1f179e54..0b88be3c 100644 --- a/lib/Core/TimingSolver.h +++ b/lib/Core/TimingSolver.h @@ -16,6 +16,7 @@ #include "klee/System/Time.h" #include <memory> +#include <utility> #include <vector> namespace klee { @@ -35,8 +36,8 @@ public: /// \param _simplifyExprs - Whether expressions should be /// simplified (via the constraint manager interface) prior to /// querying. - TimingSolver(Solver *_solver, bool _simplifyExprs = true) - : solver(_solver), simplifyExprs(_simplifyExprs) {} + TimingSolver(std::unique_ptr<Solver> solver, bool simplifyExprs = true) + : solver(std::move(solver)), simplifyExprs(simplifyExprs) {} void setTimeout(time::Span t) { solver->setCoreSolverTimeout(t); } diff --git a/lib/Solver/AssignmentValidatingSolver.cpp b/lib/Solver/AssignmentValidatingSolver.cpp index f18f43a8..d90cf6b2 100644 --- a/lib/Solver/AssignmentValidatingSolver.cpp +++ b/lib/Solver/AssignmentValidatingSolver.cpp @@ -13,6 +13,7 @@ #include "klee/Solver/SolverImpl.h" #include <memory> +#include <utility> #include <vector> namespace klee { @@ -23,7 +24,8 @@ private: void dumpAssignmentQuery(const Query &query, const Assignment &assignment); public: - AssignmentValidatingSolver(Solver *_solver) : solver(_solver) {} + AssignmentValidatingSolver(std::unique_ptr<Solver> solver) + : solver(std::move(solver)) {} bool computeValidity(const Query &, Solver::Validity &result); bool computeTruth(const Query &, bool &isValid); @@ -148,7 +150,9 @@ void AssignmentValidatingSolver::setCoreSolverTimeout(time::Span timeout) { return solver->impl->setCoreSolverTimeout(timeout); } -Solver *createAssignmentValidatingSolver(Solver *s) { - return new Solver(new AssignmentValidatingSolver(s)); +std::unique_ptr<Solver> +createAssignmentValidatingSolver(std::unique_ptr<Solver> s) { + return std::make_unique<Solver>( + std::make_unique<AssignmentValidatingSolver>(std::move(s))); } } diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp index 5d85062d..751e81c1 100644 --- a/lib/Solver/CachingSolver.cpp +++ b/lib/Solver/CachingSolver.cpp @@ -18,6 +18,7 @@ #include <memory> #include <unordered_map> +#include <utility> using namespace klee; @@ -67,7 +68,7 @@ private: cache_map cache; public: - CachingSolver(Solver *s) : solver(s) {} + CachingSolver(std::unique_ptr<Solver> solver) : solver(std::move(solver)) {} bool computeValidity(const Query&, Solver::Validity &result); bool computeTruth(const Query&, bool &isValid); @@ -255,6 +256,8 @@ void CachingSolver::setCoreSolverTimeout(time::Span timeout) { /// -Solver *klee::createCachingSolver(Solver *_solver) { - return new Solver(new CachingSolver(_solver)); +std::unique_ptr<Solver> +klee::createCachingSolver(std::unique_ptr<Solver> solver) { + return std::make_unique<Solver>( + std::make_unique<CachingSolver>(std::move(solver))); } diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp index 28996a6a..dbbd3516 100644 --- a/lib/Solver/CexCachingSolver.cpp +++ b/lib/Solver/CexCachingSolver.cpp @@ -24,6 +24,7 @@ #include "llvm/Support/CommandLine.h" #include <memory> +#include <utility> using namespace klee; using namespace llvm; @@ -87,7 +88,8 @@ class CexCachingSolver : public SolverImpl { bool getAssignment(const Query& query, Assignment *&result); public: - CexCachingSolver(Solver *_solver) : solver(_solver) {} + CexCachingSolver(std::unique_ptr<Solver> solver) + : solver(std::move(solver)) {} ~CexCachingSolver(); bool computeTruth(const Query&, bool &isValid); @@ -384,6 +386,8 @@ void CexCachingSolver::setCoreSolverTimeout(time::Span timeout) { /// -Solver *klee::createCexCachingSolver(Solver *_solver) { - return new Solver(new CexCachingSolver(_solver)); +std::unique_ptr<Solver> +klee::createCexCachingSolver(std::unique_ptr<Solver> solver) { + return std::make_unique<Solver>( + std::make_unique<CexCachingSolver>(std::move(solver))); } diff --git a/lib/Solver/ConstructSolverChain.cpp b/lib/Solver/ConstructSolverChain.cpp index 999edda4..9109fe1d 100644 --- a/lib/Solver/ConstructSolverChain.cpp +++ b/lib/Solver/ConstructSolverChain.cpp @@ -18,62 +18,72 @@ #include "llvm/Support/raw_ostream.h" +#include <memory> +#include <utility> namespace klee { -Solver *constructSolverChain(Solver *coreSolver, - std::string querySMT2LogPath, - std::string baseSolverQuerySMT2LogPath, - std::string queryKQueryLogPath, - std::string baseSolverQueryKQueryLogPath) { - Solver *solver = coreSolver; +std::unique_ptr<Solver> constructSolverChain( + std::unique_ptr<Solver> coreSolver, std::string querySMT2LogPath, + std::string baseSolverQuerySMT2LogPath, std::string queryKQueryLogPath, + std::string baseSolverQueryKQueryLogPath) { + Solver *rawCoreSolver = coreSolver.get(); + std::unique_ptr<Solver> solver = std::move(coreSolver); const time::Span minQueryTimeToLog(MinQueryTimeToLog); if (QueryLoggingOptions.isSet(SOLVER_KQUERY)) { - solver = createKQueryLoggingSolver(solver, baseSolverQueryKQueryLogPath, minQueryTimeToLog, LogTimedOutQueries); + solver = createKQueryLoggingSolver(std::move(solver), + baseSolverQueryKQueryLogPath, + minQueryTimeToLog, LogTimedOutQueries); klee_message("Logging queries that reach solver in .kquery format to %s\n", baseSolverQueryKQueryLogPath.c_str()); } if (QueryLoggingOptions.isSet(SOLVER_SMTLIB)) { - solver = createSMTLIBLoggingSolver(solver, baseSolverQuerySMT2LogPath, minQueryTimeToLog, LogTimedOutQueries); + solver = + createSMTLIBLoggingSolver(std::move(solver), baseSolverQuerySMT2LogPath, + minQueryTimeToLog, LogTimedOutQueries); klee_message("Logging queries that reach solver in .smt2 format to %s\n", baseSolverQuerySMT2LogPath.c_str()); } if (UseAssignmentValidatingSolver) - solver = createAssignmentValidatingSolver(solver); + solver = createAssignmentValidatingSolver(std::move(solver)); if (UseFastCexSolver) - solver = createFastCexSolver(solver); + solver = createFastCexSolver(std::move(solver)); if (UseCexCache) - solver = createCexCachingSolver(solver); + solver = createCexCachingSolver(std::move(solver)); if (UseBranchCache) - solver = createCachingSolver(solver); + solver = createCachingSolver(std::move(solver)); if (UseIndependentSolver) - solver = createIndependentSolver(solver); + solver = createIndependentSolver(std::move(solver)); if (DebugValidateSolver) - solver = createValidatingSolver(solver, coreSolver); + solver = createValidatingSolver(std::move(solver), rawCoreSolver, false); if (QueryLoggingOptions.isSet(ALL_KQUERY)) { - solver = createKQueryLoggingSolver(solver, queryKQueryLogPath, minQueryTimeToLog, LogTimedOutQueries); + solver = createKQueryLoggingSolver(std::move(solver), queryKQueryLogPath, + minQueryTimeToLog, LogTimedOutQueries); klee_message("Logging all queries in .kquery format to %s\n", queryKQueryLogPath.c_str()); } if (QueryLoggingOptions.isSet(ALL_SMTLIB)) { - solver = createSMTLIBLoggingSolver(solver, querySMT2LogPath, minQueryTimeToLog, LogTimedOutQueries); + solver = createSMTLIBLoggingSolver(std::move(solver), querySMT2LogPath, + minQueryTimeToLog, LogTimedOutQueries); klee_message("Logging all queries in .smt2 format to %s\n", querySMT2LogPath.c_str()); } if (DebugCrossCheckCoreSolverWith != NO_SOLVER) { - Solver *oracleSolver = createCoreSolver(DebugCrossCheckCoreSolverWith); - solver = createValidatingSolver(solver, oracleSolver, true); + std::unique_ptr<Solver> oracleSolver = + createCoreSolver(DebugCrossCheckCoreSolverWith); + solver = + createValidatingSolver(std::move(solver), oracleSolver.release(), true); } return solver; } -} +} // namespace klee diff --git a/lib/Solver/CoreSolver.cpp b/lib/Solver/CoreSolver.cpp index fbf29747..abbccf5b 100644 --- a/lib/Solver/CoreSolver.cpp +++ b/lib/Solver/CoreSolver.cpp @@ -19,15 +19,16 @@ #include "llvm/Support/raw_ostream.h" #include <string> +#include <memory> namespace klee { -Solver *createCoreSolver(CoreSolverType cst) { +std::unique_ptr<Solver> createCoreSolver(CoreSolverType cst) { switch (cst) { case STP_SOLVER: #ifdef ENABLE_STP klee_message("Using STP solver backend"); - return new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides); + return std::make_unique<STPSolver>(UseForkedCoreSolver, CoreSolverOptimizeDivides); #else klee_message("Not compiled with STP support"); return NULL; @@ -45,7 +46,7 @@ Solver *createCoreSolver(CoreSolverType cst) { case Z3_SOLVER: #ifdef ENABLE_Z3 klee_message("Using Z3 solver backend"); - return new Z3Solver(); + return std::make_unique<Z3Solver>(); #else klee_message("Not compiled with Z3 support"); return NULL; diff --git a/lib/Solver/DummySolver.cpp b/lib/Solver/DummySolver.cpp index a845f901..1cf88d64 100644 --- a/lib/Solver/DummySolver.cpp +++ b/lib/Solver/DummySolver.cpp @@ -11,6 +11,8 @@ #include "klee/Solver/SolverImpl.h" #include "klee/Solver/SolverStats.h" +#include <memory> + namespace klee { class DummySolverImpl : public SolverImpl { @@ -59,5 +61,7 @@ SolverImpl::SolverRunStatus DummySolverImpl::getOperationStatusCode() { return SOLVER_RUN_STATUS_FAILURE; } -Solver *createDummySolver() { return new Solver(new DummySolverImpl()); } +std::unique_ptr<Solver> createDummySolver() { + return std::make_unique<Solver>(std::make_unique<DummySolverImpl>()); +} } diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp index 34a44c3e..81fd6707 100644 --- a/lib/Solver/FastCexSolver.cpp +++ b/lib/Solver/FastCexSolver.cpp @@ -24,6 +24,7 @@ #include <cassert> #include <map> #include <sstream> +#include <utility> #include <vector> using namespace klee; @@ -1141,7 +1142,7 @@ FastCexSolver::computeInitialValues(const Query& query, return true; } - -Solver *klee::createFastCexSolver(Solver *s) { - return new Solver(new StagedSolverImpl(new FastCexSolver(), s)); +std::unique_ptr<Solver> klee::createFastCexSolver(std::unique_ptr<Solver> s) { + return std::make_unique<Solver>(std::make_unique<StagedSolverImpl>( + std::make_unique<FastCexSolver>(), std::move(s))); } diff --git a/lib/Solver/IncompleteSolver.cpp b/lib/Solver/IncompleteSolver.cpp index a9035eda..7aef05c9 100644 --- a/lib/Solver/IncompleteSolver.cpp +++ b/lib/Solver/IncompleteSolver.cpp @@ -11,6 +11,8 @@ #include "klee/Expr/Constraints.h" +#include <utility> + using namespace klee; using namespace llvm; @@ -58,11 +60,9 @@ IncompleteSolver::computeValidity(const Query& query) { /***/ -StagedSolverImpl::StagedSolverImpl(IncompleteSolver *_primary, - Solver *_secondary) - : primary(_primary), - secondary(_secondary) { -} +StagedSolverImpl::StagedSolverImpl(std::unique_ptr<IncompleteSolver> primary, + std::unique_ptr<Solver> secondary) + : primary(std::move(primary)), secondary(std::move(secondary)) {} bool StagedSolverImpl::computeTruth(const Query& query, bool &isValid) { IncompleteSolver::PartialValidity trueResult = primary->computeTruth(query); diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index 007bfdcb..c05fa6bb 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -393,7 +393,8 @@ private: std::unique_ptr<Solver> solver; public: - IndependentSolver(Solver *_solver) : solver(_solver) {} + IndependentSolver(std::unique_ptr<Solver> solver) + : solver(std::move(solver)) {} bool computeTruth(const Query&, bool &isValid); bool computeValidity(const Query&, Solver::Validity &result); @@ -557,6 +558,8 @@ void IndependentSolver::setCoreSolverTimeout(time::Span timeout) { solver->impl->setCoreSolverTimeout(timeout); } -Solver *klee::createIndependentSolver(Solver *s) { - return new Solver(new IndependentSolver(s)); +std::unique_ptr<Solver> +klee::createIndependentSolver(std::unique_ptr<Solver> s) { + return std::make_unique<Solver>( + std::make_unique<IndependentSolver>(std::move(s))); } diff --git a/lib/Solver/KQueryLoggingSolver.cpp b/lib/Solver/KQueryLoggingSolver.cpp index fccdd615..4be24e9c 100644 --- a/lib/Solver/KQueryLoggingSolver.cpp +++ b/lib/Solver/KQueryLoggingSolver.cpp @@ -13,6 +13,8 @@ #include "klee/Expr/ExprPPrinter.h" #include "klee/System/Time.h" +#include <utility> + using namespace klee; class KQueryLoggingSolver : public QueryLoggingSolver { @@ -48,10 +50,11 @@ private : } public: - KQueryLoggingSolver(Solver *_solver, std::string path, time::Span queryTimeToLog, bool logTimedOut) - : QueryLoggingSolver(_solver, path, "#", queryTimeToLog, logTimedOut), - printer(ExprPPrinter::create(logBuffer)) { - } + KQueryLoggingSolver(std::unique_ptr<Solver> solver, std::string path, + time::Span queryTimeToLog, bool logTimedOut) + : QueryLoggingSolver(std::move(solver), std::move(path), "#", + queryTimeToLog, logTimedOut), + printer(ExprPPrinter::create(logBuffer)) {} virtual ~KQueryLoggingSolver() { delete printer; @@ -60,8 +63,10 @@ public: /// -Solver *klee::createKQueryLoggingSolver(Solver *_solver, std::string path, - time::Span minQueryTimeToLog, bool logTimedOut) { - return new Solver(new KQueryLoggingSolver(_solver, path, minQueryTimeToLog, logTimedOut)); +std::unique_ptr<Solver> +klee::createKQueryLoggingSolver(std::unique_ptr<Solver> solver, + std::string path, time::Span minQueryTimeToLog, + bool logTimedOut) { + return std::make_unique<Solver>(std::make_unique<KQueryLoggingSolver>( + std::move(solver), std::move(path), minQueryTimeToLog, logTimedOut)); } - diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp index 37c22f0e..c3c6dfaa 100644 --- a/lib/Solver/MetaSMTSolver.cpp +++ b/lib/Solver/MetaSMTSolver.cpp @@ -51,6 +51,8 @@ #undef type_t #endif +#include <memory> + #include <errno.h> #include <signal.h> #include <sys/ipc.h> @@ -85,7 +87,6 @@ private: public: MetaSMTSolverImpl(MetaSMTSolver<SolverContext> *solver, bool useForked, bool optimizeDivides); - virtual ~MetaSMTSolverImpl(); char *getConstraintLog(const Query &); void setCoreSolverTimeout(time::Span timeout) { _timeout = timeout; } @@ -134,9 +135,6 @@ MetaSMTSolverImpl<SolverContext>::MetaSMTSolverImpl( } template <typename SolverContext> -MetaSMTSolverImpl<SolverContext>::~MetaSMTSolverImpl() {} - -template <typename SolverContext> char *MetaSMTSolverImpl<SolverContext>::getConstraintLog(const Query &) { const char *msg = "Not supported"; char *buf = new char[strlen(msg) + 1]; @@ -404,8 +402,8 @@ MetaSMTSolverImpl<SolverContext>::getOperationStatusCode() { template <typename SolverContext> MetaSMTSolver<SolverContext>::MetaSMTSolver(bool useForked, bool optimizeDivides) - : Solver(new MetaSMTSolverImpl<SolverContext>(this, useForked, - optimizeDivides)) {} + : Solver(std::make_unique<MetaSMTSolverImpl<SolverContext>>( + this, useForked, optimizeDivides)) {} template <typename SolverContext> MetaSMTSolver<SolverContext>::~MetaSMTSolver() {} @@ -420,45 +418,50 @@ void MetaSMTSolver<SolverContext>::setCoreSolverTimeout(time::Span timeout) { impl->setCoreSolverTimeout(timeout); } -Solver *createMetaSMTSolver() { +std::unique_ptr<Solver> createMetaSMTSolver() { using namespace metaSMT; - Solver *coreSolver = NULL; + std::unique_ptr<Solver> coreSolver; std::string backend; switch (MetaSMTBackend) { #ifdef METASMT_HAVE_STP case METASMT_BACKEND_STP: backend = "STP"; - coreSolver = new MetaSMTSolver<DirectSolver_Context<solver::STP_Backend> >( + coreSolver = std::make_unique< + MetaSMTSolver<DirectSolver_Context<solver::STP_Backend>>>( UseForkedCoreSolver, CoreSolverOptimizeDivides); break; #endif #ifdef METASMT_HAVE_Z3 case METASMT_BACKEND_Z3: backend = "Z3"; - coreSolver = new MetaSMTSolver<DirectSolver_Context<solver::Z3_Backend> >( + coreSolver = std::make_unique< + MetaSMTSolver<DirectSolver_Context<solver::Z3_Backend>>>( UseForkedCoreSolver, CoreSolverOptimizeDivides); break; #endif #ifdef METASMT_HAVE_BTOR case METASMT_BACKEND_BOOLECTOR: backend = "Boolector"; - coreSolver = new MetaSMTSolver<DirectSolver_Context<solver::Boolector> >( + coreSolver = std::make_unique< + MetaSMTSolver<DirectSolver_Context<solver::Boolector>>>( UseForkedCoreSolver, CoreSolverOptimizeDivides); break; #endif #ifdef METASMT_HAVE_CVC4 case METASMT_BACKEND_CVC4: backend = "CVC4"; - coreSolver = new MetaSMTSolver<DirectSolver_Context<solver::CVC4> >( - UseForkedCoreSolver, CoreSolverOptimizeDivides); + coreSolver = + std::make_unique<MetaSMTSolver<DirectSolver_Context<solver::CVC4>>>( + UseForkedCoreSolver, CoreSolverOptimizeDivides); break; #endif #ifdef METASMT_HAVE_YICES2 case METASMT_BACKEND_YICES2: backend = "Yices2"; - coreSolver = new MetaSMTSolver<DirectSolver_Context<solver::Yices2> >( - UseForkedCoreSolver, CoreSolverOptimizeDivides); + coreSolver = + std::make_unique<MetaSMTSolver<DirectSolver_Context<solver::Yices2>>>( + UseForkedCoreSolver, CoreSolverOptimizeDivides); break; #endif default: @@ -468,6 +471,5 @@ Solver *createMetaSMTSolver() { klee_message("Starting MetaSMTSolver(%s)", backend.c_str()); return coreSolver; } - } #endif // ENABLE_METASMT diff --git a/lib/Solver/MetaSMTSolver.h b/lib/Solver/MetaSMTSolver.h index 89cb7143..64c56c57 100644 --- a/lib/Solver/MetaSMTSolver.h +++ b/lib/Solver/MetaSMTSolver.h @@ -13,6 +13,8 @@ #include "klee/Solver/Solver.h" +#include <memory> + namespace klee { template <typename SolverContext> class MetaSMTSolver : public Solver { @@ -26,7 +28,7 @@ public: /// createMetaSMTSolver - Create a solver using the metaSMT backend set by /// the option MetaSMTBackend. -Solver *createMetaSMTSolver(); +std::unique_ptr<Solver> createMetaSMTSolver(); } #endif /* KLEE_METASMTSOLVER_H */ diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp index c057751c..911fa067 100644 --- a/lib/Solver/QueryLoggingSolver.cpp +++ b/lib/Solver/QueryLoggingSolver.cpp @@ -15,6 +15,8 @@ #include "klee/Support/FileHandling.h" #include "klee/System/Time.h" +#include <utility> + namespace { llvm::cl::opt<bool> DumpPartialQueryiesEarly( "log-partial-queries-early", llvm::cl::init(false), @@ -29,13 +31,14 @@ llvm::cl::opt<bool> CreateCompressedQueryLog( #endif } // namespace -QueryLoggingSolver::QueryLoggingSolver(Solver *_solver, std::string path, +QueryLoggingSolver::QueryLoggingSolver(std::unique_ptr<Solver> solver, + std::string path, const std::string &commentSign, time::Span queryTimeToLog, bool logTimedOut) - : solver(_solver), BufferString(""), logBuffer(BufferString), queryCount(0), - minQueryTimeToLog(queryTimeToLog), logTimedOutQueries(logTimedOut), - queryCommentSign(commentSign) { + : solver(std::move(solver)), BufferString(""), logBuffer(BufferString), + queryCount(0), minQueryTimeToLog(queryTimeToLog), + logTimedOutQueries(logTimedOut), queryCommentSign(commentSign) { std::string error; #ifdef HAVE_ZLIB_H if (!CreateCompressedQueryLog) { @@ -50,7 +53,7 @@ QueryLoggingSolver::QueryLoggingSolver(Solver *_solver, std::string path, if (!os) { klee_error("Could not open file %s : %s", path.c_str(), error.c_str()); } - assert(0 != solver); + assert(this->solver); } void QueryLoggingSolver::flushBufferConditionally(bool writeToFile) { diff --git a/lib/Solver/QueryLoggingSolver.h b/lib/Solver/QueryLoggingSolver.h index 76bba429..8149342f 100644 --- a/lib/Solver/QueryLoggingSolver.h +++ b/lib/Solver/QueryLoggingSolver.h @@ -58,8 +58,9 @@ protected: void flushBufferConditionally(bool writeToFile); public: - QueryLoggingSolver(Solver *_solver, std::string path, const std::string &commentSign, - time::Span queryTimeToLog, bool logTimedOut); + QueryLoggingSolver(std::unique_ptr<Solver> solver, std::string path, + const std::string &commentSign, time::Span queryTimeToLog, + bool logTimedOut); /// implementation of the SolverImpl interface bool computeTruth(const Query &query, bool &isValid); diff --git a/lib/Solver/SMTLIBLoggingSolver.cpp b/lib/Solver/SMTLIBLoggingSolver.cpp index bfea5c1b..c0713b45 100644 --- a/lib/Solver/SMTLIBLoggingSolver.cpp +++ b/lib/Solver/SMTLIBLoggingSolver.cpp @@ -11,6 +11,9 @@ #include "klee/Expr/ExprSMTLIBPrinter.h" +#include <memory> +#include <utility> + using namespace klee; /// This QueryLoggingSolver will log queries to a file in the SMTLIBv2 format @@ -18,7 +21,6 @@ using namespace klee; class SMTLIBLoggingSolver : public QueryLoggingSolver { private: - ExprSMTLIBPrinter printer; virtual void printQuery(const Query& query, @@ -41,22 +43,21 @@ class SMTLIBLoggingSolver : public QueryLoggingSolver printer.generateOutput(); } - - public: - SMTLIBLoggingSolver(Solver *_solver, - std::string path, - time::Span queryTimeToLog, - bool logTimedOut) - : QueryLoggingSolver(_solver, path, ";", queryTimeToLog, logTimedOut) - { - //Setup the printer - printer.setOutput(logBuffer); - } -}; +public: + SMTLIBLoggingSolver(std::unique_ptr<Solver> solver, std::string path, + time::Span queryTimeToLog, bool logTimedOut) + : QueryLoggingSolver(std::move(solver), std::move(path), ";", + queryTimeToLog, logTimedOut) { + // Setup the printer + printer.setOutput(logBuffer); + } +}; -Solver* klee::createSMTLIBLoggingSolver(Solver *_solver, std::string path, - time::Span minQueryTimeToLog, bool logTimedOut) -{ - return new Solver(new SMTLIBLoggingSolver(_solver, path, minQueryTimeToLog, logTimedOut)); +std::unique_ptr<Solver> +klee::createSMTLIBLoggingSolver(std::unique_ptr<Solver> solver, + std::string path, time::Span minQueryTimeToLog, + bool logTimedOut) { + return std::make_unique<Solver>(std::make_unique<SMTLIBLoggingSolver>( + std::move(solver), std::move(path), minQueryTimeToLog, logTimedOut)); } diff --git a/lib/Solver/STPSolver.cpp b/lib/Solver/STPSolver.cpp index 140ca6f4..8858e83e 100644 --- a/lib/Solver/STPSolver.cpp +++ b/lib/Solver/STPSolver.cpp @@ -430,7 +430,7 @@ SolverImpl::SolverRunStatus STPSolverImpl::getOperationStatusCode() { } STPSolver::STPSolver(bool useForkedSTP, bool optimizeDivides) - : Solver(new STPSolverImpl(useForkedSTP, optimizeDivides)) {} + : Solver(std::make_unique<STPSolverImpl>(useForkedSTP, optimizeDivides)) {} char *STPSolver::getConstraintLog(const Query &query) { return impl->getConstraintLog(query); diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index e123a667..bb6ed105 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -12,6 +12,8 @@ #include "klee/Expr/Constraints.h" #include "klee/Solver/SolverImpl.h" +#include <utility> + using namespace klee; const char *Solver::validity_to_str(Validity v) { @@ -22,7 +24,7 @@ const char *Solver::validity_to_str(Validity v) { } } -Solver::Solver(SolverImpl *impl) : impl(impl) {} +Solver::Solver(std::unique_ptr<SolverImpl> impl) : impl(std::move(impl)) {} Solver::~Solver() = default; char *Solver::getConstraintLog(const Query& query) { diff --git a/lib/Solver/ValidatingSolver.cpp b/lib/Solver/ValidatingSolver.cpp index 72bdc830..8e9886d1 100644 --- a/lib/Solver/ValidatingSolver.cpp +++ b/lib/Solver/ValidatingSolver.cpp @@ -12,6 +12,7 @@ #include "klee/Solver/SolverImpl.h" #include <memory> +#include <utility> #include <vector> namespace klee { @@ -22,8 +23,9 @@ private: std::unique_ptr<Solver, void(*)(Solver*)> oracle; public: - ValidatingSolver(Solver *solver, Solver *oracle, bool ownsOracle = false) - : solver(solver), + ValidatingSolver(std::unique_ptr<Solver> solver, Solver *oracle, + bool ownsOracle) + : solver(std::move(solver)), oracle( oracle, ownsOracle ? [](Solver *solver) { delete solver; } : [](Solver *) {}) {} @@ -140,7 +142,10 @@ void ValidatingSolver::setCoreSolverTimeout(time::Span timeout) { solver->impl->setCoreSolverTimeout(timeout); } -Solver *createValidatingSolver(Solver *s, Solver *oracle, bool ownsOracle) { - return new Solver(new ValidatingSolver(s, oracle, ownsOracle)); +std::unique_ptr<Solver> createValidatingSolver(std::unique_ptr<Solver> s, + Solver *oracle, + bool ownsOracle) { + return std::make_unique<Solver>( + std::make_unique<ValidatingSolver>(std::move(s), oracle, ownsOracle)); } } diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp index f3e8f92b..180b32f6 100644 --- a/lib/Solver/Z3Solver.cpp +++ b/lib/Solver/Z3Solver.cpp @@ -139,7 +139,7 @@ Z3SolverImpl::~Z3SolverImpl() { Z3_params_dec_ref(builder->ctx, solverParameters); } -Z3Solver::Z3Solver() : Solver(new Z3SolverImpl()) {} +Z3Solver::Z3Solver() : Solver(std::make_unique<Z3SolverImpl>()) {} char *Z3Solver::getConstraintLog(const Query &query) { return impl->getConstraintLog(query); diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index eed4e4c9..51298dfb 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -29,12 +29,11 @@ #include "llvm/Support/ManagedStatic.h" #include "llvm/Support/MemoryBuffer.h" #include "llvm/Support/raw_ostream.h" +#include "llvm/Support/Signals.h" #include <sys/stat.h> #include <unistd.h> - - -#include "llvm/Support/Signals.h" +#include <utility> using namespace llvm; using namespace klee; @@ -200,7 +199,7 @@ static bool EvaluateInputAST(const char *Filename, if (!success) return false; - Solver *coreSolver = klee::createCoreSolver(CoreSolverToUse); + std::unique_ptr<Solver> coreSolver = klee::createCoreSolver(CoreSolverToUse); if (CoreSolverToUse != DUMMY_SOLVER) { const time::Span maxCoreSolverTime(MaxCoreSolverTime); @@ -209,11 +208,11 @@ static bool EvaluateInputAST(const char *Filename, } } - Solver *S = constructSolverChain(coreSolver, - getQueryLogPath(ALL_QUERIES_SMT2_FILE_NAME), - getQueryLogPath(SOLVER_QUERIES_SMT2_FILE_NAME), - getQueryLogPath(ALL_QUERIES_KQUERY_FILE_NAME), - getQueryLogPath(SOLVER_QUERIES_KQUERY_FILE_NAME)); + std::unique_ptr<Solver> S = constructSolverChain( + std::move(coreSolver), getQueryLogPath(ALL_QUERIES_SMT2_FILE_NAME), + getQueryLogPath(SOLVER_QUERIES_SMT2_FILE_NAME), + getQueryLogPath(ALL_QUERIES_KQUERY_FILE_NAME), + getQueryLogPath(SOLVER_QUERIES_KQUERY_FILE_NAME)); unsigned Index = 0; for (std::vector<Decl*>::iterator it = Decls.begin(), @@ -294,8 +293,6 @@ static bool EvaluateInputAST(const char *Filename, delete *it; delete P; - delete S; - if (uint64_t queries = *theStatisticManager->getStatisticByName("SolverQueries")) { llvm::outs() << "--\n" diff --git a/unittests/Solver/SolverTest.cpp b/unittests/Solver/SolverTest.cpp index d5d207a0..2137602f 100644 --- a/unittests/Solver/SolverTest.cpp +++ b/unittests/Solver/SolverTest.cpp @@ -131,11 +131,11 @@ void testOpcode(Solver &solver, bool tryBool = true, bool tryZero = true, } TEST(SolverTest, Evaluation) { - Solver *solver = klee::createCoreSolver(CoreSolverToUse); + auto solver = klee::createCoreSolver(CoreSolverToUse); - solver = createCexCachingSolver(solver); - solver = createCachingSolver(solver); - solver = createIndependentSolver(solver); + solver = createCexCachingSolver(std::move(solver)); + solver = createCachingSolver(std::move(solver)); + solver = createIndependentSolver(std::move(solver)); testOpcode<SelectExpr>(*solver); testOpcode<ZExtExpr>(*solver); @@ -165,8 +165,6 @@ TEST(SolverTest, Evaluation) { testOpcode<SleExpr>(*solver); testOpcode<SgtExpr>(*solver); testOpcode<SgeExpr>(*solver); - - delete solver; } } diff --git a/unittests/Solver/Z3SolverTest.cpp b/unittests/Solver/Z3SolverTest.cpp index eab43d79..e81ff19e 100644 --- a/unittests/Solver/Z3SolverTest.cpp +++ b/unittests/Solver/Z3SolverTest.cpp @@ -19,6 +19,8 @@ #include "klee/Expr/Expr.h" #include "klee/Solver/Solver.h" +#include <memory> + using namespace klee; namespace { @@ -26,13 +28,11 @@ ArrayCache AC; } class Z3SolverTest : public ::testing::Test { protected: + std::unique_ptr<Solver> Z3Solver_; + Z3SolverTest() : Z3Solver_(createCoreSolver(CoreSolverType::Z3_SOLVER)) { Z3Solver_->setCoreSolverTimeout(time::Span("10s")); } - - virtual ~Z3SolverTest() { delete Z3Solver_; } - - Solver *Z3Solver_; }; TEST_F(Z3SolverTest, GetConstraintLog) { |