Merge pull request #15205 from pgebal/smtchecker/fix-show-proved-safe

SMTChecker: Fix internal compiler error on reporting proved targets

Author: blishko

Changelog.md

@@ -12,7 +12,8 @@ Compiler Features:
 
 
 Bugfixes:
- * SMTChecker: Fix error that reports invalid number of verified checks for BMC engine.
+ * SMTChecker: Fix error that reports invalid number of verified checks for BMC and CHC engines.
+ * SMTChecker: Fix internal compiler error when reporting proved targets for BMC engine.
  * TypeChecker: Fix segfault when assigning nested tuple to tuple.
  * Yul Optimizer: Name simplification could lead to forbidden identifiers with a leading and/or trailing dot, e.g., ``x._`` would get simplified into ``x.``.
 

libsolidity/formal/BMC.cpp

@@ -47,12 +47,13 @@ BMC::BMC(
 	smt::EncodingContext& _context,
 	UniqueErrorReporter& _errorReporter,
 	UniqueErrorReporter& _unsupportedErrorReporter,
+	ErrorReporter& _provedSafeReporter,
 	std::map<h256, std::string> const& _smtlib2Responses,
 	ReadCallback::Callback const& _smtCallback,
 	ModelCheckerSettings _settings,
 	CharStreamProvider const& _charStreamProvider
 ):
