From 7078e8f8f851152c0e51510bc84890250c04160e Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Tue, 15 Dec 2020 15:50:02 +0100 Subject: [PATCH] [SMTChecker] Fix analysis of overriding modifiers --- Changelog.md | 3 ++ libsolidity/formal/CHC.cpp | 4 +- libsolidity/formal/PredicateInstance.cpp | 2 +- libsolidity/formal/PredicateSort.cpp | 2 +- libsolidity/formal/SMTEncoder.cpp | 28 ++++++++----- libsolidity/formal/SMTEncoder.h | 4 +- .../modifiers/modifier_overriding_1.sol | 23 ++++++++++ .../modifiers/modifier_overriding_2.sol | 27 ++++++++++++ .../modifiers/modifier_overriding_3.sol | 22 ++++++++++ .../modifiers/modifier_overriding_4.sol | 42 +++++++++++++++++++ 10 files changed, 140 insertions(+), 17 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_1.sol create mode 100644 test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_2.sol create mode 100644 test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_3.sol create mode 100644 test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_4.sol diff --git a/Changelog.md b/Changelog.md index c5cefb9f8..0007fc0ce 100644 --- a/Changelog.md +++ b/Changelog.md @@ -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) diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 1111a37dd..17a481467 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -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)); diff --git a/libsolidity/formal/PredicateInstance.cpp b/libsolidity/formal/PredicateInstance.cpp index 0e8848485..62c6dafb6 100644 --- a/libsolidity/formal/PredicateInstance.cpp +++ b/libsolidity/formal/PredicateInstance.cpp @@ -179,7 +179,7 @@ vector currentBlockVariables(FunctionDefinition const& _fun { return currentFunctionVariablesForDefinition(_function, _contract, _context) + applyMap( - SMTEncoder::localVariablesIncludingModifiers(_function), + SMTEncoder::localVariablesIncludingModifiers(_function, _contract), [&](auto _var) { return _context.variable(*_var)->currentValue(); } ); } diff --git a/libsolidity/formal/PredicateSort.cpp b/libsolidity/formal/PredicateSort.cpp index e7f3e8540..a85588209 100644 --- a/libsolidity/formal/PredicateSort.cpp +++ b/libsolidity/formal/PredicateSort.cpp @@ -84,7 +84,7 @@ SortPointer functionBodySort(FunctionDefinition const& _function, ContractDefini auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); }; return make_shared( - fSort->domain + applyMap(SMTEncoder::localVariablesIncludingModifiers(_function), smtSort), + fSort->domain + applyMap(SMTEncoder::localVariablesIncludingModifiers(_function, _contract), smtSort), SortProvider::boolSort ); } diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 23e6f5cb7..3af3c404f 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -208,7 +208,11 @@ void SMTEncoder::visitFunctionOrModifier() if (dynamic_cast(refDecl)) visitFunctionOrModifier(); else if (auto modifierDef = dynamic_cast(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 localVars; if (auto const* fun = dynamic_cast(&_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 SMTEncoder::stateVariablesIncludingInheritedA return stateVariablesIncludingInheritedAndPrivate(dynamic_cast(*_function.scope())); } -vector SMTEncoder::localVariablesIncludingModifiers(FunctionDefinition const& _function) +vector SMTEncoder::localVariablesIncludingModifiers(FunctionDefinition const& _function, ContractDefinition const* _contract) { - return _function.localVariables() + modifiersVariables(_function); + return _function.localVariables() + modifiersVariables(_function, _contract); } -vector SMTEncoder::modifiersVariables(FunctionDefinition const& _function) +vector SMTEncoder::modifiersVariables(FunctionDefinition const& _function, ContractDefinition const* _contract) { struct BlockVars: ASTConstVisitor { @@ -2664,10 +2668,12 @@ vector 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; diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index b8d571eed..2e7fe3360 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -74,8 +74,8 @@ public: static std::vector stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract); static std::vector stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function); - static std::vector localVariablesIncludingModifiers(FunctionDefinition const& _function); - static std::vector modifiersVariables(FunctionDefinition const& _function); + static std::vector localVariablesIncludingModifiers(FunctionDefinition const& _function, ContractDefinition const* _contract); + static std::vector modifiersVariables(FunctionDefinition const& _function, ContractDefinition const* _contract); /// @returns the SourceUnit that contains _scopable. static SourceUnit const* sourceUnitContaining(Scopable const& _scopable); diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_1.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_1.sol new file mode 100644 index 000000000..1ef4561f1 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_1.sol @@ -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() diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_2.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_2.sol new file mode 100644 index 000000000..2a6251406 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_2.sol @@ -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() diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_3.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_3.sol new file mode 100644 index 000000000..dd66baa13 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_3.sol @@ -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() diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_4.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_4.sol new file mode 100644 index 000000000..3adc576e5 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_4.sol @@ -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()