Provenance-Style Specification of restrict

Document Number: N3058

Date: 2022-October-25

Authors: Bill Homer, Tom MacDonald (redactor)

Change History Log

  1. 2022-August-4, Original

  2. 2022-October-25, In rules 11 and 12 of the formal definition of restrict, replace "is assigned to" with "is stored in" to allow for initialization, memcpy, etc.

  3. 2022-October-26, Minor improvements to comments in examples B, E, and 2.

  4. 2022-October-26, Fix typo in Example E where c should be y.

Reference Documents: N3005 A Provenance-aware Memory Object Model for C, N3025 Defect With Wording Of restrict Specification

Introduction

Document N3025 addresses a defect with the formal specification of the restrict keyword. That document states that another approach is going to be explored that uses a provenance-style to describe the formal definition. This document provides an approach to a provenance-style definition, along with examples and explanations.

A Technical Specification (TS) N3005 provides a provenance-aware memory object model that is expected to be added to the C Standard at some future date. Document N3005 is related to the specification described below that defines the behavior of restrict-qualified pointers. Both specifications address issues concerning pointer aliasing and when compilers can justify optimizations.

The current specification in the C Standard defines the concept of a pointer expression being "based on" a restricted pointer. The "based on" concept provides information about when different pointer expressions can reference the same object without causing undefined behavior. That approach avoids spelling out the details of how "based on" propagates through expressions. Some defects have been identified with the current specification and N3025 identifies the changes needed to address these defects as well as clarifying how bit-fields are handled.

Given the existing TS effort, there appears to be a better way that no longer avoids identifying how "based on" propagates through expressions. This approach seems more straightforward and is spelled out in this document.

The intent of this specification is for all current well-defined programs that use restrict to remain well-defined, and that translators are still free to ignore any and all implications of uses of restrict. The burden is on the user to write a well-defined program, and not on the compiler to prove that uses of restrict are strictly conforming.

Finally, harmonizing the TS and this specification is viewed as beneficial.

Formal Definition of restrict

  1. Let D be a declaration of an ordinary identifier that provides a means of designating an object P as a restrict-qualified pointer to type T.

  2. If D appears inside a block and does not have storage class extern, let B denote the block. If D appears in the list of parameter declarations of a function definition, let B denote the associated block. Otherwise, let B denote the block of main (or the block of whatever function is called at program startup in a freestanding environment).

  3. During an execution of B, both P and a labeled set of objects, termed a "restricted target set" with label RTS(&P, B), are said to be associated with B. In the label, B denotes a particular execution of the block, and the address &P is determined when P is first designated as a restricted pointer, and is invariant during the execution of B. The set is initially empty, and is determined during the course of execution of B as follows.

  4. The value of a pointer expression E is said to be "directly based on" an object Q with pointer type if E is simply a reference to Q, or if the value of E is derived from the value of Q by a sequence of one or more operations that are semantically equivalent to adding or subtracting an integer value, or casting to a pointer type.

  5. The value of a pointer expression E is said to be "based on" an object Q with pointer type if E is directly based on Q, or if E is directly based on another pointer object Q1 that contains the value of an expression that is based on Q. [1]

  6. Accessing or modifying the value of an object designated by dereferencing the value of P, or the value of a pointer expression E based on P, causes that object to be added to the set RTS(&P,B). Here "designated by dereferencing E" includes expressions of the forms *E, E[n], E->m, and semantically equivalent expressions. If that object is a member of an aggregate, only the object itself is added, and not the entire aggregate. [2]

  7. Accessing or modifying the value of an object in a way that does not add it to the RTS of any restricted pointer associated with B causes the object to be added to a special RTS labeled RTS(NULL,B).

  8. The behavior is undefined if any object belongs to more than one RTS associated with B, and the object is modified during the execution of B. More generally, the behavior is undefined if an object from one RTS associated with B overlaps an object from a different RTS, and either of the objects is modified during the execution of B.

  9. The behavior is undefined if the type T of the restricted pointer P is const-qualified and any object in RTS(&P,B) is modified during the execution of B.

  10. For the purpose of this section, if any object in RTS(&P,B) is modified during the execution of B, then the pointer object P is also considered to be modified.

  11. During an execution of B, the behavior is undefined if the value of a pointer expression based on P is stored in a restricted pointer object P2 different from P that is also associated with block B.

  12. During an execution of B, the behavior is undefined if the value of a pointer expression based on P is stored in another restricted pointer object P2 that is associated with a different block B2, and the execution of B2 began before the execution of B and continues after the execution of B ends.

  13. When an execution of B ends, all RTS sets associated with that execution of B are deleted.

  14. A translator is free to ignore any or all aliasing implications of uses of restrict.

[1]The value returned by realloc is not considered to be based on any pointer object.

[2] For example, E[n1][n2] when E[n1] is an array, or E->m1.m2 when E->m1 is a struct.


