[SMTChecker] Add a new trusted mode which assumes that code that is

available at compile time is trusted.

libsolidity/formal/BMC.cpp

@@ -82,7 +82,7 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
 	m_context.setAssertionAccumulation(true);
 	m_variableUsage.setFunctionInlining(shouldInlineFunctionCall);
 	createFreeConstants(sourceDependencies(_source));
-	state().prepareForSourceUnit(_source);
+	state().prepareForSourceUnit(_source, false);
 	m_unprovedAmt = 0;
 
 	_source.accept(*this);
@@ -130,7 +130,7 @@ bool BMC::shouldInlineFunctionCall(
 
 	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
 	if (funType.kind() == FunctionType::Kind::External)
-		return isTrustedExternalCall(&_funCall.expression());
+		return isExternalCallToThis(&_funCall.expression());
 	else if (funType.kind() != FunctionType::Kind::Internal)
 		return false;
 
@@ -567,7 +567,7 @@ void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall)
 	auto const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
 	if (shouldInlineFunctionCall(_funCall, currentScopeContract(), m_currentContract))
 		inlineFunctionCall(_funCall);
-	else if (isPublicGetter(_funCall.expression()))
+	else if (publicGetter(_funCall.expression()))
 	{
 		// Do nothing here.
 		// The processing happens in SMT Encoder, but we need to prevent the resetting of the state variables.

libsolidity/formal/CHC.cpp

@@ -104,7 +104,7 @@ void CHC::analyze(SourceUnit const& _source)
 	auto sources = sourceDependencies(_source);
 	collectFreeFunctions(sources);
 	createFreeConstants(sources);
-	state().prepareForSourceUnit(_source);
+	state().prepareForSourceUnit(_source, encodeExternalCallsAsTrusted());
 
 	for (auto const* source: sources)
 		defineInterfacesAndSummaries(*source);
@@ -175,15 +175,30 @@ void CHC::endVisit(ContractDefinition const& _contract)
 	smtutil::Expression zeroes(true);
 	for (auto var: stateVariablesIncludingInheritedAndPrivate(_contract))
 		zeroes = zeroes && currentValue(*var) == smt::zeroValue(var->type());
+
+	smtutil::Expression newAddress = encodeExternalCallsAsTrusted() ?
+		!state().addressActive(state().thisAddress()) :
+		smtutil::Expression(true);
+
 	// 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,
+		initialConstraints(_contract) && zeroes && newAddress && initialBalanceConstraint,
 		predicate(entry)
 	), entry.functor().name);
+
 	setCurrentBlock(entry);
 
+	if (encodeExternalCallsAsTrusted())
+	{
+		auto const& entryAfterAddress = *createConstructorBlock(_contract, "implicit_constructor_entry_after_address");
+		state().setAddressActive(state().thisAddress(), true);
+
+		connectBlocks(m_currentBlock, predicate(entryAfterAddress));
+		setCurrentBlock(entryAfterAddress);
+	}
+
 	solAssert(!m_errorDest, "");
 	m_errorDest = m_constructorSummaries.at(&_contract);
 	// We need to evaluate the base constructor calls (arguments) from derived -> base
@@ -220,6 +235,9 @@ void CHC::endVisit(ContractDefinition const& _contract)
 		m_context.addAssertion(errorFlag().currentValue() == 0);
 	}
 
+	if (encodeExternalCallsAsTrusted())
+		state().writeStateVars(_contract, state().thisAddress());
+
 	connectBlocks(m_currentBlock, summary(_contract));
 
 	setCurrentBlock(*m_constructorSummaries.at(&_contract));
@@ -550,10 +568,12 @@ void CHC::endVisit(FunctionCall const& _funCall)
 		externalFunctionCall(_funCall);
 		SMTEncoder::endVisit(_funCall);
 		break;
+	case FunctionType::Kind::Creation:
+		visitDeployment(_funCall);
+		break;
 	case FunctionType::Kind::DelegateCall:
 	case FunctionType::Kind::BareCallCode:
 	case FunctionType::Kind::BareDelegateCall:
-	case FunctionType::Kind::Creation:
 		SMTEncoder::endVisit(_funCall);
 		unknownFunctionCall(_funCall);
 		break;
@@ -717,6 +737,19 @@ void CHC::visitAssert(FunctionCall const& _funCall)
 	verificationTargetEncountered(&_funCall, VerificationTargetType::Assert, errorCondition);
 }
 
+void CHC::visitPublicGetter(FunctionCall const& _funCall)
+{
+	createExpr(_funCall);
+	if (encodeExternalCallsAsTrusted())
+	{
+		auto const& access = dynamic_cast<MemberAccess const&>(_funCall.expression());
+		auto const& contractType = dynamic_cast<ContractType const&>(*access.expression().annotation().type);
+		state().writeStateVars(*m_currentContract, state().thisAddress());
+		state().readStateVars(contractType.contractDefinition(), expr(access.expression()));
+	}
+	SMTEncoder::visitPublicGetter(_funCall);
+}
+
 void CHC::visitAddMulMod(FunctionCall const& _funCall)
 {
 	solAssert(_funCall.arguments().at(2), "");
@@ -726,6 +759,66 @@ void CHC::visitAddMulMod(FunctionCall const& _funCall)
 	SMTEncoder::visitAddMulMod(_funCall);
 }
 
+void CHC::visitDeployment(FunctionCall const& _funCall)
+{
+	if (!encodeExternalCallsAsTrusted())
+	{
+		SMTEncoder::endVisit(_funCall);
+		unknownFunctionCall(_funCall);
+		return;
+	}
+
+	auto [callExpr, callOptions] = functionCallExpression(_funCall);
+	auto funType = dynamic_cast<FunctionType const*>(callExpr->annotation().type);
+	ContractDefinition const* contract =
+		&dynamic_cast<ContractType const&>(*funType->returnParameterTypes().front()).contractDefinition();
+
+	// copy state variables from m_currentContract to state.storage.
+	state().writeStateVars(*m_currentContract, state().thisAddress());
+	errorFlag().increaseIndex();
+
+	Expression const* value = valueOption(callOptions);
+	if (value)
+		decreaseBalanceFromOptionsValue(*value);
+
+	auto originalTx = state().tx();
+	newTxConstraints(value);
+
+	auto prevThisAddr = state().thisAddress();
+	auto newAddr = state().newThisAddress();
+
+	if (auto constructor = contract->constructor())
+	{
+		auto const& args = _funCall.sortedArguments();
+		auto const& params = constructor->parameters();
+		solAssert(args.size() == params.size(), "");
+		for (auto [arg, param]: ranges::zip_view(args, params))
+			m_context.addAssertion(expr(*arg) == m_context.variable(*param)->currentValue());
+	}
+	for (auto var: stateVariablesIncludingInheritedAndPrivate(*contract))
+		m_context.variable(*var)->increaseIndex();
+	Predicate const& constructorSummary = *m_constructorSummaries.at(contract);
+	m_context.addAssertion(smt::constructorCall(constructorSummary, m_context, false));
+
+	solAssert(m_errorDest, "");
+	connectBlocks(
+		m_currentBlock,
+		predicate(*m_errorDest),
+		errorFlag().currentValue() > 0
+	);
+	m_context.addAssertion(errorFlag().currentValue() == 0);
+
+	m_context.addAssertion(state().newThisAddress() == prevThisAddr);
+
+	// copy state variables from state.storage to m_currentContract.
+	state().readStateVars(*m_currentContract, state().thisAddress());
+
+	state().newTx();
+	m_context.addAssertion(originalTx == state().tx());
+
+	defineExpr(_funCall, newAddr);
+}
+
 void CHC::internalFunctionCall(FunctionCall const& _funCall)
 {
 	solAssert(m_currentContract, "");
@@ -750,6 +843,53 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall)
 	m_context.addAssertion(errorFlag().currentValue() == 0);
 }
 
