Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Purge using namespace from libsolidity/formal #14491

Merged
merged 1 commit into from
Aug 15, 2023
Merged

Purge using namespace from libsolidity/formal #14491

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 6 additions & 7 deletions libsolidity/formal/ArraySlicePredicate.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,18 +20,17 @@

#include <liblangutil/Exceptions.h>

using namespace std;
using namespace solidity;
using namespace solidity::smtutil;
using namespace solidity::frontend;
using namespace solidity::frontend::smt;

map<string, ArraySlicePredicate::SliceData> ArraySlicePredicate::m_slicePredicates;
std::map<std::string, ArraySlicePredicate::SliceData> ArraySlicePredicate::m_slicePredicates;

pair<bool, ArraySlicePredicate::SliceData const&> ArraySlicePredicate::create(SortPointer _sort, EncodingContext& _context)
std::pair<bool, ArraySlicePredicate::SliceData const&> ArraySlicePredicate::create(SortPointer _sort, EncodingContext& _context)
{
solAssert(_sort->kind == Kind::Tuple, "");
auto tupleSort = dynamic_pointer_cast<TupleSort>(_sort);
auto tupleSort = std::dynamic_pointer_cast<TupleSort>(_sort);
solAssert(tupleSort, "");

auto tupleName = tupleSort->name;
Expand All @@ -47,12 +46,12 @@ pair<bool, ArraySlicePredicate::SliceData const&> ArraySlicePredicate::create(So
smt::SymbolicIntVariable endVar{TypeProvider::uint256(), TypeProvider::uint256(), "end_" + tupleName, _context };
smt::SymbolicIntVariable iVar{TypeProvider::uint256(), TypeProvider::uint256(), "i_" + tupleName, _context};

vector<SortPointer> domain{sort, sort, startVar.sort(), endVar.sort()};
auto sliceSort = make_shared<FunctionSort>(domain, SortProvider::boolSort);
std::vector<SortPointer> domain{sort, sort, startVar.sort(), endVar.sort()};
auto sliceSort = std::make_shared<FunctionSort>(domain, SortProvider::boolSort);
Predicate const& slice = *Predicate::create(sliceSort, "array_slice_" + tupleName, PredicateType::Custom, _context);

domain.emplace_back(iVar.sort());
auto predSort = make_shared<FunctionSort>(domain, SortProvider::boolSort);
auto predSort = std::make_shared<FunctionSort>(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);

Expand Down
61 changes: 30 additions & 31 deletions libsolidity/formal/BMC.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,6 @@
#include <z3_version.h>
#endif

using namespace std;
using namespace solidity;
using namespace solidity::util;
using namespace solidity::langutil;
Expand All @@ -41,13 +40,13 @@ BMC::BMC(
smt::EncodingContext& _context,
UniqueErrorReporter& _errorReporter,
UniqueErrorReporter& _unsupportedErrorReporter,
map<h256, string> const& _smtlib2Responses,
std::map<h256, std::string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback,
ModelCheckerSettings _settings,
CharStreamProvider const& _charStreamProvider
):
SMTEncoder(_context, _settings, _errorReporter, _unsupportedErrorReporter, _charStreamProvider),
m_interface(make_unique<smtutil::SMTPortfolio>(
m_interface(std::make_unique<smtutil::SMTPortfolio>(
_smtlib2Responses, _smtCallback, _settings.solvers, _settings.timeout, _settings.printQuery
))
{
Expand All @@ -65,7 +64,7 @@ BMC::BMC(
#endif
}

void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<VerificationTargetType>, smt::EncodingContext::IdCompare> _solvedTargets)
void BMC::analyze(SourceUnit const& _source, std::map<ASTNode const*, std::set<VerificationTargetType>, 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)
Expand Down Expand Up @@ -97,7 +96,7 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
2788_error,
{},
"BMC: " +
to_string(m_unprovedAmt) +
std::to_string(m_unprovedAmt) +
" 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." +
Expand All @@ -108,7 +107,7 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
m_errorReporter.info(
6002_error,
"BMC: " +
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."
);
Expand Down Expand Up @@ -138,7 +137,7 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
"BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available."
" None of the installed solvers was enabled."
#ifdef HAVE_Z3_DLOPEN
" Install libz3.so." + to_string(Z3_MAJOR_VERSION) + "." + to_string(Z3_MINOR_VERSION) + " to enable Z3."
" Install libz3.so." + std::to_string(Z3_MAJOR_VERSION) + "." + std::to_string(Z3_MINOR_VERSION) + " to enable Z3."
#endif
);
}
Expand Down Expand Up @@ -504,11 +503,11 @@ bool BMC::visit(TryStatement const& _tryStatement)
if (_tryStatement.successClause()->parameters())
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<pair<VariableIndices, smtutil::Expression>> clausesVisitResults;
std::vector<std::pair<VariableIndices, smtutil::Expression>> clausesVisitResults;
for (size_t i = 0; i < clauses.size(); ++i)
clausesVisitResults.push_back(visitBranch(clauses[i].get()));

Expand Down Expand Up @@ -736,7 +735,7 @@ void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall)
}
}

