From a961a7626394dc1ed16ae895917a033d62696923 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 9 Dec 2020 10:52:49 +0100 Subject: [PATCH] Do not run SMTChecker when file level functions/constants are present. --- libsolidity/formal/BMC.cpp | 17 ++++++---- libsolidity/formal/CHC.cpp | 25 +++++++++------ libsolidity/formal/SMTEncoder.cpp | 32 +++++++++++++++++++ libsolidity/formal/SMTEncoder.h | 3 ++ .../file_level/free_constant_1.sol | 10 ++++++ .../file_level/free_constant_2.sol | 18 +++++++++++ .../file_level/free_function_1.sol | 14 ++++++++ .../file_level/free_function_2.sol | 10 ++++++ .../file_level/free_function_3.sol | 5 +++ .../file_level/free_function_4.sol | 8 +++++ .../file_level/free_function_5.sol | 9 ++++++ .../free_function_and_constant_1.sol | 17 ++++++++++ 12 files changed, 152 insertions(+), 16 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/file_level/free_constant_1.sol create mode 100644 test/libsolidity/smtCheckerTests/file_level/free_constant_2.sol create mode 100644 test/libsolidity/smtCheckerTests/file_level/free_function_1.sol create mode 100644 test/libsolidity/smtCheckerTests/file_level/free_function_2.sol create mode 100644 test/libsolidity/smtCheckerTests/file_level/free_function_3.sol create mode 100644 test/libsolidity/smtCheckerTests/file_level/free_function_4.sol create mode 100644 test/libsolidity/smtCheckerTests/file_level/free_function_5.sol create mode 100644 test/libsolidity/smtCheckerTests/file_level/free_function_and_constant_1.sol diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index 502db5836..7e8bd7d11 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -58,13 +58,18 @@ void BMC::analyze(SourceUnit const& _source, mapsolvers() > 0, ""); // If this check is true, Z3 and CVC4 are not available diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 922c1c01c..ab15c4bc0 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -69,18 +69,23 @@ void CHC::analyze(SourceUnit const& _source) { solAssert(_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker), ""); - resetSourceAnalysis(); + /// This is currently used to abort analysis of SourceUnits + /// containing file level functions or constants. + if (SMTEncoder::analyze(_source)) + { + resetSourceAnalysis(); - set sources; - sources.insert(&_source); - for (auto const& source: _source.referencedSourceUnits(true)) - sources.insert(source); - for (auto const* source: sources) - defineInterfacesAndSummaries(*source); - for (auto const* source: sources) - source->accept(*this); + set sources; + sources.insert(&_source); + for (auto const& source: _source.referencedSourceUnits(true)) + sources.insert(source); + for (auto const* source: sources) + defineInterfacesAndSummaries(*source); + for (auto const* source: sources) + source->accept(*this); - checkVerificationTargets(); + checkVerificationTargets(); + } bool ranSolver = true; #ifndef HAVE_Z3 diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 06c41d732..c704e5ab1 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -40,6 +40,38 @@ SMTEncoder::SMTEncoder(smt::EncodingContext& _context): { } +bool SMTEncoder::analyze(SourceUnit const& _source) +{ + set sources; + sources.insert(&_source); + for (auto const& source: _source.referencedSourceUnits(true)) + sources.insert(source); + + bool analysis = true; + for (auto source: sources) + for (auto node: source->nodes()) + if (auto function = dynamic_pointer_cast(node)) + { + m_errorReporter.warning( + 6660_error, + function->location(), + "Model checker analysis was not possible because file level functions are not supported." + ); + analysis = false; + } + else if (auto var = dynamic_pointer_cast(node)) + { + m_errorReporter.warning( + 8195_error, + var->location(), + "Model checker analysis was not possible because file level constants are not supported." + ); + analysis = false; + } + + return analysis; +} + bool SMTEncoder::visit(ContractDefinition const& _contract) { solAssert(m_currentContract, ""); diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 239a84820..4f08aae7e 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -52,6 +52,9 @@ class SMTEncoder: public ASTConstVisitor public: SMTEncoder(smt::EncodingContext& _context); + /// @returns true if engine should proceed with analysis. + bool analyze(SourceUnit const& _sources); + /// @returns the leftmost identifier in a multi-d IndexAccess. static Expression const* leftmostBase(IndexAccess const& _indexAccess); diff --git a/test/libsolidity/smtCheckerTests/file_level/free_constant_1.sol b/test/libsolidity/smtCheckerTests/file_level/free_constant_1.sol new file mode 100644 index 000000000..afb79abaa --- /dev/null +++ b/test/libsolidity/smtCheckerTests/file_level/free_constant_1.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; +uint constant A = 42; +contract C { + function f(uint x) public pure returns (uint) { + return x + A; + } +} +// ---- +// Warning 8195: (32-52): Model checker analysis was not possible because file level constants are not supported. +// Warning 8195: (32-52): Model checker analysis was not possible because file level constants are not supported. diff --git a/test/libsolidity/smtCheckerTests/file_level/free_constant_2.sol b/test/libsolidity/smtCheckerTests/file_level/free_constant_2.sol new file mode 100644 index 000000000..8a628541b --- /dev/null +++ b/test/libsolidity/smtCheckerTests/file_level/free_constant_2.sol @@ -0,0 +1,18 @@ +pragma experimental SMTChecker; +uint256 constant x = 56; +enum ActionChoices {GoLeft, GoRight, GoStraight, Sit} +ActionChoices constant choices = ActionChoices.GoRight; +bytes32 constant st = "abc\x00\xff__"; +contract C { + function i() public returns (uint, ActionChoices, bytes32) { + return (x, choices, st); + } +} +// ---- +// Warning 2018: (220-310): Function state mutability can be restricted to pure +// Warning 8195: (32-55): Model checker analysis was not possible because file level constants are not supported. +// Warning 8195: (111-165): Model checker analysis was not possible because file level constants are not supported. +// Warning 8195: (167-204): Model checker analysis was not possible because file level constants are not supported. +// Warning 8195: (32-55): Model checker analysis was not possible because file level constants are not supported. +// Warning 8195: (111-165): Model checker analysis was not possible because file level constants are not supported. +// Warning 8195: (167-204): Model checker analysis was not possible because file level constants are not supported. diff --git a/test/libsolidity/smtCheckerTests/file_level/free_function_1.sol b/test/libsolidity/smtCheckerTests/file_level/free_function_1.sol new file mode 100644 index 000000000..0295f070a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/file_level/free_function_1.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; +contract C { + uint[] data; + function f(uint x, uint[] calldata input) public view returns (uint, uint) { + (uint a, uint[] calldata b) = fun(input, data); + return (a, b.length + x); + } +} +function fun(uint[] calldata _x, uint[] storage _y) view returns (uint, uint[] calldata) { + return (_y[0], _x); +} +// ---- +// Warning 6660: (220-334): Model checker analysis was not possible because file level functions are not supported. +// Warning 6660: (220-334): Model checker analysis was not possible because file level functions are not supported. diff --git a/test/libsolidity/smtCheckerTests/file_level/free_function_2.sol b/test/libsolidity/smtCheckerTests/file_level/free_function_2.sol new file mode 100644 index 000000000..e480f1219 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/file_level/free_function_2.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; +contract C { + function g() external { + f(); + } +} +function f() {} +// ---- +// Warning 6660: (82-97): Model checker analysis was not possible because file level functions are not supported. +// Warning 6660: (82-97): Model checker analysis was not possible because file level functions are not supported. diff --git a/test/libsolidity/smtCheckerTests/file_level/free_function_3.sol b/test/libsolidity/smtCheckerTests/file_level/free_function_3.sol new file mode 100644 index 000000000..6b04e3550 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/file_level/free_function_3.sol @@ -0,0 +1,5 @@ +pragma experimental SMTChecker; +function f() view {} +// ---- +// Warning 6660: (32-52): Model checker analysis was not possible because file level functions are not supported. +// Warning 6660: (32-52): Model checker analysis was not possible because file level functions are not supported. diff --git a/test/libsolidity/smtCheckerTests/file_level/free_function_4.sol b/test/libsolidity/smtCheckerTests/file_level/free_function_4.sol new file mode 100644 index 000000000..c2f284fda --- /dev/null +++ b/test/libsolidity/smtCheckerTests/file_level/free_function_4.sol @@ -0,0 +1,8 @@ +pragma experimental SMTChecker; +function f()pure { + ufixed a = uint64(1) + ufixed(2); +} +// ---- +// Warning 2072: (52-60): Unused local variable. +// Warning 6660: (32-87): Model checker analysis was not possible because file level functions are not supported. +// Warning 6660: (32-87): Model checker analysis was not possible because file level functions are not supported. diff --git a/test/libsolidity/smtCheckerTests/file_level/free_function_5.sol b/test/libsolidity/smtCheckerTests/file_level/free_function_5.sol new file mode 100644 index 000000000..28e10360f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/file_level/free_function_5.sol @@ -0,0 +1,9 @@ +pragma experimental SMTChecker; +contract K {} +function f() pure { + (abi.encode, ""); +} +// ---- +// Warning 6133: (67-83): Statement has no effect. +// Warning 6660: (46-86): Model checker analysis was not possible because file level functions are not supported. +// Warning 6660: (46-86): Model checker analysis was not possible because file level functions are not supported. diff --git a/test/libsolidity/smtCheckerTests/file_level/free_function_and_constant_1.sol b/test/libsolidity/smtCheckerTests/file_level/free_function_and_constant_1.sol new file mode 100644 index 000000000..c19514c22 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/file_level/free_function_and_constant_1.sol @@ -0,0 +1,17 @@ +pragma experimental SMTChecker; +uint constant A = 42; +contract C { + uint[] data; + function f(uint x, uint[] calldata input) public view returns (uint, uint) { + (uint a, uint[] calldata b) = fun(input, data); + return (a, b.length + x + A); + } +} +function fun(uint[] calldata _x, uint[] storage _y) view returns (uint, uint[] calldata) { + return (_y[0], _x); +} +// ---- +// Warning 8195: (32-52): Model checker analysis was not possible because file level constants are not supported. +// Warning 6660: (246-360): Model checker analysis was not possible because file level functions are not supported. +// Warning 8195: (32-52): Model checker analysis was not possible because file level constants are not supported. +// Warning 6660: (246-360): Model checker analysis was not possible because file level functions are not supported.