Merge pull request #10010 from ethereum/develop

Merge develop into breaking.

libsolidity/analysis/DeclarationContainer.cpp

@@ -100,6 +100,7 @@ bool DeclarationContainer::isInvisible(ASTString const& _name) const
 bool DeclarationContainer::registerDeclaration(
 	Declaration const& _declaration,
 	ASTString const* _name,
+	langutil::SourceLocation const* _location,
 	bool _invisible,
 	bool _update
 )
@@ -115,8 +116,18 @@ bool DeclarationContainer::registerDeclaration(
 		m_declarations.erase(*_name);
 		m_invisibleDeclarations.erase(*_name);
 	}
-	else if (conflictingDeclaration(_declaration, _name))
-		return false;
+	else
+	{
+		if (conflictingDeclaration(_declaration, _name))
+			return false;
+
+		// Do not warn about shadowing for structs and enums because their members are
+		// not accessible without prefixes. Also do not warn about event parameters
+		// because they do not participate in any proper scope.
+		bool special = _declaration.scope() && (_declaration.isStructMember() || _declaration.isEnumValue() || _declaration.isEventParameter());
+		if (m_enclosingContainer && !special)
+			m_homonymCandidates.emplace_back(*_name, _location ? _location : &_declaration.location());
+	}
 
 	vector<Declaration const*>& decls = _invisible ? m_invisibleDeclarations[*_name] : m_declarations[*_name];
 	if (!util::contains(decls, &_declaration))
@@ -124,6 +135,15 @@ bool DeclarationContainer::registerDeclaration(
 	return true;
 }
 
+bool DeclarationContainer::registerDeclaration(
+	Declaration const& _declaration,
+	bool _invisible,
+	bool _update
+)
+{
+	return registerDeclaration(_declaration, nullptr, nullptr, _invisible, _update);
+}
+
 vector<Declaration const*> DeclarationContainer::resolveName(ASTString const& _name, bool _recursive, bool _alsoInvisible) const
 {
 	solAssert(!_name.empty(), "Attempt to resolve empty name.");
@@ -164,3 +184,16 @@ vector<ASTString> DeclarationContainer::similarNames(ASTString const& _name) con
 
 	return similar;
 }
+
+void DeclarationContainer::populateHomonyms(back_insert_iterator<Homonyms> _it) const
+{
+	for (DeclarationContainer const* innerContainer: m_innerContainers)
+		innerContainer->populateHomonyms(_it);
+
+	for (auto [name, location]: m_homonymCandidates)
+	{
+		vector<Declaration const*> const& declarations = m_enclosingContainer->resolveName(name, true, true);
+		if (!declarations.empty())
+			_it = make_pair(location, declarations);
+	}
+}

libsolidity/analysis/DeclarationContainer.h

@@ -24,9 +24,9 @@
 #pragma once
 
 #include <libsolidity/ast/ASTForward.h>
+#include <liblangutil/Exceptions.h>
+#include <liblangutil/SourceLocation.h>
 #include <boost/noncopyable.hpp>
-#include <map>
-#include <set>
 
 namespace solidity::frontend
 {
@@ -38,17 +38,26 @@ namespace solidity::frontend
 class DeclarationContainer
 {
 public:
+	using Homonyms = std::vector<std::pair<langutil::SourceLocation const*, std::vector<Declaration const*>>>;
+
 	explicit DeclarationContainer(
 		ASTNode const* _enclosingNode = nullptr,
-		DeclarationContainer const* _enclosingContainer = nullptr
+		DeclarationContainer* _enclosingContainer = nullptr
 	):
-		m_enclosingNode(_enclosingNode), m_enclosingContainer(_enclosingContainer) {}
+		m_enclosingNode(_enclosingNode), m_enclosingContainer(_enclosingContainer)
+	{
+		if (_enclosingContainer)
+			_enclosingContainer->m_innerContainers.emplace_back(this);
+	}
 	/// Registers the declaration in the scope unless its name is already declared or the name is empty.
 	/// @param _name the name to register, if nullptr the intrinsic name of @a _declaration is used.
-	/// @param _invisible if true, registers the declaration, reports name clashes but does not return it in @a resolveName
-	/// @param _update if true, replaces a potential declaration that is already present
+	/// @param _location alternative location, used to point at homonymous declarations.
+	/// @param _invisible if true, registers the declaration, reports name clashes but does not return it in @a resolveName.
+	/// @param _update if true, replaces a potential declaration that is already present.
 	/// @returns false if the name was already declared.
-	bool registerDeclaration(Declaration const& _declaration, ASTString const* _name = nullptr, bool _invisible = false, bool _update = false);
+	bool registerDeclaration(Declaration const& _declaration, ASTString const* _name, langutil::SourceLocation const* _location, bool _invisible, bool _update);
+	bool registerDeclaration(Declaration const& _declaration, bool _invisible, bool _update);
+
 	std::vector<Declaration const*> resolveName(ASTString const& _name, bool _recursive = false, bool _alsoInvisible = false) const;
 	ASTNode const* enclosingNode() const { return m_enclosingNode; }
 	DeclarationContainer const* enclosingContainer() const { return m_enclosingContainer; }
@@ -67,11 +76,18 @@ public:
 	/// Searches this and all parent containers.
 	std::vector<ASTString> similarNames(ASTString const& _name) const;
 
+	/// Populates a vector of (location, declaration) pairs, where location is a location of an inner-scope declaration,
+	/// and declaration is the corresponding homonymous outer-scope declaration.
+	void populateHomonyms(std::back_insert_iterator<Homonyms> _it) const;
+
 private:
 	ASTNode const* m_enclosingNode;
 	DeclarationContainer const* m_enclosingContainer;
+	std::vector<DeclarationContainer const*> m_innerContainers;
 	std::map<ASTString, std::vector<Declaration const*>> m_declarations;
 	std::map<ASTString, std::vector<Declaration const*>> m_invisibleDeclarations;
+	/// List of declarations (name and location) to check later for homonymity.
+	std::vector<std::pair<std::string, langutil::SourceLocation const*>> m_homonymCandidates;
 };
 
 }

libsolidity/analysis/NameAndTypeResolver.cpp

@@ -28,6 +28,7 @@
 #include <liblangutil/ErrorReporter.h>
 #include <libsolutil/StringUtils.h>
 #include <boost/algorithm/string.hpp>
+#include <unordered_set>
 
 using namespace std;
 using namespace solidity::langutil;
@@ -47,7 +48,7 @@ NameAndTypeResolver::NameAndTypeResolver(
 	m_scopes[nullptr] = make_shared<DeclarationContainer>();
 	for (Declaration const* declaration: _globalContext.declarations())
 	{
-		solAssert(m_scopes[nullptr]->registerDeclaration(*declaration), "Unable to register global declaration.");
+		solAssert(m_scopes[nullptr]->registerDeclaration(*declaration, false, false), "Unable to register global declaration.");
 	}
 }
 
