Document Number: N3025

Date: 2022-July-17

Authors: Hubert Tong, Martin Uecker, Bill Homer, Tom MacDonald (redactor)

Acknowledgement: Ralf Jung for raising this issue: https://www.ralfj.de/blog/2022/04/11/provenance-exposed.html

Introduction

An issue with the formal definition of restrict has been identified. Below is a discussion of the problem, followed by a proposed wording change to the restrict specification, and finally some examples that demonstrate why the changes address the problems.

Since C23 is expected to finish before this issue is resolved, this proposal is not intended to be considered for C23. This proposal involves a wording change to the existing formal definition of restrict.

There is another proposal that will be introduced in a separate WG14 document. That proposal introduces a provenance-style solution. Since that involves a complete rewrite of the formal definition of restrict, it is anticipated that it will be more complicated (but possibly a better fit) than this proposal. The recommendation is that WG14 consider the following options:

• First, incorporate some version of this proposal into the C Standard at the appropriate time.


• Second, determine if the provenance based solution is a better, but possibly a longer term goal. That way the C Standard has a fix in the shorter term, and a plan to improve the formal definition in the longer term.


• After reviewing both proposals, only consider including a proposed provenance-based solution.


• After reviewing both proposals, only consider including this proposed change to the existing wording.

Defect Description

Some wording changes are needed for the formal definition of restrict to address an identified defect. The wording changes involve the based on concept defined in the current formal definition. The concept of directly based on is also introduced because based on now has a recursive definition, and it seems clearer if the start of the recursion is identified.

Here is the executive summary of the proposed changes:

• The "address of a copy" criterion for a given pointer expression to be based on a restricted pointer is now considered only during the evaluation of that expression. In particular, there is no longer a consideration of side effects in the same, or a subsequent, expression from implicitly storing that address into the restricted pointer object.


• If an expression is at once based on two different restricted pointers associated with the same block then the behavior is undefined.


• A limitation is placed on the value of pointer expressions based on a restricted pointer. If that value is cast to a non-pointer type or stored in an object through some means other than assignment/initialization the resulting value (and any value derived from it) ceases to be based on the restricted pointer. This is an area where more debate is needed as it is not clear that a consensus exists.


• New words are added to clarify how bit-field accesses are analyzed. This new wording is added because the address of a bit-field is not available, but there is an addressable storage unit that contains it. This storage unit may also contain other bit-fields. Additional scrutiny by reviewers is recommended here.

This proposal attempts to clarify the issues, discuss what needs to change, and explain the new concepts that are intended to correct the issues. Finally, the intent is that these changes avoid creating new complexities for existing compilers. For consistency purposes, a goal of based on is that its definition should not affect compile time transformations like evaluation of conditions, forward substitution, introduction of intermediate variables, or other transformations a compiler may wish to make prior to doing alias analysis. It is still viewed as important that any aliasing information provided by the keyword restrict in a strictly conforming program can be ignored by a compiler, and the program is still strictly conforming.

The following explanations do not always use formal specification wording associated with restrict, but rather use a slightly less formal but (hopefully) a more understandable explanation. The exact wording changes to the current specification are included later on.

  // Example 1:

  int f(int * restrict p, int *q) {
    int *r = p;  // sequence point

    if (r == p) {
      r = q;
    }

    *r = 13; // here let E denote &*r == r
    *p = 42;

    return *r;
  }

On entry to the function, q is not based on p, and the intent is that after its assignment to r, r and therefore E are not based on p. But, if the value of p is modified to point to a 'copy' at the identified sequence point, then the value of E changes, because the assignment r = q would be skipped. Therefore, the unintended result of the current definition is that r is based on p. This means that the stores into *r and *p and the evaluation of *r in the return statement must be done in order, as they would if restrict was not present.

The problem is not that the usage of restrict in this example is ineffective, but that it conflicts with a goal that "based on" semantics should not be affected by compile time transformations compilers may wish to make prior to doing alias analysis. The specification for based on should not get in the compiler's way.

