Merge pull request #12969 from ethereum/smt_eld

[SMTChecker] Add Eldarica as a Horn solver

Author: Leo

Changelog.md

@@ -13,6 +13,8 @@ Compiler Features:
  * Yul Optimizer: Allow replacing the previously hard-coded cleanup sequence by specifying custom steps after a colon delimiter (``:``) in the sequence string.
  * Language Server: Add basic document hover support.
  * Optimizer: Added optimization rule ``and(shl(X, Y), shl(X, Z)) => shl(X, and(Y, Z))``.
+ * SMTChecker: Support Eldarica as a Horn solver for the CHC engine when using the CLI option ``--model-checker-solvers eld``. The binary `eld` must be available in the system.
+ * SMTChecker: Make ``z3`` the default solver for the BMC and CHC engines instead of all solvers.
 
 
 Bugfixes:

docs/smtchecker.rst

@@ -614,19 +614,19 @@ which is primarily an SMT solver and makes `Spacer
 <https://github.com/uuverifiers/eldarica>`_ which does both.
 
 The user can choose which solvers should be used, if available, via the CLI
-option ``--model-checker-solvers {all,cvc4,smtlib2,z3}`` or the JSON option
+option ``--model-checker-solvers {all,cvc4,eld,smtlib2,z3}`` or the JSON option
 ``settings.modelChecker.solvers=[smtlib2,z3]``, where:
 
 - ``cvc4`` is only available if the ``solc`` binary is compiled with it. Only BMC uses ``cvc4``.
+- ``eld`` is used via its binary which must be installed in the system. Only CHC uses ``eld``, and only if ``z3`` is not enabled.
 - ``smtlib2`` outputs SMT/Horn queries in the `smtlib2 <http://smtlib.cs.uiowa.edu/>`_ format.
   These can be used together with the compiler's `callback mechanism <https://github.com/ethereum/solc-js>`_ so that
   any solver binary from the system can be employed to synchronously return the results of the queries to the compiler.
-  This is currently the only way to use Eldarica, for example, since it does not have a C++ API.
   This can be used by both BMC and CHC depending on which solvers are called.
 - ``z3`` is available
 
   - if ``solc`` is compiled with it;
-  - if a dynamic ``z3`` library of version 4.8.x is installed in a Linux system (from Solidity 0.7.6);
+  - if a dynamic ``z3`` library of version >=4.8.x is installed in a Linux system (from Solidity 0.7.6);
   - statically in ``soljson.js`` (from Solidity 0.6.9), that is, the Javascript binary of the compiler.
 
 .. note::

libsmtutil/CHCSmtLib2Interface.cpp

@@ -40,12 +40,14 @@ using namespace solidity::smtutil;
 CHCSmtLib2Interface::CHCSmtLib2Interface(
 	map<h256, string> const& _queryResponses,
 	ReadCallback::Callback _smtCallback,
+	SMTSolverChoice _enabledSolvers,
 	optional<unsigned> _queryTimeout
 ):
 	CHCSolverInterface(_queryTimeout),
 	m_smtlib2(make_unique<SMTLib2Interface>(_queryResponses, _smtCallback, m_queryTimeout)),
 	m_queryResponses(std::move(_queryResponses)),
-	m_smtCallback(_smtCallback)
+	m_smtCallback(_smtCallback),
+	m_enabledSolvers(_enabledSolvers)
 {
 	reset();
 }
@@ -203,12 +205,15 @@ string CHCSmtLib2Interface::querySolver(string const& _input)
 	util::h256 inputHash = util::keccak256(_input);
 	if (m_queryResponses.count(inputHash))
 		return m_queryResponses.at(inputHash);
+
+	smtAssert(m_enabledSolvers.smtlib2 || m_enabledSolvers.eld);
 	if (m_smtCallback)
 	{
 		auto result = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery), _input);
 		if (result.success)
 			return result.responseOrErrorMessage;
 	}
+
 	m_unhandledQueries.push_back(_input);
 	return "unknown\n";
 }

libsmtutil/CHCSmtLib2Interface.h

@@ -35,6 +35,7 @@ class CHCSmtLib2Interface: public CHCSolverInterface
 	explicit CHCSmtLib2Interface(
 		std::map<util::h256, std::string> const& _queryResponses = {},
 		frontend::ReadCallback::Callback _smtCallback = {},
+		SMTSolverChoice _enabledSolvers = SMTSolverChoice::All(),
 		std::optional<unsigned> _queryTimeout = {}
 	);
 