@@ -149,7 +150,7 @@ bool NameAndTypeResolver::updateDeclaration(Declaration const& _declaration)
 {
 	try
 	{
-		m_scopes[nullptr]->registerDeclaration(_declaration, nullptr, false, true);
+		m_scopes[nullptr]->registerDeclaration(_declaration, false, true);
 		solAssert(_declaration.scope() == nullptr, "Updated declaration outside global scope.");
 	}
 	catch (langutil::FatalError const&)
@@ -202,7 +203,7 @@ Declaration const* NameAndTypeResolver::pathFromCurrentScope(vector<ASTString> c
 		return nullptr;
 }
 
-void NameAndTypeResolver::warnVariablesNamedLikeInstructions()
+void NameAndTypeResolver::warnVariablesNamedLikeInstructions() const
 {
 	for (auto const& instruction: evmasm::c_instructions)
 	{
@@ -223,6 +224,52 @@ void NameAndTypeResolver::warnVariablesNamedLikeInstructions()
 	}
 }
 
+void NameAndTypeResolver::warnHomonymDeclarations() const
+{
+	DeclarationContainer::Homonyms homonyms;
+	m_scopes.at(nullptr)->populateHomonyms(back_inserter(homonyms));
+
+	for (auto [innerLocation, outerDeclarations]: homonyms)
+	{
+		solAssert(innerLocation && !outerDeclarations.empty(), "");
+
+		bool magicShadowed = false;
+		SecondarySourceLocation homonymousLocations;
+		SecondarySourceLocation shadowedLocations;
+		for (Declaration const* outerDeclaration: outerDeclarations)
+		{
+			solAssert(outerDeclaration, "");
+			if (dynamic_cast<MagicVariableDeclaration const*>(outerDeclaration))
+				magicShadowed = true;
+			else if (!outerDeclaration->isVisibleInContract())
+				homonymousLocations.append("The other declaration is here:", outerDeclaration->location());
+			else
+				shadowedLocations.append("The shadowed declaration is here:", outerDeclaration->location());
+		}
+
+		if (magicShadowed)
+			m_errorReporter.warning(
+				2319_error,
+				*innerLocation,
+				"This declaration shadows a builtin symbol."
+			);
+		if (!homonymousLocations.infos.empty())
+			m_errorReporter.warning(
+				8760_error,
+				*innerLocation,
+				"This declaration has the same name as another declaration.",
+				homonymousLocations
+			);
+		if (!shadowedLocations.infos.empty())
+			m_errorReporter.warning(
+				2519_error,
+				*innerLocation,
+				"This declaration shadows an existing declaration.",
+				shadowedLocations
+			);
+	}
+}
+
 void NameAndTypeResolver::setScope(ASTNode const* _node)
 {
 	m_currentScope = m_scopes[_node].get();
@@ -281,8 +328,8 @@ bool NameAndTypeResolver::resolveNamesAndTypesInternal(ASTNode& _node, bool _res
 		}
 
 		// make "this" and "super" invisible.
-		m_scopes[nullptr]->registerDeclaration(*m_globalContext.currentThis(), nullptr, true, true);
-		m_scopes[nullptr]->registerDeclaration(*m_globalContext.currentSuper(), nullptr, true, true);
+		m_scopes[nullptr]->registerDeclaration(*m_globalContext.currentThis(), true, true);
+		m_scopes[nullptr]->registerDeclaration(*m_globalContext.currentSuper(), true, true);
 		m_globalContext.resetCurrentContract();
 
 		return success;
@@ -303,7 +350,7 @@ void NameAndTypeResolver::importInheritedScope(ContractDefinition const& _base)
 		for (auto const& declaration: nameAndDeclaration.second)
 			// Import if it was declared in the base, is not the constructor and is visible in derived classes
 			if (declaration->scope() == &_base && declaration->isVisibleInDerivedContracts())
-				if (!m_currentScope->registerDeclaration(*declaration))
+				if (!m_currentScope->registerDeclaration(*declaration, false, false))
 				{
 					SourceLocation firstDeclarationLocation;
 					SourceLocation secondDeclarationLocation;
@@ -458,19 +505,11 @@ bool DeclarationRegistrationHelper::registerDeclaration(
 		_errorLocation = &_declaration.location();
 
 	string name = _name ? *_name : _declaration.name();
-	Declaration const* shadowedDeclaration = nullptr;
-	// Do not warn about shadowing for structs and enums because their members are
-	// not accessible without prefixes. Also do not warn about event parameters
-	// because they do not participate in any proper scope.
-	bool warnOnShadow = !_declaration.isStructMember() && !_declaration.isEnumValue() && !_declaration.isEventParameter();
-	if (warnOnShadow && !name.empty() && _container.enclosingContainer())
-		for (auto const* decl: _container.enclosingContainer()->resolveName(name, true, true))
-			shadowedDeclaration = decl;
 
 	// We use "invisible" for both inactive variables in blocks and for members invisible in contracts.
 	// They cannot both be true at the same time.
 	solAssert(!(_inactive && !_declaration.isVisibleInContract()), "");
-	if (!_container.registerDeclaration(_declaration, _name, !_declaration.isVisibleInContract() || _inactive))
+	if (!_container.registerDeclaration(_declaration, _name, _errorLocation, !_declaration.isVisibleInContract() || _inactive, false))
 	{
 		SourceLocation firstDeclarationLocation;
 		SourceLocation secondDeclarationLocation;
@@ -499,34 +538,7 @@ bool DeclarationRegistrationHelper::registerDeclaration(
 		);
 		return false;
 	}
-	else if (shadowedDeclaration)
-	{
-		if (dynamic_cast<MagicVariableDeclaration const*>(shadowedDeclaration))
-			_errorReporter.warning(
-				2319_error,
-				*_errorLocation,
-				"This declaration shadows a builtin symbol."
-			);
-		else
-		{
-			auto shadowedLocation = shadowedDeclaration->location();
 
-			if (!shadowedDeclaration->isVisibleInContract())
-				_errorReporter.warning(
-					8760_error,
-					_declaration.location(),
-					"This declaration has the same name as another declaration.",
-					SecondarySourceLocation().append("The other declaration is here:", shadowedLocation)
-				);
-			else
-				_errorReporter.warning(
-					2519_error,
-					_declaration.location(),
-					"This declaration shadows an existing declaration.",
-					SecondarySourceLocation().append("The shadowed declaration is here:", shadowedLocation)
-			);
-		}
-	}
 	return true;
 }
 
@@ -556,8 +568,8 @@ bool DeclarationRegistrationHelper::visit(ImportDirective& _import)
 bool DeclarationRegistrationHelper::visit(ContractDefinition& _contract)
 {
 	m_globalContext.setCurrentContract(_contract);
-	m_scopes[nullptr]->registerDeclaration(*m_globalContext.currentThis(), nullptr, false, true);
-	m_scopes[nullptr]->registerDeclaration(*m_globalContext.currentSuper(), nullptr, false, true);
+	m_scopes[nullptr]->registerDeclaration(*m_globalContext.currentThis(), false, true);
+	m_scopes[nullptr]->registerDeclaration(*m_globalContext.currentSuper(), false, true);
 	m_currentContract = &_contract;
 
 	return ASTVisitor::visit(_contract);
@@ -566,8 +578,8 @@ bool DeclarationRegistrationHelper::visit(ContractDefinition& _contract)
 void DeclarationRegistrationHelper::endVisit(ContractDefinition& _contract)
 {
 	// make "this" and "super" invisible.
-	m_scopes[nullptr]->registerDeclaration(*m_globalContext.currentThis(), nullptr, true, true);
-	m_scopes[nullptr]->registerDeclaration(*m_globalContext.currentSuper(), nullptr, true, true);
+	m_scopes[nullptr]->registerDeclaration(*m_globalContext.currentThis(), true, true);
+	m_scopes[nullptr]->registerDeclaration(*m_globalContext.currentSuper(), true, true);
 	m_globalContext.resetCurrentContract();
 	m_currentContract = nullptr;
 	ASTVisitor::endVisit(_contract);
@@ -612,11 +624,14 @@ void DeclarationRegistrationHelper::endVisitNode(ASTNode& _node)
 
 void DeclarationRegistrationHelper::enterNewSubScope(ASTNode& _subScope)
 {
-	shared_ptr<DeclarationContainer> container{make_shared<DeclarationContainer>(m_currentScope, m_scopes[m_currentScope].get())};
-	bool newlyAdded = m_scopes.emplace(&_subScope, move(container)).second;
-	// Source units are the only AST nodes for which containers can be created from multiple places
-	// due to imports.
-	solAssert(newlyAdded || dynamic_cast<SourceUnit const*>(&_subScope), "Unable to add new scope.");
+	if (m_scopes.count(&_subScope))
+		// Source units are the only AST nodes for which containers can be created from multiple places due to imports.
+		solAssert(dynamic_cast<SourceUnit const*>(&_subScope), "Unexpected scope type.");
+	else
+	{
+		bool newlyAdded = m_scopes.emplace(&_subScope, make_shared<DeclarationContainer>(m_currentScope, m_scopes[m_currentScope].get())).second;
+		solAssert(newlyAdded, "Unable to add new scope.");
+	}
 	m_currentScope = &_subScope;
 }
 

libsolidity/analysis/NameAndTypeResolver.h

@@ -93,7 +93,10 @@ public:
 	Declaration const* pathFromCurrentScope(std::vector<ASTString> const& _path) const;
 
 	/// Generate and store warnings about variables that are named like instructions.
-	void warnVariablesNamedLikeInstructions();
+	void warnVariablesNamedLikeInstructions() const;
+
+	/// Generate and store warnings about declarations with the same name.
+	void warnHomonymDeclarations() const;
 
 	/// @returns a list of similar identifiers in the current and enclosing scopes. May return empty string if no suggestions.
 	std::string similarNameSuggestions(ASTString const& _name) const;

libsolidity/codegen/CompilerContext.h

@@ -78,6 +78,7 @@ public:
 
 	/// Update currently enabled set of experimental features.
 	void setExperimentalFeatures(std::set<ExperimentalFeature> const& _features) { m_experimentalFeatures = _features; }
+	std::set<ExperimentalFeature> const& experimentalFeaturesActive() const { return m_experimentalFeatures; }
 	/// @returns true if the given feature is enabled.
 	bool experimentalFeatureActive(ExperimentalFeature _feature) const { return m_experimentalFeatures.count(_feature); }
 

libsolidity/codegen/ContractCompiler.cpp

@@ -1326,9 +1326,14 @@ void ContractCompiler::appendModifierOrFunctionCode()
 
 	if (codeBlock)
 	{
+		std::set<ExperimentalFeature> experimentalFeaturesOutside = m_context.experimentalFeaturesActive();
+		m_context.setExperimentalFeatures(codeBlock->sourceUnit().annotation().experimentalFeatures);
+
 		m_returnTags.emplace_back(m_context.newTag(), m_context.stackHeight());
 		codeBlock->accept(*this);
 
+		m_context.setExperimentalFeatures(experimentalFeaturesOutside);
+
 		solAssert(!m_returnTags.empty(), "");
 		m_context << m_returnTags.back().first;
 		m_returnTags.pop_back();

libsolidity/codegen/ExpressionCompiler.cpp

@@ -1772,6 +1772,11 @@ bool ExpressionCompiler::visit(MemberAccess const& _memberAccess)
 			solAssert(*_memberAccess.annotation().requiredLookup == VirtualLookup::Static, "");
 			utils().pushCombinedFunctionEntryLabel(*function);
 		}
+		else if (auto const* contract = dynamic_cast<ContractDefinition const*>(_memberAccess.annotation().referencedDeclaration))
+		{
+			if (contract->isLibrary())
+				m_context.appendLibraryAddress(contract->fullyQualifiedName());
+		}
 		break;
 	}
 	default:

libsolidity/codegen/YulUtilFunctions.h

@@ -86,7 +86,6 @@ public:
 
 	/// @returns the name of a function that performs a left shift and subsequent cleanup
 	/// and, if needed, prior cleanup.
-	/// If the amount to shift by is signed, a check for negativeness is performed.
 	/// signature: (value, amountToShift) -> result
 	std::string typedShiftLeftFunction(Type const& _type, Type const& _amountType);
 	std::string typedShiftRightFunction(Type const& _type, Type const& _amountType);

libsolidity/formal/BMC.cpp

@@ -396,7 +396,6 @@ void BMC::endVisit(FunctionCall const& _funCall)
 	case FunctionType::Kind::Send:
 	case FunctionType::Kind::Transfer:
 	{
-		SMTEncoder::endVisit(_funCall);
 		auto value = _funCall.arguments().front();
 		solAssert(value, "");
 		smtutil::Expression thisBalance = m_context.state().balance();
@@ -406,6 +405,8 @@ void BMC::endVisit(FunctionCall const& _funCall)
 			thisBalance < expr(*value),
 			&_funCall
 		);
+
+		SMTEncoder::endVisit(_funCall);
 		break;
 	}
 	case FunctionType::Kind::AddMod:

libsolidity/formal/CHC.cpp

@@ -101,7 +101,7 @@ bool CHC::visit(ContractDefinition const& _contract)
 
 	solAssert(m_currentContract, "");
 	m_constructorSummaryPredicate = createSymbolicBlock(
-		constructorSort(*m_currentContract),
+		constructorSort(*m_currentContract, state()),
 		"summary_constructor_" + contractSuffix(_contract),
 		PredicateType::ConstructorSummary,
 		&_contract
@@ -114,15 +114,16 @@ bool CHC::visit(ContractDefinition const& _contract)
 void CHC::endVisit(ContractDefinition const& _contract)
 {
 	auto implicitConstructorPredicate = createSymbolicBlock(
-		implicitConstructorSort(),
+		implicitConstructorSort(state()),
 		"implicit_constructor_" + contractSuffix(_contract),
 		PredicateType::ImplicitConstructor,
 		&_contract
 	);
-	auto implicitConstructor = (*implicitConstructorPredicate)({});
-	addRule(implicitConstructor, implicitConstructor.name);
-	m_currentBlock = implicitConstructor;
-	m_context.addAssertion(errorFlag().currentValue() == 0);
+	addRule(
+		(*implicitConstructorPredicate)({0, state().thisAddress(), state().state()}),
+		implicitConstructorPredicate->functor().name
+	);
+	setCurrentBlock(*implicitConstructorPredicate);
 
 	if (auto constructor = _contract.constructor())
 		constructor->accept(*this);
@@ -178,6 +179,7 @@ bool CHC::visit(FunctionDefinition const& _function)
 		m_context.addAssertion(m_context.variable(*var)->valueAtIndex(0) == currentValue(*var));
 	for (auto const& var: _function.parameters())
 		m_context.addAssertion(m_context.variable(*var)->valueAtIndex(0) == currentValue(*var));
+	m_context.addAssertion(state().state(0) == state().state());
 
 	connectBlocks(functionPred, bodyPred);
 
@@ -215,7 +217,7 @@ void CHC::endVisit(FunctionDefinition const& _function)
 			string suffix = m_currentContract->name() + "_" + to_string(m_currentContract->id());
 			solAssert(m_currentContract, "");
 			auto constructorExit = createSymbolicBlock(
-				constructorSort(*m_currentContract),
+				constructorSort(*m_currentContract, state()),
 				"constructor_exit_" + suffix,
 				PredicateType::ConstructorSummary,
 				m_currentContract
@@ -234,7 +236,7 @@ void CHC::endVisit(FunctionDefinition const& _function)
 
 			setCurrentBlock(*m_interfaces.at(m_currentContract));
 
-			auto ifacePre = (*m_interfaces.at(m_currentContract))(initialStateVariables());
+			auto ifacePre = smt::interfacePre(*m_interfaces.at(m_currentContract), *m_currentContract, m_context);
 			if (_function.isPublic())
 			{
 				addAssertVerificationTarget(&_function, ifacePre, sum, assertionError);
@@ -598,15 +600,21 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 	for (auto var: function->returnParameters())
 		m_context.variable(*var)->increaseIndex();
 
-	auto preCallState = currentStateVariables();
+	auto preCallState = vector<smtutil::Expression>{state().state()} + currentStateVariables();
 	bool usesStaticCall = kind == FunctionType::Kind::BareStaticCall ||
 		function->stateMutability() == StateMutability::Pure ||
 		function->stateMutability() == StateMutability::View;
 	if (!usesStaticCall)
+	{
+		state().newState();
 		for (auto const* var: m_stateVariables)
 			m_context.variable(*var)->increaseIndex();
+	}
 
-	auto nondet = (*m_nondetInterfaces.at(m_currentContract))(preCallState + currentStateVariables());
+	auto postCallState = vector<smtutil::Expression>{state().state()} + currentStateVariables();
+	auto nondet = (*m_nondetInterfaces.at(m_currentContract))(preCallState + postCallState);
+	// TODO this could instead add the summary of the called function, where that summary
+	// basically has the nondet interface of this summary as a constraint.
 	m_context.addAssertion(nondet);
 
 	m_context.addAssertion(errorFlag().currentValue() == 0);
@@ -775,6 +783,8 @@ void CHC::clearIndices(ContractDefinition const* _contract, FunctionDefinition c
 		for (auto const& var: _function->localVariables())
 			m_context.variable(*var)->increaseIndex();
 	}
+
+	state().newState();
 }
 
 void CHC::setCurrentBlock(Predicate const& _block)
@@ -800,7 +810,7 @@ set<frontend::Expression const*, CHC::IdCompare> CHC::transactionAssertions(ASTN
 
 SortPointer CHC::sort(FunctionDefinition const& _function)
 {
-	return functionSort(_function, m_currentContract);
+	return functionSort(_function, m_currentContract, state());
 }
 
 SortPointer CHC::sort(ASTNode const* _node)
@@ -809,7 +819,7 @@ SortPointer CHC::sort(ASTNode const* _node)
 		return sort(*funDef);
 
 	solAssert(m_currentFunction, "");
-	return functionBodySort(*m_currentFunction, m_currentContract);
+	return functionBodySort(*m_currentFunction, m_currentContract, state());
 }
 
 Predicate const* CHC::createSymbolicBlock(SortPointer _sort, string const& _name, PredicateType _predType, ASTNode const* _node)
@@ -825,8 +835,8 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 		if (auto const* contract = dynamic_cast<ContractDefinition const*>(node.get()))
 		{
 			string suffix = contract->name() + "_" + to_string(contract->id());
-			m_interfaces[contract] = createSymbolicBlock(interfaceSort(*contract), "interface_" + suffix, PredicateType::Interface, contract);
-			m_nondetInterfaces[contract] = createSymbolicBlock(nondetInterfaceSort(*contract), "nondet_interface_" + suffix, PredicateType::NondetInterface, contract);
+			m_interfaces[contract] = createSymbolicBlock(interfaceSort(*contract, state()), "interface_" + suffix, PredicateType::Interface, contract);
+			m_nondetInterfaces[contract] = createSymbolicBlock(nondetInterfaceSort(*contract, state()), "nondet_interface_" + suffix, PredicateType::NondetInterface, contract);
 
 			for (auto const* var: stateVariablesIncludingInheritedAndPrivate(*contract))
 				if (!m_context.knownVariable(*var))
@@ -836,8 +846,7 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 			/// 0 steps to be taken, used as base for the inductive
 			/// rule for each function.
 			auto const& iface = *m_nondetInterfaces.at(contract);
-			auto state0 = stateVariablesAtIndex(0, *contract);
-			addRule(iface(state0 + state0), "base_nondet");
+			addRule(smt::nondetInterface(iface, *contract, m_context, 0, 0), "base_nondet");
 
 			for (auto const* base: contract->annotation().linearizedBaseContracts)
 				for (auto const* function: base->definedFunctions())
@@ -861,12 +870,13 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 						auto state1 = stateVariablesAtIndex(1, *contract);
 						auto state2 = stateVariablesAtIndex(2, *contract);
 
-						auto nondetPre = iface(state0 + state1);
-						auto nondetPost = iface(state0 + state2);
+						auto nondetPre = smt::nondetInterface(iface, *contract, m_context, 0, 1);
+						auto nondetPost = smt::nondetInterface(iface, *contract, m_context, 0, 2);
 
-						vector<smtutil::Expression> args{errorFlag().currentValue()};
+						vector<smtutil::Expression> args{errorFlag().currentValue(), state().thisAddress(), state().state(1)};
 						args += state1 +
 							applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); }) +
+							vector<smtutil::Expression>{state().state(2)} +
 							state2 +
 							applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 1); }) +
 							applyMap(function->returnParameters(), [this](auto _var) { return valueAtIndex(*_var, 1); });
@@ -930,7 +940,7 @@ Predicate const* CHC::createBlock(ASTNode const* _node, PredicateType _predType,
 Predicate const* CHC::createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract)
 {
 	auto block = createSymbolicBlock(
-		functionSort(_function, &_contract),
+		functionSort(_function, &_contract, state()),
 		"summary_" + uniquePrefix() + "_" + predicateName(&_function, &_contract),
 		PredicateType::FunctionSummary,
 		&_function
@@ -1042,7 +1052,7 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
 		return smtutil::Expression(true);
 
 	errorFlag().increaseIndex();
-	vector<smtutil::Expression> args{errorFlag().currentValue()};
+	vector<smtutil::Expression> args{errorFlag().currentValue(), state().thisAddress(), state().state()};
 
 	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
 	solAssert(funType.kind() == FunctionType::Kind::Internal, "");
@@ -1058,11 +1068,17 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
 	auto const* calledContract = contract->isLibrary() ? contract : m_currentContract;
 	solAssert(calledContract, "");
 
+	bool usesStaticCall = function->stateMutability() == StateMutability::Pure || function->stateMutability() == StateMutability::View;
+
 	args += currentStateVariables(*calledContract);
 	args += symbolicArguments(_funCall);
-	if (!calledContract->isLibrary())
+	if (!calledContract->isLibrary() && !usesStaticCall)
+	{
+		state().newState();
 		for (auto const& var: m_stateVariables)
 			m_context.variable(*var)->increaseIndex();
+	}
+	args += vector<smtutil::Expression>{state().state()};
 	args += currentStateVariables(*calledContract);
 
 	for (auto var: function->parameters() + function->returnParameters())
@@ -1152,7 +1168,7 @@ void CHC::addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type
 		addVerificationTarget(_scope, _type, summary(*m_currentContract), smtutil::Expression(true), _errorId);
 	else
 	{
-		auto iface = (*m_interfaces.at(m_currentContract))(initialStateVariables());
+		auto iface = smt::interfacePre(*m_interfaces.at(m_currentContract), *m_currentContract, m_context);
 		auto sum = summary(*m_currentFunction);
 		addVerificationTarget(_scope, _type, iface, sum, _errorId);
 	}
@@ -1444,7 +1460,12 @@ unsigned CHC::newErrorId(frontend::Expression const& _expr)
 	return errorId;
 }
 
+SymbolicState& CHC::state()
+{
+	return m_context.state();
+}
+
 SymbolicIntVariable& CHC::errorFlag()
 {
-	return m_context.state().errorFlag();
+	return state().errorFlag();
 }

libsolidity/formal/CHC.h

@@ -235,6 +235,7 @@ private:
 	/// it into m_errorIds.
 	unsigned newErrorId(Expression const& _expr);
 
+	smt::SymbolicState& state();
 	smt::SymbolicIntVariable& errorFlag();
 	//@}
 

libsolidity/formal/Predicate.cpp

@@ -161,9 +161,9 @@ string Predicate::formatSummaryCall(vector<string> const& _args) const
 	auto const* fun = programFunction();
 	solAssert(fun, "");
 
-	/// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postStateVars, postInputVars, outputVars).
+	/// The signature of a function summary predicate is: summary(error, this, preBlockChainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
 	/// Here we are interested in preInputVars.
-	vector<string>::const_iterator first = _args.begin() + static_cast<int>(stateVars->size()) + 1;
+	vector<string>::const_iterator first = _args.begin() + 3 + static_cast<int>(stateVars->size());
 	vector<string>::const_iterator last = first + static_cast<int>(fun->parameters().size());
 	solAssert(first >= _args.begin() && first <= _args.end(), "");
 	solAssert(last >= _args.begin() && last <= _args.end(), "");
@@ -188,8 +188,8 @@ string Predicate::formatSummaryCall(vector<string> const& _args) const
 
 vector<string> Predicate::summaryStateValues(vector<string> const& _args) const
 {
-	/// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postStateVars, postInputVars, outputVars).
-	/// The signature of an implicit constructor summary predicate is: summary(error, postStateVars).
+	/// The signature of a function summary predicate is: summary(error, this, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
+	/// The signature of an implicit constructor summary predicate is: summary(error, this, postBlockchainState, postStateVars).
 	/// Here we are interested in postStateVars.
 
 	auto stateVars = stateVariables();
@@ -199,12 +199,12 @@ vector<string> Predicate::summaryStateValues(vector<string> const& _args) const
 	vector<string>::const_iterator stateLast;
 	if (auto const* function = programFunction())
 	{
-		stateFirst = _args.begin() + 1 + static_cast<int>(stateVars->size()) + static_cast<int>(function->parameters().size());
+		stateFirst = _args.begin() + 3 + static_cast<int>(stateVars->size()) + static_cast<int>(function->parameters().size()) + 1;
 		stateLast = stateFirst + static_cast<int>(stateVars->size());
 	}
 	else if (programContract())
 	{
-		stateFirst = _args.begin() + 1;
+		stateFirst = _args.begin() + 3;
 		stateLast = stateFirst + static_cast<int>(stateVars->size());
 	}
 	else
@@ -220,7 +220,7 @@ vector<string> Predicate::summaryStateValues(vector<string> const& _args) const
 
 vector<string> Predicate::summaryPostInputValues(vector<string> const& _args) const
 {
-	/// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postStateVars, postInputVars, outputVars).
+	/// The signature of a function summary predicate is: summary(error, this, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
 	/// Here we are interested in postInputVars.
 	auto const* function = programFunction();
 	solAssert(function, "");
@@ -230,7 +230,7 @@ vector<string> Predicate::summaryPostInputValues(vector<string> const& _args) co
 
 	auto const& inParams = function->parameters();
 
-	vector<string>::const_iterator first = _args.begin() + 1 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size());
+	vector<string>::const_iterator first = _args.begin() + 3 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) + 1;
 	vector<string>::const_iterator last = first + static_cast<int>(inParams.size());
 
 	solAssert(first >= _args.begin() && first <= _args.end(), "");
@@ -243,7 +243,7 @@ vector<string> Predicate::summaryPostInputValues(vector<string> const& _args) co
 
 vector<string> Predicate::summaryPostOutputValues(vector<string> const& _args) const
 {
-	/// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postStateVars, postInputVars, outputVars).
+	/// The signature of a function summary predicate is: summary(error, this, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
 	/// Here we are interested in outputVars.
 	auto const* function = programFunction();
 	solAssert(function, "");
@@ -253,7 +253,7 @@ vector<string> Predicate::summaryPostOutputValues(vector<string> const& _args) c
 
 	auto const& inParams = function->parameters();
 
-	vector<string>::const_iterator first = _args.begin() + 1 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) * 2;
+	vector<string>::const_iterator first = _args.begin() + 3 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) * 2 + 1;
 
 	solAssert(first >= _args.begin() && first <= _args.end(), "");
 

libsolidity/formal/PredicateInstance.cpp

@@ -27,10 +27,35 @@ using namespace solidity::smtutil;
 
 namespace solidity::frontend::smt
 {
+smtutil::Expression interfacePre(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context)
+{
+	auto& state = _context.state();
+	vector<smtutil::Expression> stateExprs{state.thisAddress(0), state.state(0)};
+	return _pred(stateExprs + initialStateVariables(_contract, _context));
+}
 
 smtutil::Expression interface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context)
 {
-	return _pred(currentStateVariables(_contract, _context));
+	auto& state = _context.state();
+	vector<smtutil::Expression> stateExprs{state.thisAddress(0), state.state()};
+	return _pred(stateExprs + currentStateVariables(_contract, _context));
+}
+
+smtutil::Expression nondetInterface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context, unsigned _preIdx, unsigned _postIdx)
+{
+	return _pred(
+		vector<smtutil::Expression>{_context.state().state(_preIdx)} +
+		stateVariablesAtIndex(_preIdx, _contract, _context) +
+		vector<smtutil::Expression>{_context.state().state(_postIdx)} +
+		stateVariablesAtIndex(_postIdx, _contract, _context)
+	);
+}
+
+smtutil::Expression implicitConstructor(Predicate const& _pred, ContractDefinition const&, EncodingContext& _context)
+{
+	auto& state = _context.state();
+	vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.state(0)};
+	return _pred(stateExprs);
 }
 
 smtutil::Expression constructor(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context)
