fn subtract()

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 }),
        )
    }