in checker/src/abstract_value.rs [1973:2363]
fn conditional_expression(
&self,
mut consequent: Rc<AbstractValue>,
mut alternate: Rc<AbstractValue>,
) -> Rc<AbstractValue> {
if self.is_bottom() {
// If the condition is impossible so is the expression.
return self.clone();
}
// If either of the branches is impossible, it must be the other one.
if consequent.is_bottom() {
return alternate;
}
if alternate.is_bottom() {
return consequent;
}
// If the branches are the same, the condition does no matter.
if consequent.eq(&alternate) {
// [c ? x : x] -> x
return consequent;
}
// If the condition is unknown, the rules below won't fire.
if self.is_top() {
return self.clone();
}
if self.eq(&consequent) {
// [x ? x : y] -> x || y
return self.or(alternate);
}
if self.eq(&alternate) {
// [y ? x : y] -> y && x
return self.and(consequent);
}
let self_as_bool = self.as_bool_if_known();
if self_as_bool == Some(true) {
// [true ? x : y] -> x
return consequent;
} else if self_as_bool == Some(false) {
// [false ? x : y] -> y
return alternate;
}
// simplification rules are heuristic and can be non symmetric.
let not_self = self.logical_not();
let not_self_as_bool = not_self.as_bool_if_known();
if not_self_as_bool == Some(false) {
// [true ? x : y] -> x
return consequent;
} else if not_self_as_bool == Some(true) {
// [false ? x : y] -> y
return alternate;
}
if let (Expression::CompileTimeConstant(v1), Expression::CompileTimeConstant(v2)) =
(&consequent.expression, &alternate.expression)
{
match (v1, v2) {
(ConstantDomain::True, ConstantDomain::False) => {
// [c ? true : false] -> c
return self.clone();
}
(ConstantDomain::False, ConstantDomain::True) => {
// [c ? false : true] -> !c
return self.logical_not();
}
_ => (),
}
}
if let Expression::LogicalNot { operand } = &self.expression {
// [if !(x) { a } else { b }] -> if x { b } else { a }
return operand.conditional_expression(alternate, consequent);
}
// [if 0 == x { y } else { true }] -> x || y
// [if 0 == x { false } else { y }] -> x && y
if let Expression::Equals { left: z, right: x } = &self.expression {
if let Expression::CompileTimeConstant(ConstantDomain::U128(0)) = z.expression {
if alternate.as_bool_if_known().unwrap_or(false) {
return x.or(consequent);
}
if !consequent.as_bool_if_known().unwrap_or(true) {
return x.and(alternate);
}
}
}
// [if 0 != x { x } else { 0 } ] -> x
// [if 0 != x { 0 } else { x } ] -> x
if let Expression::Ne { left: z, right: x } = &self.expression {
if let Expression::CompileTimeConstant(ConstantDomain::U128(0)) = z.expression {
if consequent.eq(x) {
if alternate.is_zero() {
return consequent;
}
} else if alternate.eq(x) && consequent.is_zero() {
return alternate;
}
}
}
let consequent_as_bool_if_known = consequent.as_bool_if_known();
// [if x { true } else { y }] -> x || y
if consequent_as_bool_if_known.unwrap_or(false) {
return self.or(alternate);
}
// [if x { false } else { x && y) ] -> false
// [ if x { false } else { y } ] -> !x && y
if !consequent_as_bool_if_known.unwrap_or(true) {
if let Expression::And { left: x, right: y } = &alternate.expression {
if self.eq(x) || self.eq(y) {
return Rc::new(FALSE);
}
}
return self.logical_not().and(alternate);
}
// [if x { y } else { false }] -> x && y
if !alternate.as_bool_if_known().unwrap_or(true) {
return self.and(consequent);
}
if let Expression::Or { left: x, right: y } = &self.expression {
match &consequent.expression {
Expression::LogicalNot { operand } if x.eq(operand) => {
// [if x || y { !x } else { z }] -> [!x && y || !x && z] -> !x && (y || z)
return consequent.and(y.or(alternate));
}
Expression::ConditionalExpression {
condition,
consequent: a,
alternate: b,
} => {
// [if x || y { if x {a} else {b} } else {b}] -> if x {a} else {b}
if x.eq(condition) && b.eq(&alternate) {
return x.conditional_expression(a.clone(), alternate);
}
// [if x || y { if y {a} else {b} } else {b}] -> if y {a} else {b}
if y.eq(condition) && b.eq(&alternate) {
return y.conditional_expression(a.clone(), alternate);
}
// [if x || y { if x {a} else {b} } else {a}] -> if y {b} else {a}
if x.eq(condition) && a.eq(&alternate) {
return y.conditional_expression(b.clone(), alternate);
}
// [if x || y { if y {a} else {b} } else {a}] -> if x {b} else {a}
if y.eq(condition) && a.eq(&alternate) {
return x.conditional_expression(b.clone(), alternate);
}
}
_ => (),
}
}
// [if c { true join (c || d) } else { e }] -> c || e
if let Expression::Join { left, right } = &consequent.expression {
if left.as_bool_if_known().unwrap_or(false) {
if let Expression::Or { left, .. } = &right.expression {
if self.eq(left) {
return self.or(alternate);
}
}
}
}
// if self { consequent } else { alternate } implies self in the consequent and !self in the alternate
if !matches!(self.expression, Expression::Or { .. }) {
if consequent.expression_size <= k_limits::MAX_EXPRESSION_SIZE / 10 {
consequent = consequent.refine_with(self, 35);
}
if alternate.expression_size < k_limits::MAX_EXPRESSION_SIZE / 10 {
alternate = alternate.refine_with(¬_self, 35);
} else if let Expression::ConditionalExpression {
condition: c,
consequent: x,
alternate: y,
} = &alternate.expression
{
if let Expression::Or {
left: cl,
right: cr,
} = &c.expression
{
if self.eq(cl) {
alternate = cr.conditional_expression(x.clone(), y.clone());
} else if self.eq(cr) {
alternate = cl.conditional_expression(x.clone(), y.clone());
}
}
}
}
//[if x != 0 { x / c } else { 0 }] -> x / c
if alternate.is_zero() {
match &self.expression {
Expression::Ne { left: x1, right } if right.is_zero() => {
if let Expression::Div { left: x2, right: c } = &consequent.expression {
if x1.eq(x2) && matches!(&c.expression, Expression::CompileTimeConstant(..))
{
return x1.divide(c.clone());
}
}
}
_ => {}
}
}
if let Expression::ConditionalExpression {
condition: c2,
consequent: a,
alternate: b,
} = &consequent.expression
{
// [if self { if self { a } else { b } } else { c }] -> if self { a } else { b }
if self.eq(c2) {
return self.conditional_expression(a.clone(), alternate);
}
// [if self { if c2 { a } else { b } } else { b }] -> if condition && c2 { a } else { b }
if b.eq(&alternate) {
return self
.and(c2.clone())
.conditional_expression(a.clone(), alternate);
}
// [if self { if c2 { a } else { b } } else { a }] -> if self && !c2 { b } else { a }
if a.eq(&alternate) {
return self
.and(c2.logical_not())
.conditional_expression(b.clone(), alternate);
}
}
if let Expression::ConditionalExpression {
condition: c2,
consequent: a,
alternate: b,
} = &alternate.expression
{
// [if self { consequent } else { if self { a } else { b } }] -> if self { consequent } else { b }
if self.eq(c2) {
return self.conditional_expression(consequent, b.clone());
}
// [if self { a } else { if c2 { a } else { b } }] -> if self || c2 { a } else { b }
if a.eq(&consequent) {
return self
.or(c2.clone())
.conditional_expression(consequent, b.clone());
}
// [if x == y { consequent } else { if x == z { a } else { b } } ] -> switch x { y => consequent, z => a, _ => b }
if let (
Expression::Equals { left: x, right: y },
Expression::Equals { left: x1, right: z },
) = (&self.expression, &c2.expression)
{
if x.eq(x1) {
return x.switch(
vec![(y.clone(), consequent), (z.clone(), a.clone())],
b.clone(),
);
}
}
// [if y == x { consequent } else { if z == x { a } else { b } } ] -> switch x { y => consequent, z => a, _ => b }
if let (
Expression::Equals { left: y, right: x },
Expression::Equals { left: z, right: x1 },
) = (&self.expression, &c2.expression)
{
if x.eq(x1) {
return x.switch(
vec![(y.clone(), consequent), (z.clone(), a.clone())],
b.clone(),
);
}
}
// [if c { a } else { if c && d { .. } else { b } }] -> if c { a } else { b }
if let Expression::ConditionalExpression {
condition,
alternate: b,
..
} = &alternate.expression
{
if condition.implies(self) {
return self.conditional_expression(consequent, b.clone());
}
}
}
// [if x == y { consequent } else { switch x { z => a, _ => b } ] -> switch x { y => consequent, z => a, _ => b }
if let (
Expression::Equals { left: x, right: y },
Expression::Switch {
discriminator,
cases,
default,
},
) = (&self.expression, &alternate.expression)
{
if x.eq(discriminator) {
let mut cases = cases.clone();
cases.push((y.clone(), consequent));
return discriminator.switch(cases, default.clone());
}
}
// [if y == x { consequent } else { switch x { z => a, _ => b } ] -> switch x { y => consequent, z => a, _ => b }
if let (
Expression::Equals { left: y, right: x },
Expression::Switch {
discriminator,
cases,
default,
},
) = (&self.expression, &alternate.expression)
{
if x.eq(discriminator) {
let mut cases = cases.clone();
cases.push((y.clone(), consequent));
return discriminator.switch(cases, default.clone());
}
}
let mut expression_size = self
.expression_size
.saturating_add(consequent.expression_size)
.saturating_add(alternate.expression_size);
let mut consequent_type = consequent.expression.infer_type();
let mut alternate_type = alternate.expression.infer_type();
// In this context not primitive is expected to indicate that the value is a default value obtained
// via an unspecialized summary from a generic function.
if !consequent_type.is_primitive() && alternate_type.is_primitive() {
consequent = consequent.try_to_retype_as(alternate_type);
consequent_type = consequent.expression.infer_type();
} else if consequent_type.is_primitive() && !alternate_type.is_primitive() {
alternate = alternate.try_to_retype_as(consequent_type);
alternate_type = alternate.expression.infer_type();
};
if consequent_type != alternate_type
&& !(consequent_type.is_integer() && alternate_type.is_integer())
&& !(consequent.is_top() || alternate.is_top())
{
debug!(
"conditional with mismatched types {:?}: {:?} {:?}: {:?}",
consequent_type, consequent, alternate_type, alternate
);
return Rc::new(TOP);
}
let mut condition = self.clone();
if expression_size > k_limits::MAX_EXPRESSION_SIZE {
let condition_plus_consequent = self
.expression_size
.saturating_add(consequent.expression_size);
if condition_plus_consequent < k_limits::MAX_EXPRESSION_SIZE - 1 {
debug!("alternate abstracted: {:?}", alternate);
alternate = AbstractValue::make_from(alternate.expression.clone(), u64::MAX);
expression_size = condition_plus_consequent + 1;
} else {
let condition_plus_alternate = self
.expression_size
.saturating_add(alternate.expression_size);
if condition_plus_alternate < k_limits::MAX_EXPRESSION_SIZE - 1 {
debug!("consequent abstracted: {:?}", consequent);
consequent = AbstractValue::make_from(consequent.expression.clone(), u64::MAX);
expression_size = condition_plus_alternate + 1;
} else {
let consequent_plus_alternate = consequent
.expression_size
.saturating_add(alternate.expression_size);
if consequent_plus_alternate < k_limits::MAX_EXPRESSION_SIZE - 1 {
debug!("condition abstracted: {:?}", condition);
condition =
AbstractValue::make_from(condition.expression.clone(), u64::MAX);
expression_size = consequent_plus_alternate + 1;
}
}
}
}
if consequent.is_top() {
return consequent;
}
if alternate.is_top() {
return alternate;
}
AbstractValue::make_from(
ConditionalExpression {
condition,
consequent,
alternate,
},
expression_size,
)
}