Add option to choose solver

Author: Leo Alt

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,6 +23,8 @@
 
 #include <libsolutil/Common.h>
 
+#include <range/v3/view.hpp>
+
 #include <cstdio>
 #include <map>
 #include <memory>
@@ -36,16 +38,42 @@ 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;
+		for (auto&& s: _solvers | ranges::views::split(',') | ranges::to<std::vector<std::string>>())
+			if (!solvers.setFromString(s))
+				return {};
+
+		return solvers;
+	}
+
+	bool setFromString(std::string const& _solver)
+	{
+		static std::set<std::string> 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

@@ -38,15 +38,14 @@ BMC::BMC(
 	ErrorReporter& _errorReporter,
 	map<h256, string> const& _smtlib2Responses,
 	ReadCallback::Callback const& _smtCallback,
-	smtutil::SMTSolverChoice _enabledSolvers,
 	ModelCheckerSettings const& _settings
 ):
 	SMTEncoder(_context, _settings),
-	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,
@@ -60,6 +59,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(
+				0000_error,
+				SourceLocation(),
+				"BMC analysis was not possible since no SMT solver was found and enabled."
+			);
+		}
+		return;
+	}
+
 	if (SMTEncoder::analyze(_source))
 	{
 		m_solvedTargets = move(_solvedTargets);
@@ -72,19 +85,22 @@ 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 since no SMT solver (Z3 or CVC4) 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

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
 	);
 

libsolidity/formal/CHC.cpp

@@ -56,25 +56,37 @@ CHC::CHC(
 	ErrorReporter& _errorReporter,
 	[[maybe_unused]] map<util::h256, string> const& _smtlib2Responses,
 	[[maybe_unused]] ReadCallback::Callback const& _smtCallback,
-	SMTSolverChoice _enabledSolvers,
 	ModelCheckerSettings const& _settings
 ):
 	SMTEncoder(_context, _settings),
-	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(
+				0000_error,
+				SourceLocation(),
+				"CHC analysis was not possible since no Horn solver was enabled."
+			);
+		}
+		return;
+	}
+
 	if (SMTEncoder::analyze(_source))
 	{
 		resetSourceAnalysis();
@@ -91,6 +103,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)
@@ -102,7 +116,7 @@ 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 since no Horn solver was found and enabled."
 #endif
 		);
 	}
@@ -933,7 +947,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 +1441,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;
 	}

libsolidity/formal/CHC.h

@@ -56,7 +56,6 @@ class CHC: public SMTEncoder
 		langutil::ErrorReporter& _errorReporter,
 		std::map<util::h256, std::string> const& _smtlib2Responses,
 		ReadCallback::Callback const& _smtCallback,
-		smtutil::SMTSolverChoice _enabledSolvers,
 		ModelCheckerSettings const& _settings
 	);
 
@@ -392,9 +391,6 @@ class CHC: public SMTEncoder
 
 	/// ErrorReporter that comes from CompilerStack.
 	langutil::ErrorReporter& m_outerErrorReporter;
-
-	/// SMT solvers that are chosen at runtime.
-	smtutil::SMTSolverChoice m_enabledSolvers;
 };
 
 }

libsolidity/formal/ModelChecker.cpp

@@ -34,14 +34,13 @@ ModelChecker::ModelChecker(
 	ErrorReporter& _errorReporter,
 	map<h256, string> const& _smtlib2Responses,
 	ModelCheckerSettings _settings,
-	ReadCallback::Callback const& _smtCallback,
-	smtutil::SMTSolverChoice _enabledSolvers
+	ReadCallback::Callback const& _smtCallback
 ):
 	m_errorReporter(_errorReporter),
-	m_settings(_settings),
+	m_settings(move(_settings)),
 	m_context(),
-	m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers, m_settings),
-	m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers, m_settings)
+	m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, m_settings),
+	m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, m_settings)
 {
 }
 
