in checker/src/abstract_value.rs [5698:5799]
fn get_widened_subexpression(&self, path: &Rc<Path>) -> Option<Rc<AbstractValue>> {
match &self.expression {
Expression::Bottom | Expression::Top => None,
Expression::Add { left, right }
| Expression::AddOverflows { left, right, .. }
| Expression::And { left, right }
| Expression::BitAnd { left, right }
| Expression::BitOr { left, right }
| Expression::BitXor { left, right }
| Expression::Div { left, right }
| Expression::Equals { left, right }
| Expression::GreaterOrEqual { left, right }
| Expression::GreaterThan { left, right }
| Expression::IntrinsicBinary { left, right, .. }
| Expression::Join { left, right, .. }
| Expression::LessOrEqual { left, right }
| Expression::LessThan { left, right }
| Expression::Mul { left, right }
| Expression::MulOverflows { left, right, .. }
| Expression::Ne { left, right }
| Expression::Offset { left, right }
| Expression::Or { left, right }
| Expression::Rem { left, right }
| Expression::Shl { left, right }
| Expression::ShlOverflows { left, right, .. }
| Expression::Shr { left, right, .. }
| Expression::ShrOverflows { left, right, .. }
| Expression::Sub { left, right }
| Expression::SubOverflows { left, right, .. } => left
.get_widened_subexpression(path)
.or_else(|| right.get_widened_subexpression(path)),
Expression::BitNot { operand, .. }
| Expression::Cast { operand, .. }
| Expression::IntrinsicBitVectorUnary { operand, .. }
| Expression::IntrinsicFloatingPointUnary { operand, .. }
| Expression::Neg { operand }
| Expression::LogicalNot { operand }
| Expression::TaggedExpression { operand, .. }
| Expression::Transmute { operand, .. }
| Expression::UnknownTagCheck { operand, .. } => {
operand.get_widened_subexpression(path)
}
Expression::CompileTimeConstant(..) => None,
Expression::ConditionalExpression {
condition,
consequent,
alternate,
} => condition.get_widened_subexpression(path).or_else(|| {
consequent
.get_widened_subexpression(path)
.or_else(|| alternate.get_widened_subexpression(path))
}),
Expression::HeapBlock { .. } => None,
Expression::HeapBlockLayout {
length, alignment, ..
} => length
.get_widened_subexpression(path)
.or_else(|| alignment.get_widened_subexpression(path)),
Expression::Memcmp {
left,
right,
length,
} => left.get_widened_subexpression(path).or_else(|| {
right
.get_widened_subexpression(path)
.or_else(|| length.get_widened_subexpression(path))
}),
Expression::Reference(..) => None,
Expression::InitialParameterValue { .. } => None,
Expression::Switch {
discriminator,
cases,
default,
} => discriminator.get_widened_subexpression(path).or_else(|| {
default.get_widened_subexpression(path).or_else(|| {
cases.iter().find_map(|(case_val, result_val)| {
case_val
.get_widened_subexpression(path)
.or_else(|| result_val.get_widened_subexpression(path))
})
})
}),
Expression::UninterpretedCall {
callee,
arguments: args,
..
} => callee.get_widened_subexpression(path).or_else(|| {
args.iter()
.find_map(|arg| arg.get_widened_subexpression(path))
}),
Expression::UnknownModelField { .. } => None,
Expression::UnknownTagField { .. } => None,
Expression::Variable { .. } => None,
Expression::WidenedJoin { path: p, .. } => {
if p.eq(path) {
Some(self.clone())
} else {
None
}
}
}
}