The restrict qualifier as an element of specification

An insightful interjection

Stephen Canon, whose explanations about the fine points of floating-point I have appreciated on StackOverflow chimed in on the subject of the restrict qualifier. With minor edits for consistency with this blog's formatting:

Consider memcpy(); its arguments are declared restrict. This not only means that the source and destination pointers cannot be the same (which is what Pascal's "replacement" says) but also means that the buffers cannot overlap at all (i.e. the src pointer cannot be anywhere in the range [dst-(length-1) dst+(length-1)]).

restrict also has the virtue of making this contract apparent to your callers as it's part of the API. People should know that they can't call memcpy() with overlapping buffers and use memmove() instead. If the information is instead encoded in a cryptic line in the implementation then it isn't obvious to a developer who intends to use the function.

Non-aliasing granularity

I noted that my not-really-serious proposal did not have the same granularity as the original with both good and bad consequences. An advantage of my proposal is that it is possible to specify only that p does not alias with q and that r does not alias with t. As defined in C99 restrict is more concise but this also means that there are some properties you might want to specify and that you cannot.

restrict as an element of specification

But I failed to realize that restrict being a type qualifier (for the casual C/C++ programmer: like const) is part of the function prototype. I was only thinking of the opportunity for better code generation inside f() but it would theoretically be possible to have compilers that warn about passing aliasing pointers to f().

That's the theory anyway. In practice the situation is even worse than for const. For const you get type-system level warnings about casts discarding the qualifier. The warnings are sometimes useful and sometimes annoying. For restrict I do not know of any tool that makes any check of proper use at the call site.

An alternative

One tool that comes close to checking for proper use of functions with const and restrict-like specifications is developed nearby (have you heard of it?). One drawback is that it is work in progress. And it uses its own syntax for function specifications.

Here is the specification for memcpy() in that system:

/*@ requires \valid(((char*)dest)+(0..n-1)) 
  @          && \valid(((char*)src)+(0..n-1)); 
  @ requires \separated(((char *)dest)+(0..n-1) ((char *)src)+(0..n-1)); 
  @ assigns ((char*)dest)[0..n-1] \from ((char*)src)[0..n-1]; 
  @ ensures memcmp((char*)dest (char*)src n) == 0 && \esult == dest; 
  @*/ 
extern void *memcpy(void *restrict dest  
                    const void *restrict src  size_t n); 

Yes it is longer than just sprinkling the prototype with const and restrict and I did not even include the definition of the logic predicate memcmp. But on the other hand what you have here is a complete specification of memcpy(). You can ask your worst enemy to write a function to this specification and ey proves that eir implementation satisfies the specification you can rest assured that for all valid inputs the function terminates and computes the right result. The worst your enemy could do would be to provide you with a function that is arbitrarily slower than necessary.

Side note: solutions to the problem of your worst enemy providing you with a function that is too slow are being researched but even researchers working on that would agree that this field has not reached the maturity of the solutions to the problem of your worst enemy providing you with a function that functionally does the wrong thing.

I can provide a neat trick for verifying that a function executes in constant time but this is only a very partial solution to the problem.

Enough about this hypothetical worst enemy. The const part of memcpy()'s specification and more is contained in the clause:

assigns ((char*)dest)[0..n-1] \from ((char*)src)[0..n-1]; 

The restrict part is contained in:

requires \separated(((char *)dest)+(0..n-1) ((char *)src)+(0..n-1)); 

I might be biased but I think it is just as clear and separate concerns are better separated. The \separated predicate for instance is also useful for expressing exactly the conditions under which the statement (*p=*p) & (*q=*q); is defined.

The ACSL by example library contains more examples of function contracts.