SMTChecker: Allow using multiple external solvers in one analysis

We are using SMTCommand inside UniversalCallback to call external
solvers on queries produced my our engines.

Previous mechanism set the external solver once during initialization
and it was not possible to change it later. This meant, that it would
not be possible to use, e.g., Eldarica and cvc5 at the same time.

Here we move the proper setup for SMTCommand just before we call it.
This setup is customized by subclasses of (CHC)SmtLib2Interface, which
call corresponding external solvers.

libsmtutil/CHCSmtLib2Interface.cpp

@@ -43,16 +43,14 @@ using namespace solidity::frontend;
 using namespace solidity::smtutil;
 
 CHCSmtLib2Interface::CHCSmtLib2Interface(
-	std::map<h256, std::string> const& _queryResponses,
+	std::map<h256, std::string> _queryResponses,
 	ReadCallback::Callback _smtCallback,
-	SMTSolverChoice _enabledSolvers,
 	std::optional<unsigned> _queryTimeout
 ):
 	CHCSolverInterface(_queryTimeout),
 	m_smtlib2(std::make_unique<SMTLib2Interface>(_queryResponses, _smtCallback, m_queryTimeout)),
 	m_queryResponses(std::move(_queryResponses)),
-	m_smtCallback(_smtCallback),
-	m_enabledSolvers(_enabledSolvers)
+	m_smtCallback(_smtCallback)
 {
 	reset();
 }
@@ -186,9 +184,9 @@ std::string CHCSmtLib2Interface::querySolver(std::string const& _input)
 	if (m_queryResponses.count(inputHash))
 		return m_queryResponses.at(inputHash);
 
-	smtAssert(m_enabledSolvers.smtlib2 || m_enabledSolvers.eld);
 	if (m_smtCallback)
 	{
+		setupSmtCallback();
 		auto result = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery), _input);
 		if (result.success)
 			return result.responseOrErrorMessage;

libsmtutil/CHCSmtLib2Interface.h

@@ -33,9 +33,8 @@ class CHCSmtLib2Interface: public CHCSolverInterface
 {
 public:
 	explicit CHCSmtLib2Interface(
-		std::map<util::h256, std::string> const& _queryResponses = {},
+		std::map<util::h256, std::string> _queryResponses = {},
 		frontend::ReadCallback::Callback _smtCallback = {},
-		SMTSolverChoice _enabledSolvers = SMTSolverChoice::All(),
 		std::optional<unsigned> _queryTimeout = {}
 	);
 
@@ -59,7 +58,7 @@ class CHCSmtLib2Interface: public CHCSolverInterface
 
 	auto const& sortNames() const { return m_smtlib2->sortNames(); }
 
-private:
+protected:
 	std::string toSmtLibSort(SortPointer _sort);
 	std::string toSmtLibSort(std::vector<SortPointer> const& _sort);
 
@@ -79,17 +78,19 @@ class CHCSmtLib2Interface: public CHCSolverInterface
 	/// Translates CHC solver response with a model to our representation of invariants. Returns None on error.
 	std::optional<smtutil::Expression> invariantsFromSolverResponse(std::string const& response) const;
 
+	/// Hook to setup external solver call
+	virtual void setupSmtCallback() {}
+
 	/// Used to access toSmtLibSort, SExpr, and handle variables.
 	std::unique_ptr<SMTLib2Interface> m_smtlib2;
 
 	std::string m_accumulatedOutput;
 	std::set<std::string> m_variables;
 
-	std::map<util::h256, std::string> const& m_queryResponses;
+	std::map<util::h256, std::string> m_queryResponses;
 	std::vector<std::string> m_unhandledQueries;
 
 	frontend::ReadCallback::Callback m_smtCallback;
-	SMTSolverChoice m_enabledSolvers;
 };
 
 }

libsmtutil/SMTLib2Interface.cpp

@@ -322,6 +322,7 @@ std::string SMTLib2Interface::querySolver(std::string const& _input)
 		return m_queryResponses.at(inputHash);
 	if (m_smtCallback)
 	{
+		setupSmtCallback();
 		auto result = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery), _input);
 		if (result.success)
 			return result.responseOrErrorMessage;

libsmtutil/SMTLib2Interface.h

@@ -71,7 +71,9 @@ class SMTLib2Interface: public SolverInterface
 
 	std::string dumpQuery(std::vector<Expression> const& _expressionsToEvaluate);
 
-private:
+protected:
+	virtual void setupSmtCallback() {}
+
 	void declareFunction(std::string const& _name, SortPointer const& _sort);
 
 	void write(std::string _data);

libsmtutil/SMTPortfolio.cpp

@@ -18,9 +18,6 @@
 
 #include <libsmtutil/SMTPortfolio.h>
 
-#ifdef HAVE_Z3
-#include <libsmtutil/Z3Interface.h>
-#endif
 #include <libsmtutil/SMTLib2Interface.h>
 
 using namespace solidity;
