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

[SMTChecker] Fix analysis of overriding modifiers

Browse Source
This commit is contained in:
Martin Blicha 2020-12-15 15:50:02 +01:00
parent 9328503265
commit 7078e8f8f8
10 changed files with 140 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
Changelog.md
View File

@ -3,6 +3,9 @@
Compiler Features:
* SMTChecker: Support ABI functions as uninterpreted functions.
Bugfixes:
* SMTChecker: Fix false negatives in overriding modifiers.
### 0.8.0 (2020-12-16)

4
libsolidity/formal/CHC.cpp
View File

@ -821,7 +821,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: localVariablesIncludingModifiers(*_function))
for (auto const& var: localVariablesIncludingModifiers(*_function, _contract))
m_context.variable(*var)->increaseIndex();
}
@ -898,7 +898,7 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
createVariable(*var);
for (auto var: function->returnParameters())
createVariable(*var);
for (auto const* var: localVariablesIncludingModifiers(*function))
for (auto const* var: localVariablesIncludingModifiers(*function, contract))
createVariable(*var);
m_summaries[contract].emplace(function, createSummaryBlock(*function, *contract));

2
libsolidity/formal/PredicateInstance.cpp
View File

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

2
libsolidity/formal/PredicateSort.cpp
View File

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

28
libsolidity/formal/SMTEncoder.cpp
View File

