cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

group unsupported warnings

Browse Source
This commit is contained in:
Leo Alt 2023-03-06 14:19:58 +01:00
parent 0aa85153e5
commit aacbe72079
20 changed files with 126 additions and 22 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -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:

17
docs/smtchecker.rst
View File

@ -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
==================

2
docs/using-the-compiler.rst
View File

@ -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"],

5
liblangutil/UniqueErrorReporter.h
View File

@ -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))

5
libsolidity/formal/BMC.cpp
View File

@ -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."

1
libsolidity/formal/BMC.h
View File

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

3
libsolidity/formal/CHC.cpp
View File

@ -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)
{

1
libsolidity/formal/CHC.h
View File

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

19
libsolidity/formal/ModelChecker.cpp
View File

@ -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();
}

6
libsolidity/formal/ModelChecker.h
View File

@ -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.

2
libsolidity/formal/ModelCheckerSettings.h
View File

@ -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;

30
libsolidity/formal/SMTEncoder.cpp
View File

@ -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()

2
libsolidity/formal/SMTEncoder.h
View File

@ -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<CallStackEntry> m_callStack;

10
libsolidity/interface/StandardCompiler.cpp
View File

@ -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"];

10
solc/CommandLineParser.cpp
View File

@ -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);

8
test/libsolidity/SMTCheckerTest.cpp
View File

@ -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")

4
test/libsolidity/smtCheckerTests/typecast/function_type_to_function_type_internal.sol
View File

@ -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.

18
test/libsolidity/smtCheckerTests/unsupported/assembly_1.sol Normal file
View File

@ -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.

3
test/solc/CommandLineParser.cpp
View File

@ -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"}},

1
test/tools/fuzzer_common.cpp
View File

@ -112,6 +112,7 @@ void FuzzerUtil::testCompiler(
frontend::ModelCheckerInvariants::All(),
/*showProvedSafe=*/false,
/*showUnproved=*/false,
/*showUnsupported=*/false,
smtutil::SMTSolverChoice::All(),
frontend::ModelCheckerTargets::Default(),
/*timeout=*/1