Method defineExternalFunctionInterface

libsolidity/formal/CHC.cpp:1492–1575

}

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_" + std::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());

	if (encodeExternalCallsAsTrusted())
	{
		// If the contract has state variables that are addresses to other contracts,
		// we need to encode the fact that those contracts may have been called in between
		// transactions to _contract.
		//
		// We do that by adding nondet_interface constraints for those contracts,
		// in the last line of this if block.
		//
		// If there are state variables of container types like structs or arrays
		// that indirectly contain contract types, we havoc the state for simplicity,
		// in the first part of this block.
		// TODO: This could actually be supported.
		// For structs: simply collect the SMT expressions of all the indirect contract type members.
		// For arrays: more involved, needs to traverse the array symbolically and do the same for each contract.
		// For mappings: way more complicated if the element type is a contract.
		auto hasContractOrAddressSubType = [&](VariableDeclaration const* _var) -> bool {
			bool foundContract = false;
			solidity::util::BreadthFirstSearch<Type const*> bfs{{_var->type()}};
			bfs.run([&](auto _type, auto&& _addChild) {
				if (
					_type->category() == Type::Category::Address ||
					_type->category() == Type::Category::Contract
				)
				{
					foundContract = true;
					bfs.abort();
				}
				if (auto const* mapType = dynamic_cast<MappingType const*>(_type))
					_addChild(mapType->valueType());
				else if (auto const* arrayType = dynamic_cast<ArrayType const*>(_type))
					_addChild(arrayType->baseType());
				else if (auto const* structType = dynamic_cast<StructType const*>(_type))
					for (auto const& member: structType->nativeMembers(nullptr))
						_addChild(member.type);