Simple normalizations for +1/-1 bounds scenarios

[kkjeer]

This PR implements some transformation functions to enable the bounds checker to validate some additional bounds.

These normalization functions attempt to express a given upper bound expression as ((E1 + E2) +/- A) +/- B, where E1 has pointer type and A and B are integer constants. The bounds checker can use the variable part E1 + E2 and the constant part A + B to compare bounds expressions.

This enables the bounds checker to validate certain bounds that can arise in bounds widening scenarios. For example:

void f(_Nt_array_ptr<char> p : count(len), unsigned int len) {
  if (*(p + len)) {
    ++len;
  }
}

The bounds checker can express the inferred upper bound (p + (len - 1)) + 1) as ((p + len) - 1) + 1and extract the variable partp + lenand the constant part-1 + 1 == 0. The bounds checker can then use these to prove that the inferred upper bound is equivalent to the declared upper bound p + len`.

[sulekhark]

LGTM! Thank you!

[mgrang]

LGTM.