diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 5067e1396..9d8bf16d4 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -31,6 +31,7 @@ using namespace std; using namespace solidity; +using namespace solidity::util; using namespace solidity::langutil; using namespace solidity::frontend; @@ -643,19 +644,19 @@ set CHC::transactionAssertions(ASTNode const* vector CHC::stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract) { - vector stateVars; - for (auto const& contract: _contract.annotation().linearizedBaseContracts) - for (auto var: contract->stateVariables()) - stateVars.push_back(var); - return stateVars; + return fold( + _contract.annotation().linearizedBaseContracts, + vector{}, + [](auto&& _acc, auto _contract) { return _acc + _contract->stateVariables(); } + ); } vector CHC::stateSorts(ContractDefinition const& _contract) { - vector stateSorts; - for (auto const& var: stateVariablesIncludingInheritedAndPrivate(_contract)) - stateSorts.push_back(smt::smtSortAbstractFunction(*var->type())); - return stateSorts; + return applyMap( + stateVariablesIncludingInheritedAndPrivate(_contract), + [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); } + ); } smt::SortPointer CHC::constructorSort() @@ -695,12 +696,9 @@ smt::SortPointer CHC::interfaceSort(ContractDefinition const& _contract) /// - 1 set of output variables smt::SortPointer CHC::sort(FunctionDefinition const& _function) { - vector inputSorts; - for (auto const& var: _function.parameters()) - inputSorts.push_back(smt::smtSortAbstractFunction(*var->type())); - vector outputSorts; - for (auto const& var: _function.returnParameters()) - outputSorts.push_back(smt::smtSortAbstractFunction(*var->type())); + auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); }; + auto inputSorts = applyMap(_function.parameters(), smtSort); + auto outputSorts = applyMap(_function.returnParameters(), smtSort); return make_shared( vector{smt::SortProvider::intSort} + m_stateSorts + inputSorts + m_stateSorts + inputSorts + outputSorts, smt::SortProvider::boolSort @@ -715,11 +713,9 @@ smt::SortPointer CHC::sort(ASTNode const* _node) auto fSort = dynamic_pointer_cast(sort(*m_currentFunction)); solAssert(fSort, ""); - vector varSorts; - for (auto const& var: m_currentFunction->localVariables()) - varSorts.push_back(smt::smtSortAbstractFunction(*var->type())); + auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); }; return make_shared( - fSort->domain + varSorts, + fSort->domain + applyMap(m_currentFunction->localVariables(), smtSort), smt::SortProvider::boolSort ); } @@ -729,11 +725,9 @@ smt::SortPointer CHC::summarySort(FunctionDefinition const& _function, ContractD auto stateVariables = stateVariablesIncludingInheritedAndPrivate(_contract); auto sorts = stateSorts(_contract); - vector inputSorts, outputSorts; - for (auto const& var: _function.parameters()) - inputSorts.push_back(smt::smtSortAbstractFunction(*var->type())); - for (auto const& var: _function.returnParameters()) - outputSorts.push_back(smt::smtSortAbstractFunction(*var->type())); + auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); }; + auto inputSorts = applyMap(_function.parameters(), smtSort); + auto outputSorts = applyMap(_function.returnParameters(), smtSort); return make_shared( vector{smt::SortProvider::intSort} + sorts + inputSorts + sorts + outputSorts, smt::SortProvider::boolSort @@ -769,9 +763,10 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source) smt::Expression CHC::interface() { - vector paramExprs; - for (auto const& var: m_stateVariables) - paramExprs.push_back(m_context.variable(*var)->currentValue()); + auto paramExprs = applyMap( + m_stateVariables, + [this](auto _var) { return m_context.variable(*_var)->currentValue(); } + ); return (*m_interfaces.at(m_currentContract))(paramExprs); } @@ -803,11 +798,9 @@ smt::Expression CHC::summary(FunctionDefinition const& _function) vector args{m_error.currentValue()}; auto contract = _function.annotation().contract; args += contract->isLibrary() ? stateVariablesAtIndex(0, *contract) : initialStateVariables(); - for (auto const& var: _function.parameters()) - args.push_back(m_context.variable(*var)->valueAtIndex(0)); + args += applyMap(_function.parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); }); args += contract->isLibrary() ? stateVariablesAtIndex(1, *contract) : currentStateVariables(); - for (auto const& var: _function.returnParameters()) - args.push_back(m_context.variable(*var)->currentValue()); + args += applyMap(_function.returnParameters(), [this](auto _var) { return currentValue(*_var); }); return (*m_summaries.at(m_currentContract).at(&_function))(args); } @@ -854,27 +847,21 @@ vector CHC::initialStateVariables() vector CHC::stateVariablesAtIndex(int _index) { solAssert(m_currentContract, ""); - vector exprs; - for (auto const& var: m_stateVariables) - exprs.push_back(m_context.variable(*var)->valueAtIndex(_index)); - return exprs; + return applyMap(m_stateVariables, [&](auto _var) { return valueAtIndex(*_var, _index); }); } vector CHC::stateVariablesAtIndex(int _index, ContractDefinition const& _contract) { - vector exprs; - for (auto const& var: stateVariablesIncludingInheritedAndPrivate(_contract)) - exprs.push_back(m_context.variable(*var)->valueAtIndex(_index)); - return exprs; + return applyMap( + stateVariablesIncludingInheritedAndPrivate(_contract), + [&](auto _var) { return valueAtIndex(*_var, _index); } + ); } vector CHC::currentStateVariables() { solAssert(m_currentContract, ""); - vector exprs; - for (auto const& var: m_stateVariables) - exprs.push_back(m_context.variable(*var)->currentValue()); - return exprs; + return applyMap(m_stateVariables, [this](auto _var) { return currentValue(*_var); }); } vector CHC::currentFunctionVariables() @@ -886,9 +873,7 @@ vector CHC::currentFunctionVariables() initInputExprs.push_back(m_context.variable(*var)->valueAtIndex(0)); mutableInputExprs.push_back(m_context.variable(*var)->currentValue()); } - vector returnExprs; - for (auto const& var: m_currentFunction->returnParameters()) - returnExprs.push_back(m_context.variable(*var)->currentValue()); + auto returnExprs = applyMap(m_currentFunction->returnParameters(), [this](auto _var) { return currentValue(*_var); }); return vector{m_error.currentValue()} + initialStateVariables() + initInputExprs + @@ -899,11 +884,10 @@ vector CHC::currentFunctionVariables() vector CHC::currentBlockVariables() { - vector paramExprs; if (m_currentFunction) - for (auto const& var: m_currentFunction->localVariables()) - paramExprs.push_back(m_context.variable(*var)->currentValue()); - return currentFunctionVariables() + paramExprs; + return currentFunctionVariables() + applyMap(m_currentFunction->localVariables(), [this](auto _var) { return currentValue(*_var); }); + + return currentFunctionVariables(); } string CHC::predicateName(ASTNode const* _node, ContractDefinition const* _contract) @@ -958,8 +942,7 @@ smt::Expression CHC::predicate(FunctionCall const& _funCall) m_context.variable(*param)->increaseIndex(); else createVariable(*param); - for (auto const& var: function->returnParameters()) - args.push_back(m_context.variable(*var)->currentValue()); + args += applyMap(function->returnParameters(), [this](auto _var) { return currentValue(*_var); }); if (contract->isLibrary()) return (*m_summaries.at(contract).at(function))(args); diff --git a/libsolutil/CommonData.h b/libsolutil/CommonData.h index feed0925f..bd1133511 100644 --- a/libsolutil/CommonData.h +++ b/libsolutil/CommonData.h @@ -34,6 +34,7 @@ #include #include #include +#include /// Operators need to stay in the global namespace. @@ -141,6 +142,36 @@ inline std::multiset& operator-=(std::multiset& _a, C const& _b) namespace solidity::util { +/// Functional map. +/// Returns a container _oc applying @param _op to each element in @param _c. +/// By default _oc is a vector. +/// If another return type is desired, an empty contained of that type +/// is given as @param _oc. +template())) +>>> +auto applyMap(Container const& _c, Callable&& _op, OutputContainer _oc = OutputContainer{}) +{ + std::transform(std::begin(_c), std::end(_c), std::inserter(_oc, std::end(_oc)), _op); + return _oc; +} + +/// Functional fold. +/// Given a container @param _c, an initial value @param _acc, +/// and a binary operator @param _binaryOp(T, U), accumulate +/// the elements of _c over _acc. +/// Note that has a similar function `accumulate` which +/// until C++20 does *not* std::move the partial accumulated. +template +auto fold(C const& _c, T _acc, Callable&& _binaryOp) +{ + for (auto const& e: _c) + _acc = _binaryOp(std::move(_acc), e); + return _acc; +} + template T convertContainer(U const& _from) {