Merge pull request #11421 from ethereum/smt_solver_option

[SMTChecker] Solver option

Author: Leonardo

.circleci/config.yml

@@ -811,7 +811,7 @@ jobs:
 
   t_ems_solcjs:
     docker:
-      - image: buildpack-deps:latest
+      - image: << pipeline.parameters.ubuntu-2004-docker-image >>
     environment:
       TERM: xterm
     steps:
@@ -822,7 +822,7 @@ jobs:
           name: Install test dependencies
           command: |
             apt-get update
-            apt-get install -qqy --no-install-recommends nodejs npm cvc4
+            apt-get install -qqy --no-install-recommends nodejs npm
       - run:
           name: Test solcjs
           no_output_timeout: 30m

docs/smtchecker.rst

@@ -558,6 +558,39 @@ calls assume the called code is unknown and can do anything.
 The CHC engine is much more powerful than BMC in terms of what it can prove,
 and might require more computing resources.
 
+SMT and Horn solvers
+====================
+
+The two engines detailed above use automated theorem provers as their logical
+backends.  BMC uses an SMT solver, whereas CHC uses a Horn solver. Often the
+same tool can act as both, as seen in `z3 <https://github.com/Z3Prover/z3>`_,
+which is primarily an SMT solver and makes `Spacer
+<https://spacer.bitbucket.io/>`_ available as a Horn solver, and `Eldarica
+<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
+``settings.modelChecker.solvers=[smtlib2,z3]``, where:
+
+- ``cvc4`` is only available if the ``solc`` binary is compiled with it. Only BMC uses ``cvc4``.
+- ``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);
+  - statically in ``soljson.js`` (from Solidity 0.6.9), that is, the Javascript binary of the compiler.
+
+Since both BMC and CHC use ``z3``, and ``z3`` is available in a greater variety
+of environments, including in the browser, most users will almost never need to be
+concerned about this option. More advanced users might apply this option to try
+alternative solvers on more complex problems.
+
+Please note that certain combinations of chosen engine and solver will lead to
+the SMTChecker doing nothing, for example choosing CHC and ``cvc4``.
 
 *******************************
 Abstraction and False Positives

libsmtutil/SMTPortfolio.cpp

@@ -40,7 +40,8 @@ SMTPortfolio::SMTPortfolio(
 ):
 	SolverInterface(_queryTimeout)
 {
-	m_solvers.emplace_back(make_unique<SMTLib2Interface>(move(_smtlib2Responses), move(_smtCallback), m_queryTimeout));
+	if (_enabledSolvers.smtlib2)
+		m_solvers.emplace_back(make_unique<SMTLib2Interface>(move(_smtlib2Responses), move(_smtCallback), m_queryTimeout));
 #ifdef HAVE_Z3
 	if (_enabledSolvers.z3 && Z3Interface::available())
 		m_solvers.emplace_back(make_unique<Z3Interface>(m_queryTimeout));
@@ -143,10 +144,11 @@ pair<CheckResult, vector<string>> SMTPortfolio::check(vector<Expression> const&
 vector<string> SMTPortfolio::unhandledQueries()
 {
 	// This code assumes that the constructor guarantees that
-	// SmtLib2Interface is in position 0.
-	smtAssert(!m_solvers.empty(), "");
-	smtAssert(dynamic_cast<SMTLib2Interface*>(m_solvers.front().get()), "");
-	return m_solvers.front()->unhandledQueries();
+	// SmtLib2Interface is in position 0, if enabled.
+	if (!m_solvers.empty())
+		if (auto smtlib2 = dynamic_cast<SMTLib2Interface*>(m_solvers.front().get()))
+			return smtlib2->unhandledQueries();
+	return {};
 }
 
 bool SMTPortfolio::solverAnswered(CheckResult result)

libsmtutil/SolverInterface.h

@@ -23,10 +23,13 @@
 
 #include <libsolutil/Common.h>
 
+#include <range/v3/view.hpp>
+
 #include <cstdio>
 #include <map>
 #include <memory>
 #include <optional>
+#include <set>
 #include <string>
 #include <vector>
 
@@ -36,16 +39,71 @@ namespace solidity::smtutil
 struct SMTSolverChoice
 {
 	bool cvc4 = false;
+	bool smtlib2 = false;
 	bool z3 = false;
 
-	static constexpr SMTSolverChoice All() { return {true, true}; }
-	static constexpr SMTSolverChoice CVC4() { return {true, false}; }
-	static constexpr SMTSolverChoice Z3() { return {false, true}; }
-	static constexpr SMTSolverChoice None() { return {false, false}; }
+	static constexpr SMTSolverChoice All() { return {true, true, true}; }
+	static constexpr SMTSolverChoice CVC4() { return {true, false, false}; }
+	static constexpr SMTSolverChoice SMTLIB2() { return {false, true, false}; }
+	static constexpr SMTSolverChoice Z3() { return {false, false, true}; }
+	static constexpr SMTSolverChoice None() { return {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 {};
+
+		return solvers;
+	}
+
+	SMTSolverChoice& operator&(SMTSolverChoice const& _other)
+	{
+		cvc4 &= _other.cvc4;
+		smtlib2 &= _other.smtlib2;
+		z3 &= _other.z3;
+		return *this;
+	}
+
+	SMTSolverChoice& operator&=(SMTSolverChoice const& _other)
+	{
+		return *this & _other;
+	}
+
+	bool operator!=(SMTSolverChoice const& _other) const noexcept { return !(*this == _other); }
+
+	bool operator==(SMTSolverChoice const& _other) const noexcept
+	{
+		return cvc4 == _other.cvc4 &&
+			smtlib2 == _other.smtlib2 &&
+			z3 == _other.z3;
+	}
+
+	bool setSolver(std::string const& _solver)
+	{
+		static std::set<std::string> const solvers{"cvc4", "smtlib2", "z3"};
+		if (!solvers.count(_solver))
+			return false;
+		if (_solver == "cvc4")
+			cvc4 = true;
+		else if (_solver == "smtlib2")
+			smtlib2 = true;
+		else if (_solver == "z3")
+			z3 = true;
+		return true;
+	}
 
 	bool none() { return !some(); }
-	bool some() { return cvc4 || z3; }
-	bool all() { return cvc4 && z3; }
+	bool some() { return cvc4 || smtlib2 || z3; }
+	bool all() { return cvc4 && smtlib2 && z3; }
 };
 
 enum class CheckResult

libsolidity/formal/BMC.cpp

@@ -40,16 +40,15 @@ BMC::BMC(
 	ErrorReporter& _errorReporter,
 	map<h256, string> const& _smtlib2Responses,
 	ReadCallback::Callback const& _smtCallback,
-	smtutil::SMTSolverChoice _enabledSolvers,
 	ModelCheckerSettings const& _settings,
 	CharStreamProvider const& _charStreamProvider
 ):
 	SMTEncoder(_context, _settings, _charStreamProvider),
-	m_interface(make_unique<smtutil::SMTPortfolio>(_smtlib2Responses, _smtCallback, _enabledSolvers, _settings.timeout)),
+	m_interface(make_unique<smtutil::SMTPortfolio>(_smtlib2Responses, _smtCallback, _settings.solvers, _settings.timeout)),
 	m_outerErrorReporter(_errorReporter)
 {
 #if defined (HAVE_Z3) || defined (HAVE_CVC4)
-	if (_enabledSolvers.some())
+	if (m_settings.solvers.cvc4 || m_settings.solvers.z3)
 		if (!_smtlib2Responses.empty())
 			m_errorReporter.warning(
 				5622_error,
@@ -63,6 +62,20 @@ BMC::BMC(
 
 void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<VerificationTargetType>> _solvedTargets)
 {
+	if (m_interface->solvers() == 0)
+	{
+		if (!m_noSolverWarning)
+		{
+			m_noSolverWarning = true;
+			m_outerErrorReporter.warning(
+				7710_error,
+				SourceLocation(),
+				"BMC analysis was not possible since no SMT solver was found and enabled."
+			);
+		}
+		return;
+	}
+
 	if (SMTEncoder::analyze(_source))
 	{
 		m_solvedTargets = move(_solvedTargets);
@@ -75,19 +88,23 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
 		_source.accept(*this);
 	}
 
-	solAssert(m_interface->solvers() > 0, "");
 	// If this check is true, Z3 and CVC4 are not available
 	// and the query answers were not provided, since SMTPortfolio
-	// guarantees that SmtLib2Interface is the first solver.
-	if (!m_interface->unhandledQueries().empty() && m_interface->solvers() == 1)
+	// guarantees that SmtLib2Interface is the first solver, if enabled.
+	if (
+		!m_interface->unhandledQueries().empty() &&
+		m_interface->solvers() == 1 &&
+		m_settings.solvers.smtlib2
+	)
 	{
 		if (!m_noSolverWarning)
 		{
 			m_noSolverWarning = true;
 			m_outerErrorReporter.warning(
 				8084_error,
 				SourceLocation(),
-				"BMC analysis was not possible since no SMT solver (Z3 or CVC4) was found."
+				"BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available."
+				" None of the installed solvers was enabled."
 #ifdef HAVE_Z3_DLOPEN
 				" Install libz3.so." + to_string(Z3_MAJOR_VERSION) + "." + to_string(Z3_MINOR_VERSION) + " to enable Z3."
 #endif
@@ -916,16 +933,20 @@ void BMC::checkCondition(
 		solAssert(!_callStack.empty(), "");
 		std::ostringstream message;
 		message << "BMC: " << _description << " happens here.";
+
 		std::ostringstream modelMessage;
-		modelMessage << "Counterexample:\n";
-		solAssert(values.size() == expressionNames.size(), "");
-		map<string, string> sortedModel;
-		for (size_t i = 0; i < values.size(); ++i)
-			if (expressionsToEvaluate.at(i).name != values.at(i))
-				sortedModel[expressionNames.at(i)] = values.at(i);
-
-		for (auto const& eval: sortedModel)
-			modelMessage << "  " << eval.first << " = " << eval.second << "\n";
+		// Sometimes models have complex smtlib2 expressions that SMTLib2Interface fails to parse.
+		if (values.size() == expressionNames.size())
+		{
+			modelMessage << "Counterexample:\n";
+			map<string, string> sortedModel;
+			for (size_t i = 0; i < values.size(); ++i)
+				if (expressionsToEvaluate.at(i).name != values.at(i))
+					sortedModel[expressionNames.at(i)] = values.at(i);
+
+			for (auto const& eval: sortedModel)
+				modelMessage << "  " << eval.first << " = " << eval.second << "\n";
+		}
 
 		m_errorReporter.warning(
 			_errorHappens,

libsolidity/formal/BMC.h

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

libsolidity/formal/CHC.cpp

@@ -56,26 +56,38 @@ CHC::CHC(
 	ErrorReporter& _errorReporter,
 	[[maybe_unused]] map<util::h256, string> const& _smtlib2Responses,
 	[[maybe_unused]] ReadCallback::Callback const& _smtCallback,
-	SMTSolverChoice _enabledSolvers,
 	ModelCheckerSettings const& _settings,
 	CharStreamProvider const& _charStreamProvider
 ):
 	SMTEncoder(_context, _settings, _charStreamProvider),
-	m_outerErrorReporter(_errorReporter),
-	m_enabledSolvers(_enabledSolvers)
+	m_outerErrorReporter(_errorReporter)
 {
-	bool usesZ3 = _enabledSolvers.z3;
+	bool usesZ3 = m_settings.solvers.z3;
 #ifdef HAVE_Z3
 	usesZ3 = usesZ3 && Z3Interface::available();
 #else
 	usesZ3 = false;
 #endif
-	if (!usesZ3)
+	if (!usesZ3 && m_settings.solvers.smtlib2)
 		m_interface = make_unique<CHCSmtLib2Interface>(_smtlib2Responses, _smtCallback, m_settings.timeout);
 }
 
 void CHC::analyze(SourceUnit const& _source)
 {
+	if (!m_settings.solvers.z3 && !m_settings.solvers.smtlib2)
+	{
+		if (!m_noSolverWarning)
+		{
+			m_noSolverWarning = true;
+			m_outerErrorReporter.warning(
+				7649_error,
+				SourceLocation(),
+				"CHC analysis was not possible since no Horn solver was enabled."
+			);
+		}
+		return;
+	}
+
 	if (SMTEncoder::analyze(_source))
 	{
 		resetSourceAnalysis();
@@ -92,6 +104,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.
 	if (auto const* smtLibInterface = dynamic_cast<CHCSmtLib2Interface const*>(m_interface.get()))
 		ranSolver = smtLibInterface->unhandledQueries().empty();
 	if (!ranSolver && !m_noSolverWarning)
@@ -103,7 +117,8 @@ void CHC::analyze(SourceUnit const& _source)
 #ifdef HAVE_Z3_DLOPEN
 			"CHC analysis was not possible since libz3.so." + to_string(Z3_MAJOR_VERSION) + "." + to_string(Z3_MINOR_VERSION) + " was not found."
 #else
-			"CHC analysis was not possible since no integrated z3 SMT solver was found."
+			"CHC analysis was not possible. No Horn solver was available."
+			" None of the installed solvers was enabled."
 #endif
 		);
 	}
@@ -933,7 +948,7 @@ void CHC::resetSourceAnalysis()
 
 	bool usesZ3 = false;
 #ifdef HAVE_Z3
-	usesZ3 = m_enabledSolvers.z3 && Z3Interface::available();
+	usesZ3 = m_settings.solvers.z3 && Z3Interface::available();
 	if (usesZ3)
 	{
 		/// z3::fixedpoint does not have a reset mechanism, so we need to create another.
@@ -1427,20 +1442,23 @@ pair<CheckResult, CHCSolverInterface::CexGraph> CHC::query(smtutil::Expression c
 	case CheckResult::SATISFIABLE:
 	{
 #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());
-		solAssert(spacer, "");
-		spacer->setSpacerOptions(false);
+		if (m_settings.solvers.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());
+			solAssert(spacer, "");
+			spacer->setSpacerOptions(false);
 
-		CheckResult resultNoOpt;
-		CHCSolverInterface::CexGraph cexNoOpt;
-		tie(resultNoOpt, cexNoOpt) = m_interface->query(_query);
+			CheckResult resultNoOpt;
+			CHCSolverInterface::CexGraph cexNoOpt;
+			tie(resultNoOpt, cexNoOpt) = m_interface->query(_query);
 
-		if (resultNoOpt == CheckResult::SATISFIABLE)
-			cex = move(cexNoOpt);
+			if (resultNoOpt == CheckResult::SATISFIABLE)
+				cex = move(cexNoOpt);
 
-		spacer->setSpacerOptions(true);
+			spacer->setSpacerOptions(true);
+		}
 #endif
 		break;
 	}