From 763d27997937f5c0ffd0b9d50881bc2c0edae712 Mon Sep 17 00:00:00 2001 From: Nikola Matic Date: Mon, 14 Aug 2023 22:19:11 +0200 Subject: [PATCH] Purge using namespace from libsolidity/formal --- libsolidity/formal/ArraySlicePredicate.cpp | 13 +- libsolidity/formal/BMC.cpp | 61 ++++--- libsolidity/formal/CHC.cpp | 179 ++++++++++--------- libsolidity/formal/EncodingContext.cpp | 21 ++- libsolidity/formal/ExpressionFormatter.cpp | 25 ++- libsolidity/formal/Invariants.cpp | 13 +- libsolidity/formal/ModelChecker.cpp | 21 ++- libsolidity/formal/ModelCheckerSettings.cpp | 33 ++-- libsolidity/formal/Predicate.cpp | 107 ++++++----- libsolidity/formal/PredicateInstance.cpp | 47 +++-- libsolidity/formal/PredicateSort.cpp | 35 ++-- libsolidity/formal/SMTEncoder.cpp | 186 ++++++++++---------- libsolidity/formal/SSAVariable.cpp | 1 - libsolidity/formal/SymbolicState.cpp | 93 +++++----- libsolidity/formal/SymbolicTypes.cpp | 95 +++++----- libsolidity/formal/SymbolicVariables.cpp | 65 ++++--- libsolidity/formal/VariableUsage.cpp | 3 +- scripts/check_style.sh | 1 + 18 files changed, 492 insertions(+), 507 deletions(-) diff --git a/libsolidity/formal/ArraySlicePredicate.cpp b/libsolidity/formal/ArraySlicePredicate.cpp index f73985f1816d..21d5fb1add29 100644 --- a/libsolidity/formal/ArraySlicePredicate.cpp +++ b/libsolidity/formal/ArraySlicePredicate.cpp @@ -20,18 +20,17 @@ #include -using namespace std; using namespace solidity; using namespace solidity::smtutil; using namespace solidity::frontend; using namespace solidity::frontend::smt; -map ArraySlicePredicate::m_slicePredicates; +std::map ArraySlicePredicate::m_slicePredicates; -pair ArraySlicePredicate::create(SortPointer _sort, EncodingContext& _context) +std::pair ArraySlicePredicate::create(SortPointer _sort, EncodingContext& _context) { solAssert(_sort->kind == Kind::Tuple, ""); - auto tupleSort = dynamic_pointer_cast(_sort); + auto tupleSort = std::dynamic_pointer_cast(_sort); solAssert(tupleSort, ""); auto tupleName = tupleSort->name; @@ -47,12 +46,12 @@ pair ArraySlicePredicate::create(So smt::SymbolicIntVariable endVar{TypeProvider::uint256(), TypeProvider::uint256(), "end_" + tupleName, _context }; smt::SymbolicIntVariable iVar{TypeProvider::uint256(), TypeProvider::uint256(), "i_" + tupleName, _context}; - vector domain{sort, sort, startVar.sort(), endVar.sort()}; - auto sliceSort = make_shared(domain, SortProvider::boolSort); + std::vector domain{sort, sort, startVar.sort(), endVar.sort()}; + auto sliceSort = std::make_shared(domain, SortProvider::boolSort); Predicate const& slice = *Predicate::create(sliceSort, "array_slice_" + tupleName, PredicateType::Custom, _context); domain.emplace_back(iVar.sort()); - auto predSort = make_shared(domain, SortProvider::boolSort); + auto predSort = std::make_shared(domain, SortProvider::boolSort); Predicate const& header = *Predicate::create(predSort, "array_slice_header_" + tupleName, PredicateType::Custom, _context); Predicate const& loop = *Predicate::create(predSort, "array_slice_loop_" + tupleName, PredicateType::Custom, _context); diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index 220f6411a5ca..dede97cc036e 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -31,7 +31,6 @@ #include #endif -using namespace std; using namespace solidity; using namespace solidity::util; using namespace solidity::langutil; @@ -41,13 +40,13 @@ BMC::BMC( smt::EncodingContext& _context, UniqueErrorReporter& _errorReporter, UniqueErrorReporter& _unsupportedErrorReporter, - map const& _smtlib2Responses, + std::map const& _smtlib2Responses, ReadCallback::Callback const& _smtCallback, ModelCheckerSettings _settings, CharStreamProvider const& _charStreamProvider ): SMTEncoder(_context, _settings, _errorReporter, _unsupportedErrorReporter, _charStreamProvider), - m_interface(make_unique( + m_interface(std::make_unique( _smtlib2Responses, _smtCallback, _settings.solvers, _settings.timeout, _settings.printQuery )) { @@ -65,7 +64,7 @@ BMC::BMC( #endif } -void BMC::analyze(SourceUnit const& _source, map, smt::EncodingContext::IdCompare> _solvedTargets) +void BMC::analyze(SourceUnit const& _source, std::map, smt::EncodingContext::IdCompare> _solvedTargets) { // At this point every enabled solver is available. if (!m_settings.solvers.cvc4 && !m_settings.solvers.smtlib2 && !m_settings.solvers.z3) @@ -97,7 +96,7 @@ void BMC::analyze(SourceUnit const& _source, mapparameters()) expressionToTupleAssignment(_tryStatement.successClause()->parameters()->parameters(), *externalCall); - smtutil::Expression clauseId = m_context.newVariable("clause_choice_" + to_string(m_context.newUniqueId()), smtutil::SortProvider::uintSort); + smtutil::Expression clauseId = m_context.newVariable("clause_choice_" + std::to_string(m_context.newUniqueId()), smtutil::SortProvider::uintSort); auto const& clauses = _tryStatement.clauses(); m_context.addAssertion(clauseId >= 0 && clauseId < clauses.size()); solAssert(clauses[0].get() == _tryStatement.successClause(), "First clause of TryStatement should be the success clause"); - vector> clausesVisitResults; + std::vector> clausesVisitResults; for (size_t i = 0; i < clauses.size(); ++i) clausesVisitResults.push_back(visitBranch(clauses[i].get())); @@ -736,7 +735,7 @@ void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall) } } -pair BMC::arithmeticOperation( +std::pair BMC::arithmeticOperation( Token _op, smtutil::Expression const& _left, smtutil::Expression const& _right, @@ -800,10 +799,10 @@ void BMC::reset() m_loopExecutionHappened = false; } -pair, vector> BMC::modelExpressions() +std::pair, std::vector> BMC::modelExpressions() { - vector expressionsToEvaluate; - vector expressionNames; + std::vector expressionsToEvaluate; + std::vector expressionNames; for (auto const& var: m_context.variables()) if (var.first->type()->isValueType()) { @@ -826,7 +825,7 @@ pair, vector> BMC::modelExpressions() if (uf->annotation().type->isValueType()) { expressionsToEvaluate.emplace_back(expr(*uf)); - string expressionName; + std::string expressionName; if (uf->location().hasText()) expressionName = m_charStreamProvider.charStream(*uf->location().sourceName).text( uf->location() @@ -839,7 +838,7 @@ pair, vector> BMC::modelExpressions() /// Verification targets. -string BMC::targetDescription(BMCVerificationTarget const& _target) +std::string BMC::targetDescription(BMCVerificationTarget const& _target) { if ( _target.type == VerificationTargetType::Underflow || @@ -1065,20 +1064,20 @@ void BMC::addVerificationTarget( void BMC::checkCondition( BMCVerificationTarget const& _target, smtutil::Expression _condition, - vector const& _callStack, - pair, vector> const& _modelExpressions, + std::vector const& _callStack, + std::pair, std::vector> const& _modelExpressions, SourceLocation const& _location, ErrorId _errorHappens, ErrorId _errorMightHappen, - string const& _additionalValueName, + std::string const& _additionalValueName, smtutil::Expression const* _additionalValue ) { m_interface->push(); m_interface->addAssertion(_condition); - vector expressionsToEvaluate; - vector expressionNames; + std::vector expressionsToEvaluate; + std::vector expressionNames; tie(expressionsToEvaluate, expressionNames) = _modelExpressions; if (!_callStack.empty()) if (_additionalValue) @@ -1087,10 +1086,10 @@ void BMC::checkCondition( expressionNames.push_back(_additionalValueName); } smtutil::CheckResult result; - vector values; + std::vector values; tie(result, values) = checkSatisfiableAndGenerateModel(expressionsToEvaluate); - string extraComment = SMTEncoder::extraComment(); + std::string extraComment = SMTEncoder::extraComment(); if (m_loopExecutionHappened) extraComment += "False negatives are possible when unrolling loops.\n" @@ -1119,7 +1118,7 @@ void BMC::checkCondition( if (values.size() == expressionNames.size()) { modelMessage << "Counterexample:\n"; - map sortedModel; + std::map sortedModel; for (size_t i = 0; i < values.size(); ++i) if (expressionsToEvaluate.at(i).name != values.at(i)) sortedModel[expressionNames.at(i)] = values.at(i); @@ -1165,7 +1164,7 @@ void BMC::checkBooleanNotConstant( Expression const& _condition, smtutil::Expression const& _constraints, smtutil::Expression const& _value, - vector const& _callStack + std::vector const& _callStack ) { // Do not check for const-ness if this is a constant. @@ -1198,7 +1197,7 @@ void BMC::checkBooleanNotConstant( m_errorReporter.warning(2512_error, _condition.location(), "BMC: Condition unreachable.", SMTEncoder::callStackMessage(_callStack)); else { - string description; + std::string description; if (positiveResult == smtutil::CheckResult::SATISFIABLE) { solAssert(negatedResult == smtutil::CheckResult::UNSATISFIABLE, ""); @@ -1219,17 +1218,17 @@ void BMC::checkBooleanNotConstant( } } -pair> -BMC::checkSatisfiableAndGenerateModel(vector const& _expressionsToEvaluate) +std::pair> +BMC::checkSatisfiableAndGenerateModel(std::vector const& _expressionsToEvaluate) { smtutil::CheckResult result; - vector values; + std::vector values; try { if (m_settings.printQuery) { auto portfolio = dynamic_cast(m_interface.get()); - string smtlibCode = portfolio->dumpQuery(_expressionsToEvaluate); + std::string smtlibCode = portfolio->dumpQuery(_expressionsToEvaluate); m_errorReporter.info( 6240_error, "BMC: Requested query:\n" + smtlibCode @@ -1239,14 +1238,14 @@ BMC::checkSatisfiableAndGenerateModel(vector const& _expres } catch (smtutil::SolverError const& _e) { - string description("BMC: Error querying SMT solver"); + std::string description("BMC: Error querying SMT solver"); if (_e.comment()) description += ": " + *_e.comment(); m_errorReporter.warning(8140_error, description); result = smtutil::CheckResult::ERROR; } - for (string& value: values) + for (std::string& value: values) { try { diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 30c3bb0e9844..a803f87d0a1c 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -51,7 +51,6 @@ #include #include -using namespace std; using namespace solidity; using namespace solidity::util; using namespace solidity::langutil; @@ -63,7 +62,7 @@ CHC::CHC( EncodingContext& _context, UniqueErrorReporter& _errorReporter, UniqueErrorReporter& _unsupportedErrorReporter, - map const& _smtlib2Responses, + std::map const& _smtlib2Responses, ReadCallback::Callback const& _smtCallback, ModelCheckerSettings _settings, CharStreamProvider const& _charStreamProvider @@ -130,7 +129,7 @@ void CHC::analyze(SourceUnit const& _source) ); } -vector CHC::unhandledQueries() const +std::vector CHC::unhandledQueries() const { if (auto smtlib2 = dynamic_cast(m_interface.get())) return smtlib2->unhandledQueries(); @@ -213,7 +212,7 @@ void CHC::endVisit(ContractDefinition const& _contract) auto baseConstructor = base->constructor(); if (baseConstructor && baseArgs.count(base)) { - vector> const& args = baseArgs.at(base); + std::vector> const& args = baseArgs.at(base); auto const& params = baseConstructor->parameters(); solAssert(params.size() == args.size(), ""); for (unsigned i = 0; i < params.size(); ++i) @@ -280,7 +279,7 @@ bool CHC::visit(FunctionDefinition const& _function) conj = conj && currentEqualInitialVarsConstraints(stateVariablesIncludingInheritedAndPrivate(_function)); conj = conj && errorFlag().currentValue() == 0; - addRule(smtutil::Expression::implies(conj, summary(_function)), "summary_function_" + to_string(_function.id())); + addRule(smtutil::Expression::implies(conj, summary(_function)), "summary_function_" + std::to_string(_function.id())); return false; } @@ -433,7 +432,7 @@ bool CHC::visit(WhileStatement const& _while) solAssert(m_currentFunction, ""); auto const& functionBody = m_currentFunction->body(); - auto namePrefix = string(_while.isDoWhile() ? "do_" : "") + "while"; + auto namePrefix = std::string(_while.isDoWhile() ? "do_" : "") + "while"; auto loopHeaderBlock = createBlock(&_while, PredicateType::FunctionBlock, namePrefix + "_header_"); auto loopBodyBlock = createBlock(&_while.body(), PredicateType::FunctionBlock, namePrefix + "_body_"); auto afterLoopBlock = createBlock(&functionBody, PredicateType::FunctionBlock); @@ -622,8 +621,8 @@ void CHC::endVisit(IndexRangeAccess const& _range) { createExpr(_range); - auto baseArray = dynamic_pointer_cast(m_context.expression(_range.baseExpression())); - auto sliceArray = dynamic_pointer_cast(m_context.expression(_range)); + auto baseArray = std::dynamic_pointer_cast(m_context.expression(_range.baseExpression())); + auto sliceArray = std::dynamic_pointer_cast(m_context.expression(_range)); solAssert(baseArray && sliceArray, ""); auto const& sliceData = ArraySlicePredicate::create(sliceArray->sort(), m_context); @@ -864,7 +863,7 @@ void CHC::nondetCall(ContractDefinition const& _contract, VariableDeclaration co state().readStateVars(_contract, address); m_context.addAssertion(state().state() == state().state(0)); - auto preCallState = vector{state().state()} + currentStateVariables(_contract); + auto preCallState = std::vector{state().state()} + currentStateVariables(_contract); state().newState(); for (auto const* var: _contract.stateVariables()) @@ -879,8 +878,8 @@ void CHC::nondetCall(ContractDefinition const& _contract, VariableDeclaration co &_var, m_currentContract ); - auto postCallState = vector{state().state()} + currentStateVariables(_contract); - vector stateExprs{error, address, state().abi(), state().crypto()}; + auto postCallState = std::vector{state().state()} + currentStateVariables(_contract); + std::vector stateExprs{error, address, state().abi(), state().crypto()}; auto nondet = (*m_nondetInterfaces.at(&_contract))(stateExprs + preCallState + postCallState); auto nondetCall = callPredicate(stateExprs + preCallState + postCallState); @@ -945,7 +944,7 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall) if (Expression const* value = valueOption(callOptions)) decreaseBalanceFromOptionsValue(*value); - auto preCallState = vector{state().state()} + currentStateVariables(); + auto preCallState = std::vector{state().state()} + currentStateVariables(); if (!usesStaticCall(_funCall)) { @@ -962,8 +961,8 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall) PredicateType::ExternalCallUntrusted, &_funCall ); - auto postCallState = vector{state().state()} + currentStateVariables(); - vector stateExprs{error, state().thisAddress(), state().abi(), state().crypto()}; + auto postCallState = std::vector{state().state()} + currentStateVariables(); + std::vector stateExprs{error, state().thisAddress(), state().abi(), state().crypto()}; auto nondet = (*m_nondetInterfaces.at(m_currentContract))(stateExprs + preCallState + postCallState); auto nondetCall = callPredicate(stateExprs + preCallState + postCallState); @@ -1076,7 +1075,7 @@ void CHC::makeArrayPopVerificationTarget(FunctionCall const& _arrayPop) auto memberAccess = dynamic_cast(cleanExpression(_arrayPop.expression())); solAssert(memberAccess, ""); - auto symbArray = dynamic_pointer_cast(m_context.expression(memberAccess->expression())); + auto symbArray = std::dynamic_pointer_cast(m_context.expression(memberAccess->expression())); solAssert(symbArray, ""); verificationTargetEncountered(&_arrayPop, VerificationTargetType::PopEmptyArray, symbArray->length() <= 0); @@ -1089,7 +1088,7 @@ void CHC::makeOutOfBoundsVerificationTarget(IndexAccess const& _indexAccess) auto baseType = _indexAccess.baseExpression().annotation().type; - optional length; + std::optional length; if (smt::isArray(*baseType)) length = dynamic_cast( *m_context.expression(_indexAccess.baseExpression()) @@ -1097,7 +1096,7 @@ void CHC::makeOutOfBoundsVerificationTarget(IndexAccess const& _indexAccess) else if (auto const* type = dynamic_cast(baseType)) length = smtutil::Expression(static_cast(type->numBytes())); - optional target; + std::optional target; if ( auto index = _indexAccess.indexExpression(); index && length @@ -1108,7 +1107,7 @@ void CHC::makeOutOfBoundsVerificationTarget(IndexAccess const& _indexAccess) verificationTargetEncountered(&_indexAccess, VerificationTargetType::OutOfBounds, *target); } -pair CHC::arithmeticOperation( +std::pair CHC::arithmeticOperation( Token _op, smtutil::Expression const& _left, smtutil::Expression const& _right, @@ -1192,7 +1191,7 @@ void CHC::resetSourceAnalysis() solAssert(m_settings.solvers.smtlib2 || m_settings.solvers.eld); if (!m_interface) - m_interface = make_unique(m_smtlib2Responses, m_smtCallback, m_settings.solvers, m_settings.timeout); + m_interface = std::make_unique(m_smtlib2Responses, m_smtCallback, m_settings.solvers, m_settings.timeout); auto smtlib2Interface = dynamic_cast(m_interface.get()); solAssert(smtlib2Interface, ""); @@ -1249,9 +1248,9 @@ void CHC::setCurrentBlock(Predicate const& _block) m_currentBlock = predicate(_block); } -set CHC::transactionVerificationTargetsIds(ASTNode const* _txRoot) +std::set CHC::transactionVerificationTargetsIds(ASTNode const* _txRoot) { - set verificationTargetsIds; + std::set verificationTargetsIds; struct ASTNodeCompare: EncodingContext::IdCompare { bool operator<(ASTNodeCompare _other) const { return operator()(node, _other.node); } @@ -1273,9 +1272,9 @@ bool CHC::usesStaticCall(FunctionCall const& _funCall) return (function && (function->stateMutability() == StateMutability::Pure || function->stateMutability() == StateMutability::View)) || kind == FunctionType::Kind::BareStaticCall; } -optional CHC::natspecOptionFromString(string const& _option) +std::optional CHC::natspecOptionFromString(std::string const& _option) { - static map options{ + static std::map options{ {"abstract-function-nondet", CHCNatspecOption::AbstractFunctionNondet} }; if (options.count(_option)) @@ -1283,15 +1282,15 @@ optional CHC::natspecOptionFromString(string const& _opti return {}; } -set CHC::smtNatspecTags(FunctionDefinition const& _function) +std::set CHC::smtNatspecTags(FunctionDefinition const& _function) { - set options; - string smtStr = "custom:smtchecker"; + std::set options; + std::string smtStr = "custom:smtchecker"; bool errorSeen = false; for (auto const& [tag, value]: _function.annotation().docTags) if (tag == smtStr) { - string const& content = value.content; + std::string const& content = value.content; if (auto option = natspecOptionFromString(content)) options.insert(*option); else if (!errorSeen) @@ -1327,7 +1326,7 @@ SortPointer CHC::sort(ASTNode const* _node) return functionBodySort(*m_currentFunction, m_currentContract, state()); } -Predicate const* CHC::createSymbolicBlock(SortPointer _sort, string const& _name, PredicateType _predType, ASTNode const* _node, ContractDefinition const* _contractContext) +Predicate const* CHC::createSymbolicBlock(SortPointer _sort, std::string const& _name, PredicateType _predType, ASTNode const* _node, ContractDefinition const* _contractContext) { auto const* block = Predicate::create(_sort, _name, _predType, m_context, _node, _contractContext, m_scopes); m_interface->registerRelation(block->functor()); @@ -1339,7 +1338,7 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source) for (auto const& node: _source.nodes()) if (auto const* contract = dynamic_cast(node.get())) { - string suffix = contract->name() + "_" + to_string(contract->id()); + std::string suffix = contract->name() + "_" + std::to_string(contract->id()); m_interfaces[contract] = createSymbolicBlock(interfaceSort(*contract, state()), "interface_" + uniquePrefix() + "_" + suffix, PredicateType::Interface, contract, contract); m_nondetInterfaces[contract] = createSymbolicBlock(nondetInterfaceSort(*contract, state()), "nondet_interface_" + uniquePrefix() + "_" + suffix, PredicateType::NondetInterface, contract, contract); m_constructorSummaries[contract] = createConstructorBlock(*contract, "summary_constructor"); @@ -1385,10 +1384,10 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source) auto errorPost = errorFlag().increaseIndex(); auto nondetPost = smt::nondetInterface(iface, *contract, m_context, 0, 2); - vector args{errorPost, state().thisAddress(), state().abi(), state().crypto(), state().tx(), state().state(1)}; + std::vector args{errorPost, state().thisAddress(), state().abi(), state().crypto(), state().tx(), state().state(1)}; args += state1 + applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); }) + - vector{state().state(2)} + + std::vector{state().state(2)} + state2 + applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 1); }) + applyMap(function->returnParameters(), [this](auto _var) { return valueAtIndex(*_var, 1); }); @@ -1416,7 +1415,7 @@ void CHC::defineExternalFunctionInterface(FunctionDefinition const& _function, C // block.coinbase, which do not trigger calls into the contract. // So the only constraint we can add here is that the balance of // the contract grows by at least `msg.value`. - SymbolicIntVariable k{TypeProvider::uint256(), TypeProvider::uint256(), "funds_" + to_string(m_context.newUniqueId()), m_context}; + SymbolicIntVariable k{TypeProvider::uint256(), TypeProvider::uint256(), "funds_" + std::to_string(m_context.newUniqueId()), m_context}; m_context.addAssertion(k.currentValue() >= state().txMember("msg.value")); // Assume that address(this).balance cannot overflow. m_context.addAssertion(smt::symbolicUnknownConstraints(state().balance(state().thisAddress()) + k.currentValue(), TypeProvider::uint256())); @@ -1582,7 +1581,7 @@ smtutil::Expression CHC::externalSummary(FunctionDefinition const& _function) return externalSummary(_function, *m_currentContract); } -Predicate const* CHC::createBlock(ASTNode const* _node, PredicateType _predType, string const& _prefix) +Predicate const* CHC::createBlock(ASTNode const* _node, PredicateType _predType, std::string const& _prefix) { auto block = createSymbolicBlock( sort(_node), @@ -1607,7 +1606,7 @@ Predicate const* CHC::createSummaryBlock(FunctionDefinition const& _function, Co ); } -Predicate const* CHC::createConstructorBlock(ContractDefinition const& _contract, string const& _prefix) +Predicate const* CHC::createConstructorBlock(ContractDefinition const& _contract, std::string const& _prefix) { return createSymbolicBlock( constructorSort(_contract, state()), @@ -1622,7 +1621,7 @@ void CHC::createErrorBlock() { m_errorPredicate = createSymbolicBlock( arity0FunctionSort(), - "error_target_" + to_string(m_context.newUniqueId()), + "error_target_" + std::to_string(m_context.newUniqueId()), PredicateType::Error ); m_interface->registerRelation(m_errorPredicate->functor()); @@ -1650,18 +1649,18 @@ smtutil::Expression CHC::initialConstraints(ContractDefinition const& _contract, return conj; } -vector CHC::initialStateVariables() +std::vector CHC::initialStateVariables() { return stateVariablesAtIndex(0); } -vector CHC::stateVariablesAtIndex(unsigned _index) +std::vector CHC::stateVariablesAtIndex(unsigned _index) { solAssert(m_currentContract, ""); return stateVariablesAtIndex(_index, *m_currentContract); } -vector CHC::stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract) +std::vector CHC::stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract) { return applyMap( SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract), @@ -1669,27 +1668,27 @@ vector CHC::stateVariablesAtIndex(unsigned _index, Contract ); } -vector CHC::currentStateVariables() +std::vector CHC::currentStateVariables() { solAssert(m_currentContract, ""); return currentStateVariables(*m_currentContract); } -vector CHC::currentStateVariables(ContractDefinition const& _contract) +std::vector CHC::currentStateVariables(ContractDefinition const& _contract) { return applyMap(SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract), [this](auto _var) { return currentValue(*_var); }); } -smtutil::Expression CHC::currentEqualInitialVarsConstraints(vector const& _vars) const +smtutil::Expression CHC::currentEqualInitialVarsConstraints(std::vector const& _vars) const { return fold(_vars, smtutil::Expression(true), [this](auto&& _conj, auto _var) { return std::move(_conj) && currentValue(*_var) == m_context.variable(*_var)->valueAtIndex(0); }); } -string CHC::predicateName(ASTNode const* _node, ContractDefinition const* _contract) +std::string CHC::predicateName(ASTNode const* _node, ContractDefinition const* _contract) { - string prefix; + std::string prefix; if (auto funDef = dynamic_cast(_node)) { prefix += TokenTraits::toString(funDef->kind()); @@ -1701,7 +1700,7 @@ string CHC::predicateName(ASTNode const* _node, ContractDefinition const* _contr auto contract = _contract ? _contract : m_currentContract; solAssert(contract, ""); - return prefix + "_" + to_string(_node->id()) + "_" + to_string(contract->id()); + return prefix + "_" + std::to_string(_node->id()) + "_" + std::to_string(contract->id()); } smtutil::Expression CHC::predicate(Predicate const& _block) @@ -1756,7 +1755,7 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall) solAssert(false, "Unreachable!"); }; errorFlag().increaseIndex(); - vector args{errorFlag().currentValue(), contractAddressValue(_funCall), state().abi(), state().crypto(), state().tx(), state().state()}; + std::vector args{errorFlag().currentValue(), contractAddressValue(_funCall), state().abi(), state().crypto(), state().tx(), state().state()}; auto const* contract = function->annotation().contract; auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts; @@ -1773,7 +1772,7 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall) for (auto const& var: stateVariablesIncludingInheritedAndPrivate(*contract)) m_context.variable(*var)->increaseIndex(); } - args += vector{state().state()}; + args += std::vector{state().state()}; args += currentStateVariables(*contract); for (auto var: function->parameters() + function->returnParameters()) @@ -1798,12 +1797,12 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall) return callPredicate(args); } -void CHC::addRule(smtutil::Expression const& _rule, string const& _ruleName) +void CHC::addRule(smtutil::Expression const& _rule, std::string const& _ruleName) { m_interface->addRule(_rule, _ruleName); } -tuple CHC::query(smtutil::Expression const& _query, langutil::SourceLocation const& _location) +std::tuple CHC::query(smtutil::Expression const& _query, langutil::SourceLocation const& _location) { CheckResult result; smtutil::Expression invariant(true); @@ -1812,13 +1811,13 @@ tuple CHC::query { auto smtLibInterface = dynamic_cast(m_interface.get()); solAssert(smtLibInterface, "Requested to print queries but CHCSmtLib2Interface not available"); - string smtLibCode = smtLibInterface->dumpQuery(_query); + std::string smtLibCode = smtLibInterface->dumpQuery(_query); m_errorReporter.info( 2339_error, "CHC: Requested query:\n" + smtLibCode ); } - tie(result, invariant, cex) = m_interface->query(_query); + std::tie(result, invariant, cex) = m_interface->query(_query); switch (result) { case CheckResult::SATISFIABLE: @@ -1836,7 +1835,7 @@ tuple CHC::query CheckResult resultNoOpt; smtutil::Expression invariantNoOpt(true); CHCSolverInterface::CexGraph cexNoOpt; - tie(resultNoOpt, invariantNoOpt, cexNoOpt) = m_interface->query(_query); + std::tie(resultNoOpt, invariantNoOpt, cexNoOpt) = m_interface->query(_query); if (resultNoOpt == CheckResult::SATISFIABLE) cex = std::move(cexNoOpt); @@ -1902,7 +1901,7 @@ void CHC::verificationTargetEncountered( m_context.addAssertion(errorFlag().currentValue() == previousError); } -pair CHC::targetDescription(CHCVerificationTarget const& _target) +std::pair CHC::targetDescription(CHCVerificationTarget const& _target) { if (_target.type == VerificationTargetType::PopEmptyArray) { @@ -1950,7 +1949,7 @@ void CHC::checkVerificationTargets() // Also, all possible contexts in which an external function can be called has been recorded (m_queryPlaceholders). // Here we combine every context in which an external function can be called with all possible verification conditions // in its call graph. Each such combination forms a unique verification target. - map> targetEntryPoints; + std::map> targetEntryPoints; for (auto const& [function, placeholders]: m_queryPlaceholders) { auto functionTargets = transactionVerificationTargetsIds(function); @@ -1959,7 +1958,7 @@ void CHC::checkVerificationTargets() targetEntryPoints[id].push_back(placeholder); } - set checkedErrorIds; + std::set checkedErrorIds; for (auto const& [targetId, placeholders]: targetEntryPoints) { auto const& target = m_verificationTargets.at(targetId); @@ -1988,7 +1987,7 @@ void CHC::checkVerificationTargets() 5840_error, {}, "CHC: " + - to_string(m_unprovedTargets.size()) + + std::to_string(m_unprovedTargets.size()) + " verification condition(s) could not be proved." + " Enable the model checker option \"show unproved\" to see all of them." + " Consider choosing a specific contract to be verified in order to reduce the solving problems." + @@ -1999,7 +1998,7 @@ void CHC::checkVerificationTargets() m_errorReporter.info( 1391_error, "CHC: " + - to_string(m_safeTargets.size()) + + std::to_string(m_safeTargets.size()) + " verification condition(s) proved safe!" + " Enable the model checker option \"show proved safe\" to see all of them." ); @@ -2016,17 +2015,17 @@ void CHC::checkVerificationTargets() if (!m_settings.invariants.invariants.empty()) { - string msg; + std::string msg; for (auto pred: m_invariants | ranges::views::keys) { ASTNode const* node = pred->programNode(); - string what; + std::string what; if (auto contract = dynamic_cast(node)) what = contract->fullyQualifiedName(); else solAssert(false, ""); - string invType; + std::string invType; if (pred->type() == PredicateType::Interface) invType = "Contract invariant(s)"; else if (pred->type() == PredicateType::NondetInterface) @@ -2038,16 +2037,16 @@ void CHC::checkVerificationTargets() for (auto const& inv: m_invariants.at(pred)) msg += inv + "\n"; } - if (msg.find("") != string::npos) + if (msg.find("") != std::string::npos) { - set seenErrors; + std::set seenErrors; msg += " = 0 -> no errors\n"; for (auto const& [id, target]: m_verificationTargets) if (!seenErrors.count(target.errorId)) { seenErrors.insert(target.errorId); - string loc = string(m_charStreamProvider.charStream(*target.errorNode->location().sourceName).text(target.errorNode->location())); - msg += " = " + to_string(target.errorId) + " -> " + ModelCheckerTargets::targetTypeToString.at(target.type) + " at " + loc + "\n"; + std::string loc = std::string(m_charStreamProvider.charStream(*target.errorNode->location().sourceName).text(target.errorNode->location())); + msg += " = " + std::to_string(target.errorId) + " -> " + ModelCheckerTargets::targetTypeToString.at(target.type) + " at " + loc + "\n"; } } @@ -2058,12 +2057,12 @@ void CHC::checkVerificationTargets() // There can be targets in internal functions that are not reachable from the external interface. // These are safe by definition and are not even checked by the CHC engine, but this information // must still be reported safe by the BMC engine. - set allErrorIds; + std::set allErrorIds; for (auto const& entry: m_functionTargetIds) for (unsigned id: entry.second) allErrorIds.insert(id); - set unreachableErrorIds; + std::set unreachableErrorIds; set_difference( allErrorIds.begin(), allErrorIds.end(), @@ -2077,10 +2076,10 @@ void CHC::checkVerificationTargets() void CHC::checkAndReportTarget( CHCVerificationTarget const& _target, - vector const& _placeholders, + std::vector const& _placeholders, ErrorId _errorReporterId, - string _satMsg, - string _unknownMsg + std::string _satMsg, + std::string _unknownMsg ) { if (m_unsafeTargets.count(_target.errorNode) && m_unsafeTargets.at(_target.errorNode).count(_target.type)) @@ -2098,12 +2097,12 @@ void CHC::checkAndReportTarget( if (result == CheckResult::UNSATISFIABLE) { m_safeTargets[_target.errorNode].insert(_target); - set predicates; + std::set predicates; for (auto const* pred: m_interfaces | ranges::views::values) predicates.insert(pred); for (auto const* pred: m_nondetInterfaces | ranges::views::values) predicates.insert(pred); - map> invariants = collectInvariants(invariant, predicates, m_settings.invariants); + std::map> invariants = collectInvariants(invariant, predicates, m_settings.invariants); for (auto pred: invariants | ranges::views::keys) m_invariants[pred] += std::move(invariants.at(pred)); } @@ -2153,9 +2152,9 @@ the function summaries in the callgraph of the error node is the reverse transac The first function summary seen contains the values for the state, input and output variables at the error point. */ -optional CHC::generateCounterexample(CHCSolverInterface::CexGraph const& _graph, string const& _root) +std::optional CHC::generateCounterexample(CHCSolverInterface::CexGraph const& _graph, std::string const& _root) { - optional rootId; + std::optional rootId; for (auto const& [id, node]: _graph.nodes) if (node.name == _root) { @@ -2165,8 +2164,8 @@ optional CHC::generateCounterexample(CHCSolverInterface::CexGraph const& if (!rootId) return {}; - vector path; - string localState; + std::vector path; + std::string localState; auto callGraph = summaryCalls(_graph, *rootId); @@ -2204,7 +2203,7 @@ optional CHC::generateCounterexample(CHCSolverInterface::CexGraph const& if (auto outStr = formatVariableModel(outParams, outValues, "\n"); !outStr.empty()) localState += outStr + "\n"; - optional localErrorId; + std::optional localErrorId; solidity::util::BreadthFirstSearch bfs{{summaryId}}; bfs.run([&](auto _nodeId, auto&& _addChild) { auto const& children = _graph.edges.at(_nodeId); @@ -2239,9 +2238,9 @@ optional CHC::generateCounterexample(CHCSolverInterface::CexGraph const& } } - string txCex = summaryPredicate->formatSummaryCall(summaryArgs, m_charStreamProvider); + std::string txCex = summaryPredicate->formatSummaryCall(summaryArgs, m_charStreamProvider); - list calls; + std::list calls; auto dfs = [&](unsigned parent, unsigned node, unsigned depth, auto&& _dfs) -> void { auto pred = nodePred(node); auto parentPred = nodePred(parent); @@ -2254,7 +2253,7 @@ optional CHC::generateCounterexample(CHCSolverInterface::CexGraph const& bool appendTxVars = pred->isConstructorSummary() || pred->isFunctionSummary() || pred->isExternalCallUntrusted(); - calls.push_front(string(depth * 4, ' ') + pred->formatSummaryCall(nodeArgs(node), m_charStreamProvider, appendTxVars)); + calls.push_front(std::string(depth * 4, ' ') + pred->formatSummaryCall(nodeArgs(node), m_charStreamProvider, appendTxVars)); if (pred->isInternalCall()) calls.front() += " -- internal call"; else if (pred->isExternalCallTrusted()) @@ -2281,12 +2280,12 @@ optional CHC::generateCounterexample(CHCSolverInterface::CexGraph const& return localState + "\nTransaction trace:\n" + boost::algorithm::join(path | ranges::views::reverse, "\n"); } -map> CHC::summaryCalls(CHCSolverInterface::CexGraph const& _graph, unsigned _root) +std::map> CHC::summaryCalls(CHCSolverInterface::CexGraph const& _graph, unsigned _root) { - map> calls; + std::map> calls; auto compare = [&](unsigned _a, unsigned _b) { - auto extract = [&](string const& _s) { + auto extract = [&](std::string const& _s) { // We want to sort sibling predicates in the counterexample graph by their unique predicate id. // For most predicates, this actually doesn't matter. // The cases where this matters are internal and external function calls which have the form: @@ -2312,7 +2311,7 @@ map> CHC::summaryCalls(CHCSolverInterface::CexGraph c return extract(_graph.nodes.at(_a).name) > extract(_graph.nodes.at(_b).name); }; - queue> q; + std::queue> q; q.push({_root, _root}); while (!q.empty()) { @@ -2334,19 +2333,19 @@ map> CHC::summaryCalls(CHCSolverInterface::CexGraph c root = node; } auto const& edges = _graph.edges.at(node); - for (unsigned v: set(begin(edges), end(edges), compare)) + for (unsigned v: std::set(begin(edges), end(edges), compare)) q.push({v, root}); } return calls; } -string CHC::cex2dot(CHCSolverInterface::CexGraph const& _cex) +std::string CHC::cex2dot(CHCSolverInterface::CexGraph const& _cex) { - string dot = "digraph {\n"; + std::string dot = "digraph {\n"; auto pred = [&](CHCSolverInterface::CexNode const& _node) { - vector args = applyMap( + std::vector args = applyMap( _node.arguments, [&](auto const& arg) { return arg.name; } ); @@ -2361,14 +2360,14 @@ string CHC::cex2dot(CHCSolverInterface::CexGraph const& _cex) return dot; } -string CHC::uniquePrefix() +std::string CHC::uniquePrefix() { - return to_string(m_blockCounter++); + return std::to_string(m_blockCounter++); } -string CHC::contractSuffix(ContractDefinition const& _contract) +std::string CHC::contractSuffix(ContractDefinition const& _contract) { - return _contract.name() + "_" + to_string(_contract.id()); + return _contract.name() + "_" + std::to_string(_contract.id()); } unsigned CHC::newErrorId() diff --git a/libsolidity/formal/EncodingContext.cpp b/libsolidity/formal/EncodingContext.cpp index 2000efd07e2a..e0a09bcf7b8f 100644 --- a/libsolidity/formal/EncodingContext.cpp +++ b/libsolidity/formal/EncodingContext.cpp @@ -20,7 +20,6 @@ #include -using namespace std; using namespace solidity; using namespace solidity::util; using namespace solidity::frontend::smt; @@ -51,7 +50,7 @@ unsigned EncodingContext::newUniqueId() /// Variables. -shared_ptr EncodingContext::variable(frontend::VariableDeclaration const& _varDecl) +std::shared_ptr EncodingContext::variable(frontend::VariableDeclaration const& _varDecl) { solAssert(knownVariable(_varDecl), ""); return m_variables[&_varDecl]; @@ -61,7 +60,7 @@ bool EncodingContext::createVariable(frontend::VariableDeclaration const& _varDe { solAssert(!knownVariable(_varDecl), ""); auto const& type = _varDecl.type(); - auto result = newSymbolicVariable(*type, _varDecl.name() + "_" + to_string(_varDecl.id()), *this); + auto result = newSymbolicVariable(*type, _varDecl.name() + "_" + std::to_string(_varDecl.id()), *this); m_variables.emplace(&_varDecl, result.second); return result.first; } @@ -77,13 +76,13 @@ void EncodingContext::resetVariable(frontend::VariableDeclaration const& _variab setUnknownValue(_variable); } -void EncodingContext::resetVariables(set const& _variables) +void EncodingContext::resetVariables(std::set const& _variables) { for (auto const* decl: _variables) resetVariable(*decl); } -void EncodingContext::resetVariables(function const& _filter) +void EncodingContext::resetVariables(std::function const& _filter) { for_each(begin(m_variables), end(m_variables), [&](auto _variable) { @@ -127,14 +126,14 @@ void EncodingContext::setUnknownValue(SymbolicVariable& _variable) /// Expressions -shared_ptr EncodingContext::expression(frontend::Expression const& _e) +std::shared_ptr EncodingContext::expression(frontend::Expression const& _e) { if (!knownExpression(_e)) createExpression(_e); return m_expressions.at(&_e); } -bool EncodingContext::createExpression(frontend::Expression const& _e, shared_ptr _symbVar) +bool EncodingContext::createExpression(frontend::Expression const& _e, std::shared_ptr _symbVar) { solAssert(_e.annotation().type, ""); if (knownExpression(_e)) @@ -149,7 +148,7 @@ bool EncodingContext::createExpression(frontend::Expression const& _e, shared_pt } else { - auto result = newSymbolicVariable(*_e.annotation().type, "expr_" + to_string(_e.id()), *this); + auto result = newSymbolicVariable(*_e.annotation().type, "expr_" + std::to_string(_e.id()), *this); m_expressions.emplace(&_e, result.second); return result.first; } @@ -162,13 +161,13 @@ bool EncodingContext::knownExpression(frontend::Expression const& _e) const /// Global variables and functions. -shared_ptr EncodingContext::globalSymbol(string const& _name) +std::shared_ptr EncodingContext::globalSymbol(std::string const& _name) { solAssert(knownGlobalSymbol(_name), ""); return m_globalContext.at(_name); } -bool EncodingContext::createGlobalSymbol(string const& _name, frontend::Expression const& _expr) +bool EncodingContext::createGlobalSymbol(std::string const& _name, frontend::Expression const& _expr) { solAssert(!knownGlobalSymbol(_name), ""); auto result = newSymbolicVariable(*_expr.annotation().type, _name, *this); @@ -177,7 +176,7 @@ bool EncodingContext::createGlobalSymbol(string const& _name, frontend::Expressi return result.first; } -bool EncodingContext::knownGlobalSymbol(string const& _var) const +bool EncodingContext::knownGlobalSymbol(std::string const& _var) const { return m_globalContext.count(_var); } diff --git a/libsolidity/formal/ExpressionFormatter.cpp b/libsolidity/formal/ExpressionFormatter.cpp index 2591328f8403..cf2f2c3b8126 100644 --- a/libsolidity/formal/ExpressionFormatter.cpp +++ b/libsolidity/formal/ExpressionFormatter.cpp @@ -29,7 +29,6 @@ #include #include -using namespace std; using boost::algorithm::starts_with; using namespace solidity; using namespace solidity::util; @@ -42,7 +41,7 @@ namespace solidity::frontend::smt namespace { -string formatDatatypeAccessor(smtutil::Expression const& _expr, vector const& _args) +std::string formatDatatypeAccessor(smtutil::Expression const& _expr, std::vector const& _args) { auto const& op = _expr.name; @@ -63,9 +62,9 @@ string formatDatatypeAccessor(smtutil::Expression const& _expr, vector c if (op == "dt_accessor_ecrecover") return "ecrecover"; - string accessorStr = "accessor_"; + std::string accessorStr = "accessor_"; // Struct members have suffix "accessor_". - string type = op.substr(op.rfind(accessorStr) + accessorStr.size()); + std::string type = op.substr(op.rfind(accessorStr) + accessorStr.size()); solAssert(_expr.arguments.size() == 1, ""); if (type == "length") @@ -87,22 +86,22 @@ string formatDatatypeAccessor(smtutil::Expression const& _expr, vector c return _args.at(0) + "." + type; } -string formatGenericOp(smtutil::Expression const& _expr, vector const& _args) +std::string formatGenericOp(smtutil::Expression const& _expr, std::vector const& _args) { return _expr.name + "(" + boost::algorithm::join(_args, ", ") + ")"; } -string formatInfixOp(string const& _op, vector const& _args) +std::string formatInfixOp(std::string const& _op, std::vector const& _args) { return "(" + boost::algorithm::join(_args, " " + _op + " ") + ")"; } -string formatArrayOp(smtutil::Expression const& _expr, vector const& _args) +std::string formatArrayOp(smtutil::Expression const& _expr, std::vector const& _args) { if (_expr.name == "select") { auto const& a0 = _args.at(0); - static set const ufs{"keccak256", "sha256", "ripemd160", "ecrecover"}; + static std::set const ufs{"keccak256", "sha256", "ripemd160", "ecrecover"}; if (ufs.count(a0) || starts_with(a0, "t_function_abi")) return _args.at(0) + "(" + _args.at(1) + ")"; return _args.at(0) + "[" + _args.at(1) + "]"; @@ -112,7 +111,7 @@ string formatArrayOp(smtutil::Expression const& _expr, vector const& _ar return formatGenericOp(_expr, _args); } -string formatUnaryOp(smtutil::Expression const& _expr, vector const& _args) +std::string formatUnaryOp(smtutil::Expression const& _expr, std::vector const& _args) { if (_expr.name == "not") return "!" + _args.at(0); @@ -122,7 +121,7 @@ string formatUnaryOp(smtutil::Expression const& _expr, vector const& _ar } -smtutil::Expression substitute(smtutil::Expression _from, map const& _subst) +smtutil::Expression substitute(smtutil::Expression _from, std::map const& _subst) { // TODO For now we ignore nested quantifier expressions, // but we should support them in the future. @@ -135,7 +134,7 @@ smtutil::Expression substitute(smtutil::Expression _from, map co return _from; } -string toSolidityStr(smtutil::Expression const& _expr) +std::string toSolidityStr(smtutil::Expression const& _expr) { auto const& op = _expr.name; @@ -150,7 +149,7 @@ string toSolidityStr(smtutil::Expression const& _expr) return formatDatatypeAccessor(_expr, strArgs); // Infix operators with format replacements. - static map const infixOps{ + static std::map const infixOps{ {"and", "&&"}, {"or", "||"}, {"implies", "=>"}, @@ -170,7 +169,7 @@ string toSolidityStr(smtutil::Expression const& _expr) if (infixOps.count(op)) return formatInfixOp(infixOps.at(op), strArgs); - static set const arrayOps{"select", "store", "const_array"}; + static std::set const arrayOps{"select", "store", "const_array"}; if (arrayOps.count(op)) return formatArrayOp(_expr, strArgs); diff --git a/libsolidity/formal/Invariants.cpp b/libsolidity/formal/Invariants.cpp index 9177a4d4314f..017ab1e3aedb 100644 --- a/libsolidity/formal/Invariants.cpp +++ b/libsolidity/formal/Invariants.cpp @@ -25,7 +25,6 @@ #include -using namespace std; using boost::algorithm::starts_with; using namespace solidity; using namespace solidity::smtutil; @@ -34,19 +33,19 @@ using namespace solidity::frontend::smt; namespace solidity::frontend::smt { -map> collectInvariants( +std::map> collectInvariants( smtutil::Expression const& _proof, - set const& _predicates, + std::set const& _predicates, ModelCheckerInvariants const& _invariantsSetting ) { - set targets; + std::set targets; if (_invariantsSetting.has(InvariantType::Contract)) targets.insert("interface_"); if (_invariantsSetting.has(InvariantType::Reentrancy)) targets.insert("nondet_interface_"); - map> equalities; + std::map> equalities; // Collect equalities where one of the sides is a predicate we're interested in. util::BreadthFirstSearch{{&_proof}}.run([&](auto&& _expr, auto&& _addChild) { if (_expr->name == "=") @@ -63,7 +62,7 @@ map> collectInvariants( _addChild(&arg); }); - map> invariants; + std::map> invariants; for (auto pred: _predicates) { auto predName = pred->functor().name; @@ -74,7 +73,7 @@ map> collectInvariants( auto const& [predExpr, invExpr] = equalities.at(predName); - static set const ignore{"true", "false"}; + static std::set const ignore{"true", "false"}; auto r = substitute(invExpr, pred->expressionSubstitution(predExpr)); // No point in reporting true/false as invariants. if (!ignore.count(r.name)) diff --git a/libsolidity/formal/ModelChecker.cpp b/libsolidity/formal/ModelChecker.cpp index bc97c553497f..5632ff5c4ec6 100644 --- a/libsolidity/formal/ModelChecker.cpp +++ b/libsolidity/formal/ModelChecker.cpp @@ -31,7 +31,6 @@ #include #include -using namespace std; using namespace solidity; using namespace solidity::util; using namespace solidity::langutil; @@ -41,7 +40,7 @@ using namespace solidity::smtutil; ModelChecker::ModelChecker( ErrorReporter& _errorReporter, langutil::CharStreamProvider const& _charStreamProvider, - map const& _smtlib2Responses, + std::map const& _smtlib2Responses, ModelCheckerSettings _settings, ReadCallback::Callback const& _smtCallback ): @@ -54,19 +53,19 @@ ModelChecker::ModelChecker( } // TODO This should be removed for 0.9.0. -bool ModelChecker::isPragmaPresent(vector> const& _sources) +bool ModelChecker::isPragmaPresent(std::vector> const& _sources) { return ranges::any_of(_sources, [](auto _source) { return _source && _source->annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker); }); } -void ModelChecker::checkRequestedSourcesAndContracts(vector> const& _sources) +void ModelChecker::checkRequestedSourcesAndContracts(std::vector> const& _sources) { - map> exist; + std::map> exist; for (auto const& source: _sources) for (auto node: source->nodes()) - if (auto contract = dynamic_pointer_cast(node)) + if (auto contract = std::dynamic_pointer_cast(node)) exist[contract->sourceUnitName()].insert(contract->name()); // Requested sources @@ -100,7 +99,7 @@ void ModelChecker::analyze(SourceUnit const& _source) { PragmaDirective const* smtPragma = nullptr; for (auto node: _source.nodes()) - if (auto pragma = dynamic_pointer_cast(node)) + if (auto pragma = std::dynamic_pointer_cast(node)) if ( pragma->literals().size() >= 2 && pragma->literals().at(1) == "SMTChecker" @@ -125,7 +124,7 @@ void ModelChecker::analyze(SourceUnit const& _source) if (m_settings.engine.chc) m_chc.analyze(_source); - map, smt::EncodingContext::IdCompare> solvedTargets; + std::map, smt::EncodingContext::IdCompare> solvedTargets; for (auto const& [node, targets]: m_chc.safeTargets()) for (auto const& target: targets) @@ -147,7 +146,7 @@ void ModelChecker::analyze(SourceUnit const& _source) 5724_error, {}, "SMTChecker: " + - to_string(m_unsupportedErrorReporter.errors().size()) + + std::to_string(m_unsupportedErrorReporter.errors().size()) + " unsupported language feature(s)." " Enable the model checker option \"show unsupported\" to see all of them." ); @@ -156,7 +155,7 @@ void ModelChecker::analyze(SourceUnit const& _source) m_uniqueErrorReporter.clear(); } -vector ModelChecker::unhandledQueries() +std::vector ModelChecker::unhandledQueries() { return m_bmc.unhandledQueries() + m_chc.unhandledQueries(); } @@ -212,7 +211,7 @@ SMTSolverChoice ModelChecker::checkRequestedSolvers(SMTSolverChoice _enabled, Er SourceLocation(), "Solver z3 was selected for SMTChecker but it is not available." #ifdef HAVE_Z3_DLOPEN - " libz3.so." + to_string(Z3_MAJOR_VERSION) + "." + to_string(Z3_MINOR_VERSION) + " was not found." + " libz3.so." + std::to_string(Z3_MAJOR_VERSION) + "." + std::to_string(Z3_MINOR_VERSION) + " was not found." #endif ); } diff --git a/libsolidity/formal/ModelCheckerSettings.cpp b/libsolidity/formal/ModelCheckerSettings.cpp index d1e383d63f25..ed4d5ce204c0 100644 --- a/libsolidity/formal/ModelCheckerSettings.cpp +++ b/libsolidity/formal/ModelCheckerSettings.cpp @@ -21,18 +21,17 @@ #include #include -using namespace std; using namespace solidity; using namespace solidity::frontend; -map const ModelCheckerInvariants::validInvariants{ +std::map const ModelCheckerInvariants::validInvariants{ {"contract", InvariantType::Contract}, {"reentrancy", InvariantType::Reentrancy} }; -std::optional ModelCheckerInvariants::fromString(string const& _invs) +std::optional ModelCheckerInvariants::fromString(std::string const& _invs) { - set chosenInvs; + std::set chosenInvs; if (_invs == "default") { // The default is that no invariants are reported. @@ -41,7 +40,7 @@ std::optional ModelCheckerInvariants::fromString(string for (auto&& v: validInvariants | ranges::views::values) chosenInvs.insert(v); else - for (auto&& t: _invs | ranges::views::split(',') | ranges::to>()) + for (auto&& t: _invs | ranges::views::split(',') | ranges::to>()) { if (!validInvariants.count(t)) return {}; @@ -51,7 +50,7 @@ std::optional ModelCheckerInvariants::fromString(string return ModelCheckerInvariants{chosenInvs}; } -bool ModelCheckerInvariants::setFromString(string const& _inv) +bool ModelCheckerInvariants::setFromString(std::string const& _inv) { if (!validInvariants.count(_inv)) return false; @@ -60,7 +59,7 @@ bool ModelCheckerInvariants::setFromString(string const& _inv) } using TargetType = VerificationTargetType; -map const ModelCheckerTargets::targetStrings{ +std::map const ModelCheckerTargets::targetStrings{ {"constantCondition", TargetType::ConstantCondition}, {"underflow", TargetType::Underflow}, {"overflow", TargetType::Overflow}, @@ -71,7 +70,7 @@ map const ModelCheckerTargets::targetStrings{ {"outOfBounds", TargetType::OutOfBounds} }; -map const ModelCheckerTargets::targetTypeToString{ +std::map const ModelCheckerTargets::targetTypeToString{ {TargetType::ConstantCondition, "Constant condition"}, {TargetType::Underflow, "Underflow"}, {TargetType::Overflow, "Overflow"}, @@ -82,9 +81,9 @@ map const ModelCheckerTargets::targetTypeToString{ {TargetType::OutOfBounds, "Out of bounds access"} }; -std::optional ModelCheckerTargets::fromString(string const& _targets) +std::optional ModelCheckerTargets::fromString(std::string const& _targets) { - set chosenTargets; + std::set chosenTargets; if (_targets == "default" || _targets == "all") { bool all = _targets == "all"; @@ -96,7 +95,7 @@ std::optional ModelCheckerTargets::fromString(string const& } } else - for (auto&& t: _targets | ranges::views::split(',') | ranges::to>()) + for (auto&& t: _targets | ranges::views::split(',') | ranges::to>()) { if (!targetStrings.count(t)) return {}; @@ -106,7 +105,7 @@ std::optional ModelCheckerTargets::fromString(string const& return ModelCheckerTargets{chosenTargets}; } -bool ModelCheckerTargets::setFromString(string const& _target) +bool ModelCheckerTargets::setFromString(std::string const& _target) { if (!targetStrings.count(_target)) return false; @@ -114,15 +113,15 @@ bool ModelCheckerTargets::setFromString(string const& _target) return true; } -std::optional ModelCheckerContracts::fromString(string const& _contracts) +std::optional ModelCheckerContracts::fromString(std::string const& _contracts) { - map> chosen; + std::map> chosen; if (_contracts == "default") return ModelCheckerContracts::Default(); - for (auto&& sourceContract: _contracts | ranges::views::split(',') | ranges::to>()) + for (auto&& sourceContract: _contracts | ranges::views::split(',') | ranges::to>()) { - auto&& names = sourceContract | ranges::views::split(':') | ranges::to>(); + auto&& names = sourceContract | ranges::views::split(':') | ranges::to>(); if (names.size() != 2 || names.at(0).empty() || names.at(1).empty()) return {}; chosen[names.at(0)].insert(names.at(1)); @@ -131,7 +130,7 @@ std::optional ModelCheckerContracts::fromString(string co return ModelCheckerContracts{chosen}; } -std::optional ModelCheckerExtCalls::fromString(string const& _mode) +std::optional ModelCheckerExtCalls::fromString(std::string const& _mode) { if (_mode == "untrusted") return ModelCheckerExtCalls{Mode::UNTRUSTED}; diff --git a/libsolidity/formal/Predicate.cpp b/libsolidity/formal/Predicate.cpp index 7119a59e8ba8..2ab494fc4d28 100644 --- a/libsolidity/formal/Predicate.cpp +++ b/libsolidity/formal/Predicate.cpp @@ -31,27 +31,26 @@ #include #include -using namespace std; using boost::algorithm::starts_with; using namespace solidity; using namespace solidity::smtutil; using namespace solidity::frontend; using namespace solidity::frontend::smt; -map Predicate::m_predicates; +std::map Predicate::m_predicates; Predicate const* Predicate::create( SortPointer _sort, - string _name, + std::string _name, PredicateType _type, EncodingContext& _context, ASTNode const* _node, ContractDefinition const* _contractContext, - vector _scopeStack + std::vector _scopeStack ) { smt::SymbolicFunctionVariable predicate{_sort, std::move(_name), _context}; - string functorName = predicate.currentName(); + std::string functorName = predicate.currentName(); solAssert(!m_predicates.count(functorName), ""); return &m_predicates.emplace( std::piecewise_construct, @@ -65,7 +64,7 @@ Predicate::Predicate( PredicateType _type, ASTNode const* _node, ContractDefinition const* _contractContext, - vector _scopeStack + std::vector _scopeStack ): m_predicate(std::move(_predicate)), m_type(_type), @@ -75,7 +74,7 @@ Predicate::Predicate( { } -Predicate const* Predicate::predicate(string const& _name) +Predicate const* Predicate::predicate(std::string const& _name) { return &m_predicates.at(_name); } @@ -85,7 +84,7 @@ void Predicate::reset() m_predicates.clear(); } -smtutil::Expression Predicate::operator()(vector const& _args) const +smtutil::Expression Predicate::operator()(std::vector const& _args) const { return m_predicate(_args); } @@ -149,12 +148,12 @@ VariableDeclaration const* Predicate::programVariable() const return dynamic_cast(m_node); } -optional> Predicate::stateVariables() const +std::optional> Predicate::stateVariables() const { if (m_contractContext) return SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*m_contractContext); - return nullopt; + return std::nullopt; } bool Predicate::isSummary() const @@ -211,8 +210,8 @@ bool Predicate::isNondetInterface() const return m_type == PredicateType::NondetInterface; } -string Predicate::formatSummaryCall( - vector const& _args, +std::string Predicate::formatSummaryCall( + std::vector const& _args, langutil::CharStreamProvider const& _charStreamProvider, bool _appendTxVars ) const @@ -225,7 +224,7 @@ string Predicate::formatSummaryCall( if (auto funCall = programFunctionCall()) { if (funCall->location().hasText()) - return string(_charStreamProvider.charStream(*funCall->location().sourceName).text(funCall->location())); + return std::string(_charStreamProvider.charStream(*funCall->location().sourceName).text(funCall->location())); else return {}; } @@ -233,11 +232,11 @@ string Predicate::formatSummaryCall( /// The signature of a function summary predicate is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockChainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars). /// Here we are interested in preInputVars to format the function call. - string txModel; + std::string txModel; if (_appendTxVars) { - set txVars; + std::set txVars; if (isFunctionSummary()) { solAssert(programFunction(), ""); @@ -276,7 +275,7 @@ string Predicate::formatSummaryCall( return true; } - set txVars; + std::set txVars; } txVarsVisitor; if (auto fun = programFunction()) @@ -287,7 +286,7 @@ string Predicate::formatSummaryCall( // Here we are interested in txData from the summary predicate. auto txValues = readTxVars(_args.at(4)); - vector values; + std::vector values; for (auto const& _var: txVars) if (auto v = txValues.at(_var)) values.push_back(_var + ": " + *v); @@ -309,8 +308,8 @@ string Predicate::formatSummaryCall( solAssert(first >= _args.begin() && first <= _args.end(), ""); solAssert(last >= _args.begin() && last <= _args.end(), ""); auto inTypes = SMTEncoder::replaceUserTypes(FunctionType(*fun).parameterTypes()); - vector> functionArgsCex = formatExpressions(vector(first, last), inTypes); - vector functionArgs; + std::vector> functionArgsCex = formatExpressions(std::vector(first, last), inTypes); + std::vector functionArgs; auto const& params = fun->parameters(); solAssert(params.size() == functionArgsCex.size(), ""); @@ -320,12 +319,12 @@ string Predicate::formatSummaryCall( else functionArgs.emplace_back(params[i]->name()); - string fName = fun->isConstructor() ? "constructor" : + std::string fName = fun->isConstructor() ? "constructor" : fun->isFallback() ? "fallback" : fun->isReceive() ? "receive" : fun->name(); - string prefix; + std::string prefix; if (fun->isFree()) prefix = !fun->sourceUnitName().empty() ? (fun->sourceUnitName() + ":") : ""; else @@ -336,7 +335,7 @@ string Predicate::formatSummaryCall( return prefix + fName + "(" + boost::algorithm::join(functionArgs, ", ") + ")" + txModel; } -vector> Predicate::summaryStateValues(vector const& _args) const +std::vector> Predicate::summaryStateValues(std::vector const& _args) const { /// The signature of a function summary predicate is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars). /// The signature of the summary predicate of a contract without constructor is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockchainState, postBlockchainState, preStateVars, postStateVars). @@ -344,8 +343,8 @@ vector> Predicate::summaryStateValues(vector::const_iterator stateFirst; - vector::const_iterator stateLast; + std::vector::const_iterator stateFirst; + std::vector::const_iterator stateLast; if (auto const* function = programFunction()) { stateFirst = _args.begin() + 6 + static_cast(stateVars->size()) + static_cast(function->parameters().size()) + 1; @@ -364,13 +363,13 @@ vector> Predicate::summaryStateValues(vector= _args.begin() && stateFirst <= _args.end(), ""); solAssert(stateLast >= _args.begin() && stateLast <= _args.end(), ""); - vector stateArgs(stateFirst, stateLast); + std::vector stateArgs(stateFirst, stateLast); solAssert(stateArgs.size() == stateVars->size(), ""); auto stateTypes = util::applyMap(*stateVars, [&](auto const& _var) { return _var->type(); }); return formatExpressions(stateArgs, stateTypes); } -vector> Predicate::summaryPostInputValues(vector const& _args) const +std::vector> Predicate::summaryPostInputValues(std::vector const& _args) const { /// The signature of a function summary predicate is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars). /// Here we are interested in postInputVars. @@ -388,13 +387,13 @@ vector> Predicate::summaryPostInputValues(vector= _args.begin() && first <= _args.end(), ""); solAssert(last >= _args.begin() && last <= _args.end(), ""); - vector inValues(first, last); + std::vector inValues(first, last); solAssert(inValues.size() == inParams.size(), ""); auto inTypes = SMTEncoder::replaceUserTypes(FunctionType(*function).parameterTypes()); return formatExpressions(inValues, inTypes); } -vector> Predicate::summaryPostOutputValues(vector const& _args) const +std::vector> Predicate::summaryPostOutputValues(std::vector const& _args) const { /// The signature of a function summary predicate is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars). /// Here we are interested in outputVars. @@ -410,13 +409,13 @@ vector> Predicate::summaryPostOutputValues(vector= _args.begin() && first <= _args.end(), ""); - vector outValues(first, _args.end()); + std::vector outValues(first, _args.end()); solAssert(outValues.size() == function->returnParameters().size(), ""); auto outTypes = SMTEncoder::replaceUserTypes(FunctionType(*function).returnParameterTypes()); return formatExpressions(outValues, outTypes); } -pair>, vector> Predicate::localVariableValues(vector const& _args) const +std::pair>, std::vector> Predicate::localVariableValues(std::vector const& _args) const { /// The signature of a local block predicate is: /// block(error, this, abiFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars, localVars). @@ -426,7 +425,7 @@ pair>, vector> Predicate::lo auto const& localVars = SMTEncoder::localVariablesIncludingModifiers(*function, m_contractContext); auto first = _args.end() - static_cast(localVars.size()); - vector outValues(first, _args.end()); + std::vector outValues(first, _args.end()); auto mask = util::applyMap( localVars, @@ -442,10 +441,10 @@ pair>, vector> Predicate::lo return {formatExpressions(outValuesInScope, outTypes), localVarsInScope}; } -map Predicate::expressionSubstitution(smtutil::Expression const& _predExpr) const +std::map Predicate::expressionSubstitution(smtutil::Expression const& _predExpr) const { - map subst; - string predName = functor().name; + std::map subst; + std::string predName = functor().name; solAssert(contextContract(), ""); auto const& stateVars = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*contextContract()); @@ -486,16 +485,16 @@ map Predicate::expressionSubstitution(smtutil::Expression const& return subst; } -vector> Predicate::formatExpressions(vector const& _exprs, vector const& _types) const +std::vector> Predicate::formatExpressions(std::vector const& _exprs, std::vector const& _types) const { solAssert(_exprs.size() == _types.size(), ""); - vector> strExprs; + std::vector> strExprs; for (unsigned i = 0; i < _exprs.size(); ++i) strExprs.push_back(expressionToString(_exprs.at(i), _types.at(i))); return strExprs; } -optional Predicate::expressionToString(smtutil::Expression const& _expr, Type const* _type) const +std::optional Predicate::expressionToString(smtutil::Expression const& _expr, Type const* _type) const { if (smt::isNumber(*_type)) { @@ -514,10 +513,10 @@ optional Predicate::expressionToString(smtutil::Expression const& _expr, // For some reason the code below returns "0x" for "0". return util::toHex(toCompactBigEndian(bigint(_expr.name)), util::HexPrefix::Add, util::HexCase::Lower); } - catch (out_of_range const&) + catch (std::out_of_range const&) { } - catch (invalid_argument const&) + catch (std::invalid_argument const&) { } } @@ -550,11 +549,11 @@ optional Predicate::expressionToString(smtutil::Expression const& _expr, { length = stoul(_expr.arguments.at(1).name); } - catch(out_of_range const&) + catch(std::out_of_range const&) { return {}; } - catch(invalid_argument const&) + catch(std::invalid_argument const&) { return {}; } @@ -567,12 +566,12 @@ optional Predicate::expressionToString(smtutil::Expression const& _expr, return {}; try { - vector array(length); + std::vector array(length); if (!fillArray(_expr.arguments.at(0), array, arrayType)) return {}; return "[" + boost::algorithm::join(array, ", ") + "]"; } - catch (bad_alloc const&) + catch (std::bad_alloc const&) { // Solver gave a concrete array but length is too large. } @@ -585,10 +584,10 @@ optional Predicate::expressionToString(smtutil::Expression const& _expr, auto members = structType.structDefinition().members(); solAssert(tupleSort.components.size() == members.size(), ""); solAssert(_expr.arguments.size() == members.size(), ""); - vector elements; + std::vector elements; for (unsigned i = 0; i < members.size(); ++i) { - optional elementStr = expressionToString(_expr.arguments.at(i), members[i]->type()); + std::optional elementStr = expressionToString(_expr.arguments.at(i), members[i]->type()); elements.push_back(members[i]->name() + (elementStr.has_value() ? ": " + elementStr.value() : "")); } return "{" + boost::algorithm::join(elements, ", ") + "}"; @@ -597,13 +596,13 @@ optional Predicate::expressionToString(smtutil::Expression const& _expr, return {}; } -bool Predicate::fillArray(smtutil::Expression const& _expr, vector& _array, ArrayType const& _type) const +bool Predicate::fillArray(smtutil::Expression const& _expr, std::vector& _array, ArrayType const& _type) const { // Base case if (_expr.name == "const_array") { auto length = _array.size(); - optional elemStr = expressionToString(_expr.arguments.at(1), _type.baseType()); + std::optional elemStr = expressionToString(_expr.arguments.at(1), _type.baseType()); if (!elemStr) return false; _array.clear(); @@ -616,7 +615,7 @@ bool Predicate::fillArray(smtutil::Expression const& _expr, vector& _arr { if (!fillArray(_expr.arguments.at(0), _array, _type)) return false; - optional indexStr = expressionToString(_expr.arguments.at(1), TypeProvider::uint256()); + std::optional indexStr = expressionToString(_expr.arguments.at(1), TypeProvider::uint256()); if (!indexStr) return false; // Sometimes the solver assigns huge lengths that are not related, @@ -626,15 +625,15 @@ bool Predicate::fillArray(smtutil::Expression const& _expr, vector& _arr { index = stoul(*indexStr); } - catch (out_of_range const&) + catch (std::out_of_range const&) { return true; } - catch (invalid_argument const&) + catch (std::invalid_argument const&) { return true; } - optional elemStr = expressionToString(_expr.arguments.at(2), _type.baseType()); + std::optional elemStr = expressionToString(_expr.arguments.at(2), _type.baseType()); if (!elemStr) return false; if (index < _array.size()) @@ -652,9 +651,9 @@ bool Predicate::fillArray(smtutil::Expression const& _expr, vector& _arr solAssert(false, ""); } -map> Predicate::readTxVars(smtutil::Expression const& _tx) const +std::map> Predicate::readTxVars(smtutil::Expression const& _tx) const { - map const txVars{ + std::map const txVars{ {"block.basefee", TypeProvider::uint256()}, {"block.chainid", TypeProvider::uint256()}, {"block.coinbase", TypeProvider::address()}, @@ -670,7 +669,7 @@ map> Predicate::readTxVars(smtutil::Expression const& _ {"tx.gasprice", TypeProvider::uint256()}, {"tx.origin", TypeProvider::address()} }; - map> vars; + std::map> vars; for (auto&& [i, v]: txVars | ranges::views::enumerate) vars.emplace(v.first, expressionToString(_tx.arguments.at(i), v.second)); return vars; diff --git a/libsolidity/formal/PredicateInstance.cpp b/libsolidity/formal/PredicateInstance.cpp index 5e057efe3745..0bf352dd4777 100644 --- a/libsolidity/formal/PredicateInstance.cpp +++ b/libsolidity/formal/PredicateInstance.cpp @@ -21,7 +21,6 @@ #include #include -using namespace std; using namespace solidity::util; using namespace solidity::smtutil; @@ -30,14 +29,14 @@ namespace solidity::frontend::smt smtutil::Expression interfacePre(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context) { auto& state = _context.state(); - vector stateExprs{state.thisAddress(0), state.abi(0), state.crypto(0), state.state(0)}; + std::vector stateExprs{state.thisAddress(0), state.abi(0), state.crypto(0), state.state(0)}; return _pred(stateExprs + initialStateVariables(_contract, _context)); } smtutil::Expression interface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context) { auto const& state = _context.state(); - vector stateExprs{state.thisAddress(0), state.abi(0), state.crypto(0), state.state()}; + std::vector stateExprs{state.thisAddress(0), state.abi(0), state.crypto(0), state.state()}; return _pred(stateExprs + currentStateVariables(_contract, _context)); } @@ -49,12 +48,12 @@ smtutil::Expression nondetInterface( unsigned _postIdx) { auto const& state = _context.state(); - vector stateExprs{state.errorFlag().currentValue(), state.thisAddress(), state.abi(), state.crypto()}; + std::vector stateExprs{state.errorFlag().currentValue(), state.thisAddress(), state.abi(), state.crypto()}; return _pred( stateExprs + - vector{_context.state().state(_preIdx)} + + std::vector{_context.state().state(_preIdx)} + stateVariablesAtIndex(_preIdx, _contract, _context) + - vector{_context.state().state(_postIdx)} + + std::vector{_context.state().state(_postIdx)} + stateVariablesAtIndex(_postIdx, _contract, _context) ); } @@ -66,7 +65,7 @@ smtutil::Expression constructor(Predicate const& _pred, EncodingContext& _contex return _pred(currentFunctionVariablesForDefinition(*constructor, &contract, _context)); auto& state = _context.state(); - vector stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state(0), state.state()}; + std::vector stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state(0), state.state()}; return _pred(stateExprs + initialStateVariables(contract, _context) + currentStateVariables(contract, _context)); } @@ -77,9 +76,9 @@ smtutil::Expression constructorCall(Predicate const& _pred, EncodingContext& _co return _pred(currentFunctionVariablesForCall(*constructor, &contract, _context, _internal)); auto& state = _context.state(); - vector stateExprs{state.errorFlag().currentValue(), _internal ? state.thisAddress(0) : state.thisAddress(), state.abi(0), state.crypto(0), _internal ? state.tx(0) : state.tx(), state.state()}; + std::vector stateExprs{state.errorFlag().currentValue(), _internal ? state.thisAddress(0) : state.thisAddress(), state.abi(0), state.crypto(0), _internal ? state.tx(0) : state.tx(), state.state()}; state.newState(); - stateExprs += vector{state.state()}; + stateExprs += std::vector{state.state()}; stateExprs += currentStateVariables(contract, _context); stateExprs += newStateVariables(contract, _context); return _pred(stateExprs); @@ -117,12 +116,12 @@ smtutil::Expression functionBlock( /// Helpers -vector initialStateVariables(ContractDefinition const& _contract, EncodingContext& _context) +std::vector initialStateVariables(ContractDefinition const& _contract, EncodingContext& _context) { return stateVariablesAtIndex(0, _contract, _context); } -vector stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract, EncodingContext& _context) +std::vector stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract, EncodingContext& _context) { return applyMap( SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract), @@ -130,7 +129,7 @@ vector stateVariablesAtIndex(unsigned _index, ContractDefin ); } -vector currentStateVariables(ContractDefinition const& _contract, EncodingContext& _context) +std::vector currentStateVariables(ContractDefinition const& _contract, EncodingContext& _context) { return applyMap( SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract), @@ -138,7 +137,7 @@ vector currentStateVariables(ContractDefinition const& _con ); } -vector newStateVariables(ContractDefinition const& _contract, EncodingContext& _context) +std::vector newStateVariables(ContractDefinition const& _contract, EncodingContext& _context) { return applyMap( SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract), @@ -146,24 +145,24 @@ vector newStateVariables(ContractDefinition const& _contrac ); } -vector currentFunctionVariablesForDefinition( +std::vector currentFunctionVariablesForDefinition( FunctionDefinition const& _function, ContractDefinition const* _contract, EncodingContext& _context ) { auto& state = _context.state(); - vector exprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state(0)}; - exprs += _contract ? initialStateVariables(*_contract, _context) : vector{}; + std::vector exprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state(0)}; + exprs += _contract ? initialStateVariables(*_contract, _context) : std::vector{}; exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->valueAtIndex(0); }); - exprs += vector{state.state()}; - exprs += _contract ? currentStateVariables(*_contract, _context) : vector{}; + exprs += std::vector{state.state()}; + exprs += _contract ? currentStateVariables(*_contract, _context) : std::vector{}; exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); }); exprs += applyMap(_function.returnParameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); }); return exprs; } -vector currentFunctionVariablesForCall( +std::vector currentFunctionVariablesForCall( FunctionDefinition const& _function, ContractDefinition const* _contract, EncodingContext& _context, @@ -171,20 +170,20 @@ vector currentFunctionVariablesForCall( ) { auto& state = _context.state(); - vector exprs{state.errorFlag().currentValue(), _internal ? state.thisAddress(0) : state.thisAddress(), state.abi(0), state.crypto(0), _internal ? state.tx(0) : state.tx(), state.state()}; - exprs += _contract ? currentStateVariables(*_contract, _context) : vector{}; + std::vector exprs{state.errorFlag().currentValue(), _internal ? state.thisAddress(0) : state.thisAddress(), state.abi(0), state.crypto(0), _internal ? state.tx(0) : state.tx(), state.state()}; + exprs += _contract ? currentStateVariables(*_contract, _context) : std::vector{}; exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); }); state.newState(); - exprs += vector{state.state()}; - exprs += _contract ? newStateVariables(*_contract, _context) : vector{}; + exprs += std::vector{state.state()}; + exprs += _contract ? newStateVariables(*_contract, _context) : std::vector{}; exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->increaseIndex(); }); exprs += applyMap(_function.returnParameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); }); return exprs; } -vector currentBlockVariables(FunctionDefinition const& _function, ContractDefinition const* _contract, EncodingContext& _context) +std::vector currentBlockVariables(FunctionDefinition const& _function, ContractDefinition const* _contract, EncodingContext& _context) { return currentFunctionVariablesForDefinition(_function, _contract, _context) + applyMap( diff --git a/libsolidity/formal/PredicateSort.cpp b/libsolidity/formal/PredicateSort.cpp index dc134766d806..2e95a29a531d 100644 --- a/libsolidity/formal/PredicateSort.cpp +++ b/libsolidity/formal/PredicateSort.cpp @@ -21,7 +21,6 @@ #include #include -using namespace std; using namespace solidity::util; using namespace solidity::smtutil; @@ -30,8 +29,8 @@ namespace solidity::frontend::smt SortPointer interfaceSort(ContractDefinition const& _contract, SymbolicState& _state) { - return make_shared( - vector{_state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.stateSort()} + stateSorts(_contract), + return std::make_shared( + std::vector{_state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.stateSort()} + stateSorts(_contract), SortProvider::boolSort ); } @@ -39,9 +38,9 @@ SortPointer interfaceSort(ContractDefinition const& _contract, SymbolicState& _s SortPointer nondetInterfaceSort(ContractDefinition const& _contract, SymbolicState& _state) { auto varSorts = stateSorts(_contract); - vector stateSort{_state.stateSort()}; - return make_shared( - vector{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort()} + + std::vector stateSort{_state.stateSort()}; + return std::make_shared( + std::vector{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort()} + stateSort + varSorts + stateSort + @@ -56,9 +55,9 @@ SortPointer constructorSort(ContractDefinition const& _contract, SymbolicState& return functionSort(*constructor, &_contract, _state); auto varSorts = stateSorts(_contract); - vector stateSort{_state.stateSort()}; - return make_shared( - vector{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort(), _state.stateSort()} + varSorts + varSorts, + std::vector stateSort{_state.stateSort()}; + return std::make_shared( + std::vector{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort(), _state.stateSort()} + varSorts + varSorts, SortProvider::boolSort ); } @@ -66,14 +65,14 @@ SortPointer constructorSort(ContractDefinition const& _contract, SymbolicState& SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition const* _contract, SymbolicState& _state) { auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); }; - auto varSorts = _contract ? stateSorts(*_contract) : vector{}; + auto varSorts = _contract ? stateSorts(*_contract) : std::vector{}; auto inputSorts = applyMap(_function.parameters(), smtSort); auto outputSorts = applyMap(_function.returnParameters(), smtSort); - return make_shared( - vector{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort()} + + return std::make_shared( + std::vector{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort()} + varSorts + inputSorts + - vector{_state.stateSort()} + + std::vector{_state.stateSort()} + varSorts + inputSorts + outputSorts, @@ -83,11 +82,11 @@ SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition SortPointer functionBodySort(FunctionDefinition const& _function, ContractDefinition const* _contract, SymbolicState& _state) { - auto fSort = dynamic_pointer_cast(functionSort(_function, _contract, _state)); + auto fSort = std::dynamic_pointer_cast(functionSort(_function, _contract, _state)); solAssert(fSort, ""); auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); }; - return make_shared( + return std::make_shared( fSort->domain + applyMap(SMTEncoder::localVariablesIncludingModifiers(_function, _contract), smtSort), SortProvider::boolSort ); @@ -95,15 +94,15 @@ SortPointer functionBodySort(FunctionDefinition const& _function, ContractDefini SortPointer arity0FunctionSort() { - return make_shared( - vector(), + return std::make_shared( + std::vector(), SortProvider::boolSort ); } /// Helpers -vector stateSorts(ContractDefinition const& _contract) +std::vector stateSorts(ContractDefinition const& _contract) { return applyMap( SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract), diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index a328a7781a22..37f8d5771fe5 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -40,11 +40,11 @@ #include #include -using namespace std; using namespace solidity; using namespace solidity::util; using namespace solidity::langutil; using namespace solidity::frontend; +using namespace std::string_literals; SMTEncoder::SMTEncoder( smt::EncodingContext& _context, @@ -72,8 +72,8 @@ bool SMTEncoder::visit(ContractDefinition const& _contract) for (auto const& node: _contract.subNodes()) if ( - !dynamic_pointer_cast(node) && - !dynamic_pointer_cast(node) + !std::dynamic_pointer_cast(node) && + !std::dynamic_pointer_cast(node) ) node->accept(*this); @@ -198,7 +198,7 @@ void SMTEncoder::inlineModifierInvocation(ModifierInvocation const* _invocation, solAssert(_invocation, ""); _invocation->accept(*this); - vector args; + std::vector args; if (auto const* arguments = _invocation->arguments()) { auto const& modifierParams = _definition->parameters(); @@ -314,8 +314,8 @@ bool SMTEncoder::visit(InlineAssembly const& _inlineAsm) this->operator()(_inlineAsm.operations()); } - map const& externalReferences; - set assignedVars; + std::map const& externalReferences; + std::set assignedVars; using yul::ASTWalker::operator(); void operator()(yul::Assignment const& _assignment) @@ -425,14 +425,14 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple) if (_tuple.isInlineArray()) { // Add constraints for the length and values as it is known. - auto symbArray = dynamic_pointer_cast(m_context.expression(_tuple)); + auto symbArray = std::dynamic_pointer_cast(m_context.expression(_tuple)); solAssert(symbArray, ""); addArrayLiteralAssertions(*symbArray, applyMap(_tuple.components(), [&](auto const& c) { return expr(*c); })); } else { - auto values = applyMap(_tuple.components(), [this](auto const& component) -> optional { + auto values = applyMap(_tuple.components(), [this](auto const& component) -> std::optional { if (component) { if (!m_context.knownExpression(*component)) @@ -816,19 +816,19 @@ void SMTEncoder::visitABIFunction(FunctionCall const& _funCall) defineExpr(_funCall, smt::zeroValue(TypeProvider::bytesMemory())); return; } - vector symbArgs; + std::vector symbArgs; for (unsigned i = 0; i < argsActualLength; ++i) if (args.at(i)) symbArgs.emplace_back(expr(*args.at(i), inTypes.at(i))); - optional arg; + std::optional arg; if (inTypes.size() == 1) arg = expr(*args.at(0), inTypes.at(0)); else { auto inputSort = dynamic_cast(*symbFunction.sort).domain; arg = smtutil::Expression::tuple_constructor( - smtutil::Expression(make_shared(inputSort), ""), + smtutil::Expression(std::make_shared(inputSort), ""), symbArgs ); } @@ -838,7 +838,7 @@ void SMTEncoder::visitABIFunction(FunctionCall const& _funCall) defineExpr(_funCall, out); else { - auto symbTuple = dynamic_pointer_cast(m_context.expression(_funCall)); + auto symbTuple = std::dynamic_pointer_cast(m_context.expression(_funCall)); solAssert(symbTuple, ""); solAssert(symbTuple->components().size() == outTypes.size(), ""); solAssert(out.sort->kind == smtutil::Kind::Tuple, ""); @@ -854,7 +854,7 @@ void SMTEncoder::visitCryptoFunction(FunctionCall const& _funCall) auto const& funType = dynamic_cast(*_funCall.expression().annotation().type); auto kind = funType.kind(); auto arg0 = expr(*_funCall.arguments().at(0)); - optional result; + std::optional result; if (kind == FunctionType::Kind::KECCAK256) result = smtutil::Expression::select(state().cryptoFunction("keccak256"), arg0); else if (kind == FunctionType::Kind::SHA256) @@ -870,7 +870,7 @@ void SMTEncoder::visitCryptoFunction(FunctionCall const& _funCall) auto arg3 = expr(*_funCall.arguments().at(3)); auto inputSort = dynamic_cast(*e.sort).domain; auto ecrecoverInput = smtutil::Expression::tuple_constructor( - smtutil::Expression(make_shared(inputSort), ""), + smtutil::Expression(std::make_shared(inputSort), ""), {arg0, arg1, arg2, arg3} ); result = smtutil::Expression::select(e, ecrecoverInput); @@ -883,7 +883,7 @@ void SMTEncoder::visitCryptoFunction(FunctionCall const& _funCall) void SMTEncoder::visitGasLeft(FunctionCall const& _funCall) { - string gasLeft = "gasleft"; + std::string gasLeft = "gasleft"; // We increase the variable index since gasleft changes // inside a tx. defineGlobalVariable(gasLeft, _funCall, true); @@ -930,7 +930,7 @@ void SMTEncoder::visitObjectCreation(FunctionCall const& _funCall) smtutil::Expression arraySize = expr(*args.front()); setSymbolicUnknownValue(arraySize, TypeProvider::uint256(), m_context); - auto symbArray = dynamic_pointer_cast(m_context.expression(_funCall)); + auto symbArray = std::dynamic_pointer_cast(m_context.expression(_funCall)); solAssert(symbArray, ""); smt::setSymbolicZeroValue(*symbArray, m_context); auto zeroElements = symbArray->elements(); @@ -1004,9 +1004,9 @@ bool isReturnedFromStructGetter(Type const* _type) return true; } -vector structGetterReturnedMembers(StructType const& _structType) +std::vector structGetterReturnedMembers(StructType const& _structType) { - vector returnedMembers; + std::vector returnedMembers; for (auto const& member: _structType.nativeMembers(nullptr)) if (isReturnedFromStructGetter(member.type)) returnedMembers.push_back(member.name); @@ -1023,7 +1023,7 @@ void SMTEncoder::visitPublicGetter(FunctionCall const& _funCall) auto paramExpectedTypes = replaceUserTypes(FunctionType(*var).parameterTypes()); auto actualArguments = _funCall.arguments(); solAssert(actualArguments.size() == paramExpectedTypes.size(), ""); - deque symbArguments; + std::deque symbArguments; for (unsigned i = 0; i < paramExpectedTypes.size(); ++i) symbArguments.push_back(expr(*actualArguments[i], paramExpectedTypes[i])); @@ -1063,11 +1063,11 @@ void SMTEncoder::visitPublicGetter(FunctionCall const& _funCall) case Type::Category::Struct: { solAssert(symbArguments.empty(), ""); - smt::SymbolicStructVariable structVar(dynamic_cast(type), "struct_temp_" + to_string(_funCall.id()), m_context); + smt::SymbolicStructVariable structVar(dynamic_cast(type), "struct_temp_" + std::to_string(_funCall.id()), m_context); m_context.addAssertion(structVar.currentValue() == currentExpr); auto returnedMembers = structGetterReturnedMembers(dynamic_cast(*structVar.type())); solAssert(!returnedMembers.empty(), ""); - auto returnedValues = applyMap(returnedMembers, [&](string const& memberName) -> optional { return structVar.member(memberName); }); + auto returnedValues = applyMap(returnedMembers, [&](std::string const& memberName) -> std::optional { return structVar.member(memberName); }); defineExpr(_funCall, returnedValues); return; } @@ -1118,7 +1118,7 @@ void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall) if (arrayType && arrayType->isByteArrayOrString() && smt::isFixedBytes(*funCallType)) { - auto array = dynamic_pointer_cast(m_context.expression(*argument)); + auto array = std::dynamic_pointer_cast(m_context.expression(*argument)); bytesToFixedBytesAssertions(*array, _funCall); return; } @@ -1129,8 +1129,8 @@ void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall) unsigned castSize = funCallType->storageBytes(); bool castIsSigned = smt::isNumber(*funCallType) && smt::isSigned(funCallType); bool argIsSigned = smt::isNumber(*argType) && smt::isSigned(argType); - optional symbMin; - optional symbMax; + std::optional symbMin; + std::optional symbMax; if (smt::isNumber(*funCallType)) { symbMin = smt::minValue(funCallType); @@ -1285,7 +1285,7 @@ void SMTEncoder::endVisit(Literal const& _literal) createExpr(_literal); // Add constraints for the length and values as it is known. - auto symbArray = dynamic_pointer_cast(m_context.expression(_literal)); + auto symbArray = std::dynamic_pointer_cast(m_context.expression(_literal)); solAssert(symbArray, ""); addArrayLiteralAssertions( @@ -1299,7 +1299,7 @@ void SMTEncoder::endVisit(Literal const& _literal) void SMTEncoder::addArrayLiteralAssertions( smt::SymbolicArrayVariable& _symArray, - vector const& _elementValues + std::vector const& _elementValues ) { m_context.addAssertion(_symArray.length() == _elementValues.size()); @@ -1314,7 +1314,7 @@ void SMTEncoder::bytesToFixedBytesAssertions( { auto const& fixed = dynamic_cast(*_fixedBytes.annotation().type); auto intType = TypeProvider::uint256(); - string suffix = to_string(_fixedBytes.id()) + "_" + to_string(m_context.newUniqueId()); + std::string suffix = std::to_string(_fixedBytes.id()) + "_" + std::to_string(m_context.newUniqueId()); smt::SymbolicIntVariable k(intType, intType, "k_" + suffix, m_context); m_context.addAssertion(k.currentValue() == 0); size_t n = fixed.numBytes(); @@ -1333,7 +1333,7 @@ void SMTEncoder::endVisit(Return const& _return) auto returnParams = m_callStack.back().first->returnParameters(); if (returnParams.size() > 1) { - auto const& symbTuple = dynamic_pointer_cast(m_context.expression(*_return.expression())); + auto const& symbTuple = std::dynamic_pointer_cast(m_context.expression(*_return.expression())); solAssert(symbTuple, ""); solAssert(symbTuple->components().size() == returnParams.size(), ""); @@ -1410,7 +1410,7 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess) defineExpr(_memberAccess, contract.interfaceId()); } else - // NOTE: supporting name, creationCode, runtimeCode would be easy enough, but the bytes/string they return are not + // NOTE: supporting name, creationCode, runtimeCode would be easy enough, but the bytes/std::string they return are not // at all usable in the SMT checker currently m_unsupportedErrors.warning( 7507_error, @@ -1428,7 +1428,7 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess) else if (smt::isNonRecursiveStruct(*exprType)) { memberExpr->accept(*this); - auto const& symbStruct = dynamic_pointer_cast(m_context.expression(*memberExpr)); + auto const& symbStruct = std::dynamic_pointer_cast(m_context.expression(*memberExpr)); defineExpr(_memberAccess, symbStruct->member(_memberAccess.memberName())); return false; } @@ -1471,7 +1471,7 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess) memberExpr->accept(*this); if (_memberAccess.memberName() == "length") { - auto symbArray = dynamic_pointer_cast(m_context.expression(*memberExpr)); + auto symbArray = std::dynamic_pointer_cast(m_context.expression(*memberExpr)); solAssert(symbArray, ""); defineExpr(_memberAccess, symbArray->length()); m_uninterpretedTerms.insert(&_memberAccess); @@ -1554,7 +1554,7 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess) return; } - shared_ptr array; + std::shared_ptr array; if (auto const* id = dynamic_cast(&_indexAccess.baseExpression())) { auto varDecl = identifierToVariable(*id); @@ -1570,7 +1570,7 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess) array = m_context.expression(_indexAccess.baseExpression()); } - auto arrayVar = dynamic_pointer_cast(array); + auto arrayVar = std::dynamic_pointer_cast(array); solAssert(arrayVar, ""); Type const* baseType = _indexAccess.baseExpression().annotation().type; @@ -1611,10 +1611,10 @@ void SMTEncoder::indexOrMemberAssignment(Expression const& _expr, smtutil::Expre Type const* baseType = base.annotation().type; auto indexExpr = expr(*indexAccess->indexExpression(), keyType(baseType)); - auto symbArray = dynamic_pointer_cast(m_context.expression(base)); + auto symbArray = std::dynamic_pointer_cast(m_context.expression(base)); solAssert(symbArray, ""); toStore = smtutil::Expression::tuple_constructor( - smtutil::Expression(make_shared(smt::smtSort(*baseType)), baseType->toString(true)), + smtutil::Expression(std::make_shared(smt::smtSort(*baseType)), baseType->toString(true)), {smtutil::Expression::store(symbArray->elements(), indexExpr, toStore), symbArray->length()} ); defineExpr(*indexAccess, smtutil::Expression::select( @@ -1650,7 +1650,7 @@ void SMTEncoder::indexOrMemberAssignment(Expression const& _expr, smtutil::Expre break; } - auto symbStruct = dynamic_pointer_cast(m_context.expression(base)); + auto symbStruct = std::dynamic_pointer_cast(m_context.expression(base)); solAssert(symbStruct, ""); symbStruct->assignMember(memberAccess->memberName(), toStore); toStore = symbStruct->currentValue(); @@ -1688,7 +1688,7 @@ void SMTEncoder::arrayPush(FunctionCall const& _funCall) { auto memberAccess = dynamic_cast(&_funCall.expression()); solAssert(memberAccess, ""); - auto symbArray = dynamic_pointer_cast(m_context.expression(memberAccess->expression())); + auto symbArray = std::dynamic_pointer_cast(m_context.expression(memberAccess->expression())); solAssert(symbArray, ""); auto oldLength = symbArray->length(); m_context.addAssertion(oldLength >= 0); @@ -1722,7 +1722,7 @@ void SMTEncoder::arrayPop(FunctionCall const& _funCall) { auto memberAccess = dynamic_cast(cleanExpression(_funCall.expression())); solAssert(memberAccess, ""); - auto symbArray = dynamic_pointer_cast(m_context.expression(memberAccess->expression())); + auto symbArray = std::dynamic_pointer_cast(m_context.expression(memberAccess->expression())); solAssert(symbArray, ""); makeArrayPopVerificationTarget(_funCall); @@ -1742,7 +1742,7 @@ void SMTEncoder::arrayPop(FunctionCall const& _funCall) assignment(memberAccess->expression(), symbArray->currentValue()); } -void SMTEncoder::defineGlobalVariable(string const& _name, Expression const& _expr, bool _increaseIndex) +void SMTEncoder::defineGlobalVariable(std::string const& _name, Expression const& _expr, bool _increaseIndex) { if (!m_context.knownGlobalSymbol(_name)) { @@ -1807,7 +1807,7 @@ void SMTEncoder::arithmeticOperation(BinaryOperation const& _op) } } -pair SMTEncoder::arithmeticOperation( +std::pair SMTEncoder::arithmeticOperation( Token _op, smtutil::Expression const& _left, smtutil::Expression const& _right, @@ -1815,7 +1815,7 @@ pair SMTEncoder::arithmeticOperation( Expression const& _operation ) { - static set validOperators{ + static std::set validOperators{ Token::Add, Token::Sub, Token::Mul, @@ -1862,7 +1862,7 @@ pair SMTEncoder::arithmeticOperation( // - RHS is -1 // the result is then -(type.min), which wraps back to type.min smtutil::Expression maxLeft = _left == smt::minValue(*intType); - smtutil::Expression minusOneRight = _right == numeric_limits::max(); + smtutil::Expression minusOneRight = _right == std::numeric_limits::max(); smtutil::Expression wrap = smtutil::Expression::ite(maxLeft && minusOneRight, smt::minValue(*intType), valueUnbounded); return {wrap, valueUnbounded}; } @@ -1871,7 +1871,7 @@ pair SMTEncoder::arithmeticOperation( auto symbMax = smt::maxValue(*intType); smtutil::Expression intValueRange = (0 - symbMin) + symbMax + 1; - string suffix = to_string(_operation.id()) + "_" + to_string(m_context.newUniqueId()); + std::string suffix = std::to_string(_operation.id()) + "_" + std::to_string(m_context.newUniqueId()); smt::SymbolicIntVariable k(intType, intType, "k_" + suffix, m_context); smt::SymbolicIntVariable m(intType, intType, "m_" + suffix, m_context); @@ -1905,7 +1905,7 @@ smtutil::Expression SMTEncoder::bitwiseOperation( Type const* _commonType ) { - static set validOperators{ + static std::set validOperators{ Token::BitAnd, Token::BitOr, Token::BitXor, @@ -1921,7 +1921,7 @@ smtutil::Expression SMTEncoder::bitwiseOperation( auto bvLeft = smtutil::Expression::int2bv(_left, bvSize); auto bvRight = smtutil::Expression::int2bv(_right, bvSize); - optional result; + std::optional result; switch (_op) { case Token::BitAnd: @@ -1962,10 +1962,10 @@ void SMTEncoder::compareOperation(BinaryOperation const& _op) smtutil::Expression left(expr(_op.leftExpression(), commonType)); smtutil::Expression right(expr(_op.rightExpression(), commonType)); Token op = _op.getOperator(); - shared_ptr value; + std::shared_ptr value; if (smt::isNumber(*commonType)) { - value = make_shared( + value = std::make_shared( op == Token::Equal ? (left == right) : op == Token::NotEqual ? (left != right) : op == Token::LessThan ? (left < right) : @@ -1977,7 +1977,7 @@ void SMTEncoder::compareOperation(BinaryOperation const& _op) else // Bool { solUnimplementedAssert(smt::isBool(*commonType), "Operation not yet supported"); - value = make_shared( + value = std::make_shared( op == Token::Equal ? (left == right) : /*op == Token::NotEqual*/ (left != right) ); @@ -2039,7 +2039,7 @@ void SMTEncoder::bitwiseNotOperation(UnaryOperation const& _op) defineExpr(_op, smtutil::Expression::bv2int(~bvOperand, isSigned)); } -pair SMTEncoder::divModWithSlacks( +std::pair SMTEncoder::divModWithSlacks( smtutil::Expression _left, smtutil::Expression _right, IntegerType const& _type @@ -2049,7 +2049,7 @@ pair SMTEncoder::divModWithSlacks( return {_left / _right, _left % _right}; IntegerType const* intType = &_type; - string suffix = "div_mod_" + to_string(m_context.newUniqueId()); + std::string suffix = "div_mod_" + std::to_string(m_context.newUniqueId()); smt::SymbolicIntVariable dSymb(intType, intType, "d_" + suffix, m_context); smt::SymbolicIntVariable rSymb(intType, intType, "r_" + suffix, m_context); auto d = dSymb.currentValue(); @@ -2115,7 +2115,7 @@ void SMTEncoder::assignment( { auto memberAccess = dynamic_cast(&funCall->expression()); solAssert(memberAccess, ""); - auto symbArray = dynamic_pointer_cast(m_context.expression(memberAccess->expression())); + auto symbArray = std::dynamic_pointer_cast(m_context.expression(memberAccess->expression())); solAssert(symbArray, ""); auto oldLength = symbArray->length(); @@ -2190,14 +2190,14 @@ void SMTEncoder::tupleAssignment(Expression const& _left, Expression const& _rig smtutil::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment) { - static map const compoundToArithmetic{ + static std::map const compoundToArithmetic{ {Token::AssignAdd, Token::Add}, {Token::AssignSub, Token::Sub}, {Token::AssignMul, Token::Mul}, {Token::AssignDiv, Token::Div}, {Token::AssignMod, Token::Mod} }; - static map const compoundToBitwise{ + static std::map const compoundToBitwise{ {Token::AssignBitAnd, Token::BitAnd}, {Token::AssignBitOr, Token::BitOr}, {Token::AssignBitXor, Token::BitXor}, @@ -2228,12 +2228,12 @@ smtutil::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment return values.first; } -void SMTEncoder::expressionToTupleAssignment(vector> const& _variables, Expression const& _rhs) +void SMTEncoder::expressionToTupleAssignment(std::vector> const& _variables, Expression const& _rhs) { auto symbolicVar = m_context.expression(_rhs); if (_variables.size() > 1) { - auto symbTuple = dynamic_pointer_cast(symbolicVar); + auto symbTuple = std::dynamic_pointer_cast(symbolicVar); solAssert(symbTuple, ""); auto const& symbComponents = symbTuple->components(); solAssert(symbComponents.size() == _variables.size(), ""); @@ -2282,7 +2282,7 @@ void SMTEncoder::assignment(smt::SymbolicVariable& _symVar, smtutil::Expression m_context.addAssertion(_symVar.increaseIndex() == _value); } -pair SMTEncoder::visitBranch( +std::pair SMTEncoder::visitBranch( ASTNode const* _statement, smtutil::Expression _condition ) @@ -2290,7 +2290,7 @@ pair SMTEncoder::visitBranch( return visitBranch(_statement, &_condition); } -pair SMTEncoder::visitBranch( +std::pair SMTEncoder::visitBranch( ASTNode const* _statement, smtutil::Expression const* _condition ) @@ -2307,7 +2307,7 @@ pair SMTEncoder::visitBranch( return {indicesAfterBranch, pathConditionOnExit}; } -void SMTEncoder::initializeFunctionCallParameters(CallableDeclaration const& _function, vector const& _callArgs) +void SMTEncoder::initializeFunctionCallParameters(CallableDeclaration const& _function, std::vector const& _callArgs) { auto const& funParams = _function.parameters(); solAssert(funParams.size() == _callArgs.size(), ""); @@ -2319,7 +2319,7 @@ void SMTEncoder::initializeFunctionCallParameters(CallableDeclaration const& _fu m_arrayAssignmentHappened = true; } - vector localVars; + std::vector localVars; if (auto const* fun = dynamic_cast(&_function)) localVars = localVariablesIncludingModifiers(*fun, m_currentContract); else @@ -2560,14 +2560,14 @@ void SMTEncoder::defineExpr(Expression const& _e, smtutil::Expression _value) )); } -void SMTEncoder::defineExpr(Expression const& _e, vector> const& _values) +void SMTEncoder::defineExpr(Expression const& _e, std::vector> const& _values) { if (_values.size() == 1 && _values.front()) { defineExpr(_e, *_values.front()); return; } - auto const& symbTuple = dynamic_pointer_cast(m_context.expression(_e)); + auto const& symbTuple = std::dynamic_pointer_cast(m_context.expression(_e)); solAssert(symbTuple, ""); symbTuple->increaseIndex(); auto const& symbComponents = symbTuple->components(); @@ -2606,7 +2606,7 @@ smtutil::Expression SMTEncoder::currentPathConditions() return m_pathConditions.back(); } -SecondarySourceLocation SMTEncoder::callStackMessage(vector const& _callStack) +SecondarySourceLocation SMTEncoder::callStackMessage(std::vector const& _callStack) { SecondarySourceLocation callStackLocation; solAssert(!_callStack.empty(), ""); @@ -2617,7 +2617,7 @@ SecondarySourceLocation SMTEncoder::callStackMessage(vector cons return callStackLocation; } -pair SMTEncoder::popCallStack() +std::pair SMTEncoder::popCallStack() { solAssert(!m_callStack.empty(), ""); auto lastCalled = m_callStack.back(); @@ -2738,7 +2738,7 @@ TypePointers SMTEncoder::replaceUserTypes(TypePointers const& _types) }); } -pair SMTEncoder::functionCallExpression(FunctionCall const& _funCall) +std::pair SMTEncoder::functionCallExpression(FunctionCall const& _funCall) { Expression const* callExpr = &_funCall.expression(); auto const* callOptions = dynamic_cast(callExpr); @@ -2775,9 +2775,9 @@ Expression const* SMTEncoder::cleanExpression(Expression const& _expr) return expr; } -set SMTEncoder::touchedVariables(ASTNode const& _node) +std::set SMTEncoder::touchedVariables(ASTNode const& _node) { - vector callStack; + std::vector callStack; for (auto const& call: m_callStack) callStack.push_back(call.first); return m_variableUsage.touchedVariables(_node, callStack); @@ -2861,9 +2861,9 @@ bool SMTEncoder::isExternalCallToThis(Expression const* _expr) { ; } -string SMTEncoder::extraComment() +std::string SMTEncoder::extraComment() { - string extra; + std::string extra; if (m_arrayAssignmentHappened) extra += "\nNote that array aliasing is not supported," @@ -2921,28 +2921,28 @@ FunctionDefinition const* SMTEncoder::functionCallToDefinition( return {}; } -vector SMTEncoder::stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract) +std::vector SMTEncoder::stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract) { return fold( _contract.annotation().linearizedBaseContracts, - vector{}, + std::vector{}, [](auto&& _acc, auto _contract) { return _acc + _contract->stateVariables(); } ); } -vector SMTEncoder::stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function) +std::vector SMTEncoder::stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function) { if (auto contract = dynamic_cast(_function.scope())) return stateVariablesIncludingInheritedAndPrivate(*contract); return {}; } -vector SMTEncoder::localVariablesIncludingModifiers(FunctionDefinition const& _function, ContractDefinition const* _contract) +std::vector SMTEncoder::localVariablesIncludingModifiers(FunctionDefinition const& _function, ContractDefinition const* _contract) { return _function.localVariables() + tryCatchVariables(_function) + modifiersVariables(_function, _contract); } -vector SMTEncoder::tryCatchVariables(FunctionDefinition const& _function) +std::vector SMTEncoder::tryCatchVariables(FunctionDefinition const& _function) { struct TryCatchVarsVisitor : public ASTConstVisitor { @@ -2958,23 +2958,23 @@ vector SMTEncoder::tryCatchVariables(FunctionDefinit return true; } - vector vars; + std::vector vars; } tryCatchVarsVisitor; _function.accept(tryCatchVarsVisitor); return tryCatchVarsVisitor.vars; } -vector SMTEncoder::modifiersVariables(FunctionDefinition const& _function, ContractDefinition const* _contract) +std::vector SMTEncoder::modifiersVariables(FunctionDefinition const& _function, ContractDefinition const* _contract) { struct BlockVars: ASTConstVisitor { BlockVars(Block const& _block) { _block.accept(*this); } void endVisit(VariableDeclaration const& _var) { vars.push_back(&_var); } - vector vars; + std::vector vars; }; - vector vars; - set visited; + std::vector vars; + std::set visited; for (auto invok: _function.modifiers()) { if (!invok) @@ -3007,12 +3007,12 @@ ModifierDefinition const* SMTEncoder::resolveModifierInvocation(ModifierInvocati return modifier; } -set const& SMTEncoder::contractFunctions(ContractDefinition const& _contract) +std::set const& SMTEncoder::contractFunctions(ContractDefinition const& _contract) { if (!m_contractFunctions.count(&_contract)) { auto const& functions = _contract.definedFunctions(); - set resolvedFunctions(begin(functions), end(functions)); + std::set resolvedFunctions(begin(functions), end(functions)); for (auto const* base: _contract.annotation().linearizedBaseContracts) { if (base == &_contract) @@ -3042,7 +3042,7 @@ set const& SMTEncoder::contract return m_contractFunctions.at(&_contract); } -set const& SMTEncoder::contractFunctionsWithoutVirtual(ContractDefinition const& _contract) +std::set const& SMTEncoder::contractFunctionsWithoutVirtual(ContractDefinition const& _contract) { if (!m_contractFunctionsWithoutVirtual.count(&_contract)) { @@ -3057,9 +3057,9 @@ set const& SMTEncoder::contract return m_contractFunctionsWithoutVirtual.at(&_contract); } -map>> SMTEncoder::baseArguments(ContractDefinition const& _contract) +std::map>> SMTEncoder::baseArguments(ContractDefinition const& _contract) { - map>> baseArgs; + std::map>> baseArgs; for (auto contract: _contract.annotation().linearizedBaseContracts) { @@ -3104,7 +3104,7 @@ RationalNumberType const* SMTEncoder::isConstant(Expression const& _expr) return nullptr; } -set> SMTEncoder::collectABICalls(ASTNode const* _node) +std::set> SMTEncoder::collectABICalls(ASTNode const* _node) { struct ABIFunctions: public ASTConstVisitor { @@ -3126,15 +3126,15 @@ set> SMTEncoder::collectABICal } } - set> abiCalls; + std::set> abiCalls; }; return ABIFunctions(_node).abiCalls; } -set SMTEncoder::sourceDependencies(SourceUnit const& _source) +std::set SMTEncoder::sourceDependencies(SourceUnit const& _source) { - set sources; + std::set sources; sources.insert(&_source); for (auto const& source: _source.referencedSourceUnits(true)) sources.insert(source); @@ -3150,24 +3150,24 @@ void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall, Contrac auto const& returnParams = funDef->returnParameters(); for (auto param: returnParams) createVariable(*param); - auto returnValues = applyMap(returnParams, [this](auto const& param) -> optional { + auto returnValues = applyMap(returnParams, [this](auto const& param) -> std::optional { solAssert(param && m_context.knownVariable(*param), ""); return currentValue(*param); }); defineExpr(_funCall, returnValues); } -vector SMTEncoder::symbolicArguments(FunctionCall const& _funCall, ContractDefinition const* _contextContract) +std::vector SMTEncoder::symbolicArguments(FunctionCall const& _funCall, ContractDefinition const* _contextContract) { auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), _contextContract); solAssert(funDef, ""); - vector args; + std::vector args; Expression const* calledExpr = &_funCall.expression(); auto funType = dynamic_cast(calledExpr->annotation().type); solAssert(funType, ""); - vector> arguments = _funCall.sortedArguments(); + std::vector> arguments = _funCall.sortedArguments(); auto functionParams = funDef->parameters(); unsigned firstParam = 0; if (funType->hasBoundFirstArgument()) @@ -3204,7 +3204,7 @@ smtutil::Expression SMTEncoder::constantExpr(Expression const& _expr, VariableDe solAssert(false, ""); } -void SMTEncoder::collectFreeFunctions(set const& _sources) +void SMTEncoder::collectFreeFunctions(std::set const& _sources) { for (auto source: _sources) for (auto node: source->nodes()) @@ -3220,7 +3220,7 @@ void SMTEncoder::collectFreeFunctions(set const& _sources) +void SMTEncoder::createFreeConstants(std::set const& _sources) { for (auto source: _sources) for (auto node: source->nodes()) diff --git a/libsolidity/formal/SSAVariable.cpp b/libsolidity/formal/SSAVariable.cpp index bb599c35a883..482388cedbd7 100644 --- a/libsolidity/formal/SSAVariable.cpp +++ b/libsolidity/formal/SSAVariable.cpp @@ -18,7 +18,6 @@ #include -using namespace std; using namespace solidity::frontend; using namespace solidity::frontend::smt; diff --git a/libsolidity/formal/SymbolicState.cpp b/libsolidity/formal/SymbolicState.cpp index 68bd9b64621f..3859e99c6243 100644 --- a/libsolidity/formal/SymbolicState.cpp +++ b/libsolidity/formal/SymbolicState.cpp @@ -26,42 +26,41 @@ #include -using namespace std; using namespace solidity; using namespace solidity::util; using namespace solidity::smtutil; using namespace solidity::frontend::smt; BlockchainVariable::BlockchainVariable( - string _name, - map _members, + std::string _name, + std::map _members, EncodingContext& _context ): m_name(std::move(_name)), m_members(std::move(_members)), m_context(_context) { - vector members; - vector sorts; + std::vector members; + std::vector sorts; for (auto const& [component, sort]: m_members) { members.emplace_back(component); sorts.emplace_back(sort); m_componentIndices[component] = static_cast(members.size() - 1); } - m_tuple = make_unique( - make_shared(m_name + "_type", members, sorts), + m_tuple = std::make_unique( + std::make_shared(m_name + "_type", members, sorts), m_name, m_context ); } -smtutil::Expression BlockchainVariable::member(string const& _member) const +smtutil::Expression BlockchainVariable::member(std::string const& _member) const { return m_tuple->component(m_componentIndices.at(_member)); } -smtutil::Expression BlockchainVariable::assignMember(string const& _member, smtutil::Expression const& _value) +smtutil::Expression BlockchainVariable::assignMember(std::string const& _member, smtutil::Expression const& _value) { smtutil::Expression newTuple = smt::assignMember(m_tuple->currentValue(), {{_member, _value}}); m_context.addAssertion(m_tuple->increaseIndex() == newTuple); @@ -104,9 +103,9 @@ smtutil::Expression SymbolicState::blockhash(smtutil::Expression _blockNumber) c void SymbolicState::newBalances() { - auto tupleSort = dynamic_pointer_cast(stateSort()); + auto tupleSort = std::dynamic_pointer_cast(stateSort()); auto balanceSort = tupleSort->components.at(tupleSort->memberToIndex.at("balances")); - SymbolicVariable newBalances(balanceSort, "fresh_balances_" + to_string(m_context.newUniqueId()), m_context); + SymbolicVariable newBalances(balanceSort, "fresh_balances_" + std::to_string(m_context.newUniqueId()), m_context); m_state->assignMember("balances", newBalances.currentValue()); } @@ -158,7 +157,7 @@ void SymbolicState::newStorage() { auto newStorageVar = SymbolicTupleVariable( m_state->member("storage").sort, - "havoc_storage_" + to_string(m_context.newUniqueId()), + "havoc_storage_" + std::to_string(m_context.newUniqueId()), m_context ); m_state->assignMember("storage", newStorageVar.currentValue()); @@ -170,7 +169,7 @@ void SymbolicState::writeStateVars(ContractDefinition const& _contract, smtutil: if (stateVars.empty()) return; - map values; + std::map values; for (auto var: stateVars) values.emplace(stateVarStorageKey(*var, _contract), m_context.variable(*var)->currentValue()); @@ -207,7 +206,7 @@ void SymbolicState::addBalance(smtutil::Expression _address, smtutil::Expression m_state->assignMember("balances", newBalances); } -smtutil::Expression SymbolicState::txMember(string const& _member) const +smtutil::Expression SymbolicState::txMember(std::string const& _member) const { return m_tx.member(_member); } @@ -268,8 +267,8 @@ void SymbolicState::prepareForSourceUnit(SourceUnit const& _source, bool _storag { auto allSources = _source.referencedSourceUnits(true); allSources.insert(&_source); - set> abiCalls; - set> contracts; + std::set> abiCalls; + std::set> contracts; for (auto const& source: allSources) { abiCalls += SMTEncoder::collectABICalls(source); @@ -283,34 +282,34 @@ void SymbolicState::prepareForSourceUnit(SourceUnit const& _source, bool _storag /// Private helpers. -string SymbolicState::contractSuffix(ContractDefinition const& _contract) const +std::string SymbolicState::contractSuffix(ContractDefinition const& _contract) const { - return "_" + _contract.name() + "_" + to_string(_contract.id()); + return "_" + _contract.name() + "_" + std::to_string(_contract.id()); } -string SymbolicState::contractStorageKey(ContractDefinition const& _contract) const +std::string SymbolicState::contractStorageKey(ContractDefinition const& _contract) const { return "storage" + contractSuffix(_contract); } -string SymbolicState::stateVarStorageKey(VariableDeclaration const& _var, ContractDefinition const& _contract) const +std::string SymbolicState::stateVarStorageKey(VariableDeclaration const& _var, ContractDefinition const& _contract) const { - return _var.name() + "_" + to_string(_var.id()) + contractSuffix(_contract); + return _var.name() + "_" + std::to_string(_var.id()) + contractSuffix(_contract); } -void SymbolicState::buildState(set> const& _contracts, bool _allStorages) +void SymbolicState::buildState(std::set> const& _contracts, bool _allStorages) { - map stateMembers{ - {"balances", make_shared(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort)} + std::map stateMembers{ + {"balances", std::make_shared(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort)} }; if (_allStorages) { - vector memberNames; - vector memberSorts; + std::vector memberNames; + std::vector memberSorts; for (auto contract: _contracts) { - string suffix = contractSuffix(*contract); + std::string suffix = contractSuffix(*contract); // z3 doesn't like empty tuples, so if the contract has 0 // state vars we can't put it there. @@ -319,16 +318,16 @@ void SymbolicState::buildState(setname() + "_" + to_string(var->id()) + suffix; + return var->name() + "_" + std::to_string(var->id()) + suffix; }); auto sorts = applyMap(stateVars, [](auto var) { return smtSortAbstractFunction(*var->type()); }); - string name = "storage" + suffix; - auto storageTuple = make_shared( + std::string name = "storage" + suffix; + auto storageTuple = std::make_shared( name + "_type", names, sorts ); - auto storageSort = make_shared( + auto storageSort = std::make_shared( smtSort(*TypeProvider::address()), storageTuple ); @@ -339,26 +338,26 @@ void SymbolicState::buildState(set(smtSort(*TypeProvider::address()), smtutil::SortProvider::boolSort) + std::make_shared(smtSort(*TypeProvider::address()), smtutil::SortProvider::boolSort) ); stateMembers.emplace( "storage", - make_shared( + std::make_shared( "storage_type", memberNames, memberSorts ) ); } - m_state = make_unique( + m_state = std::make_unique( "state", std::move(stateMembers), m_context ); } -void SymbolicState::buildABIFunctions(set> const& _abiFunctions) +void SymbolicState::buildABIFunctions(std::set> const& _abiFunctions) { - map functions; + std::map functions; for (auto const* funCall: _abiFunctions) { @@ -375,8 +374,8 @@ void SymbolicState::buildABIFunctions(set inTypes; - vector outTypes; + std::vector inTypes; + std::vector outTypes; if (t->kind() == FunctionType::Kind::ABIDecode) { /// abi.decode : (bytes, tuple_of_types(return_types)) -> (return_types) @@ -415,7 +414,7 @@ void SymbolicState::buildABIFunctions(set bytes /// abi.encodeWithSignature : (string, one_or_more_types) -> bytes inTypes.emplace_back(paramTypes.front()); - inTypes += argTypes(vector>(args.begin() + 1, args.end())); + inTypes += argTypes(std::vector>(args.begin() + 1, args.end())); } else { @@ -455,25 +454,25 @@ void SymbolicState::buildABIFunctions(set shared_ptr { + auto typesToSort = [](auto const& _types, std::string const& _name) -> std::shared_ptr { if (_types.size() == 1) return smtSortAbstractFunction(*_types.front()); - vector inNames; - vector sorts; + std::vector inNames; + std::vector sorts; for (unsigned i = 0; i < _types.size(); ++i) { - inNames.emplace_back(_name + "_input_" + to_string(i)); + inNames.emplace_back(_name + "_input_" + std::to_string(i)); sorts.emplace_back(smtSortAbstractFunction(*_types.at(i))); } - return make_shared( + return std::make_shared( _name + "_input", inNames, sorts ); }; - auto functionSort = make_shared( + auto functionSort = std::make_shared( typesToSort(inTypes, name), typesToSort(outTypes, name) ); @@ -481,13 +480,13 @@ void SymbolicState::buildABIFunctions(set("abi", std::move(functions), m_context); + m_abi = std::make_unique("abi", std::move(functions), m_context); } smtutil::Expression SymbolicState::abiFunction(frontend::FunctionCall const* _funCall) { solAssert(m_abi, ""); - return m_abi->member(get<0>(m_abiMembers.at(_funCall))); + return m_abi->member(std::get<0>(m_abiMembers.at(_funCall))); } SymbolicState::SymbolicABIFunction const& SymbolicState::abiFunctionTypes(FunctionCall const* _funCall) const diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index ccabebcc3bfc..45b872b3d0d9 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -26,7 +26,6 @@ #include #include -using namespace std; using namespace solidity::util; using namespace solidity::smtutil; @@ -52,7 +51,7 @@ SortPointer smtSort(frontend::Type const& _type) { auto fType = dynamic_cast(&_type); solAssert(fType, ""); - vector parameterSorts = smtSort(fType->parameterTypes()); + std::vector parameterSorts = smtSort(fType->parameterTypes()); auto returnTypes = fType->returnParameterTypes(); SortPointer returnSort; // TODO change this when we support tuples. @@ -64,22 +63,22 @@ SortPointer smtSort(frontend::Type const& _type) returnSort = SortProvider::uintSort; else returnSort = smtSort(*returnTypes.front()); - return make_shared(parameterSorts, returnSort); + return std::make_shared(parameterSorts, returnSort); } case Kind::Array: { - shared_ptr array; + std::shared_ptr array; if (isMapping(_type)) { auto mapType = dynamic_cast(&_type); solAssert(mapType, ""); - array = make_shared(smtSortAbstractFunction(*mapType->keyType()), smtSortAbstractFunction(*mapType->valueType())); + array = std::make_shared(smtSortAbstractFunction(*mapType->keyType()), smtSortAbstractFunction(*mapType->valueType())); } else if (isStringLiteral(_type)) { auto stringLitType = dynamic_cast(&_type); solAssert(stringLitType, ""); - array = make_shared(SortProvider::uintSort, SortProvider::uintSort); + array = std::make_shared(SortProvider::uintSort, SortProvider::uintSort); } else { @@ -92,10 +91,10 @@ SortPointer smtSort(frontend::Type const& _type) solAssert(false, ""); solAssert(arrayType, ""); - array = make_shared(SortProvider::uintSort, smtSortAbstractFunction(*arrayType->baseType())); + array = std::make_shared(SortProvider::uintSort, smtSortAbstractFunction(*arrayType->baseType())); } - string tupleName; + std::string tupleName; auto sliceArrayType = dynamic_cast(&_type); ArrayType const* arrayType = sliceArrayType ? &sliceArrayType->arrayType() : dynamic_cast(&_type); if ( @@ -109,7 +108,7 @@ SortPointer smtSort(frontend::Type const& _type) // Solidity allows implicit conversion also when assigning arrays. // So if the base type potentially has a size, that size cannot go // in the tuple's name. - if (auto tupleSort = dynamic_pointer_cast(array->range)) + if (auto tupleSort = std::dynamic_pointer_cast(array->range)) tupleName = tupleSort->name; else if ( baseType->category() == frontend::Type::Category::Integer || @@ -128,23 +127,23 @@ SortPointer smtSort(frontend::Type const& _type) tupleName += "_tuple"; - return make_shared( + return std::make_shared( tupleName, - vector{tupleName + "_accessor_array", tupleName + "_accessor_length"}, - vector{array, SortProvider::uintSort} + std::vector{tupleName + "_accessor_array", tupleName + "_accessor_length"}, + std::vector{array, SortProvider::uintSort} ); } case Kind::Tuple: { - vector members; + std::vector members; auto const& tupleName = _type.toString(true); - vector sorts; + std::vector sorts; if (auto const* tupleType = dynamic_cast(&_type)) { auto const& components = tupleType->components(); for (unsigned i = 0; i < components.size(); ++i) - members.emplace_back(tupleName + "_accessor_" + to_string(i)); + members.emplace_back(tupleName + "_accessor_" + std::to_string(i)); sorts = smtSortAbstractFunction(tupleType->components()); } else if (auto const* structType = dynamic_cast(&_type)) @@ -161,7 +160,7 @@ SortPointer smtSort(frontend::Type const& _type) else solAssert(false, ""); - return make_shared(tupleName, members, sorts); + return std::make_shared(tupleName, members, sorts); } default: // Abstract case. @@ -169,9 +168,9 @@ SortPointer smtSort(frontend::Type const& _type) } } -vector smtSort(vector const& _types) +std::vector smtSort(std::vector const& _types) { - vector sorts; + std::vector sorts; for (auto const& type: _types) sorts.push_back(smtSort(*type)); return sorts; @@ -184,9 +183,9 @@ SortPointer smtSortAbstractFunction(frontend::Type const& _type) return smtSort(_type); } -vector smtSortAbstractFunction(vector const& _types) +std::vector smtSortAbstractFunction(std::vector const& _types) { - vector sorts; + std::vector sorts; for (auto const& type: _types) if (type) sorts.push_back(smtSortAbstractFunction(*type)); @@ -233,14 +232,14 @@ bool isSupportedTypeDeclaration(frontend::Type const& _type) isFunction(_type); } -pair> newSymbolicVariable( +std::pair> newSymbolicVariable( frontend::Type const& _type, std::string const& _uniqueName, EncodingContext& _context ) { bool abstract = false; - shared_ptr var; + std::shared_ptr var; frontend::Type const* type = &_type; if (auto userType = dynamic_cast(type)) @@ -249,10 +248,10 @@ pair> newSymbolicVariable( if (!isSupportedTypeDeclaration(_type)) { abstract = true; - var = make_shared(frontend::TypeProvider::uint256(), type, _uniqueName, _context); + var = std::make_shared(frontend::TypeProvider::uint256(), type, _uniqueName, _context); } else if (isBool(_type)) - var = make_shared(type, _uniqueName, _context); + var = std::make_shared(type, _uniqueName, _context); else if (isFunction(_type)) { auto const& fType = dynamic_cast(type); @@ -271,45 +270,45 @@ pair> newSymbolicVariable( ) { abstract = true; - var = make_shared(TypeProvider::uint256(), type, _uniqueName, _context); + var = std::make_shared(TypeProvider::uint256(), type, _uniqueName, _context); } else - var = make_shared(type, _uniqueName, _context); + var = std::make_shared(type, _uniqueName, _context); } else if (isInteger(_type)) - var = make_shared(type, type, _uniqueName, _context); + var = std::make_shared(type, type, _uniqueName, _context); else if (isFixedPoint(_type)) - var = make_shared(type, type, _uniqueName, _context); + var = std::make_shared(type, type, _uniqueName, _context); else if (isFixedBytes(_type)) { auto fixedBytesType = dynamic_cast(type); solAssert(fixedBytesType, ""); - var = make_shared(type, fixedBytesType->numBytes(), _uniqueName, _context); + var = std::make_shared(type, fixedBytesType->numBytes(), _uniqueName, _context); } else if (isAddress(_type) || isContract(_type)) - var = make_shared(_uniqueName, _context); + var = std::make_shared(_uniqueName, _context); else if (isEnum(_type)) - var = make_shared(type, _uniqueName, _context); + var = std::make_shared(type, _uniqueName, _context); else if (isRational(_type)) { auto rational = dynamic_cast(&_type); solAssert(rational, ""); if (rational->isFractional()) - var = make_shared(frontend::TypeProvider::uint256(), type, _uniqueName, _context); + var = std::make_shared(frontend::TypeProvider::uint256(), type, _uniqueName, _context); else - var = make_shared(type, type, _uniqueName, _context); + var = std::make_shared(type, type, _uniqueName, _context); } else if (isMapping(_type) || isArray(_type)) - var = make_shared(type, type, _uniqueName, _context); + var = std::make_shared(type, type, _uniqueName, _context); else if (isTuple(_type)) - var = make_shared(type, _uniqueName, _context); + var = std::make_shared(type, _uniqueName, _context); else if (isStringLiteral(_type)) { auto stringType = TypeProvider::stringMemory(); - var = make_shared(stringType, type, _uniqueName, _context); + var = std::make_shared(stringType, type, _uniqueName, _context); } else if (isNonRecursiveStruct(_type)) - var = make_shared(type, _uniqueName, _context); + var = std::make_shared(type, _uniqueName, _context); else solAssert(false, ""); return make_pair(abstract, var); @@ -482,9 +481,9 @@ smtutil::Expression zeroValue(frontend::Type const* _type) return smtutil::Expression(false); if (isArray(*_type) || isMapping(*_type)) { - auto tupleSort = dynamic_pointer_cast(smtSort(*_type)); + auto tupleSort = std::dynamic_pointer_cast(smtSort(*_type)); solAssert(tupleSort, ""); - auto sortSort = make_shared(tupleSort->components.front()); + auto sortSort = std::make_shared(tupleSort->components.front()); std::optional zeroArray; auto length = bigint(0); @@ -502,16 +501,16 @@ smtutil::Expression zeroValue(frontend::Type const* _type) solAssert(zeroArray, ""); return smtutil::Expression::tuple_constructor( smtutil::Expression(std::make_shared(tupleSort), tupleSort->name), - vector{*zeroArray, length} + std::vector{*zeroArray, length} ); } if (isNonRecursiveStruct(*_type)) { auto const* structType = dynamic_cast(_type); - auto structSort = dynamic_pointer_cast(smtSort(*_type)); + auto structSort = std::dynamic_pointer_cast(smtSort(*_type)); return smtutil::Expression::tuple_constructor( - smtutil::Expression(make_shared(structSort), structSort->name), + smtutil::Expression(std::make_shared(structSort), structSort->name), applyMap( structType->structDefinition().members(), [](auto var) { return zeroValue(var->type()); } @@ -550,7 +549,7 @@ bool isSigned(frontend::Type const* _type) return isSigned; } -pair typeBvSizeAndSignedness(frontend::Type const* _type) +std::pair typeBvSizeAndSignedness(frontend::Type const* _type) { if (auto userType = dynamic_cast(_type)) return typeBvSizeAndSignedness(&userType->underlyingType()); @@ -596,7 +595,7 @@ smtutil::Expression symbolicUnknownConstraints(smtutil::Expression _expr, fronte return smtutil::Expression(true); } -optional symbolicTypeConversion(frontend::Type const* _from, frontend::Type const* _to) +std::optional symbolicTypeConversion(frontend::Type const* _from, frontend::Type const* _to) { if (auto userType = dynamic_cast(_to)) return symbolicTypeConversion(_from, &userType->underlyingType()); @@ -618,7 +617,7 @@ optional symbolicTypeConversion(frontend::Type const* _from return std::nullopt; } -smtutil::Expression member(smtutil::Expression const& _tuple, string const& _member) +smtutil::Expression member(smtutil::Expression const& _tuple, std::string const& _member) { TupleSort const& _sort = dynamic_cast(*_tuple.sort); return smtutil::Expression::tuple_get( @@ -627,16 +626,16 @@ smtutil::Expression member(smtutil::Expression const& _tuple, string const& _mem ); } -smtutil::Expression assignMember(smtutil::Expression const _tuple, map const& _values) +smtutil::Expression assignMember(smtutil::Expression const _tuple, std::map const& _values) { TupleSort const& _sort = dynamic_cast(*_tuple.sort); - vector args; + std::vector args; for (auto const& m: _sort.members) if (auto* value = util::valueOrNullptr(_values, m)) args.emplace_back(*value); else args.emplace_back(member(_tuple, m)); - auto sortExpr = smtutil::Expression(make_shared(_tuple.sort), _tuple.name); + auto sortExpr = smtutil::Expression(std::make_shared(_tuple.sort), _tuple.name); return smtutil::Expression::tuple_constructor(sortExpr, args); } diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp index 799ac4adb426..6d6dbee65da5 100644 --- a/libsolidity/formal/SymbolicVariables.cpp +++ b/libsolidity/formal/SymbolicVariables.cpp @@ -23,7 +23,6 @@ #include -using namespace std; using namespace solidity; using namespace solidity::util; using namespace solidity::smtutil; @@ -33,14 +32,14 @@ using namespace solidity::frontend::smt; SymbolicVariable::SymbolicVariable( frontend::Type const* _type, frontend::Type const* _originalType, - string _uniqueName, + std::string _uniqueName, EncodingContext& _context ): m_type(_type), m_originalType(_originalType), m_uniqueName(std::move(_uniqueName)), m_context(_context), - m_ssa(make_unique()) + m_ssa(std::make_unique()) { solAssert(m_type, ""); m_sort = smtSort(*m_type); @@ -49,13 +48,13 @@ SymbolicVariable::SymbolicVariable( SymbolicVariable::SymbolicVariable( SortPointer _sort, - string _uniqueName, + std::string _uniqueName, EncodingContext& _context ): m_sort(std::move(_sort)), m_uniqueName(std::move(_uniqueName)), m_context(_context), - m_ssa(make_unique()) + m_ssa(std::make_unique()) { solAssert(m_sort, ""); } @@ -65,7 +64,7 @@ smtutil::Expression SymbolicVariable::currentValue(frontend::Type const*) const return valueAtIndex(m_ssa->index()); } -string SymbolicVariable::currentName() const +std::string SymbolicVariable::currentName() const { return uniqueSymbol(m_ssa->index()); } @@ -75,14 +74,14 @@ smtutil::Expression SymbolicVariable::valueAtIndex(unsigned _index) const return m_context.newVariable(uniqueSymbol(_index), m_sort); } -string SymbolicVariable::nameAtIndex(unsigned _index) const +std::string SymbolicVariable::nameAtIndex(unsigned _index) const { return uniqueSymbol(_index); } -string SymbolicVariable::uniqueSymbol(unsigned _index) const +std::string SymbolicVariable::uniqueSymbol(unsigned _index) const { - return m_uniqueName + "_" + to_string(_index); + return m_uniqueName + "_" + std::to_string(_index); } smtutil::Expression SymbolicVariable::resetIndex() @@ -105,7 +104,7 @@ smtutil::Expression SymbolicVariable::increaseIndex() SymbolicBoolVariable::SymbolicBoolVariable( frontend::Type const* _type, - string _uniqueName, + std::string _uniqueName, EncodingContext& _context ): SymbolicVariable(_type, _type, std::move(_uniqueName), _context) @@ -116,7 +115,7 @@ SymbolicBoolVariable::SymbolicBoolVariable( SymbolicIntVariable::SymbolicIntVariable( frontend::Type const* _type, frontend::Type const* _originalType, - string _uniqueName, + std::string _uniqueName, EncodingContext& _context ): SymbolicVariable(_type, _originalType, std::move(_uniqueName), _context) @@ -125,7 +124,7 @@ SymbolicIntVariable::SymbolicIntVariable( } SymbolicAddressVariable::SymbolicAddressVariable( - string _uniqueName, + std::string _uniqueName, EncodingContext& _context ): SymbolicIntVariable(TypeProvider::uint(160), TypeProvider::uint(160), std::move(_uniqueName), _context) @@ -135,7 +134,7 @@ SymbolicAddressVariable::SymbolicAddressVariable( SymbolicFixedBytesVariable::SymbolicFixedBytesVariable( frontend::Type const* _originalType, unsigned _numBytes, - string _uniqueName, + std::string _uniqueName, EncodingContext& _context ): SymbolicIntVariable(TypeProvider::uint(_numBytes * 8), _originalType, std::move(_uniqueName), _context) @@ -144,7 +143,7 @@ SymbolicFixedBytesVariable::SymbolicFixedBytesVariable( SymbolicFunctionVariable::SymbolicFunctionVariable( frontend::Type const* _type, - string _uniqueName, + std::string _uniqueName, EncodingContext& _context ): SymbolicVariable(_type, _type, std::move(_uniqueName), _context), @@ -155,7 +154,7 @@ SymbolicFunctionVariable::SymbolicFunctionVariable( SymbolicFunctionVariable::SymbolicFunctionVariable( SortPointer _sort, - string _uniqueName, + std::string _uniqueName, EncodingContext& _context ): SymbolicVariable(std::move(_sort), std::move(_uniqueName), _context), @@ -204,7 +203,7 @@ smtutil::Expression SymbolicFunctionVariable::increaseIndex() return m_abstract.currentValue(); } -smtutil::Expression SymbolicFunctionVariable::operator()(vector _arguments) const +smtutil::Expression SymbolicFunctionVariable::operator()(std::vector _arguments) const { return m_declaration(_arguments); } @@ -216,7 +215,7 @@ void SymbolicFunctionVariable::resetDeclaration() SymbolicEnumVariable::SymbolicEnumVariable( frontend::Type const* _type, - string _uniqueName, + std::string _uniqueName, EncodingContext& _context ): SymbolicVariable(_type, _type, std::move(_uniqueName), _context) @@ -226,7 +225,7 @@ SymbolicEnumVariable::SymbolicEnumVariable( SymbolicTupleVariable::SymbolicTupleVariable( frontend::Type const* _type, - string _uniqueName, + std::string _uniqueName, EncodingContext& _context ): SymbolicVariable(_type, _type, std::move(_uniqueName), _context) @@ -236,7 +235,7 @@ SymbolicTupleVariable::SymbolicTupleVariable( SymbolicTupleVariable::SymbolicTupleVariable( SortPointer _sort, - string _uniqueName, + std::string _uniqueName, EncodingContext& _context ): SymbolicVariable(std::move(_sort), std::move(_uniqueName), _context) @@ -249,22 +248,22 @@ smtutil::Expression SymbolicTupleVariable::currentValue(frontend::Type const* _t if (!_targetType || sort() == smtSort(*_targetType)) return SymbolicVariable::currentValue(); - auto thisTuple = dynamic_pointer_cast(sort()); - auto otherTuple = dynamic_pointer_cast(smtSort(*_targetType)); + auto thisTuple = std::dynamic_pointer_cast(sort()); + auto otherTuple = std::dynamic_pointer_cast(smtSort(*_targetType)); solAssert(thisTuple && otherTuple, ""); solAssert(thisTuple->components.size() == otherTuple->components.size(), ""); - vector args; + std::vector args; for (size_t i = 0; i < thisTuple->components.size(); ++i) args.emplace_back(component(i, type(), _targetType)); return smtutil::Expression::tuple_constructor( - smtutil::Expression(make_shared(smtSort(*_targetType)), ""), + smtutil::Expression(std::make_shared(smtSort(*_targetType)), ""), args ); } -vector const& SymbolicTupleVariable::components() const +std::vector const& SymbolicTupleVariable::components() const { - auto tupleSort = dynamic_pointer_cast(m_sort); + auto tupleSort = std::dynamic_pointer_cast(m_sort); solAssert(tupleSort, ""); return tupleSort->components; } @@ -275,7 +274,7 @@ smtutil::Expression SymbolicTupleVariable::component( frontend::Type const* _toType ) const { - optional conversion = symbolicTypeConversion(_fromType, _toType); + std::optional conversion = symbolicTypeConversion(_fromType, _toType); if (conversion) return *conversion; @@ -285,7 +284,7 @@ smtutil::Expression SymbolicTupleVariable::component( SymbolicArrayVariable::SymbolicArrayVariable( frontend::Type const* _type, frontend::Type const* _originalType, - string _uniqueName, + std::string _uniqueName, EncodingContext& _context ): SymbolicVariable(_type, _originalType, std::move(_uniqueName), _context), @@ -300,7 +299,7 @@ SymbolicArrayVariable::SymbolicArrayVariable( SymbolicArrayVariable::SymbolicArrayVariable( SortPointer _sort, - string _uniqueName, + std::string _uniqueName, EncodingContext& _context ): SymbolicVariable(std::move(_sort), std::move(_uniqueName), _context), @@ -319,7 +318,7 @@ SymbolicArrayVariable::SymbolicArrayVariable( smtutil::Expression SymbolicArrayVariable::currentValue(frontend::Type const* _targetType) const { - optional conversion = symbolicTypeConversion(m_originalType, _targetType); + std::optional conversion = symbolicTypeConversion(m_originalType, _targetType); if (conversion) return *conversion; @@ -343,7 +342,7 @@ smtutil::Expression SymbolicArrayVariable::length() const SymbolicStructVariable::SymbolicStructVariable( frontend::Type const* _type, - string _uniqueName, + std::string _uniqueName, EncodingContext& _context ): SymbolicVariable(_type, _type, std::move(_uniqueName), _context) @@ -359,12 +358,12 @@ SymbolicStructVariable::SymbolicStructVariable( } } -smtutil::Expression SymbolicStructVariable::member(string const& _member) const +smtutil::Expression SymbolicStructVariable::member(std::string const& _member) const { return smtutil::Expression::tuple_get(currentValue(), m_memberIndices.at(_member)); } -smtutil::Expression SymbolicStructVariable::assignMember(string const& _member, smtutil::Expression const& _memberValue) +smtutil::Expression SymbolicStructVariable::assignMember(std::string const& _member, smtutil::Expression const& _memberValue) { auto const* structType = dynamic_cast(m_type); solAssert(structType, ""); @@ -385,7 +384,7 @@ smtutil::Expression SymbolicStructVariable::assignMember(string const& _member, return currentValue(); } -smtutil::Expression SymbolicStructVariable::assignAllMembers(vector const& _memberValues) +smtutil::Expression SymbolicStructVariable::assignAllMembers(std::vector const& _memberValues) { auto structType = dynamic_cast(m_type); solAssert(structType, ""); diff --git a/libsolidity/formal/VariableUsage.cpp b/libsolidity/formal/VariableUsage.cpp index 9ae4120c8086..ab7c425ae46c 100644 --- a/libsolidity/formal/VariableUsage.cpp +++ b/libsolidity/formal/VariableUsage.cpp @@ -25,13 +25,12 @@ #include -using namespace std; using namespace solidity; using namespace solidity::util; using namespace solidity::frontend; using namespace solidity::frontend::smt; -set VariableUsage::touchedVariables(ASTNode const& _node, vector const& _outerCallstack) +std::set VariableUsage::touchedVariables(ASTNode const& _node, std::vector const& _outerCallstack) { m_touchedVariables.clear(); m_callStack.clear(); diff --git a/scripts/check_style.sh b/scripts/check_style.sh index 917deea11371..cfc9def7abb3 100755 --- a/scripts/check_style.sh +++ b/scripts/check_style.sh @@ -29,6 +29,7 @@ NAMESPACE_STD_FREE_FILES=( libsolidity/ast/* libsolidity/codegen/ir/* libsolidity/codegen/* + libsolidity/formal/* ) (