For Example 1, if the compiler evaluates r == p as true and converts the if statement to an unconditional assignment, then in the transformed program r is not based on p. The inconsistency with the original version is the problem.

One way to address this problem is to change the specification of based on to require that the expression must not only change, but change to point into the copy. In Example 1, the value of r would change, but would not refer to the copy, if the address of a copy were stored into p at the identified sequence point. So, with this new criterion, r is not based on p, and we now have the desired consistency for this example.

But the above change, by itself, is not yet enough to guarantee consistency in other cases, as the next example shows.

// Example 2:

int f(int * restrict p, int *q) {
  int *a = &p[p-q];  // If 'p' points to a copy here
                     // then the value of 'p-q' no
                     // longer has well defined behavior

  *a = 13;  // here let E denote &*a == a


  p[1] = 42;

  return *a;
}

extern int printf(const char *, ...);

int z[100];

int main(void) {
  int x = f(z+1, z);
  printf("x=%d\n", x);
}

The intent is that a is based on p because it is assigned a value that differs from p only by an offset within the object to which p refers. But because that offset happens to be expressed as a difference between p and q within the expression that is assigned to a, there is no sequence point at which storing into p the address of a copy of the object to which it refers would cause a to have a well-defined value that also points into that copy.

It follows that the behavior of the call to f() in main() has undefined behavior because *a and p[1] refer to the same object, but a is not based on p.

Now consider changing Example 2 by introducing an intermediate variable to hold the offset and an additional sequence point:

   int k = p-q; int *a = &p[k];

Now the new sequence point can be used to establish that a is based on p and so the call to f() does not have undefined behavior.

Thus, the consistency goal is not met.

The source of the problem is in modifying P to point to a copy by storing the address of the copy into P at a previous sequence point. The proposed change is to consider modifying the value of P, rather than the value in P, and specifically to consider the effect of replacing the values of some but not all references to P in the expression under consideration.

In Example 2, this allows the conclusion that a is directly based on p because replacing the value of only the first instance of p in the expression:

   &p[p-q]

  a = &p[p-q]; => int * r = p; a = &r[r-q];
  // a is directly based on r and r is directly based on p, so a is based on p.

  a = &p[p-q];  =>  int * r = (X ? p : p+1); a = &r[r-q];
  // see that r is directly based on p requires replacing both instances of p

  // Example 1:

  int f(int * restrict p, int *q) {
    // #1 sequence point after arguments have been evaluated
    int *r = p;  // #2 sequence point after initialization

    if (r == p) {  // #3 sequence point after if expression evaluation
      r = q;  // #4 sequence point at end of statement
    }  // #5 sequence point at end of statement

    *r = 13; // here let E denote &*r == r
    *p = 42;

    return *r;
  }

// Example 2:

int f(int * restrict p, int *q) {
  int *a = &p[p-q];  // 'a' is directly based on 'p' because replacing the
                     // value of only the first instance of p in &a[p-q]
                     // with the value of a copy causes 'a' to be well-defined

  *a = 13;  // here let E denote &*a == a


  p[1] = 42;

  return *a;
}

extern int printf(const char *, ...);

int z[100];

int main(void) {
  int x = f(z+1, z);
  printf("x=%d\n", x);
}

// Example 3

#include <stdint.h>

void f(int * restrict p) {
  *p = 13;
  uintptr_t i = (uintptr_t) p;  // cast p to an integer, i is not based on p
  int *q = (int *) i;           // cast back to a pointer
  *q == 14;                     // q is not based on p

  return *p + *q;
}

// Example 4

#include <stdint.h>

int f(int * restrict p, uintptr_t mask) {
  uintptr_t u1 = mask & (uintptr_t)p;
  uintptr_t u2 = (~mask) & (uintptr_t)p;
  *p =42;
  *(int *)(u1 | u2) = 13; // E is (int *)(u1 | u2)
  return *p;
}