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,
})
},
)
}