diff --git a/Changelog.md b/Changelog.md index 0cfa621e802a..19b71804a2fe 100644 --- a/Changelog.md +++ b/Changelog.md @@ -7,7 +7,8 @@ Language Features: * Yul: Introduce builtin ``blobhash()`` for retrieving versioned hashes of blobs associated with the transaction. Compiler Features: - * EVM: Support for the EVM Version "Cancun". +* EVM: Support for the EVM Version "Cancun". +* SMTChecker: Support `bytes.concat` except when string literals are passed as arguments. Bugfixes: * AST import: Fix bug when importing inline assembly with empty ``let`` variable declaration. diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 3cd1524599df..2c9075abcc4a 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -940,8 +940,6 @@ void CHC::nondetCall(ContractDefinition const& _contract, VariableDeclaration co for (auto const* var: _contract.stateVariables()) m_context.variable(*var)->increaseIndex(); - auto error = errorFlag().increaseIndex(); - Predicate const& callPredicate = *createSymbolicBlock( nondetInterfaceSort(_contract, state()), "nondet_call_" + uniquePrefix(), @@ -950,7 +948,7 @@ void CHC::nondetCall(ContractDefinition const& _contract, VariableDeclaration co m_currentContract ); auto postCallState = std::vector{state().state()} + currentStateVariables(_contract); - std::vector stateExprs{error, address, state().abi(), state().crypto()}; + std::vector stateExprs = commonStateExpressions(errorFlag().increaseIndex(), address); auto nondet = (*m_nondetInterfaces.at(&_contract))(stateExprs + preCallState + postCallState); auto nondetCall = callPredicate(stateExprs + preCallState + postCallState); @@ -1024,8 +1022,6 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall) m_context.variable(*var)->increaseIndex(); } - auto error = errorFlag().increaseIndex(); - Predicate const& callPredicate = *createSymbolicBlock( nondetInterfaceSort(*m_currentContract, state()), "nondet_call_" + uniquePrefix(), @@ -1033,7 +1029,7 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall) &_funCall ); auto postCallState = std::vector{state().state()} + currentStateVariables(); - std::vector stateExprs{error, state().thisAddress(), state().abi(), state().crypto()}; + std::vector stateExprs = commonStateExpressions(errorFlag().increaseIndex(), state().thisAddress()); auto nondet = (*m_nondetInterfaces.at(m_currentContract))(stateExprs + preCallState + postCallState); auto nondetCall = callPredicate(stateExprs + preCallState + postCallState); @@ -1464,7 +1460,9 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source) auto errorPost = errorFlag().increaseIndex(); auto nondetPost = smt::nondetInterface(iface, *contract, m_context, 0, 2); - std::vector args{errorPost, state().thisAddress(), state().abi(), state().crypto(), state().tx(), state().state(1)}; + std::vector args = + commonStateExpressions(errorPost, state().thisAddress()) + + std::vector{state().tx(), state().state(1)}; args += state1 + applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); }) + std::vector{state().state(2)} + @@ -1829,7 +1827,9 @@ smtutil::Expression CHC::predicate( errorFlag().increaseIndex(); - std::vector args{errorFlag().currentValue(), _contractAddressValue, state().abi(), state().crypto(), state().tx(), state().state()}; + std::vector args = + commonStateExpressions(errorFlag().currentValue(), _contractAddressValue) + + std::vector{state().tx(), state().state()}; auto const* contract = _funDef->annotation().contract; auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts; @@ -2311,7 +2311,6 @@ std::optional CHC::generateCounterexample(CHCSolverInterface::CexGr path.emplace_back("State: " + modelMsg); } } - std::string txCex = summaryPredicate->formatSummaryCall(summaryArgs, m_charStreamProvider); std::list calls; @@ -2486,3 +2485,10 @@ void CHC::decreaseBalanceFromOptionsValue(Expression const& _value) { state().addBalance(state().thisAddress(), 0 - expr(_value)); } + +std::vector CHC::commonStateExpressions(smtutil::Expression const& error, smtutil::Expression const& address) +{ + if (state().hasBytesConcatFunction()) + return {error, address, state().abi(), state().bytesConcat(), state().crypto()}; + return {error, address, state().abi(), state().crypto()}; +} diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index fe7387bd3568..be150baf1b54 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -362,6 +362,8 @@ class CHC: public SMTEncoder /// Adds constraints that decrease the balance of the caller by _value. void decreaseBalanceFromOptionsValue(Expression const& _value); + + std::vector commonStateExpressions(smtutil::Expression const& error, smtutil::Expression const& address); //@} /// Predicates. diff --git a/libsolidity/formal/Predicate.cpp b/libsolidity/formal/Predicate.cpp index 2ab494fc4d28..58a5a5a3e721 100644 --- a/libsolidity/formal/Predicate.cpp +++ b/libsolidity/formal/Predicate.cpp @@ -55,13 +55,15 @@ Predicate const* Predicate::create( return &m_predicates.emplace( std::piecewise_construct, std::forward_as_tuple(functorName), - std::forward_as_tuple(std::move(predicate), _type, _node, _contractContext, std::move(_scopeStack)) + std::forward_as_tuple(std::move(predicate), _type, _context.state().hasBytesConcatFunction(), + _node, _contractContext, std::move(_scopeStack)) ).first->second; } Predicate::Predicate( smt::SymbolicFunctionVariable&& _predicate, PredicateType _type, + bool _bytesConcatFunctionInContext, ASTNode const* _node, ContractDefinition const* _contractContext, std::vector _scopeStack @@ -70,7 +72,8 @@ Predicate::Predicate( m_type(_type), m_node(_node), m_contractContext(_contractContext), - m_scopeStack(_scopeStack) + m_scopeStack(_scopeStack), + m_bytesConcatFunctionInContext(_bytesConcatFunctionInContext) { } @@ -229,7 +232,7 @@ std::string Predicate::formatSummaryCall( return {}; } - /// 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, (optionally) bytesConcatFunctions, cryptoFunctions, txData, preBlockChainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars). /// Here we are interested in preInputVars to format the function call. std::string txModel; @@ -285,7 +288,7 @@ std::string Predicate::formatSummaryCall( } // Here we are interested in txData from the summary predicate. - auto txValues = readTxVars(_args.at(4)); + auto txValues = readTxVars(_args.at(txValuesIndex())); std::vector values; for (auto const& _var: txVars) if (auto v = txValues.at(_var)) @@ -303,7 +306,7 @@ std::string Predicate::formatSummaryCall( auto const* fun = programFunction(); solAssert(fun, ""); - auto first = _args.begin() + 6 + static_cast(stateVars->size()); + auto first = _args.begin() + static_cast(firstArgIndex()) + static_cast(stateVars->size()); auto last = first + static_cast(fun->parameters().size()); solAssert(first >= _args.begin() && first <= _args.end(), ""); solAssert(last >= _args.begin() && last <= _args.end(), ""); @@ -337,8 +340,8 @@ std::string Predicate::formatSummaryCall( std::vector> Predicate::summaryStateValues(std::vector const& _args) const { - /// The signature of a function summary predicate is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars). - /// The signature of the summary predicate of a contract without constructor is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockchainState, postBlockchainState, preStateVars, postStateVars). + /// The signature of a function summary predicate is: summary(error, this, abiFunctions, (optionally) bytesConcatFunctions, 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, (optionally) bytesConcatFunctions, cryptoFunctions, txData, preBlockchainState, postBlockchainState, preStateVars, postStateVars). /// Here we are interested in postStateVars. auto stateVars = stateVariables(); solAssert(stateVars.has_value(), ""); @@ -347,12 +350,12 @@ std::vector> Predicate::summaryStateValues(std::vecto std::vector::const_iterator stateLast; if (auto const* function = programFunction()) { - stateFirst = _args.begin() + 6 + static_cast(stateVars->size()) + static_cast(function->parameters().size()) + 1; + stateFirst = _args.begin() + static_cast(firstArgIndex()) + static_cast(stateVars->size()) + static_cast(function->parameters().size()) + 1; stateLast = stateFirst + static_cast(stateVars->size()); } else if (programContract()) { - stateFirst = _args.begin() + 7 + static_cast(stateVars->size()); + stateFirst = _args.begin() + static_cast(firstStateVarIndex()) + static_cast(stateVars->size()); stateLast = stateFirst + static_cast(stateVars->size()); } else if (programVariable()) @@ -371,7 +374,7 @@ std::vector> Predicate::summaryStateValues(std::vecto std::vector> Predicate::summaryPostInputValues(std::vector const& _args) const { - /// The signature of a function summary predicate is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars). + /// The signature of a function summary predicate is: summary(error, this, abiFunctions, (optionally) bytesConcatFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars). /// Here we are interested in postInputVars. auto const* function = programFunction(); solAssert(function, ""); @@ -381,7 +384,7 @@ std::vector> Predicate::summaryPostInputValues(std::v auto const& inParams = function->parameters(); - auto first = _args.begin() + 6 + static_cast(stateVars->size()) * 2 + static_cast(inParams.size()) + 1; + auto first = _args.begin() + static_cast(firstArgIndex()) + static_cast(stateVars->size()) * 2 + static_cast(inParams.size()) + 1; auto last = first + static_cast(inParams.size()); solAssert(first >= _args.begin() && first <= _args.end(), ""); @@ -395,7 +398,7 @@ std::vector> Predicate::summaryPostInputValues(std::v std::vector> Predicate::summaryPostOutputValues(std::vector const& _args) const { - /// The signature of a function summary predicate is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars). + /// The signature of a function summary predicate is: summary(error, this, abiFunctions, (optionally) bytesConcatFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars). /// Here we are interested in outputVars. auto const* function = programFunction(); solAssert(function, ""); @@ -405,7 +408,7 @@ std::vector> Predicate::summaryPostOutputValues(std:: auto const& inParams = function->parameters(); - auto first = _args.begin() + 6 + static_cast(stateVars->size()) * 2 + static_cast(inParams.size()) * 2 + 1; + auto first = _args.begin() + static_cast(firstArgIndex()) + static_cast(stateVars->size()) * 2 + static_cast(inParams.size()) * 2 + 1; solAssert(first >= _args.begin() && first <= _args.end(), ""); @@ -418,7 +421,7 @@ std::vector> Predicate::summaryPostOutputValues(std:: std::pair>, std::vector> Predicate::localVariableValues(std::vector const& _args) const { /// The signature of a local block predicate is: - /// block(error, this, abiFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars, localVars). + /// block(error, this, abiFunctions, (optionally) bytesConcatFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars, localVars). /// Here we are interested in localVars. auto const* function = programFunction(); solAssert(function, ""); @@ -452,19 +455,20 @@ std::map Predicate::expressionSubstitution(smtutil::Ex auto nArgs = _predExpr.arguments.size(); // The signature of an interface predicate is - // interface(this, abiFunctions, cryptoFunctions, blockchainState, stateVariables). + // interface(this, abiFunctions, (optionally) bytesConcatFunctions, cryptoFunctions, blockchainState, stateVariables). // An invariant for an interface predicate is a contract // invariant over its state, for example `x <= 0`. if (isInterface()) { + size_t shift = txValuesIndex(); solAssert(starts_with(predName, "interface"), ""); subst[_predExpr.arguments.at(0).name] = "address(this)"; - solAssert(nArgs == stateVars.size() + 4, ""); + solAssert(nArgs == stateVars.size() + shift, ""); for (size_t i = nArgs - stateVars.size(); i < nArgs; ++i) - subst[_predExpr.arguments.at(i).name] = stateVars.at(i - 4)->name(); + subst[_predExpr.arguments.at(i).name] = stateVars.at(i - shift)->name(); } // The signature of a nondet interface predicate is - // nondet_interface(error, this, abiFunctions, cryptoFunctions, blockchainState, stateVariables, blockchainState', stateVariables'). + // nondet_interface(error, this, abiFunctions, (optionally) bytesConcatFunctions, cryptoFunctions, blockchainState, stateVariables, blockchainState', stateVariables'). // An invariant for a nondet interface predicate is a reentrancy property // over the pre and post state variables of a contract, where pre state vars // are represented by the variable's name and post state vars are represented @@ -475,7 +479,7 @@ std::map Predicate::expressionSubstitution(smtutil::Ex solAssert(starts_with(predName, "nondet_interface"), ""); subst[_predExpr.arguments.at(0).name] = ""; subst[_predExpr.arguments.at(1).name] = "address(this)"; - solAssert(nArgs == stateVars.size() * 2 + 6, ""); + solAssert(nArgs == stateVars.size() * 2 + firstArgIndex(), ""); for (size_t i = nArgs - stateVars.size(), s = 0; i < nArgs; ++i, ++s) subst[_predExpr.arguments.at(i).name] = stateVars.at(s)->name() + "'"; for (size_t i = nArgs - (stateVars.size() * 2 + 1), s = 0; i < nArgs - (stateVars.size() + 1); ++i, ++s) diff --git a/libsolidity/formal/Predicate.h b/libsolidity/formal/Predicate.h index d7ac0da35223..638354f921dc 100644 --- a/libsolidity/formal/Predicate.h +++ b/libsolidity/formal/Predicate.h @@ -71,6 +71,7 @@ class Predicate Predicate( smt::SymbolicFunctionVariable&& _predicate, PredicateType _type, + bool _bytesConcatFunctionInContext, ASTNode const* _node = nullptr, ContractDefinition const* _contractContext = nullptr, std::vector _scopeStack = {} @@ -179,7 +180,7 @@ class Predicate /// @returns a substitution map from the arguments of _predExpr /// to a Solidity-like expression. - std::map expressionSubstitution(smtutil::Expression const& _predExpr) const; + std::map expressionSubstitution(smtutil::Expression const& _predExprs) const; private: /// @returns the formatted version of the given SMT expressions. Those expressions must be SMT constants. @@ -196,6 +197,13 @@ class Predicate std::map> readTxVars(smtutil::Expression const& _tx) const; + /// @returns index at which transaction values start in args list + size_t txValuesIndex() const { return m_bytesConcatFunctionInContext ? 5 : 4; } + /// @returns index at which function arguments start in args list + size_t firstArgIndex() const { return m_bytesConcatFunctionInContext ? 7 : 6; } + /// @returns index at which state variables values start in args list + size_t firstStateVarIndex() const { return m_bytesConcatFunctionInContext ? 8 : 7; } + /// The actual SMT expression. smt::SymbolicFunctionVariable m_predicate; @@ -219,6 +227,9 @@ class Predicate /// The scope stack when the predicate was created. /// Used to identify the subset of variables in scope. std::vector const m_scopeStack; + + /// True iff there is a bytes concat function in contract scope + bool m_bytesConcatFunctionInContext; }; struct PredicateCompare diff --git a/libsolidity/formal/PredicateInstance.cpp b/libsolidity/formal/PredicateInstance.cpp index 0bf352dd4777..b5b148cd48ed 100644 --- a/libsolidity/formal/PredicateInstance.cpp +++ b/libsolidity/formal/PredicateInstance.cpp @@ -29,14 +29,14 @@ namespace solidity::frontend::smt smtutil::Expression interfacePre(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context) { auto& state = _context.state(); - std::vector stateExprs{state.thisAddress(0), state.abi(0), state.crypto(0), state.state(0)}; + std::vector stateExprs = getStateExpressionsForInterfacePre(state); return _pred(stateExprs + initialStateVariables(_contract, _context)); } smtutil::Expression interface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context) { auto const& state = _context.state(); - std::vector stateExprs{state.thisAddress(0), state.abi(0), state.crypto(0), state.state()}; + std::vector stateExprs = getStateExpressionsForInterface(state); return _pred(stateExprs + currentStateVariables(_contract, _context)); } @@ -48,7 +48,7 @@ smtutil::Expression nondetInterface( unsigned _postIdx) { auto const& state = _context.state(); - std::vector stateExprs{state.errorFlag().currentValue(), state.thisAddress(), state.abi(), state.crypto()}; + std::vector stateExprs = getStateExpressionsForNondetInterface(state); return _pred( stateExprs + std::vector{_context.state().state(_preIdx)} + @@ -65,7 +65,7 @@ smtutil::Expression constructor(Predicate const& _pred, EncodingContext& _contex return _pred(currentFunctionVariablesForDefinition(*constructor, &contract, _context)); auto& state = _context.state(); - std::vector stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state(0), state.state()}; + std::vector stateExprs = getStateExpressionsForConstructor(state); return _pred(stateExprs + initialStateVariables(contract, _context) + currentStateVariables(contract, _context)); } @@ -76,7 +76,7 @@ smtutil::Expression constructorCall(Predicate const& _pred, EncodingContext& _co return _pred(currentFunctionVariablesForCall(*constructor, &contract, _context, _internal)); auto& state = _context.state(); - std::vector stateExprs{state.errorFlag().currentValue(), _internal ? state.thisAddress(0) : state.thisAddress(), state.abi(0), state.crypto(0), _internal ? state.tx(0) : state.tx(), state.state()}; + std::vector stateExprs = getStateExpressionsForCall(state, _internal); state.newState(); stateExprs += std::vector{state.state()}; stateExprs += currentStateVariables(contract, _context); @@ -152,7 +152,7 @@ std::vector currentFunctionVariablesForDefinition( ) { auto& state = _context.state(); - std::vector exprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state(0)}; + std::vector exprs = getStateExpressionsForDefinition(state); exprs += _contract ? initialStateVariables(*_contract, _context) : std::vector{}; exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->valueAtIndex(0); }); exprs += std::vector{state.state()}; @@ -170,7 +170,7 @@ std::vector currentFunctionVariablesForCall( ) { auto& state = _context.state(); - std::vector exprs{state.errorFlag().currentValue(), _internal ? state.thisAddress(0) : state.thisAddress(), state.abi(0), state.crypto(0), _internal ? state.tx(0) : state.tx(), state.state()}; + std::vector exprs = getStateExpressionsForCall(state, _internal); exprs += _contract ? currentStateVariables(*_contract, _context) : std::vector{}; exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); }); @@ -192,4 +192,52 @@ std::vector currentBlockVariables(FunctionDefinition const& ); } +std::vector getStateExpressionsForInterfacePre(SymbolicState const& _state) +{ + if (_state.hasBytesConcatFunction()) + return {_state.thisAddress(0), + _state.abi(0), _state.bytesConcat(0), _state.crypto(0), _state.state(0)}; +return {_state.thisAddress(0), _state.abi(0), _state.crypto(0), _state.state(0)}; +} + +std::vector getStateExpressionsForInterface(SymbolicState const& _state) +{ + if (_state.hasBytesConcatFunction()) + return {_state.thisAddress(0), _state.abi(0), _state.bytesConcat(0), _state.crypto(0), _state.state()}; + return {_state.thisAddress(0), _state.abi(0), _state.crypto(0), _state.state()}; +} + +std::vector getStateExpressionsForNondetInterface(SymbolicState const& _state) +{ + if (_state.hasBytesConcatFunction()) + return {_state.errorFlag().currentValue(), _state.thisAddress(), _state.abi(), _state.bytesConcat(), _state.crypto()}; + return {_state.errorFlag().currentValue(), _state.thisAddress(), _state.abi(), _state.crypto()}; +} + +std::vector getStateExpressionsForConstructor(SymbolicState const& _state) +{ + if (_state.hasBytesConcatFunction()) + return {_state.errorFlag().currentValue(), _state.thisAddress(0), _state.abi(0), + _state.bytesConcat(0), _state.crypto(0), _state.tx(0), _state.state(0), _state.state()}; + return {_state.errorFlag().currentValue(), _state.thisAddress(0), _state.abi(0), + _state.crypto(0), _state.tx(0), _state.state(0), _state.state()}; +} + +std::vector getStateExpressionsForCall(SymbolicState const& _state, bool _internal) +{ + if (_state.hasBytesConcatFunction()) + return {_state.errorFlag().currentValue(), _internal ? _state.thisAddress(0) : _state.thisAddress(), + _state.abi(0), _state.bytesConcat(0), _state.crypto(0), _internal ? _state.tx(0) : _state.tx(), _state.state()}; + return {_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 getStateExpressionsForDefinition(SymbolicState const& _state) +{ + if (_state.hasBytesConcatFunction()) + return {_state.errorFlag().currentValue(), _state.thisAddress(0), _state.abi(0), + _state.bytesConcat(0), _state.crypto(0), _state.tx(0), _state.state(0)}; + return {_state.errorFlag().currentValue(), _state.thisAddress(0), _state.abi(0), + _state.crypto(0), _state.tx(0), _state.state(0)}; +} } diff --git a/libsolidity/formal/PredicateInstance.h b/libsolidity/formal/PredicateInstance.h index 42a9e2040b36..33c8a8a0dde9 100644 --- a/libsolidity/formal/PredicateInstance.h +++ b/libsolidity/formal/PredicateInstance.h @@ -19,6 +19,7 @@ #pragma once #include +#include namespace solidity::frontend::smt { @@ -94,4 +95,10 @@ std::vector currentBlockVariables( EncodingContext& _context ); +std::vector getStateExpressionsForInterfacePre(SymbolicState const& _state); +std::vector getStateExpressionsForInterface(SymbolicState const& _state); +std::vector getStateExpressionsForNondetInterface(SymbolicState const& _state); +std::vector getStateExpressionsForConstructor(SymbolicState const& _state); +std::vector getStateExpressionsForCall(SymbolicState const& _state, bool _internal); +std::vector getStateExpressionsForDefinition(SymbolicState const& _state); } diff --git a/libsolidity/formal/PredicateSort.cpp b/libsolidity/formal/PredicateSort.cpp index 2e95a29a531d..0f9eae82c423 100644 --- a/libsolidity/formal/PredicateSort.cpp +++ b/libsolidity/formal/PredicateSort.cpp @@ -30,7 +30,10 @@ namespace solidity::frontend::smt SortPointer interfaceSort(ContractDefinition const& _contract, SymbolicState& _state) { return std::make_shared( - std::vector{_state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.stateSort()} + stateSorts(_contract), + std::vector{_state.thisAddressSort()} + + getBuiltInFunctionsSorts(_state) + + std::vector{_state.stateSort()} + + stateSorts(_contract), SortProvider::boolSort ); } @@ -40,7 +43,8 @@ SortPointer nondetInterfaceSort(ContractDefinition const& _contract, SymbolicSta auto varSorts = stateSorts(_contract); std::vector stateSort{_state.stateSort()}; return std::make_shared( - std::vector{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort()} + + std::vector{_state.errorFlagSort(), _state.thisAddressSort()} + + getBuiltInFunctionsSorts(_state) + stateSort + varSorts + stateSort + @@ -57,7 +61,10 @@ SortPointer constructorSort(ContractDefinition const& _contract, SymbolicState& auto varSorts = stateSorts(_contract); std::vector stateSort{_state.stateSort()}; return std::make_shared( - std::vector{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort(), _state.stateSort()} + varSorts + varSorts, + std::vector{_state.errorFlagSort(), _state.thisAddressSort()} + + getBuiltInFunctionsSorts(_state) + + std::vector{_state.txSort(), _state.stateSort(), _state.stateSort()} + + varSorts + varSorts, SortProvider::boolSort ); } @@ -69,7 +76,9 @@ SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition auto inputSorts = applyMap(_function.parameters(), smtSort); auto outputSorts = applyMap(_function.returnParameters(), smtSort); return std::make_shared( - std::vector{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort()} + + std::vector{_state.errorFlagSort(), _state.thisAddressSort()} + + getBuiltInFunctionsSorts(_state) + + std::vector{_state.txSort(), _state.stateSort()} + varSorts + inputSorts + std::vector{_state.stateSort()} + @@ -110,4 +119,10 @@ std::vector stateSorts(ContractDefinition const& _contract) ); } +std::vector getBuiltInFunctionsSorts(SymbolicState& _state) +{ + if (_state.hasBytesConcatFunction()) + return {_state.abiSort(), _state.bytesConcatSort(), _state.cryptoSort()}; + return {_state.abiSort(), _state.cryptoSort()}; +} } diff --git a/libsolidity/formal/PredicateSort.h b/libsolidity/formal/PredicateSort.h index 5638582546e9..c5f63f2a6965 100644 --- a/libsolidity/formal/PredicateSort.h +++ b/libsolidity/formal/PredicateSort.h @@ -74,6 +74,8 @@ smtutil::SortPointer arity0FunctionSort(); /// Helpers -std::vector stateSorts(ContractDefinition const& _contract) ; +std::vector stateSorts(ContractDefinition const& _contract); + +std::vector getBuiltInFunctionsSorts(SymbolicState& _state); } diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index ae3a06869d19..61aad0e8f526 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -651,6 +651,9 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall) if (publicGetter(_funCall.expression())) visitPublicGetter(_funCall); break; + case FunctionType::Kind::BytesConcat: + visitBytesConcat(_funCall); + break; case FunctionType::Kind::ABIDecode: case FunctionType::Kind::ABIEncode: case FunctionType::Kind::ABIEncodePacked: @@ -780,6 +783,33 @@ void SMTEncoder::visitRequire(FunctionCall const& _funCall) addPathImpliedExpression(expr(*args.front())); } +void SMTEncoder::visitBytesConcat(FunctionCall const& _funCall) +{ + auto const& args = _funCall.sortedArguments(); + + // bytes.concat call with no arguments returns an empty array + if (args.size() == 0) + { + defineExpr(_funCall, smt::zeroValue(TypeProvider::bytesMemory())); + return; + } + + // bytes.concat with single argument of type bytes memory + if (args.size() == 1 && args.front()->annotation().type->category() == frontend::Type::Category::Array) + { + defineExpr(_funCall, expr(*args.front(), TypeProvider::bytesMemory())); + return; + } + + auto const& [name, inTypes, outType] = state().bytesConcatFunctionTypes(&_funCall); + solAssert(inTypes.size() == args.size(), ""); + + auto symbFunction = state().bytesConcatFunction(&_funCall); + auto out = createSelectExpressionForFunction(symbFunction, args, inTypes, args.size()); + + defineExpr(_funCall, out); +} + void SMTEncoder::visitABIFunction(FunctionCall const& _funCall) { auto symbFunction = state().abiFunction(&_funCall); @@ -796,24 +826,8 @@ void SMTEncoder::visitABIFunction(FunctionCall const& _funCall) defineExpr(_funCall, smt::zeroValue(TypeProvider::bytesMemory())); return; } - std::vector symbArgs; - for (unsigned i = 0; i < argsActualLength; ++i) - if (args.at(i)) - symbArgs.emplace_back(expr(*args.at(i), inTypes.at(i))); - std::optional arg; - if (inTypes.size() == 1) - arg = expr(*args.at(0), inTypes.at(0)); - else - { - auto inputSort = dynamic_cast(*symbFunction.sort).domain; - arg = smtutil::Expression::tuple_constructor( - smtutil::Expression(std::make_shared(inputSort), ""), - symbArgs - ); - } - - auto out = smtutil::Expression::select(symbFunction, *arg); + auto out = createSelectExpressionForFunction(symbFunction, args, inTypes, argsActualLength); if (outTypes.size() == 1) defineExpr(_funCall, out); else @@ -909,7 +923,6 @@ void SMTEncoder::visitObjectCreation(FunctionCall const& _funCall) smtutil::Expression arraySize = expr(*args.front()); setSymbolicUnknownValue(arraySize, TypeProvider::uint256(), m_context); - auto symbArray = std::dynamic_pointer_cast(m_context.expression(_funCall)); solAssert(symbArray, ""); smt::setSymbolicZeroValue(*symbArray, m_context); @@ -3112,6 +3125,29 @@ std::set> SMTEncoder::collectA return ABIFunctions(_node).abiCalls; } +std::set> SMTEncoder::collectBytesConcatCalls(ASTNode const* _node) +{ + struct BytesConcatFunctions: public ASTConstVisitor + { + BytesConcatFunctions(ASTNode const* _node) { _node->accept(*this); } + void endVisit(FunctionCall const& _funCall) + { + if (*_funCall.annotation().kind == FunctionCallKind::FunctionCall) + switch (dynamic_cast(*_funCall.expression().annotation().type).kind()) + { + case FunctionType::Kind::BytesConcat: + bytesConcatCalls.insert(&_funCall); + break; + default: {} + } + } + + std::set> bytesConcatCalls; + }; + + return BytesConcatFunctions(_node).bytesConcatCalls; +} + std::set SMTEncoder::sourceDependencies(SourceUnit const& _source) { std::set sources; @@ -3216,3 +3252,30 @@ smt::SymbolicState& SMTEncoder::state() { return m_context.state(); } + +smtutil::Expression SMTEncoder::createSelectExpressionForFunction( + smtutil::Expression symbFunction, + std::vector> const& args, + frontend::TypePointers const& inTypes, + unsigned long argsActualLength +) +{ + solAssert(argsActualLength <= args.size() && inTypes.size() == argsActualLength); + if (inTypes.size() == 1) + { + smtutil::Expression arg = expr(*args.at(0), inTypes.at(0)); + return smtutil::Expression::select(symbFunction, arg); + } + + std::vector symbArgs; + for (unsigned i = 0; i < argsActualLength; ++i) + if (args.at(i)) + symbArgs.emplace_back(expr(*args.at(i), inTypes.at(i))); + + auto inputSort = dynamic_cast(*symbFunction.sort).domain; + smtutil::Expression arg = smtutil::Expression::tuple_constructor( + smtutil::Expression(std::make_shared(inputSort), ""), + symbArgs + ); + return smtutil::Expression::select(symbFunction, arg); +} diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 69010fb1cf54..be676930cab1 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -122,6 +122,7 @@ class SMTEncoder: public ASTConstVisitor static RationalNumberType const* isConstant(Expression const& _expr); static std::set> collectABICalls(ASTNode const* _node); + static std::set> collectBytesConcatCalls(ASTNode const* _node); /// @returns all the sources that @param _source depends on, /// including itself. @@ -211,6 +212,7 @@ class SMTEncoder: public ASTConstVisitor void visitAssert(FunctionCall const& _funCall); void visitRequire(FunctionCall const& _funCall); void visitABIFunction(FunctionCall const& _funCall); + void visitBytesConcat(FunctionCall const& _funCall); void visitCryptoFunction(FunctionCall const& _funCall); void visitGasLeft(FunctionCall const& _funCall); virtual void visitAddMulMod(FunctionCall const& _funCall); @@ -500,6 +502,14 @@ class SMTEncoder: public ASTConstVisitor langutil::CharStreamProvider const& m_charStreamProvider; smt::SymbolicState& state(); + +private: + smtutil::Expression createSelectExpressionForFunction( + smtutil::Expression symbFunction, + std::vector> const& args, + frontend::TypePointers const& inTypes, + unsigned long argsActualLength + ); }; } diff --git a/libsolidity/formal/SymbolicState.cpp b/libsolidity/formal/SymbolicState.cpp index 3859e99c6243..bf835b801d21 100644 --- a/libsolidity/formal/SymbolicState.cpp +++ b/libsolidity/formal/SymbolicState.cpp @@ -268,16 +268,19 @@ void SymbolicState::prepareForSourceUnit(SourceUnit const& _source, bool _storag auto allSources = _source.referencedSourceUnits(true); allSources.insert(&_source); std::set> abiCalls; + std::set> bytesConcatCalls; std::set> contracts; for (auto const& source: allSources) { abiCalls += SMTEncoder::collectABICalls(source); + bytesConcatCalls += SMTEncoder::collectBytesConcatCalls(source); for (auto node: source->nodes()) if (auto contract = dynamic_cast(node.get())) contracts.insert(contract); } buildState(contracts, _storage); buildABIFunctions(abiCalls); + buildBytesConcatFunctions(bytesConcatCalls); } /// Private helpers. @@ -355,6 +358,80 @@ void SymbolicState::buildState(std::set> const& _bytesConcatCalls) +{ + std::map functions; + + for (auto const* funCall: _bytesConcatCalls) + { + auto t = dynamic_cast(funCall->expression().annotation().type); + solAssert(t->kind() == FunctionType::Kind::BytesConcat, "Expected bytes.concat function"); + + auto const& args = funCall->sortedArguments(); + + auto argTypes = [](auto const& _args) { + return util::applyMap(_args, [](auto arg) { return arg->annotation().type; }); + }; + + // bytes.concat : (bytes/literal/fixed bytes, ... ) -> bytes + std::vector inTypes = argTypes(args); + + auto replaceUserDefinedValueTypes = [](auto& _types) { + for (auto& t: _types) + if (auto userType = dynamic_cast(t)) + t = &userType->underlyingType(); + }; + auto replaceStringLiteralTypes = [](auto& _types) { + for (auto& t: _types) + if (t->category() == frontend::Type::Category::StringLiteral) + t = TypeProvider::bytesMemory(); + }; + replaceUserDefinedValueTypes(inTypes); + replaceStringLiteralTypes(inTypes); + + auto name = t->richIdentifier(); + for (auto paramType: inTypes) + name += "_" + paramType->richIdentifier(); + + frontend::Type const* outType = TypeProvider::bytesMemory(); + name += "_" + outType->richIdentifier(); + + m_bytesConcatMembers[funCall] = {name, inTypes, outType}; + + if (functions.count(name)) + continue; + + /// If there is only one parameter, we use that type directly. + /// Otherwise we create a tuple wrapping the necessary types. + auto typesToSort = [](auto const& _types, std::string const& _name) -> std::shared_ptr { + if (_types.size() == 1) + return smtSortAbstractFunction(*_types.front()); + + std::vector inNames; + std::vector sorts; + for (unsigned i = 0; i < _types.size(); ++i) + { + inNames.emplace_back(_name + "_input_" + std::to_string(i)); + sorts.emplace_back(smtSortAbstractFunction(*_types.at(i))); + } + return std::make_shared( + _name + "_input", + inNames, + sorts + ); + }; + + auto functionSort = std::make_shared( + typesToSort(inTypes, name), + smtSortAbstractFunction(*outType) + ); + + functions[name] = functionSort; + } + + m_bytesConcat = std::make_unique("bytesConcat", std::move(functions), m_context); +} + void SymbolicState::buildABIFunctions(std::set> const& _abiFunctions) { std::map functions; @@ -367,7 +444,6 @@ void SymbolicState::buildABIFunctions(std::setparameterTypes(); auto const& returnTypes = t->returnParameterTypes(); - auto argTypes = [](auto const& _args) { return util::applyMap(_args, [](auto arg) { return arg->annotation().type; }); }; @@ -493,3 +569,14 @@ SymbolicState::SymbolicABIFunction const& SymbolicState::abiFunctionTypes(Functi { return m_abiMembers.at(_funCall); } + +smtutil::Expression SymbolicState::bytesConcatFunction(frontend::FunctionCall const* _funCall) +{ + solAssert(m_bytesConcat, ""); + return m_bytesConcat->member(std::get<0>(m_bytesConcatMembers.at(_funCall))); +} + +SymbolicState::SymbolicBytesConcatFunction const& SymbolicState::bytesConcatFunctionTypes(FunctionCall const* _funCall) const +{ + return m_bytesConcatMembers.at(_funCall); +} diff --git a/libsolidity/formal/SymbolicState.h b/libsolidity/formal/SymbolicState.h index 7fe5b028d627..ac018df1acf8 100644 --- a/libsolidity/formal/SymbolicState.h +++ b/libsolidity/formal/SymbolicState.h @@ -182,7 +182,21 @@ class SymbolicState smtutil::Expression abi() const { solAssert(m_abi, ""); return m_abi->value(); } smtutil::Expression abi(unsigned _idx) const { solAssert(m_abi, ""); return m_abi->value(_idx); } smtutil::SortPointer const& abiSort() const { solAssert(m_abi, ""); return m_abi->sort(); } - void newABI() { solAssert(m_abi, ""); m_abi->newVar(); } + //@} + + /// bytes.concat functions. + //@{ + smtutil::Expression bytesConcatFunction(FunctionCall const* _funCall); + using SymbolicBytesConcatFunction = std::tuple< + std::string, + std::vector, + frontend::Type const* + >; + SymbolicBytesConcatFunction const& bytesConcatFunctionTypes(FunctionCall const* _funCall) const; + smtutil::Expression bytesConcat() const { solAssert(m_bytesConcat, ""); return m_bytesConcat->value(); } + smtutil::Expression bytesConcat(unsigned _idx) const { solAssert(m_bytesConcat, ""); return m_bytesConcat->value(_idx); } + smtutil::SortPointer const& bytesConcatSort() const { solAssert(m_bytesConcat, ""); return m_bytesConcat->sort(); } + bool hasBytesConcatFunction() const {solAssert(m_bytesConcat, ""); return !m_bytesConcatMembers.empty(); } //@} private: @@ -196,6 +210,9 @@ class SymbolicState /// Builds m_abi based on the abi.* calls _abiFunctions. void buildABIFunctions(std::set> const& _abiFunctions); + /// Builds m_bytesConcat based on the bytes.concat calls + void buildBytesConcatFunctions(std::set> const& _bytesConcatCalls); + EncodingContext& m_context; SymbolicIntVariable m_error{ @@ -278,6 +295,12 @@ class SymbolicState /// Maps ABI functions calls to their tuple names generated by /// `buildABIFunctions`. std::map m_abiMembers; + + /// Tuple containing all used bytes.concat functions. + std::unique_ptr m_bytesConcat; + /// Maps bytes.concat functions calls to their tuple names generated by + /// `buildBytesConcatFunctions`. + std::map m_bytesConcatMembers; }; } diff --git a/test/libsolidity/smtCheckerTests/bytes_concat/equals.sol b/test/libsolidity/smtCheckerTests/bytes_concat/equals.sol new file mode 100644 index 000000000000..334a2e0c5ff4 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/bytes_concat/equals.sol @@ -0,0 +1,52 @@ +contract C { + + function concatCall(bytes8 a) public pure returns (bytes memory) { + return bytes.concat(a, a); + } + + function equalArguments1(bytes8 a, bytes8 b, bytes8 c, bytes8 d) public pure { + require(a == c); + require(b == d); + bytes memory concat1 = bytes.concat(a, b); + bytes memory concat2 = bytes.concat(c, d); + assert(keccak256(concat1) == keccak256(concat2)); + } + + function equalArguments2(bytes8 a, bytes8 c) public pure { + require(a == c); + bytes memory concat1 = bytes.concat(a, concatCall(a)); + bytes memory concat2 = bytes.concat(c, concatCall(c)); + assert(keccak256(concat1) == keccak256(concat2)); + } + + function equalLengthFixedBytes(bytes8 a, bytes8 b) public pure { + bytes memory concat1 = bytes.concat(a, b); + bytes memory concat2 = bytes.concat(a, b); + assert(concat1.length == concat2.length); + } + + function equalLengthMemoryBytes(bytes memory a, bytes memory b) public pure { + bytes memory concat1 = bytes.concat(a, b); + bytes memory concat2 = bytes.concat(a, b); + assert(concat1.length == concat2.length); + } + + function equalLengthMixed(bytes memory a, bytes2 b) public pure { + bytes memory concat1 = bytes.concat(a, b); + bytes memory concat2 = bytes.concat(a, b); + assert(concat1.length == concat2.length); + } + + function equalLengthLiterals() public pure { + bytes memory a = hex"aa"; + bytes1 b = bytes1(0xbb); + bytes memory c = "c"; + bytes memory concat1 = bytes.concat(a, b, c); + bytes memory concat2 = bytes.concat(a, b, c); + assert(concat1.length == concat2.length); + } +} +// ==== +// SMTEngine: all +// ---- +// Info 1391: CHC: 6 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/bytes_concat/one_arg_call.sol b/test/libsolidity/smtCheckerTests/bytes_concat/one_arg_call.sol new file mode 100644 index 000000000000..4f539f3184d0 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/bytes_concat/one_arg_call.sol @@ -0,0 +1,10 @@ +contract C { + function oneArg(bytes memory a) public pure { + bytes memory concat = bytes.concat(a); + assert(keccak256(a) == keccak256(concat)); + } +} +// ==== +// SMTEngine: all +// ---- +// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/bytes_concat/simple.sol b/test/libsolidity/smtCheckerTests/bytes_concat/simple.sol new file mode 100644 index 000000000000..834d89ee9b4e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/bytes_concat/simple.sol @@ -0,0 +1,35 @@ +contract C { + function zeroArgs() public pure returns(bytes memory) { + bytes memory a = bytes.concat(); + assert(a.length == 0); // zero args call is an empty bytes array + return bytes.concat(); + } + + function oneArg(bytes memory a) public pure returns(bytes memory) { + return bytes.concat(a); + } + + function oneArgFixedBytes(bytes8 a) public pure returns(bytes memory) { + return bytes.concat(a); + } + + function fixedBytes(bytes8 a, bytes8 b) public pure returns(bytes memory) { + return bytes.concat(a, b); + } + + function memoryBytes(bytes memory a, bytes memory b) public pure returns(bytes memory) { + return bytes.concat(a, b); + } + + function mixed(bytes memory a, bytes2 b) public pure returns(bytes memory) { + return bytes.concat(a, b, "StringLiteral"); + } + + function functionCallAsArg(bytes memory a) public pure returns(bytes memory) { + return bytes.concat(oneArg(a), zeroArgs()); + } +} +// ==== +// SMTEngine: all +// ---- +// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol index eb0a0c0498ae..09f001719fbe 100644 --- a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol +++ b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol @@ -21,8 +21,10 @@ contract C { // SMTIgnoreOS: macos // ---- // Warning 4984: (47-50): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. +// Warning 6328: (167-185): CHC: Assertion violation might happen here. // Warning 6328: (215-233): CHC: Assertion violation might happen here. // Warning 6328: (304-322): CHC: Assertion violation happens here. -// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. +// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. // Warning 2661: (47-50): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. +// Warning 4661: (167-185): BMC: Assertion violation happens here. // Warning 4661: (215-233): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/index_access_side_effect.sol b/test/libsolidity/smtCheckerTests/operators/index_access_side_effect.sol index d18f605f7c5e..32c9780d1134 100644 --- a/test/libsolidity/smtCheckerTests/operators/index_access_side_effect.sol +++ b/test/libsolidity/smtCheckerTests/operators/index_access_side_effect.sol @@ -23,6 +23,4 @@ contract C { // SMTIgnoreCex: yes // SMTIgnoreOS: macos // ---- -// Warning 6328: (335-354): CHC: Assertion violation might happen here. -// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. -// Warning 4661: (335-354): BMC: Assertion violation happens here. +// Info 1391: CHC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_operator_matches_equivalent_function_call.sol b/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_operator_matches_equivalent_function_call.sol index a6cad9580f72..b734079c7df5 100644 --- a/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_operator_matches_equivalent_function_call.sol +++ b/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_operator_matches_equivalent_function_call.sol @@ -63,12 +63,15 @@ contract C { // Warning 4984: (953-982): CHC: Overflow (resulting value larger than 32767) might happen here. // Warning 4984: (1051-1080): CHC: Overflow (resulting value larger than 32767) might happen here. // Warning 4281: (1051-1080): CHC: Division by zero might happen here. -// Warning 4281: (1149-1178): CHC: Division by zero happens here. +// Warning 4281: (1149-1178): CHC: Division by zero might happen here. +// Warning 6328: (2069-2095): CHC: Assertion violation might happen here. // Warning 6328: (2105-2131): CHC: Assertion violation might happen here. // Warning 6328: (2141-2163): CHC: Assertion violation might happen here. +// Warning 6328: (2173-2199): CHC: Assertion violation might happen here. // Warning 6328: (2209-2235): CHC: Assertion violation might happen here. // Warning 6328: (2245-2271): CHC: Assertion violation might happen here. -// Info 1391: CHC: 12 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. +// Info 1391: CHC: 10 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. // Warning 3046: (1051-1080): BMC: Division by zero happens here. +// Warning 3046: (1149-1178): BMC: Division by zero happens here. // Warning 7812: (2245-2271): BMC: Assertion violation might happen here. -// Info 6002: BMC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. +// Info 6002: BMC: 6 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/typecast/function_type_to_function_type_internal.sol b/test/libsolidity/smtCheckerTests/typecast/function_type_to_function_type_internal.sol index 2d3448ee7b0d..368e9c922f6c 100644 --- a/test/libsolidity/smtCheckerTests/typecast/function_type_to_function_type_internal.sol +++ b/test/libsolidity/smtCheckerTests/typecast/function_type_to_function_type_internal.sol @@ -1,10 +1,10 @@ contract C { function(uint) returns (uint) a; function(uint) returns (uint) b; - function f(function(uint) returns (uint) g, function(uint) returns (uint) h) internal { + function f(function(uint) returns (uint) g, function(uint) returns (uint) h) internal { assert(g(2) == h(2)); assert(g == h); - } + } function g() public { f(a, b); } @@ -12,11 +12,11 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 2519: (96-127): This declaration shadows an existing declaration. -// Warning 6031: (182-186): Internal error: Expression undefined for SMT solver. -// Warning 6031: (190-194): Internal error: Expression undefined for SMT solver. -// Warning 7229: (206-212): Assertion checker does not yet implement the type function (uint256) returns (uint256) for comparisons -// Warning 5729: (182-186): BMC does not yet implement this type of function call. -// Warning 5729: (190-194): BMC does not yet implement this type of function call. -// Warning 6328: (175-195): CHC: Assertion violation happens here. -// Warning 6328: (199-213): CHC: Assertion violation happens here. +// Warning 2519: (93-124): This declaration shadows an existing declaration. +// Warning 6031: (179-183): Internal error: Expression undefined for SMT solver. +// Warning 6031: (187-191): Internal error: Expression undefined for SMT solver. +// Warning 7229: (203-209): Assertion checker does not yet implement the type function (uint256) returns (uint256) for comparisons +// Warning 5729: (179-183): BMC does not yet implement this type of function call. +// Warning 5729: (187-191): BMC does not yet implement this type of function call. +// Warning 6328: (172-192): CHC: Assertion violation happens here. +// Warning 6328: (196-210): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol b/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol index 5ac20c96f869..fce586987795 100644 --- a/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol +++ b/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol @@ -45,4 +45,5 @@ contract C // Warning 6368: (850-866): CHC: Out of bounds access happens here. // Warning 6368: (850-869): CHC: Out of bounds access happens here. // Warning 6328: (936-956): CHC: Assertion violation happens here. -// Info 1391: CHC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. +// Warning 6368: (1029-1043): CHC: Out of bounds access might happen here. +// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.