@@ -29,22 +26,12 @@ using namespace solidity::frontend;
 using namespace solidity::smtutil;
 
 SMTPortfolio::SMTPortfolio(
-	std::map<h256, std::string> _smtlib2Responses,
-	frontend::ReadCallback::Callback _smtCallback,
-	[[maybe_unused]] SMTSolverChoice _enabledSolvers,
-	std::optional<unsigned> _queryTimeout,
-	bool _printQuery
+	std::vector<std::unique_ptr<SolverInterface>> _solvers,
+	std::optional<unsigned> _queryTimeout
 ):
-	SolverInterface(_queryTimeout)
-{
-	solAssert(!_printQuery || _enabledSolvers == smtutil::SMTSolverChoice::SMTLIB2(), "Only SMTLib2 solver can be enabled to print queries");
-	if (_enabledSolvers.smtlib2 || _enabledSolvers.cvc5)
-		m_solvers.emplace_back(std::make_unique<SMTLib2Interface>(std::move(_smtlib2Responses), std::move(_smtCallback), m_queryTimeout));
-#ifdef HAVE_Z3
-	if (_enabledSolvers.z3 && Z3Interface::available())
-		m_solvers.emplace_back(std::make_unique<Z3Interface>(m_queryTimeout));
-#endif
-}
+	SolverInterface(_queryTimeout), m_solvers(std::move(_solvers))
+{}
+
 
 void SMTPortfolio::reset()
 {

libsmtutil/SMTPortfolio.h

@@ -42,13 +42,7 @@ class SMTPortfolio: public SolverInterface
 	SMTPortfolio(SMTPortfolio const&) = delete;
 	SMTPortfolio& operator=(SMTPortfolio const&) = delete;
 
-	SMTPortfolio(
-		std::map<util::h256, std::string> _smtlib2Responses = {},
-		frontend::ReadCallback::Callback _smtCallback = {},
-		SMTSolverChoice _enabledSolvers = SMTSolverChoice::All(),
-		std::optional<unsigned> _queryTimeout = {},
-		bool _printQuery = false
-	);
+	SMTPortfolio(std::vector<std::unique_ptr<SolverInterface>> solvers, std::optional<unsigned> _queryTimeout);
 
 	void reset() override;
 

libsolidity/CMakeLists.txt

@@ -109,6 +109,10 @@ set(sources
 	formal/BMC.h
 	formal/CHC.cpp
 	formal/CHC.h
+	formal/Cvc5SMTLib2Interface.cpp
+	formal/Cvc5SMTLib2Interface.h
+	formal/EldaricaCHCSmtLib2Interface.cpp
+	formal/EldaricaCHCSmtLib2Interface.h
 	formal/EncodingContext.cpp
 	formal/EncodingContext.h
 	formal/ExpressionFormatter.cpp

libsolidity/formal/BMC.cpp

@@ -18,9 +18,14 @@
 
 #include <libsolidity/formal/BMC.h>
 
+#include <libsolidity/formal/Cvc5SMTLib2Interface.h>
 #include <libsolidity/formal/SymbolicTypes.h>
 
+#include <libsmtutil/SMTLib2Interface.h>
 #include <libsmtutil/SMTPortfolio.h>
+#ifdef HAVE_Z3
+#include <libsmtutil/Z3Interface.h>
+#endif
 
 #include <liblangutil/CharStream.h>
 #include <liblangutil/CharStreamProvider.h>
@@ -35,6 +40,8 @@ using namespace solidity;
 using namespace solidity::util;
 using namespace solidity::langutil;
 using namespace solidity::frontend;
+using namespace solidity::frontend::smt;
+using namespace solidity::smtutil;
 
 BMC::BMC(
 	smt::EncodingContext& _context,
@@ -45,12 +52,19 @@ BMC::BMC(
 	ModelCheckerSettings _settings,
 	CharStreamProvider const& _charStreamProvider
 ):
-	SMTEncoder(_context, _settings, _errorReporter, _unsupportedErrorReporter, _charStreamProvider),
-	m_interface(std::make_unique<smtutil::SMTPortfolio>(
-		_smtlib2Responses, _smtCallback, _settings.solvers, _settings.timeout, _settings.printQuery
-	))
+	SMTEncoder(_context, _settings, _errorReporter, _unsupportedErrorReporter, _charStreamProvider)
 {
-	solAssert(!_settings.printQuery || _settings.solvers == smtutil::SMTSolverChoice::SMTLIB2(), "Only SMTLib2 solver can be enabled to print queries");
+	solAssert(!_settings.printQuery || _settings.solvers == SMTSolverChoice::SMTLIB2(), "Only SMTLib2 solver can be enabled to print queries");
+	std::vector<std::unique_ptr<SolverInterface>> solvers;
+	if (_settings.solvers.smtlib2)
+		solvers.emplace_back(std::make_unique<SMTLib2Interface>(_smtlib2Responses, _smtCallback, _settings.timeout));
+	if (_settings.solvers.cvc5)
+		solvers.emplace_back(std::make_unique<Cvc5SMTLib2Interface>(_smtCallback, _settings.timeout));
+#ifdef HAVE_Z3
+	if (_settings.solvers.z3 && Z3Interface::available())
+		solvers.emplace_back(std::make_unique<Z3Interface>(_settings.timeout));
+#endif
+	m_interface = std::make_unique<SMTPortfolio>(std::move(solvers), _settings.timeout);
 #if defined (HAVE_Z3)
 	if (m_settings.solvers.z3)
 		if (!_smtlib2Responses.empty())

libsolidity/formal/CHC.cpp

@@ -25,6 +25,7 @@
 #endif
 
 #include <libsolidity/formal/ArraySlicePredicate.h>
+#include <libsolidity/formal/EldaricaCHCSmtLib2Interface.h>
 #include <libsolidity/formal/Invariants.h>
 #include <libsolidity/formal/PredicateInstance.h>
 #include <libsolidity/formal/PredicateSort.h>
@@ -1289,15 +1290,23 @@ void CHC::resetSourceAnalysis()
 		solAssert(false);
 #endif
 	}
-	if (!m_settings.solvers.z3)
+	else
 	{
 		solAssert(m_settings.solvers.smtlib2 || m_settings.solvers.eld);
-
 		if (!m_interface)
-			m_interface = std::make_unique<CHCSmtLib2Interface>(m_smtlib2Responses, m_smtCallback, m_settings.solvers, m_settings.timeout);
+		{
+			if (m_settings.solvers.eld)
+				m_interface = std::make_unique<EldaricaCHCSmtLib2Interface>(
+					m_smtCallback,
+					m_settings.timeout,
+					m_settings.invariants != ModelCheckerInvariants::None()
+				);
+			else
+				m_interface = std::make_unique<CHCSmtLib2Interface>(m_smtlib2Responses, m_smtCallback, m_settings.timeout);
+		}
 
 		auto smtlib2Interface = dynamic_cast<CHCSmtLib2Interface*>(m_interface.get());
-		solAssert(smtlib2Interface, "");
+		solAssert(smtlib2Interface);
 		smtlib2Interface->reset();
 		m_context.setSolver(smtlib2Interface->smtlib2Interface());
 	}

libsolidity/formal/Cvc5SMTLib2Interface.cpp

@@ -0,0 +1,35 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+#include <libsolidity/formal/Cvc5SMTLib2Interface.h>
+
+#include <libsolidity/interface/UniversalCallback.h>
+
+using namespace solidity::frontend::smt;
+
+Cvc5SMTLib2Interface::Cvc5SMTLib2Interface(
+	frontend::ReadCallback::Callback _smtCallback,
+	std::optional<unsigned int> _queryTimeout
+): SMTLib2Interface({}, std::move(_smtCallback), _queryTimeout)
+{
+}
+
+void Cvc5SMTLib2Interface::setupSmtCallback() {
+	if (auto* universalCallback = m_smtCallback.target<frontend::UniversalCallback>())
+		universalCallback->smtCommand().setCvc5(m_queryTimeout);
+}

libsolidity/formal/Cvc5SMTLib2Interface.h

@@ -0,0 +1,37 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+#pragma once
+
+#include <libsmtutil/SMTLib2Interface.h>
+
+namespace solidity::frontend::smt
+{
+
+class Cvc5SMTLib2Interface: public smtutil::SMTLib2Interface
+{
+public:
+	explicit Cvc5SMTLib2Interface(
+		frontend::ReadCallback::Callback _smtCallback = {},
+		std::optional<unsigned> _queryTimeout = {}
+	);
+private:
+	void setupSmtCallback() override;
+};
+
+}

libsolidity/formal/EldaricaCHCSmtLib2Interface.cpp

@@ -0,0 +1,37 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+#include <libsolidity/formal/EldaricaCHCSmtLib2Interface.h>
+
+#include <libsolidity/interface/UniversalCallback.h>
+
+using namespace solidity::frontend::smt;
+
+EldaricaCHCSmtLib2Interface::EldaricaCHCSmtLib2Interface(
+	frontend::ReadCallback::Callback _smtCallback,
+	std::optional<unsigned int> _queryTimeout,
+	bool computeInvariants
+): CHCSmtLib2Interface({}, std::move(_smtCallback), _queryTimeout), m_computeInvariants(computeInvariants)
+{
+}
+
+void EldaricaCHCSmtLib2Interface::setupSmtCallback()
+{
+	if (auto* universalCallback = m_smtCallback.target<frontend::UniversalCallback>())
+		universalCallback->smtCommand().setEldarica(m_queryTimeout, m_computeInvariants);
+}

libsolidity/formal/EldaricaCHCSmtLib2Interface.h

@@ -0,0 +1,41 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+#pragma once
+
+#include <libsmtutil/CHCSmtLib2Interface.h>
+
+namespace solidity::frontend::smt
+{
+
+class EldaricaCHCSmtLib2Interface: public smtutil::CHCSmtLib2Interface
+{
+public:
+	EldaricaCHCSmtLib2Interface(
+		frontend::ReadCallback::Callback _smtCallback,
+		std::optional<unsigned int> _queryTimeout,
+		bool computeInvariants
+	);
+
+private:
+	void setupSmtCallback() override;
+
+	bool m_computeInvariants;
+};
+
+}