fn less_or_equal()

in checker/src/abstract_value.rs [3461:3570]


    fn less_or_equal(&self, other: Rc<AbstractValue>) -> Rc<AbstractValue> {
        // [x <= c] -> c >= x
        if !self.is_compile_time_constant() && other.is_compile_time_constant() {
            // Normalize binary expressions so that if only one of the operands is a constant, it is
            // always the left operand.
            return other.greater_or_equal(self.clone());
        }
        if let Some(result) = self
            .get_cached_interval()
            .less_equal(&other.get_cached_interval())
        {
            return Rc::new(result.into());
        }
        // [0 <= v1] -> true if v1 is an unsigned number
        if self.is_zero() && other.expression.infer_type().is_unsigned_integer() {
            return Rc::new(TRUE);
        }
        match (&self.expression, &other.expression) {
            // [(c ? v1 : v2) <= c3] -> c ? (v1 <= c3) : (v2 <= c3)
            (
                Expression::ConditionalExpression {
                    condition: c,
                    consequent: v1,
                    alternate: v2,
                    ..
                },
                Expression::CompileTimeConstant(..),
            ) if !v1.is_top() && !v2.is_top() => {
                return c.conditional_expression(
                    v1.less_or_equal(other.clone()),
                    v2.less_or_equal(other.clone()),
                );
            }
            // [c3 <= (c ? v1 : v2)] -> c ? (c3 <= v1) : (c3 <= v2 )
            (
                Expression::CompileTimeConstant(..),
                Expression::ConditionalExpression {
                    condition: c,
                    consequent: v1,
                    alternate: v2,
                    ..
                },
            ) if !v1.is_top() && !v2.is_top() => {
                return c.conditional_expression(
                    self.less_or_equal(v1.clone()),
                    self.less_or_equal(v2.clone()),
                );
            }
            // [(if x <= y { x } else { y }) <= y] -> true
            (
                Expression::ConditionalExpression {
                    condition: c,
                    consequent: x,
                    alternate: y,
                    ..
                },
                _,
            ) if y.eq(&other) => {
                if let Expression::LessOrEqual {
                    left: x1,
                    right: y1,
                } = &c.expression
                {
                    if x1.eq(x) && y1.eq(y) {
                        return Rc::new(TRUE);
                    }
                }
            }
            // [x & c <= c] -> true
            (
                Expression::BitAnd {
                    left: _x,
                    right: c1,
                },
                Expression::CompileTimeConstant(..),
            ) if c1.eq(&other) => {
                return Rc::new(TRUE);
            }
            // [(c1 * x) <= c2] -> x <= c2 / c1
            (Expression::Mul { left: c1, right: x }, _)
                if c1.is_compile_time_constant()
                    && other.is_compile_time_constant()
                    && other.expression.infer_type().is_integer() =>
            {
                //todo: debug_checked_assume!(!c1.is_zero()); // otherwise constant folding would have reduced the Mul
                return x.less_or_equal(c1.divide(other.clone()));
            }
            // [c1 <= (c2 * x)] -> x > c1 / c2
            (_, Expression::Mul { left: c2, right: x })
                if self.is_compile_time_constant()
                    && c2.is_compile_time_constant()
                    && self.expression.infer_type().is_integer() =>
            {
                debug_checked_assume!(!c2.is_zero()); // otherwise constant folding would have reduced the Mul
                return x.greater_than(self.divide(c2.clone()));
            }
            _ => {}
        }
        self.try_to_constant_fold_and_distribute_binary_op(
            other,
            ConstantDomain::less_or_equal,
            Self::less_or_equal,
            |l, r| {
                AbstractValue::make_binary(l, r, |left, right| Expression::LessOrEqual {
                    left,
                    right,
                })
            },
        )
    }