fn get_tags()

in checker/src/abstract_value.rs [5555:5693]
114 lines of code
4 McCabe index (conditional complexity)

    fn get_tags(&self) -> TagDomain {
        let exp_tag_prop_opt = self.expression.get_tag_propagation();

        // First deal with expressions that do not propagate tags or have special propagation behavior.
        match &self.expression {
            Expression::Top
            | Expression::Bottom
            | Expression::CompileTimeConstant { .. }
            | Expression::HeapBlock { .. }
            | Expression::HeapBlockLayout { .. }
            | Expression::Reference { .. }
            | Expression::UnknownTagCheck { .. } => return TagDomain::empty_set(),

            Expression::InitialParameterValue { .. }
            | Expression::UnknownModelField { .. }
            | Expression::UnknownTagField { .. }
            | Expression::Variable { .. } => {
                // A variable is an unknown value of a place in memory.
                // Therefore, the associated tags are also unknown.
                return TagDomain::top();
            }

            Expression::ConditionalExpression {
                condition,
                consequent,
                alternate,
            } => {
                // For each tag A, whether the conditional expression has tag A or not is
                // (condition has tag A) or ((consequent has tag A) join (alternate has tag A)).
                return condition.get_cached_tags().or(&consequent
                    .get_cached_tags()
                    .join(&alternate.get_cached_tags()));
            }

            Expression::Join { left, right, .. } => {
                // For each tag A, whether the join expression has tag A or not is
                // ((left has tag A) join (right has tag A)).
                return left
                    .get_cached_tags()
                    .join(right.get_cached_tags().as_ref());
            }

            Expression::Switch {
                discriminator,
                cases,
                default,
            } => {
                // For each tag A, whether the switch expression has tag A or not is
                // (discriminator has tag A) or ((case_0 has tag A) join .. join (case_n has tag A) join (default has tag A)).
                let mut tags_from_cases = (*default.get_cached_tags()).clone();
                for case in cases {
                    tags_from_cases = tags_from_cases.join(case.1.get_cached_tags().as_ref())
                }
                return discriminator.get_cached_tags().or(&tags_from_cases);
            }

            Expression::TaggedExpression { operand, tag } => {
                return operand.get_cached_tags().add_tag(*tag);
            }

            Expression::WidenedJoin { operand, .. } => {
                let tags = operand.get_cached_tags();
                return (*tags).clone();
            }

            _ => {
                checked_assume!(exp_tag_prop_opt.is_some());
            }
        }

        let exp_tag_prop = exp_tag_prop_opt.unwrap();

        // Then deal with expressions that have standard propagation behavior, i.e., taking tags
        // from children nodes.
        match &self.expression {
            Expression::Add { left, right }
            | Expression::AddOverflows { left, right, .. }
            | Expression::And { left, right }
            | Expression::BitAnd { left, right }
            | Expression::BitOr { left, right }
            | Expression::BitXor { left, right }
            | Expression::Div { left, right }
            | Expression::Equals { left, right }
            | Expression::GreaterOrEqual { left, right }
            | Expression::GreaterThan { left, right }
            | Expression::IntrinsicBinary { left, right, .. }
            | Expression::LessOrEqual { left, right }
            | Expression::LessThan { left, right }
            | Expression::Mul { left, right }
            | Expression::MulOverflows { left, right, .. }
            | Expression::Ne { left, right }
            | Expression::Or { left, right }
            | Expression::Offset { left, right }
            | Expression::Rem { left, right }
            | Expression::Shl { left, right }
            | Expression::ShlOverflows { left, right, .. }
            | Expression::Shr { left, right, .. }
            | Expression::ShrOverflows { left, right, .. }
            | Expression::Sub { left, right }
            | Expression::SubOverflows { left, right, .. } => left
                .get_cached_tags()
                .propagate_through(exp_tag_prop)
                .or(&right.get_cached_tags().propagate_through(exp_tag_prop)),

            Expression::BitNot { operand, .. }
            | Expression::Cast { operand, .. }
            | Expression::IntrinsicBitVectorUnary { operand, .. }
            | Expression::IntrinsicFloatingPointUnary { operand, .. }
            | Expression::LogicalNot { operand, .. }
            | Expression::Neg { operand, .. }
            | Expression::Transmute { operand, .. } => {
                operand.get_cached_tags().propagate_through(exp_tag_prop)
            }

            Expression::Memcmp {
                left,
                right,
                length,
            } => left
                .get_cached_tags()
                .propagate_through(exp_tag_prop)
                .or(&right.get_cached_tags().propagate_through(exp_tag_prop))
                .or(&length.get_cached_tags().propagate_through(exp_tag_prop)),

            Expression::UninterpretedCall {
                callee, arguments, ..
            } => {
                let mut tags = callee.get_cached_tags().propagate_through(exp_tag_prop);
                for argument in arguments {
                    tags = tags.or(&argument.get_cached_tags().propagate_through(exp_tag_prop))
                }
                tags
            }

            _ => {
                verify_unreachable!();
            }
        }
    }