in checker/src/abstract_value.rs [4814:4910]
fn subtract(&self, other: Rc<AbstractValue>) -> Rc<AbstractValue> {
match (&self.expression, &other.expression) {
// [0 - other] -> -other
(Expression::CompileTimeConstant(ConstantDomain::I128(0)), _)
| (Expression::CompileTimeConstant(ConstantDomain::U128(0)), _) => {
return other.negate();
}
// [self - 0] -> self
(_, Expression::CompileTimeConstant(ConstantDomain::I128(0)))
| (_, Expression::CompileTimeConstant(ConstantDomain::U128(0))) => {
return self.clone();
}
// [self - (- operand)] -> self + operand
(_, Expression::Neg { operand }) => {
return self.addition(operand.clone());
}
// [(c1 + x) - c2] -> (c1 - c2) + x
(Expression::Add { left: c1, right: x }, Expression::CompileTimeConstant(..))
if c1.is_compile_time_constant() =>
{
let c1_min_c2 = c1.subtract(other.clone());
if !c1_min_c2.is_bottom() {
return c1_min_c2.addition(x.clone());
}
}
(
Expression::Cast {
operand: left,
target_type: ExpressionType::Usize,
},
Expression::Cast {
operand: right,
target_type: ExpressionType::Usize,
},
) => {
// [(&x[y] as usize) - (&x as usize)] -> y
if let (
Expression::Offset {
left: base,
right: offset,
},
Expression::Reference(..),
) = (&left.expression, &right.expression)
{
if base.eq(right) {
return offset.clone();
}
}
// [(expr[y] as usize) - (expr as usize)] -> y
if let (
Expression::Variable {
path: left_path,
var_type: ExpressionType::ThinPointer,
},
Expression::Variable {
path: right_path,
var_type: ExpressionType::ThinPointer,
},
) = (&left.expression, &right.expression)
{
if let PathEnum::Offset { value } = &left_path.value {
if let Expression::Offset {
left: base,
right: offset,
} = &value.expression
{
if let PathEnum::Computed { value: rv }
| PathEnum::HeapBlock { value: rv }
| PathEnum::Offset { value: rv } = &right_path.value
{
if rv.eq(base) {
return offset.clone();
}
}
}
}
}
}
_ => {
// [x - x] -> 0 if x is an integer
if self.eq(&other) {
let t = self.expression.infer_type();
if t.is_unsigned_integer() {
return Rc::new(ConstantDomain::U128(0).into());
} else if t.is_signed_integer() {
return Rc::new(ConstantDomain::I128(0).into());
}
}
}
}
self.try_to_constant_fold_and_distribute_binary_op(
other,
ConstantDomain::sub,
Self::subtract,
|l, r| AbstractValue::make_binary(l, r, |left, right| Expression::Sub { left, right }),
)
}