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

Merge pull request #10202 from ethereum/smt_fix_modifiers_branches

Browse Source 
[SMTChecker] Fix CHC false positives when using branches inside modifiers
This commit is contained in:
Leonardo 2020-11-09 16:42:30 +00:00 committed by GitHub
commit 25b2a38d8b
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
10 changed files with 145 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -19,6 +19,7 @@ Bugfixes:
* SMTChecker: Fix false negative in modifier applied multiple times.
* SMTChecker: Fix internal error in the BMC engine when inherited contract from a different source unit has private state variables.
* SMTChecker: Fix internal error when ``array.push()`` is used as the LHS of an assignment.
* SMTChecker: Fix CHC false positives when branches are used inside modifiers.
* Code generator: Fix missing creation dependency tracking for abstract contracts.

4
libsolidity/formal/CHC.cpp
View File

@ -746,7 +746,7 @@ void CHC::clearIndices(ContractDefinition const* _contract, FunctionDefinition c
{
for (auto const& var: _function->parameters() + _function->returnParameters())
m_context.variable(*var)->increaseIndex();
for (auto const& var: _function->localVariables())
for (auto const& var: localVariablesIncludingModifiers(*_function))
m_context.variable(*var)->increaseIndex();
}
@ -821,7 +821,7 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
createVariable(*var);
for (auto var: function->returnParameters())
createVariable(*var);
for (auto const* var: function->localVariables())
for (auto const* var: localVariablesIncludingModifiers(*function))
createVariable(*var);
m_summaries[contract].emplace(function, createSummaryBlock(*function, *contract));

2
libsolidity/formal/PredicateInstance.cpp
View File

@ -132,7 +132,7 @@ vector<smtutil::Expression> currentBlockVariables(FunctionDefinition const& _fun
{
return currentFunctionVariables(_function, _contract, _context) +
applyMap(
_function.localVariables(),
SMTEncoder::localVariablesIncludingModifiers(_function),
[&](auto _var) { return _context.variable(*_var)->currentValue(); }
);
}

2
libsolidity/formal/PredicateSort.cpp
View File

@ -90,7 +90,7 @@ SortPointer functionBodySort(FunctionDefinition const& _function, ContractDefini
auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); };
return make_shared<FunctionSort>(
fSort->domain + applyMap(_function.localVariables(), smtSort),
fSort->domain + applyMap(SMTEncoder::localVariablesIncludingModifiers(_function), smtSort),
SortProvider::boolSort
);
}

45
libsolidity/formal/SMTEncoder.cpp
View File

