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 #10670 from blishko/smt-virtual-modifiers-fix

Browse Source 
[SMTChecker] Fix virtual modifier called statically
This commit is contained in:
Leonardo 2020-12-21 18:05:02 +01:00 committed by GitHub
commit a48106ca1f
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
4 changed files with 55 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

33
libsolidity/formal/SMTEncoder.cpp
View File

@ -207,12 +207,8 @@ void SMTEncoder::visitFunctionOrModifier()
auto refDecl = modifierInvocation->name().annotation().referencedDeclaration;
if (dynamic_cast<ContractDefinition const*>(refDecl))
visitFunctionOrModifier();
else if (auto modifierDef = dynamic_cast<ModifierDefinition const*>(refDecl))
{
solAssert(*modifierInvocation->name().annotation().requiredLookup == VirtualLookup::Virtual, "");
ModifierDefinition const& modifier = modifierDef->resolveVirtual(*m_currentContract);
inlineModifierInvocation(modifierInvocation.get(), &modifier);
}
else if (auto modifier = resolveModifierInvocation(*modifierInvocation, m_currentContract))
inlineModifierInvocation(modifierInvocation.get(), modifier);
else
solAssert(false, "");
}
@ -2681,23 +2677,34 @@ vector<VariableDeclaration const*> SMTEncoder::modifiersVariables(FunctionDefini
{
if (!invok)
continue;
auto decl = invok->name().annotation().referencedDeclaration;
auto const* modifier = dynamic_cast<ModifierDefinition const*>(decl);
auto const* modifier = resolveModifierInvocation(*invok, _contract);
if (!modifier || visited.count(modifier))
continue;
visited.insert(modifier);
solAssert(_contract, "No contract context provided for modifier analysis!");
auto const& actualModifier = modifier->resolveVirtual(*_contract);
if (actualModifier.isImplemented())
if (modifier->isImplemented())
{
vars += applyMap(actualModifier.parameters(), [](auto _var) { return _var.get(); });
vars += BlockVars(actualModifier.body()).vars;
vars += applyMap(modifier->parameters(), [](auto _var) { return _var.get(); });
vars += BlockVars(modifier->body()).vars;
}
}
return vars;
}
ModifierDefinition const* SMTEncoder::resolveModifierInvocation(ModifierInvocation const& _invocation, ContractDefinition const* _contract)
{
auto const* modifier = dynamic_cast<ModifierDefinition const*>(_invocation.name().annotation().referencedDeclaration);
if (modifier)
{
VirtualLookup lookup = *_invocation.name().annotation().requiredLookup;
solAssert(lookup == VirtualLookup::Virtual || lookup == VirtualLookup::Static, "");
solAssert(_contract || lookup == VirtualLookup::Static, "No contract context provided for modifier lookup resolution!");
if (lookup == VirtualLookup::Virtual)
modifier = &modifier->resolveVirtual(*_contract);
}
return modifier;
}
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

@ -77,6 +77,9 @@ public:
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 ModifierDefinition of a ModifierInvocation if possible, or nullptr.
static ModifierDefinition const* resolveModifierInvocation(ModifierInvocation const& _invocation, ContractDefinition const* _contract);
/// @returns the SourceUnit that contains _scopable.
static SourceUnit const* sourceUnitContaining(Scopable const& _scopable);

10
test/libsolidity/smtCheckerTests/modifiers/modifier_virtual_static_call_1.sol Normal file
View File

@ -0,0 +1,10 @@
pragma experimental SMTChecker;
contract A {
modifier m virtual {
_;
}
}
contract C is A {
function f() public A.m returns (uint) {
}
}

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

@ -0,0 +1,22 @@
pragma experimental SMTChecker;
contract A {
int x = 0;
modifier m virtual {
assert(x == 0); // should hold
assert(x == 42); // should fail
_;
}
}
contract C is A {
modifier m override {
assert(x == 1); // This assert is not reachable, should NOT be reported
_;
}
function f() public A.m returns (uint) {
}
}
// ----
// Warning 6328: (115-130): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\n = 0\n\nTransaction trace:\nconstructor()\nState: x = 0\nf()