cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge pull request #8098 from ethereum/smt_fix_shared_ptr

Browse Source 
[SMTChecker] Replace some shared_ptr by unique_ptr/raw
This commit is contained in:
Leonardo 2020-01-06 14:58:37 +01:00 committed by GitHub
commit f7624e254c
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
9 changed files with 25 additions and 34 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
libsolidity/formal/BMC.cpp
View File

@ -35,8 +35,8 @@ BMC::BMC(
smt::SMTSolverChoice _enabledSolvers
):
SMTEncoder(_context),
m_outerErrorReporter(_errorReporter),
m_interface(make_shared<smt::SMTPortfolio>(_smtlib2Responses, _smtCallback, _enabledSolvers))
m_interface(make_unique<smt::SMTPortfolio>(_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<Expression const*> _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);

6
libsolidity/formal/BMC.h
View File

@ -71,8 +71,6 @@ public:
/// @returns true if _funCall should be inlined, otherwise false.
static bool shouldInlineFunctionCall(FunctionCall const& _funCall);
std::shared_ptr<smt::SolverInterface> 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<smt::SolverInterface> 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<Expression const*> m_safeAssertions;
std::shared_ptr<smt::SolverInterface> m_interface;
};
}

26
libsolidity/formal/CHC.cpp
View File

@ -37,24 +37,18 @@ CHC::CHC(
ErrorReporter& _errorReporter,
map<h256, string> 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<smt::CHCSolverInterface>(make_shared<smt::Z3CHCInterface>()) :
dynamic_pointer_cast<smt::CHCSolverInterface>(make_shared<smt::CHCSmtLib2Interface>(_smtlib2Responses, _smtCallback))
),
#else
m_interface(make_shared<smt::CHCSmtLib2Interface>(_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<smt::Z3CHCInterface>();
#endif
if (!m_interface)
m_interface = make_unique<smt::CHCSmtLib2Interface>(_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<smt::Z3CHCInterface>(m_interface);
auto z3Interface = dynamic_cast<smt::Z3CHCInterface const*>(m_interface.get());
solAssert(z3Interface, "");
m_context.setSolver(z3Interface->z3Interface());
}
#endif
if (!usesZ3)
{
auto smtlib2Interface = dynamic_pointer_cast<smt::CHCSmtLib2Interface>(m_interface);
auto smtlib2Interface = dynamic_cast<smt::CHCSmtLib2Interface const*>(m_interface.get());
solAssert(smtlib2Interface, "");
m_context.setSolver(smtlib2Interface->smtlib2Interface());
}
@ -95,7 +89,7 @@ void CHC::analyze(SourceUnit const& _source)
vector<string> CHC::unhandledQueries() const
{
if (auto smtlib2 = dynamic_pointer_cast<smt::CHCSmtLib2Interface>(m_interface))
if (auto smtlib2 = dynamic_cast<smt::CHCSmtLib2Interface const*>(m_interface.get()))
return smtlib2->unhandledQueries();
return {};

2
libsolidity/formal/CHC.h
View File

@ -207,7 +207,7 @@ private:
//@}
/// CHC solver.
std::shared_ptr<smt::CHCSolverInterface> m_interface;
std::unique_ptr<smt::CHCSolverInterface> m_interface;
/// ErrorReporter that comes from CompilerStack.
langutil::ErrorReporter& m_outerErrorReporter;

2
libsolidity/formal/CHCSmtLib2Interface.cpp
View File

@ -38,7 +38,7 @@ CHCSmtLib2Interface::CHCSmtLib2Interface(
map<h256, string> const& _queryResponses,
ReadCallback::Callback const& _smtCallback
):
m_smtlib2(make_shared<SMTLib2Interface>(_queryResponses, _smtCallback)),
m_smtlib2(make_unique<SMTLib2Interface>(_queryResponses, _smtCallback)),
m_queryResponses(_queryResponses),
m_smtCallback(_smtCallback)
{

5
libsolidity/formal/CHCSmtLib2Interface.h
View File

@ -52,7 +52,7 @@ public:
std::vector<std::string> unhandledQueries() const { return m_unhandledQueries; }
std::shared_ptr<SMTLib2Interface> 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<SMTLib2Interface> m_smtlib2;
std::unique_ptr<SMTLib2Interface> m_smtlib2;
std::string m_accumulatedOutput;
std::set<std::string> m_variables;

6
libsolidity/formal/EncodingContext.h
View File

@ -48,7 +48,7 @@ public:
/// Sets the current solver used by the current engine for
/// SMT variable declaration.
void setSolver(std::shared_ptr<SolverInterface> _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<SolverInterface> 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<SolverInterface> m_solver;
SolverInterface* m_solver = nullptr;
/// Assertion stack.
std::vector<Expression> m_assertions;

2
libsolidity/formal/Z3CHCInterface.cpp
View File

@ -25,7 +25,7 @@ using namespace dev;
using namespace dev::solidity::smt;
Z3CHCInterface::Z3CHCInterface():
m_z3Interface(make_shared<Z3Interface>()),
m_z3Interface(make_unique<Z3Interface>()),
m_context(m_z3Interface->context()),
m_solver(*m_context)
{

4
libsolidity/formal/Z3CHCInterface.h
View File

@ -45,11 +45,11 @@ public:
std::pair<CheckResult, std::vector<std::string>> query(Expression const& _expr) override;
std::shared_ptr<Z3Interface> z3Interface() { return m_z3Interface; }
Z3Interface* z3Interface() const { return m_z3Interface.get(); }
private:
// Used to handle variables.
std::shared_ptr<Z3Interface> m_z3Interface;
std::unique_ptr<Z3Interface> m_z3Interface;
z3::context* m_context;
// Horn solver.