Document Number: N3058
Date: 2022-October-25
Authors: Bill Homer, Tom MacDonald (redactor)
Reference Documents: N3005 A Provenance-aware Memory Object Model for C, N3025 Defect With Wording Of restrict Specification
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.
[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.
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.
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