Add option to choose solver

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,11 +88,14 @@ 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)
 		{
@@ -87,7 +103,8 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
 			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";
+		std::ostringstream modelMessage;
+		// 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 @@ public:
 		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;
 	}

libsolidity/formal/CHC.h

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

libsolidity/formal/ModelChecker.cpp

@@ -35,14 +35,13 @@ ModelChecker::ModelChecker(
 	langutil::CharStreamProvider const& _charStreamProvider,
 	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, _charStreamProvider),
-	m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers, m_settings, _charStreamProvider)
+	m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, m_settings, _charStreamProvider),
+	m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, m_settings, _charStreamProvider)
 {
 }
 
@@ -135,7 +134,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

@@ -52,8 +52,7 @@ public:
 		langutil::CharStreamProvider const& _charStreamProvider,
 		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

@@ -113,6 +113,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;
 
@@ -122,6 +123,7 @@ struct ModelCheckerSettings
 		return
 			contracts == _other.contracts &&
 			engine == _other.engine &&
+			solvers == _other.solvers &&
 			targets == _other.targets &&
 			timeout == _other.timeout;
 	}

libsolidity/interface/CompilerStack.cpp

@@ -95,7 +95,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
@@ -228,13 +227,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)
@@ -299,7 +291,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;
@@ -555,7 +546,7 @@ bool CompilerStack::analyze()
 
 		if (noErrors)
 		{
-			ModelChecker modelChecker(m_errorReporter, *this, m_smtlib2Responses, m_modelCheckerSettings, m_readFile, m_enabledSMTSolvers);
+			ModelChecker modelChecker(m_errorReporter, *this, 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

@@ -176,8 +176,6 @@ public:
 
 	/// 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
@@ -480,7 +478,6 @@ private:
 	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;

libsolidity/interface/StandardCompiler.cpp

@@ -442,7 +442,7 @@ std::optional<Json::Value> checkSettingsKeys(Json::Value const& _input)
 
 std::optional<Json::Value> checkModelCheckerSettingsKeys(Json::Value const& _input)
 {
-	static set<string> keys{"contracts", "engine", "targets", "timeout"};
+	static set<string> keys{"contracts", "engine", "solvers", "targets", "timeout"};
 	return checkKeys(_input, keys, "modelChecker");
 }
 
@@ -951,6 +951,24 @@ std::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompiler:
 		ret.modelCheckerSettings.engine = *engine;
 	}
 
+	if (modelCheckerSettings.isMember("solvers"))
+	{
+		auto const& solversArray = modelCheckerSettings["solvers"];
+		if (!solversArray.isArray())
+			return formatFatalError("JSONError", "settings.modelChecker.solvers must be an array.");
+
+		smtutil::SMTSolverChoice solvers;
+		for (auto const& s: solversArray)
+		{
+			if (!s.isString())
+				return formatFatalError("JSONError", "Every target in settings.modelChecker.solvers must be a string.");
+			if (!solvers.setSolver(s.asString()))
+				return formatFatalError("JSONError", "Invalid model checker solvers requested.");
+		}
+
+		ret.modelCheckerSettings.solvers = solvers;
+	}
+
 	if (modelCheckerSettings.isMember("targets"))
 	{
 		auto const& targetsArray = modelCheckerSettings["targets"];