Skip to content

Commit

Permalink
Purge using namespace from libsolidity/formal
Browse files Browse the repository at this point in the history
  • Loading branch information
@nikola-matic
nikola-matic committed Aug 15, 2023
1 parent f085572 commit 763d279
Show file tree
Hide file tree
Showing 18 changed files with 492 additions and 507 deletions.
13 changes: 6 additions & 7 deletions libsolidity/formal/ArraySlicePredicate.cpp
View file
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
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

0 comments on commit 763d279

Please sign in to comment.