C++ seems to finally converge with their contracts proposal, https://wg21.link/p2900. I decided to give it a try and come up with ideas how such a thing would look for C. This is in early stages, not a full proposal yet, and still would need implementation by some of the major compilers.
In particular, the C++ feature is full of sidetracks that I don’t like at all, such as user-defined global handlers and ignorability. But there is a core of ideas, syntax and semantics that I found interesting and that I think should be considered for C. The principal features are
Contract pre- and postconditions add verifiable conditions that are added to function interfaces. They are checked on entry to a function call and provide knowledge that is valuable for the code following a call.
If the condition is an integer constant expression, a pre- or postcondition is similar to an invocation of static_assert . If the condition is false, compilation fails. In the following we will not illustrate this aspect to simplify the discourse.
. If the condition is false, compilation fails. In the following we will not illustrate this aspect to simplify the discourse. They have no implications on ABI.
They can be made composable. If applied rigorously, such conditions can often be deduced from the context. They need not be checked dynamically.
Besides verified correctness, they offer optimization opportunities for the context of a function call and for the called function itself.
To see how all of this works we first need understand two fundamental primitives, assertions and assumptions. Their syntax looks something like
contract_assert(COND, "some explanatory text"); contract_assume(COND, "some explanatory text");
Here, in both cases COND is some condition that is supposed to be fulfilled.
The first, contract_assert , is quite similar to a feature that we already have in C namely the assert macro. Both test for the condition; if it is fulfilled nothing happens and execution goes on. If it is not fulfilled, a diagnostic is printed to stderr and abort is called to end the execution. The difference to assert is that contract_assert always has to be correct C code. There is no such thing as NDEBUG that pretends the assertion doesn’t even exist.
The other feature, contract_assume , is more subtle and actually quite dangerous if applied carelessly. It is as if defined as
#define contract_assume(COND, ...) do { if (!(COND)) unreachable(); } while (false)
Here unreacheable() is the new macro from C23 (and C++23) that makes the behaviour undefined whenever the branch of the invocation is reached. So in general such a condition would not even be evaluated, but it would be taken for grated that it holds. (It would be evaluated for its side effects if it had any, but you shouldn’t do such things, anyhow.) Take an example
contract_assume(p, "pointer must never be null"); *p = 34.7;
Here we, the programmer, promise that the pointer is never null and the compiler can assume that for the following without checking.
With contract_assert we can give an idea what pre- and postconditions look like from outer space. Take a conventional C function with a declaration in a header file and a definition in a .c file:
// .h header void* my_malloc(size_t size);
// .c definition void* my_malloc(size_t size) { return malloc(size); }
This function is admittedly a bit lame. It has just one function call in the body. However, please take this as a simple example for illustration. With contracts, the declaration could look something like
void* my_malloc(size_t size) pre(size) post(r: r);
This declares that the argument to size of a call to my_malloc must always be checked to be non-zero and that the return value, here named r , will always be checked such that it is non-null. An implementation with current tools of that function that takes these conditions into account, but doesn’t reflect them in the declaration part could look as follows
// .h header inline void* my_malloc(size_t size) { contracts_assert(size, "can't allocate empty buffer"); defer { contracts_assert(defer_return_value, "allocation failed"; }; return malloc(size); }
// .c instantiation extern void* my_malloc(size_t size);
Putting this as an inline function in the header ensures that the contracts are visible for all callers, and thus, when integrating this into the control flow, the conditions can either be deduced (e.g if we know that the argument is non-zero) or can be used to deduce properties in the caller (e.g the returned value is always non-null).
Note also, that here we use defer to ensure that the assertion triggers regardless on how we leave the function. This is probably not so interesting for this short example. However, if the function has complicated nesting with multiple returns, defer simplifies the process. It helps with code that we want to execute unconditionally on function return.
Changing all functions to inline functions would deviate much from the usual abstraction between interface and implementation in C (and C++). So contracts are an attempt to enrich the interface such that the core of the function stays in its own file and remains known only via the provided interface. A first advantage of pre and post should be obvious. Since it is part of the declaration, it helps people to understand what to expect of a function. It may also assist compilers in the same way. In particular the postcondition can help to take conditions ahead into the context of the caller:
double* p = my_malloc(sizeof(*p)); *p = 34.7;
Here the call to my_malloc , instead of using malloc directly, ensures that the pointer is always checked. A sensible message is printed before the execution aborts, if necessary. For any implementation of postconditions we would want the compiler to deduce that property directly, only from the declaration.
Unfortunately, this simple top level view isn’t very satisfactory:
A precondition that is hidden in a .c file is only checked when the function has already been entered. In the calling context it might already be known that size is not zero. This information is lost and the assertion has always to be checked at the start of the function.
is not zero. This information is lost and the assertion has always to be checked at the start of the function. If the postcondition is also checked within the function call, we have to come up with a mechanism that propagates the information to the calling context.
To improve these aspects, the following observation about assertions and assumptions is key:
In a series of assertions and assumptions, if they check the same condition without an intermediate change of the execution state, only the first assertion or assumption is necessary. All subsequent assertions or assumptions are redundant.
Take the null pointer check from above. Repeating the assumption clearly does not add any new information for the compiler:
contract_assume(p, "pointer must never be null"); contract_assume(p, "pointer must really not be null"); *p = 34.7;
Similarly, mixing an assertion and an assumption on the same condition does not achieve much:
contract_assert(p, "pointer must never be null"); contract_assume(p, "pointer must really not be null"); *p = 34.7;
Here the compiler has to make sure that the assertion holds, so afterwards the condition can be assumed. If we invert the order:
contract_assume(p, "pointer must never be null"); contract_assert(p, "pointer must really not be null"); *p = 34.7;
When reaching the assertion, the compiler knows that the condition has just been checked. Thus, the whole assertion can be omitted. This observation can help develop an execution model for function with contracts. It fits into C’s current execution model.
A precondition c on a function f can be replaced by an assertion of c that is executed before any call to f that is combined with an assumption of c at the start of the execution of the function body.
A postcondition c on a function f can be replaced by an assertion of c at the end of the execution of the function body combined with an assumption of c that is placed after any call to f.
Let’s visit this with our my_malloc example. If we want to execute the precondition before going into the real call of our function we can replace the declaration with the contracts by an inline function:
/* in a .h header */ inline void* my_malloc(size_t size) { contracts_assert(size, "can't allocate empty buffer"); defer { contracts_assume(defer_return_value, "allocation failed"; }; return my_malloc_inner(size); }
That inline function makes the necessary assertions and assumptions. If a call to it is inlined at some point, the compiler sees these and can use the information to check and optimize. Then it tail-calls another function my_malloc_inner that contains the code that otherwise would just have been the definition of my_malloc .
Then, in the .c file, we have to give the implementation of my_malloc_intern and the instantiation of the inline function.
/* in a .c implementation file */ extern void* my_malloc(size_t); // instantiation of the inline function void* my_malloc_intern(size_t size) { contracts_assume(size, "can't allocate empty buffer"); defer { contracts_assert(defer_return_value, "allocation failed"; }; // now do everything we need to do return malloc(size); }
This combination of an inline wrapper for the contracts and an auxiliary function for the inner workings of the functions guarantees the requested behaviour:
the precondition is checked before entry of the auxiliary function
the precondition is known to hold on entry of the auxiliary function
the postcondition is checked at the end of the auxiliary function
the postcondition is known to hold after a call to the auxiliary function.
So this combination has the properties that we want from contracts: the calling context and the called context can deduce the information from the contracts to optimize. But this approach has still a major disadvantage, we have to repeat the conditions within the code of the auxiliary function. This is tedious and error-prone.
The latest release of eĿlipsis provides a mechanism that avoids that code duplication. The contracts are expressed basically as above with an inline function:
/* in an -interface.h header */ inline void* EXBINDING(my_malloc)(size_t size) { DEFER_TYPE(void*); ellipsis_precondition(size, "can't allocate empty buffer"); ellipsis_postcondition(defer_return_value, "allocation failed"; }; // forward declare auxiliary function extern typeof(EXBINDING(my_malloc)) INBINDING(my_malloc); // call auxiliary function with same parameters return INBINDING(my_malloc)(size); }
The difference here is that the conditions are expressed with special macros. These macros make it easier to place the right pairs of assertion/assumption inside the inline function. They also help with the implementation. Macros EXBINDING/INBINDING deal with the naming of auxiliary functions. The implementation file then looks very much like the original function definition from which we started.
// -implementation.c definition void* EXBINDING(my_malloc)(size_t size) { return malloc(size); }
Only the EXBINDING macro is needed to get the name right. This approach expresses all the contracts in the header file. It also leaves the core of the implementation almost unaltered. If you are interested in the details of this approach please refer to the corresponding eĿlipsis documentation.
All of this is unfortunately nothing that can be used easily, yet. A proper interface specification similar and compatible to the one used by C++ would be needed. Nevertheless this is a proof of concept of such an approach for C. The tools we needed are