Bundle all unproved targets in a single message and only show all if setting chooses that

libsolidity/formal/BMC.cpp

@@ -60,7 +60,7 @@ BMC::BMC(
 #endif
 }
 
-void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<VerificationTargetType>> _solvedTargets)
+void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<VerificationTargetType>, smt::EncodingContext::IdCompare> _solvedTargets)
 {
 	if (m_interface->solvers() == 0)
 	{
@@ -84,8 +84,21 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
 		m_context.setAssertionAccumulation(true);
 		m_variableUsage.setFunctionInlining(shouldInlineFunctionCall);
 		createFreeConstants(sourceDependencies(_source));
+		m_unprovedAmt = 0;
 
 		_source.accept(*this);
+
+		if (m_unprovedAmt > 0 && !m_settings.showUnproved)
+			m_errorReporter.warning(
+				2788_error,
+				{},
+				"BMC: " +
+				to_string(m_unprovedAmt) +
+				" verification condition(s) could not be proved." +
+				" Enable the model checker option \"show unproved\" to see all of them." +
+				" Consider choosing a specific contract to be verified in order to reduce the solving problems." +
+				" Consider increasing the timeout per query."
+			);
 	}
 
 	// If this check is true, Z3 and CVC4 are not available
@@ -961,8 +974,12 @@ void BMC::checkCondition(
 	case smtutil::CheckResult::UNSATISFIABLE:
 		break;
 	case smtutil::CheckResult::UNKNOWN:
+	{
+		++m_unprovedAmt;
+		if (m_settings.showUnproved)
 			m_errorReporter.warning(_errorMightHappen, _location, "BMC: " + _description + " might happen here.", secondaryLocation);
 		break;
+	}
 	case smtutil::CheckResult::CONFLICTING:
 		m_errorReporter.warning(1584_error, _location, "BMC: At least two SMT solvers provided conflicting answers. Results might not be sound.");
 		break;

libsolidity/formal/BMC.h

@@ -66,7 +66,7 @@ public:
 		langutil::CharStreamProvider const& _charStreamProvider
 	);
 
-	void analyze(SourceUnit const& _sources, std::map<ASTNode const*, std::set<VerificationTargetType>> _solvedTargets);
+	void analyze(SourceUnit const& _sources, std::map<ASTNode const*, std::set<VerificationTargetType>, smt::EncodingContext::IdCompare> _solvedTargets);
 
 	/// This is used if the SMT solver is not directly linked into this binary.
 	/// @returns a list of inputs to the SMT solver that were not part of the argument to
@@ -192,7 +192,10 @@ private:
 	std::vector<BMCVerificationTarget> m_verificationTargets;
 
 	/// Targets that were already proven.
-	std::map<ASTNode const*, std::set<VerificationTargetType>> m_solvedTargets;
+	std::map<ASTNode const*, std::set<VerificationTargetType>, smt::EncodingContext::IdCompare> m_solvedTargets;
+
+	/// Number of verification conditions that could not be proved.
+	size_t m_unprovedAmt = 0;
 };
 
 }

libsolidity/formal/CHC.cpp

@@ -933,6 +933,7 @@ void CHC::resetSourceAnalysis()
 {
 	m_safeTargets.clear();
 	m_unsafeTargets.clear();
+	m_unprovedTargets.clear();
 	m_functionTargetIds.clear();
 	m_verificationTargets.clear();
 	m_queryPlaceholders.clear();
@@ -1594,6 +1595,32 @@ void CHC::checkVerificationTargets()
 		checkedErrorIds.insert(target.errorId);
 	}
 
+	auto toReport = m_unsafeTargets;
+	if (m_settings.showUnproved)
+		for (auto const& [node, targets]: m_unprovedTargets)
+			for (auto const& [target, info]: targets)
+				toReport[node].emplace(target, info);
+
+	for (auto const& [node, targets]: toReport)
+		for (auto const& [target, info]: targets)
+			m_errorReporter.warning(
+				info.error,
+				info.location,
+				info.message
+			);
+
+	if (!m_settings.showUnproved && !m_unprovedTargets.empty())
+		m_errorReporter.warning(
+			5840_error,
+			{},
+			"CHC: " +
+			to_string(m_unprovedTargets.size()) +
+			" verification condition(s) could not be proved." +
+			" Enable the model checker option \"show unproved\" to see all of them." +
+			" Consider choosing a specific contract to be verified in order to reduce the solving problems." +
+			" Consider increasing the timeout per query."
+		);
+
 	// There can be targets in internal functions that are not reachable from the external interface.
 	// These are safe by definition and are not even checked by the CHC engine, but this information
 	// must still be reported safe by the BMC engine.