@@ -134,7 +133,7 @@ vector<string> ModelChecker::unhandledQueries()
 
 solidity::smtutil::SMTSolverChoice ModelChecker::availableSolvers()
 {
-	smtutil::SMTSolverChoice available = smtutil::SMTSolverChoice::None();
+	smtutil::SMTSolverChoice available = smtutil::SMTSolverChoice::SMTLIB2();
 #ifdef HAVE_Z3
 	available.z3 = solidity::smtutil::Z3Interface::available();
 #endif

libsolidity/formal/ModelChecker.h

@@ -51,8 +51,7 @@ class ModelChecker
 		langutil::ErrorReporter& _errorReporter,
 		std::map<solidity::util::h256, std::string> const& _smtlib2Responses,
 		ModelCheckerSettings _settings = ModelCheckerSettings{},
-		ReadCallback::Callback const& _smtCallback = ReadCallback::Callback(),
-		smtutil::SMTSolverChoice _enabledSolvers = smtutil::SMTSolverChoice::All()
+		ReadCallback::Callback const& _smtCallback = ReadCallback::Callback()
 	);
 
 	// TODO This should be removed for 0.9.0.

libsolidity/formal/ModelCheckerSettings.h

@@ -104,6 +104,7 @@ struct ModelCheckerSettings
 {
 	ModelCheckerContracts contracts = ModelCheckerContracts::Default();
 	ModelCheckerEngine engine = ModelCheckerEngine::None();
+	smtutil::SMTSolverChoice solvers = smtutil::SMTSolverChoice::All();
 	ModelCheckerTargets targets = ModelCheckerTargets::Default();
 	std::optional<unsigned> timeout;
 };

libsolidity/interface/CompilerStack.cpp

@@ -94,7 +94,6 @@ static int g_compilerStackCounts = 0;
 
 CompilerStack::CompilerStack(ReadCallback::Callback _readFile):
 	m_readFile{std::move(_readFile)},
-	m_enabledSMTSolvers{smtutil::SMTSolverChoice::All()},
 	m_errorReporter{m_errorList}
 {
 	// Because TypeProvider is currently a singleton API, we must ensure that
@@ -227,13 +226,6 @@ void CompilerStack::setModelCheckerSettings(ModelCheckerSettings _settings)
 	m_modelCheckerSettings = _settings;
 }
 
-void CompilerStack::setSMTSolverChoice(smtutil::SMTSolverChoice _enabledSMTSolvers)
-{
-	if (m_stackState >= ParsedAndImported)
-		BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Must set enabled SMT solvers before parsing."));
-	m_enabledSMTSolvers = _enabledSMTSolvers;
-}
-
 void CompilerStack::setLibraries(std::map<std::string, util::h160> const& _libraries)
 {
 	if (m_stackState >= ParsedAndImported)
@@ -298,7 +290,6 @@ void CompilerStack::reset(bool _keepSettings)
 		m_viaIR = false;
 		m_evmVersion = langutil::EVMVersion();
 		m_modelCheckerSettings = ModelCheckerSettings{};
-		m_enabledSMTSolvers = smtutil::SMTSolverChoice::All();
 		m_generateIR = false;
 		m_generateEwasm = false;
 		m_revertStrings = RevertStrings::Default;
@@ -546,7 +537,7 @@ bool CompilerStack::analyze()
 
 		if (noErrors)
 		{
-			ModelChecker modelChecker(m_errorReporter, m_smtlib2Responses, m_modelCheckerSettings, m_readFile, m_enabledSMTSolvers);
+			ModelChecker modelChecker(m_errorReporter, m_smtlib2Responses, m_modelCheckerSettings, m_readFile);
 			auto allSources = applyMap(m_sourceOrder, [](Source const* _source) { return _source->ast; });
 			modelChecker.enableAllEnginesIfPragmaPresent(allSources);
 			modelChecker.checkRequestedSourcesAndContracts(allSources);

libsolidity/interface/CompilerStack.h

@@ -174,8 +174,6 @@ class CompilerStack
 
 	/// Set model checker settings.
 	void setModelCheckerSettings(ModelCheckerSettings _settings);
-	/// Set which SMT solvers should be enabled.
-	void setSMTSolverChoice(smtutil::SMTSolverChoice _enabledSolvers);
 
 	/// Sets the requested contract names by source.
 	/// If empty, no filtering is performed and every contract
@@ -475,7 +473,6 @@ class CompilerStack
 	bool m_viaIR = false;
 	langutil::EVMVersion m_evmVersion;
 	ModelCheckerSettings m_modelCheckerSettings;
-	smtutil::SMTSolverChoice m_enabledSMTSolvers;
 	std::map<std::string, std::set<std::string>> m_requestedContractNames;
 	bool m_generateEvmBytecode = true;
 	bool m_generateIR = false;