Merge pull request #11850 from ethereum/smt_remove_redundant_warnings

[SMTChecker] Remove redundant unsupported warnings

Author: Leonardo

liblangutil/CMakeLists.txt

@@ -25,6 +25,7 @@ set(sources
 	Token.cpp
 	Token.h
 	UndefMacros.h
+	UniqueErrorReporter.h
 )
 
 add_library(langutil ${sources})

liblangutil/Exceptions.h

@@ -105,6 +105,7 @@ struct ErrorId
 	unsigned long long error = 0;
 	bool operator==(ErrorId const& _rhs) const { return error == _rhs.error; }
 	bool operator!=(ErrorId const& _rhs) const { return !(*this == _rhs); }
+	bool operator<(ErrorId const& _rhs) const { return error < _rhs.error; }
 };
 constexpr ErrorId operator"" _error(unsigned long long _error) { return ErrorId{ _error }; }
 

liblangutil/UniqueErrorReporter.h

@@ -0,0 +1,94 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+#pragma once
+
+#include <liblangutil/ErrorReporter.h>
+#include <liblangutil/Exceptions.h>
+
+namespace solidity::langutil
+{
+
+/*
+ * Wrapper for ErrorReporter that removes duplicates.
+ * Two errors are considered the same if their error ID and location are the same.
+ */
+class UniqueErrorReporter
+{
+public:
+	UniqueErrorReporter(): m_errorReporter(m_uniqueErrors) {}
+
+	void warning(ErrorId _error, SourceLocation const& _location, std::string const& _description)
+	{
+		if (!seen(_error, _location, _description))
+		{
+			m_errorReporter.warning(_error, _location, _description);
+			markAsSeen(_error, _location, _description);
+		}
+	}
+
+	void warning(
+		ErrorId _error,
+		SourceLocation const& _location,
+		std::string const& _description,
+		SecondarySourceLocation const& _secondaryLocation
+	)
+	{
+		if (!seen(_error, _location, _description))
+		{
+			m_errorReporter.warning(_error, _location, _description, _secondaryLocation);
+			markAsSeen(_error, _location, _description);
+		}
+	}
+
+	void warning(ErrorId _error, std::string const& _description)
+	{
+		if (!seen(_error, {}, _description))
+		{
+			m_errorReporter.warning(_error, _description);
+			markAsSeen(_error, {}, _description);
+		}
+	}
+
+	bool seen(ErrorId _error, SourceLocation const& _location, std::string const& _description) const
+	{
+		if (m_seenErrors.count({_error, _location}))
+		{
+			solAssert(m_seenErrors.at({_error, _location}) == _description, "");
+			return true;
+		}
+		return false;
+	}
+
+	void markAsSeen(ErrorId _error, SourceLocation const& _location, std::string const& _description)
+	{
+		solAssert(!seen(_error, _location, _description), "");
+		m_seenErrors[{_error, _location}] = _description;
+	}
+
+	ErrorList const& errors() const { return m_errorReporter.errors(); }
+
+	void clear() { m_errorReporter.clear(); }
+
+private:
+	ErrorReporter m_errorReporter;
+	ErrorList m_uniqueErrors;
+	std::map<std::pair<ErrorId, SourceLocation>, std::string> m_seenErrors;
+};
+
+}

libsolidity/formal/BMC.cpp

@@ -37,15 +37,14 @@ using namespace solidity::frontend;
 
 BMC::BMC(
 	smt::EncodingContext& _context,
-	ErrorReporter& _errorReporter,
+	UniqueErrorReporter& _errorReporter,
 	map<h256, string> const& _smtlib2Responses,
 	ReadCallback::Callback const& _smtCallback,
 	ModelCheckerSettings const& _settings,
 	CharStreamProvider const& _charStreamProvider
 ):
