in checker/src/abstract_value.rs [4007:4657]
fn or(&self, other: Rc<AbstractValue>) -> Rc<AbstractValue> {
fn is_contained_in(x: &Rc<AbstractValue>, y: &Rc<AbstractValue>) -> bool {
if x.eq(y) {
return true;
}
if let Expression::Or { left, right } = &y.expression {
is_contained_in(x, left) || is_contained_in(x, right)
} else {
false
}
}
let self_as_bool = self.as_bool_if_known();
if !self_as_bool.unwrap_or(true) {
// [false || y] -> y
other
} else if self_as_bool.unwrap_or(false) || other.as_bool_if_known().unwrap_or(false) {
// [x || true] -> true
// [true || y] -> true
Rc::new(TRUE)
} else if other.is_top() || other.is_bottom() || !self.as_bool_if_known().unwrap_or(true) {
// [self || TOP] -> TOP
// [self || BOTTOM] -> BOTTOM
// [false || other] -> other
other
} else if self.is_top() || self.is_bottom() || !other.as_bool_if_known().unwrap_or(true) {
// [TOP || other] -> TOP
// [BOTTOM || other] -> BOTTOM
// [self || false] -> self
self.clone()
} else {
// [x || x] -> x
if is_contained_in(self, &other) {
return self.clone();
}
// [!x || x] -> true
if let Expression::LogicalNot { operand } = &self.expression {
if is_contained_in(operand, &other) {
return Rc::new(TRUE);
}
}
// [x || !x] -> true
if let Expression::LogicalNot { operand } = &other.expression {
if is_contained_in(operand, self) {
return Rc::new(TRUE);
}
} else if is_contained_in(&self.logical_not(), &other) {
return Rc::new(TRUE);
}
// [x || (x || y)] -> x || y
// [x || (y || x)] -> x || y
// [(x || y) || y] -> x || y
// [(x || y) || x] -> x || y
if is_contained_in(self, &other) {
return other;
} else if is_contained_in(&other, self) {
return self.clone();
}
// [self || (x && z)] -> self || z if !self => x
if let Expression::And { left, right: z } = &other.expression {
if self.inverse_implies(left) {
return self.or(z.clone());
}
if let Expression::LogicalNot { operand: xy } = &left.expression {
match &xy.expression {
// [x || (!(!x && y) && z)] -> x || (!y && z)
Expression::And {
left: nx,
right: y2,
} => {
if let Expression::LogicalNot { operand: x2 } = &nx.expression {
if self.eq(x2) {
return self.or(y2.logical_not().and(z.clone()));
}
}
}
// [x || (!(x || y) && z)] -> x || (!y && z)
Expression::Or {
left: x2,
right: y2,
} => {
if self.eq(x2) {
return self.or(y2.logical_not().and(z.clone()));
}
}
_ => {}
}
}
}
// [x || (x && y)] -> x, etc.
if self.inverse_implies_not(&other) {
return self.clone();
}
// [x || !(x && y)] -> true, etc.
if self.inverse_implies(&other) {
return Rc::new(TRUE);
}
match (&self.expression, &other.expression) {
// [!x || x] -> true
(Expression::LogicalNot { operand }, _) if operand.eq(&other) => {
return Rc::new(TRUE);
}
// [x || !x] -> true
(_, Expression::LogicalNot { operand }) if operand.eq(self) => {
return Rc::new(TRUE);
}
// [(x == y) || (x != y)] -> true if x is not a floating point
(
Expression::Equals {
left: x1,
right: y1,
},
Expression::Ne {
left: x2,
right: y2,
},
) if x1.eq(x2)
&& y1.eq(y2)
&& !x1.expression.infer_type().is_floating_point_number() =>
{
return Rc::new(TRUE);
}
// [x >= y || x < y] -> true if x is not a floating point
(
Expression::GreaterOrEqual {
left: x1,
right: y1,
},
Expression::LessThan {
left: x2,
right: y2,
},
) if x1.eq(x2)
&& y1.eq(y2)
&& !x1.expression.infer_type().is_floating_point_number() =>
{
return Rc::new(TRUE);
}
// [x < y || x >= y] -> true if x is not a floating point
(
Expression::LessThan {
left: x1,
right: y1,
},
Expression::GreaterOrEqual {
left: x2,
right: y2,
},
) if x1.eq(x2)
&& y1.eq(y2)
&& !x1.expression.infer_type().is_floating_point_number() =>
{
return Rc::new(TRUE);
}
// [x <= y || x > y] -> true if x is not a floating point
(
Expression::LessOrEqual {
left: x1,
right: y1,
},
Expression::GreaterThan {
left: x2,
right: y2,
},
) if x1.eq(x2)
&& y1.eq(y2)
&& !x1.expression.infer_type().is_floating_point_number() =>
{
return Rc::new(TRUE);
}
// [x > y || x <= y] -> true if x is not a floating point
(
Expression::GreaterThan {
left: x1,
right: y1,
},
Expression::LessOrEqual {
left: x2,
right: y2,
},
) if x1.eq(x2)
&& y1.eq(y2)
&& !x1.expression.infer_type().is_floating_point_number() =>
{
return Rc::new(TRUE);
}
// [x > y || x == y] -> x >= y
// [x >= y || x == y] -> x >= y
(
Expression::GreaterThan {
left: x1,
right: y1,
},
Expression::Equals {
left: x2,
right: y2,
},
)
| (
Expression::GreaterOrEqual {
left: x1,
right: y1,
},
Expression::Equals {
left: x2,
right: y2,
},
) if x1.eq(x2) && y1.eq(y2) => {
return x1.greater_or_equal(y1.clone());
}
// [x == y || x > y] -> x >= y
// [x == y || x >= y] -> x >= y
(
Expression::Equals {
left: x1,
right: y1,
},
Expression::GreaterThan {
left: x2,
right: y2,
},
)
| (
Expression::Equals {
left: x1,
right: y1,
},
Expression::GreaterOrEqual {
left: x2,
right: y2,
},
) if x1.eq(x2) && y1.eq(y2) => {
return x1.greater_or_equal(y1.clone());
}
// [(x == y) || (y > z)] -> y > z if z < x
(
Expression::Equals { left: x, right: y1 },
Expression::GreaterThan { left: y2, right: z },
) if y1.eq(y2) => {
if let (
Expression::CompileTimeConstant(cx),
Expression::CompileTimeConstant(cz),
) = (&x.expression, &z.expression)
{
if cz.less_than(cx).is_true() {
return other.clone();
}
}
}
// [x < y || x == y] -> x <= y
// [x <= y || x == y] -> x <= y
(
Expression::LessThan {
left: x1,
right: y1,
},
Expression::Equals {
left: x2,
right: y2,
},
)
| (
Expression::LessOrEqual {
left: x1,
right: y1,
},
Expression::Equals {
left: x2,
right: y2,
},
)
| (
Expression::LessOrEqual {
left: x1,
right: y1,
},
Expression::Equals {
left: x2,
right: y2,
},
) if x1.eq(x2) && y1.eq(y2) => {
return x1.less_or_equal(y1.clone());
}
// [x < y || x <= y] -> x <= y
// [x < y || x == y] -> x <= y
// [y == x || x < y] -> x <= y
(
Expression::LessThan {
left: x1,
right: y1,
},
Expression::LessOrEqual {
left: x2,
right: y2,
},
)
| (
Expression::LessThan {
left: x1,
right: y1,
},
Expression::Equals {
left: x2,
right: y2,
},
)
| (
Expression::Equals {
left: y1,
right: x1,
},
Expression::LessThan {
left: x2,
right: y2,
},
) if x1.eq(x2) && y1.eq(y2) => {
return x1.less_or_equal(y2.clone());
}
// [x < y || x <= y] -> x <= y
(
Expression::LessThan {
left: x1,
right: y1,
},
Expression::LessOrEqual {
left: x2,
right: y2,
},
) if x1.eq(x2) && y1.eq(y2) => {
return other.clone();
}
// [x == y || x <==> y] -> x <= y
(
Expression::Equals {
left: x1,
right: y1,
},
Expression::LessThan {
left: x2,
right: y2,
},
) if x1.eq(x2) && y1.eq(y2) => {
return x1.less_or_equal(y1.clone());
}
(
Expression::And {
left: x1,
right: y1,
},
Expression::And {
left: x2,
right: y2,
},
) => {
if x1.eq(x2) {
return if y1.logical_not().eq(y2) {
// [(x && y) || (x && !y)] -> x
x1.clone()
} else {
// [(x && y1) || (x && y2)] -> x && (y1 || y2)
x1.and(y1.or(y2.clone()))
};
} else if y1.eq(y2) {
return if x1.logical_not().eq(x2) {
// [(x && y) || (!x && y)] -> y
y1.clone()
} else {
// [(x1 && y) || (x2 && y)] -> (x1 || x2) && y
x1.or(x2.clone()).and(y1.clone())
};
} else if let Expression::And {
left: x2,
right: x3,
} = &x2.expression
{
if x1.eq(x2) {
// [(x && y1) || ((x && x3) && y2)] -> x && (y1 || (x3 && y2))
return x1.and(y1.or(x3.and(y2.clone())));
}
}
}
// [((c ? e : 1) == 1) || ((c ? e : 1) == 0)] -> !c || e == 0 || e == 1
(
Expression::Equals {
left: l1,
right: r1,
},
Expression::Equals {
left: l2,
right: r2,
},
) if l1.eq(l2) && r1.expression.is_one() && r2.expression.is_zero() => {
if let Expression::ConditionalExpression {
condition: c,
consequent: e,
alternate: one,
} = &l1.expression
{
if one.expression.is_one() {
let not_c = c.logical_not();
let e_eq_0 = e.equals(Rc::new(ConstantDomain::U128(0).into()));
let e_eq_1 = e.equals(Rc::new(ConstantDomain::U128(1).into()));
return not_c.or(e_eq_0).or(e_eq_1);
}
}
}
// [1 == ((c ? e : 1)) || (0 == (c ? e : 1))] -> !c || 0 == e || 1 == e
(
Expression::Equals {
left: l1,
right: r1,
},
Expression::Equals {
left: l2,
right: r2,
},
) if r1.eq(r2) && l1.expression.is_one() && l2.expression.is_zero() => {
if let Expression::ConditionalExpression {
condition: c,
consequent: e,
alternate: one,
} = &r1.expression
{
if one.expression.is_one() {
let not_c = c.logical_not();
let e_eq_0 = e.equals(Rc::new(ConstantDomain::U128(0).into()));
let e_eq_1 = e.equals(Rc::new(ConstantDomain::U128(1).into()));
return not_c.or(e_eq_0).or(e_eq_1);
}
}
}
// [( x ? false : y ) || x] -> x || y
(
Expression::ConditionalExpression {
condition: x,
consequent: f,
alternate: y,
},
_,
) if x.eq(&other) && !f.as_bool_if_known().unwrap_or(true) => {
return x.or(y.clone());
}
// [(x && y) || x] -> x
// [(x && y) || y] -> y
(Expression::And { left: x, right: y }, _) if x.eq(&other) || y.eq(&other) => {
return other;
}
// [x || (x && y)] -> x
// [y || (x && y)] -> y
(_, Expression::And { left: x, right: y }) if x.eq(self) || y.eq(self) => {
return self.clone();
}
// [x || (!x && z)] -> x || z
(_, Expression::And { left: y, right: z }) if self.inverse_implies(y) => {
return self.or(z.clone());
}
// [(x && y) || (!x || !y)] -> true
(Expression::And { left: x, right: y }, Expression::Or { left, right })
if x.inverse_implies(left) && y.inverse_implies(right) =>
{
return Rc::new(TRUE);
}
// [widened bool || x] -> unknown bool || x
(Expression::WidenedJoin { path, .. }, _) => {
return AbstractValue::make_typed_unknown(ExpressionType::Bool, path.clone())
.or(other);
}
// [x || widened bool] -> x || unknown bool
(_, Expression::WidenedJoin { path, .. }) => {
return self.or(AbstractValue::make_typed_unknown(
ExpressionType::Bool,
path.clone(),
));
}
// [(x && !y) || !(x || y)] -> !y
// [(x && !y) || !(y || x)] -> !y
(Expression::And { left: x1, right }, Expression::LogicalNot { operand })
if matches!(right.expression, Expression::LogicalNot { .. })
&& matches!(operand.expression, Expression::Or { .. }) =>
{
if let (
Expression::LogicalNot { operand: y1 },
Expression::Or {
left: x2,
right: y2,
},
) = (&right.expression, &operand.expression)
{
if (x1.eq(x2) && y1.eq(y2)) || (x1.eq(y2) && y1.eq(x2)) {
return right.clone();
}
}
}
// [(!x && y) || !(x || y)] -> !x
(
Expression::And {
left: nx,
right: y1,
},
Expression::LogicalNot { operand },
) if matches!(nx.expression, Expression::LogicalNot { .. })
&& matches!(operand.expression, Expression::Or { .. }) =>
{
if let (
Expression::LogicalNot { operand: x1 },
Expression::Or {
left: x2,
right: y2,
},
) = (&nx.expression, &operand.expression)
{
if x1.eq(x2) && y1.eq(y2) {
return nx.clone();
}
}
}
(Expression::And { left, right }, _) => {
match (&left.expression, &right.expression) {
// [(x && !y) || y] -> (x || y)
(_, Expression::LogicalNot { operand: y }) if y.eq(&other) => {
return left.or(y.clone());
}
// [(!x && y) || x] -> (x || y)
(Expression::LogicalNot { operand: x }, _) if x.eq(&other) => {
return x.or(right.clone());
}
_ => {}
}
}
(
Expression::Or {
left: x,
right: ynz,
},
Expression::And {
left: y2,
right: z2,
},
) => {
// [(x || (y && !z)) || (y && z)))] -> x || y
if let Expression::And {
left: y1,
right: nz,
} = &ynz.expression
{
if let Expression::LogicalNot { operand: z1 } = &nz.expression {
if y1.eq(y2) && z1.eq(z2) {
return x.or(y1.clone());
}
}
}
// [((x || (y && !z)) || a) || (y && z)] -> (x || y) || a
if let Expression::Or {
left: x1,
right: ynz1,
} = &x.expression
{
let a = ynz;
if let Expression::And {
left: y1,
right: nz,
} = &ynz1.expression
{
if let Expression::LogicalNot { operand: z1 } = &nz.expression {
if y1.eq(y2) && z1.eq(z2) {
return x1.or(y1.clone()).or(a.clone());
}
}
}
}
}
// [(x || (y < z)) || (z == y)] -> x || (y <= z)
(
Expression::Or {
left: x,
right: y_lt_z,
},
Expression::Equals {
left: z1,
right: y1,
},
) => {
if let Expression::LessThan {
left: y2,
right: z2,
} = &y_lt_z.expression
{
if y1.eq(y2) && z1.eq(z2) {
return x.or(y1.less_or_equal(z1.clone()));
}
}
}
// [x || !(x || y)] -> x || !y
(_, Expression::LogicalNot { operand }) => match &operand.expression {
Expression::Or { left: x2, right: y } if self.eq(x2) => {
return self.or(y.logical_not());
}
_ => {}
},
// [!x || (x && y ? false : z)] -> !x || (!y && z)
(
Expression::LogicalNot { operand: x1 },
Expression::ConditionalExpression {
condition: c,
consequent,
alternate: z,
},
) => {
if let Expression::And { left: x2, right: y } = &c.expression {
if x1.eq(x2) && !consequent.as_bool_if_known().unwrap_or(true) {
return self.or(y.logical_not().and(z.clone()));
}
}
}
_ => {}
}
self.try_to_constant_fold_and_distribute_binary_op(
other,
ConstantDomain::or,
Self::or,
|l, r| {
AbstractValue::make_binary(l, r, |left, right| Expression::Or { left, right })
},
)
}
}