Handling strlen in bounds widening of null terminated arrays

Currently, we have a framework to widen bounds for null-terminated arrays pointers. If an _Nt_array_ptr is dereferenced at the current upper bound then we can widen its bounds by 1. For example,

_Nt_array_ptr<T> p : bounds(p, p) = "";
if (*p) // Widen bounds by 1. New bounds for p : bounds(p, p + 1)

Now, we want to support cases where the length of an _Nt_array_ptr is obtained using calls to strlen.

int x = strlen(p); // New bounds for p : bounds(p, p + x)
if (*(p + x)) // Widen bounds by 1. New bounds for p : bounds(p, p + x + 1)
...
...
if (*(p + x + 2)) // Error: Out-of-bounds memory access.

Design for handling strlen in bounds widening We will support strlen in bounds widening if the following conditions are satisfied:

1. We will only support calls to strlen whose return value is assigned to a variable, like int x = strlen(p). This means we will not consider calls like if (i < strlen(p)) in bounds widening.

2. When using strlen with an _Nt_array_ptr the user should redeclare the bounds of the _Nt_array_ptr using a where clause. For example, int x = strlen(p) where p : bounds(p, p + x). If a strlen call is not annotated with a where clause redeclaring the bounds then we will not consider that strlen in bounds widening.

3. The bounds redeclared using strlen with a where clause only remain valid inside the block where the redeclaration happens. For example,

_Nt_array_ptr<T> p : bounds(p, p); // Bounds for p : bounds(p, p)
if (some condition) {
  int x = strlen(p) where p : bounds(p, p + x); // New bounds for p : bounds(p, p + x)
}

// Outside the if condition we fallback to the declared bounds. Thus bounds for p : bounds(p, p)

4. In a particular block, the bounds redeclared by the most recent strlen with a where clause will override all previous bounds redeclarations. For example,

int x = strlen(p) where p : bounds(p, p + x); // Bounds for p : bounds(p, p + x)
...
...
int y = strlen(p) where p : bounds(p, p + y); // New bounds for p : bounds(p, p + y)

5. At join points if there are two conflicting/different redeclarations of bounds using strlen with where clause we will fallback to the declared bounds along with a warning. For example,

int x, y;
if (some condition) {
  x = strlen(p) where p : bounds(p, p + x);
  goto L1;
}
else {
  y = strlen(p) where p : bounds(p, p + y);
  goto L1;
}

L1: // At this point we have two conflicting redeclared bounds for p: bounds(p, p + x) and bounds(p, p + y).
    // So we reset the bounds here to the declared bounds and issue a warning.