+void CHC::addNondetCalls(ContractDefinition const& _contract)
+{
+	for (auto var: _contract.stateVariables())
+		if (auto contractType = dynamic_cast<ContractType const*>(var->type()))
+		{
+			auto const& symbVar = m_context.variable(*var);
+			m_context.addAssertion(symbVar->currentValue() == symbVar->valueAtIndex(0));
+			nondetCall(contractType->contractDefinition(), *var);
+		}
+}
+
+void CHC::nondetCall(ContractDefinition const& _contract, VariableDeclaration const& _var)
+{
+	auto address = m_context.variable(_var)->currentValue();
+	// Load the called contract's state variables from the global state.
+	state().readStateVars(_contract, address);
+
+	m_context.addAssertion(state().state() == state().state(0));
+	auto preCallState = vector<smtutil::Expression>{state().state()} + currentStateVariables(_contract);
+
+	state().newState();
+	for (auto const* var: _contract.stateVariables())
+		m_context.variable(*var)->increaseIndex();
+
+	auto error = errorFlag().increaseIndex();
+
+	Predicate const& callPredicate = *createSymbolicBlock(
+		nondetInterfaceSort(_contract, state()),
+		"nondet_call_" + uniquePrefix(),
+		PredicateType::FunctionSummary,
+		&_var,
+		m_currentContract
+	);
+	auto postCallState = vector<smtutil::Expression>{state().state()} + currentStateVariables(_contract);
+	vector<smtutil::Expression> stateExprs{error, address, state().abi(), state().crypto()};
+
+	auto nondet = (*m_nondetInterfaces.at(&_contract))(stateExprs + preCallState + postCallState);
+	auto nondetCall = callPredicate(stateExprs + preCallState + postCallState);
+
+	addRule(smtutil::Expression::implies(nondet, nondetCall), nondetCall.name);
+
+	m_context.addAssertion(nondetCall);
+
+	// Load the called contract's state variables into the global state.
+	state().writeStateVars(_contract, address);
+}
+
 void CHC::externalFunctionCall(FunctionCall const& _funCall)
 {
 	/// In external function calls we do not add a "predicate call"
@@ -757,15 +897,10 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 	/// so we just add the nondet_interface predicate.
 
 	solAssert(m_currentContract, "");
+
 	auto [callExpr, callOptions] = functionCallExpression(_funCall);
-
-	if (isTrustedExternalCall(callExpr))
-	{
-		externalFunctionCallToTrustedCode(_funCall);
-		return;
-	}
-
 	FunctionType const& funType = dynamic_cast<FunctionType const&>(*callExpr->annotation().type);
+
 	auto kind = funType.kind();
 	solAssert(
 		kind == FunctionType::Kind::External ||
@@ -774,37 +909,42 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 		""
 	);
 
-	bool usesStaticCall = kind == FunctionType::Kind::BareStaticCall;
 
-	solAssert(m_currentContract, "");
-	auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
-	if (function)
+	// Only consider high level external calls in trusted mode.
+	if (
+		kind == FunctionType::Kind::External &&
+		(encodeExternalCallsAsTrusted() || isExternalCallToThis(callExpr))
+	)
 	{
-		usesStaticCall |= function->stateMutability() == StateMutability::Pure ||
-			function->stateMutability() == StateMutability::View;
-		for (auto var: function->returnParameters())
-			m_context.variable(*var)->increaseIndex();
+		externalFunctionCallToTrustedCode(_funCall);
+		return;
 	}
 
+	// Low level calls are still encoded nondeterministically.
+
+	auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
+	if (function)
+		for (auto var: function->returnParameters())
+			m_context.variable(*var)->increaseIndex();
+
+	// If we see a low level call in trusted mode,
+	// we need to havoc the global state.
+	if (
+		kind == FunctionType::Kind::BareCall &&
+		encodeExternalCallsAsTrusted()
+	)
+		state().newStorage();
+
+	// No reentrancy from constructor calls.
 	if (!m_currentFunction || m_currentFunction->isConstructor())
 		return;
 
-	if (callOptions)
-	{
-		optional<unsigned> valueIndex;
-		for (auto&& [i, name]: callOptions->names() | ranges::views::enumerate)
-			if (name && *name == "value")
-			{
-				valueIndex = i;
-				break;
-			}
-		if (valueIndex)
-			state().addBalance(state().thisAddress(), 0 - expr(*callOptions->options().at(*valueIndex)));
-	}
+	if (Expression const* value = valueOption(callOptions))
+		decreaseBalanceFromOptionsValue(*value);
 
 	auto preCallState = vector<smtutil::Expression>{state().state()} + currentStateVariables();
 
-	if (!usesStaticCall)
+	if (!usesStaticCall(_funCall))
 	{
 		state().newState();
 		for (auto const* var: m_stateVariables)
@@ -843,8 +983,14 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 
 void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall)
 {
+	if (publicGetter(_funCall.expression()))
+		visitPublicGetter(_funCall);
+
 	solAssert(m_currentContract, "");
-	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
+
+	auto [callExpr, callOptions] = functionCallExpression(_funCall);
+	FunctionType const& funType = dynamic_cast<FunctionType const&>(*callExpr->annotation().type);
+
 	auto kind = funType.kind();
 	solAssert(kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, "");
 
@@ -854,14 +1000,25 @@ void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall)
 
 	// External call creates a new transaction.
 	auto originalTx = state().tx();
-	auto txOrigin = state().txMember("tx.origin");
-	state().newTx();
-	// set the transaction sender as this contract
-	m_context.addAssertion(state().txMember("msg.sender") == state().thisAddress());
-	// set the transaction value as 0
-	m_context.addAssertion(state().txMember("msg.value") == 0);
-	// set the origin to be the current transaction origin
-	m_context.addAssertion(state().txMember("tx.origin") == txOrigin);
+	Expression const* value = valueOption(callOptions);
+	newTxConstraints(value);
+
+	auto calledAddress = contractAddressValue(_funCall);
+	if (value)
+	{
+		decreaseBalanceFromOptionsValue(*value);
+		state().addBalance(calledAddress, expr(*value));
+	}
+
+	if (encodeExternalCallsAsTrusted())
+	{
+		// The order here is important!! Write should go first.
+
+		// Load the caller contract's state variables into the global state.
+		state().writeStateVars(*m_currentContract, state().thisAddress());
+		// Load the called contract's state variables from the global state.
+		state().readStateVars(*function->annotation().contract, contractAddressValue(_funCall));
+	}
 
 	smtutil::Expression pred = predicate(_funCall);
 
@@ -878,6 +1035,17 @@ void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall)
 		(errorFlag().currentValue() > 0)
 	);
 	m_context.addAssertion(errorFlag().currentValue() == 0);
+
+	if (!usesStaticCall(_funCall))
+		if (encodeExternalCallsAsTrusted())
+		{
+			// The order here is important!! Write should go first.
+
+			// Load the called contract's state variables into the global state.
+			state().writeStateVars(*function->annotation().contract, contractAddressValue(_funCall));
+			// Load the caller contract's state variables from the global state.
+			state().readStateVars(*m_currentContract, state().thisAddress());
+		}
 }
 
 void CHC::unknownFunctionCall(FunctionCall const&)
@@ -1088,6 +1256,14 @@ set<unsigned> CHC::transactionVerificationTargetsIds(ASTNode const* _txRoot)
 	return verificationTargetsIds;
 }
 
