Merge remote-tracking branch 'origin/develop' into breaking

libsolidity/analysis/TypeChecker.cpp

@@ -82,7 +82,7 @@ TypePointer const& TypeChecker::type(VariableDeclaration const& _variable) const
 
 bool TypeChecker::visit(ContractDefinition const& _contract)
 {
-	m_scope = &_contract;
+	m_currentContract = &_contract;
 
 	ASTNode::listAccept(_contract.baseContracts(), *this);
 
@@ -266,7 +266,7 @@ void TypeChecker::endVisit(InheritanceSpecifier const& _inheritance)
 	auto base = dynamic_cast<ContractDefinition const*>(&dereference(_inheritance.name()));
 	solAssert(base, "Base contract not available.");
 
-	if (m_scope->isInterface() && !base->isInterface())
+	if (m_currentContract->isInterface() && !base->isInterface())
 		m_errorReporter.typeError(6536_error, _inheritance.location(), "Interfaces can only inherit from other interfaces.");
 
 	if (base->isLibrary())
@@ -328,8 +328,6 @@ void TypeChecker::endVisit(ModifierDefinition const& _modifier)
 
 bool TypeChecker::visit(FunctionDefinition const& _function)
 {
-	bool isLibraryFunction = _function.inContractKind() == ContractKind::Library;
-
 	if (_function.markedVirtual())
 	{
 		if (_function.annotation().contract->isInterface())
@@ -342,7 +340,7 @@ bool TypeChecker::visit(FunctionDefinition const& _function)
 
 	if (_function.isPayable())
 	{
-		if (isLibraryFunction)
+		if (_function.libraryFunction())
 			m_errorReporter.typeError(7708_error, _function.location(), "Library functions cannot be payable.");
 		if (_function.isOrdinary() && !_function.isPartOfExternalInterface())
 			m_errorReporter.typeError(5587_error, _function.location(), "Internal functions cannot be payable.");
@@ -352,15 +350,13 @@ bool TypeChecker::visit(FunctionDefinition const& _function)
 		{
 			if (var.referenceLocation() != VariableDeclaration::Location::Storage)
 			{
-				if (!isLibraryFunction && _function.isPublic())
+				if (!_function.libraryFunction() && _function.isPublic())
 					m_errorReporter.typeError(3442_error, var.location(), "Mapping types can only have a data location of \"storage\" and thus only be parameters or return variables for internal or library functions.");
 				else
 					m_errorReporter.typeError(5380_error, var.location(), "Mapping types can only have a data location of \"storage\"." );
 			}
 			else
-			{
-				solAssert(isLibraryFunction || !_function.isPublic(), "Mapping types for parameters or return variables can only be used in internal or library functions.");
-			}
+				solAssert(_function.libraryFunction() || !_function.isPublic(), "Mapping types for parameters or return variables can only be used in internal or library functions.");
 		}
 		else
 		{
@@ -368,7 +364,7 @@ bool TypeChecker::visit(FunctionDefinition const& _function)
 				m_errorReporter.typeError(3312_error, var.location(), "Type is required to live outside storage.");
 			if (_function.isPublic())
 			{
-				auto iType = type(var)->interfaceType(isLibraryFunction);
+				auto iType = type(var)->interfaceType(_function.libraryFunction());
 
 				if (!iType)
 				{
@@ -380,7 +376,7 @@ bool TypeChecker::visit(FunctionDefinition const& _function)
 		if (
 			_function.isPublic() &&
 			!_function.sourceUnit().annotation().experimentalFeatures.count(ExperimentalFeature::ABIEncoderV2) &&
-			!typeSupportedByOldABIEncoder(*type(var), isLibraryFunction)
+			!typeSupportedByOldABIEncoder(*type(var), _function.libraryFunction())
 		)
 			m_errorReporter.typeError(
 				4957_error,
@@ -419,7 +415,7 @@ bool TypeChecker::visit(FunctionDefinition const& _function)
 		else
 			modifiers.insert(decl);
 	}
-	if (m_scope->isInterface())
+	if (m_currentContract->isInterface())
 	{
 		if (_function.isImplemented())
 			m_errorReporter.typeError(4726_error, _function.location(), "Functions in interfaces cannot have an implementation.");
@@ -430,14 +426,14 @@ bool TypeChecker::visit(FunctionDefinition const& _function)
 		if (_function.isConstructor())
 			m_errorReporter.typeError(6482_error, _function.location(), "Constructor cannot be defined in interfaces.");
 	}
-	else if (m_scope->contractKind() == ContractKind::Library)
+	else if (m_currentContract->contractKind() == ContractKind::Library)
 		if (_function.isConstructor())
 			m_errorReporter.typeError(7634_error, _function.location(), "Constructor cannot be defined in libraries.");
 	if (_function.isImplemented())
 		_function.body().accept(*this);
 	else if (_function.isConstructor())
 		m_errorReporter.typeError(5700_error, _function.location(), "Constructor must be implemented if declared.");
-	else if (isLibraryFunction)
+	else if (_function.libraryFunction())
 		m_errorReporter.typeError(9231_error, _function.location(), "Library functions must be implemented if declared.");
 	else if (!_function.virtualSemantics())
 		m_errorReporter.typeError(5424_error, _function.location(), "Functions without implementation must be marked virtual.");
@@ -1796,7 +1792,7 @@ void TypeChecker::typeCheckFunctionCall(
 	if (_functionType->kind() == FunctionType::Kind::Declaration)
 	{
 		if (
-			m_scope->derivesFrom(*_functionType->declaration().annotation().contract) &&
+			m_currentContract->derivesFrom(*_functionType->declaration().annotation().contract) &&
 			!dynamic_cast<FunctionDefinition const&>(_functionType->declaration()).isImplemented()
 		)
 			m_errorReporter.typeError(
@@ -1832,7 +1828,7 @@ void TypeChecker::typeCheckFallbackFunction(FunctionDefinition const& _function)
 {
 	solAssert(_function.isFallback(), "");
 
-	if (_function.inContractKind() == ContractKind::Library)
+	if (_function.libraryFunction())
 		m_errorReporter.typeError(5982_error, _function.location(), "Libraries cannot have fallback functions.");
 	if (_function.stateMutability() != StateMutability::NonPayable && _function.stateMutability() != StateMutability::Payable)
 		m_errorReporter.typeError(
@@ -1859,7 +1855,7 @@ void TypeChecker::typeCheckReceiveFunction(FunctionDefinition const& _function)
 {
 	solAssert(_function.isReceive(), "");
 
-	if (_function.inContractKind() == ContractKind::Library)
+	if (_function.libraryFunction())
 		m_errorReporter.typeError(4549_error, _function.location(), "Libraries cannot have receive ether functions.");
 
 	if (_function.stateMutability() != StateMutability::Payable)
@@ -1918,7 +1914,7 @@ void TypeChecker::typeCheckABIEncodeFunctions(
 	bool const isPacked = _functionType->kind() == FunctionType::Kind::ABIEncodePacked;
 	solAssert(_functionType->padArguments() != isPacked, "ABI function with unexpected padding");
 
-	bool const abiEncoderV2 = m_scope->sourceUnit().annotation().experimentalFeatures.count(
+	bool const abiEncoderV2 = m_currentContract->sourceUnit().annotation().experimentalFeatures.count(
 		ExperimentalFeature::ABIEncoderV2
 	);
 
@@ -2318,7 +2314,7 @@ bool TypeChecker::visit(FunctionCall const& _functionCall)
 		case FunctionType::Kind::ABIDecode:
 		{
 			bool const abiEncoderV2 =
-				m_scope->sourceUnit().annotation().experimentalFeatures.count(
+				m_currentContract->sourceUnit().annotation().experimentalFeatures.count(
 					ExperimentalFeature::ABIEncoderV2
 				);
 			returnTypes = typeCheckABIDecodeAndRetrieveReturnType(_functionCall, abiEncoderV2);
@@ -2514,13 +2510,13 @@ void TypeChecker::endVisit(NewExpression const& _newExpression)
 		if (contract->abstract())
 			m_errorReporter.typeError(4614_error, _newExpression.location(), "Cannot instantiate an abstract contract.");
 
-		solAssert(!!m_scope, "");
-		m_scope->annotation().contractDependencies.insert(contract);
+		solAssert(!!m_currentContract, "");
+		m_currentContract->annotation().contractDependencies.insert(contract);
 		solAssert(
 			!contract->annotation().linearizedBaseContracts.empty(),
 			"Linearized base contracts not yet available."
 		);
-		if (contractDependenciesAreCyclic(*m_scope))
+		if (contractDependenciesAreCyclic(*m_currentContract))
 			m_errorReporter.typeError(
 				4579_error,
 				_newExpression.location(),
@@ -2567,7 +2563,7 @@ bool TypeChecker::visit(MemberAccess const& _memberAccess)
 
 	// Retrieve the types of the arguments if this is used to call a function.
 	auto const& arguments = _memberAccess.annotation().arguments;
-	MemberList::MemberMap possibleMembers = exprType->members(m_scope).membersByName(memberName);
+	MemberList::MemberMap possibleMembers = exprType->members(m_currentContract).membersByName(memberName);
 	size_t const initialMemberCount = possibleMembers.size();
 	if (initialMemberCount > 1 && arguments)
 	{
@@ -2593,7 +2589,7 @@ bool TypeChecker::visit(MemberAccess const& _memberAccess)
 				DataLocation::Storage,
 				exprType
 			);
-			if (!storageType->members(m_scope).membersByName(memberName).empty())
+			if (!storageType->members(m_currentContract).membersByName(memberName).empty())
 				m_errorReporter.fatalTypeError(
 					4994_error,
 					_memberAccess.location(),
@@ -2749,7 +2745,7 @@ bool TypeChecker::visit(MemberAccess const& _memberAccess)
 		{
 			annotation.isPure = true;
 			ContractType const& accessedContractType = dynamic_cast<ContractType const&>(*magicType->typeArgument());
-			m_scope->annotation().contractDependencies.insert(&accessedContractType.contractDefinition());
+			m_currentContract->annotation().contractDependencies.insert(&accessedContractType.contractDefinition());
 
 			if (
 				memberName == "runtimeCode" &&
@@ -2761,7 +2757,7 @@ bool TypeChecker::visit(MemberAccess const& _memberAccess)
 					"\"runtimeCode\" is not available for contracts containing immutable variables."
 				);
 
-			if (contractDependenciesAreCyclic(*m_scope))
+			if (contractDependenciesAreCyclic(*m_currentContract))
 				m_errorReporter.typeError(
 					4224_error,
 					_memberAccess.location(),

libsolidity/analysis/TypeChecker.h

@@ -165,7 +165,7 @@ private:
 	/// Runs type checks on @a _expression to infer its type and then checks that it is an LValue.
 	void requireLValue(Expression const& _expression, bool _ordinaryAssignment);
 
-	ContractDefinition const* m_scope = nullptr;
+	ContractDefinition const* m_currentContract = nullptr;
 
 	langutil::EVMVersion m_evmVersion;
 

libsolidity/analysis/ViewPureChecker.cpp

@@ -276,7 +276,7 @@ void ViewPureChecker::reportMutability(
 	{
 		// We do not warn for library functions because they cannot be payable anyway.
 		// Also internal functions should be allowed to use `msg.value`.
-		if (m_currentFunction->isPublic() && m_currentFunction->inContractKind() != ContractKind::Library)
+		if (m_currentFunction->isPublic() && !m_currentFunction->libraryFunction())
 		{
 			if (_nestedLocation)
 				m_errorReporter.typeError(

libsolidity/ast/AST.cpp

@@ -287,11 +287,11 @@ TypeDeclarationAnnotation& EnumDefinition::annotation() const
 	return initAnnotation<TypeDeclarationAnnotation>();
 }
 
-ContractKind FunctionDefinition::inContractKind() const
+bool FunctionDefinition::libraryFunction() const
 {
-	auto contractDef = dynamic_cast<ContractDefinition const*>(scope());
-	solAssert(contractDef, "Enclosing Scope of FunctionDefinition was not set.");
-	return contractDef->contractKind();
+	if (auto const* contractDef = dynamic_cast<ContractDefinition const*>(scope()))
+		return contractDef->isLibrary();
+	return false;
 }
 
 FunctionTypePointer FunctionDefinition::functionType(bool _internal) const

libsolidity/ast/AST.h

@@ -799,6 +799,7 @@ public:
 	void accept(ASTConstVisitor& _visitor) const override;
 
 	StateMutability stateMutability() const { return m_stateMutability; }
+	bool libraryFunction() const;
 	bool isOrdinary() const { return m_kind == Token::Function; }
 	bool isConstructor() const { return m_kind == Token::Constructor; }
 	bool isFallback() const { return m_kind == Token::Fallback; }
@@ -825,8 +826,6 @@ public:
 	/// @returns the external identifier of this function (the hash of the signature) as a hex string.
 	std::string externalIdentifierHex() const;
 
-	ContractKind inContractKind() const;
-
 	TypePointer type() const override;
 	TypePointer typeViaContractName() const override;
 

libsolidity/codegen/ir/IRGeneratorForStatements.cpp

@@ -1730,7 +1730,7 @@ void IRGeneratorForStatements::endVisit(IndexAccess const& _indexAccess)
 
 				setLValue(_indexAccess, IRLValue{
 					*arrayType.baseType(),
-					IRLValue::Memory{memAddress}
+					IRLValue::Memory{memAddress, arrayType.isByteArray()}
 				});
 				break;
 			}
@@ -1763,7 +1763,23 @@ void IRGeneratorForStatements::endVisit(IndexAccess const& _indexAccess)
 		}
 	}
 	else if (baseType.category() == Type::Category::FixedBytes)
-		solUnimplementedAssert(false, "");
+	{
+		auto const& fixedBytesType = dynamic_cast<FixedBytesType const&>(baseType);
+		solAssert(_indexAccess.indexExpression(), "Index expression expected.");
+
+		IRVariable index{m_context.newYulVariable(), *TypeProvider::uint256()};
+		define(index, *_indexAccess.indexExpression());
+		m_code << Whiskers(R"(
+			if iszero(lt(<index>, <length>)) { invalid() }
+			let <result> := <shl248>(byte(<index>, <array>))
+		)")
+		("index", index.name())
+		("length", to_string(fixedBytesType.numBytes()))
+		("array", IRVariable(_indexAccess.baseExpression()).name())
+		("shl248", m_utils.shiftLeftFunction(256 - 8))
+		("result", IRVariable(_indexAccess).name())
+		.render();
+	}
 	else if (baseType.category() == Type::Category::TypeType)
 	{
 		solAssert(baseType.sizeOnStack() == 0, "");

libsolidity/formal/BMC.cpp

@@ -604,7 +604,11 @@ void BMC::checkUnderflow(BMCVerificationTarget& _target, smtutil::Expression con
 			_target.type == VerificationTarget::Type::UnderOverflow,
 		""
 	);
-	auto intType = dynamic_cast<IntegerType const*>(_target.expression->annotation().type);
+	IntegerType const* intType = nullptr;
+	if (auto const* type = dynamic_cast<IntegerType const*>(_target.expression->annotation().type))
+		intType = type;
+	else
+		intType = TypeProvider::uint256();
 	solAssert(intType, "");
 	checkCondition(
 		_target.constraints && _constraints && _target.value < smt::minValue(*intType),
@@ -626,7 +630,12 @@ void BMC::checkOverflow(BMCVerificationTarget& _target, smtutil::Expression cons
 			_target.type == VerificationTarget::Type::UnderOverflow,
 		""
 	);
-	auto intType = dynamic_cast<IntegerType const*>(_target.expression->annotation().type);
+	IntegerType const* intType = nullptr;
+	if (auto const* type = dynamic_cast<IntegerType const*>(_target.expression->annotation().type))
+		intType = type;
+	else
+		intType = TypeProvider::uint256();
+
 	solAssert(intType, "");
 	checkCondition(
 		_target.constraints && _constraints && _target.value > smt::maxValue(*intType),

libsolidity/formal/SMTEncoder.cpp

@@ -385,44 +385,22 @@ void SMTEncoder::endVisit(Assignment const& _assignment)
 	}
 	else
 	{
-		auto const& type = _assignment.annotation().type;
-		vector<smtutil::Expression> rightArguments;
-		if (auto const* tupleTypeRight = dynamic_cast<TupleType const*>(_assignment.rightHandSide().annotation().type))
-		{
-			auto symbTupleLeft = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_assignment.leftHandSide()));
-			solAssert(symbTupleLeft, "");
-			auto symbTupleRight = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_assignment.rightHandSide()));
-			solAssert(symbTupleRight, "");
-
-			auto const& leftComponents = symbTupleLeft->components();
-			auto const& rightComponents = symbTupleRight->components();
-			solAssert(leftComponents.size() == rightComponents.size(), "");
-
-			auto tupleTypeLeft = dynamic_cast<TupleType const*>(_assignment.leftHandSide().annotation().type);
-			solAssert(tupleTypeLeft, "");
-			solAssert(tupleTypeLeft->components().size() == leftComponents.size(), "");
-			auto const& typesLeft = tupleTypeLeft->components();
-
-			solAssert(tupleTypeRight->components().size() == rightComponents.size(), "");
-			auto const& typesRight = tupleTypeRight->components();
-
-			for (unsigned i = 0; i < rightComponents.size(); ++i)
-				rightArguments.push_back(symbTupleRight->component(i, typesRight.at(i), typesLeft.at(i)));
-		}
+		if (dynamic_cast<TupleType const*>(_assignment.rightHandSide().annotation().type))
+			tupleAssignment(_assignment.leftHandSide(), _assignment.rightHandSide());
 		else
 		{
+			auto const& type = _assignment.annotation().type;
 			auto rightHandSide = compoundOps.count(op) ?
 				compoundAssignment(_assignment) :
 				expr(_assignment.rightHandSide(), type);
 			defineExpr(_assignment, rightHandSide);
-			rightArguments.push_back(expr(_assignment, type));
+			assignment(
+				_assignment.leftHandSide(),
+				expr(_assignment, type),
+				type,
+				_assignment.location()
+			);
 		}
-		assignment(
-			_assignment.leftHandSide(),
-			rightArguments,
-			type,
-			_assignment.location()
-		);
 	}
 }
 
@@ -1023,38 +1001,7 @@ void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smtutil::Expressi
 			solAssert(varDecl, "");
 
 			if (varDecl->hasReferenceOrMappingType())
-				m_context.resetVariables([&](VariableDeclaration const& _var) {
-					if (_var == *varDecl)
-						return false;
-
-					// If both are state variables no need to clear knowledge.
-					if (_var.isStateVariable() && varDecl->isStateVariable())
-						return false;
-
-					TypePointer prefix = _var.type();
-					TypePointer originalType = typeWithoutPointer(varDecl->type());
-					while (
-						prefix->category() == Type::Category::Mapping ||
-						prefix->category() == Type::Category::Array
-					)
-					{
-						if (*originalType == *typeWithoutPointer(prefix))
-							return true;
-						if (prefix->category() == Type::Category::Mapping)
-						{
-							auto mapPrefix = dynamic_cast<MappingType const*>(prefix);
-							solAssert(mapPrefix, "");
-							prefix = mapPrefix->valueType();
-						}
-						else
-						{
-							auto arrayPrefix = dynamic_cast<ArrayType const*>(prefix);
-							solAssert(arrayPrefix, "");
-							prefix = arrayPrefix->baseType();
-						}
-					}
-					return false;
-				});
+				resetReferences(*varDecl);
 
 			auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.variable(*varDecl));
 			smtutil::Expression store = smtutil::Expression::store(
@@ -1160,6 +1107,8 @@ void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smtutil::Expression
 	{
 		auto varDecl = identifierToVariable(*id);
 		solAssert(varDecl, "");
+		if (varDecl->hasReferenceOrMappingType())
+			resetReferences(*varDecl);
 		m_context.addAssertion(m_context.newValue(*varDecl) == _array);
 	}
 	else if (auto const* indexAccess = dynamic_cast<IndexAccess const*>(&_expr))
@@ -1213,7 +1162,7 @@ void SMTEncoder::arithmeticOperation(BinaryOperation const& _op)
 {
 	auto type = _op.annotation().commonType;
 	solAssert(type, "");
-	if (type->category() == Type::Category::Integer)
+	if (type->category() == Type::Category::Integer || type->category() == Type::Category::FixedPoint)
 	{
 		switch (_op.getOperator())
 		{
@@ -1266,13 +1215,21 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::arithmeticOperation(
 	};
 	solAssert(validOperators.count(_op), "");
 	solAssert(_commonType, "");
-	solAssert(_commonType->category() == Type::Category::Integer, "");
+	solAssert(
+		_commonType->category() == Type::Category::Integer || _commonType->category() == Type::Category::FixedPoint,
+		""
+	);
+
+	IntegerType const* intType = nullptr;
+	if (auto type = dynamic_cast<IntegerType const*>(_commonType))
+		intType = type;
+	else
+		intType = TypeProvider::uint256();
 
-	auto const& intType = dynamic_cast<IntegerType const&>(*_commonType);
 	smtutil::Expression valueNoMod(
 		_op == Token::Add ? _left + _right :
 		_op == Token::Sub ? _left - _right :
-		_op == Token::Div ? division(_left, _right, intType) :
+		_op == Token::Div ? division(_left, _right, *intType) :
 		_op == Token::Mul ? _left * _right :
 		/*_op == Token::Mod*/ _left % _right
 	);
@@ -1280,20 +1237,23 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::arithmeticOperation(
 	if (_op == Token::Div || _op == Token::Mod)
 		m_context.addAssertion(_right != 0);
 
-	smtutil::Expression intValueRange = (0 - smt::minValue(intType)) + smt::maxValue(intType) + 1;
+	auto symbMin = smt::minValue(*intType);
+	auto symbMax = smt::maxValue(*intType);
+
+	smtutil::Expression intValueRange = (0 - symbMin) + symbMax + 1;
 	auto value = smtutil::Expression::ite(
-		valueNoMod > smt::maxValue(intType),
+		valueNoMod > symbMax,
 		valueNoMod % intValueRange,
 		smtutil::Expression::ite(
-			valueNoMod < smt::minValue(intType),
+			valueNoMod < symbMin,
 			valueNoMod % intValueRange,
 			valueNoMod
 		)
 	);
 
-	if (intType.isSigned())
+	if (intType->isSigned())
 		value = smtutil::Expression::ite(
-			value > smt::maxValue(intType),
+			value > symbMax,
 			value - intValueRange,
 			value
 		);
@@ -1422,11 +1382,16 @@ smtutil::Expression SMTEncoder::division(smtutil::Expression _left, smtutil::Exp
 
 void SMTEncoder::assignment(
 	Expression const& _left,
-	vector<smtutil::Expression> const& _right,
+	smtutil::Expression const& _right,
 	TypePointer const& _type,
 	langutil::SourceLocation const& _location
 )
 {
+	solAssert(
+		_left.annotation().type->category() != Type::Category::Tuple,
+		"Tuple assignments should be handled by tupleAssignment."
+	);
+
 	if (!smt::isSupportedType(_type->category()))
 	{
 		// Give it a new index anyway to keep the SSA scheme sound.
@@ -1440,26 +1405,9 @@ void SMTEncoder::assignment(
 		);
 	}
 	else if (auto varDecl = identifierToVariable(_left))
-	{
-		solAssert(_right.size() == 1, "");
-		assignment(*varDecl, _right.front());
-	}
+		assignment(*varDecl, _right);
 	else if (dynamic_cast<IndexAccess const*>(&_left))
-	{
-		solAssert(_right.size() == 1, "");
-		arrayIndexAssignment(_left, _right.front());
-	}
-	else if (auto tuple = dynamic_cast<TupleExpression const*>(&_left))
-	{
-		auto const& components = tuple->components();
-		if (!_right.empty())
-		{
-			solAssert(_right.size() == components.size(), "");
-			for (unsigned i = 0; i < _right.size(); ++i)
-				if (auto component = components.at(i))
-					assignment(*component, {_right.at(i)}, component->annotation().type, component->location());
-		}
-	}
+		arrayIndexAssignment(_left, _right);
 	else
 		m_errorReporter.warning(
 			8182_error,
@@ -1468,6 +1416,52 @@ void SMTEncoder::assignment(
 		);
 }
 
+void SMTEncoder::tupleAssignment(Expression const& _left, Expression const& _right)
+{
+	auto lTuple = dynamic_cast<TupleExpression const*>(&_left);
+	solAssert(lTuple, "");
+
+	auto const& lComponents = lTuple->components();
+
+	// If both sides are tuple expressions, we individually and potentially
+	// recursively assign each pair of components.
+	// This is because of potential type conversion.
+	if (auto rTuple = dynamic_cast<TupleExpression const*>(&_right))
+	{
+		auto const& rComponents = rTuple->components();
+		solAssert(lComponents.size() == rComponents.size(), "");
+		for (unsigned i = 0; i < lComponents.size(); ++i)
+		{
+			if (!lComponents.at(i) || !rComponents.at(i))
+				continue;
+			auto const& lExpr = *lComponents.at(i);
+			auto const& rExpr = *rComponents.at(i);
+			if (lExpr.annotation().type->category() == Type::Category::Tuple)
+				tupleAssignment(lExpr, rExpr);
+			else
+			{
+				auto type = lExpr.annotation().type;
+				assignment(lExpr, expr(rExpr, type), type, lExpr.location());
+			}
+		}
+	}
+	else
+	{
+		auto rType = dynamic_cast<TupleType const*>(_right.annotation().type);
+		solAssert(rType, "");
+
+		auto const& rComponents = rType->components();
+		solAssert(lComponents.size() == rComponents.size(), "");
+
+		auto symbRight = expr(_right);
+		solAssert(symbRight.sort->kind == smtutil::Kind::Tuple, "");
+
+		for (unsigned i = 0; i < lComponents.size(); ++i)
+			if (auto component = lComponents.at(i); component && rComponents.at(i))
+				assignment(*component, smtutil::Expression::tuple_get(symbRight, i), component->annotation().type, component->location());
+	}
+}
+
 smtutil::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment)
 {
 	static map<Token, Token> const compoundToArithmetic{
@@ -1618,6 +1612,42 @@ void SMTEncoder::resetStateVariables()
 	m_context.resetVariables([&](VariableDeclaration const& _variable) { return _variable.isStateVariable(); });
 }
 
+void SMTEncoder::resetReferences(VariableDeclaration const& _varDecl)
+{
+	m_context.resetVariables([&](VariableDeclaration const& _var) {
+		if (_var == _varDecl)
+			return false;
+
+		// If both are state variables no need to clear knowledge.
+		if (_var.isStateVariable() && _varDecl.isStateVariable())
+			return false;
+
+		TypePointer prefix = _var.type();
+		TypePointer originalType = typeWithoutPointer(_varDecl.type());
+		while (
+			prefix->category() == Type::Category::Mapping ||
+			prefix->category() == Type::Category::Array
+		)
+		{
+			if (*originalType == *typeWithoutPointer(prefix))
+				return true;
+			if (prefix->category() == Type::Category::Mapping)
+			{
+				auto mapPrefix = dynamic_cast<MappingType const*>(prefix);
+				solAssert(mapPrefix, "");
+				prefix = mapPrefix->valueType();
+			}
+			else
+			{
+				auto arrayPrefix = dynamic_cast<ArrayType const*>(prefix);
+				solAssert(arrayPrefix, "");
+				prefix = arrayPrefix->baseType();
+			}
+		}
+		return false;
+	});
+}
+
 TypePointer SMTEncoder::typeWithoutPointer(TypePointer const& _type)
 {
 	if (auto refType = dynamic_cast<ReferenceType const*>(_type))

libsolidity/formal/SMTEncoder.h

@@ -157,10 +157,12 @@ protected:
 	/// Will also be used for assignments of tuple components.
 	void assignment(
 		Expression const& _left,
-		std::vector<smtutil::Expression> const& _right,
+		smtutil::Expression const& _right,
 		TypePointer const& _type,
 		langutil::SourceLocation const& _location
 	);
+	/// Handle assignments between tuples.
+	void tupleAssignment(Expression const& _left, Expression const& _right);
 	/// Computes the right hand side of a compound assignment.
 	smtutil::Expression compoundAssignment(Assignment const& _assignment);
 
@@ -181,6 +183,9 @@ protected:
 	void initializeLocalVariables(FunctionDefinition const& _function);
 	void initializeFunctionCallParameters(CallableDeclaration const& _function, std::vector<smtutil::Expression> const& _callArgs);
 	void resetStateVariables();
+	/// Resets all references/pointers that have the same type or have
+	/// a subexpression of the same type as _varDecl.
+	void resetReferences(VariableDeclaration const& _varDecl);
 	/// @returns the type without storage pointer information if it has it.
 	TypePointer typeWithoutPointer(TypePointer const& _type);