Add constraints correlating address(this).balance and msg.value

Leo Alt · Leo Alt · commit 61160aa0e765 · 2021-08-25T21:10:08.000+02:00
diff --git 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
@@ -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
 {
diff --git 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
@@ -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.
diff --git 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
@@ -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;
diff --git a/libsolidity/formal/SymbolicState.h b/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);
 

Original file line number	Diff line number	Diff line change
`@@ -2283,9 +2283,7 @@ void SMTEncoder::resetStorageVariables()`
`2283`	`2283`
`2284`	`2284`	`void SMTEncoder::resetBalances()`
`2285`	`2285`	`{`
`2286`		- // TODO this should be changed to `balances` only
`2287`		- // when `state` gets more members.
`2288`		`- state().newState();`
	`2286`	`+ state().newBalances();`
`2289`	`2287`	`}`
`2290`	`2288`
`2291`	`2289`	`void SMTEncoder::resetReferences(VariableDeclaration const& _varDecl)`