From f4f83690f3b22cdfef409253453d4dd00baaa72f Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Sat, 4 Jan 2020 21:45:21 +0100 Subject: [PATCH] Replace some shared_ptr by unique_ptr or raw pointers --- libsolidity/formal/BMC.cpp | 6 ++--- libsolidity/formal/BMC.h | 6 ++--- libsolidity/formal/CHC.cpp | 26 +++++++++------------- libsolidity/formal/CHC.h | 2 +- libsolidity/formal/CHCSmtLib2Interface.cpp | 2 +- libsolidity/formal/CHCSmtLib2Interface.h | 5 ++--- libsolidity/formal/EncodingContext.h | 6 ++--- libsolidity/formal/Z3CHCInterface.cpp | 2 +- libsolidity/formal/Z3CHCInterface.h | 4 ++-- 9 files changed, 25 insertions(+), 34 deletions(-) diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index dc1be1035..f8fa347f0 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -35,8 +35,8 @@ BMC::BMC( smt::SMTSolverChoice _enabledSolvers ): SMTEncoder(_context), - m_outerErrorReporter(_errorReporter), - m_interface(make_shared(_smtlib2Responses, _smtCallback, _enabledSolvers)) + m_interface(make_unique(_smtlib2Responses, _smtCallback, _enabledSolvers)), + m_outerErrorReporter(_errorReporter) { #if defined (HAVE_Z3) || defined (HAVE_CVC4) if (_enabledSolvers.some()) @@ -55,7 +55,7 @@ void BMC::analyze(SourceUnit const& _source, set _safeAsserti solAssert(_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker), ""); m_safeAssertions += move(_safeAssertions); - m_context.setSolver(m_interface); + m_context.setSolver(m_interface.get()); m_context.clear(); m_context.setAssertionAccumulation(true); m_variableUsage.setFunctionInlining(true); diff --git a/libsolidity/formal/BMC.h b/libsolidity/formal/BMC.h index 473b5dfee..972ee88ce 100644 --- a/libsolidity/formal/BMC.h +++ b/libsolidity/formal/BMC.h @@ -71,8 +71,6 @@ public: /// @returns true if _funCall should be inlined, otherwise false. static bool shouldInlineFunctionCall(FunctionCall const& _funCall); - std::shared_ptr solver() { return m_interface; } - private: /// AST visitors. /// Only nodes that lead to verification targets being built @@ -172,6 +170,8 @@ private: smt::CheckResult checkSatisfiable(); //@} + std::unique_ptr m_interface; + /// Flags used for better warning messages. bool m_loopExecutionHappened = false; bool m_externalFunctionCallHappened = false; @@ -183,8 +183,6 @@ private: /// Assertions that are known to be safe. std::set m_safeAssertions; - - std::shared_ptr m_interface; }; } diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index e911ce8d4..bc4e355f5 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -37,24 +37,18 @@ CHC::CHC( ErrorReporter& _errorReporter, map const& _smtlib2Responses, ReadCallback::Callback const& _smtCallback, - smt::SMTSolverChoice _enabledSolvers + [[maybe_unused]] smt::SMTSolverChoice _enabledSolvers ): SMTEncoder(_context), -#ifdef HAVE_Z3 - m_interface( - _enabledSolvers.z3 ? - dynamic_pointer_cast(make_shared()) : - dynamic_pointer_cast(make_shared(_smtlib2Responses, _smtCallback)) - ), -#else - m_interface(make_shared(_smtlib2Responses, _smtCallback)), -#endif m_outerErrorReporter(_errorReporter), m_enabledSolvers(_enabledSolvers) { - (void)_smtlib2Responses; - (void)_enabledSolvers; - (void)_smtCallback; +#ifdef HAVE_Z3 + if (_enabledSolvers.z3) + m_interface = make_unique(); +#endif + if (!m_interface) + m_interface = make_unique(_smtlib2Responses, _smtCallback); } void CHC::analyze(SourceUnit const& _source) @@ -66,14 +60,14 @@ void CHC::analyze(SourceUnit const& _source) usesZ3 = m_enabledSolvers.z3; if (usesZ3) { - auto z3Interface = dynamic_pointer_cast(m_interface); + auto z3Interface = dynamic_cast(m_interface.get()); solAssert(z3Interface, ""); m_context.setSolver(z3Interface->z3Interface()); } #endif if (!usesZ3) { - auto smtlib2Interface = dynamic_pointer_cast(m_interface); + auto smtlib2Interface = dynamic_cast(m_interface.get()); solAssert(smtlib2Interface, ""); m_context.setSolver(smtlib2Interface->smtlib2Interface()); } @@ -95,7 +89,7 @@ void CHC::analyze(SourceUnit const& _source) vector CHC::unhandledQueries() const { - if (auto smtlib2 = dynamic_pointer_cast(m_interface)) + if (auto smtlib2 = dynamic_cast(m_interface.get())) return smtlib2->unhandledQueries(); return {}; diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index 664ae98bc..6e281d5ef 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -207,7 +207,7 @@ private: //@} /// CHC solver. - std::shared_ptr m_interface; + std::unique_ptr m_interface; /// ErrorReporter that comes from CompilerStack. langutil::ErrorReporter& m_outerErrorReporter; diff --git a/libsolidity/formal/CHCSmtLib2Interface.cpp b/libsolidity/formal/CHCSmtLib2Interface.cpp index ceb12bbac..11aa87608 100644 --- a/libsolidity/formal/CHCSmtLib2Interface.cpp +++ b/libsolidity/formal/CHCSmtLib2Interface.cpp @@ -38,7 +38,7 @@ CHCSmtLib2Interface::CHCSmtLib2Interface( map const& _queryResponses, ReadCallback::Callback const& _smtCallback ): - m_smtlib2(make_shared(_queryResponses, _smtCallback)), + m_smtlib2(make_unique(_queryResponses, _smtCallback)), m_queryResponses(_queryResponses), m_smtCallback(_smtCallback) { diff --git a/libsolidity/formal/CHCSmtLib2Interface.h b/libsolidity/formal/CHCSmtLib2Interface.h index 8aebdd8b2..24e69a15d 100644 --- a/libsolidity/formal/CHCSmtLib2Interface.h +++ b/libsolidity/formal/CHCSmtLib2Interface.h @@ -52,7 +52,7 @@ public: std::vector unhandledQueries() const { return m_unhandledQueries; } - std::shared_ptr smtlib2Interface() { return m_smtlib2; } + SMTLib2Interface* smtlib2Interface() const { return m_smtlib2.get(); } private: void declareFunction(std::string const& _name, SortPointer const& _sort); @@ -63,8 +63,7 @@ private: std::string querySolver(std::string const& _input); /// Used to access toSmtLibSort, SExpr, and handle variables. - /// Needs to be a shared_ptr since it's also passed to EncodingContext. - std::shared_ptr m_smtlib2; + std::unique_ptr m_smtlib2; std::string m_accumulatedOutput; std::set m_variables; diff --git a/libsolidity/formal/EncodingContext.h b/libsolidity/formal/EncodingContext.h index 4e1e15658..f2c9d0e31 100644 --- a/libsolidity/formal/EncodingContext.h +++ b/libsolidity/formal/EncodingContext.h @@ -48,7 +48,7 @@ public: /// Sets the current solver used by the current engine for /// SMT variable declaration. - void setSolver(std::shared_ptr _solver) + void setSolver(SolverInterface* _solver) { solAssert(_solver, ""); m_solver = _solver; @@ -144,7 +144,7 @@ public: void pushSolver(); void popSolver(); void addAssertion(Expression const& _e); - std::shared_ptr solver() + SolverInterface* solver() { solAssert(m_solver, ""); return m_solver; @@ -177,7 +177,7 @@ private: /// Solver related. //@{ /// Solver can be SMT solver or Horn solver in the future. - std::shared_ptr m_solver; + SolverInterface* m_solver = nullptr; /// Assertion stack. std::vector m_assertions; diff --git a/libsolidity/formal/Z3CHCInterface.cpp b/libsolidity/formal/Z3CHCInterface.cpp index d4c53f850..017fb1a58 100644 --- a/libsolidity/formal/Z3CHCInterface.cpp +++ b/libsolidity/formal/Z3CHCInterface.cpp @@ -25,7 +25,7 @@ using namespace dev; using namespace dev::solidity::smt; Z3CHCInterface::Z3CHCInterface(): - m_z3Interface(make_shared()), + m_z3Interface(make_unique()), m_context(m_z3Interface->context()), m_solver(*m_context) { diff --git a/libsolidity/formal/Z3CHCInterface.h b/libsolidity/formal/Z3CHCInterface.h index 858e4f40f..20373c244 100644 --- a/libsolidity/formal/Z3CHCInterface.h +++ b/libsolidity/formal/Z3CHCInterface.h @@ -45,11 +45,11 @@ public: std::pair> query(Expression const& _expr) override; - std::shared_ptr z3Interface() { return m_z3Interface; } + Z3Interface* z3Interface() const { return m_z3Interface.get(); } private: // Used to handle variables. - std::shared_ptr m_z3Interface; + std::unique_ptr m_z3Interface; z3::context* m_context; // Horn solver.