@@ -38,16 +63,9 @@ smtutil::Expression constructor(Predicate const& _pred, ContractDefinition const
 	if (auto const* constructor = _contract.constructor())
 		return _pred(currentFunctionVariables(*constructor, &_contract, _context));
 
-	return _pred(
-		vector<smtutil::Expression>{_context.state().errorFlag().currentValue()} +
-		currentStateVariables(_contract, _context)
-	);
-}
-
-/// Currently it does not have arguments but it will have tx data in the future.
-smtutil::Expression implicitConstructor(Predicate const& _pred, ContractDefinition const&, EncodingContext&)
-{
-	return _pred({});
+	auto& state = _context.state();
+	vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.state()};
+	return _pred(stateExprs + currentStateVariables(_contract, _context));
 }
 
 smtutil::Expression function(
@@ -99,9 +117,11 @@ vector<smtutil::Expression> currentFunctionVariables(
 	EncodingContext& _context
 )
 {
-	vector<smtutil::Expression> exprs{_context.state().errorFlag().currentValue()};
+	auto& state = _context.state();
+	vector<smtutil::Expression> exprs{_context.state().errorFlag().currentValue(), state.thisAddress(0), state.state(0)};
 	exprs += _contract ? initialStateVariables(*_contract, _context) : vector<smtutil::Expression>{};
 	exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->valueAtIndex(0); });
