diff --git a/Changelog.md b/Changelog.md index 0a392d173..2b6d4cc4e 100644 --- a/Changelog.md +++ b/Changelog.md @@ -6,6 +6,7 @@ Language Features: Compiler Features: * Immutable variables can be read at construction time once they are initialized. * SMTChecker: Support low level ``call`` as external calls to unknown code. + * SMTChecker: Add constraints to better correlate ``address(this).balance`` and ``msg.value``. Bugfixes: diff --git a/libsmtutil/Sorts.h b/libsmtutil/Sorts.h index 45668f269..107dc1f2c 100644 --- a/libsmtutil/Sorts.h +++ b/libsmtutil/Sorts.h @@ -159,7 +159,15 @@ struct TupleSort: public Sort name(std::move(_name)), members(std::move(_members)), components(std::move(_components)) - {} + { + for (size_t i = 0; i < members.size(); ++i) + memberToIndex[members.at(i)] = i; + } + + SortPointer memberSort(std::string const& _member) + { + return components.at(memberToIndex.at(_member)); + } bool operator==(Sort const& _other) const override { @@ -186,8 +194,10 @@ struct TupleSort: public Sort std::string const name; std::vector const members; std::vector const components; + std::map memberToIndex; }; + /** Frequently used sorts.*/ struct SortProvider { diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 64f868b6a..6330f65ee 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -169,7 +169,13 @@ void CHC::endVisit(ContractDefinition const& _contract) smtutil::Expression zeroes(true); for (auto var: stateVariablesIncludingInheritedAndPrivate(_contract)) zeroes = zeroes && currentValue(*var) == smt::zeroValue(var->type()); - addRule(smtutil::Expression::implies(initialConstraints(_contract) && zeroes, predicate(entry)), entry.functor().name); + // The contract's address might already have funds before deployment, + // so the balance must be at least `msg.value`, but not equals. + auto initialBalanceConstraint = state().balance(state().thisAddress()) >= state().txMember("msg.value"); + addRule(smtutil::Expression::implies( + initialConstraints(_contract) && zeroes && initialBalanceConstraint, + predicate(entry) + ), entry.functor().name); setCurrentBlock(entry); solAssert(!m_errorDest, ""); @@ -315,11 +321,16 @@ void CHC::endVisit(FunctionDefinition const& _function) shouldAnalyze(*m_currentContract) ) { - auto sum = summary(_function); + defineExternalFunctionInterface(_function, *m_currentContract); + setCurrentBlock(*m_interfaces.at(m_currentContract)); + + // Create the rule + // interface \land externalFunctionEntry => interface' auto ifacePre = smt::interfacePre(*m_interfaces.at(m_currentContract), *m_currentContract, m_context); - auto txConstraints = state().txTypeConstraints() && state().txFunctionConstraints(_function); - m_queryPlaceholders[&_function].push_back({txConstraints && sum, errorFlag().currentValue(), ifacePre}); - connectBlocks(ifacePre, interface(), txConstraints && sum && errorFlag().currentValue() == 0); + auto sum = externalSummary(_function); + + m_queryPlaceholders[&_function].push_back({sum, errorFlag().currentValue(), ifacePre}); + connectBlocks(ifacePre, interface(), sum && errorFlag().currentValue() == 0); } m_currentFunction = nullptr; @@ -949,6 +960,7 @@ void CHC::resetSourceAnalysis() m_queryPlaceholders.clear(); m_callGraph.clear(); m_summaries.clear(); + m_externalSummaries.clear(); m_interfaces.clear(); m_nondetInterfaces.clear(); m_constructorSummaries.clear(); @@ -1128,6 +1140,8 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source) if (!function->isConstructor() && function->isPublic() && resolved.count(function)) { + m_externalSummaries[contract].emplace(function, createSummaryBlock(*function, *contract)); + auto state1 = stateVariablesAtIndex(1, *contract); auto state2 = stateVariablesAtIndex(2, *contract); @@ -1144,12 +1158,41 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source) applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 1); }) + applyMap(function->returnParameters(), [this](auto _var) { return valueAtIndex(*_var, 1); }); - connectBlocks(nondetPre, nondetPost, errorPre == 0 && (*m_summaries.at(contract).at(function))(args)); + connectBlocks(nondetPre, nondetPost, errorPre == 0 && (*m_externalSummaries.at(contract).at(function))(args)); } } } } +void CHC::defineExternalFunctionInterface(FunctionDefinition const& _function, ContractDefinition const& _contract) +{ + // Create a rule that represents an external call to this function. + // This contains more things than the function body itself, + // such as balance updates because of ``msg.value``. + auto functionEntryBlock = createBlock(&_function, PredicateType::FunctionBlock); + auto functionPred = predicate(*functionEntryBlock); + addRule(functionPred, functionPred.name); + setCurrentBlock(*functionEntryBlock); + + m_context.addAssertion(initialConstraints(_contract, &_function)); + m_context.addAssertion(state().txTypeConstraints() && state().txFunctionConstraints(_function)); + + // The contract may have received funds through a selfdestruct or + // block.coinbase, which do not trigger calls into the contract. + // So the only constraint we can add here is that the balance of + // the contract grows by at least `msg.value`. + SymbolicIntVariable k{TypeProvider::uint256(), TypeProvider::uint256(), "funds_" + to_string(m_context.newUniqueId()), m_context}; + m_context.addAssertion(k.currentValue() >= state().txMember("msg.value")); + // Assume that address(this).balance cannot overflow. + m_context.addAssertion(smt::symbolicUnknownConstraints(state().balance(state().thisAddress()) + k.currentValue(), TypeProvider::uint256())); + state().addBalance(state().thisAddress(), k.currentValue()); + + errorFlag().increaseIndex(); + m_context.addAssertion(summaryCall(_function)); + + connectBlocks(functionPred, externalSummary(_function)); +} + void CHC::defineContractInitializer(ContractDefinition const& _contract, ContractDefinition const& _contextContract) { m_contractInitializers[&_contextContract][&_contract] = createConstructorBlock(_contract, "contract_initializer"); @@ -1220,12 +1263,34 @@ smtutil::Expression CHC::summary(FunctionDefinition const& _function, ContractDe return smt::function(*m_summaries.at(&_contract).at(&_function), &_contract, m_context); } +smtutil::Expression CHC::summaryCall(FunctionDefinition const& _function, ContractDefinition const& _contract) +{ + return smt::functionCall(*m_summaries.at(&_contract).at(&_function), &_contract, m_context); +} + +smtutil::Expression CHC::externalSummary(FunctionDefinition const& _function, ContractDefinition const& _contract) +{ + return smt::function(*m_externalSummaries.at(&_contract).at(&_function), &_contract, m_context); +} + smtutil::Expression CHC::summary(FunctionDefinition const& _function) { solAssert(m_currentContract, ""); return summary(_function, *m_currentContract); } +smtutil::Expression CHC::summaryCall(FunctionDefinition const& _function) +{ + solAssert(m_currentContract, ""); + return summaryCall(_function, *m_currentContract); +} + +smtutil::Expression CHC::externalSummary(FunctionDefinition const& _function) +{ + solAssert(m_currentContract, ""); + return externalSummary(_function, *m_currentContract); +} + Predicate const* CHC::createBlock(ASTNode const* _node, PredicateType _predType, string const& _prefix) { auto block = createSymbolicBlock( diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index f2e8f62a1..12c8fbda0 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -164,6 +164,12 @@ private: /// in a given _source. void defineInterfacesAndSummaries(SourceUnit const& _source); + /// Creates the rule + /// summary_function \land transaction_entry_constraints => external_summary_function + /// This is needed to add these transaction entry constraints which include + /// potential balance increase by external means, for example. + void defineExternalFunctionInterface(FunctionDefinition const& _function, ContractDefinition const& _contract); + /// Creates a CHC system that, for a given contract, /// - initializes its state variables (as 0 or given value, if any). /// - "calls" the explicit constructor function of the contract, if any. @@ -225,6 +231,13 @@ private: /// @returns a predicate that defines a function summary. smtutil::Expression summary(FunctionDefinition const& _function); smtutil::Expression summary(FunctionDefinition const& _function, ContractDefinition const& _contract); + /// @returns a predicate that applies a function summary + /// over the constrained variables. + smtutil::Expression summaryCall(FunctionDefinition const& _function); + smtutil::Expression summaryCall(FunctionDefinition const& _function, ContractDefinition const& _contract); + /// @returns a predicate that defines an external function summary. + smtutil::Expression externalSummary(FunctionDefinition const& _function); + smtutil::Expression externalSummary(FunctionDefinition const& _function, ContractDefinition const& _contract); //@} /// Solver related. @@ -317,6 +330,9 @@ private: /// Function predicates. std::map> m_summaries; + + /// External function predicates. + std::map> m_externalSummaries; //@} /// Variables. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index c1a5393e7..cefaef901 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -2283,9 +2283,7 @@ void SMTEncoder::resetStorageVariables() void SMTEncoder::resetBalances() { - // TODO this should be changed to `balances` only - // when `state` gets more members. - state().newState(); + state().newBalances(); } void SMTEncoder::resetReferences(VariableDeclaration const& _varDecl) diff --git a/libsolidity/formal/SymbolicState.cpp b/libsolidity/formal/SymbolicState.cpp index 3789dd569..a3733bc41 100644 --- a/libsolidity/formal/SymbolicState.cpp +++ b/libsolidity/formal/SymbolicState.cpp @@ -104,6 +104,14 @@ smtutil::Expression SymbolicState::blockhash(smtutil::Expression _blockNumber) c return smtutil::Expression::select(m_tx.member("blockhash"), move(_blockNumber)); } +void SymbolicState::newBalances() +{ + auto tupleSort = dynamic_pointer_cast(stateSort()); + auto balanceSort = tupleSort->components.at(tupleSort->memberToIndex.at("balances")); + SymbolicVariable newBalances(balanceSort, "fresh_balances_" + to_string(m_context.newUniqueId()), m_context); + m_state.assignMember("balances", newBalances.currentValue()); +} + void SymbolicState::transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value) { unsigned indexBefore = m_state.index(); @@ -121,6 +129,16 @@ void SymbolicState::transfer(smtutil::Expression _from, smtutil::Expression _to, m_context.addAssertion(m_state.value() == newState); } +void SymbolicState::addBalance(smtutil::Expression _address, smtutil::Expression _value) +{ + auto newBalances = smtutil::Expression::store( + balances(), + _address, + balance(_address) + move(_value) + ); + m_state.assignMember("balances", newBalances); +} + smtutil::Expression SymbolicState::txMember(string const& _member) const { return m_tx.member(_member); @@ -181,16 +199,6 @@ void SymbolicState::prepareForSourceUnit(SourceUnit const& _source) /// Private helpers. -void SymbolicState::addBalance(smtutil::Expression _address, smtutil::Expression _value) -{ - auto newBalances = smtutil::Expression::store( - balances(), - _address, - balance(_address) + move(_value) - ); - m_state.assignMember("balances", newBalances); -} - void SymbolicState::buildABIFunctions(set const& _abiFunctions) { map functions; diff --git a/libsolidity/formal/SymbolicState.h b/libsolidity/formal/SymbolicState.h index d2f3016c3..309d545b8 100644 --- a/libsolidity/formal/SymbolicState.h +++ b/libsolidity/formal/SymbolicState.h @@ -108,6 +108,8 @@ public: smtutil::Expression state(unsigned _idx) const { return m_state.value(_idx); } smtutil::SortPointer const& stateSort() const { return m_state.sort(); } void newState() { m_state.newVar(); } + + void newBalances(); /// @returns the symbolic balances. smtutil::Expression balances() const; /// @returns the symbolic balance of address `this`. @@ -117,6 +119,9 @@ public: /// Transfer _value from _from to _to. void transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value); + + /// Adds _value to _account's balance. + void addBalance(smtutil::Expression _account, smtutil::Expression _value); //@} /// Transaction data. @@ -163,9 +168,6 @@ public: //@} 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);