From 62723b7534bcd0975e8c926978b7b27d6dc035f7 Mon Sep 17 00:00:00 2001 From: Nikola Matic Date: Wed, 12 Jul 2023 14:09:19 +0200 Subject: [PATCH] Purge using namespace std in libsmtutil and libsolc --- libsmtutil/CHCSmtLib2Interface.cpp | 43 ++++++++-------- libsmtutil/CVC4Interface.cpp | 29 ++++++----- libsmtutil/SMTLib2Interface.cpp | 79 +++++++++++++++--------------- libsmtutil/SMTPortfolio.cpp | 25 +++++----- libsmtutil/Sorts.cpp | 12 ++--- libsmtutil/Z3CHCInterface.cpp | 33 ++++++------- libsmtutil/Z3Interface.cpp | 49 +++++++++--------- libsmtutil/Z3Loader.cpp | 5 +- libsolc/libsolc.cpp | 21 ++++---- scripts/check_style.sh | 2 + 10 files changed, 145 insertions(+), 153 deletions(-) diff --git a/libsmtutil/CHCSmtLib2Interface.cpp b/libsmtutil/CHCSmtLib2Interface.cpp index 4229cf5d6..ef7c56ac0 100644 --- a/libsmtutil/CHCSmtLib2Interface.cpp +++ b/libsmtutil/CHCSmtLib2Interface.cpp @@ -31,20 +31,19 @@ #include #include -using namespace std; using namespace solidity; using namespace solidity::util; using namespace solidity::frontend; using namespace solidity::smtutil; CHCSmtLib2Interface::CHCSmtLib2Interface( - map const& _queryResponses, + std::map const& _queryResponses, ReadCallback::Callback _smtCallback, SMTSolverChoice _enabledSolvers, - optional _queryTimeout + std::optional _queryTimeout ): CHCSolverInterface(_queryTimeout), - m_smtlib2(make_unique(_queryResponses, _smtCallback, m_queryTimeout)), + m_smtlib2(std::make_unique(_queryResponses, _smtCallback, m_queryTimeout)), m_queryResponses(std::move(_queryResponses)), m_smtCallback(_smtCallback), m_enabledSolvers(_enabledSolvers) @@ -66,8 +65,8 @@ void CHCSmtLib2Interface::registerRelation(Expression const& _expr) smtAssert(_expr.sort->kind == Kind::Function); if (!m_variables.count(_expr.name)) { - auto fSort = dynamic_pointer_cast(_expr.sort); - string domain = toSmtLibSort(fSort->domain); + auto fSort = std::dynamic_pointer_cast(_expr.sort); + std::string domain = toSmtLibSort(fSort->domain); // Relations are predicates which have implicit codomain Bool. m_variables.insert(_expr.name); write( @@ -89,10 +88,10 @@ void CHCSmtLib2Interface::addRule(Expression const& _expr, std::string const& /* ); } -tuple CHCSmtLib2Interface::query(Expression const& _block) +std::tuple CHCSmtLib2Interface::query(Expression const& _block) { - string query = dumpQuery(_block); - string response = querySolver(query); + std::string query = dumpQuery(_block); + std::string response = querySolver(query); CheckResult result; // TODO proper parsing @@ -108,7 +107,7 @@ tuple CHCSmtLib2Interface return {result, Expression(true), {}}; } -void CHCSmtLib2Interface::declareVariable(string const& _name, SortPointer const& _sort) +void CHCSmtLib2Interface::declareVariable(std::string const& _name, SortPointer const& _sort) { smtAssert(_sort); if (_sort->kind == Kind::Function) @@ -120,25 +119,25 @@ void CHCSmtLib2Interface::declareVariable(string const& _name, SortPointer const } } -string CHCSmtLib2Interface::toSmtLibSort(Sort const& _sort) +std::string CHCSmtLib2Interface::toSmtLibSort(Sort const& _sort) { if (!m_sortNames.count(&_sort)) m_sortNames[&_sort] = m_smtlib2->toSmtLibSort(_sort); return m_sortNames.at(&_sort); } -string CHCSmtLib2Interface::toSmtLibSort(vector const& _sorts) +std::string CHCSmtLib2Interface::toSmtLibSort(std::vector const& _sorts) { - string ssort("("); + std::string ssort("("); for (auto const& sort: _sorts) ssort += toSmtLibSort(*sort) + " "; ssort += ")"; return ssort; } -string CHCSmtLib2Interface::forall() +std::string CHCSmtLib2Interface::forall() { - string vars("("); + std::string vars("("); for (auto const& [name, sort]: m_smtlib2->variables()) { solAssert(sort, ""); @@ -149,17 +148,17 @@ string CHCSmtLib2Interface::forall() return vars; } -void CHCSmtLib2Interface::declareFunction(string const& _name, SortPointer const& _sort) +void CHCSmtLib2Interface::declareFunction(std::string const& _name, SortPointer const& _sort) { smtAssert(_sort); smtAssert(_sort->kind == Kind::Function); // TODO Use domain and codomain as key as well if (!m_variables.count(_name)) { - auto fSort = dynamic_pointer_cast(_sort); + auto fSort = std::dynamic_pointer_cast(_sort); smtAssert(fSort->codomain); - string domain = toSmtLibSort(fSort->domain); - string codomain = toSmtLibSort(*fSort->codomain); + std::string domain = toSmtLibSort(fSort->domain); + std::string codomain = toSmtLibSort(*fSort->codomain); m_variables.insert(_name); write( "(declare-fun |" + @@ -173,12 +172,12 @@ void CHCSmtLib2Interface::declareFunction(string const& _name, SortPointer const } } -void CHCSmtLib2Interface::write(string _data) +void CHCSmtLib2Interface::write(std::string _data) { m_accumulatedOutput += std::move(_data) + "\n"; } -string CHCSmtLib2Interface::querySolver(string const& _input) +std::string CHCSmtLib2Interface::querySolver(std::string const& _input) { util::h256 inputHash = util::keccak256(_input); if (m_queryResponses.count(inputHash)) @@ -212,7 +211,7 @@ std::string CHCSmtLib2Interface::dumpQuery(Expression const& _expr) std::string CHCSmtLib2Interface::createHeaderAndDeclarations() { std::stringstream s; if (m_queryTimeout) - s << "(set-option :timeout " + to_string(*m_queryTimeout) + ")\n"; + s << "(set-option :timeout " + std::to_string(*m_queryTimeout) + ")\n"; s << "(set-logic HORN)" << std::endl; for (auto const& decl: m_smtlib2->userSorts() | ranges::views::values) diff --git a/libsmtutil/CVC4Interface.cpp b/libsmtutil/CVC4Interface.cpp index 3c047782a..f53c92ab5 100644 --- a/libsmtutil/CVC4Interface.cpp +++ b/libsmtutil/CVC4Interface.cpp @@ -23,12 +23,11 @@ #include -using namespace std; using namespace solidity; using namespace solidity::util; using namespace solidity::smtutil; -CVC4Interface::CVC4Interface(optional _queryTimeout): +CVC4Interface::CVC4Interface(std::optional _queryTimeout): SolverInterface(_queryTimeout), m_solver(&m_context) { @@ -56,7 +55,7 @@ void CVC4Interface::pop() m_solver.pop(); } -void CVC4Interface::declareVariable(string const& _name, SortPointer const& _sort) +void CVC4Interface::declareVariable(std::string const& _name, SortPointer const& _sort) { smtAssert(_sort, ""); m_variables[_name] = m_context.mkVar(_name.c_str(), cvc4Sort(*_sort)); @@ -86,10 +85,10 @@ void CVC4Interface::addAssertion(Expression const& _expr) } } -pair> CVC4Interface::check(vector const& _expressionsToEvaluate) +std::pair> CVC4Interface::check(std::vector const& _expressionsToEvaluate) { CheckResult result; - vector values; + std::vector values; try { switch (m_solver.checkSat().isSat()) @@ -119,7 +118,7 @@ pair> CVC4Interface::check(vector const& values.clear(); } - return make_pair(result, values); + return std::make_pair(result, values); } CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr) @@ -128,13 +127,13 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr) if (_expr.arguments.empty() && m_variables.count(_expr.name)) return m_variables.at(_expr.name); - vector arguments; + std::vector arguments; for (auto const& arg: _expr.arguments) arguments.push_back(toCVC4Expr(arg)); try { - string const& n = _expr.name; + std::string const& n = _expr.name; // Function application if (!arguments.empty() && m_variables.count(_expr.name)) return m_context.mkExpr(CVC4::kind::APPLY_UF, m_variables.at(n), arguments); @@ -145,7 +144,7 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr) return m_context.mkConst(true); else if (n == "false") return m_context.mkConst(false); - else if (auto sortSort = dynamic_pointer_cast(_expr.sort)) + else if (auto sortSort = std::dynamic_pointer_cast(_expr.sort)) return m_context.mkVar(n, cvc4Sort(*sortSort->inner)); else try @@ -224,7 +223,7 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr) } else if (n == "bv2int") { - auto intSort = dynamic_pointer_cast(_expr.sort); + auto intSort = std::dynamic_pointer_cast(_expr.sort); smtAssert(intSort, ""); auto nat = m_context.mkExpr(CVC4::kind::BITVECTOR_TO_NAT, arguments[0]); if (!intSort->isSigned) @@ -254,13 +253,13 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr) return m_context.mkExpr(CVC4::kind::STORE, arguments[0], arguments[1], arguments[2]); else if (n == "const_array") { - shared_ptr sortSort = std::dynamic_pointer_cast(_expr.arguments[0].sort); + std::shared_ptr sortSort = std::dynamic_pointer_cast(_expr.arguments[0].sort); smtAssert(sortSort, ""); return m_context.mkConst(CVC4::ArrayStoreAll(cvc4Sort(*sortSort->inner), arguments[1])); } else if (n == "tuple_get") { - shared_ptr tupleSort = std::dynamic_pointer_cast(_expr.arguments[0].sort); + std::shared_ptr tupleSort = std::dynamic_pointer_cast(_expr.arguments[0].sort); smtAssert(tupleSort, ""); CVC4::DatatypeType tt = m_context.mkTupleType(cvc4Sort(tupleSort->components)); CVC4::Datatype const& dt = tt.getDatatype(); @@ -270,7 +269,7 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr) } else if (n == "tuple_constructor") { - shared_ptr tupleSort = std::dynamic_pointer_cast(_expr.sort); + std::shared_ptr tupleSort = std::dynamic_pointer_cast(_expr.sort); smtAssert(tupleSort, ""); CVC4::DatatypeType tt = m_context.mkTupleType(cvc4Sort(tupleSort->components)); CVC4::Datatype const& dt = tt.getDatatype(); @@ -328,9 +327,9 @@ CVC4::Type CVC4Interface::cvc4Sort(Sort const& _sort) return m_context.integerType(); } -vector CVC4Interface::cvc4Sort(vector const& _sorts) +std::vector CVC4Interface::cvc4Sort(std::vector const& _sorts) { - vector cvc4Sorts; + std::vector cvc4Sorts; for (auto const& _sort: _sorts) cvc4Sorts.push_back(cvc4Sort(*_sort)); return cvc4Sorts; diff --git a/libsmtutil/SMTLib2Interface.cpp b/libsmtutil/SMTLib2Interface.cpp index 85103d00e..ac5645bf1 100644 --- a/libsmtutil/SMTLib2Interface.cpp +++ b/libsmtutil/SMTLib2Interface.cpp @@ -33,16 +33,15 @@ #include #include -using namespace std; using namespace solidity; using namespace solidity::util; using namespace solidity::frontend; using namespace solidity::smtutil; SMTLib2Interface::SMTLib2Interface( - map _queryResponses, + std::map _queryResponses, ReadCallback::Callback _smtCallback, - optional _queryTimeout + std::optional _queryTimeout ): SolverInterface(_queryTimeout), m_queryResponses(std::move(_queryResponses)), @@ -59,7 +58,7 @@ void SMTLib2Interface::reset() m_userSorts.clear(); write("(set-option :produce-models true)"); if (m_queryTimeout) - write("(set-option :timeout " + to_string(*m_queryTimeout) + ")"); + write("(set-option :timeout " + std::to_string(*m_queryTimeout) + ")"); write("(set-logic ALL)"); } @@ -74,7 +73,7 @@ void SMTLib2Interface::pop() m_accumulatedOutput.pop_back(); } -void SMTLib2Interface::declareVariable(string const& _name, SortPointer const& _sort) +void SMTLib2Interface::declareVariable(std::string const& _name, SortPointer const& _sort) { smtAssert(_sort, ""); if (_sort->kind == Kind::Function) @@ -86,16 +85,16 @@ void SMTLib2Interface::declareVariable(string const& _name, SortPointer const& _ } } -void SMTLib2Interface::declareFunction(string const& _name, SortPointer const& _sort) +void SMTLib2Interface::declareFunction(std::string const& _name, SortPointer const& _sort) { smtAssert(_sort, ""); smtAssert(_sort->kind == Kind::Function, ""); // TODO Use domain and codomain as key as well if (!m_variables.count(_name)) { - auto const& fSort = dynamic_pointer_cast(_sort); - string domain = toSmtLibSort(fSort->domain); - string codomain = toSmtLibSort(*fSort->codomain); + auto const& fSort = std::dynamic_pointer_cast(_sort); + std::string domain = toSmtLibSort(fSort->domain); + std::string codomain = toSmtLibSort(*fSort->codomain); m_variables.emplace(_name, _sort); write( "(declare-fun |" + @@ -114,9 +113,9 @@ void SMTLib2Interface::addAssertion(Expression const& _expr) write("(assert " + toSExpr(_expr) + ")"); } -pair> SMTLib2Interface::check(vector const& _expressionsToEvaluate) +std::pair> SMTLib2Interface::check(std::vector const& _expressionsToEvaluate) { - string response = querySolver( + std::string response = querySolver( boost::algorithm::join(m_accumulatedOutput, "\n") + checkSatAndGetValuesCommand(_expressionsToEvaluate) ); @@ -132,13 +131,13 @@ pair> SMTLib2Interface::check(vector con else result = CheckResult::ERROR; - vector values; + std::vector values; if (result == CheckResult::SATISFIABLE && !_expressionsToEvaluate.empty()) values = parseValues(find(response.cbegin(), response.cend(), '\n'), response.cend()); - return make_pair(result, values); + return std::make_pair(result, values); } -string SMTLib2Interface::toSExpr(Expression const& _expr) +std::string SMTLib2Interface::toSExpr(Expression const& _expr) { if (_expr.arguments.empty()) return _expr.name; @@ -148,16 +147,16 @@ string SMTLib2Interface::toSExpr(Expression const& _expr) { size_t size = std::stoul(_expr.arguments[1].name); auto arg = toSExpr(_expr.arguments.front()); - auto int2bv = "(_ int2bv " + to_string(size) + ")"; + auto int2bv = "(_ int2bv " + std::to_string(size) + ")"; // Some solvers treat all BVs as unsigned, so we need to manually apply 2's complement if needed. - sexpr += string("ite ") + + sexpr += std::string("ite ") + "(>= " + arg + " 0) " + "(" + int2bv + " " + arg + ") " + "(bvneg (" + int2bv + " (- " + arg + ")))"; } else if (_expr.name == "bv2int") { - auto intSort = dynamic_pointer_cast(_expr.sort); + auto intSort = std::dynamic_pointer_cast(_expr.sort); smtAssert(intSort, ""); auto arg = toSExpr(_expr.arguments.front()); @@ -166,13 +165,13 @@ string SMTLib2Interface::toSExpr(Expression const& _expr) if (!intSort->isSigned) return nat; - auto bvSort = dynamic_pointer_cast(_expr.arguments.front().sort); + auto bvSort = std::dynamic_pointer_cast(_expr.arguments.front().sort); smtAssert(bvSort, ""); - auto size = to_string(bvSort->size); - auto pos = to_string(bvSort->size - 1); + auto size = std::to_string(bvSort->size); + auto pos = std::to_string(bvSort->size - 1); // Some solvers treat all BVs as unsigned, so we need to manually apply 2's complement if needed. - sexpr += string("ite ") + + sexpr += std::string("ite ") + "(= ((_ extract " + pos + " " + pos + ")" + arg + ") #b0) " + nat + " " + "(- (bv2nat (bvneg " + arg + ")))"; @@ -182,7 +181,7 @@ string SMTLib2Interface::toSExpr(Expression const& _expr) smtAssert(_expr.arguments.size() == 2, ""); auto sortSort = std::dynamic_pointer_cast(_expr.arguments.at(0).sort); smtAssert(sortSort, ""); - auto arraySort = dynamic_pointer_cast(sortSort->inner); + auto arraySort = std::dynamic_pointer_cast(sortSort->inner); smtAssert(arraySort, ""); sexpr += "(as const " + toSmtLibSort(*arraySort) + ") "; sexpr += toSExpr(_expr.arguments.at(1)); @@ -190,14 +189,14 @@ string SMTLib2Interface::toSExpr(Expression const& _expr) else if (_expr.name == "tuple_get") { smtAssert(_expr.arguments.size() == 2, ""); - auto tupleSort = dynamic_pointer_cast(_expr.arguments.at(0).sort); + auto tupleSort = std::dynamic_pointer_cast(_expr.arguments.at(0).sort); size_t index = std::stoul(_expr.arguments.at(1).name); smtAssert(index < tupleSort->members.size(), ""); sexpr += "|" + tupleSort->members.at(index) + "| " + toSExpr(_expr.arguments.at(0)); } else if (_expr.name == "tuple_constructor") { - auto tupleSort = dynamic_pointer_cast(_expr.sort); + auto tupleSort = std::dynamic_pointer_cast(_expr.sort); smtAssert(tupleSort, ""); sexpr += "|" + tupleSort->name + "|"; for (auto const& arg: _expr.arguments) @@ -213,7 +212,7 @@ string SMTLib2Interface::toSExpr(Expression const& _expr) return sexpr; } -string SMTLib2Interface::toSmtLibSort(Sort const& _sort) +std::string SMTLib2Interface::toSmtLibSort(Sort const& _sort) { switch (_sort.kind) { @@ -222,7 +221,7 @@ string SMTLib2Interface::toSmtLibSort(Sort const& _sort) case Kind::Bool: return "Bool"; case Kind::BitVector: - return "(_ BitVec " + to_string(dynamic_cast(_sort).size) + ")"; + return "(_ BitVec " + std::to_string(dynamic_cast(_sort).size) + ")"; case Kind::Array: { auto const& arraySort = dynamic_cast(_sort); @@ -232,11 +231,11 @@ string SMTLib2Interface::toSmtLibSort(Sort const& _sort) case Kind::Tuple: { auto const& tupleSort = dynamic_cast(_sort); - string tupleName = "|" + tupleSort.name + "|"; + std::string tupleName = "|" + tupleSort.name + "|"; auto isName = [&](auto entry) { return entry.first == tupleName; }; if (ranges::find_if(m_userSorts, isName) == m_userSorts.end()) { - string decl("(declare-datatypes ((" + tupleName + " 0)) (((" + tupleName); + std::string decl("(declare-datatypes ((" + tupleName + " 0)) (((" + tupleName); smtAssert(tupleSort.members.size() == tupleSort.components.size(), ""); for (unsigned i = 0; i < tupleSort.members.size(); ++i) decl += " (|" + tupleSort.members.at(i) + "| " + toSmtLibSort(*tupleSort.components.at(i)) + ")"; @@ -252,24 +251,24 @@ string SMTLib2Interface::toSmtLibSort(Sort const& _sort) } } -string SMTLib2Interface::toSmtLibSort(vector const& _sorts) +std::string SMTLib2Interface::toSmtLibSort(std::vector const& _sorts) { - string ssort("("); + std::string ssort("("); for (auto const& sort: _sorts) ssort += toSmtLibSort(*sort) + " "; ssort += ")"; return ssort; } -void SMTLib2Interface::write(string _data) +void SMTLib2Interface::write(std::string _data) { smtAssert(!m_accumulatedOutput.empty(), ""); m_accumulatedOutput.back() += std::move(_data) + "\n"; } -string SMTLib2Interface::checkSatAndGetValuesCommand(vector const& _expressionsToEvaluate) +std::string SMTLib2Interface::checkSatAndGetValuesCommand(std::vector const& _expressionsToEvaluate) { - string command; + std::string command; if (_expressionsToEvaluate.empty()) command = "(check-sat)\n"; else @@ -279,22 +278,22 @@ string SMTLib2Interface::checkSatAndGetValuesCommand(vector const& _ { auto const& e = _expressionsToEvaluate.at(i); smtAssert(e.sort->kind == Kind::Int || e.sort->kind == Kind::Bool, "Invalid sort for expression to evaluate."); - command += "(declare-const |EVALEXPR_" + to_string(i) + "| " + (e.sort->kind == Kind::Int ? "Int" : "Bool") + ")\n"; - command += "(assert (= |EVALEXPR_" + to_string(i) + "| " + toSExpr(e) + "))\n"; + command += "(declare-const |EVALEXPR_" + std::to_string(i) + "| " + (e.sort->kind == Kind::Int ? "Int" : "Bool") + ")\n"; + command += "(assert (= |EVALEXPR_" + std::to_string(i) + "| " + toSExpr(e) + "))\n"; } command += "(check-sat)\n"; command += "(get-value ("; for (size_t i = 0; i < _expressionsToEvaluate.size(); i++) - command += "|EVALEXPR_" + to_string(i) + "| "; + command += "|EVALEXPR_" + std::to_string(i) + "| "; command += "))\n"; } return command; } -vector SMTLib2Interface::parseValues(string::const_iterator _start, string::const_iterator _end) +std::vector SMTLib2Interface::parseValues(std::string::const_iterator _start, std::string::const_iterator _end) { - vector values; + std::vector values; while (_start < _end) { auto valStart = find(_start, _end, ' '); @@ -308,7 +307,7 @@ vector SMTLib2Interface::parseValues(string::const_iterator _start, stri return values; } -string SMTLib2Interface::querySolver(string const& _input) +std::string SMTLib2Interface::querySolver(std::string const& _input) { h256 inputHash = keccak256(_input); if (m_queryResponses.count(inputHash)) @@ -323,7 +322,7 @@ string SMTLib2Interface::querySolver(string const& _input) return "unknown\n"; } -string SMTLib2Interface::dumpQuery(vector const& _expressionsToEvaluate) +std::string SMTLib2Interface::dumpQuery(std::vector const& _expressionsToEvaluate) { return boost::algorithm::join(m_accumulatedOutput, "\n") + checkSatAndGetValuesCommand(_expressionsToEvaluate); diff --git a/libsmtutil/SMTPortfolio.cpp b/libsmtutil/SMTPortfolio.cpp index be961d01f..76c69d018 100644 --- a/libsmtutil/SMTPortfolio.cpp +++ b/libsmtutil/SMTPortfolio.cpp @@ -26,31 +26,30 @@ #endif #include -using namespace std; using namespace solidity; using namespace solidity::util; using namespace solidity::frontend; using namespace solidity::smtutil; SMTPortfolio::SMTPortfolio( - map _smtlib2Responses, + std::map _smtlib2Responses, frontend::ReadCallback::Callback _smtCallback, [[maybe_unused]] SMTSolverChoice _enabledSolvers, - optional _queryTimeout, + std::optional _queryTimeout, bool _printQuery ): SolverInterface(_queryTimeout) { solAssert(!_printQuery || _enabledSolvers == smtutil::SMTSolverChoice::SMTLIB2(), "Only SMTLib2 solver can be enabled to print queries"); if (_enabledSolvers.smtlib2) - m_solvers.emplace_back(make_unique(std::move(_smtlib2Responses), std::move(_smtCallback), m_queryTimeout)); + m_solvers.emplace_back(std::make_unique(std::move(_smtlib2Responses), std::move(_smtCallback), m_queryTimeout)); #ifdef HAVE_Z3 if (_enabledSolvers.z3 && Z3Interface::available()) - m_solvers.emplace_back(make_unique(m_queryTimeout)); + m_solvers.emplace_back(std::make_unique(m_queryTimeout)); #endif #ifdef HAVE_CVC4 if (_enabledSolvers.cvc4) - m_solvers.emplace_back(make_unique(m_queryTimeout)); + m_solvers.emplace_back(std::make_unique(m_queryTimeout)); #endif } @@ -72,7 +71,7 @@ void SMTPortfolio::pop() s->pop(); } -void SMTPortfolio::declareVariable(string const& _name, SortPointer const& _sort) +void SMTPortfolio::declareVariable(std::string const& _name, SortPointer const& _sort) { smtAssert(_sort, ""); for (auto const& s: m_solvers) @@ -115,14 +114,14 @@ void SMTPortfolio::addAssertion(Expression const& _expr) * * If all solvers return ERROR, the result is ERROR. */ -pair> SMTPortfolio::check(vector const& _expressionsToEvaluate) +std::pair> SMTPortfolio::check(std::vector const& _expressionsToEvaluate) { CheckResult lastResult = CheckResult::ERROR; - vector finalValues; + std::vector finalValues; for (auto const& s: m_solvers) { CheckResult result; - vector values; + std::vector values; tie(result, values) = s->check(_expressionsToEvaluate); if (solverAnswered(result)) { @@ -140,10 +139,10 @@ pair> SMTPortfolio::check(vector const& else if (result == CheckResult::UNKNOWN && lastResult == CheckResult::ERROR) lastResult = result; } - return make_pair(lastResult, finalValues); + return std::make_pair(lastResult, finalValues); } -vector SMTPortfolio::unhandledQueries() +std::vector SMTPortfolio::unhandledQueries() { // This code assumes that the constructor guarantees that // SmtLib2Interface is in position 0, if enabled. @@ -158,7 +157,7 @@ bool SMTPortfolio::solverAnswered(CheckResult result) return result == CheckResult::SATISFIABLE || result == CheckResult::UNSATISFIABLE; } -string SMTPortfolio::dumpQuery(vector const& _expressionsToEvaluate) +std::string SMTPortfolio::dumpQuery(std::vector const& _expressionsToEvaluate) { // This code assumes that the constructor guarantees that // SmtLib2Interface is in position 0, if enabled. diff --git a/libsmtutil/Sorts.cpp b/libsmtutil/Sorts.cpp index 543c7ba0f..b45bb303c 100644 --- a/libsmtutil/Sorts.cpp +++ b/libsmtutil/Sorts.cpp @@ -19,22 +19,20 @@ #include -using namespace std; - namespace solidity::smtutil { -shared_ptr const SortProvider::boolSort{make_shared(Kind::Bool)}; -shared_ptr const SortProvider::uintSort{make_shared(false)}; -shared_ptr const SortProvider::sintSort{make_shared(true)}; +std::shared_ptr const SortProvider::boolSort{std::make_shared(Kind::Bool)}; +std::shared_ptr const SortProvider::uintSort{std::make_shared(false)}; +std::shared_ptr const SortProvider::sintSort{std::make_shared(true)}; -shared_ptr SortProvider::intSort(bool _signed) +std::shared_ptr SortProvider::intSort(bool _signed) { if (_signed) return sintSort; return uintSort; } -shared_ptr const SortProvider::bitVectorSort{make_shared(256)}; +std::shared_ptr const SortProvider::bitVectorSort{std::make_shared(256)}; } diff --git a/libsmtutil/Z3CHCInterface.cpp b/libsmtutil/Z3CHCInterface.cpp index bfbc9841b..a25890e8d 100644 --- a/libsmtutil/Z3CHCInterface.cpp +++ b/libsmtutil/Z3CHCInterface.cpp @@ -23,21 +23,20 @@ #include #include -using namespace std; using namespace solidity; using namespace solidity::smtutil; -Z3CHCInterface::Z3CHCInterface(optional _queryTimeout): +Z3CHCInterface::Z3CHCInterface(std::optional _queryTimeout): CHCSolverInterface(_queryTimeout), - m_z3Interface(make_unique(m_queryTimeout)), + m_z3Interface(std::make_unique(m_queryTimeout)), m_context(m_z3Interface->context()), m_solver(*m_context) { Z3_get_version( - &get<0>(m_version), - &get<1>(m_version), - &get<2>(m_version), - &get<3>(m_version) + &std::get<0>(m_version), + &std::get<1>(m_version), + &std::get<2>(m_version), + &std::get<3>(m_version) ); // These need to be set globally. @@ -51,7 +50,7 @@ Z3CHCInterface::Z3CHCInterface(optional _queryTimeout): setSpacerOptions(); } -void Z3CHCInterface::declareVariable(string const& _name, SortPointer const& _sort) +void Z3CHCInterface::declareVariable(std::string const& _name, SortPointer const& _sort) { smtAssert(_sort, ""); m_z3Interface->declareVariable(_name, _sort); @@ -62,7 +61,7 @@ void Z3CHCInterface::registerRelation(Expression const& _expr) m_solver.register_relation(m_z3Interface->functions().at(_expr.name)); } -void Z3CHCInterface::addRule(Expression const& _expr, string const& _name) +void Z3CHCInterface::addRule(Expression const& _expr, std::string const& _name) { z3::expr rule = m_z3Interface->toZ3Expr(_expr); if (m_z3Interface->constants().empty()) @@ -77,7 +76,7 @@ void Z3CHCInterface::addRule(Expression const& _expr, string const& _name) } } -tuple Z3CHCInterface::query(Expression const& _expr) +std::tuple Z3CHCInterface::query(Expression const& _expr) { CheckResult result; try @@ -90,7 +89,7 @@ tuple Z3CHCInterface::que result = CheckResult::SATISFIABLE; // z3 version 4.8.8 modified Spacer to also return // proofs containing nonlinear clauses. - if (m_version >= tuple(4, 8, 8, 0)) + if (m_version >= std::tuple(4, 8, 8, 0)) { auto proof = m_solver.get_answer(); return {result, Expression(true), cexGraph(proof)}; @@ -113,7 +112,7 @@ tuple Z3CHCInterface::que } catch (z3::exception const& _err) { - set msgs{ + std::set msgs{ /// Resource limit (rlimit) exhausted. "max. resource limit exceeded", /// User given timeout exhausted. @@ -178,13 +177,13 @@ CHCSolverInterface::CexGraph Z3CHCInterface::cexGraph(z3::expr const& _proof) CexGraph graph; - stack proofStack; + std::stack proofStack; proofStack.push(_proof.arg(0)); auto const& root = proofStack.top(); graph.nodes.emplace(root.id(), m_z3Interface->fromZ3Expr(fact(root))); - set visited; + std::set visited; visited.insert(root.id()); while (!proofStack.empty()) @@ -227,16 +226,16 @@ z3::expr Z3CHCInterface::fact(z3::expr const& _node) return _node.arg(_node.num_args() - 1); } -string Z3CHCInterface::name(z3::expr const& _predicate) +std::string Z3CHCInterface::name(z3::expr const& _predicate) { smtAssert(_predicate.is_app(), ""); return _predicate.decl().name().str(); } -vector Z3CHCInterface::arguments(z3::expr const& _predicate) +std::vector Z3CHCInterface::arguments(z3::expr const& _predicate) { smtAssert(_predicate.is_app(), ""); - vector args; + std::vector args; for (unsigned i = 0; i < _predicate.num_args(); ++i) args.emplace_back(_predicate.arg(i).to_string()); return args; diff --git a/libsmtutil/Z3Interface.cpp b/libsmtutil/Z3Interface.cpp index 21b31d19f..a16e75668 100644 --- a/libsmtutil/Z3Interface.cpp +++ b/libsmtutil/Z3Interface.cpp @@ -26,7 +26,6 @@ #include #endif -using namespace std; using namespace solidity::smtutil; using namespace solidity::util; @@ -69,7 +68,7 @@ void Z3Interface::pop() m_solver.pop(); } -void Z3Interface::declareVariable(string const& _name, SortPointer const& _sort) +void Z3Interface::declareVariable(std::string const& _name, SortPointer const& _sort) { smtAssert(_sort, ""); if (_sort->kind == Kind::Function) @@ -80,7 +79,7 @@ void Z3Interface::declareVariable(string const& _name, SortPointer const& _sort) m_constants.emplace(_name, m_context.constant(_name.c_str(), z3Sort(*_sort))); } -void Z3Interface::declareFunction(string const& _name, Sort const& _sort) +void Z3Interface::declareFunction(std::string const& _name, Sort const& _sort) { smtAssert(_sort.kind == Kind::Function, ""); FunctionSort fSort = dynamic_cast(_sort); @@ -95,10 +94,10 @@ void Z3Interface::addAssertion(Expression const& _expr) m_solver.add(toZ3Expr(_expr)); } -pair> Z3Interface::check(vector const& _expressionsToEvaluate) +std::pair> Z3Interface::check(std::vector const& _expressionsToEvaluate) { CheckResult result; - vector values; + std::vector values; try { switch (m_solver.check()) @@ -123,7 +122,7 @@ pair> Z3Interface::check(vector const& _ } catch (z3::exception const& _err) { - set msgs{ + std::set msgs{ /// Resource limit (rlimit) exhausted. "max. resource limit exceeded", /// User given timeout exhausted. @@ -137,7 +136,7 @@ pair> Z3Interface::check(vector const& _ values.clear(); } - return make_pair(result, values); + return std::make_pair(result, values); } z3::expr Z3Interface::toZ3Expr(Expression const& _expr) @@ -150,7 +149,7 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr) try { - string const& n = _expr.name; + std::string const& n = _expr.name; if (m_functions.count(n)) return m_functions.at(n)(arguments); else if (m_constants.count(n)) @@ -166,7 +165,7 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr) return m_context.bool_val(false); else if (_expr.sort->kind == Kind::Sort) { - auto sortSort = dynamic_pointer_cast(_expr.sort); + auto sortSort = std::dynamic_pointer_cast(_expr.sort); smtAssert(sortSort, ""); return m_context.constant(n.c_str(), z3Sort(*sortSort->inner)); } @@ -233,7 +232,7 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr) } else if (n == "bv2int") { - auto intSort = dynamic_pointer_cast(_expr.sort); + auto intSort = std::dynamic_pointer_cast(_expr.sort); smtAssert(intSort, ""); return z3::bv2int(arguments[0], intSort->isSigned); } @@ -243,9 +242,9 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr) return z3::store(arguments[0], arguments[1], arguments[2]); else if (n == "const_array") { - shared_ptr sortSort = std::dynamic_pointer_cast(_expr.arguments[0].sort); + std::shared_ptr sortSort = std::dynamic_pointer_cast(_expr.arguments[0].sort); smtAssert(sortSort, ""); - auto arraySort = dynamic_pointer_cast(sortSort->inner); + auto arraySort = std::dynamic_pointer_cast(sortSort->inner); smtAssert(arraySort && arraySort->domain, ""); return z3::const_array(z3Sort(*arraySort->domain), arguments[1]); } @@ -285,7 +284,7 @@ Expression Z3Interface::fromZ3Expr(z3::expr const& _expr) if (_expr.is_quantifier()) { - string quantifierName; + std::string quantifierName; if (_expr.is_exists()) quantifierName = "exists"; else if (_expr.is_forall()) @@ -297,7 +296,7 @@ Expression Z3Interface::fromZ3Expr(z3::expr const& _expr) return Expression(quantifierName, {fromZ3Expr(_expr.body())}, sort); } smtAssert(_expr.is_app(), ""); - vector arguments; + std::vector arguments; for (unsigned i = 0; i < _expr.num_args(); ++i) arguments.push_back(fromZ3Expr(_expr.arg(i))); @@ -370,12 +369,12 @@ Expression Z3Interface::fromZ3Expr(z3::expr const& _expr) return Expression::store(arguments[0], arguments[1], arguments[2]); else if (kind == Z3_OP_CONST_ARRAY) { - auto sortSort = make_shared(fromZ3Sort(_expr.get_sort())); + auto sortSort = std::make_shared(fromZ3Sort(_expr.get_sort())); return Expression::const_array(Expression(sortSort), arguments[0]); } else if (kind == Z3_OP_DT_CONSTRUCTOR) { - auto sortSort = make_shared(fromZ3Sort(_expr.get_sort())); + auto sortSort = std::make_shared(fromZ3Sort(_expr.get_sort())); return Expression::tuple_constructor(Expression(sortSort), arguments); } else if (kind == Z3_OP_DT_ACCESSOR) @@ -412,12 +411,12 @@ z3::sort Z3Interface::z3Sort(Sort const& _sort) case Kind::Tuple: { auto const& tupleSort = dynamic_cast(_sort); - vector cMembers; + std::vector cMembers; for (auto const& member: tupleSort.members) cMembers.emplace_back(member.c_str()); /// Using this instead of the function below because with that one /// we can't use `&sorts[0]` here. - vector sorts; + std::vector sorts; for (auto const& sort: tupleSort.components) sorts.push_back(z3Sort(*sort)); z3::func_decl_vector projs(m_context); @@ -439,7 +438,7 @@ z3::sort Z3Interface::z3Sort(Sort const& _sort) return m_context.int_sort(); } -z3::sort_vector Z3Interface::z3Sort(vector const& _sorts) +z3::sort_vector Z3Interface::z3Sort(std::vector const& _sorts) { z3::sort_vector z3Sorts(m_context); for (auto const& _sort: _sorts) @@ -454,27 +453,27 @@ SortPointer Z3Interface::fromZ3Sort(z3::sort const& _sort) if (_sort.is_int()) return SortProvider::sintSort; if (_sort.is_bv()) - return make_shared(_sort.bv_size()); + return std::make_shared(_sort.bv_size()); if (_sort.is_array()) - return make_shared(fromZ3Sort(_sort.array_domain()), fromZ3Sort(_sort.array_range())); + return std::make_shared(fromZ3Sort(_sort.array_domain()), fromZ3Sort(_sort.array_range())); if (_sort.is_datatype()) { auto name = _sort.name().str(); auto constructor = z3::func_decl(m_context, Z3_get_tuple_sort_mk_decl(m_context, _sort)); - vector memberNames; - vector memberSorts; + std::vector memberNames; + std::vector memberSorts; for (unsigned i = 0; i < constructor.arity(); ++i) { auto accessor = z3::func_decl(m_context, Z3_get_tuple_sort_field_decl(m_context, _sort, i)); memberNames.push_back(accessor.name().str()); memberSorts.push_back(fromZ3Sort(accessor.range())); } - return make_shared(name, memberNames, memberSorts); + return std::make_shared(name, memberNames, memberSorts); } smtAssert(false, ""); } -vector Z3Interface::fromZ3Sort(z3::sort_vector const& _sorts) +std::vector Z3Interface::fromZ3Sort(z3::sort_vector const& _sorts) { return applyMap(_sorts, [this](auto const& sort) { return fromZ3Sort(sort); }); } diff --git a/libsmtutil/Z3Loader.cpp b/libsmtutil/Z3Loader.cpp index 86b17aa03..0211f600d 100644 --- a/libsmtutil/Z3Loader.cpp +++ b/libsmtutil/Z3Loader.cpp @@ -27,7 +27,6 @@ #endif #include -using namespace std; using namespace solidity; using namespace solidity::smtutil; @@ -41,7 +40,7 @@ void* Z3Loader::loadSymbol(char const* _name) const { smtAssert(m_handle, "Attempted to use dynamically loaded Z3, even though it is not available."); void* sym = dlsym(m_handle, _name); - smtAssert(sym, string("Symbol \"") + _name + "\" not found in libz3.so"); + smtAssert(sym, std::string("Symbol \"") + _name + "\" not found in libz3.so"); return sym; } @@ -59,7 +58,7 @@ bool Z3Loader::available() const Z3Loader::Z3Loader() { - string libname{"libz3.so." + to_string(Z3_MAJOR_VERSION) + "." + to_string(Z3_MINOR_VERSION)}; + std::string libname{"libz3.so." + std::to_string(Z3_MAJOR_VERSION) + "." + std::to_string(Z3_MINOR_VERSION)}; m_handle = dlmopen(LM_ID_NEWLM, libname.c_str(), RTLD_NOW); } diff --git a/libsolc/libsolc.cpp b/libsolc/libsolc.cpp index 4ceeeac6f..105949253 100644 --- a/libsolc/libsolc.cpp +++ b/libsolc/libsolc.cpp @@ -32,7 +32,6 @@ #include "license.h" -using namespace std; using namespace solidity; using namespace solidity::util; @@ -42,21 +41,21 @@ using solidity::frontend::StandardCompiler; namespace { -// The strings in this list must not be resized after they have been added here (via solidity_alloc()), because +// The std::strings in this list must not be resized after they have been added here (via solidity_alloc()), because // this may potentially change the pointer that was passed to the caller from solidity_alloc(). -static list solidityAllocations; +static std::list solidityAllocations; /// Find the equivalent to @p _data in the list of allocations of solidity_alloc(), /// removes it from the list and returns its value. /// /// If any invalid argument is being passed, it is considered a programming error /// on the caller-side and hence, will call abort() then. -string takeOverAllocation(char const* _data) +std::string takeOverAllocation(char const* _data) { for (auto iter = begin(solidityAllocations); iter != end(solidityAllocations); ++iter) if (iter->data() == _data) { - string chunk = std::move(*iter); + std::string chunk = std::move(*iter); solidityAllocations.erase(iter); return chunk; } @@ -64,11 +63,11 @@ string takeOverAllocation(char const* _data) abort(); } -/// Resizes a std::string to the proper length based on the occurrence of a zero terminator. -void truncateCString(string& _data) +/// Resizes a std::std::string to the proper length based on the occurrence of a zero terminator. +void truncateCString(std::string& _data) { size_t pos = _data.find('\0'); - if (pos != string::npos) + if (pos != std::string::npos) _data.resize(pos); } @@ -77,7 +76,7 @@ ReadCallback::Callback wrapReadCallback(CStyleReadFileCallback _readCallback, vo ReadCallback::Callback readCallback; if (_readCallback) { - readCallback = [=](string const& _kind, string const& _data) + readCallback = [=](std::string const& _kind, std::string const& _data) { char* contents_c = nullptr; char* error_c = nullptr; @@ -106,7 +105,7 @@ ReadCallback::Callback wrapReadCallback(CStyleReadFileCallback _readCallback, vo return readCallback; } -string compile(string _input, CStyleReadFileCallback _readCallback, void* _readContext) +std::string compile(std::string _input, CStyleReadFileCallback _readCallback, void* _readContext) { StandardCompiler compiler(wrapReadCallback(_readCallback, _readContext)); return compiler.compile(std::move(_input)); @@ -118,7 +117,7 @@ extern "C" { extern char const* solidity_license() noexcept { - static string fullLicenseText = otherLicenses + licenseText; + static std::string fullLicenseText = otherLicenses + licenseText; return fullLicenseText.c_str(); } diff --git a/scripts/check_style.sh b/scripts/check_style.sh index bd9fbf005..34fbf0381 100755 --- a/scripts/check_style.sh +++ b/scripts/check_style.sh @@ -23,6 +23,8 @@ EXCLUDE_FILES_JOINED=${EXCLUDE_FILES_JOINED%??} NAMESPACE_STD_FREE_FILES=( libevmasm/* liblangutil/* + libsmtutil/* + libsolc/* ) (