diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index bc20f3319..1111a37dd 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -916,7 +916,7 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source) auto nondetPre = smt::nondetInterface(iface, *contract, m_context, 0, 1); auto nondetPost = smt::nondetInterface(iface, *contract, m_context, 0, 2); - vector args{errorFlag().currentValue(), state().thisAddress(), state().crypto(), state().tx(), state().state(1)}; + vector args{errorFlag().currentValue(), state().thisAddress(), state().abi(), state().crypto(), state().tx(), state().state(1)}; args += state1 + applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); }) + vector{state().state(2)} + @@ -1160,7 +1160,7 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall) solAssert(false, "Unreachable!"); }; errorFlag().increaseIndex(); - vector args{errorFlag().currentValue(), contractAddressValue(_funCall), state().crypto(), state().tx(), state().state()}; + vector args{errorFlag().currentValue(), contractAddressValue(_funCall), state().abi(), state().crypto(), state().tx(), state().state()}; auto const* contract = function->annotation().contract; auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts; diff --git a/libsolidity/formal/Predicate.cpp b/libsolidity/formal/Predicate.cpp index b95738eaf..3255e7937 100644 --- a/libsolidity/formal/Predicate.cpp +++ b/libsolidity/formal/Predicate.cpp @@ -161,9 +161,9 @@ string Predicate::formatSummaryCall(vector const& _args) co auto const* fun = programFunction(); solAssert(fun, ""); - /// The signature of a function summary predicate is: summary(error, this, 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. - auto first = _args.begin() + 5 + static_cast(stateVars->size()); + auto first = _args.begin() + 6 + 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(), ""); @@ -189,8 +189,8 @@ string Predicate::formatSummaryCall(vector const& _args) co vector> Predicate::summaryStateValues(vector const& _args) const { - /// The signature of a function summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars). - /// The signature of the summary predicate of a contract without constructor is: summary(error, this, cryptoFunctions, txData, preBlockchainState, postBlockchainState, preStateVars, postStateVars). + /// 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). /// Here we are interested in postStateVars. auto stateVars = stateVariables(); solAssert(stateVars.has_value(), ""); @@ -199,12 +199,12 @@ vector> Predicate::summaryStateValues(vector::const_iterator stateLast; if (auto const* function = programFunction()) { - stateFirst = _args.begin() + 5 + static_cast(stateVars->size()) + static_cast(function->parameters().size()) + 1; + stateFirst = _args.begin() + 6 + static_cast(stateVars->size()) + static_cast(function->parameters().size()) + 1; stateLast = stateFirst + static_cast(stateVars->size()); } else if (programContract()) { - stateFirst = _args.begin() + 6 + static_cast(stateVars->size()); + stateFirst = _args.begin() + 7 + static_cast(stateVars->size()); stateLast = stateFirst + static_cast(stateVars->size()); } else @@ -221,7 +221,7 @@ vector> Predicate::summaryStateValues(vector> Predicate::summaryPostInputValues(vector const& _args) const { - /// The signature of a function summary predicate is: summary(error, this, 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. auto const* function = programFunction(); solAssert(function, ""); @@ -231,7 +231,7 @@ vector> Predicate::summaryPostInputValues(vectorparameters(); - auto first = _args.begin() + 5 + static_cast(stateVars->size()) * 2 + static_cast(inParams.size()) + 1; + auto first = _args.begin() + 6 + static_cast(stateVars->size()) * 2 + static_cast(inParams.size()) + 1; auto last = first + static_cast(inParams.size()); solAssert(first >= _args.begin() && first <= _args.end(), ""); @@ -245,7 +245,7 @@ vector> Predicate::summaryPostInputValues(vector> Predicate::summaryPostOutputValues(vector const& _args) const { - /// The signature of a function summary predicate is: summary(error, this, 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. auto const* function = programFunction(); solAssert(function, ""); @@ -255,7 +255,7 @@ vector> Predicate::summaryPostOutputValues(vectorparameters(); - auto first = _args.begin() + 5 + static_cast(stateVars->size()) * 2 + static_cast(inParams.size()) * 2 + 1; + auto first = _args.begin() + 6 + static_cast(stateVars->size()) * 2 + static_cast(inParams.size()) * 2 + 1; solAssert(first >= _args.begin() && first <= _args.end(), ""); @@ -311,6 +311,11 @@ optional Predicate::expressionToString(smtutil::Expression const& _expr, { return {}; } + catch(invalid_argument const&) + { + return {}; + } + // Limit this counterexample size to 1k. // Some OSs give you "unlimited" memory through swap and other virtual memory, // so purely relying on bad_alloc being thrown is not a good idea. @@ -382,6 +387,10 @@ bool Predicate::fillArray(smtutil::Expression const& _expr, vector& _arr { return true; } + catch (invalid_argument const&) + { + return true; + } optional elemStr = expressionToString(_expr.arguments.at(2), _type.baseType()); if (!elemStr) return false; diff --git a/libsolidity/formal/PredicateInstance.cpp b/libsolidity/formal/PredicateInstance.cpp index 53cc03c79..0e8848485 100644 --- a/libsolidity/formal/PredicateInstance.cpp +++ b/libsolidity/formal/PredicateInstance.cpp @@ -30,14 +30,14 @@ namespace solidity::frontend::smt smtutil::Expression interfacePre(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context) { auto& state = _context.state(); - vector stateExprs{state.thisAddress(0), state.crypto(0), state.state(0)}; + vector stateExprs{state.thisAddress(0), state.abi(0), state.crypto(0), state.state(0)}; return _pred(stateExprs + initialStateVariables(_contract, _context)); } smtutil::Expression interface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context) { auto& state = _context.state(); - vector stateExprs{state.thisAddress(0), state.crypto(0), state.state()}; + vector stateExprs{state.thisAddress(0), state.abi(0), state.crypto(0), state.state()}; return _pred(stateExprs + currentStateVariables(_contract, _context)); } @@ -58,7 +58,7 @@ smtutil::Expression constructor(Predicate const& _pred, EncodingContext& _contex return _pred(currentFunctionVariablesForDefinition(*constructor, &contract, _context)); auto& state = _context.state(); - vector stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.crypto(0), state.tx(0), state.state(0), state.state()}; + vector 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)); } @@ -69,7 +69,7 @@ smtutil::Expression constructorCall(Predicate const& _pred, EncodingContext& _co return _pred(currentFunctionVariablesForCall(*constructor, &contract, _context)); auto& state = _context.state(); - vector stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.crypto(0), state.tx(0), state.state()}; + vector stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state()}; state.newState(); stateExprs += vector{state.state()}; stateExprs += currentStateVariables(contract, _context); @@ -145,7 +145,7 @@ vector currentFunctionVariablesForDefinition( ) { auto& state = _context.state(); - vector exprs{state.errorFlag().currentValue(), state.thisAddress(0), state.crypto(0), state.tx(0), state.state(0)}; + vector 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{}; exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->valueAtIndex(0); }); exprs += vector{state.state()}; @@ -162,7 +162,7 @@ vector currentFunctionVariablesForCall( ) { auto& state = _context.state(); - vector exprs{state.errorFlag().currentValue(), state.thisAddress(0), state.crypto(0), state.tx(0), state.state()}; + vector exprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state()}; exprs += _contract ? currentStateVariables(*_contract, _context) : vector{}; exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); }); diff --git a/libsolidity/formal/PredicateSort.cpp b/libsolidity/formal/PredicateSort.cpp index 2c3443bc6..e7f3e8540 100644 --- a/libsolidity/formal/PredicateSort.cpp +++ b/libsolidity/formal/PredicateSort.cpp @@ -31,7 +31,7 @@ namespace solidity::frontend::smt SortPointer interfaceSort(ContractDefinition const& _contract, SymbolicState& _state) { return make_shared( - vector{_state.thisAddressSort(), _state.cryptoSort(), _state.stateSort()} + stateSorts(_contract), + vector{_state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.stateSort()} + stateSorts(_contract), SortProvider::boolSort ); } @@ -54,7 +54,7 @@ SortPointer constructorSort(ContractDefinition const& _contract, SymbolicState& auto varSorts = stateSorts(_contract); vector stateSort{_state.stateSort()}; return make_shared( - vector{_state.errorFlagSort(), _state.thisAddressSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort(), _state.stateSort()} + varSorts + varSorts, + vector{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort(), _state.stateSort()} + varSorts + varSorts, SortProvider::boolSort ); } @@ -66,7 +66,7 @@ SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition auto inputSorts = applyMap(_function.parameters(), smtSort); auto outputSorts = applyMap(_function.returnParameters(), smtSort); return make_shared( - vector{_state.errorFlagSort(), _state.thisAddressSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort()} + + vector{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort()} + varSorts + inputSorts + vector{_state.stateSort()} + diff --git a/libsolidity/formal/PredicateSort.h b/libsolidity/formal/PredicateSort.h index b30d09a71..b1d1f61c2 100644 --- a/libsolidity/formal/PredicateSort.h +++ b/libsolidity/formal/PredicateSort.h @@ -33,7 +33,7 @@ namespace solidity::frontend::smt * * 1. Interface * The idle state of a contract. Signature: - * interface(this, cryptoFunctions, blockchainState, stateVariables). + * interface(this, abiFunctions, cryptoFunctions, blockchainState, stateVariables). * * 2. Nondet interface * The nondeterminism behavior of a contract. Signature: @@ -43,15 +43,15 @@ namespace solidity::frontend::smt * The summary of a contract's deployment procedure. * Signature: * If the contract has a constructor function, this is the same as the summary of that function. Otherwise: - * constructor_summary(error, this, cryptoFunctions, txData, blockchainState, blockchainState', stateVariables, stateVariables'). + * constructor_summary(error, this, abiFunctions, cryptoFunctions, txData, blockchainState, blockchainState', stateVariables, stateVariables'). * * 4. Function entry/summary * The entry point of a function definition. Signature: - * function_entry(error, this, cryptoFunctions, txData, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables'). + * function_entry(error, this, abiFunctions, cryptoFunctions, txData, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables'). * * 5. Function body * Use for any predicate within a function. Signature: - * function_body(error, this, txData, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables', localVariables). + * function_body(error, this, abiFunctions, cryptoFunctions, txData, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables', localVariables). */ /// @returns the interface predicate sort for _contract. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 8b7bbcc8e..23e6f5cb7 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -71,7 +71,12 @@ bool SMTEncoder::analyze(SourceUnit const& _source) analysis = false; } - return analysis; + if (!analysis) + return false; + + m_context.state().prepareForSourceUnit(_source); + + return true; } bool SMTEncoder::visit(ContractDefinition const& _contract) @@ -680,13 +685,15 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall) if (isPublicGetter(_funCall.expression())) visitPublicGetter(_funCall); break; + case FunctionType::Kind::ABIDecode: + case FunctionType::Kind::ABIEncode: + case FunctionType::Kind::ABIEncodePacked: + case FunctionType::Kind::ABIEncodeWithSelector: + case FunctionType::Kind::ABIEncodeWithSignature: + visitABIFunction(_funCall); + break; case FunctionType::Kind::Internal: - case FunctionType::Kind::DelegateCall: - case FunctionType::Kind::BareCall: - case FunctionType::Kind::BareCallCode: - case FunctionType::Kind::BareDelegateCall: case FunctionType::Kind::BareStaticCall: - case FunctionType::Kind::Creation: break; case FunctionType::Kind::KECCAK256: case FunctionType::Kind::ECRecover: @@ -728,6 +735,11 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall) case FunctionType::Kind::ObjectCreation: visitObjectCreation(_funCall); return; + case FunctionType::Kind::DelegateCall: + case FunctionType::Kind::BareCall: + case FunctionType::Kind::BareCallCode: + case FunctionType::Kind::BareDelegateCall: + case FunctionType::Kind::Creation: default: m_errorReporter.warning( 4588_error, @@ -786,6 +798,50 @@ void SMTEncoder::visitRequire(FunctionCall const& _funCall) addPathImpliedExpression(expr(*args.front())); } +void SMTEncoder::visitABIFunction(FunctionCall const& _funCall) +{ + auto symbFunction = m_context.state().abiFunction(&_funCall); + auto const& [name, inTypes, outTypes] = m_context.state().abiFunctionTypes(&_funCall); + + auto const& funType = dynamic_cast(*_funCall.expression().annotation().type); + auto kind = funType.kind(); + auto const& args = _funCall.sortedArguments(); + auto argsActualLength = kind == FunctionType::Kind::ABIDecode ? 1 : args.size(); + + vector symbArgs; + solAssert(inTypes.size() == argsActualLength, ""); + for (unsigned i = 0; i < argsActualLength; ++i) + if (args.at(i)) + symbArgs.emplace_back(expr(*args.at(i), inTypes.at(i))); + + optional arg; + if (inTypes.size() == 1) + arg = expr(*args.at(0)); + else + { + auto inputSort = dynamic_cast(*symbFunction.sort).domain; + arg = smtutil::Expression::tuple_constructor( + smtutil::Expression(make_shared(inputSort), ""), + symbArgs + ); + } + + auto out = smtutil::Expression::select(symbFunction, *arg); + if (outTypes.size() == 1) + defineExpr(_funCall, out); + else + { + auto symbTuple = dynamic_pointer_cast(m_context.expression(_funCall)); + solAssert(symbTuple, ""); + solAssert(symbTuple->components().size() == outTypes.size(), ""); + solAssert(out.sort->kind == smtutil::Kind::Tuple, ""); + + symbTuple->increaseIndex(); + for (unsigned i = 0; i < symbTuple->components().size(); ++i) + m_context.addAssertion(symbTuple->component(i) == smtutil::Expression::tuple_get(out, i)); + } +} + void SMTEncoder::visitCryptoFunction(FunctionCall const& _funCall) { auto const& funType = dynamic_cast(*_funCall.expression().annotation().type); @@ -2672,6 +2728,33 @@ RationalNumberType const* SMTEncoder::isConstant(Expression const& _expr) return nullptr; } +set SMTEncoder::collectABICalls(ASTNode const* _node) +{ + struct ABIFunctions: public ASTConstVisitor + { + ABIFunctions(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::ABIEncode: + case FunctionType::Kind::ABIEncodePacked: + case FunctionType::Kind::ABIEncodeWithSelector: + case FunctionType::Kind::ABIEncodeWithSignature: + case FunctionType::Kind::ABIDecode: + abiCalls.insert(&_funCall); + break; + default: {} + } + } + + set abiCalls; + }; + + return ABIFunctions(_node).abiCalls; +} + void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall) { FunctionDefinition const* funDef = functionCallToDefinition(_funCall); diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 14a1556d5..b8d571eed 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -87,6 +87,8 @@ public: /// RationalNumberType or can be const evaluated, and nullptr otherwise. static RationalNumberType const* isConstant(Expression const& _expr); + static std::set collectABICalls(ASTNode const* _node); + protected: // TODO: Check that we do not have concurrent reads and writes to a variable, // because the order of expression evaluation is undefined @@ -159,6 +161,7 @@ protected: void initFunction(FunctionDefinition const& _function); void visitAssert(FunctionCall const& _funCall); void visitRequire(FunctionCall const& _funCall); + void visitABIFunction(FunctionCall const& _funCall); void visitCryptoFunction(FunctionCall const& _funCall); void visitGasLeft(FunctionCall const& _funCall); virtual void visitAddMulMod(FunctionCall const& _funCall); diff --git a/libsolidity/formal/SymbolicState.cpp b/libsolidity/formal/SymbolicState.cpp index 5d38eac0f..99c5a9fb1 100644 --- a/libsolidity/formal/SymbolicState.cpp +++ b/libsolidity/formal/SymbolicState.cpp @@ -20,6 +20,7 @@ #include #include +#include using namespace std; using namespace solidity; @@ -77,6 +78,10 @@ void SymbolicState::reset() m_state.reset(); m_tx.reset(); m_crypto.reset(); + /// We don't reset m_abi's pointer nor clear m_abiMembers on purpose, + /// since it only helps to keep the already generated types. + solAssert(m_abi, ""); + m_abi->reset(); } smtutil::Expression SymbolicState::balances() const @@ -149,6 +154,14 @@ smtutil::Expression SymbolicState::txConstraints(FunctionDefinition const& _func return conj; } +void SymbolicState::prepareForSourceUnit(SourceUnit const& _source) +{ + set abiCalls = SMTEncoder::collectABICalls(&_source); + for (auto const& source: _source.referencedSourceUnits(true)) + abiCalls += SMTEncoder::collectABICalls(source); + buildABIFunctions(abiCalls); +} + /// Private helpers. void SymbolicState::addBalance(smtutil::Expression _address, smtutil::Expression _value) @@ -160,3 +173,126 @@ void SymbolicState::addBalance(smtutil::Expression _address, smtutil::Expression ); m_state.assignMember("balances", newBalances); } + +void SymbolicState::buildABIFunctions(set const& _abiFunctions) +{ + map functions; + + for (auto const* funCall: _abiFunctions) + { + auto t = dynamic_cast(funCall->expression().annotation().type); + + auto const& args = funCall->sortedArguments(); + auto const& paramTypes = t->parameterTypes(); + auto const& returnTypes = t->returnParameterTypes(); + + + auto argTypes = [](auto const& _args) { + return applyMap(_args, [](auto arg) { return arg->annotation().type; }); + }; + + /// Since each abi.* function may have a different number of input/output parameters, + /// we generically compute those types. + vector inTypes; + vector outTypes; + if (t->kind() == FunctionType::Kind::ABIDecode) + { + /// abi.decode : (bytes, tuple_of_types(return_types)) -> (return_types) + inTypes.emplace_back(TypeProvider::bytesMemory()); + auto const* tupleType = dynamic_cast(args.at(1)->annotation().type); + solAssert(tupleType, ""); + for (auto t: tupleType->components()) + { + auto typeType = dynamic_cast(t); + solAssert(typeType, ""); + outTypes.emplace_back(typeType->actualType()); + } + } + else + { + outTypes = returnTypes; + if ( + t->kind() == FunctionType::Kind::ABIEncodeWithSelector || + t->kind() == FunctionType::Kind::ABIEncodeWithSignature + ) + { + /// abi.encodeWithSelector : (bytes4, one_or_more_types) -> bytes + /// abi.encodeWithSignature : (string, one_or_more_types) -> bytes + inTypes.emplace_back(paramTypes.front()); + inTypes += argTypes(vector>(args.begin() + 1, args.end())); + } + else + { + /// abi.encode/abi.encodePacked : one_or_more_types -> bytes + solAssert( + t->kind() == FunctionType::Kind::ABIEncode || + t->kind() == FunctionType::Kind::ABIEncodePacked, + "" + ); + inTypes = argTypes(args); + } + } + + /// Rational numbers and string literals add the concrete values to the type name, + /// so we replace them by uint256 and bytes since those are the same as their SMT types. + /// TODO we could also replace all types by their ABI type. + auto replaceTypes = [](auto& _types) { + for (auto& t: _types) + if (t->category() == frontend::Type::Category::RationalNumber) + t = TypeProvider::uint256(); + else if (t->category() == frontend::Type::Category::StringLiteral) + t = TypeProvider::bytesMemory(); + }; + replaceTypes(inTypes); + replaceTypes(outTypes); + + auto name = t->richIdentifier(); + for (auto paramType: inTypes + outTypes) + name += "_" + paramType->richIdentifier(); + + m_abiMembers[funCall] = {name, inTypes, outTypes}; + + if (functions.count(name)) + continue; + + /// 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. + auto typesToSort = [](auto const& _types, string const& _name) -> shared_ptr { + if (_types.size() == 1) + return smtSort(*_types.front()); + + vector inNames; + vector sorts; + for (unsigned i = 0; i < _types.size(); ++i) + { + inNames.emplace_back(_name + "_input_" + to_string(i)); + sorts.emplace_back(smtSort(*_types.at(i))); + } + return make_shared( + _name + "_input", + inNames, + sorts + ); + }; + + auto functionSort = make_shared( + typesToSort(inTypes, name), + typesToSort(outTypes, name) + ); + + functions[name] = functionSort; + } + + m_abi = make_unique("abi", move(functions), m_context); +} + +smtutil::Expression SymbolicState::abiFunction(frontend::FunctionCall const* _funCall) +{ + solAssert(m_abi, ""); + return m_abi->member(get<0>(m_abiMembers.at(_funCall))); +} + +SymbolicState::SymbolicABIFunction const& SymbolicState::abiFunctionTypes(FunctionCall const* _funCall) const +{ + return m_abiMembers.at(_funCall); +} diff --git a/libsolidity/formal/SymbolicState.h b/libsolidity/formal/SymbolicState.h index 16e376b05..d18c4f0ca 100644 --- a/libsolidity/formal/SymbolicState.h +++ b/libsolidity/formal/SymbolicState.h @@ -138,10 +138,32 @@ public: smtutil::Expression cryptoFunction(std::string const& _member) const { return m_crypto.member(_member); } //@} + /// ABI functions. + //@{ + /// Calls the internal methods that build the symbolic ABI functions + /// based on the abi.* calls in _source and referenced sources. + void prepareForSourceUnit(SourceUnit const& _source); + smtutil::Expression abiFunction(FunctionCall const* _funCall); + using SymbolicABIFunction = std::tuple< + std::string, + std::vector, + std::vector + >; + SymbolicABIFunction const& abiFunctionTypes(FunctionCall const* _funCall) const; + + 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(); } + //@} + private: /// Adds _value to _account's balance. void addBalance(smtutil::Expression _account, smtutil::Expression _value); + /// Builds m_abi based on the abi.* calls _abiFunctions. + void buildABIFunctions(std::set const& _abiFunctions); + EncodingContext& m_context; SymbolicIntVariable m_error{ @@ -213,6 +235,12 @@ private: }, m_context }; + + /// Tuple containing all used ABI functions. + std::unique_ptr m_abi; + /// Maps ABI functions calls to their tuple names generated by + /// `buildABIFunctions`. + std::map m_abiMembers; }; } diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index 6fdd59d96..5e0f05f2c 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -556,6 +556,10 @@ smtutil::Expression symbolicUnknownConstraints(smtutil::Expression _expr, fronte solAssert(intType, ""); return _expr >= minValue(*intType) && _expr <= maxValue(*intType); } + else if (isArray(*_type) || isMapping(*_type)) + /// Length cannot be negative. + return smtutil::Expression::tuple_get(_expr, 1) >= 0; + return smtutil::Expression(true); }