fn get_as_interval()

in checker/src/abstract_value.rs [5412:5507]


    fn get_as_interval(&self) -> IntervalDomain {
        match &self.expression {
            Expression::Top => interval_domain::BOTTOM,
            Expression::Add { left, right } => left.get_as_interval().add(&right.get_as_interval()),
            Expression::BitAnd { left, .. } => {
                if let Expression::CompileTimeConstant(ConstantDomain::U128(v)) = left.expression {
                    if v < (i128::MAX as u128) && (v + 1).is_power_of_two() {
                        let lower: IntervalDomain = 0u128.into();
                        let upper: IntervalDomain = v.into();
                        return lower.widen(&upper);
                    }
                }
                interval_domain::BOTTOM
            }
            Expression::Cast {
                operand,
                target_type,
            } => operand
                .get_as_interval()
                .intersect(&IntervalDomain::from(*target_type)),
            Expression::CompileTimeConstant(ConstantDomain::I128(val)) => (*val).into(),
            Expression::CompileTimeConstant(ConstantDomain::U128(val)) => (*val).into(),
            Expression::ConditionalExpression {
                consequent,
                alternate,
                ..
            } => consequent
                .get_as_interval()
                .widen(&alternate.get_as_interval()),
            Expression::Div { left, right } => left.get_as_interval().div(&right.get_as_interval()),
            Expression::IntrinsicBitVectorUnary {
                name, bit_length, ..
            } => match name {
                KnownNames::StdIntrinsicsCtlz
                | KnownNames::StdIntrinsicsCtlzNonzero
                | KnownNames::StdIntrinsicsCtpop
                | KnownNames::StdIntrinsicsCttz
                | KnownNames::StdIntrinsicsCttzNonzero => {
                    let min_value: IntervalDomain = IntervalDomain::from(0u128);
                    let max_value = IntervalDomain::from(*bit_length as u128);
                    min_value.widen(&max_value)
                }
                _ => interval_domain::BOTTOM,
            },
            Expression::Join { left, right, .. } => {
                left.get_as_interval().widen(&right.get_as_interval())
            }
            Expression::Mul { left, right } => left.get_as_interval().mul(&right.get_as_interval()),
            Expression::Neg { operand } => operand.get_as_interval().neg(),
            Expression::Rem { left, right } => left.get_as_interval().rem(&right.get_as_interval()),
            Expression::Sub { left, right } => left.get_as_interval().sub(&right.get_as_interval()),
            Expression::Switch { cases, default, .. } => cases
                .iter()
                .fold(default.get_as_interval(), |acc, (_, result)| {
                    acc.widen(&result.get_as_interval())
                }),
            Expression::TaggedExpression { operand, .. } => operand.get_as_interval(),
            Expression::Variable { var_type, .. } => IntervalDomain::from(*var_type),
            Expression::WidenedJoin { operand, .. } => {
                let interval = operand.get_as_interval();
                if interval.is_bottom() {
                    return interval;
                }
                if let Expression::Join { left, .. } = &operand.expression {
                    let left_interval = left.get_as_interval();
                    if left_interval.is_bottom() {
                        return interval_domain::BOTTOM;
                    }
                    match (left_interval.lower_bound(), interval.lower_bound()) {
                        (Some(llb), Some(lb)) if llb == lb => {
                            // The lower bound is finite and does not change as a result of the fixed
                            // point computation, so we can keep it, but we widen the upper bound.
                            let target_type = operand.expression.infer_type();
                            return interval
                                .remove_upper_bound()
                                .intersect(&IntervalDomain::from(target_type));
                        }
                        _ => (),
                    }
                    match (left_interval.upper_bound(), interval.upper_bound()) {
                        (Some(lub), Some(ub)) if lub == ub => {
                            // The upper bound is finite and does not change as a result of the fixed
                            // point computation, so we can keep it, but we widen the lower bound.
                            let target_type = operand.expression.infer_type();
                            return interval
                                .remove_lower_bound()
                                .intersect(&IntervalDomain::from(target_type));
                        }
                        _ => (),
                    }
                }
                interval
            }
            _ => interval_domain::BOTTOM,
        }
    }