Method indexOrMemberAssignment

libsolidity/formal/SMTEncoder.cpp:1637–1722

}

void SMTEncoder::indexOrMemberAssignment(Expression const& _expr, smtutil::Expression const& _rightHandSide)
{
	auto toStore = _rightHandSide;
	auto const* lastExpr = &_expr;
	while (true)
	{
		if (auto const* indexAccess = dynamic_cast<IndexAccess const*>(lastExpr))
		{
			auto const& base = indexAccess->baseExpression();
			if (dynamic_cast<Identifier const*>(&base))
				base.accept(*this);

			Type const* baseType = base.annotation().type;
			auto indexExpr = expr(*indexAccess->indexExpression(), keyType(baseType));
			auto symbArray = std::dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(base));
			solAssert(symbArray, "");
			toStore = smtutil::Expression::tuple_constructor(
				smtutil::Expression(std::make_shared<smtutil::SortSort>(smt::smtSort(*baseType)), baseType->toString(true)),
				{smtutil::Expression::store(symbArray->elements(), indexExpr, toStore), symbArray->length()}
			);
			defineExpr(*indexAccess, smtutil::Expression::select(
				symbArray->elements(),
				indexExpr
			));
			lastExpr = &indexAccess->baseExpression();
		}
		else if (auto const* memberAccess = dynamic_cast<MemberAccess const*>(lastExpr))
		{
			auto const& base = memberAccess->expression();
			if (dynamic_cast<Identifier const*>(&base))
				base.accept(*this);

			if (
				auto const* structType = dynamic_cast<StructType const*>(base.annotation().type);
				structType && structType->recursive()
			)
			{
				m_unsupportedErrors.warning(
					4375_error,
					memberAccess->location(),
					"Assertion checker does not support recursive structs."
				);
				return;
			}
			if (auto varDecl = identifierToVariable(*memberAccess))
			{
				if (varDecl->hasReferenceOrMappingType())
					resetReferences(*varDecl);

				assignment(*varDecl, toStore);
				break;
			}

			auto symbStruct = std::dynamic_pointer_cast<smt::SymbolicStructVariable>(m_context.expression(base));
			solAssert(symbStruct, "");
			symbStruct->assignMember(memberAccess->memberName(), toStore);
			toStore = symbStruct->currentValue();
			defineExpr(*memberAccess, symbStruct->member(memberAccess->memberName()));