@ -1991,7 +1991,12 @@ void SMTEncoder::initializeFunctionCallParameters(CallableDeclaration const& _fu
m_arrayAssignmentHappened = true;
}
for (auto const& variable: _function.localVariables())
vector<VariableDeclaration const*> localVars;
if (auto const* fun = dynamic_cast<FunctionDefinition const*>(&_function))
localVars = localVariablesIncludingModifiers(*fun);
else
localVars = _function.localVariables();
for (auto const& variable: localVars)
if (createVariable(*variable))
{
m_context.newValue(*variable);
@ -2031,7 +2036,7 @@ void SMTEncoder::initializeStateVariables(ContractDefinition const& _contract)
void SMTEncoder::createLocalVariables(FunctionDefinition const& _function)
{
for (auto const& variable: _function.localVariables())
for (auto const& variable: localVariablesIncludingModifiers(_function))
createVariable(*variable);
for (auto const& param: _function.parameters())
@ -2044,7 +2049,7 @@ void SMTEncoder::createLocalVariables(FunctionDefinition const& _function)
void SMTEncoder::initializeLocalVariables(FunctionDefinition const& _function)
{
for (auto const& variable: _function.localVariables())
for (auto const& variable: localVariablesIncludingModifiers(_function))
{
solAssert(m_context.knownVariable(*variable), "");
m_context.setZeroValue(*variable);
@ -2299,7 +2304,7 @@ void SMTEncoder::clearIndices(ContractDefinition const* _contract, FunctionDefin
{
for (auto const& var: _function->parameters() + _function->returnParameters())
m_context.variable(*var)->resetIndex();
for (auto const& var: _function->localVariables())
for (auto const& var: localVariablesIncludingModifiers(*_function))
m_context.variable(*var)->resetIndex();
}
m_context.state().reset();
@ -2434,6 +2439,38 @@ vector<VariableDeclaration const*> SMTEncoder::stateVariablesIncludingInheritedA
return stateVariablesIncludingInheritedAndPrivate(dynamic_cast<ContractDefinition const&>(*_function.scope()));
}
vector<VariableDeclaration const*> SMTEncoder::localVariablesIncludingModifiers(FunctionDefinition const& _function)
{
return _function.localVariables() + modifiersVariables(_function);
}
vector<VariableDeclaration const*> SMTEncoder::modifiersVariables(FunctionDefinition const& _function)
{
struct BlockVars: ASTConstVisitor
{
BlockVars(Block const& _block) { _block.accept(*this); }
void endVisit(VariableDeclaration const& _var) { vars.push_back(&_var); }
vector<VariableDeclaration const*> vars;
};
vector<VariableDeclaration const*> vars;
set<ModifierDefinition const*> visited;
for (auto invok: _function.modifiers())
{
if (!invok)
continue;
auto decl = invok->name()->annotation().referencedDeclaration;
auto const* modifier = dynamic_cast<ModifierDefinition const*>(decl);
if (!modifier || visited.count(modifier))
continue;
visited.insert(modifier);
vars += applyMap(modifier->parameters(), [](auto _var) { return _var.get(); });
vars += BlockVars(modifier->body()).vars;
}
return vars;
}
SourceUnit const* SMTEncoder::sourceUnitContaining(Scopable const& _scopable)
{
for (auto const* s = &_scopable; s; s = dynamic_cast<Scopable const*>(s->scope()))

3
libsolidity/formal/SMTEncoder.h
View File

@ -71,6 +71,9 @@ public:
static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract);
static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function);
static std::vector<VariableDeclaration const*> localVariablesIncludingModifiers(FunctionDefinition const& _function);
static std::vector<VariableDeclaration const*> modifiersVariables(FunctionDefinition const& _function);
/// @returns the SourceUnit that contains _scopable.
static SourceUnit const* sourceUnitContaining(Scopable const& _scopable);

24
test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_1.sol Normal file
View File

@ -0,0 +1,24 @@
pragma experimental SMTChecker;
contract C {
uint x;
modifier m(uint z) {
uint y = 3;
if (z == 10)
x = 2 + y;
_;
if (z == 10)
x = 4 + y;
}
function f() m(10) internal {
x = 3;
}
function g() public {
x = 0;
f();
assert(x == 7);
// Fails
assert(x == 6);
}
}
// ----
// Warning 6328: (359-373): CHC: Assertion violation happens here.

24
test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_2.sol Normal file
View File

@ -0,0 +1,24 @@
pragma experimental SMTChecker;
contract C {
uint x;
modifier m(uint z) {
uint y = 3;
if (z == 10)
x = 2 + y;
_;
if (z == 10)
x = 4 + y;
}
function f() m(10) m(12) internal {
x = 3;
}
function g() public {
x = 0;
f();
assert(x == 3);
// Fails
assert(x == 6);
}
}
// ----
// Warning 6328: (365-379): CHC: Assertion violation happens here.

24
test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_3.sol Normal file
View File

@ -0,0 +1,24 @@
pragma experimental SMTChecker;
contract C {
uint x;
modifier m(uint z) {
uint y = 3;
if (z == 10)
x = 2 + y;
_;
if (z == 10)
x = 4 + y;
}
function f() m(8) internal {
x = 3;
}
function g() public {
x = 0;
f();
assert(x == 3);
// Fails
assert(x == 6);
}
}
// ----
// Warning 6328: (358-372): CHC: Assertion violation happens here.

24
test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_4.sol Normal file
View File

@ -0,0 +1,24 @@
pragma experimental SMTChecker;
contract C {
uint x;
modifier m(uint z) {
uint y = 3;
if (z >= 10)
x = 2 + y;
_;
if (z >= 10)
x = 4 + y;
}
function f() m(10) m(12) internal {
x = 3;
}
function g() public {
x = 0;
f();
assert(x == 7);
// Fails
assert(x == 6);
}
}
// ----
// Warning 6328: (365-379): CHC: Assertion violation happens here.