Merge pull request #11828 from ethereum/smt_chc_balance

[SMTChecker] Add proper constraints on the contract's balance

Author: Leonardo

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:

docs/smtchecker.rst

@@ -830,6 +830,25 @@ are located in storage, even though they also have type ``uint[]``.  However,
 if ``d`` was assigned, we would need to clear knowledge about ``array`` and
 vice-versa.
 
+Contract Balance
+================
+
+A contract may be deployed with funds sent to it, if ``msg.value`` > 0 in the
+deployment transaction.
+However, the contract's address may already have funds before deployment,
+which are kept by the contract.
+Therefore, the SMTChecker assumes that ``address(this).balance >= msg.value``
+in the constructor in order to be consistent with the EVM rules.
+The contract's balance may also increase without triggering any calls to the
+contract, if
+
+- ``selfdestruct`` is executed by another contract with the analyzed contract
+  as the target of the remaining funds,
+- the contract is the coinbase (i.e., ``block.coinbase``) of some block.
+
+To model this properly, the SMTChecker assumes that at every new transaction
+the contract's balance may grow by at least ``msg.value``.
+
 **********************
 Real World Assumptions
 **********************
@@ -841,3 +860,7 @@ push: If the ``push`` operation is applied to an array of length 2^256 - 1, its
 length silently overflows.
 However, this is unlikely to happen in practice, since the operations required
 to grow the array to that point would take billions of years to execute.
+Another similar assumption taken by the SMTChecker is that an address' balance
+can never overflow.
+
+A similar idea was presented in `EIP-1985 <https://eips.ethereum.org/EIPS/eip-1985>`_.

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<std::string> const members;
 	std::vector<SortPointer> const components;
+	std::map<std::string, size_t> memberToIndex;
 };
 
+
 /** Frequently used sorts.*/
 struct SortProvider
 {

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(

libsolidity/formal/CHC.h

@@ -164,6 +164,12 @@ class CHC: public SMTEncoder
 	/// 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 @@ class CHC: public SMTEncoder
 	/// @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 @@ class CHC: public SMTEncoder
 
 	/// Function predicates.
 	std::map<ContractDefinition const*, std::map<FunctionDefinition const*, Predicate const*>> m_summaries;
+
+	/// External function predicates.
+	std::map<ContractDefinition const*, std::map<FunctionDefinition const*, Predicate const*>> m_externalSummaries;
 	//@}
 
 	/// Variables.

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)

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<TupleSort>(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<FunctionCall const*> const& _abiFunctions)
 {
 	map<string, SortPointer> functions;

libsolidity/formal/SymbolicState.h

@@ -108,6 +108,8 @@ class SymbolicState
 	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 @@ class SymbolicState
 
 	/// 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 @@ class SymbolicState
 	//@}
 
 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<FunctionCall const*> const& _abiFunctions);