in checker/src/abstract_value.rs [1128:1711]
fn and(&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::And { left, right } = &y.expression {
is_contained_in(x, left) || is_contained_in(x, right)
} else {
false
}
}
// Do these tests here lest BOTTOM get simplified away.
if self.is_bottom() || other.is_top() {
return self.clone();
}
if other.is_bottom() || self.is_top() {
return other;
}
let self_bool = self.as_bool_if_known();
if let Some(false) = self_bool {
// [false && other] -> false
return Rc::new(FALSE);
};
let other_bool = other.as_bool_if_known();
if let Some(false) = other_bool {
// [self && false] -> false
return Rc::new(FALSE);
};
if self_bool.unwrap_or(false) {
if other_bool.unwrap_or(false) {
// [true && true] -> true
Rc::new(TRUE)
} else {
// [true && other] -> other
other
}
} else if other_bool.unwrap_or(false) {
// [self && true] -> self
self.clone()
} else {
// [x && (x && y)] -> x && y
// [y && (x && y)] -> x && y
// [(x && y) && x] -> x && y
// [(x && y) && y] -> x && y
if is_contained_in(self, &other) {
return other;
} else if is_contained_in(&other, self) {
return self.clone();
}
match &self.expression {
Expression::And { left: x, right: yz } => {
if let Expression::Or { left: y, right: z } = &yz.expression {
// [(x && (y || z)) && z] -> x && z
// [(x && (y || z)) && y] -> x && y
if y.eq(&other) || z.eq(&other) {
return x.and(other);
}
// [(x && (y || z)) && !a] -> (x && z) && !a if y => a
if let Expression::LogicalNot { operand: y2 } = &other.expression {
if y.implies(y2) {
return x.and(z.clone()).and(other);
}
}
}
// [(x && !y) && y] -> false
if let Expression::LogicalNot { operand: y } = &yz.expression {
if y.eq(&other) {
return Rc::new(FALSE);
}
}
}
Expression::LogicalNot { operand } if operand.eq(&other) => {
// [!x && x] -> false
return Rc::new(FALSE);
}
Expression::Or { left: x, right: y } => {
// [((c == x) || y) && (c != x)] -> y
if let (
Expression::Equals {
left: c1,
right: x1,
},
Expression::Ne {
left: c2,
right: x2,
},
) = (&x.expression, &other.expression)
{
if c1.eq(c2) && x1.eq(x2) {
return y.clone();
}
}
// [(x || (c == y)) && (c != y)] -> x
if let (
Expression::Equals {
left: c1,
right: x1,
},
Expression::Ne {
left: c2,
right: x2,
},
) = (&y.expression, &other.expression)
{
if c1.eq(c2) && x1.eq(x2) {
return x.clone();
}
}
// [(x || y) && x] -> x
// [(x || y) && y] -> y
if other.implies(x) || other.implies(y) {
return other;
}
if let Expression::LogicalNot { operand } = &other.expression {
// [(x || y) && (!x)] -> y && !x
if x.eq(operand) {
return y.and(other);
}
// [(x || y) && (!y)] -> x && !y
if y.eq(operand) {
return x.and(other);
}
}
}
_ => (),
}
match &other.expression {
Expression::And { left: x, right: y } => {
// [x && (x && y)] -> x && y
// [y && (x && y)] -> x && y
if x.eq(self) || y.eq(self) {
return other.clone();
}
}
// [x && c == y] -> c == y if refining x with c == y produces true
Expression::Equals { left: c, .. }
if self.expression_size < k_limits::MAX_EXPRESSION_SIZE / 10
&& c.is_compile_time_constant()
&& self
.refine_with(&other, 35)
.as_bool_if_known()
.unwrap_or(false) =>
{
return other.clone();
}
// [x && (true join x)] -> x
Expression::Join { left, right: x }
if left.as_bool_if_known().unwrap_or(false) && self.eq(x) =>
{
return self.clone();
}
// [x && (x join true)] -> x
Expression::Join { left: x, right }
if right.as_bool_if_known().unwrap_or(false) && self.eq(x) =>
{
return self.clone();
}
// [x && (true join false)] -> x
Expression::Join { left: x, right: y }
if x.as_bool_if_known().unwrap_or(false)
&& !y.as_bool_if_known().unwrap_or(true) =>
{
return self.clone();
}
// [x && (false join true)] -> x
Expression::Join { left: x, right: y }
if !x.as_bool_if_known().unwrap_or(true)
&& y.as_bool_if_known().unwrap_or(false) =>
{
return self.clone();
}
Expression::LogicalNot { operand } if operand.eq(self) => {
// [x && !x] -> false
return Rc::new(FALSE);
}
Expression::Or { left: x, right: y } => {
// [x && (x || y)] -> x
// [y && (x || y)] -> y
if x.eq(self) || y.eq(self) {
return self.clone();
}
if let Expression::LogicalNot { operand } = &self.expression {
// [(!x) && (x || y)] -> !x && y
if x.eq(operand) {
return self.and(y.clone());
}
// [(!y) && (x || y) ] -> !y && x
if y.eq(operand) {
return self.and(x.clone());
}
}
// [x && (x && y || x && z)] -> x && (y || z)
if let (
Expression::And { left: x1, right: y },
Expression::And { left: x2, right: z },
) = (&x.expression, &y.expression)
{
if self.eq(x1) && self.eq(x2) {
return self.and(y.or(z.clone()));
}
}
}
_ => (),
}
match (&self.expression, &other.expression) {
// [(a && (b != x)) && (c < x)] -> a && (c < x) if c >= b
(
Expression::And {
left: a1,
right: bx,
},
Expression::LessThan { left: c, right: x2 },
) => {
if let Expression::Ne { left: b, right: x1 } = &bx.expression {
if x1.eq(x2)
&& c.greater_or_equal(b.clone())
.as_bool_if_known()
.unwrap_or(false)
{
return a1.and(other);
}
}
}
// [(a && (x || b)) && (a && b)] -> a && b
// [(a && (0 == x)) && (x && b)] -> false
(
Expression::And {
left: a1,
right: xb,
},
Expression::And {
left: a2,
right: b2,
},
) => {
if let Expression::Or { right: b1, .. } = &xb.expression {
if a1.eq(a2) && b1.eq(b2) {
return other.clone();
}
}
if let Expression::Equals { left, right: x } = &xb.expression {
if left.is_zero() && x.eq(a2) {
return Rc::new(FALSE);
}
}
}
// [(a && (b || x )) && (x || y)] -> a && (x || (b && y)
(Expression::And { left: a, right: bx }, Expression::Or { left: x2, right: y }) => {
if let Expression::Or { left: b, right: x1 } = &bx.expression {
if x1.eq(x2) {
return a.and(x1.or(b.and(y.clone())));
}
}
}
// [(c ? a : b) && (c ? x : y)] -> c ? (a && x) : (b && y)
(
Expression::ConditionalExpression {
condition: c,
consequent: a,
alternate: b,
},
ConditionalExpression {
condition,
consequent,
alternate,
},
) if c.eq(condition) => {
return c.conditional_expression(
a.and(consequent.clone()),
b.and(alternate.clone()),
);
}
// [!x && !y] -> !(x || y)
(Expression::LogicalNot { operand: x }, Expression::LogicalNot { operand: y }) => {
return x.or(y.clone()).logical_not();
}
// [!(x && y) && x] -> x
// [!(x && y) && y] -> y
(Expression::LogicalNot { operand }, _) => {
if let Expression::And { left: x, right: y } = &operand.expression {
if x.eq(&other) || y.eq(&other) {
return other;
}
}
}
// [(x || y) && (!y && z)] -> x && !y && z
(Expression::Or { left: x, right: y1 }, Expression::And { left: ny, right: z }) => {
if let Expression::LogicalNot { operand: y2 } = &ny.expression {
if y1.eq(y2) {
return x.and(ny.and(z.clone()));
}
}
}
// [(x || !y) && !(x || y)] -> !x && !y
(
Expression::Or {
left: x1,
right: ny,
},
Expression::LogicalNot { operand: xy },
) if matches!(xy.expression, Expression::Or { .. }) => {
if let Expression::LogicalNot { operand: y1 } = &ny.expression {
if let Expression::Or {
left: x2,
right: y2,
} = &xy.expression
{
if x1.eq(x2) && y1.eq(y2) {
return x1.logical_not().and(ny.clone());
}
}
}
}
(
Expression::Or {
left: x1,
right: yz,
},
y,
) => {
// [(x || (y && z)) && y] -> [(x && y) || (y && z && y)] -> (x && y) || (y && z)
if let Expression::And { left: y1, right: z } = &yz.expression {
if y1.eq(&other) {
return x1.and(y1.clone()).or(y1.and(z.clone()));
}
}
if let Expression::Or {
left: x2,
right: y2,
} = y
{
// [(x || !y) && (x || y)] -> x
if let Expression::LogicalNot { operand: y1 } = &yz.expression {
if x1.eq(x2) && y1.eq(y2) {
return x1.clone();
}
}
// [(x || y) && (x || !y)] -> x
if let Expression::LogicalNot { operand: y2a } = &y2.expression {
if x1.eq(x2) && yz.eq(y2a) {
return x1.clone();
}
}
}
// [(0 = x || k == x) && (0 != x)] -> k == x if k != 0
if let Expression::Ne { left: c, right: x3 } = y {
if c.is_zero() {
if let (
Expression::Equals { left: e, right: x1 },
Expression::Equals { left: k, right: x2 },
) = (&x1.expression, &yz.expression)
{
if x1.eq(x2)
&& x2.eq(x3)
&& e.is_zero()
&& k.is_compile_time_constant()
&& !k.is_zero()
{
return yz.clone();
}
}
}
}
}
// [(x >= y) && (x == y)] -> x == y
// [(x >= y) && (x > y)] -> x > y
(
Expression::GreaterOrEqual {
left: x1,
right: y1,
},
Expression::Equals {
left: x2,
right: y2,
}
| Expression::GreaterThan {
left: x2,
right: y2,
},
) if x1.eq(x2) && y1.eq(y2) => {
return other.clone();
}
// [(x <= y) && (x == y)] -> x == y
// [(x <= y) && (x < y)] -> x < y
(
Expression::LessOrEqual {
left: x1,
right: y1,
},
Expression::Equals {
left: x2,
right: y2,
}
| Expression::LessThan {
left: x2,
right: y2,
},
) if x1.eq(x2) && y1.eq(y2) => {
return other.clone();
}
// [(x == y) && (x >= y)] -> x == y
// [(x > y) && (x >= y)] -> x > y
(
Expression::Equals {
left: x1,
right: y1,
}
| Expression::GreaterThan {
left: x1,
right: y1,
},
Expression::GreaterOrEqual {
left: x2,
right: y2,
},
) if x1.eq(x2) && y1.eq(y2) => {
return self.clone();
}
// [(x == y) && (x <= y)] -> x == y
// [(x < y) && (x <= y)] -> x < y
(
Expression::Equals {
left: x1,
right: y1,
}
| Expression::LessThan {
left: x1,
right: y1,
},
Expression::LessOrEqual {
left: x2,
right: y2,
},
) if x1.eq(x2) && y1.eq(y2) => {
return self.clone();
}
// [(x >= y) && (x != y)] -> x > y
(
Expression::GreaterOrEqual {
left: x1,
right: y1,
},
Expression::Ne {
left: x2,
right: y2,
},
) if x1.eq(x2) && y1.eq(y2) => {
return x1.greater_than(y1.clone());
}
// [(x <= y) && (x != y)] -> x < y
(
Expression::LessOrEqual {
left: x1,
right: y1,
},
Expression::Ne {
left: x2,
right: y2,
},
) if x1.eq(x2) && y1.eq(y2) => {
return x1.less_than(y1.clone());
}
// [(x <= y) && (x < z)] -> x < z if z <= y
(
Expression::LessOrEqual { left: x1, right: y },
Expression::LessThan { left: x2, right: z },
) if x1.eq(x2) => {
if let (
Expression::CompileTimeConstant(c1),
Expression::CompileTimeConstant(c2),
) = (&y.expression, &z.expression)
{
if c2.less_or_equal(c1).is_true() {
return other.clone();
}
}
}
// [(x != y) && (x >= y)] -> x > y
(
Expression::Ne {
left: x1,
right: y1,
},
Expression::GreaterOrEqual {
left: x2,
right: y2,
},
) if x1.eq(x2) && y1.eq(y2) => {
return x1.greater_than(y1.clone());
}
// [(x != y) && (x <= y)] -> x < y
(
Expression::Ne {
left: x1,
right: y1,
},
Expression::LessOrEqual {
left: x2,
right: y2,
},
) if x1.eq(x2) && y1.eq(y2) => {
return x1.less_than(y1.clone());
}
// [(x <= y) && (x >= y)] -> x == y
(
Expression::LessOrEqual {
left: x1,
right: y1,
},
Expression::GreaterOrEqual {
left: x2,
right: y2,
},
) if x1.eq(x2) && y1.eq(y2) => {
return x1.equals(y1.clone());
}
// [(x && (y >= z)) && (z != y)] -> x && (y > z)
(
Expression::And { left: x, right: yz },
Expression::Ne {
left: z1,
right: y1,
},
) => {
if let Expression::GreaterOrEqual {
left: y2,
right: z2,
} = &yz.expression
{
if y1.eq(y2) && z1.eq(z2) {
return x.and(y1.greater_than(z1.clone()));
}
}
}
_ => (),
}
// Refine other expression, except if it is known, or it is an assumed condition
// (the latter having an expression size zero so that they get retained when
// conjuncts are pruned away because of an expression overflow).
let other = if self_bool.is_none()
&& other.expression_size > 0
&& other.expression_size < k_limits::MAX_EXPRESSION_SIZE / 10
{
other.refine_with(self, 35)
} else {
other
};
if let Some(false) = other.as_bool_if_known() {
return other;
}
if other.expression_size >= k_limits::MAX_EXPRESSION_SIZE {
return other;
}
let mut trimmed_self = self.clone();
if self.expression_size.saturating_add(other.expression_size)
> k_limits::MAX_EXPRESSION_SIZE
{
// The overall expression is going to overflow, so abstract away part of the self
// (left) expression to keep the overall expression within bounds.
// We keep the right expression intact because it is usually path conditions that
// overflow and in a path condition the most recent (i.e. the right hand) condition
// is the most useful. In particular, we don't want to abstract away assume conditions.
if let Some(trimmed) = self
.trim_prefix_conjuncts(k_limits::MAX_EXPRESSION_SIZE - other.expression_size)
{
debug!("and expression prefix trimmed, self: {:?}", self);
trimmed_self = trimmed;
} else {
return other;
}
}
AbstractValue::make_binary(trimmed_self, other, |left, right| Expression::And {
left,
right,
})
}
}