Merge pull request #6712 from ethereum/smt_unique_ptr

[SMTChecker] Use unique_ptr instead of shared_ptr where applicable

libsolidity/formal/SMTChecker.cpp

@@ -34,7 +34,7 @@ using namespace langutil;
 using namespace dev::solidity;
 
 SMTChecker::SMTChecker(ErrorReporter& _errorReporter, map<h256, string> const& _smtlib2Responses):
-	m_interface(make_shared<smt::SMTPortfolio>(_smtlib2Responses)),
+	m_interface(make_unique<smt::SMTPortfolio>(_smtlib2Responses)),
 	m_errorReporterReference(_errorReporter),
 	m_errorReporter(m_smtErrors),
 	m_context(*m_interface)
@@ -79,7 +79,7 @@ void SMTChecker::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _
 bool SMTChecker::visit(ContractDefinition const& _contract)
 {
 	for (auto const& contract: _contract.annotation().linearizedBaseContracts)
-		for (auto var : contract->stateVariables())
+		for (auto var: contract->stateVariables())
 			if (*contract == _contract || var->isVisibleInDerivedContracts())
 				createVariable(*var);
 	return true;

libsolidity/formal/SMTChecker.h

@@ -293,7 +293,7 @@ private:
 	/// @returns the VariableDeclaration referenced by an Identifier or nullptr.
 	VariableDeclaration const* identifierToVariable(Expression const& _expr);
 
-	std::shared_ptr<smt::SolverInterface> m_interface;
+	std::unique_ptr<smt::SolverInterface> m_interface;
 	VariableUsage m_variableUsage;
 	bool m_loopExecutionHappened = false;
 	bool m_arrayAssignmentHappened = false;

libsolidity/formal/SMTPortfolio.cpp

@@ -32,42 +32,42 @@ using namespace dev::solidity::smt;
 
 SMTPortfolio::SMTPortfolio(map<h256, string> const& _smtlib2Responses)
 {
-	m_solvers.emplace_back(make_shared<smt::SMTLib2Interface>(_smtlib2Responses));
+	m_solvers.emplace_back(make_unique<smt::SMTLib2Interface>(_smtlib2Responses));
 #ifdef HAVE_Z3
-	m_solvers.emplace_back(make_shared<smt::Z3Interface>());
+	m_solvers.emplace_back(make_unique<smt::Z3Interface>());
 #endif
 #ifdef HAVE_CVC4
-	m_solvers.emplace_back(make_shared<smt::CVC4Interface>());
+	m_solvers.emplace_back(make_unique<smt::CVC4Interface>());
 #endif
 }
 
 void SMTPortfolio::reset()
 {
-	for (auto s : m_solvers)
+	for (auto const& s: m_solvers)
 		s->reset();
 }
 
 void SMTPortfolio::push()
 {
-	for (auto s : m_solvers)
+	for (auto const& s: m_solvers)
 		s->push();
 }
 
 void SMTPortfolio::pop()
 {
-	for (auto s : m_solvers)
+	for (auto const& s: m_solvers)
 		s->pop();
 }
 
 void SMTPortfolio::declareVariable(string const& _name, Sort const& _sort)
 {
-	for (auto s : m_solvers)
+	for (auto const& s: m_solvers)
 		s->declareVariable(_name, _sort);
 }
 
 void SMTPortfolio::addAssertion(Expression const& _expr)
 {
-	for (auto s : m_solvers)
+	for (auto const& s: m_solvers)
 		s->addAssertion(_expr);
 }
 
@@ -105,7 +105,7 @@ pair<CheckResult, vector<string>> SMTPortfolio::check(vector<Expression> const&
 {
 	CheckResult lastResult = CheckResult::ERROR;
 	vector<string> finalValues;
-	for (auto s : m_solvers)
+	for (auto const& s: m_solvers)
 	{
 		CheckResult result;
 		vector<string> values;

libsolidity/formal/SMTPortfolio.h

@@ -59,7 +59,7 @@ public:
 private:
 	static bool solverAnswered(CheckResult result);
 
-	std::vector<std::shared_ptr<smt::SolverInterface>> m_solvers;
+	std::vector<std::unique_ptr<smt::SolverInterface>> m_solvers;
 };
 
 }

libsolidity/formal/SSAVariable.cpp

@@ -28,6 +28,5 @@ SSAVariable::SSAVariable()
 void SSAVariable::resetIndex()
 {
 	m_currentIndex = 0;
-	m_nextFreeIndex.reset (new unsigned);
-	*m_nextFreeIndex = 1;
+	m_nextFreeIndex = make_unique<unsigned>(1);
 }

libsolidity/formal/SSAVariable.h

@@ -44,9 +44,7 @@ public:
 
 private:
 	unsigned m_currentIndex;
-	/// The next free index is a shared pointer because we want
-	/// the copy and the copied to share it.
-	std::shared_ptr<unsigned> m_nextFreeIndex;
+	std::unique_ptr<unsigned> m_nextFreeIndex;
 };
 
 }

libsolidity/formal/SymbolicVariables.cpp

@@ -33,7 +33,7 @@ SymbolicVariable::SymbolicVariable(
 	m_type(move(_type)),
 	m_uniqueName(move(_uniqueName)),
 	m_interface(_interface),
-	m_ssa(make_shared<SSAVariable>())
+	m_ssa(make_unique<SSAVariable>())
 {
 	solAssert(m_type, "");
 	m_sort = smtSort(*m_type);
@@ -48,7 +48,7 @@ SymbolicVariable::SymbolicVariable(
 	m_sort(move(_sort)),
 	m_uniqueName(move(_uniqueName)),
 	m_interface(_interface),
-	m_ssa(make_shared<SSAVariable>())
+	m_ssa(make_unique<SSAVariable>())
 {
 	solAssert(m_sort, "");
 }

libsolidity/formal/SymbolicVariables.h

@@ -71,7 +71,7 @@ protected:
 	TypePointer m_type;
 	std::string m_uniqueName;
 	smt::SolverInterface& m_interface;
-	std::shared_ptr<SSAVariable> m_ssa;
+	std::unique_ptr<SSAVariable> m_ssa;
 };
 
 /**