@@ -1633,27 +1660,26 @@ void CHC::checkAndReportTarget(
 	else if (result == CheckResult::SATISFIABLE)
 	{
 		solAssert(!_satMsg.empty(), "");
-		m_unsafeTargets[_target.errorNode].insert(_target.type);
 		auto cex = generateCounterexample(model, error().name);
 		if (cex)
-			m_errorReporter.warning(
+			m_unsafeTargets[_target.errorNode][_target.type] = {
 				_errorReporterId,
 				location,
 				"CHC: " + _satMsg + "\nCounterexample:\n" + *cex
-			);
+			};
 		else
-			m_errorReporter.warning(
+			m_unsafeTargets[_target.errorNode][_target.type] = {
 				_errorReporterId,
 				location,
 				"CHC: " + _satMsg
-			);
+			};
 	}
 	else if (!_unknownMsg.empty())
-		m_errorReporter.warning(
+		m_unprovedTargets[_target.errorNode][_target.type] = {
 			_errorReporterId,
 			location,
 			"CHC: " + _unknownMsg
-		);
+		};
 }
 
 /**

libsolidity/formal/CHC.h

@@ -39,6 +39,8 @@
 
 #include <libsmtutil/CHCSolverInterface.h>
 
+#include <liblangutil/SourceLocation.h>
+
 #include <boost/algorithm/string/join.hpp>
 
 #include <map>
@@ -62,8 +64,14 @@ public:
 
 	void analyze(SourceUnit const& _sources);
 
-	std::map<ASTNode const*, std::set<VerificationTargetType>> const& safeTargets() const { return m_safeTargets; }
-	std::map<ASTNode const*, std::set<VerificationTargetType>> const& unsafeTargets() const { return m_unsafeTargets; }
+	struct ReportTargetInfo
+	{
+		langutil::ErrorId error;
+		langutil::SourceLocation location;
+		std::string message;
+	};
+	std::map<ASTNode const*, std::set<VerificationTargetType>, smt::EncodingContext::IdCompare> const& safeTargets() const { return m_safeTargets; }
+	std::map<ASTNode const*, std::map<VerificationTargetType, ReportTargetInfo>, smt::EncodingContext::IdCompare> const& unsafeTargets() const { return m_unsafeTargets; }
 
 	/// This is used if the Horn solver is not directly linked into this binary.
 	/// @returns a list of inputs to the Horn solver that were not part of the argument to
@@ -347,10 +355,12 @@ private:
 	/// Helper mapping unique IDs to actual verification targets.
 	std::map<unsigned, CHCVerificationTarget> m_verificationTargets;
 
-	/// Targets proven safe.
-	std::map<ASTNode const*, std::set<VerificationTargetType>> m_safeTargets;
-	/// Targets proven unsafe.
-	std::map<ASTNode const*, std::set<VerificationTargetType>> m_unsafeTargets;
+	/// Targets proved safe.
+	std::map<ASTNode const*, std::set<VerificationTargetType>, smt::EncodingContext::IdCompare> m_safeTargets;
+	/// Targets proved unsafe.
+	std::map<ASTNode const*, std::map<VerificationTargetType, ReportTargetInfo>, smt::EncodingContext::IdCompare> m_unsafeTargets;
+	/// Targets not proved.
+	std::map<ASTNode const*, std::map<VerificationTargetType, ReportTargetInfo>, smt::EncodingContext::IdCompare> m_unprovedTargets;
 	//@}
 
 	/// Control-flow.

libsolidity/formal/ModelChecker.cpp

@@ -120,8 +120,8 @@ void ModelChecker::analyze(SourceUnit const& _source)
 		m_chc.analyze(_source);
 
 	auto solvedTargets = m_chc.safeTargets();
-	for (auto const& target: m_chc.unsafeTargets())
-		solvedTargets[target.first] += target.second;
+	for (auto const& [node, targets]: m_chc.unsafeTargets())
+		solvedTargets[node] += targets | ranges::views::keys;
 
 	if (m_settings.engine.bmc)
 		m_bmc.analyze(_source, solvedTargets);

libsolidity/formal/ModelCheckerSettings.h

@@ -113,6 +113,7 @@ struct ModelCheckerSettings
 {
 	ModelCheckerContracts contracts = ModelCheckerContracts::Default();
 	ModelCheckerEngine engine = ModelCheckerEngine::None();
+	bool showUnproved = false;
 	smtutil::SMTSolverChoice solvers = smtutil::SMTSolverChoice::All();
 	ModelCheckerTargets targets = ModelCheckerTargets::Default();
 	std::optional<unsigned> timeout;
@@ -123,6 +124,7 @@ struct ModelCheckerSettings
 		return
 			contracts == _other.contracts &&
 			engine == _other.engine &&
+			showUnproved == _other.showUnproved &&
 			solvers == _other.solvers &&
 			targets == _other.targets &&
 			timeout == _other.timeout;

test/tools/fuzzer_common.cpp

@@ -20,6 +20,7 @@
 
 #include <libsolidity/interface/OptimiserSettings.h>
 #include <libsolidity/interface/CompilerStack.h>
+#include <libsolidity/formal/ModelCheckerSettings.h>
 
 #include <libsolutil/JSON.h>
 
@@ -104,6 +105,7 @@ void FuzzerUtil::testCompiler(
 		compiler.setModelCheckerSettings({
 			frontend::ModelCheckerContracts::Default(),
 			frontend::ModelCheckerEngine::All(),
+			/*showUnproved=*/false,
 			smtutil::SMTSolverChoice::All(),
 			frontend::ModelCheckerTargets::Default(),
 			/*timeout=*/1