Bounds context: update after assignments [3/n]

[kkjeer]

This PR updates the context mapping variable declarations to their current known bounds after an assignment to a variable.

Context:

This work is part of the soundness of bounds declaration checking. After this PR is merged, the next step is to validate that each variable declaration's observed bounds implies the variable's declared bounds after checking a top-level CFG statement.

Notable changes:

• Modify UpdateAfterAssignment to update the observed bounds context after an assignment to a variable
• Modify UpdateAfterAssignment to return updated rvalue bounds for the source of an assignment
• Use the modified source bounds as the rvalue bounds of an assignment or increment/decrement operator. For example, the rvalue bounds of the assignment p = p + 2, if p has declared bounds (p, p + 1) will be (p - 2, p - 2 + 1), since the original value of p is p - 2.
• Check that the modified source bounds of an increment/decrement operator on a variable imply the declared bounds for the variable. For example, if p has declared bounds (p, p + 1), after p++, check that the updated result bounds (p - 1, p - 1 + 1) imply the declared bounds (p, p + 1).
• Account for equality information from nested assignments when checking bounds declarations at assignments, initializers, and call arguments.

Implications for pointer arithmetic:

One important change in this PR is that the source bounds used to check an assignment are the updated observed bounds. This means that pointer arithmetic on variables with declared bounds will frequently result in bounds warnings or errors.

For example, these assignments will all result in a warning:

• cannot prove declared bounds for p are valid after assignment
• (expanded) declared bounds: bounds(p, p + i)
• (expanded) inferred bounds: bounds(p - 1, p - 1 + i)

void f(array_ptr<int> p : bounds(p, p + i), int i) {
  // Original value of p: p - 1
  // Updated source bounds: (p - 1, (p - 1) + i)
  // Updated source bounds are also the result bounds for the assignment
  p = p + 1;
  p += 1;
  p++;
}

These assignments will all result in an error:

• declared bounds for p are invalid after assignment
• (expanded) declared bounds are bounds(p, p)
• (expanded) inferred bounds are bounds(p - 1, p - 1)
• source bounds are an empty range
• destination upper bound is above source upper bound

void f(array_ptr<int> p : bounds(p, p)) {
  // Original value of p: p - 1
  // Updated source bounds: (p - 1, p - 1)
  // Updated source bounds are also the result bounds for the assignment
  p = p + 1;
  p += 1;
  p++;
}

Testing:

• Updated bounds-context.c to test updating observed bounds
• Modified checked-c tests to account for new warnings and errors when checking the updated source bounds of an assignment (checkedc PR 402)
• Passed manual testing on Windows X64
• Passed automated testing on Windows/Linux

[dtarditi]

Overall, looks good. I have some suggestions for comments and a few questions.

[dtarditi]

Instead of duplicating the explanation in the comment from CheckBoundsDeclAtAssignment, could you just reference back to the explanation in that comment?

[dtarditi]

Should buf be in the observed bound context before the declaration?

[dtarditi]

I found this comment and code confusing. Are you overloading creation of the integer literal to account for the different bitwidth of integer literals required for integer arithmetic vs. pointer arithmetic involving a literal. For pointer arithmetic, if the pointee type is an integer type, why would you make the type of the integer literal match the pointee type? An example, for "char *", it is valid to add an integer larger than a char to the pointer.

[dtarditi]

Overall, this change looks great! Thank you.

There is a follow-up issue that can be addressed in a future change. I believe the observed bounds for local/global array variables aren't correct right now. It is based on the declared bounds. The observed bounds should be based on the (complete) type of the array variable. Could you open an issue about this?

[dtarditi]

The observed bounds declaration for an array variable should be based on the declared type of the array variable. It seems to be based on the declared bounds declaration here, which is incorrect. I checked the code in SemaBounds.cpp. Handling of this case seems to be missing, and there is a even a "TODO" that hints at this.

Could you open a new issue for this case? I think this should be handled as a separate change. You should not try to fix it in this PR. There's no reason for this to block further.

[kkjeer]

Created #862 to track this.

[dtarditi]

I believe the observed bounds need to be set in this case. Please open an issue to track this, as a separate follow-up. Addressing this case I believe will handled the TODO that is just above (at line 3273).