fn addition()

in checker/src/abstract_value.rs [947:1037]


    fn addition(&self, other: Rc<AbstractValue>) -> Rc<AbstractValue> {
        // [x + c] -> c + x
        if !self.is_compile_time_constant() && other.is_compile_time_constant() {
            // Normalize binary expressions so that if only one of the operands is a constant, it is
            // always the left operand.
            return other.addition(self.clone());
        }
        if let Expression::CompileTimeConstant(c1) = &self.expression {
            // [0 + x] -> x
            if c1.is_zero() {
                return other;
            }
            // [c1 + (c2 + x)] -> c3 + x where c3 = c1 + c2
            if let Expression::Add { left, right: x } = &other.expression {
                if let Expression::CompileTimeConstant(c2) = &left.expression {
                    let c3 = c1.add(c2);
                    if c3 != ConstantDomain::Bottom {
                        let c3val: Rc<AbstractValue> = Rc::new(c3.into());
                        return c3val.addition(x.clone());
                    }
                }
            }
        }

        // [x + (-y)] -> x - y
        if let Expression::Neg { operand } = &other.expression {
            return self.subtract(operand.clone());
        }
        // [(-x) + y] -> y - x
        if let Expression::Neg { operand } = &self.expression {
            return other.subtract(operand.clone());
        }
        // [x + x] -> 2 * x
        if self.eq(&other) {
            let t = self.expression.infer_type();
            if t.is_unsigned_integer() {
                let two: Rc<AbstractValue> = Rc::new(ConstantDomain::U128(2).into());
                return two.multiply(other);
            } else if t.is_signed_integer() {
                let two: Rc<AbstractValue> = Rc::new(ConstantDomain::I128(2).into());
                return two.multiply(other);
            }
        }

        // [x + (y - x)] -> y
        if let Expression::Sub { left: y, right: x } = &other.expression {
            if self.eq(x) {
                return y.clone();
            }
        }

        // [(c * x) + (c * y)] -> c * (x + y)
        if let (
            Expression::Mul {
                left: cv1,
                right: x,
            },
            Expression::Mul {
                left: cv2,
                right: y,
            },
        ) = (&self.expression, &other.expression)
        {
            if let (Expression::CompileTimeConstant(c1), Expression::CompileTimeConstant(c2)) =
                (&cv1.expression, &cv2.expression)
            {
                if !c1.eq(c2) {
                    let right = x.addition(y.clone());
                    // Don't use multiply because we don't want to simplify this
                    let expression_size = cv1
                        .expression_size
                        .saturating_add(right.expression_size)
                        .saturating_add(1);
                    return AbstractValue::make_from(
                        Expression::Mul {
                            left: cv1.clone(),
                            right,
                        },
                        expression_size,
                    );
                }
            }
        }

        self.try_to_constant_fold_and_distribute_binary_op(
            other,
            ConstantDomain::add,
            Self::addition,
            |l, r| AbstractValue::make_binary(l, r, |left, right| Expression::Add { left, right }),
        )
    }