pair<smtutil::Expression, smtutil::Expression> BMC::arithmeticOperation(
std::pair<smtutil::Expression, smtutil::Expression> BMC::arithmeticOperation(
Token _op,
smtutil::Expression const& _left,
smtutil::Expression const& _right,
Expand Down Expand Up @@ -800,10 +799,10 @@ void BMC::reset()
m_loopExecutionHappened = false;
}

pair<vector<smtutil::Expression>, vector<string>> BMC::modelExpressions()
std::pair<std::vector<smtutil::Expression>, std::vector<std::string>> BMC::modelExpressions()
{
vector<smtutil::Expression> expressionsToEvaluate;
vector<string> expressionNames;
std::vector<smtutil::Expression> expressionsToEvaluate;
std::vector<std::string> expressionNames;
for (auto const& var: m_context.variables())
if (var.first->type()->isValueType())
{
Expand All @@ -826,7 +825,7 @@ pair<vector<smtutil::Expression>, vector<string>> 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()
Expand All @@ -839,7 +838,7 @@ pair<vector<smtutil::Expression>, vector<string>> BMC::modelExpressions()

/// Verification targets.

string BMC::targetDescription(BMCVerificationTarget const& _target)
std::string BMC::targetDescription(BMCVerificationTarget const& _target)
{
if (
_target.type == VerificationTargetType::Underflow ||
Expand Down Expand Up @@ -1065,20 +1064,20 @@ void BMC::addVerificationTarget(
void BMC::checkCondition(
BMCVerificationTarget const& _target,
smtutil::Expression _condition,
vector<SMTEncoder::CallStackEntry> const& _callStack,
pair<vector<smtutil::Expression>, vector<string>> const& _modelExpressions,
std::vector<SMTEncoder::CallStackEntry> const& _callStack,
std::pair<std::vector<smtutil::Expression>, std::vector<std::string>> 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<smtutil::Expression> expressionsToEvaluate;
vector<string> expressionNames;
std::vector<smtutil::Expression> expressionsToEvaluate;
std::vector<std::string> expressionNames;
tie(expressionsToEvaluate, expressionNames) = _modelExpressions;
if (!_callStack.empty())
if (_additionalValue)
Expand All @@ -1087,10 +1086,10 @@ void BMC::checkCondition(
expressionNames.push_back(_additionalValueName);
}
smtutil::CheckResult result;
vector<string> values;
std::vector<std::string> 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"
Expand Down Expand Up @@ -1119,7 +1118,7 @@ void BMC::checkCondition(
if (values.size() == expressionNames.size())
{
modelMessage << "Counterexample:\n";
map<string, string> sortedModel;
std::map<std::string, std::string> 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);
Expand Down Expand Up @@ -1165,7 +1164,7 @@ void BMC::checkBooleanNotConstant(
Expression const& _condition,
smtutil::Expression const& _constraints,
smtutil::Expression const& _value,
vector<SMTEncoder::CallStackEntry> const& _callStack
std::vector<SMTEncoder::CallStackEntry> const& _callStack
)
{
// Do not check for const-ness if this is a constant.
Expand Down Expand Up @@ -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, "");
Expand All @@ -1219,17 +1218,17 @@ void BMC::checkBooleanNotConstant(
}
}

pair<smtutil::CheckResult, vector<string>>
BMC::checkSatisfiableAndGenerateModel(vector<smtutil::Expression> const& _expressionsToEvaluate)
std::pair<smtutil::CheckResult, std::vector<std::string>>
BMC::checkSatisfiableAndGenerateModel(std::vector<smtutil::Expression> const& _expressionsToEvaluate)
{
smtutil::CheckResult result;
vector<string> values;
std::vector<std::string> values;
try
{
if (m_settings.printQuery)
{
auto portfolio = dynamic_cast<smtutil::SMTPortfolio*>(m_interface.get());
string smtlibCode = portfolio->dumpQuery(_expressionsToEvaluate);
std::string smtlibCode = portfolio->dumpQuery(_expressionsToEvaluate);
m_errorReporter.info(
6240_error,
"BMC: Requested query:\n" + smtlibCode
Expand All @@ -1239,14 +1238,14 @@ BMC::checkSatisfiableAndGenerateModel(vector<smtutil::Expression> 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
{
Expand Down
Loading