in checker/src/abstract_value.rs [2521:2778]
fn equals(&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.equals(self.clone());
}
match (&self.expression, &other.expression) {
// true == x -> x
(Expression::CompileTimeConstant(ConstantDomain::True), _) => {
return other.clone();
}
// false == x -> !x
(Expression::CompileTimeConstant(ConstantDomain::False), _) => {
return other.logical_not();
}
// [(x as *t) == (y as *t)] -> x == y if known at compile time
(
Expression::Cast {
operand: x,
target_type: tt1,
},
Expression::Cast {
operand: y,
target_type: tt2,
},
) if *tt1 == ExpressionType::ThinPointer && *tt2 == ExpressionType::ThinPointer => {
let operands_are_equal = x.equals(y.clone());
if operands_are_equal.is_compile_time_constant() {
return operands_are_equal;
}
}
// [not null == (0 as *T)] -> false
(
_,
Expression::Cast {
operand,
target_type,
},
) if *target_type == ExpressionType::ThinPointer
&& operand.is_zero()
&& self.is_non_null() =>
{
return Rc::new(FALSE);
}
(
Expression::HeapBlock {
abstract_address: a1,
..
},
Expression::HeapBlock {
abstract_address: a2,
..
},
) => {
return if *a1 == *a2 {
Rc::new(TRUE)
} else {
Rc::new(FALSE)
};
}
// [(widened == val)] -> if !interval(widened).intersect(interval(val)) { false } else { unknown == val }
(Expression::WidenedJoin { path, .. }, _) => {
let widened_interval = self.get_cached_interval();
let val_interval = other.get_cached_interval();
if !widened_interval.is_bottom()
&& !val_interval.is_bottom()
&& widened_interval.intersect(&val_interval).is_bottom()
{
return Rc::new(FALSE);
} else if self.expression_size.saturating_add(other.expression_size)
> k_limits::MAX_EXPRESSION_SIZE / 2
|| self.expression.contains_local_variable(false)
{
return AbstractValue::make_typed_unknown(
other.expression.infer_type(),
path.clone(),
)
.equals(other);
};
}
// [(val == widened)] -> if !interval(widened).intersect(interval(val)) { false } else { val == unknown }
(_, Expression::WidenedJoin { path, .. }) => {
let val_interval = self.get_cached_interval();
let widened_interval = other.get_cached_interval();
if !widened_interval.is_bottom()
&& !val_interval.is_bottom()
&& widened_interval.intersect(&val_interval).is_bottom()
{
return Rc::new(FALSE);
} else if self.expression_size.saturating_add(other.expression_size)
> k_limits::MAX_EXPRESSION_SIZE / 2
|| other.expression.contains_local_variable(false)
{
return self.equals(AbstractValue::make_typed_unknown(
other.expression.infer_type(),
path.clone(),
));
};
}
// [c3 == (c ? v1 : v2)] -> !c if v1 != c3 && v2 == c3
// [c3 == (c ? v1 : v2)] -> c if v1 == c3 && v2 != c3
// [c3 == (c ? v1 : v2)] -> true if v1 == c3 && v2 == c3
// [c3 == (c ? v1 : v2)] -> c ? (c3 == v1) : (c3 == v2)
(
Expression::CompileTimeConstant(..),
Expression::ConditionalExpression {
condition: c,
consequent: v1,
alternate: v2,
..
},
) if !v1.is_top()
&& v1.expression_size < k_limits::MAX_EXPRESSION_SIZE / 10
&& !v2.is_top()
&& v2.expression_size < k_limits::MAX_EXPRESSION_SIZE / 10 =>
{
let self_eq_v2 = self.equals(v2.clone()).as_bool_if_known().unwrap_or(false);
if self
.not_equals(v1.clone())
.as_bool_if_known()
.unwrap_or(false)
&& self_eq_v2
{
return c.logical_not();
}
if self.equals(v1.clone()).as_bool_if_known().unwrap_or(false) {
if self
.not_equals(v2.clone())
.as_bool_if_known()
.unwrap_or(false)
{
return c.clone();
} else if self_eq_v2 {
return Rc::new(TRUE);
}
}
if self.eq(&other) && !self.expression.infer_type().is_floating_point_number() {
return Rc::new(TRUE);
}
if v1.expression_size < k_limits::MAX_EXPRESSION_SIZE / 10
&& v2.expression_size < k_limits::MAX_EXPRESSION_SIZE / 10
{
return c
.conditional_expression(self.equals(v1.clone()), self.equals(v2.clone()));
}
}
// [0 == !x] -> x when x is Boolean. Canonicalize it to the latter.
(
Expression::CompileTimeConstant(ConstantDomain::U128(val)),
Expression::LogicalNot { operand },
) => {
if *val == 0 && operand.expression.infer_type() == ExpressionType::Bool {
return operand.clone();
}
}
// [0 == c * x] -> 0 == x
(Expression::CompileTimeConstant(z), Expression::Mul { left: c, right: x })
if z.is_zero() && c.is_compile_time_constant() =>
{
return self.equals(x.clone());
}
// [0 == (0 % x)] -> true
(Expression::CompileTimeConstant(z), Expression::Rem { left: c, .. })
if z.is_zero() && c.is_zero() =>
{
return Rc::new(TRUE);
}
// [0 == (1 << x)] -> false (we can assume no overflows occur)
(
Expression::CompileTimeConstant(ConstantDomain::U128(0)),
Expression::Shl { left, .. },
) => {
if let Expression::CompileTimeConstant(ConstantDomain::U128(1)) = left.expression {
return Rc::new(FALSE);
}
}
// [0 == x] -> !x when x is a Boolean. Canonicalize it to the latter.
// [1 == x] -> x when x is a Boolean. Canonicalize it to the latter.
(Expression::CompileTimeConstant(ConstantDomain::U128(val)), x) => {
if x.infer_type() == ExpressionType::Bool {
return if *val == 0 {
other.logical_not()
} else {
other.clone()
};
}
}
// [(if x { y } else { z }) == z] -> [if x { y == z } else { true }] -> !x || y == z
(
Expression::ConditionalExpression {
condition: x,
consequent: y,
alternate: z,
},
_,
) if z.eq(&other) => {
return x.logical_not().or(y.equals(z.clone()));
}
// [z == (if x { y } else { z })] -> [if x { y == z } else { true }] -> !x || y == z
(
_,
Expression::ConditionalExpression {
condition: x,
consequent: y,
alternate: z,
},
) if z.eq(self) => {
return x.logical_not().or(y.equals(z.clone()));
}
// [(if x { y } else { z }) == a] -> [if x { y == a } else { z == a }]
(
Expression::ConditionalExpression {
condition: x,
consequent: y,
alternate: z,
},
_,
) => {
if self.expression_size + other.expression_size * 2 < k_limits::MAX_EXPRESSION_SIZE
&& !y.is_top()
&& !z.is_top()
{
return x
.conditional_expression(y.equals(other.clone()), z.equals(other.clone()));
}
}
// [c1 == (c2 * x)] -> (c1 / c2) == x
(Expression::CompileTimeConstant(..), Expression::Mul { left: c2, right: x })
if 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 self.divide(c2.clone()).equals(x.clone());
}
(Expression::Reference { .. }, Expression::Cast { .. })
| (Expression::Cast { .. }, Expression::Reference { .. }) => {
return Rc::new(FALSE);
}
_ => {
// If self and other are the same expression and the expression could not result in
// NaN we can simplify this to true.
if self.eq(&other) && !self.expression.infer_type().is_floating_point_number() {
return Rc::new(TRUE);
}
}
}
self.try_to_constant_fold_and_distribute_binary_op(
other,
ConstantDomain::equals,
Self::equals,
|l, r| {
AbstractValue::make_binary(l, r, |left, right| Expression::Equals { left, right })
},
)
}