@@ -78,6 +79,7 @@ class CHCSmtLib2Interface: public CHCSolverInterface
 	std::vector<std::string> m_unhandledQueries;
 
 	frontend::ReadCallback::Callback m_smtCallback;
+	SMTSolverChoice m_enabledSolvers;
 
 	std::map<Sort const*, std::string> m_sortNames;
 };

libsmtutil/SolverInterface.h

@@ -42,35 +42,31 @@ namespace solidity::smtutil
 struct SMTSolverChoice
 {
 	bool cvc4 = false;
+	bool eld = false;
 	bool smtlib2 = false;
 	bool z3 = false;
 
-	static constexpr SMTSolverChoice All() noexcept { return {true, true, true}; }
-	static constexpr SMTSolverChoice CVC4() noexcept { return {true, false, false}; }
-	static constexpr SMTSolverChoice SMTLIB2() noexcept { return {false, true, false}; }
-	static constexpr SMTSolverChoice Z3() noexcept { return {false, false, true}; }
-	static constexpr SMTSolverChoice None() noexcept { return {false, false, false}; }
+	static constexpr SMTSolverChoice All() noexcept { return {true, true, true, true}; }
+	static constexpr SMTSolverChoice CVC4() noexcept { return {true, false, false, false}; }
+	static constexpr SMTSolverChoice ELD() noexcept { return {false, true, false, false}; }
+	static constexpr SMTSolverChoice SMTLIB2() noexcept { return {false, false, true, false}; }
+	static constexpr SMTSolverChoice Z3() noexcept { return {false, false, false, true}; }
+	static constexpr SMTSolverChoice None() noexcept { return {false, false, false, false}; }
 
 	static std::optional<SMTSolverChoice> fromString(std::string const& _solvers)
 	{
 		SMTSolverChoice solvers;
-		if (_solvers == "all")
-		{
-			smtAssert(solvers.setSolver("cvc4"), "");
-			smtAssert(solvers.setSolver("smtlib2"), "");
-			smtAssert(solvers.setSolver("z3"), "");
-		}
-		else
-			for (auto&& s: _solvers | ranges::views::split(',') | ranges::to<std::vector<std::string>>())
-				if (!solvers.setSolver(s))
-					return {};
+		for (auto&& s: _solvers | ranges::views::split(',') | ranges::to<std::vector<std::string>>())
+			if (!solvers.setSolver(s))
+				return {};
 
 		return solvers;
 	}
 
 	SMTSolverChoice& operator&=(SMTSolverChoice const& _other)
 	{
 		cvc4 &= _other.cvc4;
+		eld &= _other.eld;
 		smtlib2 &= _other.smtlib2;
 		z3 &= _other.z3;
 		return *this;
@@ -87,17 +83,20 @@ struct SMTSolverChoice
 	bool operator==(SMTSolverChoice const& _other) const noexcept
 	{
 		return cvc4 == _other.cvc4 &&
+			eld == _other.eld &&
 			smtlib2 == _other.smtlib2 &&
 			z3 == _other.z3;
 	}
 
 	bool setSolver(std::string const& _solver)
 	{
-		static std::set<std::string> const solvers{"cvc4", "smtlib2", "z3"};
+		static std::set<std::string> const solvers{"cvc4", "eld", "smtlib2", "z3"};
 		if (!solvers.count(_solver))
 			return false;
 		if (_solver == "cvc4")
 			cvc4 = true;
+		if (_solver == "eld")
+			eld = true;
 		else if (_solver == "smtlib2")
 			smtlib2 = true;
 		else if (_solver == "z3")
@@ -106,8 +105,8 @@ struct SMTSolverChoice
 	}
 
 	bool none() const noexcept { return !some(); }
-	bool some() const noexcept { return cvc4 || smtlib2 || z3; }
-	bool all() const noexcept { return cvc4 && smtlib2 && z3; }
+	bool some() const noexcept { return cvc4 || eld || smtlib2 || z3; }
+	bool all() const noexcept { return cvc4 && eld && smtlib2 && z3; }
 };
 
 enum class CheckResult

libsolidity/CMakeLists.txt

@@ -149,10 +149,13 @@ set(sources
 	interface/Natspec.h
 	interface/OptimiserSettings.h
 	interface/ReadFile.h
+	interface/SMTSolverCommand.cpp
+	interface/SMTSolverCommand.h
 	interface/StandardCompiler.cpp
 	interface/StandardCompiler.h
 	interface/StorageLayout.cpp
 	interface/StorageLayout.h
+	interface/UniversalCallback.h
 	interface/Version.cpp
 	interface/Version.h
 	lsp/DocumentHoverHandler.cpp
@@ -181,5 +184,5 @@ set(sources
 )
 
 add_library(solidity ${sources})
-target_link_libraries(solidity PUBLIC yul evmasm langutil smtutil solutil Boost::boost fmt::fmt-header-only)
+target_link_libraries(solidity PUBLIC yul evmasm langutil smtutil solutil Boost::boost fmt::fmt-header-only Threads::Threads)
 

libsolidity/formal/BMC.cpp

@@ -18,6 +18,7 @@
 
 #include <libsolidity/formal/BMC.h>
 
+#include <libsolidity/formal/ModelChecker.h>
 #include <libsolidity/formal/SymbolicTypes.h>
 
 #include <libsmtutil/SMTPortfolio.h>
@@ -40,7 +41,7 @@ BMC::BMC(
 	UniqueErrorReporter& _errorReporter,
 	map<h256, string> const& _smtlib2Responses,
 	ReadCallback::Callback const& _smtCallback,
-	ModelCheckerSettings const& _settings,
+	ModelCheckerSettings _settings,
 	CharStreamProvider const& _charStreamProvider
 ):
 	SMTEncoder(_context, _settings, _errorReporter, _charStreamProvider),
@@ -61,15 +62,14 @@ BMC::BMC(
 
 void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<VerificationTargetType>, smt::EncodingContext::IdCompare> _solvedTargets)
 {
-	if (m_interface->solvers() == 0)
+	// At this point every enabled solver is available.
+	if (!m_settings.solvers.cvc4 && !m_settings.solvers.smtlib2 && !m_settings.solvers.z3)
 	{
 		m_errorReporter.warning(
 			7710_error,
 			SourceLocation(),
 			"BMC analysis was not possible since no SMT solver was found and enabled."
-#ifdef HAVE_Z3_DLOPEN
-			" Install libz3.so." + to_string(Z3_MAJOR_VERSION) + "." + to_string(Z3_MINOR_VERSION) + " to enable Z3."
-#endif
+			" The accepted solvers for BMC are cvc4 and z3."
 		);
 		return;
 	}

libsolidity/formal/BMC.h

@@ -62,7 +62,7 @@ class BMC: public SMTEncoder
 		langutil::UniqueErrorReporter& _errorReporter,
 		std::map<h256, std::string> const& _smtlib2Responses,
 		ReadCallback::Callback const& _smtCallback,
-		ModelCheckerSettings const& _settings,
+		ModelCheckerSettings _settings,
 		langutil::CharStreamProvider const& _charStreamProvider
 	);
 

libsolidity/formal/CHC.cpp

@@ -18,6 +18,8 @@
 
 #include <libsolidity/formal/CHC.h>
 
+#include <libsolidity/formal/ModelChecker.h>
+
 #ifdef HAVE_Z3
 #include <libsmtutil/Z3CHCInterface.h>
 #endif
@@ -62,7 +64,7 @@ CHC::CHC(
 	UniqueErrorReporter& _errorReporter,
 	map<util::h256, string> const& _smtlib2Responses,
 	ReadCallback::Callback const& _smtCallback,
-	ModelCheckerSettings const& _settings,
+	ModelCheckerSettings _settings,
 	CharStreamProvider const& _charStreamProvider
 ):
 	SMTEncoder(_context, _settings, _errorReporter, _charStreamProvider),
@@ -73,31 +75,29 @@ CHC::CHC(
 
 void CHC::analyze(SourceUnit const& _source)
 {
-	if (!shouldAnalyze(_source))
-		return;
-
-	bool usesZ3 = m_settings.solvers.z3;
-#ifdef HAVE_Z3_DLOPEN
-	if (m_settings.solvers.z3 && !Z3Interface::available())
+	// At this point every enabled solver is available.
+	if (!m_settings.solvers.eld && !m_settings.solvers.smtlib2 && !m_settings.solvers.z3)
 	{
-		usesZ3 = false;
 		m_errorReporter.warning(
-			8158_error,
+			7649_error,
 			SourceLocation(),
-			"z3 was selected as a Horn solver for CHC analysis but libz3.so." + to_string(Z3_MAJOR_VERSION) + "." + to_string(Z3_MINOR_VERSION) + " was not found."
+			"CHC analysis was not possible since no Horn solver was found and enabled."
+			" The accepted solvers for CHC are Eldarica and z3."
 		);
+		return;
 	}
-#endif
 
-	if (!usesZ3 && !m_settings.solvers.smtlib2)
-	{
+	if (m_settings.solvers.eld && m_settings.solvers.z3)
 		m_errorReporter.warning(
-			7649_error,
+			5798_error,
 			SourceLocation(),
-			"CHC analysis was not possible since no Horn solver was found and enabled."
+			"Multiple Horn solvers were selected for CHC."
+			" CHC only supports one solver at a time, therefore only z3 will be used."
+			" If you wish to use Eldarica, please enable Eldarica only."
 		);
+
+	if (!shouldAnalyze(_source))
 		return;
-	}
 
 	resetSourceAnalysis();
 
@@ -115,7 +115,8 @@ void CHC::analyze(SourceUnit const& _source)
 
 	bool ranSolver = true;
 	// If ranSolver is true here it's because an SMT solver callback was
-	// actually given and the queries were solved.
+	// actually given and the queries were solved,
+	// or Eldarica was chosen and was present in the system.
 	if (auto const* smtLibInterface = dynamic_cast<CHCSmtLib2Interface const*>(m_interface.get()))
 		ranSolver = smtLibInterface->unhandledQueries().empty();
 	if (!ranSolver)
@@ -994,24 +995,27 @@ void CHC::resetSourceAnalysis()
 	ArraySlicePredicate::reset();
 	m_blockCounter = 0;
 
-	bool usesZ3 = false;
-#ifdef HAVE_Z3
-	usesZ3 = m_settings.solvers.z3 && Z3Interface::available();
-	if (usesZ3)
+	// At this point every enabled solver is available.
+	// If more than one Horn solver is selected we go with z3.
+	// We still need the ifdef because of Z3CHCInterface.
+	if (m_settings.solvers.z3)
 	{
-		/// z3::fixedpoint does not have a reset mechanism, so we need to create another.
+#ifdef HAVE_Z3
+		// z3::fixedpoint does not have a reset mechanism, so we need to create another.
 		m_interface = std::make_unique<Z3CHCInterface>(m_settings.timeout);
 		auto z3Interface = dynamic_cast<Z3CHCInterface const*>(m_interface.get());
 		solAssert(z3Interface, "");
 		m_context.setSolver(z3Interface->z3Interface());
-	}
+#else
+		solAssert(false);
 #endif
-	if (!usesZ3)
+	}
+	if (!m_settings.solvers.z3)
 	{
-		solAssert(m_settings.solvers.smtlib2);
+		solAssert(m_settings.solvers.smtlib2 || m_settings.solvers.eld);
 
 		if (!m_interface)
-			m_interface = make_unique<CHCSmtLib2Interface>(m_smtlib2Responses, m_smtCallback, m_settings.timeout);
+			m_interface = make_unique<CHCSmtLib2Interface>(m_smtlib2Responses, m_smtCallback, m_settings.solvers, m_settings.timeout);
 
 		auto smtlib2Interface = dynamic_cast<CHCSmtLib2Interface*>(m_interface.get());
 		solAssert(smtlib2Interface, "");
@@ -1551,9 +1555,10 @@ tuple<CheckResult, smtutil::Expression, CHCSolverInterface::CexGraph> CHC::query
 	{
 	case CheckResult::SATISFIABLE:
 	{
-#ifdef HAVE_Z3
+	// We still need the ifdef because of Z3CHCInterface.
 		if (m_settings.solvers.z3)
 		{
+#ifdef HAVE_Z3
 			// Even though the problem is SAT, Spacer's pre processing makes counterexamples incomplete.
 			// We now disable those optimizations and check whether we can still solve the problem.
 			auto* spacer = dynamic_cast<Z3CHCInterface*>(m_interface.get());
@@ -1569,8 +1574,10 @@ tuple<CheckResult, smtutil::Expression, CHCSolverInterface::CexGraph> CHC::query
 				cex = std::move(cexNoOpt);
 
 			spacer->setSpacerOptions(true);
-		}
+#else
+			solAssert(false);
 #endif
+		}
 		break;
 	}
 	case CheckResult::UNSATISFIABLE:

libsolidity/formal/CHC.h

@@ -59,7 +59,7 @@ class CHC: public SMTEncoder
 		langutil::UniqueErrorReporter& _errorReporter,
 		std::map<util::h256, std::string> const& _smtlib2Responses,
 		ReadCallback::Callback const& _smtCallback,
-		ModelCheckerSettings const& _settings,
+		ModelCheckerSettings _settings,
 		langutil::CharStreamProvider const& _charStreamProvider
 	);