cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Purge using namespace from libsolidity/formal

Browse Source
This commit is contained in:
Nikola Matic 2023-08-14 22:19:11 +02:00
parent f085572e24
commit d0a5556fd0
18 changed files with 491 additions and 506 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
libsolidity/formal/ArraySlicePredicate.cpp
View File

@ -20,18 +20,17 @@
#include <liblangutil/Exceptions.h> #include <liblangutil/Exceptions.h>
using namespace std;
using namespace solidity; using namespace solidity;
using namespace solidity::smtutil; using namespace solidity::smtutil;
using namespace solidity::frontend; using namespace solidity::frontend;
using namespace solidity::frontend::smt; 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, ""); solAssert(_sort->kind == Kind::Tuple, "");
auto tupleSort = dynamic_pointer_cast<TupleSort>(_sort); auto tupleSort = std::dynamic_pointer_cast<TupleSort>(_sort);
solAssert(tupleSort, ""); solAssert(tupleSort, "");
auto tupleName = tupleSort->name; auto tupleName = tupleSort->name;
@ -47,12 +46,12 @@ pair<bool, ArraySlicePredicate::SliceData const&> ArraySlicePredicate::create(So
smt::SymbolicIntVariable endVar{TypeProvider::uint256(), TypeProvider::uint256(), "end_" + tupleName, _context }; smt::SymbolicIntVariable endVar{TypeProvider::uint256(), TypeProvider::uint256(), "end_" + tupleName, _context };
smt::SymbolicIntVariable iVar{TypeProvider::uint256(), TypeProvider::uint256(), "i_" + tupleName, _context}; smt::SymbolicIntVariable iVar{TypeProvider::uint256(), TypeProvider::uint256(), "i_" + tupleName, _context};
vector<SortPointer> domain{sort, sort, startVar.sort(), endVar.sort()}; std::vector<SortPointer> domain{sort, sort, startVar.sort(), endVar.sort()};
auto sliceSort = make_shared<FunctionSort>(domain, SortProvider::boolSort); auto sliceSort = std::make_shared<FunctionSort>(domain, SortProvider::boolSort);
Predicate const& slice = *Predicate::create(sliceSort, "array_slice_" + tupleName, PredicateType::Custom, _context); Predicate const& slice = *Predicate::create(sliceSort, "array_slice_" + tupleName, PredicateType::Custom, _context);
domain.emplace_back(iVar.sort()); 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& header = *Predicate::create(predSort, "array_slice_header_" + tupleName, PredicateType::Custom, _context);
Predicate const& loop = *Predicate::create(predSort, "array_slice_loop_" + tupleName, PredicateType::Custom, _context); Predicate const& loop = *Predicate::create(predSort, "array_slice_loop_" + tupleName, PredicateType::Custom, _context);

61
libsolidity/formal/BMC.cpp
View File

@ -31,7 +31,6 @@
#include <z3_version.h> #include <z3_version.h>
#endif #endif
using namespace std;
using namespace solidity; using namespace solidity;
using namespace solidity::util; using namespace solidity::util;
using namespace solidity::langutil; using namespace solidity::langutil;
@ -41,13 +40,13 @@ BMC::BMC(
smt::EncodingContext& _context, smt::EncodingContext& _context,
UniqueErrorReporter& _errorReporter, UniqueErrorReporter& _errorReporter,
UniqueErrorReporter& _unsupportedErrorReporter, UniqueErrorReporter& _unsupportedErrorReporter,
map<h256, string> const& _smtlib2Responses, std::map<h256, std::string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback, ReadCallback::Callback const& _smtCallback,
ModelCheckerSettings _settings, ModelCheckerSettings _settings,
CharStreamProvider const& _charStreamProvider CharStreamProvider const& _charStreamProvider
): ):
SMTEncoder(_context, _settings, _errorReporter, _unsupportedErrorReporter, _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 _smtlib2Responses, _smtCallback, _settings.solvers, _settings.timeout, _settings.printQuery
)) ))
{ {
@ -65,7 +64,7 @@ BMC::BMC(
#endif #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. // At this point every enabled solver is available.
if (!m_settings.solvers.cvc4 && !m_settings.solvers.smtlib2 && !m_settings.solvers.z3) if (!m_settings.solvers.cvc4 && !m_settings.solvers.smtlib2 && !m_settings.solvers.z3)
@ -97,7 +96,7 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
2788_error, 2788_error,
{}, {},
"BMC: " + "BMC: " +
to_string(m_unprovedAmt) + std::to_string(m_unprovedAmt) +
" verification condition(s) could not be proved." + " verification condition(s) could not be proved." +
" Enable the model checker option \"show unproved\" to see all of them." + " 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." + " Consider choosing a specific contract to be verified in order to reduce the solving problems." +
@ -108,7 +107,7 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
m_errorReporter.info( m_errorReporter.info(
6002_error, 6002_error,
"BMC: " + "BMC: " +
to_string(m_safeTargets.size()) + std::to_string(m_safeTargets.size()) +
" verification condition(s) proved safe!" + " verification condition(s) proved safe!" +
" Enable the model checker option \"show proved safe\" to see all of them." " Enable the model checker option \"show proved safe\" to see all of them."
); );
@ -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." "BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available."
" None of the installed solvers was enabled." " None of the installed solvers was enabled."
#ifdef HAVE_Z3_DLOPEN #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 #endif
); );
} }
@ -504,11 +503,11 @@ bool BMC::visit(TryStatement const& _tryStatement)
if (_tryStatement.successClause()->parameters()) if (_tryStatement.successClause()->parameters())
expressionToTupleAssignment(_tryStatement.successClause()->parameters()->parameters(), *externalCall); 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(); auto const& clauses = _tryStatement.clauses();
m_context.addAssertion(clauseId >= 0 && clauseId < clauses.size()); m_context.addAssertion(clauseId >= 0 && clauseId < clauses.size());
solAssert(clauses[0].get() == _tryStatement.successClause(), "First clause of TryStatement should be the success clause"); 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) for (size_t i = 0; i < clauses.size(); ++i)
clausesVisitResults.push_back(visitBranch(clauses[i].get())); clausesVisitResults.push_back(visitBranch(clauses[i].get()));
@ -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, Token _op,
smtutil::Expression const& _left, smtutil::Expression const& _left,
smtutil::Expression const& _right, smtutil::Expression const& _right,
@ -800,10 +799,10 @@ void BMC::reset()
m_loopExecutionHappened = false; 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; std::vector<smtutil::Expression> expressionsToEvaluate;
vector<string> expressionNames; std::vector<std::string> expressionNames;
for (auto const& var: m_context.variables()) for (auto const& var: m_context.variables())
if (var.first->type()->isValueType()) if (var.first->type()->isValueType())
{ {
@ -826,7 +825,7 @@ pair<vector<smtutil::Expression>, vector<string>> BMC::modelExpressions()
if (uf->annotation().type->isValueType()) if (uf->annotation().type->isValueType())
{ {
expressionsToEvaluate.emplace_back(expr(*uf)); expressionsToEvaluate.emplace_back(expr(*uf));
string expressionName; std::string expressionName;
if (uf->location().hasText()) if (uf->location().hasText())
expressionName = m_charStreamProvider.charStream(*uf->location().sourceName).text( expressionName = m_charStreamProvider.charStream(*uf->location().sourceName).text(
uf->location() uf->location()
@ -839,7 +838,7 @@ pair<vector<smtutil::Expression>, vector<string>> BMC::modelExpressions()
/// Verification targets. /// Verification targets.
string BMC::targetDescription(BMCVerificationTarget const& _target) std::string BMC::targetDescription(BMCVerificationTarget const& _target)
{ {
if ( if (
_target.type == VerificationTargetType::Underflow || _target.type == VerificationTargetType::Underflow ||
@ -1065,20 +1064,20 @@ void BMC::addVerificationTarget(
void BMC::checkCondition( void BMC::checkCondition(
BMCVerificationTarget const& _target, BMCVerificationTarget const& _target,
smtutil::Expression _condition, smtutil::Expression _condition,
vector<SMTEncoder::CallStackEntry> const& _callStack, std::vector<SMTEncoder::CallStackEntry> const& _callStack,
pair<vector<smtutil::Expression>, vector<string>> const& _modelExpressions, std::pair<std::vector<smtutil::Expression>, std::vector<std::string>> const& _modelExpressions,
SourceLocation const& _location, SourceLocation const& _location,
ErrorId _errorHappens, ErrorId _errorHappens,
ErrorId _errorMightHappen, ErrorId _errorMightHappen,
string const& _additionalValueName, std::string const& _additionalValueName,
smtutil::Expression const* _additionalValue smtutil::Expression const* _additionalValue
) )
{ {
m_interface->push(); m_interface->push();
m_interface->addAssertion(_condition); m_interface->addAssertion(_condition);
vector<smtutil::Expression> expressionsToEvaluate; std::vector<smtutil::Expression> expressionsToEvaluate;
vector<string> expressionNames; std::vector<std::string> expressionNames;
tie(expressionsToEvaluate, expressionNames) = _modelExpressions; tie(expressionsToEvaluate, expressionNames) = _modelExpressions;
if (!_callStack.empty()) if (!_callStack.empty())
if (_additionalValue) if (_additionalValue)
@ -1087,10 +1086,10 @@ void BMC::checkCondition(
expressionNames.push_back(_additionalValueName); expressionNames.push_back(_additionalValueName);
} }
smtutil::CheckResult result; smtutil::CheckResult result;
vector<string> values; std::vector<std::string> values;
tie(result, values) = checkSatisfiableAndGenerateModel(expressionsToEvaluate); tie(result, values) = checkSatisfiableAndGenerateModel(expressionsToEvaluate);
string extraComment = SMTEncoder::extraComment(); std::string extraComment = SMTEncoder::extraComment();
if (m_loopExecutionHappened) if (m_loopExecutionHappened)
extraComment += extraComment +=
"False negatives are possible when unrolling loops.\n" "False negatives are possible when unrolling loops.\n"
@ -1119,7 +1118,7 @@ void BMC::checkCondition(
if (values.size() == expressionNames.size()) if (values.size() == expressionNames.size())
{ {
modelMessage << "Counterexample:\n"; modelMessage << "Counterexample:\n";
map<string, string> sortedModel; std::map<std::string, std::string> sortedModel;
for (size_t i = 0; i < values.size(); ++i) for (size_t i = 0; i < values.size(); ++i)
if (expressionsToEvaluate.at(i).name != values.at(i)) if (expressionsToEvaluate.at(i).name != values.at(i))
sortedModel[expressionNames.at(i)] = values.at(i); sortedModel[expressionNames.at(i)] = values.at(i);
@ -1165,7 +1164,7 @@ void BMC::checkBooleanNotConstant(
Expression const& _condition, Expression const& _condition,
smtutil::Expression const& _constraints, smtutil::Expression const& _constraints,
smtutil::Expression const& _value, 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. // 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)); m_errorReporter.warning(2512_error, _condition.location(), "BMC: Condition unreachable.", SMTEncoder::callStackMessage(_callStack));
else else
{ {
string description; std::string description;
if (positiveResult == smtutil::CheckResult::SATISFIABLE) if (positiveResult == smtutil::CheckResult::SATISFIABLE)
{ {
solAssert(negatedResult == smtutil::CheckResult::UNSATISFIABLE, ""); solAssert(negatedResult == smtutil::CheckResult::UNSATISFIABLE, "");
@ -1219,17 +1218,17 @@ void BMC::checkBooleanNotConstant(
} }
} }
pair<smtutil::CheckResult, vector<string>> std::pair<smtutil::CheckResult, std::vector<std::string>>
BMC::checkSatisfiableAndGenerateModel(vector<smtutil::Expression> const& _expressionsToEvaluate) BMC::checkSatisfiableAndGenerateModel(std::vector<smtutil::Expression> const& _expressionsToEvaluate)
{ {
smtutil::CheckResult result; smtutil::CheckResult result;
vector<string> values; std::vector<std::string> values;
try try
{ {
if (m_settings.printQuery) if (m_settings.printQuery)
{ {
auto portfolio = dynamic_cast<smtutil::SMTPortfolio*>(m_interface.get()); auto portfolio = dynamic_cast<smtutil::SMTPortfolio*>(m_interface.get());
string smtlibCode = portfolio->dumpQuery(_expressionsToEvaluate); std::string smtlibCode = portfolio->dumpQuery(_expressionsToEvaluate);
m_errorReporter.info( m_errorReporter.info(
6240_error, 6240_error,
"BMC: Requested query:\n" + smtlibCode "BMC: Requested query:\n" + smtlibCode
@ -1239,14 +1238,14 @@ BMC::checkSatisfiableAndGenerateModel(vector<smtutil::Expression> const& _expres
} }
catch (smtutil::SolverError const& _e) catch (smtutil::SolverError const& _e)
{ {
string description("BMC: Error querying SMT solver"); std::string description("BMC: Error querying SMT solver");
if (_e.comment()) if (_e.comment())
description += ": " + *_e.comment(); description += ": " + *_e.comment();
m_errorReporter.warning(8140_error, description); m_errorReporter.warning(8140_error, description);
result = smtutil::CheckResult::ERROR; result = smtutil::CheckResult::ERROR;
} }
for (string& value: values) for (std::string& value: values)
{ {
try try
{ {

179
libsolidity/formal/CHC.cpp
View File

@ -51,7 +51,6 @@
#include <charconv> #include <charconv>
#include <queue> #include <queue>
using namespace std;
using namespace solidity; using namespace solidity;
using namespace solidity::util; using namespace solidity::util;
using namespace solidity::langutil; using namespace solidity::langutil;
@ -63,7 +62,7 @@ CHC::CHC(
EncodingContext& _context, EncodingContext& _context,
UniqueErrorReporter& _errorReporter, UniqueErrorReporter& _errorReporter,
UniqueErrorReporter& _unsupportedErrorReporter, UniqueErrorReporter& _unsupportedErrorReporter,
map<util::h256, string> const& _smtlib2Responses, std::map<util::h256, std::string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback, ReadCallback::Callback const& _smtCallback,
ModelCheckerSettings _settings, ModelCheckerSettings _settings,
CharStreamProvider const& _charStreamProvider CharStreamProvider const& _charStreamProvider
@ -130,7 +129,7 @@ void CHC::analyze(SourceUnit const& _source)
); );
} }
vector<string> CHC::unhandledQueries() const std::vector<std::string> CHC::unhandledQueries() const
{ {
if (auto smtlib2 = dynamic_cast<CHCSmtLib2Interface const*>(m_interface.get())) if (auto smtlib2 = dynamic_cast<CHCSmtLib2Interface const*>(m_interface.get()))
return smtlib2->unhandledQueries(); return smtlib2->unhandledQueries();
@ -213,7 +212,7 @@ void CHC::endVisit(ContractDefinition const& _contract)
auto baseConstructor = base->constructor(); auto baseConstructor = base->constructor();
if (baseConstructor && baseArgs.count(base)) if (baseConstructor && baseArgs.count(base))
{ {
vector<ASTPointer<Expression>> const& args = baseArgs.at(base); std::vector<ASTPointer<Expression>> const& args = baseArgs.at(base);
auto const& params = baseConstructor->parameters(); auto const& params = baseConstructor->parameters();
solAssert(params.size() == args.size(), ""); solAssert(params.size() == args.size(), "");
for (unsigned i = 0; i < params.size(); ++i) 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 && currentEqualInitialVarsConstraints(stateVariablesIncludingInheritedAndPrivate(_function));
conj = conj && errorFlag().currentValue() == 0; 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; return false;
} }
@ -433,7 +432,7 @@ bool CHC::visit(WhileStatement const& _while)
solAssert(m_currentFunction, ""); solAssert(m_currentFunction, "");
auto const& functionBody = m_currentFunction->body(); 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 loopHeaderBlock = createBlock(&_while, PredicateType::FunctionBlock, namePrefix + "_header_");
auto loopBodyBlock = createBlock(&_while.body(), PredicateType::FunctionBlock, namePrefix + "_body_"); auto loopBodyBlock = createBlock(&_while.body(), PredicateType::FunctionBlock, namePrefix + "_body_");
auto afterLoopBlock = createBlock(&functionBody, PredicateType::FunctionBlock); auto afterLoopBlock = createBlock(&functionBody, PredicateType::FunctionBlock);
@ -622,8 +621,8 @@ void CHC::endVisit(IndexRangeAccess const& _range)
{ {
createExpr(_range); createExpr(_range);
auto baseArray = dynamic_pointer_cast<SymbolicArrayVariable>(m_context.expression(_range.baseExpression())); auto baseArray = std::dynamic_pointer_cast<SymbolicArrayVariable>(m_context.expression(_range.baseExpression()));
auto sliceArray = dynamic_pointer_cast<SymbolicArrayVariable>(m_context.expression(_range)); auto sliceArray = std::dynamic_pointer_cast<SymbolicArrayVariable>(m_context.expression(_range));
solAssert(baseArray && sliceArray, ""); solAssert(baseArray && sliceArray, "");
auto const& sliceData = ArraySlicePredicate::create(sliceArray->sort(), m_context); 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); state().readStateVars(_contract, address);
m_context.addAssertion(state().state() == state().state(0)); m_context.addAssertion(state().state() == state().state(0));
auto preCallState = vector<smtutil::Expression>{state().state()} + currentStateVariables(_contract); auto preCallState = std::vector<smtutil::Expression>{state().state()} + currentStateVariables(_contract);
state().newState(); state().newState();
for (auto const* var: _contract.stateVariables()) for (auto const* var: _contract.stateVariables())
@ -879,8 +878,8 @@ void CHC::nondetCall(ContractDefinition const& _contract, VariableDeclaration co
&_var, &_var,
m_currentContract m_currentContract
); );
auto postCallState = vector<smtutil::Expression>{state().state()} + currentStateVariables(_contract); auto postCallState = std::vector<smtutil::Expression>{state().state()} + currentStateVariables(_contract);
vector<smtutil::Expression> stateExprs{error, address, state().abi(), state().crypto()}; std::vector<smtutil::Expression> stateExprs{error, address, state().abi(), state().crypto()};
auto nondet = (*m_nondetInterfaces.at(&_contract))(stateExprs + preCallState + postCallState); auto nondet = (*m_nondetInterfaces.at(&_contract))(stateExprs + preCallState + postCallState);
auto nondetCall = callPredicate(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)) if (Expression const* value = valueOption(callOptions))
decreaseBalanceFromOptionsValue(*value); decreaseBalanceFromOptionsValue(*value);
auto preCallState = vector<smtutil::Expression>{state().state()} + currentStateVariables(); auto preCallState = std::vector<smtutil::Expression>{state().state()} + currentStateVariables();
if (!usesStaticCall(_funCall)) if (!usesStaticCall(_funCall))
{ {
@ -962,8 +961,8 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
PredicateType::ExternalCallUntrusted, PredicateType::ExternalCallUntrusted,
&_funCall &_funCall
); );
auto postCallState = vector<smtutil::Expression>{state().state()} + currentStateVariables(); auto postCallState = std::vector<smtutil::Expression>{state().state()} + currentStateVariables();
vector<smtutil::Expression> stateExprs{error, state().thisAddress(), state().abi(), state().crypto()}; std::vector<smtutil::Expression> stateExprs{error, state().thisAddress(), state().abi(), state().crypto()};
auto nondet = (*m_nondetInterfaces.at(m_currentContract))(stateExprs + preCallState + postCallState); auto nondet = (*m_nondetInterfaces.at(m_currentContract))(stateExprs + preCallState + postCallState);
auto nondetCall = callPredicate(stateExprs + preCallState + postCallState); auto nondetCall = callPredicate(stateExprs + preCallState + postCallState);
@ -1076,7 +1075,7 @@ void CHC::makeArrayPopVerificationTarget(FunctionCall const& _arrayPop)
auto memberAccess = dynamic_cast<MemberAccess const*>(cleanExpression(_arrayPop.expression())); auto memberAccess = dynamic_cast<MemberAccess const*>(cleanExpression(_arrayPop.expression()));
solAssert(memberAccess, ""); solAssert(memberAccess, "");
auto symbArray = dynamic_pointer_cast<SymbolicArrayVariable>(m_context.expression(memberAccess->expression())); auto symbArray = std::dynamic_pointer_cast<SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
solAssert(symbArray, ""); solAssert(symbArray, "");
verificationTargetEncountered(&_arrayPop, VerificationTargetType::PopEmptyArray, symbArray->length() <= 0); verificationTargetEncountered(&_arrayPop, VerificationTargetType::PopEmptyArray, symbArray->length() <= 0);
@ -1089,7 +1088,7 @@ void CHC::makeOutOfBoundsVerificationTarget(IndexAccess const& _indexAccess)
auto baseType = _indexAccess.baseExpression().annotation().type; auto baseType = _indexAccess.baseExpression().annotation().type;
optional<smtutil::Expression> length; std::optional<smtutil::Expression> length;
if (smt::isArray(*baseType)) if (smt::isArray(*baseType))
length = dynamic_cast<smt::SymbolicArrayVariable const&>( length = dynamic_cast<smt::SymbolicArrayVariable const&>(
*m_context.expression(_indexAccess.baseExpression()) *m_context.expression(_indexAccess.baseExpression())
@ -1097,7 +1096,7 @@ void CHC::makeOutOfBoundsVerificationTarget(IndexAccess const& _indexAccess)
else if (auto const* type = dynamic_cast<FixedBytesType const*>(baseType)) else if (auto const* type = dynamic_cast<FixedBytesType const*>(baseType))
length = smtutil::Expression(static_cast<size_t>(type->numBytes())); length = smtutil::Expression(static_cast<size_t>(type->numBytes()));
optional<smtutil::Expression> target; std::optional<smtutil::Expression> target;
if ( if (
auto index = _indexAccess.indexExpression(); auto index = _indexAccess.indexExpression();
index && length index && length
@ -1108,7 +1107,7 @@ void CHC::makeOutOfBoundsVerificationTarget(IndexAccess const& _indexAccess)
verificationTargetEncountered(&_indexAccess, VerificationTargetType::OutOfBounds, *target); verificationTargetEncountered(&_indexAccess, VerificationTargetType::OutOfBounds, *target);
} }
pair<smtutil::Expression, smtutil::Expression> CHC::arithmeticOperation( std::pair<smtutil::Expression, smtutil::Expression> CHC::arithmeticOperation(
Token _op, Token _op,
smtutil::Expression const& _left, smtutil::Expression const& _left,
smtutil::Expression const& _right, smtutil::Expression const& _right,
@ -1192,7 +1191,7 @@ void CHC::resetSourceAnalysis()
solAssert(m_settings.solvers.smtlib2 || m_settings.solvers.eld); solAssert(m_settings.solvers.smtlib2 || m_settings.solvers.eld);
if (!m_interface) if (!m_interface)
m_interface = make_unique<CHCSmtLib2Interface>(m_smtlib2Responses, m_smtCallback, m_settings.solvers, m_settings.timeout); m_interface = std::make_unique<CHCSmtLib2Interface>(m_smtlib2Responses, m_smtCallback, m_settings.solvers, m_settings.timeout);
auto smtlib2Interface = dynamic_cast<CHCSmtLib2Interface*>(m_interface.get()); auto smtlib2Interface = dynamic_cast<CHCSmtLib2Interface*>(m_interface.get());
solAssert(smtlib2Interface, ""); solAssert(smtlib2Interface, "");
@ -1249,9 +1248,9 @@ void CHC::setCurrentBlock(Predicate const& _block)
m_currentBlock = predicate(_block); m_currentBlock = predicate(_block);
} }
set<unsigned> CHC::transactionVerificationTargetsIds(ASTNode const* _txRoot) std::set<unsigned> CHC::transactionVerificationTargetsIds(ASTNode const* _txRoot)
{ {
set<unsigned> verificationTargetsIds; std::set<unsigned> verificationTargetsIds;
struct ASTNodeCompare: EncodingContext::IdCompare struct ASTNodeCompare: EncodingContext::IdCompare
{ {
bool operator<(ASTNodeCompare _other) const { return operator()(node, _other.node); } 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; return (function && (function->stateMutability() == StateMutability::Pure || function->stateMutability() == StateMutability::View)) || kind == FunctionType::Kind::BareStaticCall;
} }
optional<CHC::CHCNatspecOption> CHC::natspecOptionFromString(string const& _option) std::optional<CHC::CHCNatspecOption> CHC::natspecOptionFromString(std::string const& _option)
{ {
static map<string, CHCNatspecOption> options{ static std::map<std::string, CHCNatspecOption> options{
{"abstract-function-nondet", CHCNatspecOption::AbstractFunctionNondet} {"abstract-function-nondet", CHCNatspecOption::AbstractFunctionNondet}
}; };
if (options.count(_option)) if (options.count(_option))
@ -1283,15 +1282,15 @@ optional<CHC::CHCNatspecOption> CHC::natspecOptionFromString(string const& _opti
return {}; return {};
} }
set<CHC::CHCNatspecOption> CHC::smtNatspecTags(FunctionDefinition const& _function) std::set<CHC::CHCNatspecOption> CHC::smtNatspecTags(FunctionDefinition const& _function)
{ {
set<CHC::CHCNatspecOption> options; std::set<CHC::CHCNatspecOption> options;
string smtStr = "custom:smtchecker"; std::string smtStr = "custom:smtchecker";
bool errorSeen = false; bool errorSeen = false;
for (auto const& [tag, value]: _function.annotation().docTags) for (auto const& [tag, value]: _function.annotation().docTags)
if (tag == smtStr) if (tag == smtStr)
{ {
string const& content = value.content; std::string const& content = value.content;
if (auto option = natspecOptionFromString(content)) if (auto option = natspecOptionFromString(content))
options.insert(*option); options.insert(*option);
else if (!errorSeen) else if (!errorSeen)
@ -1327,7 +1326,7 @@ SortPointer CHC::sort(ASTNode const* _node)
return functionBodySort(*m_currentFunction, m_currentContract, state()); 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); auto const* block = Predicate::create(_sort, _name, _predType, m_context, _node, _contractContext, m_scopes);
m_interface->registerRelation(block->functor()); m_interface->registerRelation(block->functor());
@ -1339,7 +1338,7 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
for (auto const& node: _source.nodes()) for (auto const& node: _source.nodes())
if (auto const* contract = dynamic_cast<ContractDefinition const*>(node.get())) if (auto const* contract = dynamic_cast<ContractDefinition const*>(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_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_nondetInterfaces[contract] = createSymbolicBlock(nondetInterfaceSort(*contract, state()), "nondet_interface_" + uniquePrefix() + "_" + suffix, PredicateType::NondetInterface, contract, contract);
m_constructorSummaries[contract] = createConstructorBlock(*contract, "summary_constructor"); m_constructorSummaries[contract] = createConstructorBlock(*contract, "summary_constructor");
@ -1385,10 +1384,10 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
auto errorPost = errorFlag().increaseIndex(); auto errorPost = errorFlag().increaseIndex();
auto nondetPost = smt::nondetInterface(iface, *contract, m_context, 0, 2); auto nondetPost = smt::nondetInterface(iface, *contract, m_context, 0, 2);
vector<smtutil::Expression> args{errorPost, state().thisAddress(), state().abi(), state().crypto(), state().tx(), state().state(1)}; std::vector<smtutil::Expression> args{errorPost, state().thisAddress(), state().abi(), state().crypto(), state().tx(), state().state(1)};
args += state1 + args += state1 +
applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); }) + applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); }) +
vector<smtutil::Expression>{state().state(2)} + std::vector<smtutil::Expression>{state().state(2)} +
state2 + state2 +
applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 1); }) + applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 1); }) +
applyMap(function->returnParameters(), [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. // block.coinbase, which do not trigger calls into the contract.
// So the only constraint we can add here is that the balance of // So the only constraint we can add here is that the balance of
// the contract grows by at least `msg.value`. // 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")); m_context.addAssertion(k.currentValue() >= state().txMember("msg.value"));
// Assume that address(this).balance cannot overflow. // Assume that address(this).balance cannot overflow.
m_context.addAssertion(smt::symbolicUnknownConstraints(state().balance(state().thisAddress()) + k.currentValue(), TypeProvider::uint256())); 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); 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( auto block = createSymbolicBlock(
sort(_node), 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( return createSymbolicBlock(
constructorSort(_contract, state()), constructorSort(_contract, state()),
@ -1622,7 +1621,7 @@ void CHC::createErrorBlock()
{ {
m_errorPredicate = createSymbolicBlock( m_errorPredicate = createSymbolicBlock(
arity0FunctionSort(), arity0FunctionSort(),
"error_target_" + to_string(m_context.newUniqueId()), "error_target_" + std::to_string(m_context.newUniqueId()),
PredicateType::Error PredicateType::Error
); );
m_interface->registerRelation(m_errorPredicate->functor()); m_interface->registerRelation(m_errorPredicate->functor());
@ -1650,18 +1649,18 @@ smtutil::Expression CHC::initialConstraints(ContractDefinition const& _contract,
return conj; return conj;
} }
vector<smtutil::Expression> CHC::initialStateVariables() std::vector<smtutil::Expression> CHC::initialStateVariables()
{ {
return stateVariablesAtIndex(0); return stateVariablesAtIndex(0);
} }
vector<smtutil::Expression> CHC::stateVariablesAtIndex(unsigned _index) std::vector<smtutil::Expression> CHC::stateVariablesAtIndex(unsigned _index)
{ {
solAssert(m_currentContract, ""); solAssert(m_currentContract, "");
return stateVariablesAtIndex(_index, *m_currentContract); return stateVariablesAtIndex(_index, *m_currentContract);
} }
vector<smtutil::Expression> CHC::stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract) std::vector<smtutil::Expression> CHC::stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract)
{ {
return applyMap( return applyMap(
SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract), SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract),
@ -1669,27 +1668,27 @@ vector<smtutil::Expression> CHC::stateVariablesAtIndex(unsigned _index, Contract
); );
} }
vector<smtutil::Expression> CHC::currentStateVariables() std::vector<smtutil::Expression> CHC::currentStateVariables()
{ {
solAssert(m_currentContract, ""); solAssert(m_currentContract, "");
return currentStateVariables(*m_currentContract); return currentStateVariables(*m_currentContract);
} }
vector<smtutil::Expression> CHC::currentStateVariables(ContractDefinition const& _contract) std::vector<smtutil::Expression> CHC::currentStateVariables(ContractDefinition const& _contract)
{ {
return applyMap(SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract), [this](auto _var) { return currentValue(*_var); }); return applyMap(SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract), [this](auto _var) { return currentValue(*_var); });
} }
smtutil::Expression CHC::currentEqualInitialVarsConstraints(vector<VariableDeclaration const*> const& _vars) const smtutil::Expression CHC::currentEqualInitialVarsConstraints(std::vector<VariableDeclaration const*> const& _vars) const
{ {
return fold(_vars, smtutil::Expression(true), [this](auto&& _conj, auto _var) { return fold(_vars, smtutil::Expression(true), [this](auto&& _conj, auto _var) {
return std::move(_conj) && currentValue(*_var) == m_context.variable(*_var)->valueAtIndex(0); 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<FunctionDefinition const*>(_node)) if (auto funDef = dynamic_cast<FunctionDefinition const*>(_node))
{ {
prefix += TokenTraits::toString(funDef->kind()); prefix += TokenTraits::toString(funDef->kind());
@ -1701,7 +1700,7 @@ string CHC::predicateName(ASTNode const* _node, ContractDefinition const* _contr
auto contract = _contract ? _contract : m_currentContract; auto contract = _contract ? _contract : m_currentContract;
solAssert(contract, ""); 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) smtutil::Expression CHC::predicate(Predicate const& _block)
@ -1756,7 +1755,7 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
solAssert(false, "Unreachable!"); solAssert(false, "Unreachable!");
}; };
errorFlag().increaseIndex(); errorFlag().increaseIndex();
vector<smtutil::Expression> args{errorFlag().currentValue(), contractAddressValue(_funCall), state().abi(), state().crypto(), state().tx(), state().state()}; std::vector<smtutil::Expression> args{errorFlag().currentValue(), contractAddressValue(_funCall), state().abi(), state().crypto(), state().tx(), state().state()};
auto const* contract = function->annotation().contract; auto const* contract = function->annotation().contract;
auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts; auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts;
@ -1773,7 +1772,7 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
for (auto const& var: stateVariablesIncludingInheritedAndPrivate(*contract)) for (auto const& var: stateVariablesIncludingInheritedAndPrivate(*contract))
m_context.variable(*var)->increaseIndex(); m_context.variable(*var)->increaseIndex();
} }
args += vector<smtutil::Expression>{state().state()}; args += std::vector<smtutil::Expression>{state().state()};
args += currentStateVariables(*contract); args += currentStateVariables(*contract);
for (auto var: function->parameters() + function->returnParameters()) for (auto var: function->parameters() + function->returnParameters())
@ -1798,12 +1797,12 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
return callPredicate(args); 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); m_interface->addRule(_rule, _ruleName);
} }
tuple<CheckResult, smtutil::Expression, CHCSolverInterface::CexGraph> CHC::query(smtutil::Expression const& _query, langutil::SourceLocation const& _location) std::tuple<CheckResult, smtutil::Expression, CHCSolverInterface::CexGraph> CHC::query(smtutil::Expression const& _query, langutil::SourceLocation const& _location)
{ {
CheckResult result; CheckResult result;
smtutil::Expression invariant(true); smtutil::Expression invariant(true);
@ -1812,13 +1811,13 @@ tuple<CheckResult, smtutil::Expression, CHCSolverInterface::CexGraph> CHC::query
{ {
auto smtLibInterface = dynamic_cast<CHCSmtLib2Interface*>(m_interface.get()); auto smtLibInterface = dynamic_cast<CHCSmtLib2Interface*>(m_interface.get());
solAssert(smtLibInterface, "Requested to print queries but CHCSmtLib2Interface not available"); solAssert(smtLibInterface, "Requested to print queries but CHCSmtLib2Interface not available");
string smtLibCode = smtLibInterface->dumpQuery(_query); std::string smtLibCode = smtLibInterface->dumpQuery(_query);
m_errorReporter.info( m_errorReporter.info(
2339_error, 2339_error,
"CHC: Requested query:\n" + smtLibCode "CHC: Requested query:\n" + smtLibCode
); );
} }
tie(result, invariant, cex) = m_interface->query(_query); std::tie(result, invariant, cex) = m_interface->query(_query);
switch (result) switch (result)
{ {
case CheckResult::SATISFIABLE: case CheckResult::SATISFIABLE:
@ -1836,7 +1835,7 @@ tuple<CheckResult, smtutil::Expression, CHCSolverInterface::CexGraph> CHC::query
CheckResult resultNoOpt; CheckResult resultNoOpt;
smtutil::Expression invariantNoOpt(true); smtutil::Expression invariantNoOpt(true);
CHCSolverInterface::CexGraph cexNoOpt; CHCSolverInterface::CexGraph cexNoOpt;
tie(resultNoOpt, invariantNoOpt, cexNoOpt) = m_interface->query(_query); std::tie(resultNoOpt, invariantNoOpt, cexNoOpt) = m_interface->query(_query);
if (resultNoOpt == CheckResult::SATISFIABLE) if (resultNoOpt == CheckResult::SATISFIABLE)
cex = std::move(cexNoOpt); cex = std::move(cexNoOpt);
@ -1902,7 +1901,7 @@ void CHC::verificationTargetEncountered(
m_context.addAssertion(errorFlag().currentValue() == previousError); m_context.addAssertion(errorFlag().currentValue() == previousError);
} }
pair<string, ErrorId> CHC::targetDescription(CHCVerificationTarget const& _target) std::pair<std::string, ErrorId> CHC::targetDescription(CHCVerificationTarget const& _target)
{ {
if (_target.type == VerificationTargetType::PopEmptyArray) 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). // 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 // 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. // in its call graph. Each such combination forms a unique verification target.
map<unsigned, vector<CHCQueryPlaceholder>> targetEntryPoints; std::map<unsigned, std::vector<CHCQueryPlaceholder>> targetEntryPoints;
for (auto const& [function, placeholders]: m_queryPlaceholders) for (auto const& [function, placeholders]: m_queryPlaceholders)
{ {
auto functionTargets = transactionVerificationTargetsIds(function); auto functionTargets = transactionVerificationTargetsIds(function);
@ -1959,7 +1958,7 @@ void CHC::checkVerificationTargets()
targetEntryPoints[id].push_back(placeholder); targetEntryPoints[id].push_back(placeholder);
} }
set<unsigned> checkedErrorIds; std::set<unsigned> checkedErrorIds;
for (auto const& [targetId, placeholders]: targetEntryPoints) for (auto const& [targetId, placeholders]: targetEntryPoints)
{ {
auto const& target = m_verificationTargets.at(targetId); auto const& target = m_verificationTargets.at(targetId);
@ -1988,7 +1987,7 @@ void CHC::checkVerificationTargets()
5840_error, 5840_error,
{}, {},
"CHC: " + "CHC: " +
to_string(m_unprovedTargets.size()) + std::to_string(m_unprovedTargets.size()) +
" verification condition(s) could not be proved." + " verification condition(s) could not be proved." +
" Enable the model checker option \"show unproved\" to see all of them." + " 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." + " 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( m_errorReporter.info(
1391_error, 1391_error,
"CHC: " + "CHC: " +
to_string(m_safeTargets.size()) + std::to_string(m_safeTargets.size()) +
" verification condition(s) proved safe!" + " verification condition(s) proved safe!" +
" Enable the model checker option \"show proved safe\" to see all of them." " 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()) if (!m_settings.invariants.invariants.empty())
{ {
string msg; std::string msg;
for (auto pred: m_invariants | ranges::views::keys) for (auto pred: m_invariants | ranges::views::keys)
{ {
ASTNode const* node = pred->programNode(); ASTNode const* node = pred->programNode();
string what; std::string what;
if (auto contract = dynamic_cast<ContractDefinition const*>(node)) if (auto contract = dynamic_cast<ContractDefinition const*>(node))
what = contract->fullyQualifiedName(); what = contract->fullyQualifiedName();
else else
solAssert(false, ""); solAssert(false, "");
string invType; std::string invType;
if (pred->type() == PredicateType::Interface) if (pred->type() == PredicateType::Interface)
invType = "Contract invariant(s)"; invType = "Contract invariant(s)";
else if (pred->type() == PredicateType::NondetInterface) else if (pred->type() == PredicateType::NondetInterface)
@ -2038,16 +2037,16 @@ void CHC::checkVerificationTargets()
for (auto const& inv: m_invariants.at(pred)) for (auto const& inv: m_invariants.at(pred))
msg += inv + "\n"; msg += inv + "\n";
} }
if (msg.find("<errorCode>") != string::npos) if (msg.find("<errorCode>") != std::string::npos)
{ {
set<unsigned> seenErrors; std::set<unsigned> seenErrors;
msg += "<errorCode> = 0 -> no errors\n"; msg += "<errorCode> = 0 -> no errors\n";
for (auto const& [id, target]: m_verificationTargets) for (auto const& [id, target]: m_verificationTargets)
if (!seenErrors.count(target.errorId)) if (!seenErrors.count(target.errorId))
{ {
seenErrors.insert(target.errorId); seenErrors.insert(target.errorId);
string loc = string(m_charStreamProvider.charStream(*target.errorNode->location().sourceName).text(target.errorNode->location())); std::string loc = std::string(m_charStreamProvider.charStream(*target.errorNode->location().sourceName).text(target.errorNode->location()));
msg += "<errorCode> = " + to_string(target.errorId) + " -> " + ModelCheckerTargets::targetTypeToString.at(target.type) + " at " + loc + "\n"; msg += "<errorCode> = " + 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. // 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 // 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. // must still be reported safe by the BMC engine.
set<unsigned> allErrorIds; std::set<unsigned> allErrorIds;
for (auto const& entry: m_functionTargetIds) for (auto const& entry: m_functionTargetIds)
for (unsigned id: entry.second) for (unsigned id: entry.second)
allErrorIds.insert(id); allErrorIds.insert(id);
set<unsigned> unreachableErrorIds; std::set<unsigned> unreachableErrorIds;
set_difference( set_difference(
allErrorIds.begin(), allErrorIds.begin(),
allErrorIds.end(), allErrorIds.end(),
@ -2077,10 +2076,10 @@ void CHC::checkVerificationTargets()
void CHC::checkAndReportTarget( void CHC::checkAndReportTarget(
CHCVerificationTarget const& _target, CHCVerificationTarget const& _target,
vector<CHCQueryPlaceholder> const& _placeholders, std::vector<CHCQueryPlaceholder> const& _placeholders,
ErrorId _errorReporterId, ErrorId _errorReporterId,
string _satMsg, std::string _satMsg,
string _unknownMsg std::string _unknownMsg
) )
{ {
if (m_unsafeTargets.count(_target.errorNode) && m_unsafeTargets.at(_target.errorNode).count(_target.type)) 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) if (result == CheckResult::UNSATISFIABLE)
{ {
m_safeTargets[_target.errorNode].insert(_target); m_safeTargets[_target.errorNode].insert(_target);
set<Predicate const*> predicates; std::set<Predicate const*> predicates;
for (auto const* pred: m_interfaces | ranges::views::values) for (auto const* pred: m_interfaces | ranges::views::values)
predicates.insert(pred); predicates.insert(pred);
for (auto const* pred: m_nondetInterfaces | ranges::views::values) for (auto const* pred: m_nondetInterfaces | ranges::views::values)
predicates.insert(pred); predicates.insert(pred);
map<Predicate const*, set<string>> invariants = collectInvariants(invariant, predicates, m_settings.invariants); std::map<Predicate const*, std::set<std::string>> invariants = collectInvariants(invariant, predicates, m_settings.invariants);
for (auto pred: invariants | ranges::views::keys) for (auto pred: invariants | ranges::views::keys)
m_invariants[pred] += std::move(invariants.at(pred)); 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 The first function summary seen contains the values for the state, input and output variables at the
error point. error point.
*/ */
optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const& _graph, string const& _root) std::optional<std::string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const& _graph, std::string const& _root)
{ {
optional<unsigned> rootId; std::optional<unsigned> rootId;
for (auto const& [id, node]: _graph.nodes) for (auto const& [id, node]: _graph.nodes)
if (node.name == _root) if (node.name == _root)
{ {
@ -2165,8 +2164,8 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
if (!rootId) if (!rootId)
return {}; return {};
vector<string> path; std::vector<std::string> path;
string localState; std::string localState;
auto callGraph = summaryCalls(_graph, *rootId); auto callGraph = summaryCalls(_graph, *rootId);
@ -2204,7 +2203,7 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
if (auto outStr = formatVariableModel(outParams, outValues, "\n"); !outStr.empty()) if (auto outStr = formatVariableModel(outParams, outValues, "\n"); !outStr.empty())
localState += outStr + "\n"; localState += outStr + "\n";
optional<unsigned> localErrorId; std::optional<unsigned> localErrorId;
solidity::util::BreadthFirstSearch<unsigned> bfs{{summaryId}}; solidity::util::BreadthFirstSearch<unsigned> bfs{{summaryId}};
bfs.run([&](auto _nodeId, auto&& _addChild) { bfs.run([&](auto _nodeId, auto&& _addChild) {
auto const& children = _graph.edges.at(_nodeId); auto const& children = _graph.edges.at(_nodeId);
@ -2239,9 +2238,9 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
} }
} }
string txCex = summaryPredicate->formatSummaryCall(summaryArgs, m_charStreamProvider); std::string txCex = summaryPredicate->formatSummaryCall(summaryArgs, m_charStreamProvider);
list<string> calls; std::list<std::string> calls;
auto dfs = [&](unsigned parent, unsigned node, unsigned depth, auto&& _dfs) -> void { auto dfs = [&](unsigned parent, unsigned node, unsigned depth, auto&& _dfs) -> void {
auto pred = nodePred(node); auto pred = nodePred(node);
auto parentPred = nodePred(parent); auto parentPred = nodePred(parent);
@ -2254,7 +2253,7 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
bool appendTxVars = pred->isConstructorSummary() || pred->isFunctionSummary() || pred->isExternalCallUntrusted(); 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()) if (pred->isInternalCall())
calls.front() += " -- internal call"; calls.front() += " -- internal call";
else if (pred->isExternalCallTrusted()) else if (pred->isExternalCallTrusted())
@ -2281,12 +2280,12 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
return localState + "\nTransaction trace:\n" + boost::algorithm::join(path | ranges::views::reverse, "\n"); return localState + "\nTransaction trace:\n" + boost::algorithm::join(path | ranges::views::reverse, "\n");
} }
map<unsigned, vector<unsigned>> CHC::summaryCalls(CHCSolverInterface::CexGraph const& _graph, unsigned _root) std::map<unsigned, std::vector<unsigned>> CHC::summaryCalls(CHCSolverInterface::CexGraph const& _graph, unsigned _root)
{ {
map<unsigned, vector<unsigned>> calls; std::map<unsigned, std::vector<unsigned>> calls;
auto compare = [&](unsigned _a, unsigned _b) { 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. // We want to sort sibling predicates in the counterexample graph by their unique predicate id.
// For most predicates, this actually doesn't matter. // For most predicates, this actually doesn't matter.
// The cases where this matters are internal and external function calls which have the form: // The cases where this matters are internal and external function calls which have the form:
@ -2312,7 +2311,7 @@ map<unsigned, vector<unsigned>> CHC::summaryCalls(CHCSolverInterface::CexGraph c
return extract(_graph.nodes.at(_a).name) > extract(_graph.nodes.at(_b).name); return extract(_graph.nodes.at(_a).name) > extract(_graph.nodes.at(_b).name);
}; };
queue<pair<unsigned, unsigned>> q; std::queue<std::pair<unsigned, unsigned>> q;
q.push({_root, _root}); q.push({_root, _root});
while (!q.empty()) while (!q.empty())
{ {
@ -2334,19 +2333,19 @@ map<unsigned, vector<unsigned>> CHC::summaryCalls(CHCSolverInterface::CexGraph c
root = node; root = node;
} }
auto const& edges = _graph.edges.at(node); auto const& edges = _graph.edges.at(node);
for (unsigned v: set<unsigned, decltype(compare)>(begin(edges), end(edges), compare)) for (unsigned v: std::set<unsigned, decltype(compare)>(begin(edges), end(edges), compare))
q.push({v, root}); q.push({v, root});
} }
return calls; 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) { auto pred = [&](CHCSolverInterface::CexNode const& _node) {
vector<string> args = applyMap( std::vector<std::string> args = applyMap(
_node.arguments, _node.arguments,
[&](auto const& arg) { return arg.name; } [&](auto const& arg) { return arg.name; }
); );
@ -2361,14 +2360,14 @@ string CHC::cex2dot(CHCSolverInterface::CexGraph const& _cex)
return dot; 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() unsigned CHC::newErrorId()

21
libsolidity/formal/EncodingContext.cpp
View File

@ -20,7 +20,6 @@
#include <libsolidity/formal/SymbolicTypes.h> #include <libsolidity/formal/SymbolicTypes.h>
using namespace std;
using namespace solidity; using namespace solidity;
using namespace solidity::util; using namespace solidity::util;
using namespace solidity::frontend::smt; using namespace solidity::frontend::smt;
@ -51,7 +50,7 @@ unsigned EncodingContext::newUniqueId()
/// Variables. /// Variables.
shared_ptr<SymbolicVariable> EncodingContext::variable(frontend::VariableDeclaration const& _varDecl) std::shared_ptr<SymbolicVariable> EncodingContext::variable(frontend::VariableDeclaration const& _varDecl)
{ {
solAssert(knownVariable(_varDecl), ""); solAssert(knownVariable(_varDecl), "");
return m_variables[&_varDecl]; return m_variables[&_varDecl];
@ -61,7 +60,7 @@ bool EncodingContext::createVariable(frontend::VariableDeclaration const& _varDe
{ {
solAssert(!knownVariable(_varDecl), ""); solAssert(!knownVariable(_varDecl), "");
auto const& type = _varDecl.type(); 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); m_variables.emplace(&_varDecl, result.second);
return result.first; return result.first;
} }
@ -77,13 +76,13 @@ void EncodingContext::resetVariable(frontend::VariableDeclaration const& _variab
setUnknownValue(_variable); setUnknownValue(_variable);
} }
void EncodingContext::resetVariables(set<frontend::VariableDeclaration const*> const& _variables) void EncodingContext::resetVariables(std::set<frontend::VariableDeclaration const*> const& _variables)
{ {
for (auto const* decl: _variables) for (auto const* decl: _variables)
resetVariable(*decl); resetVariable(*decl);
} }
void EncodingContext::resetVariables(function<bool(frontend::VariableDeclaration const&)> const& _filter) void EncodingContext::resetVariables(std::function<bool(frontend::VariableDeclaration const&)> const& _filter)
{ {
for_each(begin(m_variables), end(m_variables), [&](auto _variable) for_each(begin(m_variables), end(m_variables), [&](auto _variable)
{ {
@ -127,14 +126,14 @@ void EncodingContext::setUnknownValue(SymbolicVariable& _variable)
/// Expressions /// Expressions
shared_ptr<SymbolicVariable> EncodingContext::expression(frontend::Expression const& _e) std::shared_ptr<SymbolicVariable> EncodingContext::expression(frontend::Expression const& _e)
{ {
if (!knownExpression(_e)) if (!knownExpression(_e))
createExpression(_e); createExpression(_e);
return m_expressions.at(&_e); return m_expressions.at(&_e);
} }
bool EncodingContext::createExpression(frontend::Expression const& _e, shared_ptr<SymbolicVariable> _symbVar) bool EncodingContext::createExpression(frontend::Expression const& _e, std::shared_ptr<SymbolicVariable> _symbVar)
{ {
solAssert(_e.annotation().type, ""); solAssert(_e.annotation().type, "");
if (knownExpression(_e)) if (knownExpression(_e))
@ -149,7 +148,7 @@ bool EncodingContext::createExpression(frontend::Expression const& _e, shared_pt
} }
else 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); m_expressions.emplace(&_e, result.second);
return result.first; return result.first;
} }
@ -162,13 +161,13 @@ bool EncodingContext::knownExpression(frontend::Expression const& _e) const
/// Global variables and functions. /// Global variables and functions.
shared_ptr<SymbolicVariable> EncodingContext::globalSymbol(string const& _name) std::shared_ptr<SymbolicVariable> EncodingContext::globalSymbol(std::string const& _name)
{ {
solAssert(knownGlobalSymbol(_name), ""); solAssert(knownGlobalSymbol(_name), "");
return m_globalContext.at(_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), ""); solAssert(!knownGlobalSymbol(_name), "");
auto result = newSymbolicVariable(*_expr.annotation().type, _name, *this); auto result = newSymbolicVariable(*_expr.annotation().type, _name, *this);
@ -177,7 +176,7 @@ bool EncodingContext::createGlobalSymbol(string const& _name, frontend::Expressi
return result.first; return result.first;
} }
bool EncodingContext::knownGlobalSymbol(string const& _var) const bool EncodingContext::knownGlobalSymbol(std::string const& _var) const
{ {
return m_globalContext.count(_var); return m_globalContext.count(_var);
} }

25
libsolidity/formal/ExpressionFormatter.cpp
View File

@ -29,7 +29,6 @@
#include <vector> #include <vector>
#include <string> #include <string>
using namespace std;
using boost::algorithm::starts_with; using boost::algorithm::starts_with;
using namespace solidity; using namespace solidity;
using namespace solidity::util; using namespace solidity::util;
@ -42,7 +41,7 @@ namespace solidity::frontend::smt
namespace namespace
{ {
string formatDatatypeAccessor(smtutil::Expression const& _expr, vector<string> const& _args) std::string formatDatatypeAccessor(smtutil::Expression const& _expr, std::vector<std::string> const& _args)
{ {
auto const& op = _expr.name; auto const& op = _expr.name;
@ -63,9 +62,9 @@ string formatDatatypeAccessor(smtutil::Expression const& _expr, vector<string> c
if (op == "dt_accessor_ecrecover") if (op == "dt_accessor_ecrecover")
return "ecrecover"; return "ecrecover";
string accessorStr = "accessor_"; std::string accessorStr = "accessor_";
// Struct members have suffix "accessor_<memberName>". // Struct members have suffix "accessor_<memberName>".
string type = op.substr(op.rfind(accessorStr) + accessorStr.size()); std::string type = op.substr(op.rfind(accessorStr) + accessorStr.size());
solAssert(_expr.arguments.size() == 1, ""); solAssert(_expr.arguments.size() == 1, "");
if (type == "length") if (type == "length")
@ -87,22 +86,22 @@ string formatDatatypeAccessor(smtutil::Expression const& _expr, vector<string> c
return _args.at(0) + "." + type; return _args.at(0) + "." + type;
} }
string formatGenericOp(smtutil::Expression const& _expr, vector<string> const& _args) std::string formatGenericOp(smtutil::Expression const& _expr, std::vector<std::string> const& _args)
{ {
return _expr.name + "(" + boost::algorithm::join(_args, ", ") + ")"; return _expr.name + "(" + boost::algorithm::join(_args, ", ") + ")";
} }
string formatInfixOp(string const& _op, vector<string> const& _args) std::string formatInfixOp(std::string const& _op, std::vector<std::string> const& _args)
{ {
return "(" + boost::algorithm::join(_args, " " + _op + " ") + ")"; return "(" + boost::algorithm::join(_args, " " + _op + " ") + ")";
} }
string formatArrayOp(smtutil::Expression const& _expr, vector<string> const& _args) std::string formatArrayOp(smtutil::Expression const& _expr, std::vector<std::string> const& _args)
{ {
if (_expr.name == "select") if (_expr.name == "select")
{ {
auto const& a0 = _args.at(0); auto const& a0 = _args.at(0);
static set<string> const ufs{"keccak256", "sha256", "ripemd160", "ecrecover"}; static std::set<std::string> const ufs{"keccak256", "sha256", "ripemd160", "ecrecover"};
if (ufs.count(a0) || starts_with(a0, "t_function_abi")) if (ufs.count(a0) || starts_with(a0, "t_function_abi"))
return _args.at(0) + "(" + _args.at(1) + ")"; return _args.at(0) + "(" + _args.at(1) + ")";
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<string> const& _ar
return formatGenericOp(_expr, _args); return formatGenericOp(_expr, _args);
} }
string formatUnaryOp(smtutil::Expression const& _expr, vector<string> const& _args) std::string formatUnaryOp(smtutil::Expression const& _expr, std::vector<std::string> const& _args)
{ {
if (_expr.name == "not") if (_expr.name == "not")
return "!" + _args.at(0); return "!" + _args.at(0);
@ -122,7 +121,7 @@ string formatUnaryOp(smtutil::Expression const& _expr, vector<string> const& _ar
} }
smtutil::Expression substitute(smtutil::Expression _from, map<string, string> const& _subst) smtutil::Expression substitute(smtutil::Expression _from, std::map<std::string, std::string> const& _subst)
{ {
// TODO For now we ignore nested quantifier expressions, // TODO For now we ignore nested quantifier expressions,
// but we should support them in the future. // but we should support them in the future.
@ -135,7 +134,7 @@ smtutil::Expression substitute(smtutil::Expression _from, map<string, string> co
return _from; return _from;
} }
string toSolidityStr(smtutil::Expression const& _expr) std::string toSolidityStr(smtutil::Expression const& _expr)
{ {
auto const& op = _expr.name; auto const& op = _expr.name;
@ -150,7 +149,7 @@ string toSolidityStr(smtutil::Expression const& _expr)
return formatDatatypeAccessor(_expr, strArgs); return formatDatatypeAccessor(_expr, strArgs);
// Infix operators with format replacements. // Infix operators with format replacements.
static map<string, string> const infixOps{ static std::map<std::string, std::string> const infixOps{
{"and", "&&"}, {"and", "&&"},
{"or", "||"}, {"or", "||"},
{"implies", "=>"}, {"implies", "=>"},
@ -170,7 +169,7 @@ string toSolidityStr(smtutil::Expression const& _expr)
if (infixOps.count(op)) if (infixOps.count(op))
return formatInfixOp(infixOps.at(op), strArgs); return formatInfixOp(infixOps.at(op), strArgs);
static set<string> const arrayOps{"select", "store", "const_array"}; static std::set<std::string> const arrayOps{"select", "store", "const_array"};
if (arrayOps.count(op)) if (arrayOps.count(op))
return formatArrayOp(_expr, strArgs); return formatArrayOp(_expr, strArgs);

13
libsolidity/formal/Invariants.cpp
View File

@ -25,7 +25,6 @@
#include <boost/algorithm/string.hpp> #include <boost/algorithm/string.hpp>
using namespace std;
using boost::algorithm::starts_with; using boost::algorithm::starts_with;
using namespace solidity; using namespace solidity;
using namespace solidity::smtutil; using namespace solidity::smtutil;
@ -34,19 +33,19 @@ using namespace solidity::frontend::smt;
namespace solidity::frontend::smt namespace solidity::frontend::smt
{ {
map<Predicate const*, set<string>> collectInvariants( std::map<Predicate const*, std::set<std::string>> collectInvariants(
smtutil::Expression const& _proof, smtutil::Expression const& _proof,
set<Predicate const*> const& _predicates, std::set<Predicate const*> const& _predicates,
ModelCheckerInvariants const& _invariantsSetting ModelCheckerInvariants const& _invariantsSetting
) )
{ {
set<string> targets; std::set<std::string> targets;
if (_invariantsSetting.has(InvariantType::Contract)) if (_invariantsSetting.has(InvariantType::Contract))
targets.insert("interface_"); targets.insert("interface_");
if (_invariantsSetting.has(InvariantType::Reentrancy)) if (_invariantsSetting.has(InvariantType::Reentrancy))
targets.insert("nondet_interface_"); targets.insert("nondet_interface_");
map<string, pair<smtutil::Expression, smtutil::Expression>> equalities; std::map<std::string, std::pair<smtutil::Expression, smtutil::Expression>> equalities;
// Collect equalities where one of the sides is a predicate we're interested in. // Collect equalities where one of the sides is a predicate we're interested in.
util::BreadthFirstSearch<smtutil::Expression const*>{{&_proof}}.run([&](auto&& _expr, auto&& _addChild) { util::BreadthFirstSearch<smtutil::Expression const*>{{&_proof}}.run([&](auto&& _expr, auto&& _addChild) {
if (_expr->name == "=") if (_expr->name == "=")
@ -63,7 +62,7 @@ map<Predicate const*, set<string>> collectInvariants(
_addChild(&arg); _addChild(&arg);
}); });
map<Predicate const*, set<string>> invariants; std::map<Predicate const*, std::set<std::string>> invariants;
for (auto pred: _predicates) for (auto pred: _predicates)
{ {
auto predName = pred->functor().name; auto predName = pred->functor().name;
@ -74,7 +73,7 @@ map<Predicate const*, set<string>> collectInvariants(
auto const& [predExpr, invExpr] = equalities.at(predName); auto const& [predExpr, invExpr] = equalities.at(predName);
static set<string> const ignore{"true", "false"}; static std::set<std::string> const ignore{"true", "false"};
auto r = substitute(invExpr, pred->expressionSubstitution(predExpr)); auto r = substitute(invExpr, pred->expressionSubstitution(predExpr));
// No point in reporting true/false as invariants. // No point in reporting true/false as invariants.
if (!ignore.count(r.name)) if (!ignore.count(r.name))

21
libsolidity/formal/ModelChecker.cpp
View File

@ -31,7 +31,6 @@
#include <range/v3/algorithm/any_of.hpp> #include <range/v3/algorithm/any_of.hpp>
#include <range/v3/view.hpp> #include <range/v3/view.hpp>
using namespace std;
using namespace solidity; using namespace solidity;
using namespace solidity::util; using namespace solidity::util;
using namespace solidity::langutil; using namespace solidity::langutil;
@ -41,7 +40,7 @@ using namespace solidity::smtutil;
ModelChecker::ModelChecker( ModelChecker::ModelChecker(
ErrorReporter& _errorReporter, ErrorReporter& _errorReporter,
langutil::CharStreamProvider const& _charStreamProvider, langutil::CharStreamProvider const& _charStreamProvider,
map<h256, string> const& _smtlib2Responses, std::map<h256, std::string> const& _smtlib2Responses,
ModelCheckerSettings _settings, ModelCheckerSettings _settings,
ReadCallback::Callback const& _smtCallback ReadCallback::Callback const& _smtCallback
): ):
@ -54,19 +53,19 @@ ModelChecker::ModelChecker(
} }
// TODO This should be removed for 0.9.0. // TODO This should be removed for 0.9.0.
bool ModelChecker::isPragmaPresent(vector<shared_ptr<SourceUnit>> const& _sources) bool ModelChecker::isPragmaPresent(std::vector<std::shared_ptr<SourceUnit>> const& _sources)
{ {
return ranges::any_of(_sources, [](auto _source) { return ranges::any_of(_sources, [](auto _source) {
return _source && _source->annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker); return _source && _source->annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker);
}); });
} }
void ModelChecker::checkRequestedSourcesAndContracts(vector<shared_ptr<SourceUnit>> const& _sources) void ModelChecker::checkRequestedSourcesAndContracts(std::vector<std::shared_ptr<SourceUnit>> const& _sources)
{ {
map<string, set<string>> exist; std::map<std::string, std::set<std::string>> exist;
for (auto const& source: _sources) for (auto const& source: _sources)
for (auto node: source->nodes()) for (auto node: source->nodes())
if (auto contract = dynamic_pointer_cast<ContractDefinition>(node)) if (auto contract = std::dynamic_pointer_cast<ContractDefinition>(node))
exist[contract->sourceUnitName()].insert(contract->name()); exist[contract->sourceUnitName()].insert(contract->name());
// Requested sources // Requested sources
@ -100,7 +99,7 @@ void ModelChecker::analyze(SourceUnit const& _source)
{ {
PragmaDirective const* smtPragma = nullptr; PragmaDirective const* smtPragma = nullptr;
for (auto node: _source.nodes()) for (auto node: _source.nodes())
if (auto pragma = dynamic_pointer_cast<PragmaDirective>(node)) if (auto pragma = std::dynamic_pointer_cast<PragmaDirective>(node))
if ( if (
pragma->literals().size() >= 2 && pragma->literals().size() >= 2 &&
pragma->literals().at(1) == "SMTChecker" pragma->literals().at(1) == "SMTChecker"
@ -125,7 +124,7 @@ void ModelChecker::analyze(SourceUnit const& _source)
if (m_settings.engine.chc) if (m_settings.engine.chc)
m_chc.analyze(_source); m_chc.analyze(_source);
map<ASTNode const*, set<VerificationTargetType>, smt::EncodingContext::IdCompare> solvedTargets; std::map<ASTNode const*, std::set<VerificationTargetType>, smt::EncodingContext::IdCompare> solvedTargets;
for (auto const& [node, targets]: m_chc.safeTargets()) for (auto const& [node, targets]: m_chc.safeTargets())
for (auto const& target: targets) for (auto const& target: targets)
@ -147,7 +146,7 @@ void ModelChecker::analyze(SourceUnit const& _source)
5724_error, 5724_error,
{}, {},
"SMTChecker: " + "SMTChecker: " +
to_string(m_unsupportedErrorReporter.errors().size()) + std::to_string(m_unsupportedErrorReporter.errors().size()) +
" unsupported language feature(s)." " unsupported language feature(s)."
" Enable the model checker option \"show unsupported\" to see all of them." " 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(); m_uniqueErrorReporter.clear();
} }
vector<string> ModelChecker::unhandledQueries() std::vector<std::string> ModelChecker::unhandledQueries()
{ {
return m_bmc.unhandledQueries() + m_chc.unhandledQueries(); return m_bmc.unhandledQueries() + m_chc.unhandledQueries();
} }
@ -212,7 +211,7 @@ SMTSolverChoice ModelChecker::checkRequestedSolvers(SMTSolverChoice _enabled, Er
SourceLocation(), SourceLocation(),
"Solver z3 was selected for SMTChecker but it is not available." "Solver z3 was selected for SMTChecker but it is not available."
#ifdef HAVE_Z3_DLOPEN #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 #endif
); );
} }

33
libsolidity/formal/ModelCheckerSettings.cpp
View File

@ -21,18 +21,17 @@
#include <optional> #include <optional>
#include <range/v3/view.hpp> #include <range/v3/view.hpp>
using namespace std;
using namespace solidity; using namespace solidity;
using namespace solidity::frontend; using namespace solidity::frontend;
map<string, InvariantType> const ModelCheckerInvariants::validInvariants{ std::map<std::string, InvariantType> const ModelCheckerInvariants::validInvariants{
{"contract", InvariantType::Contract}, {"contract", InvariantType::Contract},
{"reentrancy", InvariantType::Reentrancy} {"reentrancy", InvariantType::Reentrancy}
}; };
std::optional<ModelCheckerInvariants> ModelCheckerInvariants::fromString(string const& _invs) std::optional<ModelCheckerInvariants> ModelCheckerInvariants::fromString(std::string const& _invs)
{ {
set<InvariantType> chosenInvs; std::set<InvariantType> chosenInvs;
if (_invs == "default") if (_invs == "default")
{ {
// The default is that no invariants are reported. // The default is that no invariants are reported.
@ -41,7 +40,7 @@ std::optional<ModelCheckerInvariants> ModelCheckerInvariants::fromString(string
for (auto&& v: validInvariants | ranges::views::values) for (auto&& v: validInvariants | ranges::views::values)
chosenInvs.insert(v); chosenInvs.insert(v);
else else
for (auto&& t: _invs | ranges::views::split(',') | ranges::to<vector<string>>()) for (auto&& t: _invs | ranges::views::split(',') | ranges::to<std::vector<std::string>>())
{ {
if (!validInvariants.count(t)) if (!validInvariants.count(t))
return {}; return {};
@ -51,7 +50,7 @@ std::optional<ModelCheckerInvariants> ModelCheckerInvariants::fromString(string
return ModelCheckerInvariants{chosenInvs}; return ModelCheckerInvariants{chosenInvs};
} }
bool ModelCheckerInvariants::setFromString(string const& _inv) bool ModelCheckerInvariants::setFromString(std::string const& _inv)
{ {
if (!validInvariants.count(_inv)) if (!validInvariants.count(_inv))
return false; return false;
@ -60,7 +59,7 @@ bool ModelCheckerInvariants::setFromString(string const& _inv)
} }
using TargetType = VerificationTargetType; using TargetType = VerificationTargetType;
map<string, TargetType> const ModelCheckerTargets::targetStrings{ std::map<std::string, TargetType> const ModelCheckerTargets::targetStrings{
{"constantCondition", TargetType::ConstantCondition}, {"constantCondition", TargetType::ConstantCondition},
{"underflow", TargetType::Underflow}, {"underflow", TargetType::Underflow},
{"overflow", TargetType::Overflow}, {"overflow", TargetType::Overflow},
@ -71,7 +70,7 @@ map<string, TargetType> const ModelCheckerTargets::targetStrings{
{"outOfBounds", TargetType::OutOfBounds} {"outOfBounds", TargetType::OutOfBounds}
}; };
map<TargetType, string> const ModelCheckerTargets::targetTypeToString{ std::map<TargetType, std::string> const ModelCheckerTargets::targetTypeToString{
{TargetType::ConstantCondition, "Constant condition"}, {TargetType::ConstantCondition, "Constant condition"},
{TargetType::Underflow, "Underflow"}, {TargetType::Underflow, "Underflow"},
{TargetType::Overflow, "Overflow"}, {TargetType::Overflow, "Overflow"},
@ -82,9 +81,9 @@ map<TargetType, string> const ModelCheckerTargets::targetTypeToString{
{TargetType::OutOfBounds, "Out of bounds access"} {TargetType::OutOfBounds, "Out of bounds access"}
}; };
std::optional<ModelCheckerTargets> ModelCheckerTargets::fromString(string const& _targets) std::optional<ModelCheckerTargets> ModelCheckerTargets::fromString(std::string const& _targets)
{ {
set<TargetType> chosenTargets; std::set<TargetType> chosenTargets;
if (_targets == "default" || _targets == "all") if (_targets == "default" || _targets == "all")
{ {
bool all = _targets == "all"; bool all = _targets == "all";
@ -96,7 +95,7 @@ std::optional<ModelCheckerTargets> ModelCheckerTargets::fromString(string const&
} }
} }
else else
for (auto&& t: _targets | ranges::views::split(',') | ranges::to<vector<string>>()) for (auto&& t: _targets | ranges::views::split(',') | ranges::to<std::vector<std::string>>())
{ {
if (!targetStrings.count(t)) if (!targetStrings.count(t))
return {}; return {};
@ -106,7 +105,7 @@ std::optional<ModelCheckerTargets> ModelCheckerTargets::fromString(string const&
return ModelCheckerTargets{chosenTargets}; return ModelCheckerTargets{chosenTargets};
} }
bool ModelCheckerTargets::setFromString(string const& _target) bool ModelCheckerTargets::setFromString(std::string const& _target)
{ {
if (!targetStrings.count(_target)) if (!targetStrings.count(_target))
return false; return false;
@ -114,15 +113,15 @@ bool ModelCheckerTargets::setFromString(string const& _target)
return true; return true;
} }
std::optional<ModelCheckerContracts> ModelCheckerContracts::fromString(string const& _contracts) std::optional<ModelCheckerContracts> ModelCheckerContracts::fromString(std::string const& _contracts)
{ {
map<string, set<string>> chosen; std::map<std::string, std::set<std::string>> chosen;
if (_contracts == "default") if (_contracts == "default")
return ModelCheckerContracts::Default(); return ModelCheckerContracts::Default();
for (auto&& sourceContract: _contracts | ranges::views::split(',') | ranges::to<vector<string>>()) for (auto&& sourceContract: _contracts | ranges::views::split(',') | ranges::to<std::vector<std::string>>())
{ {
auto&& names = sourceContract | ranges::views::split(':') | ranges::to<vector<string>>(); auto&& names = sourceContract | ranges::views::split(':') | ranges::to<std::vector<std::string>>();
if (names.size() != 2 || names.at(0).empty() || names.at(1).empty()) if (names.size() != 2 || names.at(0).empty() || names.at(1).empty())
return {}; return {};
chosen[names.at(0)].insert(names.at(1)); chosen[names.at(0)].insert(names.at(1));
@ -131,7 +130,7 @@ std::optional<ModelCheckerContracts> ModelCheckerContracts::fromString(string co
return ModelCheckerContracts{chosen}; return ModelCheckerContracts{chosen};
} }
std::optional<ModelCheckerExtCalls> ModelCheckerExtCalls::fromString(string const& _mode) std::optional<ModelCheckerExtCalls> ModelCheckerExtCalls::fromString(std::string const& _mode)
{ {
if (_mode == "untrusted") if (_mode == "untrusted")
return ModelCheckerExtCalls{Mode::UNTRUSTED}; return ModelCheckerExtCalls{Mode::UNTRUSTED};

107
libsolidity/formal/Predicate.cpp
View File

@ -31,27 +31,26 @@
#include <range/v3/view.hpp> #include <range/v3/view.hpp>
#include <utility> #include <utility>
using namespace std;
using boost::algorithm::starts_with; using boost::algorithm::starts_with;
using namespace solidity; using namespace solidity;
using namespace solidity::smtutil; using namespace solidity::smtutil;
using namespace solidity::frontend; using namespace solidity::frontend;
using namespace solidity::frontend::smt; using namespace solidity::frontend::smt;
map<string, Predicate> Predicate::m_predicates; std::map<std::string, Predicate> Predicate::m_predicates;
Predicate const* Predicate::create( Predicate const* Predicate::create(
SortPointer _sort, SortPointer _sort,
string _name, std::string _name,
PredicateType _type, PredicateType _type,
EncodingContext& _context, EncodingContext& _context,
ASTNode const* _node, ASTNode const* _node,
ContractDefinition const* _contractContext, ContractDefinition const* _contractContext,
vector<ScopeOpener const*> _scopeStack std::vector<ScopeOpener const*> _scopeStack
) )
{ {
smt::SymbolicFunctionVariable predicate{_sort, std::move(_name), _context}; smt::SymbolicFunctionVariable predicate{_sort, std::move(_name), _context};
string functorName = predicate.currentName(); std::string functorName = predicate.currentName();
solAssert(!m_predicates.count(functorName), ""); solAssert(!m_predicates.count(functorName), "");
return &m_predicates.emplace( return &m_predicates.emplace(
std::piecewise_construct, std::piecewise_construct,
@ -65,7 +64,7 @@ Predicate::Predicate(
PredicateType _type, PredicateType _type,
ASTNode const* _node, ASTNode const* _node,
ContractDefinition const* _contractContext, ContractDefinition const* _contractContext,
vector<ScopeOpener const*> _scopeStack std::vector<ScopeOpener const*> _scopeStack
): ):
m_predicate(std::move(_predicate)), m_predicate(std::move(_predicate)),
m_type(_type), 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); return &m_predicates.at(_name);
} }
@ -85,7 +84,7 @@ void Predicate::reset()
m_predicates.clear(); m_predicates.clear();
} }
smtutil::Expression Predicate::operator()(vector<smtutil::Expression> const& _args) const smtutil::Expression Predicate::operator()(std::vector<smtutil::Expression> const& _args) const
{ {
return m_predicate(_args); return m_predicate(_args);
} }
@ -149,12 +148,12 @@ VariableDeclaration const* Predicate::programVariable() const
return dynamic_cast<VariableDeclaration const*>(m_node); return dynamic_cast<VariableDeclaration const*>(m_node);
} }
optional<vector<VariableDeclaration const*>> Predicate::stateVariables() const std::optional<std::vector<VariableDeclaration const*>> Predicate::stateVariables() const
{ {
if (m_contractContext) if (m_contractContext)
return SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*m_contractContext); return SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*m_contractContext);
return nullopt; return std::nullopt;
} }
bool Predicate::isSummary() const bool Predicate::isSummary() const
@ -211,8 +210,8 @@ bool Predicate::isNondetInterface() const
return m_type == PredicateType::NondetInterface; return m_type == PredicateType::NondetInterface;
} }
string Predicate::formatSummaryCall( std::string Predicate::formatSummaryCall(
vector<smtutil::Expression> const& _args, std::vector<smtutil::Expression> const& _args,
langutil::CharStreamProvider const& _charStreamProvider, langutil::CharStreamProvider const& _charStreamProvider,
bool _appendTxVars bool _appendTxVars
) const ) const
@ -225,7 +224,7 @@ string Predicate::formatSummaryCall(
if (auto funCall = programFunctionCall()) if (auto funCall = programFunctionCall())
{ {
if (funCall->location().hasText()) 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 else
return {}; 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). /// 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. /// Here we are interested in preInputVars to format the function call.
string txModel; std::string txModel;
if (_appendTxVars) if (_appendTxVars)
{ {
set<string> txVars; std::set<std::string> txVars;
if (isFunctionSummary()) if (isFunctionSummary())
{ {
solAssert(programFunction(), ""); solAssert(programFunction(), "");
@ -276,7 +275,7 @@ string Predicate::formatSummaryCall(
return true; return true;
} }
set<string> txVars; std::set<std::string> txVars;
} txVarsVisitor; } txVarsVisitor;
if (auto fun = programFunction()) if (auto fun = programFunction())
@ -287,7 +286,7 @@ string Predicate::formatSummaryCall(
// Here we are interested in txData from the summary predicate. // Here we are interested in txData from the summary predicate.
auto txValues = readTxVars(_args.at(4)); auto txValues = readTxVars(_args.at(4));
vector<string> values; std::vector<std::string> values;
for (auto const& _var: txVars) for (auto const& _var: txVars)
if (auto v = txValues.at(_var)) if (auto v = txValues.at(_var))
values.push_back(_var + ": " + *v); values.push_back(_var + ": " + *v);
@ -309,8 +308,8 @@ string Predicate::formatSummaryCall(
solAssert(first >= _args.begin() && first <= _args.end(), ""); solAssert(first >= _args.begin() && first <= _args.end(), "");
solAssert(last >= _args.begin() && last <= _args.end(), ""); solAssert(last >= _args.begin() && last <= _args.end(), "");
auto inTypes = SMTEncoder::replaceUserTypes(FunctionType(*fun).parameterTypes()); auto inTypes = SMTEncoder::replaceUserTypes(FunctionType(*fun).parameterTypes());
vector<optional<string>> functionArgsCex = formatExpressions(vector<smtutil::Expression>(first, last), inTypes); std::vector<std::optional<std::string>> functionArgsCex = formatExpressions(std::vector<smtutil::Expression>(first, last), inTypes);
vector<string> functionArgs; std::vector<std::string> functionArgs;
auto const& params = fun->parameters(); auto const& params = fun->parameters();
solAssert(params.size() == functionArgsCex.size(), ""); solAssert(params.size() == functionArgsCex.size(), "");
@ -320,12 +319,12 @@ string Predicate::formatSummaryCall(
else else
functionArgs.emplace_back(params[i]->name()); functionArgs.emplace_back(params[i]->name());
string fName = fun->isConstructor() ? "constructor" : std::string fName = fun->isConstructor() ? "constructor" :
fun->isFallback() ? "fallback" : fun->isFallback() ? "fallback" :
fun->isReceive() ? "receive" : fun->isReceive() ? "receive" :
fun->name(); fun->name();
string prefix; std::string prefix;
if (fun->isFree()) if (fun->isFree())
prefix = !fun->sourceUnitName().empty() ? (fun->sourceUnitName() + ":") : ""; prefix = !fun->sourceUnitName().empty() ? (fun->sourceUnitName() + ":") : "";
else else
@ -336,7 +335,7 @@ string Predicate::formatSummaryCall(
return prefix + fName + "(" + boost::algorithm::join(functionArgs, ", ") + ")" + txModel; return prefix + fName + "(" + boost::algorithm::join(functionArgs, ", ") + ")" + txModel;
} }
vector<optional<string>> Predicate::summaryStateValues(vector<smtutil::Expression> const& _args) const std::vector<std::optional<std::string>> Predicate::summaryStateValues(std::vector<smtutil::Expression> 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 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). /// 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<optional<string>> Predicate::summaryStateValues(vector<smtutil::Expressio
auto stateVars = stateVariables(); auto stateVars = stateVariables();
solAssert(stateVars.has_value(), ""); solAssert(stateVars.has_value(), "");
vector<smtutil::Expression>::const_iterator stateFirst; std::vector<smtutil::Expression>::const_iterator stateFirst;
vector<smtutil::Expression>::const_iterator stateLast; std::vector<smtutil::Expression>::const_iterator stateLast;
if (auto const* function = programFunction()) if (auto const* function = programFunction())
{ {
stateFirst = _args.begin() + 6 + static_cast<int>(stateVars->size()) + static_cast<int>(function->parameters().size()) + 1; stateFirst = _args.begin() + 6 + static_cast<int>(stateVars->size()) + static_cast<int>(function->parameters().size()) + 1;
@ -364,13 +363,13 @@ vector<optional<string>> Predicate::summaryStateValues(vector<smtutil::Expressio
solAssert(stateFirst >= _args.begin() && stateFirst <= _args.end(), ""); solAssert(stateFirst >= _args.begin() && stateFirst <= _args.end(), "");
solAssert(stateLast >= _args.begin() && stateLast <= _args.end(), ""); solAssert(stateLast >= _args.begin() && stateLast <= _args.end(), "");
vector<smtutil::Expression> stateArgs(stateFirst, stateLast); std::vector<smtutil::Expression> stateArgs(stateFirst, stateLast);
solAssert(stateArgs.size() == stateVars->size(), ""); solAssert(stateArgs.size() == stateVars->size(), "");
auto stateTypes = util::applyMap(*stateVars, [&](auto const& _var) { return _var->type(); }); auto stateTypes = util::applyMap(*stateVars, [&](auto const& _var) { return _var->type(); });
return formatExpressions(stateArgs, stateTypes); return formatExpressions(stateArgs, stateTypes);
} }
vector<optional<string>> Predicate::summaryPostInputValues(vector<smtutil::Expression> const& _args) const std::vector<std::optional<std::string>> Predicate::summaryPostInputValues(std::vector<smtutil::Expression> 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 a function summary predicate is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// Here we are interested in postInputVars. /// Here we are interested in postInputVars.
@ -388,13 +387,13 @@ vector<optional<string>> Predicate::summaryPostInputValues(vector<smtutil::Expre
solAssert(first >= _args.begin() && first <= _args.end(), ""); solAssert(first >= _args.begin() && first <= _args.end(), "");
solAssert(last >= _args.begin() && last <= _args.end(), ""); solAssert(last >= _args.begin() && last <= _args.end(), "");
vector<smtutil::Expression> inValues(first, last); std::vector<smtutil::Expression> inValues(first, last);
solAssert(inValues.size() == inParams.size(), ""); solAssert(inValues.size() == inParams.size(), "");
auto inTypes = SMTEncoder::replaceUserTypes(FunctionType(*function).parameterTypes()); auto inTypes = SMTEncoder::replaceUserTypes(FunctionType(*function).parameterTypes());
return formatExpressions(inValues, inTypes); return formatExpressions(inValues, inTypes);
} }
vector<optional<string>> Predicate::summaryPostOutputValues(vector<smtutil::Expression> const& _args) const std::vector<std::optional<std::string>> Predicate::summaryPostOutputValues(std::vector<smtutil::Expression> 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 a function summary predicate is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// Here we are interested in outputVars. /// Here we are interested in outputVars.
@ -410,13 +409,13 @@ vector<optional<string>> Predicate::summaryPostOutputValues(vector<smtutil::Expr
solAssert(first >= _args.begin() && first <= _args.end(), ""); solAssert(first >= _args.begin() && first <= _args.end(), "");
vector<smtutil::Expression> outValues(first, _args.end()); std::vector<smtutil::Expression> outValues(first, _args.end());
solAssert(outValues.size() == function->returnParameters().size(), ""); solAssert(outValues.size() == function->returnParameters().size(), "");
auto outTypes = SMTEncoder::replaceUserTypes(FunctionType(*function).returnParameterTypes()); auto outTypes = SMTEncoder::replaceUserTypes(FunctionType(*function).returnParameterTypes());
return formatExpressions(outValues, outTypes); return formatExpressions(outValues, outTypes);
} }
pair<vector<optional<string>>, vector<VariableDeclaration const*>> Predicate::localVariableValues(vector<smtutil::Expression> const& _args) const std::pair<std::vector<std::optional<std::string>>, std::vector<VariableDeclaration const*>> Predicate::localVariableValues(std::vector<smtutil::Expression> const& _args) const
{ {
/// The signature of a local block predicate is: /// The signature of a local block predicate is:
/// block(error, this, abiFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars, localVars). /// block(error, this, abiFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars, localVars).
@ -426,7 +425,7 @@ pair<vector<optional<string>>, vector<VariableDeclaration const*>> Predicate::lo
auto const& localVars = SMTEncoder::localVariablesIncludingModifiers(*function, m_contractContext); auto const& localVars = SMTEncoder::localVariablesIncludingModifiers(*function, m_contractContext);
auto first = _args.end() - static_cast<int>(localVars.size()); auto first = _args.end() - static_cast<int>(localVars.size());
vector<smtutil::Expression> outValues(first, _args.end()); std::vector<smtutil::Expression> outValues(first, _args.end());
auto mask = util::applyMap( auto mask = util::applyMap(
localVars, localVars,
@ -442,10 +441,10 @@ pair<vector<optional<string>>, vector<VariableDeclaration const*>> Predicate::lo
return {formatExpressions(outValuesInScope, outTypes), localVarsInScope}; return {formatExpressions(outValuesInScope, outTypes), localVarsInScope};
} }
map<string, string> Predicate::expressionSubstitution(smtutil::Expression const& _predExpr) const std::map<std::string, std::string> Predicate::expressionSubstitution(smtutil::Expression const& _predExpr) const
{ {
map<string, string> subst; std::map<std::string, std::string> subst;
string predName = functor().name; std::string predName = functor().name;
solAssert(contextContract(), ""); solAssert(contextContract(), "");
auto const& stateVars = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*contextContract()); auto const& stateVars = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*contextContract());
@ -486,16 +485,16 @@ map<string, string> Predicate::expressionSubstitution(smtutil::Expression const&
return subst; return subst;
} }
vector<optional<string>> Predicate::formatExpressions(vector<smtutil::Expression> const& _exprs, vector<Type const*> const& _types) const std::vector<std::optional<std::string>> Predicate::formatExpressions(std::vector<smtutil::Expression> const& _exprs, std::vector<Type const*> const& _types) const
{ {
solAssert(_exprs.size() == _types.size(), ""); solAssert(_exprs.size() == _types.size(), "");
vector<optional<string>> strExprs; std::vector<std::optional<std::string>> strExprs;
for (unsigned i = 0; i < _exprs.size(); ++i) for (unsigned i = 0; i < _exprs.size(); ++i)
strExprs.push_back(expressionToString(_exprs.at(i), _types.at(i))); strExprs.push_back(expressionToString(_exprs.at(i), _types.at(i)));
return strExprs; return strExprs;
} }
optional<string> Predicate::expressionToString(smtutil::Expression const& _expr, Type const* _type) const std::optional<std::string> Predicate::expressionToString(smtutil::Expression const& _expr, Type const* _type) const
{ {
if (smt::isNumber(*_type)) if (smt::isNumber(*_type))
{ {
@ -514,10 +513,10 @@ optional<string> Predicate::expressionToString(smtutil::Expression const& _expr,
// For some reason the code below returns "0x" for "0". // For some reason the code below returns "0x" for "0".
return util::toHex(toCompactBigEndian(bigint(_expr.name)), util::HexPrefix::Add, util::HexCase::Lower); 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<string> Predicate::expressionToString(smtutil::Expression const& _expr,
{ {
length = stoul(_expr.arguments.at(1).name); length = stoul(_expr.arguments.at(1).name);
} }
catch(out_of_range const&) catch(std::out_of_range const&)
{ {
return {}; return {};
} }
catch(invalid_argument const&) catch(std::invalid_argument const&)
{ {
return {}; return {};
} }
@ -567,12 +566,12 @@ optional<string> Predicate::expressionToString(smtutil::Expression const& _expr,
return {}; return {};
try try
{ {
vector<string> array(length); std::vector<std::string> array(length);
if (!fillArray(_expr.arguments.at(0), array, arrayType)) if (!fillArray(_expr.arguments.at(0), array, arrayType))
return {}; return {};
return "[" + boost::algorithm::join(array, ", ") + "]"; return "[" + boost::algorithm::join(array, ", ") + "]";
} }
catch (bad_alloc const&) catch (std::bad_alloc const&)
{ {
// Solver gave a concrete array but length is too large. // Solver gave a concrete array but length is too large.
} }
@ -585,10 +584,10 @@ optional<string> Predicate::expressionToString(smtutil::Expression const& _expr,
auto members = structType.structDefinition().members(); auto members = structType.structDefinition().members();
solAssert(tupleSort.components.size() == members.size(), ""); solAssert(tupleSort.components.size() == members.size(), "");
solAssert(_expr.arguments.size() == members.size(), ""); solAssert(_expr.arguments.size() == members.size(), "");
vector<string> elements; std::vector<std::string> elements;
for (unsigned i = 0; i < members.size(); ++i) for (unsigned i = 0; i < members.size(); ++i)
{ {
optional<string> elementStr = expressionToString(_expr.arguments.at(i), members[i]->type()); std::optional<std::string> elementStr = expressionToString(_expr.arguments.at(i), members[i]->type());
elements.push_back(members[i]->name() + (elementStr.has_value() ? ": " + elementStr.value() : "")); elements.push_back(members[i]->name() + (elementStr.has_value() ? ": " + elementStr.value() : ""));
} }
return "{" + boost::algorithm::join(elements, ", ") + "}"; return "{" + boost::algorithm::join(elements, ", ") + "}";
@ -597,13 +596,13 @@ optional<string> Predicate::expressionToString(smtutil::Expression const& _expr,
return {}; return {};
} }
bool Predicate::fillArray(smtutil::Expression const& _expr, vector<string>& _array, ArrayType const& _type) const bool Predicate::fillArray(smtutil::Expression const& _expr, std::vector<std::string>& _array, ArrayType const& _type) const
{ {
// Base case // Base case
if (_expr.name == "const_array") if (_expr.name == "const_array")
{ {
auto length = _array.size(); auto length = _array.size();
optional<string> elemStr = expressionToString(_expr.arguments.at(1), _type.baseType()); std::optional<std::string> elemStr = expressionToString(_expr.arguments.at(1), _type.baseType());
if (!elemStr) if (!elemStr)
return false; return false;
_array.clear(); _array.clear();
@ -616,7 +615,7 @@ bool Predicate::fillArray(smtutil::Expression const& _expr, vector<string>& _arr
{ {
if (!fillArray(_expr.arguments.at(0), _array, _type)) if (!fillArray(_expr.arguments.at(0), _array, _type))
return false; return false;
optional<string> indexStr = expressionToString(_expr.arguments.at(1), TypeProvider::uint256()); std::optional<std::string> indexStr = expressionToString(_expr.arguments.at(1), TypeProvider::uint256());
if (!indexStr) if (!indexStr)
return false; return false;
// Sometimes the solver assigns huge lengths that are not related, // Sometimes the solver assigns huge lengths that are not related,
@ -626,15 +625,15 @@ bool Predicate::fillArray(smtutil::Expression const& _expr, vector<string>& _arr
{ {
index = stoul(*indexStr); index = stoul(*indexStr);
} }
catch (out_of_range const&) catch (std::out_of_range const&)
{ {
return true; return true;
} }
catch (invalid_argument const&) catch (std::invalid_argument const&)
{ {
return true; return true;
} }
optional<string> elemStr = expressionToString(_expr.arguments.at(2), _type.baseType()); std::optional<std::string> elemStr = expressionToString(_expr.arguments.at(2), _type.baseType());
if (!elemStr) if (!elemStr)
return false; return false;
if (index < _array.size()) if (index < _array.size())
@ -652,9 +651,9 @@ bool Predicate::fillArray(smtutil::Expression const& _expr, vector<string>& _arr
solAssert(false, ""); solAssert(false, "");
} }
map<string, optional<string>> Predicate::readTxVars(smtutil::Expression const& _tx) const std::map<std::string, std::optional<std::string>> Predicate::readTxVars(smtutil::Expression const& _tx) const
{ {
map<string, Type const*> const txVars{ std::map<std::string, Type const*> const txVars{
{"block.basefee", TypeProvider::uint256()}, {"block.basefee", TypeProvider::uint256()},
{"block.chainid", TypeProvider::uint256()}, {"block.chainid", TypeProvider::uint256()},
{"block.coinbase", TypeProvider::address()}, {"block.coinbase", TypeProvider::address()},
@ -670,7 +669,7 @@ map<string, optional<string>> Predicate::readTxVars(smtutil::Expression const& _
{"tx.gasprice", TypeProvider::uint256()}, {"tx.gasprice", TypeProvider::uint256()},
{"tx.origin", TypeProvider::address()} {"tx.origin", TypeProvider::address()}
}; };
map<string, optional<string>> vars; std::map<std::string, std::optional<std::string>> vars;
for (auto&& [i, v]: txVars | ranges::views::enumerate) for (auto&& [i, v]: txVars | ranges::views::enumerate)
vars.emplace(v.first, expressionToString(_tx.arguments.at(i), v.second)); vars.emplace(v.first, expressionToString(_tx.arguments.at(i), v.second));
return vars; return vars;

47
libsolidity/formal/PredicateInstance.cpp
View File

@ -21,7 +21,6 @@
#include <libsolidity/formal/EncodingContext.h> #include <libsolidity/formal/EncodingContext.h>
#include <libsolidity/formal/SMTEncoder.h> #include <libsolidity/formal/SMTEncoder.h>
using namespace std;
using namespace solidity::util; using namespace solidity::util;
using namespace solidity::smtutil; using namespace solidity::smtutil;
@ -30,14 +29,14 @@ namespace solidity::frontend::smt
smtutil::Expression interfacePre(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context) smtutil::Expression interfacePre(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context)
{ {
auto& state = _context.state(); auto& state = _context.state();
vector<smtutil::Expression> stateExprs{state.thisAddress(0), state.abi(0), state.crypto(0), state.state(0)}; std::vector<smtutil::Expression> stateExprs{state.thisAddress(0), state.abi(0), state.crypto(0), state.state(0)};
return _pred(stateExprs + initialStateVariables(_contract, _context)); return _pred(stateExprs + initialStateVariables(_contract, _context));
} }
smtutil::Expression interface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context) smtutil::Expression interface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context)
{ {
auto const& state = _context.state(); auto const& state = _context.state();
vector<smtutil::Expression> stateExprs{state.thisAddress(0), state.abi(0), state.crypto(0), state.state()}; std::vector<smtutil::Expression> stateExprs{state.thisAddress(0), state.abi(0), state.crypto(0), state.state()};
return _pred(stateExprs + currentStateVariables(_contract, _context)); return _pred(stateExprs + currentStateVariables(_contract, _context));
} }
@ -49,12 +48,12 @@ smtutil::Expression nondetInterface(
unsigned _postIdx) unsigned _postIdx)
{ {
auto const& state = _context.state(); auto const& state = _context.state();
vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(), state.abi(), state.crypto()}; std::vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(), state.abi(), state.crypto()};
return _pred( return _pred(
stateExprs + stateExprs +
vector<smtutil::Expression>{_context.state().state(_preIdx)} + std::vector<smtutil::Expression>{_context.state().state(_preIdx)} +
stateVariablesAtIndex(_preIdx, _contract, _context) + stateVariablesAtIndex(_preIdx, _contract, _context) +
vector<smtutil::Expression>{_context.state().state(_postIdx)} + std::vector<smtutil::Expression>{_context.state().state(_postIdx)} +
stateVariablesAtIndex(_postIdx, _contract, _context) stateVariablesAtIndex(_postIdx, _contract, _context)
); );
} }
@ -66,7 +65,7 @@ smtutil::Expression constructor(Predicate const& _pred, EncodingContext& _contex
return _pred(currentFunctionVariablesForDefinition(*constructor, &contract, _context)); return _pred(currentFunctionVariablesForDefinition(*constructor, &contract, _context));
auto& state = _context.state(); auto& state = _context.state();
vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state(0), state.state()}; std::vector<smtutil::Expression> 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)); 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)); return _pred(currentFunctionVariablesForCall(*constructor, &contract, _context, _internal));
auto& state = _context.state(); auto& state = _context.state();
vector<smtutil::Expression> 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<smtutil::Expression> 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(); state.newState();
stateExprs += vector<smtutil::Expression>{state.state()}; stateExprs += std::vector<smtutil::Expression>{state.state()};
stateExprs += currentStateVariables(contract, _context); stateExprs += currentStateVariables(contract, _context);
stateExprs += newStateVariables(contract, _context); stateExprs += newStateVariables(contract, _context);
return _pred(stateExprs); return _pred(stateExprs);
@ -117,12 +116,12 @@ smtutil::Expression functionBlock(
/// Helpers /// Helpers
vector<smtutil::Expression> initialStateVariables(ContractDefinition const& _contract, EncodingContext& _context) std::vector<smtutil::Expression> initialStateVariables(ContractDefinition const& _contract, EncodingContext& _context)
{ {
return stateVariablesAtIndex(0, _contract, _context); return stateVariablesAtIndex(0, _contract, _context);
} }
vector<smtutil::Expression> stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract, EncodingContext& _context) std::vector<smtutil::Expression> stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract, EncodingContext& _context)
{ {
return applyMap( return applyMap(
SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract), SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract),
@ -130,7 +129,7 @@ vector<smtutil::Expression> stateVariablesAtIndex(unsigned _index, ContractDefin
); );
} }
vector<smtutil::Expression> currentStateVariables(ContractDefinition const& _contract, EncodingContext& _context) std::vector<smtutil::Expression> currentStateVariables(ContractDefinition const& _contract, EncodingContext& _context)
{ {
return applyMap( return applyMap(
SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract), SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract),
@ -138,7 +137,7 @@ vector<smtutil::Expression> currentStateVariables(ContractDefinition const& _con
); );
} }
vector<smtutil::Expression> newStateVariables(ContractDefinition const& _contract, EncodingContext& _context) std::vector<smtutil::Expression> newStateVariables(ContractDefinition const& _contract, EncodingContext& _context)
{ {
return applyMap( return applyMap(
SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract), SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract),
@ -146,24 +145,24 @@ vector<smtutil::Expression> newStateVariables(ContractDefinition const& _contrac
); );
} }
vector<smtutil::Expression> currentFunctionVariablesForDefinition( std::vector<smtutil::Expression> currentFunctionVariablesForDefinition(
FunctionDefinition const& _function, FunctionDefinition const& _function,
ContractDefinition const* _contract, ContractDefinition const* _contract,
EncodingContext& _context EncodingContext& _context
) )
{ {
auto& state = _context.state(); auto& state = _context.state();
vector<smtutil::Expression> exprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state(0)}; std::vector<smtutil::Expression> 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<smtutil::Expression>{}; exprs += _contract ? initialStateVariables(*_contract, _context) : std::vector<smtutil::Expression>{};
exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->valueAtIndex(0); }); exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->valueAtIndex(0); });
exprs += vector<smtutil::Expression>{state.state()}; exprs += std::vector<smtutil::Expression>{state.state()};
exprs += _contract ? currentStateVariables(*_contract, _context) : vector<smtutil::Expression>{}; exprs += _contract ? currentStateVariables(*_contract, _context) : std::vector<smtutil::Expression>{};
exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); }); exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); });
exprs += applyMap(_function.returnParameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); }); exprs += applyMap(_function.returnParameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); });
return exprs; return exprs;
} }
vector<smtutil::Expression> currentFunctionVariablesForCall( std::vector<smtutil::Expression> currentFunctionVariablesForCall(
FunctionDefinition const& _function, FunctionDefinition const& _function,
ContractDefinition const* _contract, ContractDefinition const* _contract,
EncodingContext& _context, EncodingContext& _context,
@ -171,20 +170,20 @@ vector<smtutil::Expression> currentFunctionVariablesForCall(
) )
{ {
auto& state = _context.state(); auto& state = _context.state();
vector<smtutil::Expression> exprs{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<smtutil::Expression> 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<smtutil::Expression>{}; exprs += _contract ? currentStateVariables(*_contract, _context) : std::vector<smtutil::Expression>{};
exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); }); exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); });
state.newState(); state.newState();
exprs += vector<smtutil::Expression>{state.state()}; exprs += std::vector<smtutil::Expression>{state.state()};
exprs += _contract ? newStateVariables(*_contract, _context) : vector<smtutil::Expression>{}; exprs += _contract ? newStateVariables(*_contract, _context) : std::vector<smtutil::Expression>{};
exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->increaseIndex(); }); exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->increaseIndex(); });
exprs += applyMap(_function.returnParameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); }); exprs += applyMap(_function.returnParameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); });
return exprs; return exprs;
} }
vector<smtutil::Expression> currentBlockVariables(FunctionDefinition const& _function, ContractDefinition const* _contract, EncodingContext& _context) std::vector<smtutil::Expression> currentBlockVariables(FunctionDefinition const& _function, ContractDefinition const* _contract, EncodingContext& _context)
{ {
return currentFunctionVariablesForDefinition(_function, _contract, _context) + return currentFunctionVariablesForDefinition(_function, _contract, _context) +
applyMap( applyMap(

35
libsolidity/formal/PredicateSort.cpp
View File

@ -21,7 +21,6 @@
#include <libsolidity/formal/SMTEncoder.h> #include <libsolidity/formal/SMTEncoder.h>
#include <libsolidity/formal/SymbolicTypes.h> #include <libsolidity/formal/SymbolicTypes.h>
using namespace std;
using namespace solidity::util; using namespace solidity::util;
using namespace solidity::smtutil; using namespace solidity::smtutil;
@ -30,8 +29,8 @@ namespace solidity::frontend::smt
SortPointer interfaceSort(ContractDefinition const& _contract, SymbolicState& _state) SortPointer interfaceSort(ContractDefinition const& _contract, SymbolicState& _state)
{ {
return make_shared<FunctionSort>( return std::make_shared<FunctionSort>(
vector<SortPointer>{_state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.stateSort()} + stateSorts(_contract), std::vector<SortPointer>{_state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.stateSort()} + stateSorts(_contract),
SortProvider::boolSort SortProvider::boolSort
); );
} }
@ -39,9 +38,9 @@ SortPointer interfaceSort(ContractDefinition const& _contract, SymbolicState& _s
SortPointer nondetInterfaceSort(ContractDefinition const& _contract, SymbolicState& _state) SortPointer nondetInterfaceSort(ContractDefinition const& _contract, SymbolicState& _state)
{ {
auto varSorts = stateSorts(_contract); auto varSorts = stateSorts(_contract);
vector<SortPointer> stateSort{_state.stateSort()}; std::vector<SortPointer> stateSort{_state.stateSort()};
return make_shared<FunctionSort>( return std::make_shared<FunctionSort>(
vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort()} + std::vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort()} +
stateSort + stateSort +
varSorts + varSorts +
stateSort + stateSort +
@ -56,9 +55,9 @@ SortPointer constructorSort(ContractDefinition const& _contract, SymbolicState&
return functionSort(*constructor, &_contract, _state); return functionSort(*constructor, &_contract, _state);
auto varSorts = stateSorts(_contract); auto varSorts = stateSorts(_contract);
vector<SortPointer> stateSort{_state.stateSort()}; std::vector<SortPointer> stateSort{_state.stateSort()};
return make_shared<FunctionSort>( return std::make_shared<FunctionSort>(
vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort(), _state.stateSort()} + varSorts + varSorts, std::vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort(), _state.stateSort()} + varSorts + varSorts,
SortProvider::boolSort SortProvider::boolSort
); );
} }
@ -66,14 +65,14 @@ SortPointer constructorSort(ContractDefinition const& _contract, SymbolicState&
SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition const* _contract, SymbolicState& _state) SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition const* _contract, SymbolicState& _state)
{ {
auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); }; auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); };
auto varSorts = _contract ? stateSorts(*_contract) : vector<SortPointer>{}; auto varSorts = _contract ? stateSorts(*_contract) : std::vector<SortPointer>{};
auto inputSorts = applyMap(_function.parameters(), smtSort); auto inputSorts = applyMap(_function.parameters(), smtSort);
auto outputSorts = applyMap(_function.returnParameters(), smtSort); auto outputSorts = applyMap(_function.returnParameters(), smtSort);
return make_shared<FunctionSort>( return std::make_shared<FunctionSort>(
vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort()} + std::vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort()} +
varSorts + varSorts +
inputSorts + inputSorts +
vector<SortPointer>{_state.stateSort()} + std::vector<SortPointer>{_state.stateSort()} +
varSorts + varSorts +
inputSorts + inputSorts +
outputSorts, outputSorts,
@ -83,11 +82,11 @@ SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition
SortPointer functionBodySort(FunctionDefinition const& _function, ContractDefinition const* _contract, SymbolicState& _state) SortPointer functionBodySort(FunctionDefinition const& _function, ContractDefinition const* _contract, SymbolicState& _state)
{ {
auto fSort = dynamic_pointer_cast<FunctionSort>(functionSort(_function, _contract, _state)); auto fSort = std::dynamic_pointer_cast<FunctionSort>(functionSort(_function, _contract, _state));
solAssert(fSort, ""); solAssert(fSort, "");
auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); }; auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); };
return make_shared<FunctionSort>( return std::make_shared<FunctionSort>(
fSort->domain + applyMap(SMTEncoder::localVariablesIncludingModifiers(_function, _contract), smtSort), fSort->domain + applyMap(SMTEncoder::localVariablesIncludingModifiers(_function, _contract), smtSort),
SortProvider::boolSort SortProvider::boolSort
); );
@ -95,15 +94,15 @@ SortPointer functionBodySort(FunctionDefinition const& _function, ContractDefini
SortPointer arity0FunctionSort() SortPointer arity0FunctionSort()
{ {
return make_shared<FunctionSort>( return std::make_shared<FunctionSort>(
vector<SortPointer>(), std::vector<SortPointer>(),
SortProvider::boolSort SortProvider::boolSort
); );
} }
/// Helpers /// Helpers
vector<SortPointer> stateSorts(ContractDefinition const& _contract) std::vector<SortPointer> stateSorts(ContractDefinition const& _contract)
{ {
return applyMap( return applyMap(
SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract), SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract),

184
libsolidity/formal/SMTEncoder.cpp
View File

@ -40,11 +40,11 @@
#include <limits> #include <limits>
#include <deque> #include <deque>
using namespace std;
using namespace solidity; using namespace solidity;
using namespace solidity::util; using namespace solidity::util;
using namespace solidity::langutil; using namespace solidity::langutil;
using namespace solidity::frontend; using namespace solidity::frontend;
using namespace std::string_literals;
SMTEncoder::SMTEncoder( SMTEncoder::SMTEncoder(
smt::EncodingContext& _context, smt::EncodingContext& _context,
@ -72,8 +72,8 @@ bool SMTEncoder::visit(ContractDefinition const& _contract)
for (auto const& node: _contract.subNodes()) for (auto const& node: _contract.subNodes())
if ( if (
!dynamic_pointer_cast<FunctionDefinition>(node) && !std::dynamic_pointer_cast<FunctionDefinition>(node) &&
!dynamic_pointer_cast<VariableDeclaration>(node) !std::dynamic_pointer_cast<VariableDeclaration>(node)
) )
node->accept(*this); node->accept(*this);
@ -198,7 +198,7 @@ void SMTEncoder::inlineModifierInvocation(ModifierInvocation const* _invocation,
solAssert(_invocation, ""); solAssert(_invocation, "");
_invocation->accept(*this); _invocation->accept(*this);
vector<smtutil::Expression> args; std::vector<smtutil::Expression> args;
if (auto const* arguments = _invocation->arguments()) if (auto const* arguments = _invocation->arguments())
{ {
auto const& modifierParams = _definition->parameters(); auto const& modifierParams = _definition->parameters();
@ -314,8 +314,8 @@ bool SMTEncoder::visit(InlineAssembly const& _inlineAsm)
this->operator()(_inlineAsm.operations()); this->operator()(_inlineAsm.operations());
} }
map<yul::Identifier const*, InlineAssemblyAnnotation::ExternalIdentifierInfo> const& externalReferences; std::map<yul::Identifier const*, InlineAssemblyAnnotation::ExternalIdentifierInfo> const& externalReferences;
set<VariableDeclaration const*> assignedVars; std::set<VariableDeclaration const*> assignedVars;
using yul::ASTWalker::operator(); using yul::ASTWalker::operator();
void operator()(yul::Assignment const& _assignment) void operator()(yul::Assignment const& _assignment)
@ -425,14 +425,14 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple)
if (_tuple.isInlineArray()) if (_tuple.isInlineArray())
{ {
// Add constraints for the length and values as it is known. // Add constraints for the length and values as it is known.
auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(_tuple)); auto symbArray = std::dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(_tuple));
solAssert(symbArray, ""); solAssert(symbArray, "");
addArrayLiteralAssertions(*symbArray, applyMap(_tuple.components(), [&](auto const& c) { return expr(*c); })); addArrayLiteralAssertions(*symbArray, applyMap(_tuple.components(), [&](auto const& c) { return expr(*c); }));
} }
else else
{ {
auto values = applyMap(_tuple.components(), [this](auto const& component) -> optional<smtutil::Expression> { auto values = applyMap(_tuple.components(), [this](auto const& component) -> std::optional<smtutil::Expression> {
if (component) if (component)
{ {
if (!m_context.knownExpression(*component)) if (!m_context.knownExpression(*component))
@ -816,19 +816,19 @@ void SMTEncoder::visitABIFunction(FunctionCall const& _funCall)
defineExpr(_funCall, smt::zeroValue(TypeProvider::bytesMemory())); defineExpr(_funCall, smt::zeroValue(TypeProvider::bytesMemory()));
return; return;
} }
vector<smtutil::Expression> symbArgs; std::vector<smtutil::Expression> symbArgs;
for (unsigned i = 0; i < argsActualLength; ++i) for (unsigned i = 0; i < argsActualLength; ++i)
if (args.at(i)) if (args.at(i))
symbArgs.emplace_back(expr(*args.at(i), inTypes.at(i))); symbArgs.emplace_back(expr(*args.at(i), inTypes.at(i)));
optional<smtutil::Expression> arg; std::optional<smtutil::Expression> arg;
if (inTypes.size() == 1) if (inTypes.size() == 1)
arg = expr(*args.at(0), inTypes.at(0)); arg = expr(*args.at(0), inTypes.at(0));
else else
{ {
auto inputSort = dynamic_cast<smtutil::ArraySort&>(*symbFunction.sort).domain; auto inputSort = dynamic_cast<smtutil::ArraySort&>(*symbFunction.sort).domain;
arg = smtutil::Expression::tuple_constructor( arg = smtutil::Expression::tuple_constructor(
smtutil::Expression(make_shared<smtutil::SortSort>(inputSort), ""), smtutil::Expression(std::make_shared<smtutil::SortSort>(inputSort), ""),
symbArgs symbArgs
); );
} }
@ -838,7 +838,7 @@ void SMTEncoder::visitABIFunction(FunctionCall const& _funCall)
defineExpr(_funCall, out); defineExpr(_funCall, out);
else else
{ {
auto symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_funCall)); auto symbTuple = std::dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_funCall));
solAssert(symbTuple, ""); solAssert(symbTuple, "");
solAssert(symbTuple->components().size() == outTypes.size(), ""); solAssert(symbTuple->components().size() == outTypes.size(), "");
solAssert(out.sort->kind == smtutil::Kind::Tuple, ""); solAssert(out.sort->kind == smtutil::Kind::Tuple, "");
@ -854,7 +854,7 @@ void SMTEncoder::visitCryptoFunction(FunctionCall const& _funCall)
auto const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type); auto const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
auto kind = funType.kind(); auto kind = funType.kind();
auto arg0 = expr(*_funCall.arguments().at(0)); auto arg0 = expr(*_funCall.arguments().at(0));
optional<smtutil::Expression> result; std::optional<smtutil::Expression> result;
if (kind == FunctionType::Kind::KECCAK256) if (kind == FunctionType::Kind::KECCAK256)
result = smtutil::Expression::select(state().cryptoFunction("keccak256"), arg0); result = smtutil::Expression::select(state().cryptoFunction("keccak256"), arg0);
else if (kind == FunctionType::Kind::SHA256) else if (kind == FunctionType::Kind::SHA256)
@ -870,7 +870,7 @@ void SMTEncoder::visitCryptoFunction(FunctionCall const& _funCall)
auto arg3 = expr(*_funCall.arguments().at(3)); auto arg3 = expr(*_funCall.arguments().at(3));
auto inputSort = dynamic_cast<smtutil::ArraySort&>(*e.sort).domain; auto inputSort = dynamic_cast<smtutil::ArraySort&>(*e.sort).domain;
auto ecrecoverInput = smtutil::Expression::tuple_constructor( auto ecrecoverInput = smtutil::Expression::tuple_constructor(
smtutil::Expression(make_shared<smtutil::SortSort>(inputSort), ""), smtutil::Expression(std::make_shared<smtutil::SortSort>(inputSort), ""),
{arg0, arg1, arg2, arg3} {arg0, arg1, arg2, arg3}
); );
result = smtutil::Expression::select(e, ecrecoverInput); result = smtutil::Expression::select(e, ecrecoverInput);
@ -883,7 +883,7 @@ void SMTEncoder::visitCryptoFunction(FunctionCall const& _funCall)
void SMTEncoder::visitGasLeft(FunctionCall const& _funCall) void SMTEncoder::visitGasLeft(FunctionCall const& _funCall)
{ {
string gasLeft = "gasleft"; std::string gasLeft = "gasleft";
// We increase the variable index since gasleft changes // We increase the variable index since gasleft changes
// inside a tx. // inside a tx.
defineGlobalVariable(gasLeft, _funCall, true); defineGlobalVariable(gasLeft, _funCall, true);
@ -930,7 +930,7 @@ void SMTEncoder::visitObjectCreation(FunctionCall const& _funCall)
smtutil::Expression arraySize = expr(*args.front()); smtutil::Expression arraySize = expr(*args.front());
setSymbolicUnknownValue(arraySize, TypeProvider::uint256(), m_context); setSymbolicUnknownValue(arraySize, TypeProvider::uint256(), m_context);
auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(_funCall)); auto symbArray = std::dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(_funCall));
solAssert(symbArray, ""); solAssert(symbArray, "");
smt::setSymbolicZeroValue(*symbArray, m_context); smt::setSymbolicZeroValue(*symbArray, m_context);
auto zeroElements = symbArray->elements(); auto zeroElements = symbArray->elements();
@ -1004,9 +1004,9 @@ bool isReturnedFromStructGetter(Type const* _type)
return true; return true;
} }
vector<string> structGetterReturnedMembers(StructType const& _structType) std::vector<std::string> structGetterReturnedMembers(StructType const& _structType)
{ {
vector<string> returnedMembers; std::vector<std::string> returnedMembers;
for (auto const& member: _structType.nativeMembers(nullptr)) for (auto const& member: _structType.nativeMembers(nullptr))
if (isReturnedFromStructGetter(member.type)) if (isReturnedFromStructGetter(member.type))
returnedMembers.push_back(member.name); returnedMembers.push_back(member.name);
@ -1023,7 +1023,7 @@ void SMTEncoder::visitPublicGetter(FunctionCall const& _funCall)
auto paramExpectedTypes = replaceUserTypes(FunctionType(*var).parameterTypes()); auto paramExpectedTypes = replaceUserTypes(FunctionType(*var).parameterTypes());
auto actualArguments = _funCall.arguments(); auto actualArguments = _funCall.arguments();
solAssert(actualArguments.size() == paramExpectedTypes.size(), ""); solAssert(actualArguments.size() == paramExpectedTypes.size(), "");
deque<smtutil::Expression> symbArguments; std::deque<smtutil::Expression> symbArguments;
for (unsigned i = 0; i < paramExpectedTypes.size(); ++i) for (unsigned i = 0; i < paramExpectedTypes.size(); ++i)
symbArguments.push_back(expr(*actualArguments[i], paramExpectedTypes[i])); symbArguments.push_back(expr(*actualArguments[i], paramExpectedTypes[i]));
@ -1063,11 +1063,11 @@ void SMTEncoder::visitPublicGetter(FunctionCall const& _funCall)
case Type::Category::Struct: case Type::Category::Struct:
{ {
solAssert(symbArguments.empty(), ""); solAssert(symbArguments.empty(), "");
smt::SymbolicStructVariable structVar(dynamic_cast<StructType const*>(type), "struct_temp_" + to_string(_funCall.id()), m_context); smt::SymbolicStructVariable structVar(dynamic_cast<StructType const*>(type), "struct_temp_" + std::to_string(_funCall.id()), m_context);
m_context.addAssertion(structVar.currentValue() == currentExpr); m_context.addAssertion(structVar.currentValue() == currentExpr);
auto returnedMembers = structGetterReturnedMembers(dynamic_cast<StructType const&>(*structVar.type())); auto returnedMembers = structGetterReturnedMembers(dynamic_cast<StructType const&>(*structVar.type()));
solAssert(!returnedMembers.empty(), ""); solAssert(!returnedMembers.empty(), "");
auto returnedValues = applyMap(returnedMembers, [&](string const& memberName) -> optional<smtutil::Expression> { return structVar.member(memberName); }); auto returnedValues = applyMap(returnedMembers, [&](std::string const& memberName) -> std::optional<smtutil::Expression> { return structVar.member(memberName); });
defineExpr(_funCall, returnedValues); defineExpr(_funCall, returnedValues);
return; return;
} }
@ -1118,7 +1118,7 @@ void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall)
if (arrayType && arrayType->isByteArrayOrString() && smt::isFixedBytes(*funCallType)) if (arrayType && arrayType->isByteArrayOrString() && smt::isFixedBytes(*funCallType))
{ {
auto array = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(*argument)); auto array = std::dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(*argument));
bytesToFixedBytesAssertions(*array, _funCall); bytesToFixedBytesAssertions(*array, _funCall);
return; return;
} }
@ -1129,8 +1129,8 @@ void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall)
unsigned castSize = funCallType->storageBytes(); unsigned castSize = funCallType->storageBytes();
bool castIsSigned = smt::isNumber(*funCallType) && smt::isSigned(funCallType); bool castIsSigned = smt::isNumber(*funCallType) && smt::isSigned(funCallType);
bool argIsSigned = smt::isNumber(*argType) && smt::isSigned(argType); bool argIsSigned = smt::isNumber(*argType) && smt::isSigned(argType);
optional<smtutil::Expression> symbMin; std::optional<smtutil::Expression> symbMin;
optional<smtutil::Expression> symbMax; std::optional<smtutil::Expression> symbMax;
if (smt::isNumber(*funCallType)) if (smt::isNumber(*funCallType))
{ {
symbMin = smt::minValue(funCallType); symbMin = smt::minValue(funCallType);
@ -1285,7 +1285,7 @@ void SMTEncoder::endVisit(Literal const& _literal)
createExpr(_literal); createExpr(_literal);
// Add constraints for the length and values as it is known. // Add constraints for the length and values as it is known.
auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(_literal)); auto symbArray = std::dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(_literal));
solAssert(symbArray, ""); solAssert(symbArray, "");
addArrayLiteralAssertions( addArrayLiteralAssertions(
@ -1299,7 +1299,7 @@ void SMTEncoder::endVisit(Literal const& _literal)
void SMTEncoder::addArrayLiteralAssertions( void SMTEncoder::addArrayLiteralAssertions(
smt::SymbolicArrayVariable& _symArray, smt::SymbolicArrayVariable& _symArray,
vector<smtutil::Expression> const& _elementValues std::vector<smtutil::Expression> const& _elementValues
) )
{ {
m_context.addAssertion(_symArray.length() == _elementValues.size()); m_context.addAssertion(_symArray.length() == _elementValues.size());
@ -1314,7 +1314,7 @@ void SMTEncoder::bytesToFixedBytesAssertions(
{ {
auto const& fixed = dynamic_cast<FixedBytesType const&>(*_fixedBytes.annotation().type); auto const& fixed = dynamic_cast<FixedBytesType const&>(*_fixedBytes.annotation().type);
auto intType = TypeProvider::uint256(); 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); smt::SymbolicIntVariable k(intType, intType, "k_" + suffix, m_context);
m_context.addAssertion(k.currentValue() == 0); m_context.addAssertion(k.currentValue() == 0);
size_t n = fixed.numBytes(); size_t n = fixed.numBytes();
@ -1333,7 +1333,7 @@ void SMTEncoder::endVisit(Return const& _return)
auto returnParams = m_callStack.back().first->returnParameters(); auto returnParams = m_callStack.back().first->returnParameters();
if (returnParams.size() > 1) if (returnParams.size() > 1)
{ {
auto const& symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(*_return.expression())); auto const& symbTuple = std::dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(*_return.expression()));
solAssert(symbTuple, ""); solAssert(symbTuple, "");
solAssert(symbTuple->components().size() == returnParams.size(), ""); solAssert(symbTuple->components().size() == returnParams.size(), "");
@ -1428,7 +1428,7 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
else if (smt::isNonRecursiveStruct(*exprType)) else if (smt::isNonRecursiveStruct(*exprType))
{ {
memberExpr->accept(*this); memberExpr->accept(*this);
auto const& symbStruct = dynamic_pointer_cast<smt::SymbolicStructVariable>(m_context.expression(*memberExpr)); auto const& symbStruct = std::dynamic_pointer_cast<smt::SymbolicStructVariable>(m_context.expression(*memberExpr));
defineExpr(_memberAccess, symbStruct->member(_memberAccess.memberName())); defineExpr(_memberAccess, symbStruct->member(_memberAccess.memberName()));
return false; return false;
} }
@ -1471,7 +1471,7 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
memberExpr->accept(*this); memberExpr->accept(*this);
if (_memberAccess.memberName() == "length") if (_memberAccess.memberName() == "length")
{ {
auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(*memberExpr)); auto symbArray = std::dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(*memberExpr));
solAssert(symbArray, ""); solAssert(symbArray, "");
defineExpr(_memberAccess, symbArray->length()); defineExpr(_memberAccess, symbArray->length());
m_uninterpretedTerms.insert(&_memberAccess); m_uninterpretedTerms.insert(&_memberAccess);
@ -1554,7 +1554,7 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
return; return;
} }
shared_ptr<smt::SymbolicVariable> array; std::shared_ptr<smt::SymbolicVariable> array;
if (auto const* id = dynamic_cast<Identifier const*>(&_indexAccess.baseExpression())) if (auto const* id = dynamic_cast<Identifier const*>(&_indexAccess.baseExpression()))
{ {
auto varDecl = identifierToVariable(*id); auto varDecl = identifierToVariable(*id);
@ -1570,7 +1570,7 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
array = m_context.expression(_indexAccess.baseExpression()); array = m_context.expression(_indexAccess.baseExpression());
} }
auto arrayVar = dynamic_pointer_cast<smt::SymbolicArrayVariable>(array); auto arrayVar = std::dynamic_pointer_cast<smt::SymbolicArrayVariable>(array);
solAssert(arrayVar, ""); solAssert(arrayVar, "");
Type const* baseType = _indexAccess.baseExpression().annotation().type; 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; Type const* baseType = base.annotation().type;
auto indexExpr = expr(*indexAccess->indexExpression(), keyType(baseType)); auto indexExpr = expr(*indexAccess->indexExpression(), keyType(baseType));
auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(base)); auto symbArray = std::dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(base));
solAssert(symbArray, ""); solAssert(symbArray, "");
toStore = smtutil::Expression::tuple_constructor( toStore = smtutil::Expression::tuple_constructor(
smtutil::Expression(make_shared<smtutil::SortSort>(smt::smtSort(*baseType)), baseType->toString(true)), smtutil::Expression(std::make_shared<smtutil::SortSort>(smt::smtSort(*baseType)), baseType->toString(true)),
{smtutil::Expression::store(symbArray->elements(), indexExpr, toStore), symbArray->length()} {smtutil::Expression::store(symbArray->elements(), indexExpr, toStore), symbArray->length()}
); );
defineExpr(*indexAccess, smtutil::Expression::select( defineExpr(*indexAccess, smtutil::Expression::select(
@ -1650,7 +1650,7 @@ void SMTEncoder::indexOrMemberAssignment(Expression const& _expr, smtutil::Expre
break; break;
} }
auto symbStruct = dynamic_pointer_cast<smt::SymbolicStructVariable>(m_context.expression(base)); auto symbStruct = std::dynamic_pointer_cast<smt::SymbolicStructVariable>(m_context.expression(base));
solAssert(symbStruct, ""); solAssert(symbStruct, "");
symbStruct->assignMember(memberAccess->memberName(), toStore); symbStruct->assignMember(memberAccess->memberName(), toStore);
toStore = symbStruct->currentValue(); toStore = symbStruct->currentValue();
@ -1688,7 +1688,7 @@ void SMTEncoder::arrayPush(FunctionCall const& _funCall)
{ {
auto memberAccess = dynamic_cast<MemberAccess const*>(&_funCall.expression()); auto memberAccess = dynamic_cast<MemberAccess const*>(&_funCall.expression());
solAssert(memberAccess, ""); solAssert(memberAccess, "");
auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(memberAccess->expression())); auto symbArray = std::dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
solAssert(symbArray, ""); solAssert(symbArray, "");
auto oldLength = symbArray->length(); auto oldLength = symbArray->length();
m_context.addAssertion(oldLength >= 0); m_context.addAssertion(oldLength >= 0);
@ -1722,7 +1722,7 @@ void SMTEncoder::arrayPop(FunctionCall const& _funCall)
{ {
auto memberAccess = dynamic_cast<MemberAccess const*>(cleanExpression(_funCall.expression())); auto memberAccess = dynamic_cast<MemberAccess const*>(cleanExpression(_funCall.expression()));
solAssert(memberAccess, ""); solAssert(memberAccess, "");
auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(memberAccess->expression())); auto symbArray = std::dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
solAssert(symbArray, ""); solAssert(symbArray, "");
makeArrayPopVerificationTarget(_funCall); makeArrayPopVerificationTarget(_funCall);
@ -1742,7 +1742,7 @@ void SMTEncoder::arrayPop(FunctionCall const& _funCall)
assignment(memberAccess->expression(), symbArray->currentValue()); 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)) if (!m_context.knownGlobalSymbol(_name))
{ {
@ -1807,7 +1807,7 @@ void SMTEncoder::arithmeticOperation(BinaryOperation const& _op)
} }
} }
pair<smtutil::Expression, smtutil::Expression> SMTEncoder::arithmeticOperation( std::pair<smtutil::Expression, smtutil::Expression> SMTEncoder::arithmeticOperation(
Token _op, Token _op,
smtutil::Expression const& _left, smtutil::Expression const& _left,
smtutil::Expression const& _right, smtutil::Expression const& _right,
@ -1815,7 +1815,7 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::arithmeticOperation(
Expression const& _operation Expression const& _operation
) )
{ {
static set<Token> validOperators{ static std::set<Token> validOperators{
Token::Add, Token::Add,
Token::Sub, Token::Sub,
Token::Mul, Token::Mul,
@ -1862,7 +1862,7 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::arithmeticOperation(
// - RHS is -1 // - RHS is -1
// the result is then -(type.min), which wraps back to type.min // the result is then -(type.min), which wraps back to type.min
smtutil::Expression maxLeft = _left == smt::minValue(*intType); smtutil::Expression maxLeft = _left == smt::minValue(*intType);
smtutil::Expression minusOneRight = _right == numeric_limits<size_t >::max(); smtutil::Expression minusOneRight = _right == std::numeric_limits<size_t >::max();
smtutil::Expression wrap = smtutil::Expression::ite(maxLeft && minusOneRight, smt::minValue(*intType), valueUnbounded); smtutil::Expression wrap = smtutil::Expression::ite(maxLeft && minusOneRight, smt::minValue(*intType), valueUnbounded);
return {wrap, valueUnbounded}; return {wrap, valueUnbounded};
} }
@ -1871,7 +1871,7 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::arithmeticOperation(
auto symbMax = smt::maxValue(*intType); auto symbMax = smt::maxValue(*intType);
smtutil::Expression intValueRange = (0 - symbMin) + symbMax + 1; 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 k(intType, intType, "k_" + suffix, m_context);
smt::SymbolicIntVariable m(intType, intType, "m_" + suffix, m_context); smt::SymbolicIntVariable m(intType, intType, "m_" + suffix, m_context);
@ -1905,7 +1905,7 @@ smtutil::Expression SMTEncoder::bitwiseOperation(
Type const* _commonType Type const* _commonType
) )
{ {
static set<Token> validOperators{ static std::set<Token> validOperators{
Token::BitAnd, Token::BitAnd,
Token::BitOr, Token::BitOr,
Token::BitXor, Token::BitXor,
@ -1921,7 +1921,7 @@ smtutil::Expression SMTEncoder::bitwiseOperation(
auto bvLeft = smtutil::Expression::int2bv(_left, bvSize); auto bvLeft = smtutil::Expression::int2bv(_left, bvSize);
auto bvRight = smtutil::Expression::int2bv(_right, bvSize); auto bvRight = smtutil::Expression::int2bv(_right, bvSize);
optional<smtutil::Expression> result; std::optional<smtutil::Expression> result;
switch (_op) switch (_op)
{ {
case Token::BitAnd: case Token::BitAnd:
@ -1962,10 +1962,10 @@ void SMTEncoder::compareOperation(BinaryOperation const& _op)
smtutil::Expression left(expr(_op.leftExpression(), commonType)); smtutil::Expression left(expr(_op.leftExpression(), commonType));
smtutil::Expression right(expr(_op.rightExpression(), commonType)); smtutil::Expression right(expr(_op.rightExpression(), commonType));
Token op = _op.getOperator(); Token op = _op.getOperator();
shared_ptr<smtutil::Expression> value; std::shared_ptr<smtutil::Expression> value;
if (smt::isNumber(*commonType)) if (smt::isNumber(*commonType))
{ {
value = make_shared<smtutil::Expression>( value = std::make_shared<smtutil::Expression>(
op == Token::Equal ? (left == right) : op == Token::Equal ? (left == right) :
op == Token::NotEqual ? (left != right) : op == Token::NotEqual ? (left != right) :
op == Token::LessThan ? (left < right) : op == Token::LessThan ? (left < right) :
@ -1977,7 +1977,7 @@ void SMTEncoder::compareOperation(BinaryOperation const& _op)
else // Bool else // Bool
{ {
solUnimplementedAssert(smt::isBool(*commonType), "Operation not yet supported"); solUnimplementedAssert(smt::isBool(*commonType), "Operation not yet supported");
value = make_shared<smtutil::Expression>( value = std::make_shared<smtutil::Expression>(
op == Token::Equal ? (left == right) : op == Token::Equal ? (left == right) :
/*op == Token::NotEqual*/ (left != right) /*op == Token::NotEqual*/ (left != right)
); );
@ -2039,7 +2039,7 @@ void SMTEncoder::bitwiseNotOperation(UnaryOperation const& _op)
defineExpr(_op, smtutil::Expression::bv2int(~bvOperand, isSigned)); defineExpr(_op, smtutil::Expression::bv2int(~bvOperand, isSigned));
} }
pair<smtutil::Expression, smtutil::Expression> SMTEncoder::divModWithSlacks( std::pair<smtutil::Expression, smtutil::Expression> SMTEncoder::divModWithSlacks(
smtutil::Expression _left, smtutil::Expression _left,
smtutil::Expression _right, smtutil::Expression _right,
IntegerType const& _type IntegerType const& _type
@ -2049,7 +2049,7 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::divModWithSlacks(
return {_left / _right, _left % _right}; return {_left / _right, _left % _right};
IntegerType const* intType = &_type; 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 dSymb(intType, intType, "d_" + suffix, m_context);
smt::SymbolicIntVariable rSymb(intType, intType, "r_" + suffix, m_context); smt::SymbolicIntVariable rSymb(intType, intType, "r_" + suffix, m_context);
auto d = dSymb.currentValue(); auto d = dSymb.currentValue();
@ -2115,7 +2115,7 @@ void SMTEncoder::assignment(
{ {
auto memberAccess = dynamic_cast<MemberAccess const*>(&funCall->expression()); auto memberAccess = dynamic_cast<MemberAccess const*>(&funCall->expression());
solAssert(memberAccess, ""); solAssert(memberAccess, "");
auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(memberAccess->expression())); auto symbArray = std::dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
solAssert(symbArray, ""); solAssert(symbArray, "");
auto oldLength = symbArray->length(); auto oldLength = symbArray->length();
@ -2190,14 +2190,14 @@ void SMTEncoder::tupleAssignment(Expression const& _left, Expression const& _rig
smtutil::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment) smtutil::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment)
{ {
static map<Token, Token> const compoundToArithmetic{ static std::map<Token, Token> const compoundToArithmetic{
{Token::AssignAdd, Token::Add}, {Token::AssignAdd, Token::Add},
{Token::AssignSub, Token::Sub}, {Token::AssignSub, Token::Sub},
{Token::AssignMul, Token::Mul}, {Token::AssignMul, Token::Mul},
{Token::AssignDiv, Token::Div}, {Token::AssignDiv, Token::Div},
{Token::AssignMod, Token::Mod} {Token::AssignMod, Token::Mod}
}; };
static map<Token, Token> const compoundToBitwise{ static std::map<Token, Token> const compoundToBitwise{
{Token::AssignBitAnd, Token::BitAnd}, {Token::AssignBitAnd, Token::BitAnd},
{Token::AssignBitOr, Token::BitOr}, {Token::AssignBitOr, Token::BitOr},
{Token::AssignBitXor, Token::BitXor}, {Token::AssignBitXor, Token::BitXor},
@ -2228,12 +2228,12 @@ smtutil::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment
return values.first; return values.first;
} }
void SMTEncoder::expressionToTupleAssignment(vector<shared_ptr<VariableDeclaration>> const& _variables, Expression const& _rhs) void SMTEncoder::expressionToTupleAssignment(std::vector<std::shared_ptr<VariableDeclaration>> const& _variables, Expression const& _rhs)
{ {
auto symbolicVar = m_context.expression(_rhs); auto symbolicVar = m_context.expression(_rhs);
if (_variables.size() > 1) if (_variables.size() > 1)
{ {
auto symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(symbolicVar); auto symbTuple = std::dynamic_pointer_cast<smt::SymbolicTupleVariable>(symbolicVar);
solAssert(symbTuple, ""); solAssert(symbTuple, "");
auto const& symbComponents = symbTuple->components(); auto const& symbComponents = symbTuple->components();
solAssert(symbComponents.size() == _variables.size(), ""); solAssert(symbComponents.size() == _variables.size(), "");
@ -2282,7 +2282,7 @@ void SMTEncoder::assignment(smt::SymbolicVariable& _symVar, smtutil::Expression
m_context.addAssertion(_symVar.increaseIndex() == _value); m_context.addAssertion(_symVar.increaseIndex() == _value);
} }
pair<SMTEncoder::VariableIndices, smtutil::Expression> SMTEncoder::visitBranch( std::pair<SMTEncoder::VariableIndices, smtutil::Expression> SMTEncoder::visitBranch(
ASTNode const* _statement, ASTNode const* _statement,
smtutil::Expression _condition smtutil::Expression _condition
) )
@ -2290,7 +2290,7 @@ pair<SMTEncoder::VariableIndices, smtutil::Expression> SMTEncoder::visitBranch(
return visitBranch(_statement, &_condition); return visitBranch(_statement, &_condition);
} }
pair<SMTEncoder::VariableIndices, smtutil::Expression> SMTEncoder::visitBranch( std::pair<SMTEncoder::VariableIndices, smtutil::Expression> SMTEncoder::visitBranch(
ASTNode const* _statement, ASTNode const* _statement,
smtutil::Expression const* _condition smtutil::Expression const* _condition
) )
@ -2307,7 +2307,7 @@ pair<SMTEncoder::VariableIndices, smtutil::Expression> SMTEncoder::visitBranch(
return {indicesAfterBranch, pathConditionOnExit}; return {indicesAfterBranch, pathConditionOnExit};
} }
void SMTEncoder::initializeFunctionCallParameters(CallableDeclaration const& _function, vector<smtutil::Expression> const& _callArgs) void SMTEncoder::initializeFunctionCallParameters(CallableDeclaration const& _function, std::vector<smtutil::Expression> const& _callArgs)
{ {
auto const& funParams = _function.parameters(); auto const& funParams = _function.parameters();
solAssert(funParams.size() == _callArgs.size(), ""); solAssert(funParams.size() == _callArgs.size(), "");
@ -2319,7 +2319,7 @@ void SMTEncoder::initializeFunctionCallParameters(CallableDeclaration const& _fu
m_arrayAssignmentHappened = true; m_arrayAssignmentHappened = true;
} }
vector<VariableDeclaration const*> localVars; std::vector<VariableDeclaration const*> localVars;
if (auto const* fun = dynamic_cast<FunctionDefinition const*>(&_function)) if (auto const* fun = dynamic_cast<FunctionDefinition const*>(&_function))
localVars = localVariablesIncludingModifiers(*fun, m_currentContract); localVars = localVariablesIncludingModifiers(*fun, m_currentContract);
else else
@ -2560,14 +2560,14 @@ void SMTEncoder::defineExpr(Expression const& _e, smtutil::Expression _value)
)); ));
} }
void SMTEncoder::defineExpr(Expression const& _e, vector<optional<smtutil::Expression>> const& _values) void SMTEncoder::defineExpr(Expression const& _e, std::vector<std::optional<smtutil::Expression>> const& _values)
{ {
if (_values.size() == 1 && _values.front()) if (_values.size() == 1 && _values.front())
{ {
defineExpr(_e, *_values.front()); defineExpr(_e, *_values.front());
return; return;
} }
auto const& symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_e)); auto const& symbTuple = std::dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_e));
solAssert(symbTuple, ""); solAssert(symbTuple, "");
symbTuple->increaseIndex(); symbTuple->increaseIndex();
auto const& symbComponents = symbTuple->components(); auto const& symbComponents = symbTuple->components();
@ -2606,7 +2606,7 @@ smtutil::Expression SMTEncoder::currentPathConditions()
return m_pathConditions.back(); return m_pathConditions.back();
} }
SecondarySourceLocation SMTEncoder::callStackMessage(vector<CallStackEntry> const& _callStack) SecondarySourceLocation SMTEncoder::callStackMessage(std::vector<CallStackEntry> const& _callStack)
{ {
SecondarySourceLocation callStackLocation; SecondarySourceLocation callStackLocation;
solAssert(!_callStack.empty(), ""); solAssert(!_callStack.empty(), "");
@ -2617,7 +2617,7 @@ SecondarySourceLocation SMTEncoder::callStackMessage(vector<CallStackEntry> cons
return callStackLocation; return callStackLocation;
} }
pair<CallableDeclaration const*, ASTNode const*> SMTEncoder::popCallStack() std::pair<CallableDeclaration const*, ASTNode const*> SMTEncoder::popCallStack()
{ {
solAssert(!m_callStack.empty(), ""); solAssert(!m_callStack.empty(), "");
auto lastCalled = m_callStack.back(); auto lastCalled = m_callStack.back();
@ -2738,7 +2738,7 @@ TypePointers SMTEncoder::replaceUserTypes(TypePointers const& _types)
}); });
} }
pair<Expression const*, FunctionCallOptions const*> SMTEncoder::functionCallExpression(FunctionCall const& _funCall) std::pair<Expression const*, FunctionCallOptions const*> SMTEncoder::functionCallExpression(FunctionCall const& _funCall)
{ {
Expression const* callExpr = &_funCall.expression(); Expression const* callExpr = &_funCall.expression();
auto const* callOptions = dynamic_cast<FunctionCallOptions const*>(callExpr); auto const* callOptions = dynamic_cast<FunctionCallOptions const*>(callExpr);
@ -2775,9 +2775,9 @@ Expression const* SMTEncoder::cleanExpression(Expression const& _expr)
return expr; return expr;
} }
set<VariableDeclaration const*> SMTEncoder::touchedVariables(ASTNode const& _node) std::set<VariableDeclaration const*> SMTEncoder::touchedVariables(ASTNode const& _node)
{ {
vector<CallableDeclaration const*> callStack; std::vector<CallableDeclaration const*> callStack;
for (auto const& call: m_callStack) for (auto const& call: m_callStack)
callStack.push_back(call.first); callStack.push_back(call.first);
return m_variableUsage.touchedVariables(_node, callStack); 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) if (m_arrayAssignmentHappened)
extra += extra +=
"\nNote that array aliasing is not supported," "\nNote that array aliasing is not supported,"
@ -2921,28 +2921,28 @@ FunctionDefinition const* SMTEncoder::functionCallToDefinition(
return {}; return {};
} }
vector<VariableDeclaration const*> SMTEncoder::stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract) std::vector<VariableDeclaration const*> SMTEncoder::stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract)
{ {
return fold( return fold(
_contract.annotation().linearizedBaseContracts, _contract.annotation().linearizedBaseContracts,
vector<VariableDeclaration const*>{}, std::vector<VariableDeclaration const*>{},
[](auto&& _acc, auto _contract) { return _acc + _contract->stateVariables(); } [](auto&& _acc, auto _contract) { return _acc + _contract->stateVariables(); }
); );
} }
vector<VariableDeclaration const*> SMTEncoder::stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function) std::vector<VariableDeclaration const*> SMTEncoder::stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function)
{ {
if (auto contract = dynamic_cast<ContractDefinition const*>(_function.scope())) if (auto contract = dynamic_cast<ContractDefinition const*>(_function.scope()))
return stateVariablesIncludingInheritedAndPrivate(*contract); return stateVariablesIncludingInheritedAndPrivate(*contract);
return {}; return {};
} }
vector<VariableDeclaration const*> SMTEncoder::localVariablesIncludingModifiers(FunctionDefinition const& _function, ContractDefinition const* _contract) std::vector<VariableDeclaration const*> SMTEncoder::localVariablesIncludingModifiers(FunctionDefinition const& _function, ContractDefinition const* _contract)
{ {
return _function.localVariables() + tryCatchVariables(_function) + modifiersVariables(_function, _contract); return _function.localVariables() + tryCatchVariables(_function) + modifiersVariables(_function, _contract);
} }
vector<VariableDeclaration const*> SMTEncoder::tryCatchVariables(FunctionDefinition const& _function) std::vector<VariableDeclaration const*> SMTEncoder::tryCatchVariables(FunctionDefinition const& _function)
{ {
struct TryCatchVarsVisitor : public ASTConstVisitor struct TryCatchVarsVisitor : public ASTConstVisitor
{ {
@ -2958,23 +2958,23 @@ vector<VariableDeclaration const*> SMTEncoder::tryCatchVariables(FunctionDefinit
return true; return true;
} }
vector<VariableDeclaration const*> vars; std::vector<VariableDeclaration const*> vars;
} tryCatchVarsVisitor; } tryCatchVarsVisitor;
_function.accept(tryCatchVarsVisitor); _function.accept(tryCatchVarsVisitor);
return tryCatchVarsVisitor.vars; return tryCatchVarsVisitor.vars;
} }
vector<VariableDeclaration const*> SMTEncoder::modifiersVariables(FunctionDefinition const& _function, ContractDefinition const* _contract) std::vector<VariableDeclaration const*> SMTEncoder::modifiersVariables(FunctionDefinition const& _function, ContractDefinition const* _contract)
{ {
struct BlockVars: ASTConstVisitor struct BlockVars: ASTConstVisitor
{ {
BlockVars(Block const& _block) { _block.accept(*this); } BlockVars(Block const& _block) { _block.accept(*this); }
void endVisit(VariableDeclaration const& _var) { vars.push_back(&_var); } void endVisit(VariableDeclaration const& _var) { vars.push_back(&_var); }
vector<VariableDeclaration const*> vars; std::vector<VariableDeclaration const*> vars;
}; };
vector<VariableDeclaration const*> vars; std::vector<VariableDeclaration const*> vars;
set<ModifierDefinition const*> visited; std::set<ModifierDefinition const*> visited;
for (auto invok: _function.modifiers()) for (auto invok: _function.modifiers())
{ {
if (!invok) if (!invok)
@ -3007,12 +3007,12 @@ ModifierDefinition const* SMTEncoder::resolveModifierInvocation(ModifierInvocati
return modifier; return modifier;
} }
set<FunctionDefinition const*, ASTNode::CompareByID> const& SMTEncoder::contractFunctions(ContractDefinition const& _contract) std::set<FunctionDefinition const*, ASTNode::CompareByID> const& SMTEncoder::contractFunctions(ContractDefinition const& _contract)
{ {
if (!m_contractFunctions.count(&_contract)) if (!m_contractFunctions.count(&_contract))
{ {
auto const& functions = _contract.definedFunctions(); auto const& functions = _contract.definedFunctions();
set<FunctionDefinition const*, ASTNode::CompareByID> resolvedFunctions(begin(functions), end(functions)); std::set<FunctionDefinition const*, ASTNode::CompareByID> resolvedFunctions(begin(functions), end(functions));
for (auto const* base: _contract.annotation().linearizedBaseContracts) for (auto const* base: _contract.annotation().linearizedBaseContracts)
{ {
if (base == &_contract) if (base == &_contract)
@ -3042,7 +3042,7 @@ set<FunctionDefinition const*, ASTNode::CompareByID> const& SMTEncoder::contract
return m_contractFunctions.at(&_contract); return m_contractFunctions.at(&_contract);
} }
set<FunctionDefinition const*, ASTNode::CompareByID> const& SMTEncoder::contractFunctionsWithoutVirtual(ContractDefinition const& _contract) std::set<FunctionDefinition const*, ASTNode::CompareByID> const& SMTEncoder::contractFunctionsWithoutVirtual(ContractDefinition const& _contract)
{ {
if (!m_contractFunctionsWithoutVirtual.count(&_contract)) if (!m_contractFunctionsWithoutVirtual.count(&_contract))
{ {
@ -3057,9 +3057,9 @@ set<FunctionDefinition const*, ASTNode::CompareByID> const& SMTEncoder::contract
return m_contractFunctionsWithoutVirtual.at(&_contract); return m_contractFunctionsWithoutVirtual.at(&_contract);
} }
map<ContractDefinition const*, vector<ASTPointer<frontend::Expression>>> SMTEncoder::baseArguments(ContractDefinition const& _contract) std::map<ContractDefinition const*, std::vector<ASTPointer<frontend::Expression>>> SMTEncoder::baseArguments(ContractDefinition const& _contract)
{ {
map<ContractDefinition const*, vector<ASTPointer<Expression>>> baseArgs; std::map<ContractDefinition const*, std::vector<ASTPointer<Expression>>> baseArgs;
for (auto contract: _contract.annotation().linearizedBaseContracts) for (auto contract: _contract.annotation().linearizedBaseContracts)
{ {
@ -3104,7 +3104,7 @@ RationalNumberType const* SMTEncoder::isConstant(Expression const& _expr)
return nullptr; return nullptr;
} }
set<FunctionCall const*, ASTCompareByID<FunctionCall>> SMTEncoder::collectABICalls(ASTNode const* _node) std::set<FunctionCall const*, ASTCompareByID<FunctionCall>> SMTEncoder::collectABICalls(ASTNode const* _node)
{ {
struct ABIFunctions: public ASTConstVisitor struct ABIFunctions: public ASTConstVisitor
{ {
@ -3126,15 +3126,15 @@ set<FunctionCall const*, ASTCompareByID<FunctionCall>> SMTEncoder::collectABICal
} }
} }
set<FunctionCall const*, ASTCompareByID<FunctionCall>> abiCalls; std::set<FunctionCall const*, ASTCompareByID<FunctionCall>> abiCalls;
}; };
return ABIFunctions(_node).abiCalls; return ABIFunctions(_node).abiCalls;
} }
set<SourceUnit const*, ASTNode::CompareByID> SMTEncoder::sourceDependencies(SourceUnit const& _source) std::set<SourceUnit const*, ASTNode::CompareByID> SMTEncoder::sourceDependencies(SourceUnit const& _source)
{ {
set<SourceUnit const*, ASTNode::CompareByID> sources; std::set<SourceUnit const*, ASTNode::CompareByID> sources;
sources.insert(&_source); sources.insert(&_source);
for (auto const& source: _source.referencedSourceUnits(true)) for (auto const& source: _source.referencedSourceUnits(true))
sources.insert(source); sources.insert(source);
@ -3150,24 +3150,24 @@ void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall, Contrac
auto const& returnParams = funDef->returnParameters(); auto const& returnParams = funDef->returnParameters();
for (auto param: returnParams) for (auto param: returnParams)
createVariable(*param); createVariable(*param);
auto returnValues = applyMap(returnParams, [this](auto const& param) -> optional<smtutil::Expression> { auto returnValues = applyMap(returnParams, [this](auto const& param) -> std::optional<smtutil::Expression> {
solAssert(param && m_context.knownVariable(*param), ""); solAssert(param && m_context.knownVariable(*param), "");
return currentValue(*param); return currentValue(*param);
}); });
defineExpr(_funCall, returnValues); defineExpr(_funCall, returnValues);
} }
vector<smtutil::Expression> SMTEncoder::symbolicArguments(FunctionCall const& _funCall, ContractDefinition const* _contextContract) std::vector<smtutil::Expression> SMTEncoder::symbolicArguments(FunctionCall const& _funCall, ContractDefinition const* _contextContract)
{ {
auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), _contextContract); auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), _contextContract);
solAssert(funDef, ""); solAssert(funDef, "");
vector<smtutil::Expression> args; std::vector<smtutil::Expression> args;
Expression const* calledExpr = &_funCall.expression(); Expression const* calledExpr = &_funCall.expression();
auto funType = dynamic_cast<FunctionType const*>(calledExpr->annotation().type); auto funType = dynamic_cast<FunctionType const*>(calledExpr->annotation().type);
solAssert(funType, ""); solAssert(funType, "");
vector<ASTPointer<Expression const>> arguments = _funCall.sortedArguments(); std::vector<ASTPointer<Expression const>> arguments = _funCall.sortedArguments();
auto functionParams = funDef->parameters(); auto functionParams = funDef->parameters();
unsigned firstParam = 0; unsigned firstParam = 0;
if (funType->hasBoundFirstArgument()) if (funType->hasBoundFirstArgument())
@ -3204,7 +3204,7 @@ smtutil::Expression SMTEncoder::constantExpr(Expression const& _expr, VariableDe
solAssert(false, ""); solAssert(false, "");
} }
void SMTEncoder::collectFreeFunctions(set<SourceUnit const*, ASTNode::CompareByID> const& _sources) void SMTEncoder::collectFreeFunctions(std::set<SourceUnit const*, ASTNode::CompareByID> const& _sources)
{ {
for (auto source: _sources) for (auto source: _sources)
for (auto node: source->nodes()) for (auto node: source->nodes())
@ -3220,7 +3220,7 @@ void SMTEncoder::collectFreeFunctions(set<SourceUnit const*, ASTNode::CompareByI
m_freeFunctions.insert(function); m_freeFunctions.insert(function);
} }
void SMTEncoder::createFreeConstants(set<SourceUnit const*, ASTNode::CompareByID> const& _sources) void SMTEncoder::createFreeConstants(std::set<SourceUnit const*, ASTNode::CompareByID> const& _sources)
{ {
for (auto source: _sources) for (auto source: _sources)
for (auto node: source->nodes()) for (auto node: source->nodes())

1
libsolidity/formal/SSAVariable.cpp
View File

@ -18,7 +18,6 @@
#include <libsolidity/formal/SSAVariable.h> #include <libsolidity/formal/SSAVariable.h>
using namespace std;
using namespace solidity::frontend; using namespace solidity::frontend;
using namespace solidity::frontend::smt; using namespace solidity::frontend::smt;

93
libsolidity/formal/SymbolicState.cpp
View File

@ -26,42 +26,41 @@
#include <range/v3/view.hpp> #include <range/v3/view.hpp>
using namespace std;
using namespace solidity; using namespace solidity;
using namespace solidity::util; using namespace solidity::util;
using namespace solidity::smtutil; using namespace solidity::smtutil;
using namespace solidity::frontend::smt; using namespace solidity::frontend::smt;
BlockchainVariable::BlockchainVariable( BlockchainVariable::BlockchainVariable(
string _name, std::string _name,
map<string, smtutil::SortPointer> _members, std::map<std::string, smtutil::SortPointer> _members,
EncodingContext& _context EncodingContext& _context
): ):
m_name(std::move(_name)), m_name(std::move(_name)),
m_members(std::move(_members)), m_members(std::move(_members)),
m_context(_context) m_context(_context)
{ {
vector<string> members; std::vector<std::string> members;
vector<SortPointer> sorts; std::vector<SortPointer> sorts;
for (auto const& [component, sort]: m_members) for (auto const& [component, sort]: m_members)
{ {
members.emplace_back(component); members.emplace_back(component);
sorts.emplace_back(sort); sorts.emplace_back(sort);
m_componentIndices[component] = static_cast<unsigned>(members.size() - 1); m_componentIndices[component] = static_cast<unsigned>(members.size() - 1);
} }
m_tuple = make_unique<SymbolicTupleVariable>( m_tuple = std::make_unique<SymbolicTupleVariable>(
make_shared<smtutil::TupleSort>(m_name + "_type", members, sorts), std::make_shared<smtutil::TupleSort>(m_name + "_type", members, sorts),
m_name, m_name,
m_context 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)); 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}}); smtutil::Expression newTuple = smt::assignMember(m_tuple->currentValue(), {{_member, _value}});
m_context.addAssertion(m_tuple->increaseIndex() == newTuple); m_context.addAssertion(m_tuple->increaseIndex() == newTuple);
@ -104,9 +103,9 @@ smtutil::Expression SymbolicState::blockhash(smtutil::Expression _blockNumber) c
void SymbolicState::newBalances() void SymbolicState::newBalances()
{ {
auto tupleSort = dynamic_pointer_cast<TupleSort>(stateSort()); auto tupleSort = std::dynamic_pointer_cast<TupleSort>(stateSort());
auto balanceSort = tupleSort->components.at(tupleSort->memberToIndex.at("balances")); 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()); m_state->assignMember("balances", newBalances.currentValue());
} }
@ -158,7 +157,7 @@ void SymbolicState::newStorage()
{ {
auto newStorageVar = SymbolicTupleVariable( auto newStorageVar = SymbolicTupleVariable(
m_state->member("storage").sort, m_state->member("storage").sort,
"havoc_storage_" + to_string(m_context.newUniqueId()), "havoc_storage_" + std::to_string(m_context.newUniqueId()),
m_context m_context
); );
m_state->assignMember("storage", newStorageVar.currentValue()); m_state->assignMember("storage", newStorageVar.currentValue());
@ -170,7 +169,7 @@ void SymbolicState::writeStateVars(ContractDefinition const& _contract, smtutil:
if (stateVars.empty()) if (stateVars.empty())
return; return;
map<string, smtutil::Expression> values; std::map<std::string, smtutil::Expression> values;
for (auto var: stateVars) for (auto var: stateVars)
values.emplace(stateVarStorageKey(*var, _contract), m_context.variable(*var)->currentValue()); 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); 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); return m_tx.member(_member);
} }
@ -268,8 +267,8 @@ void SymbolicState::prepareForSourceUnit(SourceUnit const& _source, bool _storag
{ {
auto allSources = _source.referencedSourceUnits(true); auto allSources = _source.referencedSourceUnits(true);
allSources.insert(&_source); allSources.insert(&_source);
set<FunctionCall const*, ASTCompareByID<FunctionCall>> abiCalls; std::set<FunctionCall const*, ASTCompareByID<FunctionCall>> abiCalls;
set<ContractDefinition const*, ASTCompareByID<ContractDefinition>> contracts; std::set<ContractDefinition const*, ASTCompareByID<ContractDefinition>> contracts;
for (auto const& source: allSources) for (auto const& source: allSources)
{ {
abiCalls += SMTEncoder::collectABICalls(source); abiCalls += SMTEncoder::collectABICalls(source);
@ -283,34 +282,34 @@ void SymbolicState::prepareForSourceUnit(SourceUnit const& _source, bool _storag
/// Private helpers. /// 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); 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<ContractDefinition const*, ASTCompareByID<ContractDefinition>> const& _contracts, bool _allStorages) void SymbolicState::buildState(std::set<ContractDefinition const*, ASTCompareByID<ContractDefinition>> const& _contracts, bool _allStorages)
{ {
map<string, SortPointer> stateMembers{ std::map<std::string, SortPointer> stateMembers{
{"balances", make_shared<smtutil::ArraySort>(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort)} {"balances", std::make_shared<smtutil::ArraySort>(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort)}
}; };
if (_allStorages) if (_allStorages)
{ {
vector<string> memberNames; std::vector<std::string> memberNames;
vector<SortPointer> memberSorts; std::vector<SortPointer> memberSorts;
for (auto contract: _contracts) 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 // z3 doesn't like empty tuples, so if the contract has 0
// state vars we can't put it there. // state vars we can't put it there.
@ -319,16 +318,16 @@ void SymbolicState::buildState(set<ContractDefinition const*, ASTCompareByID<Con
continue; continue;
auto names = applyMap(stateVars, [&](auto var) { auto names = applyMap(stateVars, [&](auto var) {
return var->name() + "_" + to_string(var->id()) + suffix; return var->name() + "_" + std::to_string(var->id()) + suffix;
}); });
auto sorts = applyMap(stateVars, [](auto var) { return smtSortAbstractFunction(*var->type()); }); auto sorts = applyMap(stateVars, [](auto var) { return smtSortAbstractFunction(*var->type()); });
string name = "storage" + suffix; std::string name = "storage" + suffix;
auto storageTuple = make_shared<smtutil::TupleSort>( auto storageTuple = std::make_shared<smtutil::TupleSort>(
name + "_type", names, sorts name + "_type", names, sorts
); );
auto storageSort = make_shared<smtutil::ArraySort>( auto storageSort = std::make_shared<smtutil::ArraySort>(
smtSort(*TypeProvider::address()), smtSort(*TypeProvider::address()),
storageTuple storageTuple
); );
@ -339,26 +338,26 @@ void SymbolicState::buildState(set<ContractDefinition const*, ASTCompareByID<Con
stateMembers.emplace( stateMembers.emplace(
"isActive", "isActive",
make_shared<smtutil::ArraySort>(smtSort(*TypeProvider::address()), smtutil::SortProvider::boolSort) std::make_shared<smtutil::ArraySort>(smtSort(*TypeProvider::address()), smtutil::SortProvider::boolSort)
); );
stateMembers.emplace( stateMembers.emplace(
"storage", "storage",
make_shared<smtutil::TupleSort>( std::make_shared<smtutil::TupleSort>(
"storage_type", memberNames, memberSorts "storage_type", memberNames, memberSorts
) )
); );
} }
m_state = make_unique<BlockchainVariable>( m_state = std::make_unique<BlockchainVariable>(
"state", "state",
std::move(stateMembers), std::move(stateMembers),
m_context m_context
); );
} }
void SymbolicState::buildABIFunctions(set<FunctionCall const*, ASTCompareByID<FunctionCall>> const& _abiFunctions) void SymbolicState::buildABIFunctions(std::set<FunctionCall const*, ASTCompareByID<FunctionCall>> const& _abiFunctions)
{ {
map<string, SortPointer> functions; std::map<std::string, SortPointer> functions;
for (auto const* funCall: _abiFunctions) for (auto const* funCall: _abiFunctions)
{ {
@ -375,8 +374,8 @@ void SymbolicState::buildABIFunctions(set<FunctionCall const*, ASTCompareByID<Fu
/// Since each abi.* function may have a different number of input/output parameters, /// Since each abi.* function may have a different number of input/output parameters,
/// we generically compute those types. /// we generically compute those types.
vector<frontend::Type const*> inTypes; std::vector<frontend::Type const*> inTypes;
vector<frontend::Type const*> outTypes; std::vector<frontend::Type const*> outTypes;
if (t->kind() == FunctionType::Kind::ABIDecode) if (t->kind() == FunctionType::Kind::ABIDecode)
{ {
/// abi.decode : (bytes, tuple_of_types(return_types)) -> (return_types) /// abi.decode : (bytes, tuple_of_types(return_types)) -> (return_types)
@ -415,7 +414,7 @@ void SymbolicState::buildABIFunctions(set<FunctionCall const*, ASTCompareByID<Fu
/// abi.encodeWithSelector : (bytes4, one_or_more_types) -> bytes /// abi.encodeWithSelector : (bytes4, one_or_more_types) -> bytes
/// abi.encodeWithSignature : (string, one_or_more_types) -> bytes /// abi.encodeWithSignature : (string, one_or_more_types) -> bytes
inTypes.emplace_back(paramTypes.front()); inTypes.emplace_back(paramTypes.front());
inTypes += argTypes(vector<ASTPointer<Expression const>>(args.begin() + 1, args.end())); inTypes += argTypes(std::vector<ASTPointer<Expression const>>(args.begin() + 1, args.end()));
} }
else else
{ {
@ -455,25 +454,25 @@ void SymbolicState::buildABIFunctions(set<FunctionCall const*, ASTCompareByID<Fu
/// If there is only one input or output parameter, we use that type directly. /// If there is only one input or output parameter, we use that type directly.
/// Otherwise we create a tuple wrapping the necessary input or output types. /// Otherwise we create a tuple wrapping the necessary input or output types.
auto typesToSort = [](auto const& _types, string const& _name) -> shared_ptr<Sort> { auto typesToSort = [](auto const& _types, std::string const& _name) -> std::shared_ptr<Sort> {
if (_types.size() == 1) if (_types.size() == 1)
return smtSortAbstractFunction(*_types.front()); return smtSortAbstractFunction(*_types.front());
vector<string> inNames; std::vector<std::string> inNames;
vector<SortPointer> sorts; std::vector<SortPointer> sorts;
for (unsigned i = 0; i < _types.size(); ++i) 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))); sorts.emplace_back(smtSortAbstractFunction(*_types.at(i)));
} }
return make_shared<smtutil::TupleSort>( return std::make_shared<smtutil::TupleSort>(
_name + "_input", _name + "_input",
inNames, inNames,
sorts sorts
); );
}; };
auto functionSort = make_shared<smtutil::ArraySort>( auto functionSort = std::make_shared<smtutil::ArraySort>(
typesToSort(inTypes, name), typesToSort(inTypes, name),
typesToSort(outTypes, name) typesToSort(outTypes, name)
); );
@ -481,13 +480,13 @@ void SymbolicState::buildABIFunctions(set<FunctionCall const*, ASTCompareByID<Fu
functions[name] = functionSort; functions[name] = functionSort;
} }
m_abi = make_unique<BlockchainVariable>("abi", std::move(functions), m_context); m_abi = std::make_unique<BlockchainVariable>("abi", std::move(functions), m_context);
} }
smtutil::Expression SymbolicState::abiFunction(frontend::FunctionCall const* _funCall) smtutil::Expression SymbolicState::abiFunction(frontend::FunctionCall const* _funCall)
{ {
solAssert(m_abi, ""); 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 SymbolicState::SymbolicABIFunction const& SymbolicState::abiFunctionTypes(FunctionCall const* _funCall) const

95
libsolidity/formal/SymbolicTypes.cpp
View File

@ -26,7 +26,6 @@
#include <memory> #include <memory>
#include <vector> #include <vector>
using namespace std;
using namespace solidity::util; using namespace solidity::util;
using namespace solidity::smtutil; using namespace solidity::smtutil;
@ -52,7 +51,7 @@ SortPointer smtSort(frontend::Type const& _type)
{ {
auto fType = dynamic_cast<frontend::FunctionType const*>(&_type); auto fType = dynamic_cast<frontend::FunctionType const*>(&_type);
solAssert(fType, ""); solAssert(fType, "");
vector<SortPointer> parameterSorts = smtSort(fType->parameterTypes()); std::vector<SortPointer> parameterSorts = smtSort(fType->parameterTypes());
auto returnTypes = fType->returnParameterTypes(); auto returnTypes = fType->returnParameterTypes();
SortPointer returnSort; SortPointer returnSort;
// TODO change this when we support tuples. // TODO change this when we support tuples.
@ -64,22 +63,22 @@ SortPointer smtSort(frontend::Type const& _type)
returnSort = SortProvider::uintSort; returnSort = SortProvider::uintSort;
else else
returnSort = smtSort(*returnTypes.front()); returnSort = smtSort(*returnTypes.front());
return make_shared<FunctionSort>(parameterSorts, returnSort); return std::make_shared<FunctionSort>(parameterSorts, returnSort);
} }
case Kind::Array: case Kind::Array:
{ {
shared_ptr<ArraySort> array; std::shared_ptr<ArraySort> array;
if (isMapping(_type)) if (isMapping(_type))
{ {
auto mapType = dynamic_cast<frontend::MappingType const*>(&_type); auto mapType = dynamic_cast<frontend::MappingType const*>(&_type);
solAssert(mapType, ""); solAssert(mapType, "");
array = make_shared<ArraySort>(smtSortAbstractFunction(*mapType->keyType()), smtSortAbstractFunction(*mapType->valueType())); array = std::make_shared<ArraySort>(smtSortAbstractFunction(*mapType->keyType()), smtSortAbstractFunction(*mapType->valueType()));
} }
else if (isStringLiteral(_type)) else if (isStringLiteral(_type))
{ {
auto stringLitType = dynamic_cast<frontend::StringLiteralType const*>(&_type); auto stringLitType = dynamic_cast<frontend::StringLiteralType const*>(&_type);
solAssert(stringLitType, ""); solAssert(stringLitType, "");
array = make_shared<ArraySort>(SortProvider::uintSort, SortProvider::uintSort); array = std::make_shared<ArraySort>(SortProvider::uintSort, SortProvider::uintSort);
} }
else else
{ {
@ -92,10 +91,10 @@ SortPointer smtSort(frontend::Type const& _type)
solAssert(false, ""); solAssert(false, "");
solAssert(arrayType, ""); solAssert(arrayType, "");
array = make_shared<ArraySort>(SortProvider::uintSort, smtSortAbstractFunction(*arrayType->baseType())); array = std::make_shared<ArraySort>(SortProvider::uintSort, smtSortAbstractFunction(*arrayType->baseType()));
} }
string tupleName; std::string tupleName;
auto sliceArrayType = dynamic_cast<ArraySliceType const*>(&_type); auto sliceArrayType = dynamic_cast<ArraySliceType const*>(&_type);
ArrayType const* arrayType = sliceArrayType ? &sliceArrayType->arrayType() : dynamic_cast<ArrayType const*>(&_type); ArrayType const* arrayType = sliceArrayType ? &sliceArrayType->arrayType() : dynamic_cast<ArrayType const*>(&_type);
if ( if (
@ -109,7 +108,7 @@ SortPointer smtSort(frontend::Type const& _type)
// Solidity allows implicit conversion also when assigning arrays. // Solidity allows implicit conversion also when assigning arrays.
// So if the base type potentially has a size, that size cannot go // So if the base type potentially has a size, that size cannot go
// in the tuple's name. // in the tuple's name.
if (auto tupleSort = dynamic_pointer_cast<TupleSort>(array->range)) if (auto tupleSort = std::dynamic_pointer_cast<TupleSort>(array->range))
tupleName = tupleSort->name; tupleName = tupleSort->name;
else if ( else if (
baseType->category() == frontend::Type::Category::Integer || baseType->category() == frontend::Type::Category::Integer ||
@ -128,23 +127,23 @@ SortPointer smtSort(frontend::Type const& _type)
tupleName += "_tuple"; tupleName += "_tuple";
return make_shared<TupleSort>( return std::make_shared<TupleSort>(
tupleName, tupleName,
vector<string>{tupleName + "_accessor_array", tupleName + "_accessor_length"}, std::vector<std::string>{tupleName + "_accessor_array", tupleName + "_accessor_length"},
vector<SortPointer>{array, SortProvider::uintSort} std::vector<SortPointer>{array, SortProvider::uintSort}
); );
} }
case Kind::Tuple: case Kind::Tuple:
{ {
vector<string> members; std::vector<std::string> members;
auto const& tupleName = _type.toString(true); auto const& tupleName = _type.toString(true);
vector<SortPointer> sorts; std::vector<SortPointer> sorts;
if (auto const* tupleType = dynamic_cast<frontend::TupleType const*>(&_type)) if (auto const* tupleType = dynamic_cast<frontend::TupleType const*>(&_type))
{ {
auto const& components = tupleType->components(); auto const& components = tupleType->components();
for (unsigned i = 0; i < components.size(); ++i) 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()); sorts = smtSortAbstractFunction(tupleType->components());
} }
else if (auto const* structType = dynamic_cast<frontend::StructType const*>(&_type)) else if (auto const* structType = dynamic_cast<frontend::StructType const*>(&_type))
@ -161,7 +160,7 @@ SortPointer smtSort(frontend::Type const& _type)
else else
solAssert(false, ""); solAssert(false, "");
return make_shared<TupleSort>(tupleName, members, sorts); return std::make_shared<TupleSort>(tupleName, members, sorts);
} }
default: default:
// Abstract case. // Abstract case.
@ -169,9 +168,9 @@ SortPointer smtSort(frontend::Type const& _type)
} }
} }
vector<SortPointer> smtSort(vector<frontend::Type const*> const& _types) std::vector<SortPointer> smtSort(std::vector<frontend::Type const*> const& _types)
{ {
vector<SortPointer> sorts; std::vector<SortPointer> sorts;
for (auto const& type: _types) for (auto const& type: _types)
sorts.push_back(smtSort(*type)); sorts.push_back(smtSort(*type));
return sorts; return sorts;
@ -184,9 +183,9 @@ SortPointer smtSortAbstractFunction(frontend::Type const& _type)
return smtSort(_type); return smtSort(_type);
} }
vector<SortPointer> smtSortAbstractFunction(vector<frontend::Type const*> const& _types) std::vector<SortPointer> smtSortAbstractFunction(std::vector<frontend::Type const*> const& _types)
{ {
vector<SortPointer> sorts; std::vector<SortPointer> sorts;
for (auto const& type: _types) for (auto const& type: _types)
if (type) if (type)
sorts.push_back(smtSortAbstractFunction(*type)); sorts.push_back(smtSortAbstractFunction(*type));
@ -233,14 +232,14 @@ bool isSupportedTypeDeclaration(frontend::Type const& _type)
isFunction(_type); isFunction(_type);
} }
pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable( std::pair<bool, std::shared_ptr<SymbolicVariable>> newSymbolicVariable(
frontend::Type const& _type, frontend::Type const& _type,
std::string const& _uniqueName, std::string const& _uniqueName,
EncodingContext& _context EncodingContext& _context
) )
{ {
bool abstract = false; bool abstract = false;
shared_ptr<SymbolicVariable> var; std::shared_ptr<SymbolicVariable> var;
frontend::Type const* type = &_type; frontend::Type const* type = &_type;
if (auto userType = dynamic_cast<UserDefinedValueType const*>(type)) if (auto userType = dynamic_cast<UserDefinedValueType const*>(type))
@ -249,10 +248,10 @@ pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
if (!isSupportedTypeDeclaration(_type)) if (!isSupportedTypeDeclaration(_type))
{ {
abstract = true; abstract = true;
var = make_shared<SymbolicIntVariable>(frontend::TypeProvider::uint256(), type, _uniqueName, _context); var = std::make_shared<SymbolicIntVariable>(frontend::TypeProvider::uint256(), type, _uniqueName, _context);
} }
else if (isBool(_type)) else if (isBool(_type))
var = make_shared<SymbolicBoolVariable>(type, _uniqueName, _context); var = std::make_shared<SymbolicBoolVariable>(type, _uniqueName, _context);
else if (isFunction(_type)) else if (isFunction(_type))
{ {
auto const& fType = dynamic_cast<FunctionType const*>(type); auto const& fType = dynamic_cast<FunctionType const*>(type);
@ -271,45 +270,45 @@ pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
) )
{ {
abstract = true; abstract = true;
var = make_shared<SymbolicIntVariable>(TypeProvider::uint256(), type, _uniqueName, _context); var = std::make_shared<SymbolicIntVariable>(TypeProvider::uint256(), type, _uniqueName, _context);
} }
else else
var = make_shared<SymbolicFunctionVariable>(type, _uniqueName, _context); var = std::make_shared<SymbolicFunctionVariable>(type, _uniqueName, _context);
} }
else if (isInteger(_type)) else if (isInteger(_type))
var = make_shared<SymbolicIntVariable>(type, type, _uniqueName, _context); var = std::make_shared<SymbolicIntVariable>(type, type, _uniqueName, _context);
else if (isFixedPoint(_type)) else if (isFixedPoint(_type))
var = make_shared<SymbolicIntVariable>(type, type, _uniqueName, _context); var = std::make_shared<SymbolicIntVariable>(type, type, _uniqueName, _context);
else if (isFixedBytes(_type)) else if (isFixedBytes(_type))
{ {
auto fixedBytesType = dynamic_cast<frontend::FixedBytesType const*>(type); auto fixedBytesType = dynamic_cast<frontend::FixedBytesType const*>(type);
solAssert(fixedBytesType, ""); solAssert(fixedBytesType, "");
var = make_shared<SymbolicFixedBytesVariable>(type, fixedBytesType->numBytes(), _uniqueName, _context); var = std::make_shared<SymbolicFixedBytesVariable>(type, fixedBytesType->numBytes(), _uniqueName, _context);
} }
else if (isAddress(_type) || isContract(_type)) else if (isAddress(_type) || isContract(_type))
var = make_shared<SymbolicAddressVariable>(_uniqueName, _context); var = std::make_shared<SymbolicAddressVariable>(_uniqueName, _context);
else if (isEnum(_type)) else if (isEnum(_type))
var = make_shared<SymbolicEnumVariable>(type, _uniqueName, _context); var = std::make_shared<SymbolicEnumVariable>(type, _uniqueName, _context);
else if (isRational(_type)) else if (isRational(_type))
{ {
auto rational = dynamic_cast<frontend::RationalNumberType const*>(&_type); auto rational = dynamic_cast<frontend::RationalNumberType const*>(&_type);
solAssert(rational, ""); solAssert(rational, "");
if (rational->isFractional()) if (rational->isFractional())
var = make_shared<SymbolicIntVariable>(frontend::TypeProvider::uint256(), type, _uniqueName, _context); var = std::make_shared<SymbolicIntVariable>(frontend::TypeProvider::uint256(), type, _uniqueName, _context);
else else
var = make_shared<SymbolicIntVariable>(type, type, _uniqueName, _context); var = std::make_shared<SymbolicIntVariable>(type, type, _uniqueName, _context);
} }
else if (isMapping(_type) || isArray(_type)) else if (isMapping(_type) || isArray(_type))
var = make_shared<SymbolicArrayVariable>(type, type, _uniqueName, _context); var = std::make_shared<SymbolicArrayVariable>(type, type, _uniqueName, _context);
else if (isTuple(_type)) else if (isTuple(_type))
var = make_shared<SymbolicTupleVariable>(type, _uniqueName, _context); var = std::make_shared<SymbolicTupleVariable>(type, _uniqueName, _context);
else if (isStringLiteral(_type)) else if (isStringLiteral(_type))
{ {
auto stringType = TypeProvider::stringMemory(); auto stringType = TypeProvider::stringMemory();
var = make_shared<SymbolicArrayVariable>(stringType, type, _uniqueName, _context); var = std::make_shared<SymbolicArrayVariable>(stringType, type, _uniqueName, _context);
} }
else if (isNonRecursiveStruct(_type)) else if (isNonRecursiveStruct(_type))
var = make_shared<SymbolicStructVariable>(type, _uniqueName, _context); var = std::make_shared<SymbolicStructVariable>(type, _uniqueName, _context);
else else
solAssert(false, ""); solAssert(false, "");
return make_pair(abstract, var); return make_pair(abstract, var);
@ -482,9 +481,9 @@ smtutil::Expression zeroValue(frontend::Type const* _type)
return smtutil::Expression(false); return smtutil::Expression(false);
if (isArray(*_type) || isMapping(*_type)) if (isArray(*_type) || isMapping(*_type))
{ {
auto tupleSort = dynamic_pointer_cast<TupleSort>(smtSort(*_type)); auto tupleSort = std::dynamic_pointer_cast<TupleSort>(smtSort(*_type));
solAssert(tupleSort, ""); solAssert(tupleSort, "");
auto sortSort = make_shared<SortSort>(tupleSort->components.front()); auto sortSort = std::make_shared<SortSort>(tupleSort->components.front());
std::optional<smtutil::Expression> zeroArray; std::optional<smtutil::Expression> zeroArray;
auto length = bigint(0); auto length = bigint(0);
@ -502,16 +501,16 @@ smtutil::Expression zeroValue(frontend::Type const* _type)
solAssert(zeroArray, ""); solAssert(zeroArray, "");
return smtutil::Expression::tuple_constructor( return smtutil::Expression::tuple_constructor(
smtutil::Expression(std::make_shared<SortSort>(tupleSort), tupleSort->name), smtutil::Expression(std::make_shared<SortSort>(tupleSort), tupleSort->name),
vector<smtutil::Expression>{*zeroArray, length} std::vector<smtutil::Expression>{*zeroArray, length}
); );
} }
if (isNonRecursiveStruct(*_type)) if (isNonRecursiveStruct(*_type))
{ {
auto const* structType = dynamic_cast<StructType const*>(_type); auto const* structType = dynamic_cast<StructType const*>(_type);
auto structSort = dynamic_pointer_cast<TupleSort>(smtSort(*_type)); auto structSort = std::dynamic_pointer_cast<TupleSort>(smtSort(*_type));
return smtutil::Expression::tuple_constructor( return smtutil::Expression::tuple_constructor(
smtutil::Expression(make_shared<SortSort>(structSort), structSort->name), smtutil::Expression(std::make_shared<SortSort>(structSort), structSort->name),
applyMap( applyMap(
structType->structDefinition().members(), structType->structDefinition().members(),
[](auto var) { return zeroValue(var->type()); } [](auto var) { return zeroValue(var->type()); }
@ -550,7 +549,7 @@ bool isSigned(frontend::Type const* _type)
return isSigned; return isSigned;
} }
pair<unsigned, bool> typeBvSizeAndSignedness(frontend::Type const* _type) std::pair<unsigned, bool> typeBvSizeAndSignedness(frontend::Type const* _type)
{ {
if (auto userType = dynamic_cast<UserDefinedValueType const*>(_type)) if (auto userType = dynamic_cast<UserDefinedValueType const*>(_type))
return typeBvSizeAndSignedness(&userType->underlyingType()); return typeBvSizeAndSignedness(&userType->underlyingType());
@ -596,7 +595,7 @@ smtutil::Expression symbolicUnknownConstraints(smtutil::Expression _expr, fronte
return smtutil::Expression(true); return smtutil::Expression(true);
} }
optional<smtutil::Expression> symbolicTypeConversion(frontend::Type const* _from, frontend::Type const* _to) std::optional<smtutil::Expression> symbolicTypeConversion(frontend::Type const* _from, frontend::Type const* _to)
{ {
if (auto userType = dynamic_cast<UserDefinedValueType const*>(_to)) if (auto userType = dynamic_cast<UserDefinedValueType const*>(_to))
return symbolicTypeConversion(_from, &userType->underlyingType()); return symbolicTypeConversion(_from, &userType->underlyingType());
@ -618,7 +617,7 @@ optional<smtutil::Expression> symbolicTypeConversion(frontend::Type const* _from
return std::nullopt; 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<TupleSort const&>(*_tuple.sort); TupleSort const& _sort = dynamic_cast<TupleSort const&>(*_tuple.sort);
return smtutil::Expression::tuple_get( 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<string, smtutil::Expression> const& _values) smtutil::Expression assignMember(smtutil::Expression const _tuple, std::map<std::string, smtutil::Expression> const& _values)
{ {
TupleSort const& _sort = dynamic_cast<TupleSort const&>(*_tuple.sort); TupleSort const& _sort = dynamic_cast<TupleSort const&>(*_tuple.sort);
vector<smtutil::Expression> args; std::vector<smtutil::Expression> args;
for (auto const& m: _sort.members) for (auto const& m: _sort.members)
if (auto* value = util::valueOrNullptr(_values, m)) if (auto* value = util::valueOrNullptr(_values, m))
args.emplace_back(*value); args.emplace_back(*value);
else else
args.emplace_back(member(_tuple, m)); args.emplace_back(member(_tuple, m));
auto sortExpr = smtutil::Expression(make_shared<smtutil::SortSort>(_tuple.sort), _tuple.name); auto sortExpr = smtutil::Expression(std::make_shared<smtutil::SortSort>(_tuple.sort), _tuple.name);
return smtutil::Expression::tuple_constructor(sortExpr, args); return smtutil::Expression::tuple_constructor(sortExpr, args);
} }

65
libsolidity/formal/SymbolicVariables.cpp
View File

@ -23,7 +23,6 @@
#include <libsolutil/Algorithms.h> #include <libsolutil/Algorithms.h>
using namespace std;
using namespace solidity; using namespace solidity;
using namespace solidity::util; using namespace solidity::util;
using namespace solidity::smtutil; using namespace solidity::smtutil;
@ -33,14 +32,14 @@ using namespace solidity::frontend::smt;
SymbolicVariable::SymbolicVariable( SymbolicVariable::SymbolicVariable(
frontend::Type const* _type, frontend::Type const* _type,
frontend::Type const* _originalType, frontend::Type const* _originalType,
string _uniqueName, std::string _uniqueName,
EncodingContext& _context EncodingContext& _context
): ):
m_type(_type), m_type(_type),
m_originalType(_originalType), m_originalType(_originalType),
m_uniqueName(std::move(_uniqueName)), m_uniqueName(std::move(_uniqueName)),
m_context(_context), m_context(_context),
m_ssa(make_unique<SSAVariable>()) m_ssa(std::make_unique<SSAVariable>())
{ {
solAssert(m_type, ""); solAssert(m_type, "");
m_sort = smtSort(*m_type); m_sort = smtSort(*m_type);
@ -49,13 +48,13 @@ SymbolicVariable::SymbolicVariable(
SymbolicVariable::SymbolicVariable( SymbolicVariable::SymbolicVariable(
SortPointer _sort, SortPointer _sort,
string _uniqueName, std::string _uniqueName,
EncodingContext& _context EncodingContext& _context
): ):
m_sort(std::move(_sort)), m_sort(std::move(_sort)),
m_uniqueName(std::move(_uniqueName)), m_uniqueName(std::move(_uniqueName)),
m_context(_context), m_context(_context),
m_ssa(make_unique<SSAVariable>()) m_ssa(std::make_unique<SSAVariable>())
{ {
solAssert(m_sort, ""); solAssert(m_sort, "");
} }
@ -65,7 +64,7 @@ smtutil::Expression SymbolicVariable::currentValue(frontend::Type const*) const
return valueAtIndex(m_ssa->index()); return valueAtIndex(m_ssa->index());
} }
string SymbolicVariable::currentName() const std::string SymbolicVariable::currentName() const
{ {
return uniqueSymbol(m_ssa->index()); return uniqueSymbol(m_ssa->index());
} }
@ -75,14 +74,14 @@ smtutil::Expression SymbolicVariable::valueAtIndex(unsigned _index) const
return m_context.newVariable(uniqueSymbol(_index), m_sort); return m_context.newVariable(uniqueSymbol(_index), m_sort);
} }
string SymbolicVariable::nameAtIndex(unsigned _index) const std::string SymbolicVariable::nameAtIndex(unsigned _index) const
{ {
return uniqueSymbol(_index); 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() smtutil::Expression SymbolicVariable::resetIndex()
@ -105,7 +104,7 @@ smtutil::Expression SymbolicVariable::increaseIndex()
SymbolicBoolVariable::SymbolicBoolVariable( SymbolicBoolVariable::SymbolicBoolVariable(
frontend::Type const* _type, frontend::Type const* _type,
string _uniqueName, std::string _uniqueName,
EncodingContext& _context EncodingContext& _context
): ):
SymbolicVariable(_type, _type, std::move(_uniqueName), _context) SymbolicVariable(_type, _type, std::move(_uniqueName), _context)
@ -116,7 +115,7 @@ SymbolicBoolVariable::SymbolicBoolVariable(
SymbolicIntVariable::SymbolicIntVariable( SymbolicIntVariable::SymbolicIntVariable(
frontend::Type const* _type, frontend::Type const* _type,
frontend::Type const* _originalType, frontend::Type const* _originalType,
string _uniqueName, std::string _uniqueName,
EncodingContext& _context EncodingContext& _context
): ):
SymbolicVariable(_type, _originalType, std::move(_uniqueName), _context) SymbolicVariable(_type, _originalType, std::move(_uniqueName), _context)
@ -125,7 +124,7 @@ SymbolicIntVariable::SymbolicIntVariable(
} }
SymbolicAddressVariable::SymbolicAddressVariable( SymbolicAddressVariable::SymbolicAddressVariable(
string _uniqueName, std::string _uniqueName,
EncodingContext& _context EncodingContext& _context
): ):
SymbolicIntVariable(TypeProvider::uint(160), TypeProvider::uint(160), std::move(_uniqueName), _context) SymbolicIntVariable(TypeProvider::uint(160), TypeProvider::uint(160), std::move(_uniqueName), _context)
@ -135,7 +134,7 @@ SymbolicAddressVariable::SymbolicAddressVariable(
SymbolicFixedBytesVariable::SymbolicFixedBytesVariable( SymbolicFixedBytesVariable::SymbolicFixedBytesVariable(
frontend::Type const* _originalType, frontend::Type const* _originalType,
unsigned _numBytes, unsigned _numBytes,
string _uniqueName, std::string _uniqueName,
EncodingContext& _context EncodingContext& _context
): ):
SymbolicIntVariable(TypeProvider::uint(_numBytes * 8), _originalType, std::move(_uniqueName), _context) SymbolicIntVariable(TypeProvider::uint(_numBytes * 8), _originalType, std::move(_uniqueName), _context)
@ -144,7 +143,7 @@ SymbolicFixedBytesVariable::SymbolicFixedBytesVariable(
SymbolicFunctionVariable::SymbolicFunctionVariable( SymbolicFunctionVariable::SymbolicFunctionVariable(
frontend::Type const* _type, frontend::Type const* _type,
string _uniqueName, std::string _uniqueName,
EncodingContext& _context EncodingContext& _context
): ):
SymbolicVariable(_type, _type, std::move(_uniqueName), _context), SymbolicVariable(_type, _type, std::move(_uniqueName), _context),
@ -155,7 +154,7 @@ SymbolicFunctionVariable::SymbolicFunctionVariable(
SymbolicFunctionVariable::SymbolicFunctionVariable( SymbolicFunctionVariable::SymbolicFunctionVariable(
SortPointer _sort, SortPointer _sort,
string _uniqueName, std::string _uniqueName,
EncodingContext& _context EncodingContext& _context
): ):
SymbolicVariable(std::move(_sort), std::move(_uniqueName), _context), SymbolicVariable(std::move(_sort), std::move(_uniqueName), _context),
@ -204,7 +203,7 @@ smtutil::Expression SymbolicFunctionVariable::increaseIndex()
return m_abstract.currentValue(); return m_abstract.currentValue();
} }
smtutil::Expression SymbolicFunctionVariable::operator()(vector<smtutil::Expression> _arguments) const smtutil::Expression SymbolicFunctionVariable::operator()(std::vector<smtutil::Expression> _arguments) const
{ {
return m_declaration(_arguments); return m_declaration(_arguments);
} }
@ -216,7 +215,7 @@ void SymbolicFunctionVariable::resetDeclaration()
SymbolicEnumVariable::SymbolicEnumVariable( SymbolicEnumVariable::SymbolicEnumVariable(
frontend::Type const* _type, frontend::Type const* _type,
string _uniqueName, std::string _uniqueName,
EncodingContext& _context EncodingContext& _context
): ):
SymbolicVariable(_type, _type, std::move(_uniqueName), _context) SymbolicVariable(_type, _type, std::move(_uniqueName), _context)
@ -226,7 +225,7 @@ SymbolicEnumVariable::SymbolicEnumVariable(
SymbolicTupleVariable::SymbolicTupleVariable( SymbolicTupleVariable::SymbolicTupleVariable(
frontend::Type const* _type, frontend::Type const* _type,
string _uniqueName, std::string _uniqueName,
EncodingContext& _context EncodingContext& _context
): ):
SymbolicVariable(_type, _type, std::move(_uniqueName), _context) SymbolicVariable(_type, _type, std::move(_uniqueName), _context)
@ -236,7 +235,7 @@ SymbolicTupleVariable::SymbolicTupleVariable(
SymbolicTupleVariable::SymbolicTupleVariable( SymbolicTupleVariable::SymbolicTupleVariable(
SortPointer _sort, SortPointer _sort,
string _uniqueName, std::string _uniqueName,
EncodingContext& _context EncodingContext& _context
): ):
SymbolicVariable(std::move(_sort), std::move(_uniqueName), _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)) if (!_targetType || sort() == smtSort(*_targetType))
return SymbolicVariable::currentValue(); return SymbolicVariable::currentValue();
auto thisTuple = dynamic_pointer_cast<TupleSort>(sort()); auto thisTuple = std::dynamic_pointer_cast<TupleSort>(sort());
auto otherTuple = dynamic_pointer_cast<TupleSort>(smtSort(*_targetType)); auto otherTuple = std::dynamic_pointer_cast<TupleSort>(smtSort(*_targetType));
solAssert(thisTuple && otherTuple, ""); solAssert(thisTuple && otherTuple, "");
solAssert(thisTuple->components.size() == otherTuple->components.size(), ""); solAssert(thisTuple->components.size() == otherTuple->components.size(), "");
vector<smtutil::Expression> args; std::vector<smtutil::Expression> args;
for (size_t i = 0; i < thisTuple->components.size(); ++i) for (size_t i = 0; i < thisTuple->components.size(); ++i)
args.emplace_back(component(i, type(), _targetType)); args.emplace_back(component(i, type(), _targetType));
return smtutil::Expression::tuple_constructor( return smtutil::Expression::tuple_constructor(
smtutil::Expression(make_shared<smtutil::SortSort>(smtSort(*_targetType)), ""), smtutil::Expression(std::make_shared<smtutil::SortSort>(smtSort(*_targetType)), ""),
args args
); );
} }
vector<SortPointer> const& SymbolicTupleVariable::components() const std::vector<SortPointer> const& SymbolicTupleVariable::components() const
{ {
auto tupleSort = dynamic_pointer_cast<TupleSort>(m_sort); auto tupleSort = std::dynamic_pointer_cast<TupleSort>(m_sort);
solAssert(tupleSort, ""); solAssert(tupleSort, "");
return tupleSort->components; return tupleSort->components;
} }
@ -275,7 +274,7 @@ smtutil::Expression SymbolicTupleVariable::component(
frontend::Type const* _toType frontend::Type const* _toType
) const ) const
{ {
optional<smtutil::Expression> conversion = symbolicTypeConversion(_fromType, _toType); std::optional<smtutil::Expression> conversion = symbolicTypeConversion(_fromType, _toType);
if (conversion) if (conversion)
return *conversion; return *conversion;
@ -285,7 +284,7 @@ smtutil::Expression SymbolicTupleVariable::component(
SymbolicArrayVariable::SymbolicArrayVariable( SymbolicArrayVariable::SymbolicArrayVariable(
frontend::Type const* _type, frontend::Type const* _type,
frontend::Type const* _originalType, frontend::Type const* _originalType,
string _uniqueName, std::string _uniqueName,
EncodingContext& _context EncodingContext& _context
): ):
SymbolicVariable(_type, _originalType, std::move(_uniqueName), _context), SymbolicVariable(_type, _originalType, std::move(_uniqueName), _context),
@ -300,7 +299,7 @@ SymbolicArrayVariable::SymbolicArrayVariable(
SymbolicArrayVariable::SymbolicArrayVariable( SymbolicArrayVariable::SymbolicArrayVariable(
SortPointer _sort, SortPointer _sort,
string _uniqueName, std::string _uniqueName,
EncodingContext& _context EncodingContext& _context
): ):
SymbolicVariable(std::move(_sort), std::move(_uniqueName), _context), SymbolicVariable(std::move(_sort), std::move(_uniqueName), _context),
@ -319,7 +318,7 @@ SymbolicArrayVariable::SymbolicArrayVariable(
smtutil::Expression SymbolicArrayVariable::currentValue(frontend::Type const* _targetType) const smtutil::Expression SymbolicArrayVariable::currentValue(frontend::Type const* _targetType) const
{ {
optional<smtutil::Expression> conversion = symbolicTypeConversion(m_originalType, _targetType); std::optional<smtutil::Expression> conversion = symbolicTypeConversion(m_originalType, _targetType);
if (conversion) if (conversion)
return *conversion; return *conversion;
@ -343,7 +342,7 @@ smtutil::Expression SymbolicArrayVariable::length() const
SymbolicStructVariable::SymbolicStructVariable( SymbolicStructVariable::SymbolicStructVariable(
frontend::Type const* _type, frontend::Type const* _type,
string _uniqueName, std::string _uniqueName,
EncodingContext& _context EncodingContext& _context
): ):
SymbolicVariable(_type, _type, std::move(_uniqueName), _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)); 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<StructType const*>(m_type); auto const* structType = dynamic_cast<StructType const*>(m_type);
solAssert(structType, ""); solAssert(structType, "");
@ -385,7 +384,7 @@ smtutil::Expression SymbolicStructVariable::assignMember(string const& _member,
return currentValue(); return currentValue();
} }
smtutil::Expression SymbolicStructVariable::assignAllMembers(vector<smtutil::Expression> const& _memberValues) smtutil::Expression SymbolicStructVariable::assignAllMembers(std::vector<smtutil::Expression> const& _memberValues)
{ {
auto structType = dynamic_cast<StructType const*>(m_type); auto structType = dynamic_cast<StructType const*>(m_type);
solAssert(structType, ""); solAssert(structType, "");

3
libsolidity/formal/VariableUsage.cpp
View File

@ -25,13 +25,12 @@
#include <algorithm> #include <algorithm>
using namespace std;
using namespace solidity; using namespace solidity;
using namespace solidity::util; using namespace solidity::util;
using namespace solidity::frontend; using namespace solidity::frontend;
using namespace solidity::frontend::smt; using namespace solidity::frontend::smt;
set<VariableDeclaration const*> VariableUsage::touchedVariables(ASTNode const& _node, vector<CallableDeclaration const*> const& _outerCallstack) std::set<VariableDeclaration const*> VariableUsage::touchedVariables(ASTNode const& _node, std::vector<CallableDeclaration const*> const& _outerCallstack)
{ {
m_touchedVariables.clear(); m_touchedVariables.clear();
m_callStack.clear(); m_callStack.clear();

1
scripts/check_style.sh
View File

@ -29,6 +29,7 @@ NAMESPACE_STD_FREE_FILES=(
libsolidity/ast/* libsolidity/ast/*
libsolidity/codegen/ir/* libsolidity/codegen/ir/*
libsolidity/codegen/* libsolidity/codegen/*
libsolidity/formal/*
) )
( (