group unsupported warnings

Changelog.md

@@ -5,6 +5,7 @@ Language Features:
 
 Compiler Features:
  * SMTChecker: Properties that are proved safe are now reported explicitly at the end of the analysis. By default, only the number of safe properties is shown. The CLI option ``--model-checker-show-proved-safe`` and the JSON option ``settings.modelChecker.showProvedSafe`` can be enabled to show the full list of safe properties.
+ * SMTChecker: Group all messages about unsupported language features in a single warning. The CLI option ``--model-checker-show-unsupported`` and the JSON option ``settings.modelChecker.showUnsupported`` can be enabled to show the full list.
 
 
 Bugfixes:

docs/smtchecker.rst

@@ -499,6 +499,23 @@ how many unproved targets there are. If the user wishes to see all the specific
 unproved targets, the CLI option ``--model-checker-show-unproved`` and
 the JSON option ``settings.modelChecker.showUnproved = true`` can be used.
 
+Unsupported Language Features
+=============================
+
+Certain Solidity language features are not completely supported by the SMT
+encoding that the SMTChecker applies, for example assembly blocks.
+The unsupported construct is abstracted via overapproximation to preserve
+soundness, meaning any properties reported safe are safe even though this
+feature is unsupported.
+However such abstraction may cause false positives when the target properties
+depend on the precise behavior of the unsupported feature.
+If the encoder encounters such cases it will by default report a generic warning
+stating how many unsupported features it has seen.
+If the user wishes to see all the specific unsupported features, the CLI option
+``--model-checker-show-unsupported`` and the JSON option
+``settings.modelChecker.showUnsupported = true`` can be used, where their default
+value is ``false``.
+
 Verified Contracts
 ==================
 

docs/using-the-compiler.rst

@@ -443,6 +443,8 @@ Input Description
           "showProved": true,
           // Choose whether to output all unproved targets. The default is `false`.
           "showUnproved": true,
+          // Choose whether to output all unsupported language features. The default is `false`.
+          "showUnsupported": true,
           // Choose which solvers should be used, if available.
           // See the Formal Verification section for the solvers description.
           "solvers": ["cvc4", "smtlib2", "z3"],

liblangutil/UniqueErrorReporter.h

@@ -33,6 +33,11 @@ class UniqueErrorReporter
 public:
 	UniqueErrorReporter(): m_errorReporter(m_uniqueErrors) {}
 
+	void append(UniqueErrorReporter const& _other)
+	{
+		m_errorReporter.append(_other.m_errorReporter.errors());
+	}
+
 	void warning(ErrorId _error, SourceLocation const& _location, std::string const& _description)
 	{
 		if (!seen(_error, _location, _description))

libsolidity/formal/BMC.cpp

@@ -39,12 +39,13 @@ using namespace solidity::frontend;
 BMC::BMC(
 	smt::EncodingContext& _context,
 	UniqueErrorReporter& _errorReporter,
+	UniqueErrorReporter& _unsupportedErrorReporter,
 	map<h256, string> const& _smtlib2Responses,
 	ReadCallback::Callback const& _smtCallback,
 	ModelCheckerSettings _settings,
 	CharStreamProvider const& _charStreamProvider
 ):
-	SMTEncoder(_context, _settings, _errorReporter, _charStreamProvider),
+	SMTEncoder(_context, _settings, _errorReporter, _unsupportedErrorReporter, _charStreamProvider),
 	m_interface(make_unique<smtutil::SMTPortfolio>(_smtlib2Responses, _smtCallback, _settings.solvers, _settings.timeout))
 {
 #if defined (HAVE_Z3) || defined (HAVE_CVC4)
@@ -593,7 +594,7 @@ void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall)
 		// The processing happens in SMT Encoder, but we need to prevent the resetting of the state variables.
 	}
 	else if (funType.kind() == FunctionType::Kind::Internal)