+	exprs += vector<smtutil::Expression>{state.state()};
 	exprs += _contract ? currentStateVariables(*_contract, _context) : vector<smtutil::Expression>{};
 	exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); });
 	exprs += applyMap(_function.returnParameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); });

libsolidity/formal/PredicateInstance.h

@@ -30,8 +30,12 @@ class EncodingContext;
  * The predicates follow the specification in PredicateSort.h.
  * */
 
+smtutil::Expression interfacePre(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context);
+
 smtutil::Expression interface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context);
 
+smtutil::Expression nondetInterface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context, unsigned _preIdx, unsigned _postIdx);
+
 smtutil::Expression constructor(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context);
 
 smtutil::Expression implicitConstructor(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context);

libsolidity/formal/PredicateSort.cpp

@@ -28,49 +28,54 @@ using namespace solidity::smtutil;
 namespace solidity::frontend::smt
 {
 
-SortPointer interfaceSort(ContractDefinition const& _contract)
+SortPointer interfaceSort(ContractDefinition const& _contract, SymbolicState& _state)
 {
 	return make_shared<FunctionSort>(
-		stateSorts(_contract),
+		vector<SortPointer>{_state.thisAddressSort(), _state.stateSort()} + stateSorts(_contract),
 		SortProvider::boolSort
 	);
 }
 
-SortPointer nondetInterfaceSort(ContractDefinition const& _contract)
+SortPointer nondetInterfaceSort(ContractDefinition const& _contract, SymbolicState& _state)
 {
 	auto varSorts = stateSorts(_contract);
+	vector<SortPointer> stateSort{_state.stateSort()};
 	return make_shared<FunctionSort>(
-		varSorts + varSorts,
+		stateSort + varSorts + stateSort + varSorts,
 		SortProvider::boolSort
 	);
 }
 
-SortPointer implicitConstructorSort()
+SortPointer implicitConstructorSort(SymbolicState& _state)
 {
-	return arity0FunctionSort();
+	return make_shared<FunctionSort>(
+		vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.stateSort()},
+		SortProvider::boolSort
+	);
 }
 
