Merge pull request #11705 from ethereum/smt_show_unproved

[SMTChecker] Bundle unproved messages by default

Author: Leonardo

Changelog.md

@@ -9,6 +9,7 @@ Compiler Features:
  * Yul EVM Code Transform: Also pop unused argument slots for functions without return variables (under the same restrictions as for functions with return variables).
  * Yul Optimizer: Move function arguments and return variables to memory with the experimental Stack Limit Evader (which is not enabled by default).
  * Commandline Interface: option ``--pretty-json`` works also with ``--standard--json``.
+ * SMTChecker: Unproved targets are hidden by default, and the SMTChecker only states how many unproved targets there are. They can be listed using the command line option ``--model-checker-show-unproved`` or the JSON option ``settings.modelChecker.showUnproved``.
 
 
 Bugfixes:

docs/smtchecker.rst

@@ -474,6 +474,14 @@ A common subset of targets might be, for example:
 There is no precise heuristic on how and when to split verification targets,
 but it can be useful especially when dealing with large contracts.
 
+Unproved Targets
+================
+
+If there are any unproved targets, the SMTChecker issues one warning stating
+how many unproved targets there are. If the user wishes to see all the specific
+unproved targets, the CLI option ``--model-checker-show-unproved true`` and
+the JSON option ``settings.modelChecker.showUnproved = true`` can be used.
+
 Verified Contracts
 ==================
 

docs/using-the-compiler.rst

@@ -402,6 +402,8 @@ Input Description
           },
           // Choose which model checker engine to use: all (default), bmc, chc, none.
           "engine": "chc",
+          // Choose whether to output all unproved targets. The default is `false`.
+          "showUnproved": true,
           // Choose which targets should be checked: constantCondition,
           // underflow, overflow, divByZero, balance, assert, popEmptyArray, outOfBounds.
           // If the option is not given all targets are checked by default.

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_errorReporter.warning(_errorMightHappen, _location, "BMC: " + _description + " might happen here.", secondaryLocation);
+	{
+		++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 @@ class BMC: public SMTEncoder
 		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 @@ class BMC: public SMTEncoder
 	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 @@ class CHC: public SMTEncoder
 
 	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 @@ class CHC: public SMTEncoder
 	/// 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;

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", "solvers", "targets", "timeout"};
+	static set<string> keys{"contracts", "engine", "showUnproved", "solvers", "targets", "timeout"};
 	return checkKeys(_input, keys, "modelChecker");
 }
 
@@ -951,6 +951,14 @@ std::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompiler:
 		ret.modelCheckerSettings.engine = *engine;
 	}
 
+	if (modelCheckerSettings.isMember("showUnproved"))
+	{
+		auto const& showUnproved = modelCheckerSettings["showUnproved"];
+		if (!showUnproved.isBool())
+			return formatFatalError("JSONError", "settings.modelChecker.showUnproved must be a Boolean value.");
+		ret.modelCheckerSettings.showUnproved = showUnproved.asBool();
+	}
+
 	if (modelCheckerSettings.isMember("solvers"))
 	{
 		auto const& solversArray = modelCheckerSettings["solvers"];