-		m_errorReporter.warning(
+		m_unsupportedErrors.warning(
 			5729_error,
 			_funCall.location(),
 			"BMC does not yet implement this type of function call."

libsolidity/formal/BMC.h

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

libsolidity/formal/CHC.cpp

@@ -62,12 +62,13 @@ using namespace solidity::frontend::smt;
 CHC::CHC(
 	EncodingContext& _context,
 	UniqueErrorReporter& _errorReporter,
+	UniqueErrorReporter& _unsupportedErrorReporter,
 	map<util::h256, string> const& _smtlib2Responses,
 	ReadCallback::Callback const& _smtCallback,
 	ModelCheckerSettings _settings,
 	CharStreamProvider const& _charStreamProvider
 ):
-	SMTEncoder(_context, _settings, _errorReporter, _charStreamProvider),
+	SMTEncoder(_context, _settings, _errorReporter, _unsupportedErrorReporter, _charStreamProvider),
 	m_smtlib2Responses(_smtlib2Responses),
 	m_smtCallback(_smtCallback)
 {

libsolidity/formal/CHC.h

@@ -57,6 +57,7 @@ class CHC: public SMTEncoder
 	CHC(
 		smt::EncodingContext& _context,
 		langutil::UniqueErrorReporter& _errorReporter,
+		langutil::UniqueErrorReporter& _unsupportedErrorReporter,
 		std::map<util::h256, std::string> const& _smtlib2Responses,
 		ReadCallback::Callback const& _smtCallback,
 		ModelCheckerSettings _settings,

libsolidity/formal/ModelChecker.cpp

@@ -48,8 +48,8 @@ ModelChecker::ModelChecker(
 	m_errorReporter(_errorReporter),
 	m_settings(std::move(_settings)),
 	m_context(),
-	m_bmc(m_context, m_uniqueErrorReporter, _smtlib2Responses, _smtCallback, m_settings, _charStreamProvider),
-	m_chc(m_context, m_uniqueErrorReporter, _smtlib2Responses, _smtCallback, m_settings, _charStreamProvider)
+	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)
 {
 }
 
@@ -137,6 +137,21 @@ void ModelChecker::analyze(SourceUnit const& _source)
 	if (m_settings.engine.bmc)
 		m_bmc.analyze(_source, solvedTargets);
 
+	if (m_settings.showUnsupported)
+	{
+		m_errorReporter.append(m_unsupportedErrorReporter.errors());
+		m_unsupportedErrorReporter.clear();
+	}
+	else if (!m_unsupportedErrorReporter.errors().empty())
+		m_errorReporter.warning(
+			5724_error,
+			{},
+			"SMTChecker: " +
+			to_string(m_unsupportedErrorReporter.errors().size()) +
+			" unsupported language feature(s)."
+			" Enable the model checker option \"show unsupported\" to see all of them."
+		);
+
 	m_errorReporter.append(m_uniqueErrorReporter.errors());
 	m_uniqueErrorReporter.clear();
 }

libsolidity/formal/ModelChecker.h

@@ -89,6 +89,12 @@ class ModelChecker
 	/// to m_errorReporter at the end of the analysis.
 	langutil::UniqueErrorReporter m_uniqueErrorReporter;
 
+	/// Used by SMTEncoder, BMC and CHC to accumulate unsupported
+	/// warnings and avoid duplicates.
+	/// This is local to ModelChecker, so needs to be appended
+	/// to m_errorReporter at the end of the analysis.
+	langutil::UniqueErrorReporter m_unsupportedErrorReporter;
+
 	ModelCheckerSettings m_settings;
 
 	/// Stores the context of the encoding.

libsolidity/formal/ModelCheckerSettings.h

@@ -170,6 +170,7 @@ struct ModelCheckerSettings
 	ModelCheckerInvariants invariants = ModelCheckerInvariants::Default();
 	bool showProvedSafe = false;
 	bool showUnproved = false;
+	bool showUnsupported = false;
 	smtutil::SMTSolverChoice solvers = smtutil::SMTSolverChoice::Z3();
 	ModelCheckerTargets targets = ModelCheckerTargets::Default();
 	std::optional<unsigned> timeout;
@@ -185,6 +186,7 @@ struct ModelCheckerSettings
 			invariants == _other.invariants &&
 			showProvedSafe == _other.showProvedSafe &&
 			showUnproved == _other.showUnproved &&
+			showUnsupported == _other.showUnsupported &&
 			solvers == _other.solvers &&
 			targets == _other.targets &&
 			timeout == _other.timeout;

libsolidity/formal/SMTEncoder.cpp

@@ -49,9 +49,11 @@ SMTEncoder::SMTEncoder(
 	smt::EncodingContext& _context,
 	ModelCheckerSettings _settings,
 	UniqueErrorReporter& _errorReporter,
+	UniqueErrorReporter& _unsupportedErrorReporter,
 	langutil::CharStreamProvider const& _charStreamProvider
 ):
 	m_errorReporter(_errorReporter),
+	m_unsupportedErrors(_unsupportedErrorReporter),
 	m_context(_context),
 	m_settings(std::move(_settings)),
 	m_charStreamProvider(_charStreamProvider)
@@ -339,7 +341,7 @@ bool SMTEncoder::visit(InlineAssembly const& _inlineAsm)
 		m_context.resetVariable(*var);
 	}
 
-	m_errorReporter.warning(
+	m_unsupportedErrors.warning(
 		7737_error,
 		_inlineAsm.location(),
 		"Inline assembly may cause SMTChecker to produce spurious warnings (false positives)."
@@ -458,7 +460,7 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
 	if (*_op.annotation().userDefinedFunction)
 	{
 		// TODO: Implement user-defined operators properly.
-		m_errorReporter.warning(
+		m_unsupportedErrors.warning(
 			6156_error,
 			_op.location(),
 			"User-defined operators are not yet supported by SMTChecker. "s +
@@ -560,7 +562,7 @@ void SMTEncoder::endVisit(BinaryOperation const& _op)
 	if (*_op.annotation().userDefinedFunction)
 	{
 		// TODO: Implement user-defined operators properly.
-		m_errorReporter.warning(
+		m_unsupportedErrors.warning(
 			6756_error,
 			_op.location(),
 			"User-defined operators are not yet supported by SMTChecker. "s +
@@ -726,7 +728,7 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
 		return;
 	case FunctionType::Kind::Creation:
 		if (!m_settings.engine.chc || !m_settings.externalCalls.isTrusted())
-			m_errorReporter.warning(
+			m_unsupportedErrors.warning(
 				8729_error,
 				_funCall.location(),
 				"Contract deployment is only supported in the trusted mode for external calls"
@@ -737,7 +739,7 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
 	case FunctionType::Kind::BareCallCode:
 	case FunctionType::Kind::BareDelegateCall:
 	default:
-		m_errorReporter.warning(
+		m_unsupportedErrors.warning(
 			4588_error,
 			_funCall.location(),
 			"Assertion checker does not yet implement this type of function call."
@@ -1406,7 +1408,7 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
 				else
 					// NOTE: supporting name, creationCode, runtimeCode would be easy enough, but the bytes/string they return are not
 					//       at all usable in the SMT checker currently
-					m_errorReporter.warning(
+					m_unsupportedErrors.warning(
 						7507_error,
 						_memberAccess.location(),
 						"Assertion checker does not yet support this expression."
@@ -1497,7 +1499,7 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
 		}
 	}
 
-	m_errorReporter.warning(
+	m_unsupportedErrors.warning(
 		7650_error,
 		_memberAccess.location(),
 		"Assertion checker does not yet support this expression."
@@ -1628,7 +1630,7 @@ void SMTEncoder::indexOrMemberAssignment(Expression const& _expr, smtutil::Expre
 				structType && structType->recursive()
 			)
 			{
-				m_errorReporter.warning(
+				m_unsupportedErrors.warning(
 					4375_error,
 					memberAccess->location(),
 					"Assertion checker does not support recursive structs."
@@ -1742,7 +1744,7 @@ void SMTEncoder::defineGlobalVariable(string const& _name, Expression const& _ex
 	{
 		bool abstract = m_context.createGlobalSymbol(_name, _expr);
 		if (abstract)
-			m_errorReporter.warning(
+			m_unsupportedErrors.warning(
 				1695_error,
 				_expr.location(),
 				"Assertion checker does not yet support this global variable."
@@ -1793,7 +1795,7 @@ void SMTEncoder::arithmeticOperation(BinaryOperation const& _op)
 		break;
 	}
 	default:
-		m_errorReporter.warning(
+		m_unsupportedErrors.warning(
 			5188_error,
 			_op.location(),
 			"Assertion checker does not yet implement this operator."
@@ -1980,7 +1982,7 @@ void SMTEncoder::compareOperation(BinaryOperation const& _op)
 		defineExpr(_op, *value);
 	}
 	else
-		m_errorReporter.warning(
+		m_unsupportedErrors.warning(
 			7229_error,
 			_op.location(),
 			"Assertion checker does not yet implement the type " + _op.annotation().commonType->toString() + " for comparisons"
@@ -2507,7 +2509,7 @@ bool SMTEncoder::createVariable(VariableDeclaration const& _varDecl)
 	bool abstract = m_context.createVariable(_varDecl);
 	if (abstract)
 	{
-		m_errorReporter.warning(
+		m_unsupportedErrors.warning(
 			8115_error,
 			_varDecl.location(),
 			"Assertion checker does not yet support the type of this variable."
@@ -2521,7 +2523,7 @@ smtutil::Expression SMTEncoder::expr(Expression const& _e, Type const* _targetTy
 {
 	if (!m_context.knownExpression(_e))
 	{
-		m_errorReporter.warning(6031_error, _e.location(), "Internal error: Expression undefined for SMT solver." );
+		m_unsupportedErrors.warning(6031_error, _e.location(), "Internal error: Expression undefined for SMT solver." );
 		createExpr(_e);
 	}
 
@@ -2532,7 +2534,7 @@ void SMTEncoder::createExpr(Expression const& _e)
 {
 	bool abstract = m_context.createExpression(_e);
 	if (abstract)
-		m_errorReporter.warning(
+		m_unsupportedErrors.warning(
 			8364_error,
 			_e.location(),
 			"Assertion checker does not yet implement type " + _e.annotation().type->toString()

libsolidity/formal/SMTEncoder.h

@@ -56,6 +56,7 @@ class SMTEncoder: public ASTConstVisitor
 		smt::EncodingContext& _context,
 		ModelCheckerSettings _settings,
 		langutil::UniqueErrorReporter& _errorReporter,
+		langutil::UniqueErrorReporter& _unsupportedErrorReporter,
 		langutil::CharStreamProvider const& _charStreamProvider
 	);
 
@@ -440,6 +441,7 @@ class SMTEncoder: public ASTConstVisitor
 	bool m_checked = true;
 
 	langutil::UniqueErrorReporter& m_errorReporter;
+	langutil::UniqueErrorReporter& m_unsupportedErrors;
 
 	/// Stores the current function/modifier call/invocation path.
 	std::vector<CallStackEntry> m_callStack;

libsolidity/interface/StandardCompiler.cpp

@@ -445,7 +445,7 @@ std::optional<Json::Value> checkSettingsKeys(Json::Value const& _input)
 
 std::optional<Json::Value> checkModelCheckerSettingsKeys(Json::Value const& _input)
 {
-	static set<string> keys{"contracts", "divModNoSlacks", "engine", "extCalls", "invariants", "showProvedSafe", "showUnproved", "solvers", "targets", "timeout"};
+	static set<string> keys{"contracts", "divModNoSlacks", "engine", "extCalls", "invariants", "showProvedSafe", "showUnproved", "showUnsupported", "solvers", "targets", "timeout"};
 	return checkKeys(_input, keys, "modelChecker");
 }
 
@@ -1063,6 +1063,14 @@ std::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompiler:
 		ret.modelCheckerSettings.showUnproved = showUnproved.asBool();
 	}
 
+	if (modelCheckerSettings.isMember("showUnsupported"))
+	{
+		auto const& showUnsupported = modelCheckerSettings["showUnsupported"];
+		if (!showUnsupported.isBool())
+			return formatFatalError(Error::Type::JSONError, "settings.modelChecker.showUnsupported must be a Boolean value.");
+		ret.modelCheckerSettings.showUnsupported = showUnsupported.asBool();
+	}
+
 	if (modelCheckerSettings.isMember("solvers"))
 	{
 		auto const& solversArray = modelCheckerSettings["solvers"];

solc/CommandLineParser.cpp

@@ -73,6 +73,7 @@ static string const g_strModelCheckerExtCalls = "model-checker-ext-calls";
 static string const g_strModelCheckerInvariants = "model-checker-invariants";
 static string const g_strModelCheckerShowProvedSafe = "model-checker-show-proved-safe";
 static string const g_strModelCheckerShowUnproved = "model-checker-show-unproved";
+static string const g_strModelCheckerShowUnsupported = "model-checker-show-unsupported";
 static string const g_strModelCheckerSolvers = "model-checker-solvers";
 static string const g_strModelCheckerTargets = "model-checker-targets";
 static string const g_strModelCheckerTimeout = "model-checker-timeout";
@@ -854,6 +855,10 @@ General Information)").c_str(),
 			g_strModelCheckerShowUnproved.c_str(),
 			"Show all unproved targets separately."
 		)
+		(
+			g_strModelCheckerShowUnsupported.c_str(),
+			"Show all unsupported language features separately."
+		)
 		(
 			g_strModelCheckerSolvers.c_str(),
 			po::value<string>()->value_name("cvc4,eld,z3,smtlib2")->default_value("z3"),
@@ -960,6 +965,7 @@ void CommandLineParser::processArgs()
 		{g_strMetadataHash, {InputMode::Compiler, InputMode::CompilerWithASTImport}},
 		{g_strModelCheckerShowProvedSafe, {InputMode::Compiler, InputMode::CompilerWithASTImport}},
 		{g_strModelCheckerShowUnproved, {InputMode::Compiler, InputMode::CompilerWithASTImport}},
+		{g_strModelCheckerShowUnsupported, {InputMode::Compiler, InputMode::CompilerWithASTImport}},
 		{g_strModelCheckerDivModNoSlacks, {InputMode::Compiler, InputMode::CompilerWithASTImport}},
 		{g_strModelCheckerEngine, {InputMode::Compiler, InputMode::CompilerWithASTImport}},
 		{g_strModelCheckerInvariants, {InputMode::Compiler, InputMode::CompilerWithASTImport}},
@@ -1326,6 +1332,9 @@ void CommandLineParser::processArgs()
 	if (m_args.count(g_strModelCheckerShowUnproved))
 		m_options.modelChecker.settings.showUnproved = true;
 
+	if (m_args.count(g_strModelCheckerShowUnsupported))
+		m_options.modelChecker.settings.showUnsupported = true;
+
 	if (m_args.count(g_strModelCheckerSolvers))
 	{
 		string solversStr = m_args[g_strModelCheckerSolvers].as<string>();
@@ -1356,6 +1365,7 @@ void CommandLineParser::processArgs()
 		m_args.count(g_strModelCheckerInvariants) ||
 		m_args.count(g_strModelCheckerShowProvedSafe) ||
 		m_args.count(g_strModelCheckerShowUnproved) ||
+		m_args.count(g_strModelCheckerShowUnsupported) ||
 		m_args.count(g_strModelCheckerSolvers) ||
 		m_args.count(g_strModelCheckerTargets) ||
 		m_args.count(g_strModelCheckerTimeout);