-	SMTEncoder(_context, _settings, _charStreamProvider),
-	m_interface(make_unique<smtutil::SMTPortfolio>(_smtlib2Responses, _smtCallback, _settings.solvers, _settings.timeout)),
-	m_outerErrorReporter(_errorReporter)
+	SMTEncoder(_context, _settings, _errorReporter, _charStreamProvider),
+	m_interface(make_unique<smtutil::SMTPortfolio>(_smtlib2Responses, _smtCallback, _settings.solvers, _settings.timeout))
 {
 #if defined (HAVE_Z3) || defined (HAVE_CVC4)
 	if (m_settings.solvers.cvc4 || m_settings.solvers.z3)
@@ -67,7 +66,7 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
 		if (!m_noSolverWarning)
 		{
 			m_noSolverWarning = true;
-			m_outerErrorReporter.warning(
+			m_errorReporter.warning(
 				7710_error,
 				SourceLocation(),
 				"BMC analysis was not possible since no SMT solver was found and enabled."
@@ -113,7 +112,7 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
 		if (!m_noSolverWarning)
 		{
 			m_noSolverWarning = true;
-			m_outerErrorReporter.warning(
+			m_errorReporter.warning(
 				8084_error,
 				SourceLocation(),
 				"BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available."
@@ -124,10 +123,6 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
 			);
 		}
 	}
-	else
-		m_outerErrorReporter.append(m_errorReporter.errors());
-
-	m_errorReporter.clear();
 }
 
 bool BMC::shouldInlineFunctionCall(

libsolidity/formal/BMC.h

@@ -36,7 +36,7 @@
 #include <libsolidity/interface/ReadFile.h>
 
 #include <libsmtutil/SolverInterface.h>
-#include <liblangutil/ErrorReporter.h>
+#include <liblangutil/UniqueErrorReporter.h>
 
 #include <set>
 #include <string>
@@ -59,7 +59,7 @@ class BMC: public SMTEncoder
 public:
 	BMC(
 		smt::EncodingContext& _context,
-		langutil::ErrorReporter& _errorReporter,
+		langutil::UniqueErrorReporter& _errorReporter,
 		std::map<h256, std::string> const& _smtlib2Responses,
 		ReadCallback::Callback const& _smtCallback,
 		ModelCheckerSettings const& _settings,
@@ -186,9 +186,6 @@ class BMC: public SMTEncoder
 	bool m_loopExecutionHappened = false;
 	bool m_externalFunctionCallHappened = false;
 
-	/// ErrorReporter that comes from CompilerStack.
-	langutil::ErrorReporter& m_outerErrorReporter;
-
 	std::vector<BMCVerificationTarget> m_verificationTargets;
 
 	/// Targets that were already proven.

libsolidity/formal/CHC.cpp

@@ -53,14 +53,13 @@ using namespace solidity::frontend::smt;
 
 CHC::CHC(
 	EncodingContext& _context,
-	ErrorReporter& _errorReporter,
+	UniqueErrorReporter& _errorReporter,
 	[[maybe_unused]] map<util::h256, string> const& _smtlib2Responses,
 	[[maybe_unused]] ReadCallback::Callback const& _smtCallback,
 	ModelCheckerSettings const& _settings,
 	CharStreamProvider const& _charStreamProvider
 ):
-	SMTEncoder(_context, _settings, _charStreamProvider),
-	m_outerErrorReporter(_errorReporter)
+	SMTEncoder(_context, _settings, _errorReporter, _charStreamProvider)
 {
 	bool usesZ3 = m_settings.solvers.z3;
 #ifdef HAVE_Z3
@@ -79,7 +78,7 @@ void CHC::analyze(SourceUnit const& _source)
 		if (!m_noSolverWarning)
 		{
 			m_noSolverWarning = true;
-			m_outerErrorReporter.warning(
+			m_errorReporter.warning(
 				7649_error,
 				SourceLocation(),
 				"CHC analysis was not possible since no Horn solver was enabled."
@@ -111,7 +110,7 @@ void CHC::analyze(SourceUnit const& _source)
 	if (!ranSolver && !m_noSolverWarning)
 	{
 		m_noSolverWarning = true;
-		m_outerErrorReporter.warning(
+		m_errorReporter.warning(
 			3996_error,
 			SourceLocation(),
 #ifdef HAVE_Z3_DLOPEN
@@ -122,10 +121,6 @@ void CHC::analyze(SourceUnit const& _source)
 #endif
 		);
 	}
-	else
-		m_outerErrorReporter.append(m_errorReporter.errors());
-
-	m_errorReporter.clear();
 }
 
 vector<string> CHC::unhandledQueries() const

libsolidity/formal/CHC.h

@@ -40,6 +40,7 @@
 #include <libsmtutil/CHCSolverInterface.h>
 
 #include <liblangutil/SourceLocation.h>
+#include <liblangutil/UniqueErrorReporter.h>
 
 #include <boost/algorithm/string/join.hpp>
 
@@ -55,7 +56,7 @@ class CHC: public SMTEncoder
 public:
 	CHC(
 		smt::EncodingContext& _context,
-		langutil::ErrorReporter& _errorReporter,
+		langutil::UniqueErrorReporter& _errorReporter,
 		std::map<util::h256, std::string> const& _smtlib2Responses,
 		ReadCallback::Callback const& _smtCallback,
 		ModelCheckerSettings const& _settings,
@@ -415,9 +416,6 @@ class CHC: public SMTEncoder
 
 	/// CHC solver.
 	std::unique_ptr<smtutil::CHCSolverInterface> m_interface;
-
-	/// ErrorReporter that comes from CompilerStack.
-	langutil::ErrorReporter& m_outerErrorReporter;
 };
 
 }

libsolidity/formal/ModelChecker.cpp

@@ -40,8 +40,8 @@ ModelChecker::ModelChecker(
 	m_errorReporter(_errorReporter),
 	m_settings(move(_settings)),
 	m_context(),
-	m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, m_settings, _charStreamProvider),
-	m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, m_settings, _charStreamProvider)
+	m_bmc(m_context, m_uniqueErrorReporter, _smtlib2Responses, _smtCallback, m_settings, _charStreamProvider),
+	m_chc(m_context, m_uniqueErrorReporter, _smtlib2Responses, _smtCallback, m_settings, _charStreamProvider)
 {
 }
 
@@ -68,7 +68,7 @@ void ModelChecker::checkRequestedSourcesAndContracts(vector<shared_ptr<SourceUni
 	{
 		if (!exist.count(sourceName))
 		{
-			m_errorReporter.warning(
+			m_uniqueErrorReporter.warning(
 				9134_error,
 				SourceLocation(),
 				"Requested source \"" + sourceName + "\" does not exist."
@@ -79,7 +79,7 @@ void ModelChecker::checkRequestedSourcesAndContracts(vector<shared_ptr<SourceUni
 		// Requested contracts in source `s`.
 		for (auto const& contract: m_settings.contracts.contracts.at(sourceName))
 			if (!source.count(contract))
-				m_errorReporter.warning(
+				m_uniqueErrorReporter.warning(
 					7400_error,
 					SourceLocation(),
 					"Requested contract \"" + contract + "\" does not exist in source \"" + sourceName + "\"."
@@ -104,7 +104,7 @@ void ModelChecker::analyze(SourceUnit const& _source)
 					break;
 				}
 		solAssert(smtPragma, "");
-		m_errorReporter.warning(
+		m_uniqueErrorReporter.warning(
 			5523_error,
 			smtPragma->location(),
 			"The SMTChecker pragma has been deprecated and will be removed in the future. "
@@ -125,6 +125,9 @@ void ModelChecker::analyze(SourceUnit const& _source)
 
 	if (m_settings.engine.bmc)
 		m_bmc.analyze(_source, solvedTargets);
+
+	m_errorReporter.append(m_uniqueErrorReporter.errors());
+	m_uniqueErrorReporter.clear();
 }
 
 vector<string> ModelChecker::unhandledQueries()

libsolidity/formal/ModelChecker.h

@@ -31,7 +31,9 @@
 #include <libsolidity/interface/ReadFile.h>
 
 #include <libsmtutil/SolverInterface.h>
+
 #include <liblangutil/ErrorReporter.h>
+#include <liblangutil/UniqueErrorReporter.h>
 
 namespace solidity::langutil
 {
@@ -73,8 +75,16 @@ class ModelChecker
 	static smtutil::SMTSolverChoice availableSolvers();
 
 private:
+	/// Error reporter from CompilerStack.
+	/// We need to append m_uniqueErrorReporter
+	/// to this one when the analysis is done.
 	langutil::ErrorReporter& m_errorReporter;
 
+	/// Used by ModelChecker, SMTEncoder, BMC and CHC to avoid duplicates.
+	/// This is local to ModelChecker, so needs to be appended
+	/// to m_errorReporter at the end of the analysis.
+	langutil::UniqueErrorReporter m_uniqueErrorReporter;
+
 	ModelCheckerSettings m_settings;
 
 	/// Stores the context of the encoding.

libsolidity/formal/SMTEncoder.cpp

@@ -46,9 +46,10 @@ using namespace solidity::frontend;
 SMTEncoder::SMTEncoder(
 	smt::EncodingContext& _context,
 	ModelCheckerSettings const& _settings,
+	UniqueErrorReporter& _errorReporter,
 	langutil::CharStreamProvider const& _charStreamProvider
 ):
-	m_errorReporter(m_smtErrors),
+	m_errorReporter(_errorReporter),
 	m_context(_context),
 	m_settings(_settings),
 	m_charStreamProvider(_charStreamProvider)