-	SMTEncoder(_context, _settings, _errorReporter, _unsupportedErrorReporter, _charStreamProvider)
+	SMTEncoder(_context, _settings, _errorReporter, _unsupportedErrorReporter, _provedSafeReporter, _charStreamProvider)
 {
 	solAssert(!_settings.printQuery || _settings.solvers == SMTSolverChoice::SMTLIB2(), "Only SMTLib2 solver can be enabled to print queries");
 	std::vector<std::unique_ptr<SolverInterface>> solvers;
@@ -133,15 +134,14 @@ void BMC::analyze(SourceUnit const& _source, std::map<ASTNode const*, std::set<V
 	else if (m_settings.showProvedSafe)
 		for (auto const& [node, targets]: m_safeTargets)
 			for (auto const& target: targets)
-				m_errorReporter.info(
+				m_provedSafeReporter.info(
 					2961_error,
 					node->location(),
 					"BMC: " +
 					targetDescription(target) +
 					" check is safe!"
 				);
 
-
 	// If this check is true, Z3 and cvc5 are not available
 	// and the query answers were not provided, since SMTPortfolio
 	// guarantees that SmtLib2Interface is the first solver, if enabled.

libsolidity/formal/BMC.h

@@ -62,6 +62,7 @@ class BMC: public SMTEncoder
 		smt::EncodingContext& _context,
 		langutil::UniqueErrorReporter& _errorReporter,
 		langutil::UniqueErrorReporter& _unsupportedErrorReporter,
+		langutil::ErrorReporter& _provedSafeReporter,
 		std::map<h256, std::string> const& _smtlib2Responses,
 		ReadCallback::Callback const& _smtCallback,
 		ModelCheckerSettings _settings,

libsolidity/formal/CHC.cpp

@@ -63,12 +63,13 @@ CHC::CHC(
 	EncodingContext& _context,
 	UniqueErrorReporter& _errorReporter,
 	UniqueErrorReporter& _unsupportedErrorReporter,
+	ErrorReporter& _provedSafeReporter,
 	std::map<util::h256, std::string> const& _smtlib2Responses,
 	ReadCallback::Callback const& _smtCallback,
 	ModelCheckerSettings _settings,
 	CharStreamProvider const& _charStreamProvider
 ):
-	SMTEncoder(_context, _settings, _errorReporter, _unsupportedErrorReporter, _charStreamProvider),
+	SMTEncoder(_context, _settings, _errorReporter, _unsupportedErrorReporter, _provedSafeReporter, _charStreamProvider),
 	m_smtlib2Responses(_smtlib2Responses),
 	m_smtCallback(_smtCallback)
 {
@@ -2116,17 +2117,22 @@ void CHC::checkVerificationTargets()
 		);
 
 	if (!m_settings.showProvedSafe && !m_safeTargets.empty())
+	{
+		std::size_t provedSafeNum = 0;
+		for (auto&& [_, targets]: m_safeTargets)
+			provedSafeNum += targets.size();
 		m_errorReporter.info(
 			1391_error,
 			"CHC: " +
-			std::to_string(m_safeTargets.size()) +
+			std::to_string(provedSafeNum) +
 			" verification condition(s) proved safe!" +
 			" Enable the model checker option \"show proved safe\" to see all of them."
 		);
+	}
 	else if (m_settings.showProvedSafe)
 		for (auto const& [node, targets]: m_safeTargets)
 			for (auto const& target: targets)
-				m_errorReporter.info(
+				m_provedSafeReporter.info(
 					9576_error,
 					node->location(),
 					"CHC: " +

libsolidity/formal/CHC.h

@@ -58,6 +58,7 @@ class CHC: public SMTEncoder
 		smt::EncodingContext& _context,
 		langutil::UniqueErrorReporter& _errorReporter,
 		langutil::UniqueErrorReporter& _unsupportedErrorReporter,
+		langutil::ErrorReporter& _provedSafeReporter,
 		std::map<util::h256, std::string> const& _smtlib2Responses,
 		ReadCallback::Callback const& _smtCallback,
 		ModelCheckerSettings _settings,
@@ -77,14 +78,25 @@ class CHC: public SMTEncoder
 		}
 	};
 
+	struct SafeTargetsCompare
+	{
+		bool operator()(CHCVerificationTarget const & _lhs, CHCVerificationTarget const & _rhs) const
+		{
+			if (_lhs.errorNode->id() == _rhs.errorNode->id())
+				return _lhs.type  < _rhs.type;
+			else
+				return _lhs.errorNode->id() == _rhs.errorNode->id();
+		}
+	};
+
 	struct ReportTargetInfo
 	{
 		langutil::ErrorId error;
 		langutil::SourceLocation location;
 		std::string message;
 	};
 
-	std::map<ASTNode const*, std::set<CHCVerificationTarget>, smt::EncodingContext::IdCompare> const& safeTargets() const { return m_safeTargets; }
+	std::map<ASTNode const*, std::set<CHCVerificationTarget, SafeTargetsCompare>, 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.
@@ -423,7 +435,7 @@ class CHC: public SMTEncoder
 	std::map<unsigned, CHCVerificationTarget> m_verificationTargets;
 
 	/// Targets proved safe.
-	std::map<ASTNode const*, std::set<CHCVerificationTarget>, smt::EncodingContext::IdCompare> m_safeTargets;
+	std::map<ASTNode const*, std::set<CHCVerificationTarget, SafeTargetsCompare>, smt::EncodingContext::IdCompare> m_safeTargets;
 	/// Targets proved unsafe.
 	std::map<ASTNode const*, std::map<VerificationTargetType, ReportTargetInfo>, smt::EncodingContext::IdCompare> m_unsafeTargets;
 	/// Targets not proved.

libsolidity/formal/ModelChecker.cpp

@@ -43,10 +43,11 @@ ModelChecker::ModelChecker(
 	ReadCallback::Callback const& _smtCallback
 ):
 	m_errorReporter(_errorReporter),
+	m_provedSafeReporter(m_provedSafeLogs),
 	m_settings(std::move(_settings)),
 	m_context(),
-	m_bmc(m_context, m_uniqueErrorReporter, m_unsupportedErrorReporter, _smtlib2Responses, _smtCallback, m_settings, _charStreamProvider),
-	m_chc(m_context, m_uniqueErrorReporter, m_unsupportedErrorReporter, _smtlib2Responses, _smtCallback, m_settings, _charStreamProvider)
+	m_bmc(m_context, m_uniqueErrorReporter, m_unsupportedErrorReporter, m_provedSafeReporter, _smtlib2Responses, _smtCallback, m_settings, _charStreamProvider),
+	m_chc(m_context, m_uniqueErrorReporter, m_unsupportedErrorReporter, m_provedSafeReporter, _smtlib2Responses, _smtCallback, m_settings, _charStreamProvider)
 {
 }
 
@@ -151,6 +152,12 @@ void ModelChecker::analyze(SourceUnit const& _source)
 
 	m_errorReporter.append(m_uniqueErrorReporter.errors());
 	m_uniqueErrorReporter.clear();
+
+	if (m_settings.showProvedSafe)
+	{
+		m_errorReporter.append(m_provedSafeReporter.errors());
+		m_provedSafeReporter.clear();
+	}
 }
 
 std::vector<std::string> ModelChecker::unhandledQueries()

libsolidity/formal/ModelChecker.h

@@ -95,6 +95,12 @@ class ModelChecker
 	/// to m_errorReporter at the end of the analysis.
 	langutil::UniqueErrorReporter m_unsupportedErrorReporter;
 
+	langutil::ErrorList m_provedSafeLogs;
+	/// Used by SMTEncoder, BMC and CHC to accumulate info about proved targets.
+	/// This is local to ModelChecker, so needs to be appended
+	/// to m_errorReporter at the end of the analysis.
+	langutil::ErrorReporter m_provedSafeReporter;
+
 	ModelCheckerSettings m_settings;
 
 	/// Stores the context of the encoding.

libsolidity/formal/SMTEncoder.cpp

@@ -51,10 +51,12 @@ SMTEncoder::SMTEncoder(
 	ModelCheckerSettings _settings,
 	UniqueErrorReporter& _errorReporter,
 	UniqueErrorReporter& _unsupportedErrorReporter,
+	ErrorReporter& _provedSafeReporter,
 	langutil::CharStreamProvider const& _charStreamProvider
 ):
 	m_errorReporter(_errorReporter),
 	m_unsupportedErrors(_unsupportedErrorReporter),
+	m_provedSafeReporter(_provedSafeReporter),
 	m_context(_context),
 	m_settings(std::move(_settings)),
 	m_charStreamProvider(_charStreamProvider)

libsolidity/formal/SMTEncoder.h

@@ -57,6 +57,7 @@ class SMTEncoder: public ASTConstVisitor
 		ModelCheckerSettings _settings,
 		langutil::UniqueErrorReporter& _errorReporter,
 		langutil::UniqueErrorReporter& _unsupportedErrorReporter,
+		langutil::ErrorReporter& _provedSafeReporter,
 		langutil::CharStreamProvider const& _charStreamProvider
 	);
 
@@ -463,6 +464,7 @@ class SMTEncoder: public ASTConstVisitor
 
 	langutil::UniqueErrorReporter& m_errorReporter;
 	langutil::UniqueErrorReporter& m_unsupportedErrors;
+	langutil::ErrorReporter& m_provedSafeReporter;
 
 	/// Stores the current function/modifier call/invocation path.
 	std::vector<CallStackEntry> m_callStack;

scripts/error_codes.py

@@ -205,7 +205,6 @@ def examine_id_coverage(top_dir, source_id_to_file_names, new_ids_only=False):
         "7053", # Unimplemented feature error (parsing stage), currently has no tests
         "1180", # SMTChecker, covered by CL tests
         "2339", # SMTChecker, covered by CL tests
-        "2961", # SMTChecker, covered by CL tests
         "6240", # SMTChecker, covered by CL tests
     }
     assert len(test_ids & white_ids) == 0, "The sets are not supposed to intersect"