Local variable bounds dependent on global variable can be invalidated by function call (unsound)

[mattmccutchen-cci]

Checked C seems to allow the bounds of a variable p local to a function f to depend on a global variable x. If f calls a function that changes x, then p is not consistent with the new value of x, which can lead to a spatial safety violation. Example:

#pragma CHECKED_SCOPE on

#include <stdlib.h>

size_t global_len;

void change_global_len(void) {
  global_len = 100000000;
}

int main(void) {
  global_len = 100;
  _Array_ptr<char> local_ptr : count(global_len) = malloc<char>(global_len);
  // Doing this directly would cause a compile error.
  //global_len = 100000000;
  // No error, and local_ptr no longer meets its declared bound.
  change_global_len();
  for (size_t i = 0; i < global_len; i++)
    local_ptr[i]++;  // SIGSEGV
  return 0;
}

[dtarditi]

The Checked C specification does not allow this. See Section 3.6.2 of version 0.9 of the spec for the discussion. This check is not enforced by the Checked C compiler, however.

I believe the logic is there, but we turned it off because one of our early benchmark programs from the Olden benchmark site (em3d) contained local variables with bounds that are declared global variables. The fix is to turn the check back on and change the Checked C version of the benchmark program.