diff --git a/Changelog.md b/Changelog.md index 3b801c1c9..949eeff1f 100644 --- a/Changelog.md +++ b/Changelog.md @@ -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. diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 08b50c03f..15111dd31 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -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)); diff --git a/libsolidity/formal/PredicateInstance.cpp b/libsolidity/formal/PredicateInstance.cpp index 29a6e75d8..3c38d4d60 100644 --- a/libsolidity/formal/PredicateInstance.cpp +++ b/libsolidity/formal/PredicateInstance.cpp @@ -132,7 +132,7 @@ vector currentBlockVariables(FunctionDefinition const& _fun { return currentFunctionVariables(_function, _contract, _context) + applyMap( - _function.localVariables(), + SMTEncoder::localVariablesIncludingModifiers(_function), [&](auto _var) { return _context.variable(*_var)->currentValue(); } ); } diff --git a/libsolidity/formal/PredicateSort.cpp b/libsolidity/formal/PredicateSort.cpp index ac730d7a5..18fcbdfc3 100644 --- a/libsolidity/formal/PredicateSort.cpp +++ b/libsolidity/formal/PredicateSort.cpp @@ -90,7 +90,7 @@ SortPointer functionBodySort(FunctionDefinition const& _function, ContractDefini auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); }; return make_shared( - fSort->domain + applyMap(_function.localVariables(), smtSort), + fSort->domain + applyMap(SMTEncoder::localVariablesIncludingModifiers(_function), smtSort), SortProvider::boolSort ); } diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index b2aa31400..a81e63184 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -1989,7 +1989,12 @@ void SMTEncoder::initializeFunctionCallParameters(CallableDeclaration const& _fu m_arrayAssignmentHappened = true; } - for (auto const& variable: _function.localVariables()) + vector localVars; + if (auto const* fun = dynamic_cast(&_function)) + localVars = localVariablesIncludingModifiers(*fun); + else + localVars = _function.localVariables(); + for (auto const& variable: localVars) if (createVariable(*variable)) { m_context.newValue(*variable); @@ -2029,7 +2034,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()) @@ -2042,7 +2047,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); @@ -2297,7 +2302,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(); @@ -2432,6 +2437,38 @@ vector SMTEncoder::stateVariablesIncludingInheritedA return stateVariablesIncludingInheritedAndPrivate(dynamic_cast(*_function.scope())); } +vector SMTEncoder::localVariablesIncludingModifiers(FunctionDefinition const& _function) +{ + return _function.localVariables() + modifiersVariables(_function); +} + +vector 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 vars; + }; + + vector vars; + set visited; + for (auto invok: _function.modifiers()) + { + if (!invok) + continue; + auto decl = invok->name()->annotation().referencedDeclaration; + auto const* modifier = dynamic_cast(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(s->scope())) diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 366cfc0b2..49cac0082 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -71,6 +71,9 @@ 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); + /// @returns the SourceUnit that contains _scopable. static SourceUnit const* sourceUnitContaining(Scopable const& _scopable); diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_1.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_1.sol new file mode 100644 index 000000000..151ea9216 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_1.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_2.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_2.sol new file mode 100644 index 000000000..e1c66050d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_2.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_3.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_3.sol new file mode 100644 index 000000000..816ffc600 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_3.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_4.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_4.sol new file mode 100644 index 000000000..2817f16d2 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_4.sol @@ -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.