[SMTChecker] Warn when no solver was found and there are unhandled queries.

liblangutil/ErrorReporter.h

@@ -22,6 +22,8 @@
 
 #pragma once
 
+#include <libdevcore/CommonData.h>
+
 #include <liblangutil/Exceptions.h>
 #include <liblangutil/SourceLocation.h>
 
@@ -40,6 +42,11 @@ public:
 
 	ErrorReporter& operator=(ErrorReporter const& _errorReporter);
 
+	void append(ErrorList const& _errorList)
+	{
+		m_errorList += _errorList;
+	}
+
 	void warning(std::string const& _description);
 
 	void warning(SourceLocation const& _location, std::string const& _description);

libsolidity/formal/SMTChecker.cpp

@@ -34,7 +34,8 @@ using namespace dev::solidity;
 
 SMTChecker::SMTChecker(ErrorReporter& _errorReporter, map<h256, string> const& _smtlib2Responses):
 	m_interface(make_shared<smt::SMTPortfolio>(_smtlib2Responses)),
-	m_errorReporter(_errorReporter)
+	m_errorReporterReference(_errorReporter),
+	m_errorReporter(m_smtErrors)
 {
 #if defined (HAVE_Z3) || defined (HAVE_CVC4)
 	if (!_smtlib2Responses.empty())
@@ -53,6 +54,25 @@ void SMTChecker::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _
 	m_scanner = _scanner;
 	if (_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
 		_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)
+	{
+		if (!m_noSolverWarning)
+		{
+			m_noSolverWarning = true;
+			m_errorReporterReference.warning(
+				SourceLocation(),
+				"SMTChecker analysis was not possible since no integrated SMT solver (Z3 or CVC4) was found."
+			);
+		}
+	}
+	else
+		m_errorReporterReference.append(m_errorReporter.errors());
+	m_errorReporter.clear();
 }
 
 bool SMTChecker::visit(ContractDefinition const& _contract)

libsolidity/formal/SMTChecker.h

@@ -23,6 +23,7 @@
 
 #include <libsolidity/ast/ASTVisitor.h>
 #include <libsolidity/interface/ReadFile.h>
+#include <liblangutil/ErrorReporter.h>
 #include <liblangutil/Scanner.h>
 
 #include <string>
@@ -215,6 +216,8 @@ private:
 	std::shared_ptr<VariableUsage> m_variableUsage;
 	bool m_loopExecutionHappened = false;
 	bool m_arrayAssignmentHappened = false;
+	// True if the "No SMT solver available" warning was already created.
+	bool m_noSolverWarning = false;
 	/// An Expression may have multiple smt::Expression due to
 	/// repeated calls to the same function.
 	std::unordered_map<Expression const*, std::shared_ptr<SymbolicVariable>> m_expressions;
@@ -225,7 +228,13 @@ private:
 	/// Used to retrieve models.
 	std::set<Expression const*> m_uninterpretedTerms;
 	std::vector<smt::Expression> m_pathConditions;
-	langutil::ErrorReporter& m_errorReporter;
+	/// ErrorReporter that comes from CompilerStack.
+	langutil::ErrorReporter& m_errorReporterReference;
+	/// Local SMTChecker ErrorReporter.
+	/// This is necessary to show the "No SMT solver available"
+	/// warning before the others in case it's needed.
+	langutil::ErrorReporter m_errorReporter;
+	langutil::ErrorList m_smtErrors;
 	std::shared_ptr<langutil::Scanner> m_scanner;
 
 	/// Stores the current path of function calls.

libsolidity/formal/SMTPortfolio.cpp

@@ -129,6 +129,15 @@ pair<CheckResult, vector<string>> SMTPortfolio::check(vector<Expression> const&
 	return make_pair(lastResult, finalValues);
 }
 
+vector<string> SMTPortfolio::unhandledQueries()
+{
+	// This code assumes that the constructor guarantees that
+	// SmtLib2Interface is in position 0.
+	solAssert(!m_solvers.empty(), "");
+	solAssert(dynamic_cast<smt::SMTLib2Interface*>(m_solvers.at(0).get()), "");
+	return m_solvers.at(0)->unhandledQueries();
+}
+
 bool SMTPortfolio::solverAnswered(CheckResult result)
 {
 	return result == CheckResult::SATISFIABLE || result == CheckResult::UNSATISFIABLE;

libsolidity/formal/SMTPortfolio.h

@@ -54,7 +54,8 @@ public:
 	void addAssertion(Expression const& _expr) override;
 	std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
 
-	std::vector<std::string> unhandledQueries() override { return m_solvers.at(0)->unhandledQueries(); }
+	std::vector<std::string> unhandledQueries() override;
+	unsigned solvers() override { return m_solvers.size(); }
 private:
 	static bool solverAnswered(CheckResult result);
 

libsolidity/formal/SolverInterface.h

@@ -305,6 +305,9 @@ public:
 	/// @returns a list of queries that the system was not able to respond to.
 	virtual std::vector<std::string> unhandledQueries() { return {}; }
 
+	/// @returns how many SMT solvers this interface has.
+	virtual unsigned solvers() { return 1; }
+
 protected:
 	// SMT query timeout in milliseconds.
 	static int const queryTimeout = 10000;