From aacbe72079f595a02d6375b53d60a9390fba2300 Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Mon, 6 Mar 2023 14:19:58 +0100 Subject: [PATCH] group unsupported warnings --- Changelog.md | 1 + docs/smtchecker.rst | 17 +++++++++++ docs/using-the-compiler.rst | 2 ++ liblangutil/UniqueErrorReporter.h | 5 ++++ libsolidity/formal/BMC.cpp | 5 ++-- libsolidity/formal/BMC.h | 1 + libsolidity/formal/CHC.cpp | 3 +- libsolidity/formal/CHC.h | 1 + libsolidity/formal/ModelChecker.cpp | 19 ++++++++++-- libsolidity/formal/ModelChecker.h | 6 ++++ libsolidity/formal/ModelCheckerSettings.h | 2 ++ libsolidity/formal/SMTEncoder.cpp | 30 ++++++++++--------- libsolidity/formal/SMTEncoder.h | 2 ++ libsolidity/interface/StandardCompiler.cpp | 10 ++++++- solc/CommandLineParser.cpp | 10 +++++++ test/libsolidity/SMTCheckerTest.cpp | 8 +++++ ...unction_type_to_function_type_internal.sol | 4 +-- .../unsupported/assembly_1.sol | 18 +++++++++++ test/solc/CommandLineParser.cpp | 3 ++ test/tools/fuzzer_common.cpp | 1 + 20 files changed, 126 insertions(+), 22 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/unsupported/assembly_1.sol diff --git a/Changelog.md b/Changelog.md index a2c485691..5cb2b7095 100644 --- a/Changelog.md +++ b/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: diff --git a/docs/smtchecker.rst b/docs/smtchecker.rst index 27d2cfaa1..3ad700a30 100644 --- a/docs/smtchecker.rst +++ b/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 ================== diff --git a/docs/using-the-compiler.rst b/docs/using-the-compiler.rst index 4dc385627..2eac2d157 100644 --- a/docs/using-the-compiler.rst +++ b/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"], diff --git a/liblangutil/UniqueErrorReporter.h b/liblangutil/UniqueErrorReporter.h index ebcb8d976..902068b8f 100644 --- a/liblangutil/UniqueErrorReporter.h +++ b/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)) diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index caca4f6be..e0a5f312b 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -39,12 +39,13 @@ using namespace solidity::frontend; BMC::BMC( smt::EncodingContext& _context, UniqueErrorReporter& _errorReporter, + UniqueErrorReporter& _unsupportedErrorReporter, map 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(_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." diff --git a/libsolidity/formal/BMC.h b/libsolidity/formal/BMC.h index 9c106689e..9a8242047 100644 --- a/libsolidity/formal/BMC.h +++ b/libsolidity/formal/BMC.h @@ -60,6 +60,7 @@ public: BMC( smt::EncodingContext& _context, langutil::UniqueErrorReporter& _errorReporter, + langutil::UniqueErrorReporter& _unsupportedErrorReporter, std::map const& _smtlib2Responses, ReadCallback::Callback const& _smtCallback, ModelCheckerSettings _settings, diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 0281a4cbd..3d93bf599 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -62,12 +62,13 @@ using namespace solidity::frontend::smt; CHC::CHC( EncodingContext& _context, UniqueErrorReporter& _errorReporter, + UniqueErrorReporter& _unsupportedErrorReporter, map 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) { diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index 5f6b71b39..27bdaebf2 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -57,6 +57,7 @@ public: CHC( smt::EncodingContext& _context, langutil::UniqueErrorReporter& _errorReporter, + langutil::UniqueErrorReporter& _unsupportedErrorReporter, std::map const& _smtlib2Responses, ReadCallback::Callback const& _smtCallback, ModelCheckerSettings _settings, diff --git a/libsolidity/formal/ModelChecker.cpp b/libsolidity/formal/ModelChecker.cpp index 5ec06d107..bc97c5534 100644 --- a/libsolidity/formal/ModelChecker.cpp +++ b/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(); } diff --git a/libsolidity/formal/ModelChecker.h b/libsolidity/formal/ModelChecker.h index 2625bd1e0..4c795fa70 100644 --- a/libsolidity/formal/ModelChecker.h +++ b/libsolidity/formal/ModelChecker.h @@ -89,6 +89,12 @@ private: /// 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. diff --git a/libsolidity/formal/ModelCheckerSettings.h b/libsolidity/formal/ModelCheckerSettings.h index 023d7800f..fafb2cdac 100644 --- a/libsolidity/formal/ModelCheckerSettings.h +++ b/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 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; diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index e8598392f..8f22ab824 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/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() diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 47e51b54d..c16569686 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -56,6 +56,7 @@ public: smt::EncodingContext& _context, ModelCheckerSettings _settings, langutil::UniqueErrorReporter& _errorReporter, + langutil::UniqueErrorReporter& _unsupportedErrorReporter, langutil::CharStreamProvider const& _charStreamProvider ); @@ -440,6 +441,7 @@ protected: bool m_checked = true; langutil::UniqueErrorReporter& m_errorReporter; + langutil::UniqueErrorReporter& m_unsupportedErrors; /// Stores the current function/modifier call/invocation path. std::vector m_callStack; diff --git a/libsolidity/interface/StandardCompiler.cpp b/libsolidity/interface/StandardCompiler.cpp index 3a16551eb..1511b2179 100644 --- a/libsolidity/interface/StandardCompiler.cpp +++ b/libsolidity/interface/StandardCompiler.cpp @@ -445,7 +445,7 @@ std::optional checkSettingsKeys(Json::Value const& _input) std::optional checkModelCheckerSettingsKeys(Json::Value const& _input) { - static set keys{"contracts", "divModNoSlacks", "engine", "extCalls", "invariants", "showProvedSafe", "showUnproved", "solvers", "targets", "timeout"}; + static set keys{"contracts", "divModNoSlacks", "engine", "extCalls", "invariants", "showProvedSafe", "showUnproved", "showUnsupported", "solvers", "targets", "timeout"}; return checkKeys(_input, keys, "modelChecker"); } @@ -1063,6 +1063,14 @@ std::variant 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"]; diff --git a/solc/CommandLineParser.cpp b/solc/CommandLineParser.cpp index 8fd245402..f7c99fd38 100644 --- a/solc/CommandLineParser.cpp +++ b/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()->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(); @@ -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); diff --git a/test/libsolidity/SMTCheckerTest.cpp b/test/libsolidity/SMTCheckerTest.cpp index 93590994a..949589527 100644 --- a/test/libsolidity/SMTCheckerTest.cpp +++ b/test/libsolidity/SMTCheckerTest.cpp @@ -47,6 +47,14 @@ SMTCheckerTest::SMTCheckerTest(string const& _filename): SyntaxTest(_filename, E else BOOST_THROW_EXCEPTION(runtime_error("Invalid SMT \"show unproved\" choice.")); + auto const& showUnsupported = m_reader.stringSetting("SMTShowUnsupported", "yes"); + if (showUnsupported == "no") + m_modelCheckerSettings.showUnsupported = false; + else if (showUnsupported == "yes") + m_modelCheckerSettings.showUnsupported = true; + else + BOOST_THROW_EXCEPTION(runtime_error("Invalid SMT \"show unsupported\" choice.")); + m_modelCheckerSettings.solvers = smtutil::SMTSolverChoice::None(); auto const& choice = m_reader.stringSetting("SMTSolvers", "z3"); if (choice == "none") diff --git a/test/libsolidity/smtCheckerTests/typecast/function_type_to_function_type_internal.sol b/test/libsolidity/smtCheckerTests/typecast/function_type_to_function_type_internal.sol index 6596c6f59..2d3448ee7 100644 --- a/test/libsolidity/smtCheckerTests/typecast/function_type_to_function_type_internal.sol +++ b/test/libsolidity/smtCheckerTests/typecast/function_type_to_function_type_internal.sol @@ -16,7 +16,7 @@ contract C { // Warning 6031: (182-186): Internal error: Expression undefined for SMT solver. // Warning 6031: (190-194): Internal error: Expression undefined for SMT solver. // Warning 7229: (206-212): Assertion checker does not yet implement the type function (uint256) returns (uint256) for comparisons -// Warning 6328: (175-195): CHC: Assertion violation happens here.\nCounterexample:\na = 0, b = 0\n\nTransaction trace:\nC.constructor()\nState: a = 0, b = 0\nC.g()\n C.f(0, 0) -- internal call -// Warning 6328: (199-213): CHC: Assertion violation happens here.\nCounterexample:\na = 0, b = 0\n\nTransaction trace:\nC.constructor()\nState: a = 0, b = 0\nC.g()\n C.f(0, 0) -- internal call // Warning 5729: (182-186): BMC does not yet implement this type of function call. // Warning 5729: (190-194): BMC does not yet implement this type of function call. +// Warning 6328: (175-195): CHC: Assertion violation happens here. +// Warning 6328: (199-213): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/unsupported/assembly_1.sol b/test/libsolidity/smtCheckerTests/unsupported/assembly_1.sol new file mode 100644 index 000000000..4c7ded319 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/unsupported/assembly_1.sol @@ -0,0 +1,18 @@ +contract C { + function f(uint x, uint y) public pure { + assembly {} + assert(x < y); + } + + function g(uint x, uint y) public pure { + assembly {} + assert(x < y); + } +} +// ==== +// SMTEngine: all +// SMTShowUnsupported: no +// ---- +// Warning 5724: SMTChecker: 2 unsupported language feature(s). Enable the model checker option "show unsupported" to see all of them. +// Warning 6328: (86-99): CHC: Assertion violation happens here. +// Warning 6328: (181-194): CHC: Assertion violation happens here. diff --git a/test/solc/CommandLineParser.cpp b/test/solc/CommandLineParser.cpp index 1dc180ab4..6fdecd7fa 100644 --- a/test/solc/CommandLineParser.cpp +++ b/test/solc/CommandLineParser.cpp @@ -149,6 +149,7 @@ BOOST_AUTO_TEST_CASE(cli_mode_options) "--model-checker-invariants=contract,reentrancy", "--model-checker-show-proved-safe", "--model-checker-show-unproved", + "--model-checker-show-unsupported", "--model-checker-solvers=z3,smtlib2", "--model-checker-targets=underflow,divByZero", "--model-checker-timeout=5", @@ -217,6 +218,7 @@ BOOST_AUTO_TEST_CASE(cli_mode_options) {{InvariantType::Contract, InvariantType::Reentrancy}}, true, true, + true, {false, false, true, true}, {{VerificationTargetType::Underflow, VerificationTargetType::DivByZero}}, 5, @@ -414,6 +416,7 @@ BOOST_AUTO_TEST_CASE(invalid_options_input_modes_combinations) {"--metadata-hash=swarm", {"--assemble", "--yul", "--strict-assembly", "--standard-json", "--link"}}, {"--model-checker-show-proved-safe", {"--assemble", "--yul", "--strict-assembly", "--standard-json", "--link"}}, {"--model-checker-show-unproved", {"--assemble", "--yul", "--strict-assembly", "--standard-json", "--link"}}, + {"--model-checker-show-unsupported", {"--assemble", "--yul", "--strict-assembly", "--standard-json", "--link"}}, {"--model-checker-div-mod-no-slacks", {"--assemble", "--yul", "--strict-assembly", "--standard-json", "--link"}}, {"--model-checker-engine=bmc", {"--assemble", "--yul", "--strict-assembly", "--standard-json", "--link"}}, {"--model-checker-invariants=contract,reentrancy", {"--assemble", "--yul", "--strict-assembly", "--standard-json", "--link"}}, diff --git a/test/tools/fuzzer_common.cpp b/test/tools/fuzzer_common.cpp index 185f547c4..51b8a0e68 100644 --- a/test/tools/fuzzer_common.cpp +++ b/test/tools/fuzzer_common.cpp @@ -112,6 +112,7 @@ void FuzzerUtil::testCompiler( frontend::ModelCheckerInvariants::All(), /*showProvedSafe=*/false, /*showUnproved=*/false, + /*showUnsupported=*/false, smtutil::SMTSolverChoice::All(), frontend::ModelCheckerTargets::Default(), /*timeout=*/1