Record equality between target and source for checking bounds

[kkjeer]

After the updated bounds context is used to check bounds for variables, there will be an issue with the way that expression equality is recorded. Certain kinds of expressions (expressions that create a new object or read memory via a pointer, such as "abc", *p, s->f, etc.) are not included in the set State.EquivExprs of expressions that produce the same value. This introduces proof failures when checking bounds. Consider:

void missing_equality(array_ptr<int> a : count(1)) {
  // s->f reads memory via a pointer
  // s->f is not included in State.EquivExprs
  // Bounds checking does not know that a and s->f produce the same value
  // The inferred bounds (s->f, s->f + 1) do not provably imply
  // the declared bounds (a, a + 1)
  a = s->f;
}

When checking that the inferred bounds of a imply the declared bounds of a, equality between a and s->f should be temporarily recorded so that the bounds checker is able to prove that the inferred bounds imply the declared bounds.