bounds expressions not respected by aliases (core dump)

[mwhicks1]

The following program type checks in checked mode, and yet it will core dump because it permits changing a bounds expression via a pointer. This seems like a serious problem, since it's at the heart of what the type system will/will not support.

#include <stdlib_checked.h>
#include <stdio_checked.h>

#pragma BOUNDS_CHECKED ON

struct p {
  _Array_ptr<char> buf : count(len);
  unsigned int len;
};

void foo(_Ptr<struct p> ptr) {
  unsigned int i;
  for (int i=0; i<ptr->len; i++) {
    ptr->buf[i] = 'a';
    _Unchecked { printf("Assigning index %d an %c\n",i,'a'); }
    ptr->len++;
  }
}

int main(int argc, _Nt_array_ptr<char> argv[] : count(argc)) {
  _Ptr<struct p> p = 0;
  p = malloc(sizeof(struct p));
  p->buf = malloc(10);
  p->len = 10;
  foo(p);
  return 0;
}

[lenary]

My understanding is we want to allow the programmer to modify len-like members of structs like this, say if they realloc the underlying buffer.

Here, the programmer has got the invariant wrong. It is not the case that ptr->buf + ptr->len always represents the end of the buffer at ptr->buf.

For main, the allocation to p, p->buf and p->len should all be correct according to the static analysis we wish to do, though you may need to use a bundled block around the assignments to p->buf and p->len as between these two statements, the invariant is not held.

I think @dtarditi does want to do some static analysis of modifications to fields referenced within bounds expressions, but I'm not sure exactly what that entails. I do know that we are going to extend the aliasing rules to prevent odd aliasing of bounds-referenced fields, so that we can understand everywhere they're updated, but I think these are aliasing /assumptions/ and not things we can always enforce statically in the general case.

[dtarditi]

When the static checking of bounds declarations is fully implemented, this will fall the checking. Chapter 6 of the spec describes how we'll check struct expressions. It is not implemented. There is still a lot of implementation work to do in the compiler to do on checking bound declarations (subsumption checking). We decided to prioritize having runtime checking for null-terminated pointers above the subsumption checking.

[mwhicks1]

As I said in my prior comment: We need to be able to draw a box around what we do/do not check now if the reviewers are going to understand our contribution. I don't see why dealing with overwriting a length field is "subsumption checking." We might just want to talk through this in real time.