Comparison with provenance

The "based on" relation can be expressed in terms of PNVI-plain provenance, as specified in the TS, except that a corresponding provenance is never recreated at integer-to-pointer cast points. This can then be viewed as a new model called PNVI-strict. There are pros and cons involved when choosing a new PVNI model instead of one of the currently defined PVNI-* models. Mostly the trade offs involve the behavior when integers are cast to pointers and vice versa. The goal is to create a well defined specification that meets the needs of both users and developers.

The value of a pointer expression E is said to be "directly based on" an object Q with a pointer type if E is simply a reference to Q, or if the value of E is derived from the value of Q by a sequence of one or more operations that are guaranteed to preserve the provenance of Q.

An RTS may be characterized as an "effective storage instance", but with a lifetime, associated with a block, that may be less than the storage instance of objects it contains, and that is determined dynamically by the execution of the block, rather than being created in its entirety upon encountering a declaration or an allocation.

It is possible to more closely match the PVNI-plain model specified in the TS by saying something like, if the result of an integer to pointer cast is equal to P, or is equal to an address within an object in RTS(&P,B), then that result is considered to be based on P. This change introduces some complications and it isn't clear that there are compelling use cases where there is not a straightforward alternative that can be expressed without using these casts. This is an area that is open to more debate.

Examples

Several restricted pointer examples are presented below to demonstrate how this specification can be used to analyze aliasing. Examples 1, 2, and 3 are examples from document N3025 and are also presented here to demonstrate how this specification applies, and that the resulting semantics are the same as the current C Standard.