+bool CHC::usesStaticCall(FunctionCall const& _funCall)
+{
+	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
+	auto kind = funType.kind();
+	auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
+	return (function && (function->stateMutability() == StateMutability::Pure || function->stateMutability() == StateMutability::View)) || kind == FunctionType::Kind::BareStaticCall;
+}
+
 optional<CHC::CHCNatspecOption> CHC::natspecOptionFromString(string const& _option)
 {
 	static map<string, CHCNatspecOption> options{
@@ -1128,6 +1304,11 @@ SortPointer CHC::sort(FunctionDefinition const& _function)
 	return functionBodySort(_function, m_currentContract, state());
 }
 
+bool CHC::encodeExternalCallsAsTrusted()
+{
+	return m_settings.externalCalls.isTrusted();
+}
+
 SortPointer CHC::sort(ASTNode const* _node)
 {
 	if (auto funDef = dynamic_cast<FunctionDefinition const*>(_node))
@@ -1232,6 +1413,62 @@ void CHC::defineExternalFunctionInterface(FunctionDefinition const& _function, C
 	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);
+			});
+			return foundContract;
+		};
+		bool found = false;
+		for (auto var: m_currentContract->stateVariables())
+			if (
+				var->type()->category() != Type::Category::Address &&
+				var->type()->category() != Type::Category::Contract &&
+				hasContractOrAddressSubType(var)
+			)
+			{
+				found = true;
+				break;
+			}
+
+		if (found)
+			state().newStorage();
+		else
+			addNondetCalls(*m_currentContract);
+	}
+
 	errorFlag().increaseIndex();
 	m_context.addAssertion(summaryCall(_function));
 
@@ -1308,28 +1545,28 @@ 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, ContractDefinition const& _contract)
+{
+	return smt::functionCall(*m_summaries.at(&_contract).at(&_function), &_contract, m_context);
+}
+
 smtutil::Expression CHC::summaryCall(FunctionDefinition const& _function)
 {
 	solAssert(m_currentContract, "");
 	return summaryCall(_function, *m_currentContract);
 }
 
+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::externalSummary(FunctionDefinition const& _function)
 {
 	solAssert(m_currentContract, "");
@@ -1516,18 +1753,19 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
 	auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts;
 	solAssert(kind != FunctionType::Kind::Internal || function->isFree() || (contract && contract->isLibrary()) || util::contains(hierarchy, contract), "");
 
-	bool usesStaticCall = function->stateMutability() == StateMutability::Pure || function->stateMutability() == StateMutability::View;
+	if (kind == FunctionType::Kind::Internal)
+		contract = m_currentContract;
 
-	args += currentStateVariables(*m_currentContract);
-	args += symbolicArguments(_funCall, m_currentContract);
-	if (!m_currentContract->isLibrary() && !usesStaticCall)
+	args += currentStateVariables(*contract);
+	args += symbolicArguments(_funCall, contract);
+	if (!usesStaticCall(_funCall))
 	{
 		state().newState();
-		for (auto const& var: m_stateVariables)
+		for (auto const& var: stateVariablesIncludingInheritedAndPrivate(*contract))
 			m_context.variable(*var)->increaseIndex();
 	}
 	args += vector<smtutil::Expression>{state().state()};
-	args += currentStateVariables(*m_currentContract);
+	args += currentStateVariables(*contract);
 
 	for (auto var: function->parameters() + function->returnParameters())
 	{
@@ -1538,14 +1776,14 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
 		args.push_back(currentValue(*var));
 	}
 
-	Predicate const& summary = *m_summaries.at(m_currentContract).at(function);
-	auto from = smt::function(summary, m_currentContract, m_context);
+	Predicate const& summary = *m_summaries.at(contract).at(function);
+	auto from = smt::function(summary, contract, m_context);
 	Predicate const& callPredicate = *createSummaryBlock(
 		*function,
-		*m_currentContract,
+		*contract,
 		kind == FunctionType::Kind::Internal ? PredicateType::InternalCall : PredicateType::ExternalCallTrusted
 	);
-	auto to = smt::function(callPredicate, m_currentContract, m_context);
+	auto to = smt::function(callPredicate, contract, m_context);
 	addRule(smtutil::Expression::implies(from, to), to.name);
 
 	return callPredicate(args);
@@ -1910,60 +2148,63 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
 		Predicate const* summaryPredicate = Predicate::predicate(summaryNode.name);
 		auto const& summaryArgs = summaryNode.arguments;
 
-		auto stateVars = summaryPredicate->stateVariables();
-		solAssert(stateVars.has_value(), "");
-		auto stateValues = summaryPredicate->summaryStateValues(summaryArgs);
-		solAssert(stateValues.size() == stateVars->size(), "");
-
-		if (first)
+		if (!summaryPredicate->programVariable())
 		{
-			first = false;
-			/// Generate counterexample message local to the failed target.
-			localState = formatVariableModel(*stateVars, stateValues, ", ") + "\n";
+			auto stateVars = summaryPredicate->stateVariables();
+			solAssert(stateVars.has_value(), "");
+			auto stateValues = summaryPredicate->summaryStateValues(summaryArgs);
+			solAssert(stateValues.size() == stateVars->size(), "");
 
-			if (auto calledFun = summaryPredicate->programFunction())
+			if (first)
 			{
-				auto inValues = summaryPredicate->summaryPostInputValues(summaryArgs);
-				auto const& inParams = calledFun->parameters();
-				if (auto inStr = formatVariableModel(inParams, inValues, "\n"); !inStr.empty())
-					localState += inStr + "\n";
-				auto outValues = summaryPredicate->summaryPostOutputValues(summaryArgs);
-				auto const& outParams = calledFun->returnParameters();
-				if (auto outStr = formatVariableModel(outParams, outValues, "\n"); !outStr.empty())
-					localState += outStr + "\n";
+				first = false;
+				/// Generate counterexample message local to the failed target.
+				localState = formatVariableModel(*stateVars, stateValues, ", ") + "\n";
 
-				optional<unsigned> localErrorId;
-				solidity::util::BreadthFirstSearch<unsigned> bfs{{summaryId}};
-				bfs.run([&](auto _nodeId, auto&& _addChild) {
-					auto const& children = _graph.edges.at(_nodeId);
-					if (
-						children.size() == 1 &&
-						nodePred(children.front())->isFunctionErrorBlock()
-					)
-					{
-						localErrorId = children.front();
-						bfs.abort();
-					}
-					ranges::for_each(children, _addChild);
-				});
-
-				if (localErrorId.has_value())
+				if (auto calledFun = summaryPredicate->programFunction())
 				{
-					auto const* localError = nodePred(*localErrorId);
-					solAssert(localError && localError->isFunctionErrorBlock(), "");
-					auto const [localValues, localVars] = localError->localVariableValues(nodeArgs(*localErrorId));
-					if (auto localStr = formatVariableModel(localVars, localValues, "\n"); !localStr.empty())
-						localState += localStr + "\n";
+					auto inValues = summaryPredicate->summaryPostInputValues(summaryArgs);
+					auto const& inParams = calledFun->parameters();
+					if (auto inStr = formatVariableModel(inParams, inValues, "\n"); !inStr.empty())
+						localState += inStr + "\n";
+					auto outValues = summaryPredicate->summaryPostOutputValues(summaryArgs);
+					auto const& outParams = calledFun->returnParameters();
+					if (auto outStr = formatVariableModel(outParams, outValues, "\n"); !outStr.empty())
+						localState += outStr + "\n";
+
+					optional<unsigned> localErrorId;
+					solidity::util::BreadthFirstSearch<unsigned> bfs{{summaryId}};
+					bfs.run([&](auto _nodeId, auto&& _addChild) {
+						auto const& children = _graph.edges.at(_nodeId);
+						if (
+							children.size() == 1 &&
+							nodePred(children.front())->isFunctionErrorBlock()
+						)
+						{
+							localErrorId = children.front();
+							bfs.abort();
+						}
+						ranges::for_each(children, _addChild);
+					});
+
+					if (localErrorId.has_value())
+					{
+						auto const* localError = nodePred(*localErrorId);
+						solAssert(localError && localError->isFunctionErrorBlock(), "");
+						auto const [localValues, localVars] = localError->localVariableValues(nodeArgs(*localErrorId));
+						if (auto localStr = formatVariableModel(localVars, localValues, "\n"); !localStr.empty())
+							localState += localStr + "\n";
+					}
 				}
 			}
-		}
-		else
-		{
-			auto modelMsg = formatVariableModel(*stateVars, stateValues, ", ");
-			/// We report the state after every tx in the trace except for the last, which is reported
-			/// first in the code above.
-			if (!modelMsg.empty())
-				path.emplace_back("State: " + modelMsg);
+			else
+			{
+				auto modelMsg = formatVariableModel(*stateVars, stateValues, ", ");
+				/// We report the state after every tx in the trace except for the last, which is reported
+				/// first in the code above.
+				if (!modelMsg.empty())
+					path.emplace_back("State: " + modelMsg);
+			}
 		}
 
 		string txCex = summaryPredicate->formatSummaryCall(summaryArgs, m_charStreamProvider);
@@ -1992,6 +2233,12 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
 				if (calls.size() > callTraceSize + 1)
 					calls.front() += ", synthesized as:";
 			}
+			else if (pred->programVariable())
+			{
+				calls.front() += "-- action on external contract in state variable \"" + pred->programVariable()->name() + "\"";
+				if (calls.size() > callTraceSize + 1)
+					calls.front() += ", synthesized as:";
+			}
 			else if (pred->isFunctionSummary() && parentPred->isExternalCallUntrusted())
 				calls.front() += " -- reentrant call";
 		};
@@ -2047,7 +2294,8 @@ map<unsigned, vector<unsigned>> CHC::summaryCalls(CHCSolverInterface::CexGraph c
 			nodePred->isInternalCall() ||
 			nodePred->isExternalCallTrusted() ||
 			nodePred->isExternalCallUntrusted() ||
-			rootPred->isExternalCallUntrusted()
+			rootPred->isExternalCallUntrusted() ||
+			rootPred->programVariable()
 		))
 		{
 			calls[root].push_back(node);
@@ -2105,3 +2353,31 @@ SymbolicIntVariable& CHC::errorFlag()
 {
 	return state().errorFlag();
 }
+
+void CHC::newTxConstraints(Expression const* _value)
+{
+	auto txOrigin = state().txMember("tx.origin");
+	state().newTx();
+	// set the transaction sender as this contract
+	m_context.addAssertion(state().txMember("msg.sender") == state().thisAddress());
+	// set the origin to be the current transaction origin
+	m_context.addAssertion(state().txMember("tx.origin") == txOrigin);
+
+	if (_value)
+		// set the msg value
+		m_context.addAssertion(state().txMember("msg.value") == expr(*_value));
+}
+
+frontend::Expression const* CHC::valueOption(FunctionCallOptions const* _options)
+{
+	if (_options)
+		for (auto&& [i, name]: _options->names() | ranges::views::enumerate)
+			if (name && *name == "value")
+				return _options->options().at(i).get();
+	return nullptr;
+}
+
+void CHC::decreaseBalanceFromOptionsValue(Expression const& _value)
+{
+	state().addBalance(state().thisAddress(), 0 - expr(_value));
+}

libsolidity/formal/CHC.h

@@ -110,10 +110,14 @@ private:
 	void popInlineFrame(CallableDeclaration const& _callable) override;
 
 	void visitAssert(FunctionCall const& _funCall);
+	void visitPublicGetter(FunctionCall const& _funCall) override;
 	void visitAddMulMod(FunctionCall const& _funCall) override;
+	void visitDeployment(FunctionCall const& _funCall);
 	void internalFunctionCall(FunctionCall const& _funCall);
 	void externalFunctionCall(FunctionCall const& _funCall);
 	void externalFunctionCallToTrustedCode(FunctionCall const& _funCall);
+	void addNondetCalls(ContractDefinition const& _contract);
+	void nondetCall(ContractDefinition const& _contract, VariableDeclaration const& _var);
 	void unknownFunctionCall(FunctionCall const& _funCall);
 	void makeArrayPopVerificationTarget(FunctionCall const& _arrayPop) override;
 	void makeOutOfBoundsVerificationTarget(IndexAccess const& _access) override;
@@ -135,6 +139,7 @@ private:
 	void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr) override;
 	void setCurrentBlock(Predicate const& _block);
 	std::set<unsigned> transactionVerificationTargetsIds(ASTNode const* _txRoot);
+	bool usesStaticCall(FunctionCall const& _funCall);
 	//@}
 
 	/// SMT Natspec and abstraction helpers.
@@ -148,6 +153,10 @@ private:
 	/// @returns true if _function is Natspec annotated to be abstracted by
 	/// nondeterministic values.
 	bool abstractAsNondet(FunctionDefinition const& _function);
+
+	/// @returns true if external calls should be considered trusted.
+	/// If that's the case, their code is used if available at compile time.
+	bool encodeExternalCallsAsTrusted();
 	//@}
 
 	/// Sort helpers.
@@ -310,6 +319,20 @@ private:
 	unsigned newErrorId();
 
 	smt::SymbolicIntVariable& errorFlag();
+
+	/// Adds to the solver constraints that
+	/// - propagate tx.origin
+	/// - set the current contract as msg.sender
+	/// - set the msg.value as _value, if not nullptr
+	void newTxConstraints(Expression const* _value);
+
+	/// @returns the expression representing the value sent in
+	/// an external call if present,
+	/// and nullptr otherwise.
+	frontend::Expression const* valueOption(FunctionCallOptions const* _options);
+
+	/// Adds constraints that decrease the balance of the caller by _value.
+	void decreaseBalanceFromOptionsValue(Expression const& _value);
 	//@}
 
 	/// Predicates.

libsolidity/formal/ModelCheckerSettings.cpp

@@ -130,3 +130,12 @@ std::optional<ModelCheckerContracts> ModelCheckerContracts::fromString(string co
 
 	return ModelCheckerContracts{chosen};
 }
+
+std::optional<ModelCheckerExtCalls> ModelCheckerExtCalls::fromString(string const& _mode)
+{
+	if (_mode == "untrusted")
+		return ModelCheckerExtCalls{Mode::UNTRUSTED};
+	if (_mode == "trusted")
+		return ModelCheckerExtCalls{Mode::TRUSTED};
+	return {};
+}

libsolidity/formal/ModelCheckerSettings.h

@@ -140,6 +140,21 @@ struct ModelCheckerTargets
 	std::set<VerificationTargetType> targets;
 };
 
+struct ModelCheckerExtCalls
+{
+	enum class Mode
+	{
+		UNTRUSTED,
+		TRUSTED
+	};
+
+	Mode mode = Mode::UNTRUSTED;
+
+	static std::optional<ModelCheckerExtCalls> fromString(std::string const& _mode);
+
+	bool isTrusted() const { return mode == Mode::TRUSTED; }
+};
+
 struct ModelCheckerSettings
 {
 	ModelCheckerContracts contracts = ModelCheckerContracts::Default();
@@ -151,6 +166,7 @@ struct ModelCheckerSettings
 	/// might prefer the precise encoding.
 	bool divModNoSlacks = false;
 	ModelCheckerEngine engine = ModelCheckerEngine::None();
+	ModelCheckerExtCalls externalCalls = {};
 	ModelCheckerInvariants invariants = ModelCheckerInvariants::Default();
 	bool showUnproved = false;
 	smtutil::SMTSolverChoice solvers = smtutil::SMTSolverChoice::Z3();
@@ -164,6 +180,7 @@ struct ModelCheckerSettings
 			contracts == _other.contracts &&
 			divModNoSlacks == _other.divModNoSlacks &&
 			engine == _other.engine &&
+			externalCalls.mode == _other.externalCalls.mode &&
 			invariants == _other.invariants &&
 			showUnproved == _other.showUnproved &&
 			solvers == _other.solvers &&

libsolidity/formal/Predicate.cpp

@@ -144,6 +144,11 @@ FunctionCall const* Predicate::programFunctionCall() const
 	return dynamic_cast<FunctionCall const*>(m_node);
 }
 
+VariableDeclaration  const* Predicate::programVariable() const
+{
+	return dynamic_cast<VariableDeclaration const*>(m_node);
+}
+
 optional<vector<VariableDeclaration const*>> Predicate::stateVariables() const
 {
 	if (m_contractContext)
@@ -214,6 +219,9 @@ string Predicate::formatSummaryCall(
 {
 	solAssert(isSummary(), "");
 
+	if (programVariable())
+		return {};
+
 	if (auto funCall = programFunctionCall())
 	{
 		if (funCall->location().hasText())
@@ -348,6 +356,8 @@ vector<optional<string>> Predicate::summaryStateValues(vector<smtutil::Expressio
 		stateFirst = _args.begin() + 7 + static_cast<int>(stateVars->size());
 		stateLast = stateFirst + static_cast<int>(stateVars->size());
 	}
+	else if (programVariable())
+		return {};
 	else
 		solAssert(false, "");
 

libsolidity/formal/Predicate.h

@@ -115,6 +115,10 @@ public:
 	/// or nullptr otherwise.
 	FunctionCall const* programFunctionCall() const;
 
+	/// @returns the VariableDeclaration that this predicate represents
+	/// or nullptr otherwise.
+	VariableDeclaration const* programVariable() const;
+
 	/// @returns the program state variables in the scope of this predicate.
 	std::optional<std::vector<VariableDeclaration const*>> stateVariables() const;
 

libsolidity/formal/PredicateInstance.cpp

@@ -70,14 +70,14 @@ smtutil::Expression constructor(Predicate const& _pred, EncodingContext& _contex
 	return _pred(stateExprs + initialStateVariables(contract, _context) + currentStateVariables(contract, _context));
 }
 
-smtutil::Expression constructorCall(Predicate const& _pred, EncodingContext& _context)
+smtutil::Expression constructorCall(Predicate const& _pred, EncodingContext& _context, bool _internal)
 {
 	auto const& contract = dynamic_cast<ContractDefinition const&>(*_pred.programNode());
 	if (auto const* constructor = contract.constructor())
-		return _pred(currentFunctionVariablesForCall(*constructor, &contract, _context));
+		return _pred(currentFunctionVariablesForCall(*constructor, &contract, _context, _internal));
 
 	auto& state = _context.state();
-	vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state()};
+	vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), _internal ? state.thisAddress(0) : state.thisAddress(), state.abi(0), state.crypto(0), _internal ? state.tx(0) : state.tx(), state.state()};
 	state.newState();
 	stateExprs += vector<smtutil::Expression>{state.state()};
 	stateExprs += currentStateVariables(contract, _context);
@@ -166,11 +166,12 @@ vector<smtutil::Expression> currentFunctionVariablesForDefinition(
 vector<smtutil::Expression> currentFunctionVariablesForCall(
 	FunctionDefinition const& _function,
 	ContractDefinition const* _contract,
-	EncodingContext& _context
+	EncodingContext& _context,
+	bool _internal
 )
 {
 	auto& state = _context.state();
-	vector<smtutil::Expression> exprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state()};
+	vector<smtutil::Expression> exprs{state.errorFlag().currentValue(), _internal ? state.thisAddress(0) : state.thisAddress(), state.abi(0), state.crypto(0), _internal ? state.tx(0) : state.tx(), state.state()};
 	exprs += _contract ? currentStateVariables(*_contract, _context) : vector<smtutil::Expression>{};
 	exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); });
 

libsolidity/formal/PredicateInstance.h

@@ -37,7 +37,14 @@ smtutil::Expression interface(Predicate const& _pred, ContractDefinition const&
 smtutil::Expression nondetInterface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context, unsigned _preIdx, unsigned _postIdx);
 
 smtutil::Expression constructor(Predicate const& _pred, EncodingContext& _context);
-smtutil::Expression constructorCall(Predicate const& _pred, EncodingContext& _context);
+/// The encoding of the deployment procedure includes adding constraints
+/// for base constructors if inheritance is used.
+/// From the predicate point of view this is not different,
+/// but some of the arguments are different.
+/// @param _internal = true means that this constructor call is used in the
+/// deployment procedure, whereas false means it is used in the deployment
+/// of a contract.
+smtutil::Expression constructorCall(Predicate const& _pred, EncodingContext& _context, bool _internal = true);
 
 smtutil::Expression function(
 	Predicate const& _pred,
@@ -77,7 +84,8 @@ std::vector<smtutil::Expression> currentFunctionVariablesForDefinition(
 std::vector<smtutil::Expression> currentFunctionVariablesForCall(
 	FunctionDefinition const& _function,
 	ContractDefinition const* _contract,
-	EncodingContext& _context
+	EncodingContext& _context,
+	bool _internal = true
 );
 
 std::vector<smtutil::Expression> currentBlockVariables(

libsolidity/formal/SMTEncoder.cpp

@@ -637,7 +637,7 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
 		visitGasLeft(_funCall);
 		break;
 	case FunctionType::Kind::External:
-		if (isPublicGetter(_funCall.expression()))
+		if (publicGetter(_funCall.expression()))
 			visitPublicGetter(_funCall);
 		break;
 	case FunctionType::Kind::ABIDecode:
@@ -696,10 +696,18 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
 	case FunctionType::Kind::ObjectCreation:
 		visitObjectCreation(_funCall);
 		return;
+	case FunctionType::Kind::Creation:
+		if (!m_settings.engine.chc || !m_settings.externalCalls.isTrusted())
+			m_errorReporter.warning(
+				8729_error,
+				_funCall.location(),
+				"Contract deployment is only supported in the trusted mode for external calls"
+				" with the CHC engine."
+			);
+		break;
 	case FunctionType::Kind::DelegateCall:
 	case FunctionType::Kind::BareCallCode:
 	case FunctionType::Kind::BareDelegateCall:
-	case FunctionType::Kind::Creation:
 	default:
 		m_errorReporter.warning(
 			4588_error,
@@ -978,9 +986,8 @@ vector<string> structGetterReturnedMembers(StructType const& _structType)
 
 void SMTEncoder::visitPublicGetter(FunctionCall const& _funCall)
 {
-	MemberAccess const& access = dynamic_cast<MemberAccess const&>(_funCall.expression());
-	auto var = dynamic_cast<VariableDeclaration const*>(access.annotation().referencedDeclaration);
-	solAssert(var, "");
+	auto var = publicGetter(_funCall.expression());
+	solAssert(var && var->isStateVariable(), "");
 	solAssert(m_context.knownExpression(_funCall), "");
 	auto paramExpectedTypes = replaceUserTypes(FunctionType(*var).parameterTypes());
 	auto actualArguments = _funCall.arguments();
@@ -1054,7 +1061,7 @@ bool SMTEncoder::shouldAnalyze(ContractDefinition const& _contract) const
 		return false;
 
 	return m_settings.contracts.isDefault() ||
-		m_settings.contracts.has(_contract.sourceUnitName(), _contract.name());
+		m_settings.contracts.has(_contract.sourceUnitName());
 }
 
 void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall)
@@ -2789,16 +2796,24 @@ MemberAccess const* SMTEncoder::isEmptyPush(Expression const& _expr) const
 	return nullptr;
 }
 
-bool SMTEncoder::isPublicGetter(Expression const& _expr) {
-	if (!isTrustedExternalCall(&_expr))
-		return false;
-	auto varDecl = dynamic_cast<VariableDeclaration const*>(
-		dynamic_cast<MemberAccess const&>(_expr).annotation().referencedDeclaration
-	);
-	return varDecl != nullptr;
+smtutil::Expression SMTEncoder::contractAddressValue(FunctionCall const& _f)
+{
+	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_f.expression().annotation().type);
+	if (funType.kind() == FunctionType::Kind::Internal)
+		return state().thisAddress();
+	auto [funExpr, funOptions] = functionCallExpression(_f);
+	if (MemberAccess const* callBase = dynamic_cast<MemberAccess const*>(funExpr))
+		return expr(callBase->expression());
+	solAssert(false, "Unreachable!");
 }
 
-bool SMTEncoder::isTrustedExternalCall(Expression const* _expr) {
+VariableDeclaration const* SMTEncoder::publicGetter(Expression const& _expr) const {
+	if (auto memberAccess = dynamic_cast<MemberAccess const*>(&_expr))
+		return dynamic_cast<VariableDeclaration const*>(memberAccess->annotation().referencedDeclaration);
+	return nullptr;
+}
+
+bool SMTEncoder::isExternalCallToThis(Expression const* _expr) {
 	auto memberAccess = dynamic_cast<MemberAccess const*>(_expr);
 	if (!memberAccess)
 		return false;
@@ -3060,7 +3075,7 @@ RationalNumberType const* SMTEncoder::isConstant(Expression const& _expr)
 	return nullptr;
 }
 
-set<FunctionCall const*> SMTEncoder::collectABICalls(ASTNode const* _node)
+set<FunctionCall const*, ASTCompareByID<FunctionCall>> SMTEncoder::collectABICalls(ASTNode const* _node)
 {
 	struct ABIFunctions: public ASTConstVisitor
 	{
@@ -3082,7 +3097,7 @@ set<FunctionCall const*> SMTEncoder::collectABICalls(ASTNode const* _node)
 				}
 		}
 
-		set<FunctionCall const*> abiCalls;
+		set<FunctionCall const*, ASTCompareByID<FunctionCall>> abiCalls;
 	};
 
 	return ABIFunctions(_node).abiCalls;

libsolidity/formal/SMTEncoder.h

@@ -123,7 +123,7 @@ public:
 	/// RationalNumberType or can be const evaluated, and nullptr otherwise.
 	static RationalNumberType const* isConstant(Expression const& _expr);
 
-	static std::set<FunctionCall const*> collectABICalls(ASTNode const* _node);
+	static std::set<FunctionCall const*, ASTCompareByID<FunctionCall>> collectABICalls(ASTNode const* _node);
 
 	/// @returns all the sources that @param _source depends on,
 	/// including itself.
@@ -219,7 +219,7 @@ protected:
 	void visitTypeConversion(FunctionCall const& _funCall);
 	void visitStructConstructorCall(FunctionCall const& _funCall);
 	void visitFunctionIdentifier(Identifier const& _identifier);
-	void visitPublicGetter(FunctionCall const& _funCall);
+	virtual void visitPublicGetter(FunctionCall const& _funCall);
 
 	/// @returns true if @param _contract is set for analysis in the settings
 	/// and it is not abstract.
@@ -227,7 +227,12 @@ protected:
 	/// @returns true if @param _source is set for analysis in the settings.
 	bool shouldAnalyze(SourceUnit const& _source) const;
 
-	bool isPublicGetter(Expression const& _expr);
+	/// @returns the state variable returned by a public getter if
+	/// @a _expr is a call to a public getter,
+	/// otherwise nullptr.
+	VariableDeclaration const* publicGetter(Expression const& _expr) const;
+
+	smtutil::Expression contractAddressValue(FunctionCall const& _f);
 
 	/// Encodes a modifier or function body according to the modifier
 	/// visit depth.
@@ -392,9 +397,9 @@ protected:
 	/// otherwise nullptr.
 	MemberAccess const* isEmptyPush(Expression const& _expr) const;
 
-	/// @returns true if the given identifier is a contract which is known and trusted.
+	/// @returns true if the given expression is `this`.
 	/// This means we don't have to abstract away effects of external function calls to this contract.
-	static bool isTrustedExternalCall(Expression const* _expr);
+	static bool isExternalCallToThis(Expression const* _expr);
 
 	/// Creates symbolic expressions for the returned values
 	/// and set them as the components of the symbolic tuple.

libsolidity/formal/SymbolicState.cpp

@@ -22,8 +22,13 @@
 #include <libsolidity/formal/EncodingContext.h>
 #include <libsolidity/formal/SMTEncoder.h>
 
+#include <libsmtutil/Sorts.h>
+
+#include <range/v3/view.hpp>
+
 using namespace std;
 using namespace solidity;
+using namespace solidity::util;
 using namespace solidity::smtutil;
 using namespace solidity::frontend::smt;
 
@@ -58,16 +63,8 @@ smtutil::Expression BlockchainVariable::member(string const& _member) const
 
 smtutil::Expression BlockchainVariable::assignMember(string const& _member, smtutil::Expression const& _value)
 {
-	vector<smtutil::Expression> args;
-	for (auto const& m: m_members)
-		if (m.first == _member)
-			args.emplace_back(_value);
-		else
-			args.emplace_back(member(m.first));
-	m_tuple->increaseIndex();
-	auto tuple = m_tuple->currentValue();
-	auto sortExpr = smtutil::Expression(make_shared<smtutil::SortSort>(tuple.sort), tuple.name);
-	m_context.addAssertion(tuple == smtutil::Expression::tuple_constructor(sortExpr, args));
+	smtutil::Expression newTuple = smt::assignMember(m_tuple->currentValue(), {{_member, _value}});
+	m_context.addAssertion(m_tuple->increaseIndex() == newTuple);
 	return m_tuple->currentValue();
 }
 
@@ -75,16 +72,19 @@ void SymbolicState::reset()
 {
 	m_error.resetIndex();
 	m_thisAddress.resetIndex();
-	m_state.reset();
 	m_tx.reset();
 	m_crypto.reset();
 	if (m_abi)
 		m_abi->reset();
+	/// We don't reset nor clear these pointers on purpose,
+	/// since it only helps to keep the already generated types.
+	if (m_state)
+		m_state->reset();
 }
 
 smtutil::Expression SymbolicState::balances() const
 {
-	return m_state.member("balances");
+	return m_state->member("balances");
 }
 
 smtutil::Expression SymbolicState::balance() const
@@ -107,24 +107,94 @@ 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());
+	m_state->assignMember("balances", newBalances.currentValue());
 }
 
 void SymbolicState::transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value)
 {
-	unsigned indexBefore = m_state.index();
+	unsigned indexBefore = m_state->index();
 	addBalance(_from, 0 - _value);
 	addBalance(_to, std::move(_value));
-	unsigned indexAfter = m_state.index();
+	unsigned indexAfter = m_state->index();
 	solAssert(indexAfter > indexBefore, "");
-	m_state.newVar();
+	m_state->newVar();
 	/// Do not apply the transfer operation if _from == _to.
 	auto newState = smtutil::Expression::ite(
 		std::move(_from) == std::move(_to),
-		m_state.value(indexBefore),
-		m_state.value(indexAfter)
+		m_state->value(indexBefore),
+		m_state->value(indexAfter)
 	);
-	m_context.addAssertion(m_state.value() == newState);
+	m_context.addAssertion(m_state->value() == newState);
+}
+
+smtutil::Expression SymbolicState::storage(ContractDefinition const& _contract) const
+{
+	return smt::member(m_state->member("storage"), contractStorageKey(_contract));
+}
+
+smtutil::Expression SymbolicState::storage(ContractDefinition const& _contract, smtutil::Expression _address) const
+{
+	return smtutil::Expression::select(storage(_contract), std::move(_address));
+}
+
+smtutil::Expression SymbolicState::addressActive(smtutil::Expression _address) const
+{
+	return smtutil::Expression::select(m_state->member("isActive"), std::move(_address));
+}
+
+void SymbolicState::setAddressActive(
+	smtutil::Expression _address,
+	bool _active
+)
+{
+	m_state->assignMember("isActive", smtutil::Expression::store(
+		m_state->member("isActive"),
+		std::move(_address),
+		smtutil::Expression(_active))
+	);
+}
+
+void SymbolicState::newStorage()
+{
+	auto newStorageVar = SymbolicTupleVariable(
+		m_state->member("storage").sort,
+		"havoc_storage_" + to_string(m_context.newUniqueId()),
+		m_context
+	);
+	m_state->assignMember("storage", newStorageVar.currentValue());
+}
+
+void SymbolicState::writeStateVars(ContractDefinition const& _contract, smtutil::Expression _address)
+{
+	auto stateVars = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract);
+	if (stateVars.empty())
+		return;
+
+	map<string, smtutil::Expression> values;
+	for (auto var: stateVars)
+		values.emplace(stateVarStorageKey(*var, _contract), m_context.variable(*var)->currentValue());
+
+	smtutil::Expression thisStorage = storage(_contract, _address);
+	smtutil::Expression newStorage = smt::assignMember(thisStorage, values);
+	auto newContractStorage = smtutil::Expression::store(
+		storage(_contract), std::move(_address), newStorage
+	);
+	smtutil::Expression newAllStorage = smt::assignMember(m_state->member("storage"), {{contractStorageKey(_contract), newContractStorage}});
+	m_state->assignMember("storage", newAllStorage);
+}
+
+void SymbolicState::readStateVars(ContractDefinition const& _contract, smtutil::Expression _address)
+{
+	auto stateVars = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract);
+	if (stateVars.empty())
+		return;
+
+	auto contractStorage = storage(_contract, std::move(_address));
+	for (auto var: stateVars)
+		m_context.addAssertion(
+			m_context.variable(*var)->increaseIndex() ==
+			smt::member(contractStorage, stateVarStorageKey(*var, _contract))
+		);
 }
 
 void SymbolicState::addBalance(smtutil::Expression _address, smtutil::Expression _value)
@@ -134,7 +204,7 @@ void SymbolicState::addBalance(smtutil::Expression _address, smtutil::Expression
 		_address,
 		balance(_address) + std::move(_value)
 	);
-	m_state.assignMember("balances", newBalances);
+	m_state->assignMember("balances", newBalances);
 }
 
 smtutil::Expression SymbolicState::txMember(string const& _member) const
@@ -194,17 +264,99 @@ smtutil::Expression SymbolicState::txFunctionConstraints(FunctionDefinition cons
 	return conj;
 }
 
-void SymbolicState::prepareForSourceUnit(SourceUnit const& _source)
+void SymbolicState::prepareForSourceUnit(SourceUnit const& _source, bool _storage)
 {
-	set<FunctionCall const*> abiCalls = SMTEncoder::collectABICalls(&_source);
-	for (auto const& source: _source.referencedSourceUnits(true))
+	auto allSources = _source.referencedSourceUnits(true);
+	allSources.insert(&_source);
+	set<FunctionCall const*, ASTCompareByID<FunctionCall>> abiCalls;
+	set<ContractDefinition const*, ASTCompareByID<ContractDefinition>> contracts;
+	for (auto const& source: allSources)
+	{
 		abiCalls += SMTEncoder::collectABICalls(source);
+		for (auto node: source->nodes())
+			if (auto contract = dynamic_cast<ContractDefinition const*>(node.get()))
+				contracts.insert(contract);
+	}
+	buildState(contracts, _storage);
 	buildABIFunctions(abiCalls);
 }
 
 /// Private helpers.
 
-void SymbolicState::buildABIFunctions(set<FunctionCall const*> const& _abiFunctions)
+string SymbolicState::contractSuffix(ContractDefinition const& _contract) const
+{
+	return "_" + _contract.name() + "_" + to_string(_contract.id());
+}
+
+string SymbolicState::contractStorageKey(ContractDefinition const& _contract) const
+{
+	return "storage" + contractSuffix(_contract);
+}
+
+string SymbolicState::stateVarStorageKey(VariableDeclaration const& _var, ContractDefinition const& _contract) const
+{
+	return _var.name() + "_" + to_string(_var.id()) + contractSuffix(_contract);
+}
+
+void SymbolicState::buildState(set<ContractDefinition const*, ASTCompareByID<ContractDefinition>> const& _contracts, bool _allStorages)
+{
+	map<string, SortPointer> stateMembers{
+		{"balances", make_shared<smtutil::ArraySort>(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort)}
+	};
+
+	if (_allStorages)
+	{
+		vector<string> memberNames;
+		vector<SortPointer> memberSorts;
+		for (auto contract: _contracts)
+		{
+			string suffix = contractSuffix(*contract);
+
+			// z3 doesn't like empty tuples, so if the contract has 0
+			// state vars we can't put it there.
+			auto stateVars = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*contract);
+			if (stateVars.empty())
+				continue;
+
+			auto names = applyMap(stateVars, [&](auto var) {
+				return var->name() + "_" + to_string(var->id()) + suffix;
+			});
+			auto sorts = applyMap(stateVars, [](auto var) { return smtSortAbstractFunction(*var->type()); });
+
+			string name = "storage" + suffix;
+			auto storageTuple = make_shared<smtutil::TupleSort>(
+				name + "_type", names, sorts
+			);
+
+			auto storageSort = make_shared<smtutil::ArraySort>(
+				smtSort(*TypeProvider::address()),
+				storageTuple
+			);
+
+			memberNames.emplace_back(name);
+			memberSorts.emplace_back(storageSort);
+		}
+
+		stateMembers.emplace(
+			"isActive",
+			make_shared<smtutil::ArraySort>(smtSort(*TypeProvider::address()), smtutil::SortProvider::boolSort)
+		);
+		stateMembers.emplace(
+			"storage",
+			make_shared<smtutil::TupleSort>(
+				"storage_type", memberNames, memberSorts
+			)
+		);
+	}
+
+	m_state = make_unique<BlockchainVariable>(
+		"state",
+		std::move(stateMembers),
+		m_context
+	);
+}
+
+void SymbolicState::buildABIFunctions(set<FunctionCall const*, ASTCompareByID<FunctionCall>> const& _abiFunctions)
 {
 	map<string, SortPointer> functions;
 

libsolidity/formal/SymbolicState.h

@@ -62,7 +62,8 @@ private:
  * - this (the address of the currently executing contract)
  * - state, represented as a tuple of:
  *   - balances
- *   - TODO: potentially storage of contracts
+ *   - array of address => bool representing whether an address is used by a contract
+ *   - storage of contracts
  * - block and transaction properties, represented as a tuple of:
  *   - blockhash
  *   - block basefee
@@ -99,29 +100,41 @@ public:
 	/// @returns the symbolic value of the currently executing contract's address.
 	smtutil::Expression thisAddress() const { return m_thisAddress.currentValue(); }
 	smtutil::Expression thisAddress(unsigned _idx) const { return m_thisAddress.valueAtIndex(_idx); }
+	smtutil::Expression newThisAddress() { return m_thisAddress.increaseIndex(); }
 	smtutil::SortPointer const& thisAddressSort() const { return m_thisAddress.sort(); }
 	//@}
 
 	/// Blockchain state.
 	//@{
-	smtutil::Expression state() const { return m_state.value(); }
-	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(); }
+	smtutil::Expression state() const { solAssert(m_state, ""); return m_state->value(); }
+	smtutil::Expression state(unsigned _idx) const { solAssert(m_state, ""); return m_state->value(_idx); }
+	smtutil::SortPointer const& stateSort() const { solAssert(m_state, ""); return m_state->sort(); }
+	void newState() { solAssert(m_state, ""); m_state->newVar(); }
 
 	void newBalances();
+
+	/// Balance.
 	/// @returns the symbolic balances.
 	smtutil::Expression balances() const;
 	/// @returns the symbolic balance of address `this`.
 	smtutil::Expression balance() const;
 	/// @returns the symbolic balance of an address.
 	smtutil::Expression balance(smtutil::Expression _address) const;
-
 	/// 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);
+
+	/// Storage.
+	smtutil::Expression storage(ContractDefinition const& _contract) const;
+	smtutil::Expression storage(ContractDefinition const& _contract, smtutil::Expression _address) const;
+	smtutil::Expression addressActive(smtutil::Expression _address) const;
+	void setAddressActive(smtutil::Expression _address, bool _active);
+
+	void newStorage();
+	void writeStateVars(ContractDefinition const& _contract, smtutil::Expression _address);
+	void readStateVars(ContractDefinition const& _contract, smtutil::Expression _address);
 	//@}
 
 	/// Transaction data.
@@ -149,11 +162,15 @@ public:
 	smtutil::Expression cryptoFunction(std::string const& _member) const { return m_crypto.member(_member); }
 	//@}
 
+	/// Calls the internal methods that build
+	/// - the symbolic ABI functions based on the abi.* calls
+	///   in _source and referenced sources.
+	/// - the symbolic storages for all contracts in _source and
+	///   referenced sources.
+	void prepareForSourceUnit(SourceUnit const& _source, bool _storage);
+
 	/// 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,
@@ -169,8 +186,15 @@ public:
 	//@}
 
 private:
+	std::string contractSuffix(ContractDefinition const& _contract) const;
+	std::string contractStorageKey(ContractDefinition const& _contract) const;
+	std::string stateVarStorageKey(VariableDeclaration const& _var, ContractDefinition const& _contract) const;
+
+	/// Builds state.storage based on _contracts.
+	void buildState(std::set<ContractDefinition const*, ASTCompareByID<ContractDefinition>> const& _contracts, bool _allStorages);
+
 	/// Builds m_abi based on the abi.* calls _abiFunctions.
-	void buildABIFunctions(std::set<FunctionCall const*> const& _abiFunctions);
+	void buildABIFunctions(std::set<FunctionCall const*, ASTCompareByID<FunctionCall>> const& _abiFunctions);
 
 	EncodingContext& m_context;
 
@@ -186,11 +210,14 @@ private:
 		m_context
 	};
 
-	BlockchainVariable m_state{
-		"state",
-		{{"balances", std::make_shared<smtutil::ArraySort>(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort)}},
-		m_context
-	};
+	/// m_state is a tuple of
+	/// - balances: array of address to balance of address.
+	/// - isActive: array of address to Boolean, where element is true iff address is used.
+	/// - storage: tuple containing the storage of every contract, where
+	/// each element of the tuple represents a contract,
+	/// and is defined by an array where the index is the contract's address
+	/// and the element is a tuple containing the state variables of that contract.
+	std::unique_ptr<BlockchainVariable> m_state;
 
 	BlockchainVariable m_tx{
 		"tx",

libsolidity/formal/SymbolicTypes.cpp

@@ -618,4 +618,26 @@ optional<smtutil::Expression> symbolicTypeConversion(frontend::Type const* _from
 	return std::nullopt;
 }
 
+smtutil::Expression member(smtutil::Expression const& _tuple, string const& _member)
+{
+	TupleSort const& _sort = dynamic_cast<TupleSort const&>(*_tuple.sort);
+	return smtutil::Expression::tuple_get(
+		_tuple,
+		_sort.memberToIndex.at(_member)
+	);
+}
+
+smtutil::Expression assignMember(smtutil::Expression const _tuple, map<string, smtutil::Expression> const& _values)
+{
+	TupleSort const& _sort = dynamic_cast<TupleSort const&>(*_tuple.sort);
+	vector<smtutil::Expression> args;
+	for (auto const& m: _sort.members)
+		if (auto* value = util::valueOrNullptr(_values, m))
+			args.emplace_back(*value);
+		else
+			args.emplace_back(member(_tuple, m));
+	auto sortExpr = smtutil::Expression(make_shared<smtutil::SortSort>(_tuple.sort), _tuple.name);
+	return smtutil::Expression::tuple_constructor(sortExpr, args);
+}
+
 }

libsolidity/formal/SymbolicTypes.h

@@ -82,4 +82,8 @@ void setSymbolicUnknownValue(smtutil::Expression _expr, frontend::Type const* _t
 smtutil::Expression symbolicUnknownConstraints(smtutil::Expression _expr, frontend::Type const* _type);
 
 std::optional<smtutil::Expression> symbolicTypeConversion(frontend::Type const* _from, frontend::Type const* _to);
+
+smtutil::Expression member(smtutil::Expression const& _tuple, std::string const& _member);
+smtutil::Expression assignMember(smtutil::Expression const _tuple, std::map<std::string, smtutil::Expression> const& _values);
+
 }

libsolidity/interface/StandardCompiler.cpp

@@ -445,7 +445,7 @@ std::optional<Json::Value> checkSettingsKeys(Json::Value const& _input)
 
 std::optional<Json::Value> checkModelCheckerSettingsKeys(Json::Value const& _input)
 {
-	static set<string> keys{"contracts", "divModNoSlacks", "engine", "invariants", "showUnproved", "solvers", "targets", "timeout"};
+	static set<string> keys{"contracts", "divModNoSlacks", "engine", "extCalls", "invariants", "showUnproved", "solvers", "targets", "timeout"};
 	return checkKeys(_input, keys, "modelChecker");
 }
 
@@ -1016,6 +1016,16 @@ std::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompiler:
 		ret.modelCheckerSettings.engine = *engine;
 	}
 
+	if (modelCheckerSettings.isMember("extCalls"))
+	{
+		if (!modelCheckerSettings["extCalls"].isString())
+			return formatFatalError(Error::Type::JSONError, "settings.modelChecker.extCalls must be a string.");
+		std::optional<ModelCheckerExtCalls> extCalls = ModelCheckerExtCalls::fromString(modelCheckerSettings["extCalls"].asString());
+		if (!extCalls)
+			return formatFatalError(Error::Type::JSONError, "Invalid model checker extCalls requested.");
+		ret.modelCheckerSettings.externalCalls = *extCalls;
+	}
+
 	if (modelCheckerSettings.isMember("invariants"))
 	{
 		auto const& invariantsArray = modelCheckerSettings["invariants"];