cerc-io/solidity
15
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

Do not run SMTChecker when file level functions/constants are present.

Browse Source
This commit is contained in:
Leonardo Alt 2020-12-09 10:52:49 +01:00
parent e23cf26d98
commit a961a76263
12 changed files with 152 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
libsolidity/formal/BMC.cpp
View File

@ -58,13 +58,18 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
{
solAssert(_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker), "");
m_solvedTargets = move(_solvedTargets);
m_context.setSolver(m_interface.get());
m_context.clear();
m_context.setAssertionAccumulation(true);
m_variableUsage.setFunctionInlining(shouldInlineFunctionCall);
/// This is currently used to abort analysis of SourceUnits
/// containing file level functions or constants.
if (SMTEncoder::analyze(_source))
{
m_solvedTargets = move(_solvedTargets);
m_context.setSolver(m_interface.get());
m_context.clear();
m_context.setAssertionAccumulation(true);
m_variableUsage.setFunctionInlining(shouldInlineFunctionCall);
_source.accept(*this);
_source.accept(*this);
}
solAssert(m_interface->solvers() > 0, "");
// If this check is true, Z3 and CVC4 are not available

25
libsolidity/formal/CHC.cpp
View File

@ -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<SourceUnit const*, EncodingContext::IdCompare> 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<SourceUnit const*, EncodingContext::IdCompare> 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

32
libsolidity/formal/SMTEncoder.cpp
View File

@ -40,6 +40,38 @@ SMTEncoder::SMTEncoder(smt::EncodingContext& _context):
{
}
bool SMTEncoder::analyze(SourceUnit const& _source)
{
set<SourceUnit const*, smt::EncodingContext::IdCompare> 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<FunctionDefinition>(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<VariableDeclaration>(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, "");

3
libsolidity/formal/SMTEncoder.h
View File

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

10
test/libsolidity/smtCheckerTests/file_level/free_constant_1.sol Normal file
View File

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

18
test/libsolidity/smtCheckerTests/file_level/free_constant_2.sol Normal file
View File

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

14
test/libsolidity/smtCheckerTests/file_level/free_function_1.sol Normal file
View File

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

10
test/libsolidity/smtCheckerTests/file_level/free_function_2.sol Normal file
View File

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

5
test/libsolidity/smtCheckerTests/file_level/free_function_3.sol Normal file
View File

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

8
test/libsolidity/smtCheckerTests/file_level/free_function_4.sol Normal file
View File

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

9
test/libsolidity/smtCheckerTests/file_level/free_function_5.sol Normal file
View File

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

17
test/libsolidity/smtCheckerTests/file_level/free_function_and_constant_1.sol Normal file
View File

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