-SortPointer constructorSort(ContractDefinition const& _contract)
+SortPointer constructorSort(ContractDefinition const& _contract, SymbolicState& _state)
 {
 	if (auto const* constructor = _contract.constructor())
-		return functionSort(*constructor, &_contract);
+		return functionSort(*constructor, &_contract, _state);
 
 	return make_shared<FunctionSort>(
-		vector<SortPointer>{SortProvider::uintSort} + stateSorts(_contract),
+		vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.stateSort()} + stateSorts(_contract),
 		SortProvider::boolSort
 	);
 }
 
-SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition const* _contract)
+SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition const* _contract, SymbolicState& _state)
 {
 	auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); };
 	auto varSorts = _contract ? stateSorts(*_contract) : vector<SortPointer>{};
 	auto inputSorts = applyMap(_function.parameters(), smtSort);
 	auto outputSorts = applyMap(_function.returnParameters(), smtSort);
 	return make_shared<FunctionSort>(
-		vector<SortPointer>{SortProvider::uintSort} +
+		vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.stateSort()} +
 			varSorts +
 			inputSorts +
+			vector<SortPointer>{_state.stateSort()} +
 			varSorts +
 			inputSorts +
 			outputSorts,
@@ -78,9 +83,9 @@ SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition
 	);
 }
 