@ -208,7 +208,11 @@ void SMTEncoder::visitFunctionOrModifier()
if (dynamic_cast<ContractDefinition const*>(refDecl))
visitFunctionOrModifier();
else if (auto modifierDef = dynamic_cast<ModifierDefinition const*>(refDecl))
inlineModifierInvocation(modifierInvocation.get(), modifierDef);
{
solAssert(*modifierInvocation->name().annotation().requiredLookup == VirtualLookup::Virtual, "");
ModifierDefinition const& modifier = modifierDef->resolveVirtual(*m_currentContract);
inlineModifierInvocation(modifierInvocation.get(), &modifier);
}
else
solAssert(false, "");
}
@ -2162,7 +2166,7 @@ void SMTEncoder::initializeFunctionCallParameters(CallableDeclaration const& _fu
vector<VariableDeclaration const*> localVars;
if (auto const* fun = dynamic_cast<FunctionDefinition const*>(&_function))
localVars = localVariablesIncludingModifiers(*fun);
localVars = localVariablesIncludingModifiers(*fun, m_currentContract);
else
localVars = _function.localVariables();
for (auto const& variable: localVars)
@ -2205,7 +2209,7 @@ void SMTEncoder::initializeStateVariables(ContractDefinition const& _contract)
void SMTEncoder::createLocalVariables(FunctionDefinition const& _function)
{
for (auto const& variable: localVariablesIncludingModifiers(_function))
for (auto const& variable: localVariablesIncludingModifiers(_function, m_currentContract))
createVariable(*variable);
for (auto const& param: _function.parameters())
@ -2218,7 +2222,7 @@ void SMTEncoder::createLocalVariables(FunctionDefinition const& _function)
void SMTEncoder::initializeLocalVariables(FunctionDefinition const& _function)
{
for (auto const& variable: localVariablesIncludingModifiers(_function))
for (auto const& variable: localVariablesIncludingModifiers(_function, m_currentContract))
{
solAssert(m_context.knownVariable(*variable), "");
m_context.setZeroValue(*variable);
@ -2481,7 +2485,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: localVariablesIncludingModifiers(*_function))
for (auto const& var: localVariablesIncludingModifiers(*_function, _contract))
m_context.variable(*var)->resetIndex();
}
m_context.state().reset();
@ -2638,12 +2642,12 @@ vector<VariableDeclaration const*> SMTEncoder::stateVariablesIncludingInheritedA
return stateVariablesIncludingInheritedAndPrivate(dynamic_cast<ContractDefinition const&>(*_function.scope()));
}
vector<VariableDeclaration const*> SMTEncoder::localVariablesIncludingModifiers(FunctionDefinition const& _function)
vector<VariableDeclaration const*> SMTEncoder::localVariablesIncludingModifiers(FunctionDefinition const& _function, ContractDefinition const* _contract)
{
return _function.localVariables() + modifiersVariables(_function);
return _function.localVariables() + modifiersVariables(_function, _contract);
}
vector<VariableDeclaration const*> SMTEncoder::modifiersVariables(FunctionDefinition const& _function)
vector<VariableDeclaration const*> SMTEncoder::modifiersVariables(FunctionDefinition const& _function, ContractDefinition const* _contract)
{
struct BlockVars: ASTConstVisitor
{
@ -2664,10 +2668,12 @@ vector<VariableDeclaration const*> SMTEncoder::modifiersVariables(FunctionDefini
continue;
visited.insert(modifier);
if (modifier->isImplemented())
solAssert(_contract, "No contract context provided for modifier analysis!");
auto const& actualModifier = modifier->resolveVirtual(*_contract);
if (actualModifier.isImplemented())
{
vars += applyMap(modifier->parameters(), [](auto _var) { return _var.get(); });
vars += BlockVars(modifier->body()).vars;
vars += applyMap(actualModifier.parameters(), [](auto _var) { return _var.get(); });
vars += BlockVars(actualModifier.body()).vars;
}
}
return vars;

4
libsolidity/formal/SMTEncoder.h
View File

@ -74,8 +74,8 @@ 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);
static std::vector<VariableDeclaration const*> localVariablesIncludingModifiers(FunctionDefinition const& _function, ContractDefinition const* _contract);
static std::vector<VariableDeclaration const*> modifiersVariables(FunctionDefinition const& _function, ContractDefinition const* _contract);
/// @returns the SourceUnit that contains _scopable.
static SourceUnit const* sourceUnitContaining(Scopable const& _scopable);

23
test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_1.sol Normal file
View File

@ -0,0 +1,23 @@
pragma experimental SMTChecker;
abstract contract A {
uint s;
function f() public mod(s) {}
modifier mod(uint x) virtual;
}
contract B is A {
modifier mod(uint x) override {
require(x == 42);
_;
assert(x == 42); // should hold
assert(x == 0); // should fail
}
function set(uint x) public {
s = x;
}
}
// ----
// Warning 6328: (242-256): CHC: Assertion violation happens here.\nCounterexample:\ns = 42\n\n\n\nTransaction trace:\nconstructor()\nState: s = 0\nset(42)\nState: s = 42\nf()

27
test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_2.sol Normal file
View File

@ -0,0 +1,27 @@
pragma experimental SMTChecker;
abstract contract A {
bool s;
function f() public view mod {
assert(s); // holds for C, but fails for B
}
modifier mod() virtual;
}
contract B is A {
modifier mod() virtual override {
s = false;
_;
}
}
contract C is B {
modifier mod() override {
s = true;
_;
}
}
// ----
// Warning 5740: (95-144): Unreachable code.
// Warning 6328: (99-108): CHC: Assertion violation happens here.\nCounterexample:\ns = false\n\n\n\nTransaction trace:\nconstructor()\nState: s = false\nf()

22
test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_3.sol Normal file
View File

@ -0,0 +1,22 @@
pragma experimental SMTChecker;
abstract contract A {
bool s;
function f() public view mod {
assert(s); // holds for B
assert(!s); // fails for B
}
modifier mod() virtual;
}
contract B is A {
modifier mod() virtual override {
bool x = true;
s = x;
_;
}
}
// ----
// Warning 5740: (95-156): Unreachable code.
// Warning 6328: (127-137): CHC: Assertion violation happens here.\nCounterexample:\ns = true\n\n\n\nTransaction trace:\nconstructor()\nState: s = false\nf()

42
test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_4.sol Normal file
View File

@ -0,0 +1,42 @@
pragma experimental SMTChecker;
abstract contract A {
int x = 0;
function f() public view mod() {
assert(x != 0); // fails for A
assert(x != 1); // fails for B
assert(x != 2); // fails for C
assert(x != 3); // fails for D
}
modifier mod() virtual {
_;
}
}
contract B is A {
modifier mod() virtual override {
x = 1;
_;
}
}
contract C is A {
modifier mod() virtual override {
x = 2;
_;
}
}
contract D is B,C {
modifier mod() virtual override (B,C){
x = 3;
_;
}
}
// ----
// Warning 6328: (104-118): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf()
// Warning 6328: (137-151): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf()
// Warning 6328: (170-184): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf()
// Warning 6328: (203-217): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf()