The restrict qualifier as an element of specificationPascal Cuoq - 25th Jul 2012
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:
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)]).
restrictalso 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.
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
That's the theory anyway. In practice the situation is even worse than 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.
One tool that comes close to checking for proper use of functions with
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
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];
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.