In each example, any number inside parentheses identifies a section in the formal definition that is key to explaining the formulation. For example, The notation <D,P,T> refers to <declaration D, object P, type T> as described in (1).


  // Example A:

  void f1(int * restrict q1, int n) {  // Begin Block B
    extern int c[];

    // (1) <D,P,T> is <int * restrict q1, q1, int>

    if (n < 1) return;

    q1[0]++;   // (6) object q1[0] added to set RTS(&q1,B)
    c[0]--;    // (7) object c[0] added to set RTS(NULL,B)
               // (8) UB if q1 == c because &q1 != NULL and B == B
  }  // End Block B


  // Example B:

  void f2(int n, int q2[restrict n][n]) {  // Begin Block B
    // (1) <D,P,T> is <int q2[restrict n][n], q2, int[]>

    if (n < 0) return;

    extern int a[];
    
    q2[0][0] = 13;     // (6) object q2[0][0] added to set RTS(&q2,B)
    a[0] = 42;         // (7) object a[0] added to RTS(NULL,B)
                       // (8) UB if a == q2[0]
                       //     because &q2 != NULL and B == B
  }  // End Block B


  // Example C:
  // Here the comments in functions f0(), f1(), and f2() are tailored to
  // analyzing their calls in main().  The intent here is to illustrate
  // that semantics of an individual 'restrict' qualifier is "shallow" when
  // a type involves multiple pointer derivations, but multiple qualifiers
  // can combine to provide "deep" semantics (and the point of rule 10 is
  // to make the combination effective).

  int f0(int ** restrict p,
         int ** restrict q) {  // Begin Block B
    p[0][0] = 13;   // (7) object p[0][0] added to RTS(NULL,B)
                    //     because p[0] is not restrict-qualified
    q[0][0] = 42;   // (7) object q[0][0] added to RTS(NULL,B)
                    //     because q[0] is not restrict-qualified
                    // no UB because p[0] and q[0] are not modified
                    // and p[0][0] and q[0][0] belong to the same RTS
                    // (independently of whether p == q)
    return p[0][0];
  }  // End Block B

  int f1(int * restrict *p,
         int * restrict *q) {  // Begin Block B
  // neither p nor q are restricted pointers

    p[0][0] = 13;     // (6) object p[0][0] added to set RTS(&p[0],B)
                      // (10) object p[0] is considered modified
                      // (7) object p[0] added to set RTS(NULL,B)

    q[0][0] = 42;     // (6) object q[0][0] added to set RTS(&q[0],B)
                      // (10) object q[0] is considered modified
                      // (7) object q[0] added to set RTS(NULL,B)

    return p[0][0];   // no UB because p[0] and q[0] belong to the same RTS
                      // and if p==q, then p[0][0] and q[0][0] are same object
                      // but RTS(&p[0],B) and RTS(&q[0],B) are the same RTS.
  }  // End Block B

  int f2(int * restrict * restrict p,
        int * restrict * restrict q) {  // Begin Block B
  // (1)<D,P,T> is <int * restrict * restrict p, p, int * restrict>
  // (1)<D,P,T> is <int * restrict * restrict q, q, int * restrict>

    p[0][0] = 13;  // (6) object p[0] added to set RTS(&p,B) and
                   // (10) object p[0] is considered modified
    q[0][0] = 42;  // (6) object q[0] added to RTS(&q,B) and
                   // (10) object q[0] considered modified
                   // (8) UB if p == q (so, p[0] and q[0] are the same object)
                   //     because &p != &q and B == B
    return p[0][0];
  }  // End Block B

  // Without (10) the calls to f0, f1, and f2 should all behave the same because
  // p[0] and q[0] refer to the same object, but it is not modified.
  // Without (10) the top-level 'restrict' in the parameter declarations
  // of f2() have no anti-aliasing effect.
  // Thus, optimizations allowing 13 to be returned are inhibited.
  // In f1() the top-level pointers are not restrict-qualified and
  // this allows p[0] and q[0] to refer to the same object.

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

  int main() {
    int x = 0;
    int *px = &x;
    int *gpx = &x;

    printf("f0: %d\n", f0(&px, &px)); // no UB
    printf("f1: %d\n", f1(&px, &px)); // no UB
    printf("f2: %d\n", f2(&px, &px));  // UB
  }


  // Example D:

  int f(int *q) {  // Begin Block B
    *q = 13;  // (7) object *q added to set RTS(NULL,B)

    int * restrict p = q;
      // (1) <D,P,T> is <int * restrict p, p, int>

    *p = 42;  // (6) object *p added to set RTS(&p,B)
              // (8) UB because *q and *p modify same object
              // NULL != &p and B == B
    return *q;
  }  //End Block B

  int g(int *q) {  // Begin Block B1
    *q = 13;  // (7) object *q added to set RTS(NULL,B1)

    {  // Begin Block B2
      int * restrict p = q;  // (1) <D,P,T> is <int * restrict p, p, int>
      *p = 42;               // (6) object *p added to set RTS(&p,B2)
                             // no UB, NULL != &p but B1 != B2
    }  // (13) End Block B2, all RTS sets labeled with B2 are deleted

    return *q;  // 42 is returned

    // p is declared in a nested block B2 and there is no UB as the
    // object modified by *q and *p is added to different sets 
    // RTS(NULL,B1) and RTS(&P,B2) but are associated with different blocks
  }  // End Block B1


  // Example E:

  int f(const int * restrict p) {  // Begin Block B
    // (1) <D,P,T> is <const int * restrict p, p, const int>

    int *q = (int *)p;  // (4) q is directly based on p
    *q = 13;            // (6) object *q added to set RTS(&p,B)
                        // (9) UB as T is const-qualified
    return *q;
  }  // End Block B

  int g(const int *p) {
    int *q = (int *)p;
    *q = 13;
    return *q;  // (9) UB only if p points to a const object

    // This leverages the restrict qualifier to enable a parameter declaration
    // that means "points to an object that shall be treated as const"
    // versus "points to an object that may be const". 
    // Above, f() always has UB but g() has UB only if it is passed a pointer
    // to an object that was declared as const
  }

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

  int main() {
    const int x = 42;
    int y;

    printf("f(&x) = %d\n", f(&x)); // UB
    printf("f(&y) = %d\n", f(&y)); // UB
    printf("g(&x) = %d\n", g(&x)); // UB
    printf("g(&y) = %d\n", g(&y)); // no UB
  }


  // Example 1:

  int f(int * restrict p, int *q) {  // Begin Block B
    // (1) <D,P,T> is <int * restrict p, p, int>

    int *r = p;  // (4) r directly based on p

    if (r == p) {
      r = q;    // (4) r now directly based on q
    }

    *r = 13; // (7) object *r added to set RTS(NULL,B)
    *p = 42; // (6) object *p added to set RTS(&p,B)
             // (8) UB if r == q because object is modified and
             // NULL != &p and B == B

    return *r;
  }  // End Block B


  // Example 2:

  int f(int * restrict p, int *q) {  // Begin Block B
    // (1) <D,P,T> is <int * restrict p, p, int>

  int *a = &p[p-q];  // (4) a is directly based on p
  *a = 13;           // (6) object *a added to set RTS(&p,B)
  p[1] = 42;         // (6) object p[1] added to set RTS(&p,B)
  return *a;         // no UB because *a and p[1] modify same object
                     // but &p == &p and B == B
}  // End Block B

  // (4) Consider &p[p-q] written as p+(p-q) (semantically equivalent to &p[p-q])
  // to see that a is still directly based on p

  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>

  int f(int * restrict p) {  // Begin Block B
    // (1) <D,P,T> is <int * restrict p, p, int>

    *p = 13;  // (6) object *p is added to set RTS(&p,B)
    uintptr_t i = (uintptr_t) p;  // (4) cast is not to a pointer
                                  // i is not based on p
    int *q = (int *) i;
    *q = 14;  // (7) object *q added to set RTS(NULL,B)
              // UB: because *p and *q modify same object
              // &p != NULL and B == B

    return *p + *q;
  }  // End Block B