in checker/src/abstract_value.rs [5412:5507]
fn get_as_interval(&self) -> IntervalDomain {
match &self.expression {
Expression::Top => interval_domain::BOTTOM,
Expression::Add { left, right } => left.get_as_interval().add(&right.get_as_interval()),
Expression::BitAnd { left, .. } => {
if let Expression::CompileTimeConstant(ConstantDomain::U128(v)) = left.expression {
if v < (i128::MAX as u128) && (v + 1).is_power_of_two() {
let lower: IntervalDomain = 0u128.into();
let upper: IntervalDomain = v.into();
return lower.widen(&upper);
}
}
interval_domain::BOTTOM
}
Expression::Cast {
operand,
target_type,
} => operand
.get_as_interval()
.intersect(&IntervalDomain::from(*target_type)),
Expression::CompileTimeConstant(ConstantDomain::I128(val)) => (*val).into(),
Expression::CompileTimeConstant(ConstantDomain::U128(val)) => (*val).into(),
Expression::ConditionalExpression {
consequent,
alternate,
..
} => consequent
.get_as_interval()
.widen(&alternate.get_as_interval()),
Expression::Div { left, right } => left.get_as_interval().div(&right.get_as_interval()),
Expression::IntrinsicBitVectorUnary {
name, bit_length, ..
} => match name {
KnownNames::StdIntrinsicsCtlz
| KnownNames::StdIntrinsicsCtlzNonzero
| KnownNames::StdIntrinsicsCtpop
| KnownNames::StdIntrinsicsCttz
| KnownNames::StdIntrinsicsCttzNonzero => {
let min_value: IntervalDomain = IntervalDomain::from(0u128);
let max_value = IntervalDomain::from(*bit_length as u128);
min_value.widen(&max_value)
}
_ => interval_domain::BOTTOM,
},
Expression::Join { left, right, .. } => {
left.get_as_interval().widen(&right.get_as_interval())
}
Expression::Mul { left, right } => left.get_as_interval().mul(&right.get_as_interval()),
Expression::Neg { operand } => operand.get_as_interval().neg(),
Expression::Rem { left, right } => left.get_as_interval().rem(&right.get_as_interval()),
Expression::Sub { left, right } => left.get_as_interval().sub(&right.get_as_interval()),
Expression::Switch { cases, default, .. } => cases
.iter()
.fold(default.get_as_interval(), |acc, (_, result)| {
acc.widen(&result.get_as_interval())
}),
Expression::TaggedExpression { operand, .. } => operand.get_as_interval(),
Expression::Variable { var_type, .. } => IntervalDomain::from(*var_type),
Expression::WidenedJoin { operand, .. } => {
let interval = operand.get_as_interval();
if interval.is_bottom() {
return interval;
}
if let Expression::Join { left, .. } = &operand.expression {
let left_interval = left.get_as_interval();
if left_interval.is_bottom() {
return interval_domain::BOTTOM;
}
match (left_interval.lower_bound(), interval.lower_bound()) {
(Some(llb), Some(lb)) if llb == lb => {
// The lower bound is finite and does not change as a result of the fixed
// point computation, so we can keep it, but we widen the upper bound.
let target_type = operand.expression.infer_type();
return interval
.remove_upper_bound()
.intersect(&IntervalDomain::from(target_type));
}
_ => (),
}
match (left_interval.upper_bound(), interval.upper_bound()) {
(Some(lub), Some(ub)) if lub == ub => {
// The upper bound is finite and does not change as a result of the fixed
// point computation, so we can keep it, but we widen the lower bound.
let target_type = operand.expression.infer_type();
return interval
.remove_lower_bound()
.intersect(&IntervalDomain::from(target_type));
}
_ => (),
}
}
interval
}
_ => interval_domain::BOTTOM,
}
}