From 4e343590635f98f7c1d0973e82f9bafc67e03466 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 7 Apr 2021 14:52:56 +0200 Subject: [PATCH] Basic support to free functions --- libsolidity/formal/BMC.cpp | 17 +++++-- libsolidity/formal/CHC.cpp | 47 +++++++++---------- libsolidity/formal/Predicate.cpp | 11 ++++- libsolidity/formal/SMTEncoder.cpp | 37 ++++++++++----- libsolidity/formal/SMTEncoder.h | 9 ++++ libsolutil/CommonData.h | 12 ++--- .../file_level/free_function_1.sol | 4 +- .../file_level/free_function_2.sol | 3 -- .../file_level/free_function_3.sol | 3 -- .../file_level/free_function_4.sol | 4 +- .../file_level/free_function_5.sol | 4 +- .../free_function_and_constant_1.sol | 6 +-- 12 files changed, 90 insertions(+), 67 deletions(-) diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index f6630f0da..8c225975d 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -149,11 +149,13 @@ void BMC::endVisit(ContractDefinition const& _contract) bool BMC::visit(FunctionDefinition const& _function) { + // Free functions need to be visited in the context of a contract. + if (!m_currentContract) + return false; + auto contract = dynamic_cast(_function.scope()); - solAssert(contract, ""); - solAssert(m_currentContract, ""); auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts; - if (find(hierarchy.begin(), hierarchy.end(), contract) == hierarchy.end()) + if (contract && find(hierarchy.begin(), hierarchy.end(), contract) == hierarchy.end()) createStateVariables(*contract); if (m_callStack.empty()) @@ -165,7 +167,10 @@ bool BMC::visit(FunctionDefinition const& _function) } if (_function.isConstructor()) - inlineConstructorHierarchy(dynamic_cast(*_function.scope())); + { + solAssert(contract, ""); + inlineConstructorHierarchy(*contract); + } /// Already visits the children. SMTEncoder::visit(_function); @@ -175,6 +180,10 @@ bool BMC::visit(FunctionDefinition const& _function) void BMC::endVisit(FunctionDefinition const& _function) { + // Free functions need to be visited in the context of a contract. + if (!m_currentContract) + return; + if (isRootFunction()) { checkVerificationTargets(); diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 65e29870b..6734c4755 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -82,10 +82,11 @@ void CHC::analyze(SourceUnit const& _source) { resetSourceAnalysis(); - set sources; + set sources; sources.insert(&_source); for (auto const& source: _source.referencedSourceUnits(true)) sources.insert(source); + collectFreeFunctions(sources); for (auto const* source: sources) defineInterfacesAndSummaries(*source); for (auto const* source: sources) @@ -219,6 +220,10 @@ void CHC::endVisit(ContractDefinition const& _contract) bool CHC::visit(FunctionDefinition const& _function) { + // Free functions need to be visited in the context of a contract. + if (!m_currentContract) + return false; + if (!_function.isImplemented()) { addRule(summary(_function), "summary_function_" + to_string(_function.id())); @@ -258,6 +263,10 @@ bool CHC::visit(FunctionDefinition const& _function) void CHC::endVisit(FunctionDefinition const& _function) { + // Free functions need to be visited in the context of a contract. + if (!m_currentContract) + return; + if (!_function.isImplemented()) return; @@ -677,19 +686,13 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall) { solAssert(m_currentContract, ""); - auto scopeContract = currentScopeContract(); - auto function = functionCallToDefinition(_funCall, scopeContract, m_currentContract); + auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract); if (function) { if (m_currentFunction && !m_currentFunction->isConstructor()) m_callGraph[m_currentFunction].insert(function); else m_callGraph[m_currentContract].insert(function); - - // Libraries can have constants as their "state" variables, - // so we need to ensure they were constructed correctly. - if (function->annotation().contract->isLibrary()) - m_context.addAssertion(interface(*scopeContract)); } m_context.addAssertion(predicate(_funCall)); @@ -1045,7 +1048,7 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source) addRule(smtutil::Expression::implies(errorFlag().currentValue() == 0, smt::nondetInterface(iface, *contract, m_context, 0, 0)), "base_nondet"); auto const& resolved = contractFunctions(*contract); - for (auto const* function: contractFunctionsWithoutVirtual(*contract)) + for (auto const* function: contractFunctionsWithoutVirtual(*contract) + allFreeFunctions()) { for (auto var: function->parameters()) createVariable(*var); @@ -1310,8 +1313,7 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall) solAssert(kind == FunctionType::Kind::Internal || kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, ""); solAssert(m_currentContract, ""); - auto scopeContract = currentScopeContract(); - auto function = functionCallToDefinition(_funCall, scopeContract, m_currentContract); + auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract); if (!function) return smtutil::Expression(true); @@ -1328,27 +1330,20 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall) auto const* contract = function->annotation().contract; auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts; - solAssert(kind != FunctionType::Kind::Internal || contract->isLibrary() || contains(hierarchy, contract), ""); - - /// If the call is to a library, we use that library as the called contract. - /// If the call is to a contract not in the inheritance hierarchy, we also use that as the called contract. - /// Otherwise, the call is to some contract in the inheritance hierarchy of the current contract. - /// In this case we use current contract as the called one since the interfaces/predicates are different. - auto const* calledContract = contains(hierarchy, contract) ? m_currentContract : contract; - solAssert(calledContract, ""); + solAssert(kind != FunctionType::Kind::Internal || function->isFree() || (contract && contract->isLibrary()) || contains(hierarchy, contract), ""); bool usesStaticCall = function->stateMutability() == StateMutability::Pure || function->stateMutability() == StateMutability::View; - args += currentStateVariables(*calledContract); + args += currentStateVariables(*m_currentContract); args += symbolicArguments(_funCall, m_currentContract); - if (!calledContract->isLibrary() && !usesStaticCall) + if (!m_currentContract->isLibrary() && !usesStaticCall) { state().newState(); for (auto const& var: m_stateVariables) m_context.variable(*var)->increaseIndex(); } args += vector{state().state()}; - args += currentStateVariables(*calledContract); + args += currentStateVariables(*m_currentContract); for (auto var: function->parameters() + function->returnParameters()) { @@ -1359,14 +1354,14 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall) args.push_back(currentValue(*var)); } - Predicate const& summary = *m_summaries.at(calledContract).at(function); - auto from = smt::function(summary, calledContract, m_context); + Predicate const& summary = *m_summaries.at(m_currentContract).at(function); + auto from = smt::function(summary, m_currentContract, m_context); Predicate const& callPredicate = *createSummaryBlock( *function, - *calledContract, + *m_currentContract, kind == FunctionType::Kind::Internal ? PredicateType::InternalCall : PredicateType::ExternalCallTrusted ); - auto to = smt::function(callPredicate, calledContract, m_context); + auto to = smt::function(callPredicate, m_currentContract, m_context); addRule(smtutil::Expression::implies(from, to), to.name); return callPredicate(args); diff --git a/libsolidity/formal/Predicate.cpp b/libsolidity/formal/Predicate.cpp index 064815869..c2b8fd607 100644 --- a/libsolidity/formal/Predicate.cpp +++ b/libsolidity/formal/Predicate.cpp @@ -243,9 +243,16 @@ string Predicate::formatSummaryCall(vector const& _args) co fun->isFallback() ? "fallback" : fun->isReceive() ? "receive" : fun->name(); - solAssert(fun->annotation().contract, ""); - return fun->annotation().contract->name() + "." + fName + "(" + boost::algorithm::join(functionArgs, ", ") + ")" + value; + string prefix; + if (fun->isFree()) + prefix = !fun->sourceUnitName().empty() ? (fun->sourceUnitName() + ":") : ""; + else + { + solAssert(fun->annotation().contract, ""); + prefix = fun->annotation().contract->name() + "."; + } + return prefix + fName + "(" + boost::algorithm::join(functionArgs, ", ") + ")" + value; } vector> Predicate::summaryStateValues(vector const& _args) const diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 7749ea0f1..301157233 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -59,16 +59,7 @@ bool SMTEncoder::analyze(SourceUnit const& _source) bool analysis = true; for (auto source: sources) for (auto node: source->nodes()) - if (auto function = dynamic_pointer_cast(node)) - { - m_errorReporter.warning( - 6660_error, - function->location(), - "Model checker analysis was not possible because file level functions are not supported." - ); - analysis = false; - } - else if (auto var = dynamic_pointer_cast(node)) + if (auto var = dynamic_pointer_cast(node)) { m_errorReporter.warning( 8195_error, @@ -116,7 +107,7 @@ bool SMTEncoder::visit(ContractDefinition const& _contract) // the constructor. // Constructors are visited as part of the constructor // hierarchy inlining. - for (auto const* function: contractFunctionsWithoutVirtual(_contract)) + for (auto const* function: contractFunctionsWithoutVirtual(_contract) + allFreeFunctions()) if (!function->isConstructor()) function->accept(*this); @@ -152,6 +143,8 @@ bool SMTEncoder::visit(ModifierDefinition const&) bool SMTEncoder::visit(FunctionDefinition const& _function) { + solAssert(m_currentContract, ""); + m_modifierDepthStack.push_back(-1); initializeLocalVariables(_function); @@ -288,6 +281,8 @@ bool SMTEncoder::visit(PlaceholderStatement const&) void SMTEncoder::endVisit(FunctionDefinition const&) { + solAssert(m_currentContract, ""); + popCallStack(); solAssert(m_modifierDepthStack.back() == -1, ""); m_modifierDepthStack.pop_back(); @@ -2963,6 +2958,26 @@ vector SMTEncoder::symbolicArguments(FunctionCall const& _f return args; } +void SMTEncoder::collectFreeFunctions(set const& _sources) +{ + if (!m_freeFunctions.empty()) + return; + + for (auto source: _sources) + for (auto node: source->nodes()) + if (auto function = dynamic_cast(node.get())) + m_freeFunctions.insert(function); + else if ( + auto contract = dynamic_cast(node.get()); + contract && contract->isLibrary() + ) + { + for (auto function: contract->definedFunctions()) + if (!function->isPublic()) + m_freeFunctions.insert(function); + } +} + smt::SymbolicState& SMTEncoder::state() { return m_context.state(); diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index b644b26b9..0bdd0a679 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -369,6 +369,11 @@ protected: /// type conversion. std::vector symbolicArguments(FunctionCall const& _funCall, ContractDefinition const* _contextContract); + /// Traverses all source units available collecting free functions + /// and internal library functions in m_freeFunctions. + void collectFreeFunctions(std::set const& _sources); + std::set const& allFreeFunctions() const { return m_freeFunctions; } + /// @returns a note to be added to warnings. std::string extraComment(); @@ -437,6 +442,10 @@ protected: ContractDefinition const* m_currentContract = nullptr; + /// Stores the free functions and internal library functions. + /// Those need to be encoded repeatedely for every analyzed contract. + std::set m_freeFunctions; + /// Stores the context of the encoding. smt::EncodingContext& m_context; diff --git a/libsolutil/CommonData.h b/libsolutil/CommonData.h index 3ec5b5739..ec858777e 100644 --- a/libsolutil/CommonData.h +++ b/libsolutil/CommonData.h @@ -99,19 +99,19 @@ inline std::vector operator+(std::vector&& _a, std::vector&& _b) } /// Concatenate something to a sets of elements. -template -inline std::set operator+(std::set const& _a, U&& _b) +template +inline std::set operator+(std::set const& _a, U&& _b) { - std::set ret(_a); + std::set ret(_a); ret += std::forward(_b); return ret; } /// Concatenate something to a sets of elements, move variant. -template -inline std::set operator+(std::set&& _a, U&& _b) +template +inline std::set operator+(std::set&& _a, U&& _b) { - std::set ret(std::move(_a)); + std::set ret(std::move(_a)); ret += std::forward(_b); return ret; } diff --git a/test/libsolidity/smtCheckerTests/file_level/free_function_1.sol b/test/libsolidity/smtCheckerTests/file_level/free_function_1.sol index ab214484b..1da78ef51 100644 --- a/test/libsolidity/smtCheckerTests/file_level/free_function_1.sol +++ b/test/libsolidity/smtCheckerTests/file_level/free_function_1.sol @@ -11,5 +11,5 @@ function fun(uint[] calldata _x, uint[] storage _y) view returns (uint, uint[] // ==== // SMTEngine: all // ---- -// Warning 6660: (188-302): Model checker analysis was not possible because file level functions are not supported. -// Warning 6660: (188-302): Model checker analysis was not possible because file level functions are not supported. +// Warning 4984: (168-180): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\ndata = []\nx = 1\n = 0\n = 0\na = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(1, input)\n fun(_x, []) -- internal call +// Warning 6368: (289-294): CHC: Out of bounds access happens here.\nCounterexample:\ndata = []\nx = 0\ninput = [5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 13, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5]\n = 0\n = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(0, [5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 13, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5])\n fun([5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 13, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5], []) -- internal call diff --git a/test/libsolidity/smtCheckerTests/file_level/free_function_2.sol b/test/libsolidity/smtCheckerTests/file_level/free_function_2.sol index b07c32fc6..a9fdffa45 100644 --- a/test/libsolidity/smtCheckerTests/file_level/free_function_2.sol +++ b/test/libsolidity/smtCheckerTests/file_level/free_function_2.sol @@ -6,6 +6,3 @@ contract C { function f() {} // ==== // SMTEngine: all -// ---- -// Warning 6660: (50-65): Model checker analysis was not possible because file level functions are not supported. -// Warning 6660: (50-65): Model checker analysis was not possible because file level functions are not supported. diff --git a/test/libsolidity/smtCheckerTests/file_level/free_function_3.sol b/test/libsolidity/smtCheckerTests/file_level/free_function_3.sol index 7fd7d8419..994281dff 100644 --- a/test/libsolidity/smtCheckerTests/file_level/free_function_3.sol +++ b/test/libsolidity/smtCheckerTests/file_level/free_function_3.sol @@ -1,6 +1,3 @@ function f() view {} // ==== // SMTEngine: all -// ---- -// Warning 6660: (0-20): Model checker analysis was not possible because file level functions are not supported. -// Warning 6660: (0-20): Model checker analysis was not possible because file level functions are not supported. diff --git a/test/libsolidity/smtCheckerTests/file_level/free_function_4.sol b/test/libsolidity/smtCheckerTests/file_level/free_function_4.sol index 0033da96d..84ab81300 100644 --- a/test/libsolidity/smtCheckerTests/file_level/free_function_4.sol +++ b/test/libsolidity/smtCheckerTests/file_level/free_function_4.sol @@ -4,6 +4,4 @@ function f()pure { // ==== // SMTEngine: all // ---- -// Warning 2072: (20-28): Unused local variable. -// Warning 6660: (0-55): Model checker analysis was not possible because file level functions are not supported. -// Warning 6660: (0-55): Model checker analysis was not possible because file level functions are not supported. +// Warning 2072: (52-60): Unused local variable. diff --git a/test/libsolidity/smtCheckerTests/file_level/free_function_5.sol b/test/libsolidity/smtCheckerTests/file_level/free_function_5.sol index 093167676..7e1be87b9 100644 --- a/test/libsolidity/smtCheckerTests/file_level/free_function_5.sol +++ b/test/libsolidity/smtCheckerTests/file_level/free_function_5.sol @@ -5,6 +5,4 @@ function f() pure { // ==== // SMTEngine: all // ---- -// Warning 6133: (35-51): Statement has no effect. -// Warning 6660: (14-54): Model checker analysis was not possible because file level functions are not supported. -// Warning 6660: (14-54): Model checker analysis was not possible because file level functions are not supported. +// Warning 6133: (67-83): Statement has no effect. diff --git a/test/libsolidity/smtCheckerTests/file_level/free_function_and_constant_1.sol b/test/libsolidity/smtCheckerTests/file_level/free_function_and_constant_1.sol index db4d38008..7c4f1099f 100644 --- a/test/libsolidity/smtCheckerTests/file_level/free_function_and_constant_1.sol +++ b/test/libsolidity/smtCheckerTests/file_level/free_function_and_constant_1.sol @@ -12,7 +12,5 @@ function fun(uint[] calldata _x, uint[] storage _y) view returns (uint, uint[] // ==== // SMTEngine: all // ---- -// Warning 8195: (0-20): Model checker analysis was not possible because file level constants are not supported. -// Warning 6660: (214-328): Model checker analysis was not possible because file level functions are not supported. -// Warning 8195: (0-20): Model checker analysis was not possible because file level constants are not supported. -// Warning 6660: (214-328): Model checker analysis was not possible because file level functions are not supported. +// Warning 8195: (32-52): Model checker analysis was not possible because file level constants are not supported. +// Warning 8195: (32-52): Model checker analysis was not possible because file level constants are not supported.