Allowing bounds of function-scope static variable to depend on function-scope non-static variable is unsound

[mattmccutchen-cci]

One more soundness issue that I forgot to file earlier (still no urgency from CCI):

The compiler allows the bounds of a static variable local to a function to depend on non-static variables local to the function. This is unsound because the static variable persists across calls but the non-static variables do not, so the static variable may be read with a different bounds expression than it was written. The obligatory example code that generates a segmentation fault (which seems to be becoming the Checked C analogue of alert('XSS'); 😁):

#pragma CHECKED_SCOPE on

int foo(_Array_ptr<int> p : count(n), int n) {
  static _Array_ptr<int> sp : count(n) = 0;
  if (p != 0) {
    sp = p;
  }
  return sp[n - 1];
}

int main(int argc, _Nt_array_ptr<_Nt_array_ptr<char>> argv : count(argc)) {
  int x _Checked[1];
  foo(x, 1);
  foo(0, 123456789);
  return 0;
}

I always thought function-scope static variables were a weird C language feature, and now I see that they are a gratuitous trap for program analyses too. But we're stuck with the C language as it is now. 🙁