-SortPointer functionBodySort(FunctionDefinition const& _function, ContractDefinition const* _contract)
+SortPointer functionBodySort(FunctionDefinition const& _function, ContractDefinition const* _contract, SymbolicState& _state)
 {
-	auto fSort = dynamic_pointer_cast<FunctionSort>(functionSort(_function, _contract));
+	auto fSort = dynamic_pointer_cast<FunctionSort>(functionSort(_function, _contract, _state));
 	solAssert(fSort, "");
 
 	auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); };

libsolidity/formal/PredicateSort.h

@@ -20,6 +20,8 @@
 
 #include <libsolidity/formal/Predicate.h>
 
+#include <libsolidity/formal/SymbolicState.h>
+
 #include <libsmtutil/Sorts.h>
 
 namespace solidity::frontend::smt
@@ -31,46 +33,46 @@ namespace solidity::frontend::smt
  *
  * 1. Interface
  * The idle state of a contract. Signature:
- * interface(stateVariables).
+ * interface(this, blockchainState, stateVariables).
  *
  * 2. Nondet interface
  * The nondeterminism behavior of a contract. Signature:
- * nondet_interface(stateVariables, stateVariables').
+ * nondet_interface(blockchainState, stateVariables, blockchainState', stateVariables').
  *
  * 3. Implicit constructor
  * The implicit constructor of a contract, that is, without input parameters. Signature:
- * implicit_constructor().
+ * implicit_constructor(error, this, blockchainState).
  *
  * 4. Constructor entry/summary
  * The summary of an implicit constructor. Signature:
- * constructor_summary(error, stateVariables').
+ * constructor_summary(error, this, blockchainState, blockchainState', stateVariables').
  *
  * 5. Function entry/summary
  * The entry point of a function definition. Signature:
- * function_entry(error, stateVariables, inputVariables, stateVariables', inputVariables', outputVariables').
+ * function_entry(error, this, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables').
  *
  * 6. Function body
  * Use for any predicate within a function. Signature:
- * function_body(error, stateVariables, inputVariables, stateVariables', inputVariables', outputVariables', localVariables).
+ * function_body(error, this, blockchainState, stateVariables, inputVariables, blockchainState' ,stateVariables', inputVariables', outputVariables', localVariables).
  */
 
 /// @returns the interface predicate sort for _contract.
-smtutil::SortPointer interfaceSort(ContractDefinition const& _contract);
+smtutil::SortPointer interfaceSort(ContractDefinition const& _contract, SymbolicState& _state);
 
 /// @returns the nondeterminisc interface predicate sort for _contract.
-smtutil::SortPointer nondetInterfaceSort(ContractDefinition const& _contract);
+smtutil::SortPointer nondetInterfaceSort(ContractDefinition const& _contract, SymbolicState& _state);
 
 /// @returns the implicit constructor predicate sort.
-smtutil::SortPointer implicitConstructorSort();
+smtutil::SortPointer implicitConstructorSort(SymbolicState& _state);
 
 /// @returns the constructor entry/summary predicate sort for _contract.
-smtutil::SortPointer constructorSort(ContractDefinition const& _contract);
+smtutil::SortPointer constructorSort(ContractDefinition const& _contract, SymbolicState& _state);
 
 /// @returns the function entry/summary predicate sort for _function contained in _contract.
-smtutil::SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition const* _contract);
+smtutil::SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition const* _contract, SymbolicState& _state);
 
 /// @returns the function body predicate sort for _function contained in _contract.
-smtutil::SortPointer functionBodySort(FunctionDefinition const& _function, ContractDefinition const* _contract);
+smtutil::SortPointer functionBodySort(FunctionDefinition const& _function, ContractDefinition const* _contract, SymbolicState& _state);
 
 /// @returns the sort of a predicate without parameters.
 smtutil::SortPointer arity0FunctionSort();

libsolidity/formal/SMTEncoder.cpp

@@ -2162,6 +2162,7 @@ void SMTEncoder::clearIndices(ContractDefinition const* _contract, FunctionDefin
 		for (auto const& var: _function->localVariables())
 			m_context.variable(*var)->resetIndex();
 	}
+	m_context.state().reset();
 }
 
 Expression const* SMTEncoder::leftmostBase(IndexAccess const& _indexAccess)

libsolidity/formal/SymbolicState.cpp

@@ -18,61 +18,118 @@
 
 #include <libsolidity/formal/SymbolicState.h>
 
+#include <libsolidity/formal/SymbolicTypes.h>
 #include <libsolidity/formal/EncodingContext.h>
 
 using namespace std;
 using namespace solidity;
+using namespace solidity::smtutil;
 using namespace solidity::frontend::smt;
 
 SymbolicState::SymbolicState(EncodingContext& _context):
 	m_context(_context)
 {
+	m_stateMembers.emplace("balances", make_shared<smtutil::ArraySort>(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort));
+
+	vector<string> members;
+	vector<SortPointer> sorts;
+	for (auto const& [component, sort]: m_stateMembers)
+	{
+		members.emplace_back(component);
+		sorts.emplace_back(sort);
+		m_componentIndices[component] = members.size() - 1;
+	}
+	m_stateTuple = make_unique<SymbolicTupleVariable>(
+		make_shared<smtutil::TupleSort>("state_type", members, sorts),
+		"state",
+		m_context
+	);
 }
 
 void SymbolicState::reset()
 {
-	m_thisAddress.resetIndex();
-	m_balances.resetIndex();
 	m_error.resetIndex();
+	m_thisAddress.resetIndex();
+	m_stateTuple->resetIndex();
 }
 
 // Blockchain
 
-smtutil::Expression SymbolicState::thisAddress()
-{
-	return m_thisAddress.currentValue();
-}
-
-smtutil::Expression SymbolicState::balance()
-{
-	return balance(m_thisAddress.currentValue());
-}
-
-smtutil::Expression SymbolicState::balance(smtutil::Expression _address)
-{
-	return smtutil::Expression::select(m_balances.elements(), move(_address));
-}
-
 SymbolicIntVariable& SymbolicState::errorFlag()
 {
 	return m_error;
 }
 
+SortPointer SymbolicState::errorFlagSort()
+{
+	return m_error.sort();
+}
+
+smtutil::Expression SymbolicState::thisAddress()
+{
+	return m_thisAddress.currentValue();
+}
+
+smtutil::Expression SymbolicState::thisAddress(unsigned _idx)
+{
+	return m_thisAddress.valueAtIndex(_idx);
+}
+
+SortPointer SymbolicState::thisAddressSort()
+{
+	return m_thisAddress.sort();
+}
+
+smtutil::Expression SymbolicState::state()
+{
+	return m_stateTuple->currentValue();
+}
+
+smtutil::Expression SymbolicState::state(unsigned _idx)
+{
+	return m_stateTuple->valueAtIndex(_idx);
+}
+
+SortPointer SymbolicState::stateSort()
+{
+	return m_stateTuple->sort();
+}
+
+void SymbolicState::newState()
+{
+	m_stateTuple->increaseIndex();
+}
+
+smtutil::Expression SymbolicState::balances()
+{
+	return m_stateTuple->component(m_componentIndices.at("balances"));
+}
+
+smtutil::Expression SymbolicState::balance()
+{
+	return balance(thisAddress());
+}
+
+smtutil::Expression SymbolicState::balance(smtutil::Expression _address)
+{
+	return smtutil::Expression::select(balances(), move(_address));
+}
+
 void SymbolicState::transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value)
 {
-	unsigned indexBefore = m_balances.index();
+	unsigned indexBefore = m_stateTuple->index();
 	addBalance(_from, 0 - _value);
 	addBalance(_to, move(_value));
-	unsigned indexAfter = m_balances.index();
+	unsigned indexAfter = m_stateTuple->index();
 	solAssert(indexAfter > indexBefore, "");
-	m_balances.increaseIndex();
+	m_stateTuple->increaseIndex();
 	/// Do not apply the transfer operation if _from == _to.
-	auto newBalances = smtutil::Expression::ite(
+	auto newState = smtutil::Expression::ite(
 		move(_from) == move(_to),
-		m_balances.valueAtIndex(indexBefore),
-		m_balances.valueAtIndex(indexAfter)
+		m_stateTuple->valueAtIndex(indexBefore),
+		m_stateTuple->valueAtIndex(indexAfter)
 	);
-	m_context.addAssertion(m_balances.currentValue() == newBalances);
+	m_context.addAssertion(m_stateTuple->currentValue() == newState);
 }
 
 /// Private helpers.
@@ -80,13 +137,24 @@ void SymbolicState::transfer(smtutil::Expression _from, smtutil::Expression _to,
 void SymbolicState::addBalance(smtutil::Expression _address, smtutil::Expression _value)
 {
 	auto newBalances = smtutil::Expression::store(
-		m_balances.elements(),
+		balances(),
 		_address,
 		balance(_address) + move(_value)
 	);
-	auto oldLength = m_balances.length();
-	m_balances.increaseIndex();
-	m_context.addAssertion(m_balances.elements() == newBalances);
-	m_context.addAssertion(m_balances.length() == oldLength);
+	assignStateMember("balances", newBalances);
 }
 
+smtutil::Expression SymbolicState::assignStateMember(string const& _member, smtutil::Expression const& _value)
+{
+	vector<smtutil::Expression> args;
+	for (auto const& member: m_stateMembers)
+		if (member.first == _member)
+			args.emplace_back(_value);
+		else
+			args.emplace_back(m_stateTuple->component(m_componentIndices.at(member.first)));
+	m_stateTuple->increaseIndex();
+	auto tuple = m_stateTuple->currentValue();
+	auto sortExpr = smtutil::Expression(make_shared<smtutil::SortSort>(tuple.sort), tuple.name);
+	m_context.addAssertion(tuple == smtutil::Expression::tuple_constructor(sortExpr, args));
+	return m_stateTuple->currentValue();
+}

libsolidity/formal/SymbolicState.h

@@ -27,9 +27,17 @@ namespace solidity::frontend::smt
 {
 
 class EncodingContext;
+class SymbolicAddressVariable;
+class SymbolicArrayVariable;
 
 /**
- * Symbolic representation of the blockchain state.
+ * Symbolic representation of the blockchain context:
+ * - error flag
+ * - this (the address of the currently executing contract)
+ * - state, represented as a tuple of:
+ *   - balances
+ *   - TODO: potentially storage of contracts
+ * - TODO transaction variables
  */
 class SymbolicState
 {
@@ -40,15 +48,27 @@ public:
 
 	/// Blockchain.
 	//@{
-	/// Value of `this` address.
+	SymbolicIntVariable& errorFlag();
+	smtutil::SortPointer errorFlagSort();
+
+	/// @returns the symbolic value of the currently executing contract's address.
 	smtutil::Expression thisAddress();
+	smtutil::Expression thisAddress(unsigned _idx);
+	smtutil::SortPointer thisAddressSort();
+
+	/// @returns the state as a tuple.
+	smtutil::Expression state();
+	smtutil::Expression state(unsigned _idx);
+	smtutil::SortPointer stateSort();
+	void newState();
+
+	/// @returns the symbolic balances.
+	smtutil::Expression balances();
 	/// @returns the symbolic balance of address `this`.
 	smtutil::Expression balance();
 	/// @returns the symbolic balance of an address.
 	smtutil::Expression balance(smtutil::Expression _address);
 
-	SymbolicIntVariable& errorFlag();
-
 	/// Transfer _value from _from to _to.
 	void transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value);
 	//@}
@@ -57,27 +77,27 @@ private:
 	/// Adds _value to _account's balance.
 	void addBalance(smtutil::Expression _account, smtutil::Expression _value);
 
+	/// Generates a new tuple where _member is assigned _value.
+	smtutil::Expression assignStateMember(std::string const& _member, smtutil::Expression const& _value);
+
 	EncodingContext& m_context;
 
-	/// Symbolic `this` address.
-	SymbolicAddressVariable m_thisAddress{
-		"this",
-		m_context
-	};
-
-	/// Symbolic balances.
-	SymbolicArrayVariable m_balances{
-		std::make_shared<smtutil::ArraySort>(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort),
-		"balances",
-		m_context
-	};
-
-	smt::SymbolicIntVariable m_error{
+	SymbolicIntVariable m_error{
 		TypeProvider::uint256(),
 		TypeProvider::uint256(),
 		"error",
 		m_context
 	};
+
+	SymbolicAddressVariable m_thisAddress{
+		"this",
+		m_context
+	};
+
+	std::map<std::string, unsigned> m_componentIndices;
+	/// balances, TODO storage of other contracts
+	std::map<std::string, smtutil::SortPointer> m_stateMembers;
+	std::unique_ptr<SymbolicTupleVariable> m_stateTuple;
 };
 
 }

libsolidity/interface/CompilerStack.cpp

@@ -343,6 +343,8 @@ bool CompilerStack::analyze()
 			if (source->ast && !resolver.performImports(*source->ast, sourceUnitsByName))
 				return false;
 
+		resolver.warnHomonymDeclarations();
+
 		for (Source const* source: m_sourceOrder)
 			if (source->ast && !resolver.resolveNamesAndTypes(*source->ast))
 				return false;