target

preliminary discussion for possible integration into IS ISO/IEC 9899:202y

document history

license

CC BY, see https://creativecommons.org/licenses/by/4.0

1 Motivation

Traditionally, C’s function interfaces are particularly poor in the way information that can be transferred from the calling context into the caller and even poorer for the way back from the called function back to the caller. Originally, C only accounted for the number of arguments of a call and the return type, the addition of prototypes to the language added more static information about parameter types. This has later be enriched with only some more bits of dynamic information, in particular array sizes.

The goal of this paper is to continue this process of improvement of interface specifications to the dynamic verification of predicates which the current syntax is not capable to warrant. Algorithmic invariants or properties that are needed for optimization are not expressible in the interfaces that the language currently offers and, in general, are either missed, annotated manually with external tools, or, most commonly, by handwritten textual proofs.

Nevertheless, many predicates that would be needed here can be written as C expressions, provided that we add some additional state that, without interacting with the core of the computation, helps to propagate properties forward. The goal of this paper is to show how function interfaces in C can be enriched such that necessary predicates for calling them and conclusions from a call can be naturally expressed in otherwise existing C syntax and semantics. The core argument of this paper is to show that this execution model, with reasonable assumptions on the acceptable predicates, is equivalent to an implementation in conventional C where shallow inline wrappers execute cascaded if statements to check the predicates.

The goal of this paper is not to provide methods for hardening existing interfaces, and, in particular, the C library. In the contrary, adding contracts as proposed here changes the semantics of interfaces (in general from UB to well-defined failures) and they are thus not suited to paint over existing deficiencies in interface design.

2 Related features

Numerous tools exist in the field that ensure the check of predicates, usually expressed either as assertions or as pre- or postconditions. In the following we discuss three of them that have had the most influence on this proposal, here. The main motivation came from a similar feature that is a candidate to make it into C++26, C++ contracts; others are the traditional assert macro and Annex K of the C standard.

2.1 C++ contracts

C++ contracts are a complicated feature, in particular they let implementations chose between different semantics of a translated contract (ignore, observe, enforce and quick-enforce). Additionally, for two of these semantics (observe and enforce) they allow to configure behavior in the case of a contract violation by means of a user-supplied contract handler, ::handle_contract_violation. We don’t think that this whole spectrum of possibilities is adequate for a C feature.

First, for C it is not appropriate that readily compiled translation units (such as the C library or other third-party libraries) change behavior by means of a user-supplied contract handler. Such a global contract handler has similar effects as the runtime-constraint handler that is proposed by optional Annex K; for various reasons such a runtime-constraint constraint handler was not accepted by large parts of the C community as an appropriate tool and the annex is only implemented by very few implementations.

Second, the ignore semantics are counter-productive as they inhibit the evaluation of the predicate, and thus change semantics even in case that a contract holds. Thereby, the ignore semantics partially repeat a design error that was already present for C’s assert feature, see below.

Third, C++ contracts allow the predicates to have side effects, which then are possibly elided. In C we do not have that concept, and so allowing side effects makes it difficult to argue about semantics of contracts.

As a consequence our proposal with its default behavior only is compatible with C++’s quick-enforce semantics, and this only if the contract has no side effects. In particular, as proposed here for C, an optimizing compiler will be allowed to assume that the predicate holds unconditionally in all code that is sequenced after the evaluation. But, in contrast to earlier versions of this proposal, side effects are allowed; only they may appear out of sequence and up to two times (issued by the caller and by the callee). The details of such evaluations of side effects are implementation-defined.

Other features in our proposal that are different from C++ contracts:

• We allow declarations of ghost states, similar to declarations in if-statements.
• The name of the return variable in postconditions is fixed to _ReturnValue and cannot be annotated with attributes.
• We use keywords _Pre, _Post and _Inv for contracts. C++’s syntax with pre and post (plus inv) is available with function-like macros. Contracts cannot be annotated with attributes.
• We provide a macro (and function) stdc_contract_terminate that in general leads to the printing of a diagnostic and then to program termination.

Our proposed feature is meant to be compatible to C++ contracts at least for the quick-enforce semantics and in the absence of side-effects and contract attributes. We impose that the strategy in case of a contract violation is statically determined for each pre- or postcondition; the default behavior is that the execution (of the program or thread) terminates. In any case, a C proposal for contracts cannot have exactly the same syntax as for C++, because C++ uses syntactic concepts that are not available in C. Nevertheless, we try to provide a syntax that can be mapped between the languages by using some macro glue.

In particular, the difference in the syntax for the name of the return value could be simply avoided in C++ by using a definition such as

#define post(...) post(_ReturnValue: __VA_ARGS__)

This then forces that a return value of the name that C understands is defined, and that a post condition that has the C++ syntax for return values results in a syntax error.

2.2 The assert C library macro

Historically, C also has a macro that is intended to diagnose the violation of a given predicate, assert from clause 7.2 “Diagnostics <assert.h>”. Unfortunately this macro has not aged well and lacks capacities that would be needed in a modern environment of translators with improved optimization capabilities or even with integrated static analyzers. The main defect of that macro is that it is switched off as a whole by the user defined macro NDEBUG and that thus the resulting executables have different syntax and semantics:

• Syntax: The predicate that is used within an assert invocation may inadvertently be invalidated by distant changes of the source.
• Semantics: The predicate that is supposed to hold is not visible in optimized executables were NDEBUG is set:
  • Side effects differ with or without NDEBUG.
  • The knowledge about an assumed predicate is lost where it would be the most useful.
  • Assertions that do not hold have to be considered as errors, so setting NDEBUG continues an erroneous execution if the predicate does not hold. This may lead to undefined behavior somewhere down the line.

These semantic defects seem to be shared with C++’s ignore semantics.

Another issue with assert is that it uses abort to terminate the execution. Leaving invocations of assert without using NDEBUG is problematic:

• abort passes through the signal handling mechanism (with the signal SIGABRT) and is catchable.
  • Terminating with a signal has UB in the presence of several threads.
  • A signal handler could even return and have the execution continue for an error that is considered fatal, even though the design of the corresponding TU is not equipped to continue execution.
• If it terminates execution, there are no guarantees for cleanup:
  • Files may not be closed properly and data may get lost.
  • Application specific exit or quick_exit handlers are not run.
  • Core dumps may eat up disk space and leak sensitive information.

One goal of this paper here is to provide a better tool that in the future could replace uses of assert that are meant what the name verbally indicates, namely where the users seeks to assert a specific property. On the other hand, uses of assert as a diagnostic tool (and which goal is indicated by the clause header of 7.2 “Diagnostics”) would and should not be replaced.

2.3 Annex K, “bounds checking”

For the C library, Annex K has already taken the approach to replace the existing C library interfaces by new variants that make more guarantees and that introduce runtime checks for constraints. This can be seen as a case-study to amended specific C library interfaces. What are called runtime constraints, there, has a lot of similarities with predicates as defined in this paper.

Our approach differs from Annex K in multiple ways

• It is general: it provides a general language feature for contracted function interfaces, not a set of handcrafted new interface for some deficient library features.
• It has expressible semantics: in contrast to runtime constraints, contracts clearly express verifiable semantics on the level of the function interface; runtime constraints are not visible in the interface and are added as semantic description to each individual function description.
• It is compile-time configured: the decision not to terminate an execution even in presence of a contract violation is taken at the time of compilation of a translation unit. There are no handlers that could be changed dynamically and thus turn the interplay between different translation units to be inconsistent.
• It does not change platform ABI: the direct calling convention for a function with contracts stays the same as the version without. If a specific compiler is not able to produce checks for the contracts at the call side, the called function will be called “as always” and then perform the necessary checks for the contracts.
• It is optimization friendly: contracts can be verified at the calling site and are easily propagated into and out-of a function. In contrast to Annex K where runtime constraints are checked at each call, redundant contracts can be optimized out.

3 Approach

As it is the common model in C, we will assume that the functions that make up a program are split in translation units, TU, that each correspond to a C file that is compiled separately from all the others. A TU knows about functions in another TU only by declarations, most properties of these other functions are hidden. The advantages of such an approach are plenty, for example modularization, maintainability and fast compilation times, but there are also severe disadvantages: false assumptions lead to complicated bugs and lack of information misses optimization opportunities.

The proposed model for adding contracts to C interfaces is relatively simple at the surface: we create the possibility to add a list of contracts (pre-, postconditions and invariants) to function declarations at the very end. Contracts can effectively be checked from the calling context of a function or within the function itself (or both) without leading to semantic differences. The intent is that in general for preconditions the check is effected in the caller and for postconditions in the callee, such that these checks may seamlessly use knowledge that is already present in these contexts.

We took care that contracts as proposed here

• are useful in the context of C,
• provide guaranteed execution semantics when all contracts are fulfilled,
• cannot be added to existing interfaces without changing semantics,
• do not have runtime configurable semantics, and,
• have translation time configurable semantics that are strictly local to the definition of each function and only switch between forced termination and UB in case of a contract violation.

3.1 Design choices

There is a multitude of possible design choices for contracts, but for us, when restricted to the context of C, several choices seemed to impose themselves.

3.1.1 Overall design

Our main choices for the feature are as follows; changing any of these substantially would possibly invalidate the approach as a whole.

• An execution where any predicate is violated is considered erroneous.
• The default action, though implementation-defined for the details, is to terminate the execution in case of errors.
• An execution where all predicates hold has semantics that are independent from application or implementation choices.
• Contracts have to be specified consistently such that all information to evaluate them is present at the calling and the called side. Therefore, the use of contracts constrains the possibility for function declarations:
  • All parameter types must be completely determined for any declaration with contracts.
  • Parameter names in different declarations with contracts, if given, must agree.
• Contracts cannot be sidelined. Therefore contracts become part of the function type and calling a function that has been defined without contracts with a prototype that has them is invalid.
• Functions with contracts may be called with the same mechanism as functions without contracts. No ABI changes are required.

3.1.2 Termination

A crucial property of contracts is, that, in general, a violated predicate terminates execution. As of today, after more than half a century of C, there is still no established strategy on how to terminate an erroneous execution; the C standard alone has 6 different features (exit, quick_exit, _Exit, thrd_exit, abort and signals). Indeed, depending on the field, requirements for such termination are very different; in some contexts a graceful exit with cleanup is completely adequate; others should never terminate at all (such as an operating system); some cannot assure any consistent behavior after a violation and should halt instantly without any cleanup.

For these reasons we left the specific choice how to terminate by default to the implementation. They are best placed to offer the necessary tools and local choices to their customers.

Nevertheless all implementations have to provide a default behavior. This mode is particularly important for providers of libraries that cannot afford that user code (or other libraries) impose a different termination strategy on them. Implementations may want provide fine-tuning for this policy by means of command line arguments or configuration macros; such a specification is willingly left out of the proposed text.

3.1.3 Enforcing consistency within the same TU

Different declarations of the same function with contracts within the same TU would raise the question of consistency between those declarations. An early version of this paper attempted to provide a mechanism that would enforce consistency, but was considered too complicated, at least for an initial specification of such a feature.

Now we only require simpler properties. First, function parameters of different declarations for the same function with contracts must have the same name (if any). Second, at most one declaration may be annotated with contracts, such that a contradiction can simply not occur. For functions that are defined before possibly being redeclared (in general static or inline functions) contracts should be specified there; for functions that are forward declared in headers and then only defined in one TU, the contract is assumed to be at the forward declaration.

Within the same TU, function types with contracts can only be compatible if they are the same, that is if they refer to the same function type declaration; no redeclaration with contracts of a function type that already has them leads to a compatible type. Thereby function pointers to functions with contracts can only be interchanged if they refer to the same original type, and not a redeclaration of a compatible type. In cases where there is need for such a design, forward declarations with contracts should refer to a common type either by using a typedef:

typedef void* allocation_type(size_t n) _Post(_ReturnValue);
allocation_type my_malloc;
allocation_type my_arena;
allocation_type* what_can_we_do_for_you_today = my_arena;

or by using typeof to avoid a redeclaration

void* my_alloc(size_t n) _Post(_ReturnValue);
typeof(my_alloc) my_arena;
typeof(my_alloc)* what_can_we_do_for_you_today = my_arena;

3.1.4 Consistency between TU

Between different TU, ensuring consistency is difficult. The overall idea is that for functions that are called from different TU, the contract is specified in a declaration in a header file, and that that specification is precise enough such that no ambiguity occurs.

In general, such consistency cannot be guaranteed without additional mechanisms and tools. Therefore our specification only forsees UB in case that during an execution evaluations of parameter types or contracts would lead to different results. Additionally, we require that the number and kind of contracts (pre-, postcondition or invariant) agree, and that for any call of the function the evaluation of the contracts has the same result.

For parameter types the UB was already present, though implicitly. For contracts this is a new UB, but which we think is unavoidable for current C.

It is possible to put stronger mechanisms in place that would ensure that contracts between different translation units are consistent. Our reference implementation (see below) for example does this by encoding all contracts into the name of the auxiliary function as hashs; thus only translation units with consistent contracts can be linked into one executable. But since there is no commonly agreed mechanism for this, we leave it to the quality of implementation for the moment.

4 Suggested text

4.1 Language

4.1.1 in 6.2.1, Scopes of identifiers, type names, and compound literals

in p4

… If the declarator or type specifier that declares the identifier appears within the list of parameter declarations in a function prototype (not part of a function definition), the identifier has function prototype scope, which terminates at the end of the innermost full declarator that contains the function declarator or the end of the innermost full abstract declarator that contains the function abstract declarator. …

4.1.2 in 6.3.3.3 Pointers

8 A pointer to a function of one type can be converted to a pointer to a function of another type and back again; the result shall compare equal to the original pointer. If a converted pointer is used to call a function whose type is not compatible with the referenced type or if a function without contracts is called with a type with contracts, the behavior is undefined.

4.1.3 in 6.4.2, Keywords

add _Inv, _Post and _Pre to the list of keywords.

4.1.4 in 6.5.17.2 Simple Assignment

Add items in p1 after the second position

— the left operand has atomic, qualified, or unqualified pointer to a function type without contracts, and (considering the type the left operand would have after lvalue conversion) both operands are pointers to compatible types;

— the left operand has atomic, qualified, or unqualified pointer to a function type with contracts, and (considering the type the left operand would have after lvalue conversion) and the right operand has the same type as the left operand;

and amend the now fifth item

— the left operand has atomic, qualified, or unqualified pointer type, and (considering the type the left operand would have after lvalue conversion) both operands are pointers to qualified or unqualified versions of compatible object types, and the type pointed to by the left operand has all the qualifiers of the type pointed to by the right operand;

4.1.5 Clause 6.7.7.4

4.1.5.1 Syntax

Apply the following changes.

Add contract-list to the syntax in 6.7.7.1

declarator:

pointer_opt direct-declarator contract-list_opt

[…]

Constraint

1′ If a contract list appears in a declarator, that declarator shall be a full declarator, there shall be a function type T such that the declared type is T or a pointer to T, and, before possible replacement of array length expressions by the token *, no type of a parameter of T shall have a type component of unspecified array length.

and in 6.7.8

abstract-declarator:

pointer contract-list_opt

pointer_opt direct-abstract-declarator contract-list_opt

[…]

Constraints

1′ If a contract list appears in an abstract declarator, that abstract declarator shall be a full abstract declarator, there shall be a function type T such that the declared type is T or a pointer to T, and, before possible replacement of array length expressions by the token *, no type of a parameter of T shall have a type component of unspecified array length.

Semantics

2 In several contexts, it is necessary to specify a type. This is accomplished using a type name, which is syntactically a declaration for a function or an object of that type that omits the identifier.¹⁴⁴⁾ A full abstract declarator is an abstract declarator that is not part of another abstract declarator. The optional attribute specifier sequence in a direct abstract declarator appertains to the preceding array or function type. The attribute specifier sequence affects the type only for the declaration it appears in, not other declarations involving the same type.

4.1.5.2 In 6.7.7.4, Function declarators

add a new paragraph to the Constraints section

Constraints

[…]

4′ Where a composite type of two compatible function types that are declared in the same translation unit is required, at most one of them shall have a contract list.

Then, in the Semantics section

15 Two function types without contract list are compatible if and only if all of the following hold:

• They specify compatible return types.
• The parameter type lists agree in the number of parameters and in whether the function is variadic or not.
• The corresponding parameters have compatible types.

In the determination of type compatibility and of a composite type, each parameter declared with function or array type is taken as having the adjusted type and each parameter declared with qualified type is taken as having the unqualified version of its declared type.

4.1.6 Add a new subclause for contracts

Rationale: predicates that are known to be always false should abort compilation with semantics similar to static_assert.

Rationale: contracts are primarily thought as annotations of an interface between different translation units. Therefore they should not read the contents of static variables or call static functions. They must not have UB if a ghost state would be uninitialized in some situations.

Rationale: The definition must always implement the contracts for the case that it is called through a function pointer.

Rationale: It is difficult to specify conditions in different parts of a TU that would be guaranteed to evaluate to the same value, regardless of the circumstances.

Rationale: Calling such a function would evaluate the contracts in a different thread than the visible context of the call to thrd_create.

Rationale: This forbids the compilation of a function without contracts and then adding such contracts later to a header file. If that would be allowed, the function could eventually be called without the check for any of the predicates in place, and thus the semantics of the contracted interface would be violated.

void *my_memcpy(void*const dest, const void*const src, size_t const n)
    _Pre(n)
    _Pre(const unsigned char *const dest_start = dest)
    _Pre(const unsigned char *const src_start  = src)
    _Pre(((uintptr_t)(src_start + n)  <= (uintptr_t)dest_start)
        || ((uintptr_t)(dest_start + n) <= (uintptr_t)src_start))
    _Post(_ReturnValue == dest);

// header "range.h"
#include <stdint.h>
inline
bool range_check(void const*const a,
                 void const*const b,
                 size_t const n) [[unsequenced]]
    _Pre(a) _Pre(b) _Pre(n)
{
     const unsigned char *const dest_start = a,
     const unsigned char *const src_start  = b;
     return
        ((uintptr_t)(src_start + n)  <= (uintptr_t)dest_start)
        || ((uintptr_t)(dest_start + n) <= (uintptr_t)src_start);
}

#include "range.h"
void *my_memcpy(void*const dest, const void*const src, size_t const n)
    _Pre(range_check(dest, src, n))
    _Post(_ReturnValue == dest);

#include "range.h"

// makes the definition external
extern typeof(range_check) range_check;

// header file "alloc.h"
typedef void* alloc_t(size_t n) _Pre(n) _Post(_ReturnValue);
extern alloc_t  alloc_uninit;
extern alloc_t  alloc_init;
extern alloc_t* alloc_today;

// implementation
#include <stdlib.h>
#include "alloc.h"

alloc_t* alloc_today =
#if USE_ALLOC‿UNINIT
    alloc_uninit
#else
    alloc_init
#endif
;

// the composite type has the contracts
void* alloc_uninit(size_t n) {
    void* ret = malloc(n);
    if (!ret) {
        stdc_contract_terminate("out of memory in allocation");
    }
    return ret;
}

// the composite type has the contracts
void* alloc_init(size_t n) {
    void* ret = calloc(n, 1);
    if (!ret) {
        stdc_contract_terminate("out of memory in allocation");
    }
    return ret;
}

4.2 Library: add a new header <stdc_contract.h>

Remark: It would also be possible to add these macros to <assert.h>, but without using the NDEBUG mechanism.

#include <stdc_contract.h>

#ifdef __cplusplus
# define post(...) post(_ReturnValue: __VA_ARGS__)
#else
# ifndef inv
#  define inv(...)  _Inv(__VA_ARGS__)
# endif
# ifndef pre
#  define pre(...)  _Pre(__VA_ARGS__)
# endif
# ifndef post
#  define post(...) _Post(__VA_ARGS__)
# endif
#endif

[[noreturn]] void (stdc_contract_terminate)(char const* mess);
typedef void stdc_contract_termination_t(int);

Rationale: strings are always required to be ordinary string literals, here, to ensure that these strings are valid during all phases of termination of the execution and that no character set conversion has to be performed dynamically. In particular, dynamic allocations of diagnostic strings are to be avoided.

5 Discussion of the semantics expressed in equivalent C code

As defined in the suggested text above, it may seem as if contracts impose severe constraints to all executions, as they assume that all contracts are checked on all function calls. Because of the strong impact that such a behavior would then have for example on execution times, as such this would probably not be a viable proposal.

In fact, modern compilers and static analyzers should be able to prove for many contracts that they hold unconditionally; thus they are dead code and can be removed. One of the keys to that is that all evaluations in contracts are forced to be free of side effects and can in general be hoisted out of the immediate calling context. The other key is the requirement that contracts for the same function, even if specified in different translation units, have to behave the same when presented with the same arguments.

In the following a selection-header of a precondition is given in the form

dec_preᵢ predicate_preᵢ

where the part

• dec_preᵢ is a declaration (of one or several ghost states) in the form

type_preᵢ ghost_pre⁰ᵢ = init_pre⁰ᵢ, ...;

• and predicate_preᵢ is a predicate that is to be checked.

The same syntax as for if-statements is admissible, that is either dec_preᵢ or predicate_preᵢ can be empty, but not both. Both, dec_preᵢ and predicate_preᵢ, are the usual C constructs as they may appear in if-statements.

If predicate_preᵢ is empty, then (per definition of the if statement) dec_preᵢ is a simple declaration defining exactly one ghost state ghost_pre⁰ᵢ with initializer init_pre⁰ᵢ. predicate_preᵢ is then assumed to be the expression init_pre⁰ᵢ.

Analogous definitions hold for postconditions in the form dec_postᵢ predicate_postᵢ.

In the following we discuss three different views of a function with contracts,

• one from the view of a caller that has an inline definition with contracts.
• one from the view of a caller that only has a declaration with contracts and no definition,
• one from the view of the TU that implements a function with contracts.

5.1 Semantics of an inline definition

If a function with contracts is given as an inline definition, the semantics are relatively simple and easily explained in existing C syntax: tests for the preconditions have to be inserted before the rest of the function body and tests for post conditions afterwards. There is only one subtlety, namely the handling of return statements. In fact, all return statements are replaced by assignments to the auxiliary variable _ReturnValue and then a proper return statement is added at the end, after all postconditions have been checked.

Suppose a list of contracts is attached to a function definition with inline:

// header
inline returnType func(parameterTypeList)
  pre(dec_pre₀ predicate_pre₀)
  pre(dec_pre₁ predicate_pre₁)
  …
  pre(dec_preₙ predicate_preₙ)
  post(dec_post₀ predicate_post₀)
  post(dec_post₁ predicate_post₁)
  …
  post(dec_postₘ predicate_postₘ)
function-body

// translation unit
typeof(func) func; // instantiation of func

The effect is as-if the function was augmented with cascaded if statements that test for the conditions.

// header
inline returnType func(parameterTypeList) {
    returnType _ReturnValue;

    if (dec_pre₀ !predicate_pre₀) {
        static_assert(ICE_OR_TRUE(predicate_pre₀), "some string");
        stdc_contract_terminate("some string");
    } else if (dec_pre₁ !predicate_pre₁) {
        static_assert(ICE_OR_TRUE(predicate_pre₁), "some string");
        stdc_contract_terminate("some string");
    } else if (…) {
        ...
    } else if (dec_preₙ !predicate_preₙ) {
        static_assert(ICE_OR_TRUE(predicate_preₙ), "some string");
        stdc_contract_terminate("some string");
    } else {
        _Defer {
            if (dec_post₀ !predicate_post₀) {
                static_assert(ICE_OR_TRUE(predicate_post₀), "some string");
                stdc_contract_terminate("some string");
            } else if (dec_post₁ !predicate_post₁) {
                static_assert(ICE_OR_TRUE(predicate_post₁), "some string");
                stdc_contract_terminate("some string");
            } else if (…) {
                ...
            } else if (dec_postₘ !predicate_postₘ) {
                static_assert(ICE_OR_TRUE(predicate_postₘ), "some string");
                stdc_contract_terminate("some string");
            }
        }
        replaced-function-body      // amend return with assignment
    }
}

Here, replaced-function-body is the function-body where all expressions in a return statement of the form

return expression

are replaced by assignments

return (_ReturnValue = expression)

_Defer is the defer feature as described in the defer technical specification, and the macro ICE_OR_TRUE is supposed to resolve to its argument if that is an integer constant expression (ICE) and to true, otherwise.

Note that the if-statements with the inverted condition are such that all definitions of ghost states in the form dec_preᵢ or dec_postᵢ are visible to all evaluations in the subsequent contracts.

The derived inline function definition has the following properties.

• If any of the predicates is an ICE, it is asserted at compilation time; the static_assert expressions only trigger for ICE.
• It ensures that all the preconditions hold and that the program terminates with an error if they do not.
• It executes the function body.
• Then it checks the postconditions.
• It warrants to callers (and in particular inliners) that the postconditions hold.

In the calling context some information may be present which ensures that the preconditions are always satisfied. Then, these can effectively be optimized out at compile time without changing the semantics. Similarly, the knowledge about postconditions can be integrated into the calling context.

5.2 Semantics of an external declaration

If a function is split into an external declaration in a header and a definition in one TU, things get a bit more complicated. Here, we define an auxiliary inline definition that tests for contracts as above and calls a different internal function to access the original definition. The subtlety here is that we only want violations of preconditions in the calling context to terminate the execution, but in postconditions they should be unreachable.

Suppose a list of contracts is attached to a function declaration without inline:

// header
returnType func(parameterTypeList)
  pre(dec_pre₀ predicate_pre₀)
  pre(dec_pre₁ predicate_pre₁)
  …
  pre(dec_preₙ predicate_preₙ)
  post(dec_post₀ predicate_post₀)
  post(dec_post₁ predicate_post₁)
  …
  post(dec_postₘ predicate_postₘ);

// translation unit
returnType func(parameterTypeList) function-body

The effect is as-if the following function were defined in the header.

// header
inline returnType func(parameterTypeList) {
    returnType _ReturnValue;

    if (dec_pre₀ !predicate_pre₀) {
        static_assert(ICE_OR_TRUE(predicate_pre₀), "some string");
        stdc_contract_terminate("some string");
    } else if (dec_pre₁ !predicate_pre₁) {
        static_assert(ICE_OR_TRUE(predicate_pre₁), "some string");
        stdc_contract_terminate("some string");
    } else if (…) {
        ...
    } else if (dec_preₙ !predicate_preₙ) {
        static_assert(ICE_OR_TRUE(predicate_preₙ), "some string");
        stdc_contract_terminate("some string");
    } else {

        typeof(func) func_aux;
        _ReturnValue = func_aux(parameters, …);

        if (dec_post₀ !predicate_post₀) {
            static_assert(ICE_OR_TRUE(predicate_post₀), "some string");
            unreachable();
        } else if (dec_post₁ !predicate_post₁) {
            static_assert(ICE_OR_TRUE(predicate_post₁), "some string");
            unreachable();
        } else if (…) {
            ...
        } else if (dec_postₘ !predicate_postₘ) {
            static_assert(ICE_OR_TRUE(predicate_postₘ), "some string");
            unreachable();
        } else {
            return _ReturnValue;
        }
    }
    stdc_contract_terminate("severe bug, execution must never reach here");
}

The function func_aux will be shown in the next section. The name func_aux is only chosen for the example, a real implementation chooses a unique name that is not predictable for the user.

The auxiliary inline function definition has the following properties.

• If any of the predicates is an ICE (pre- or postconditions alike), it is asserted at compilation time. As above, the macro ICE_OR_TRUE ensures that the static_assert expressions only trigger for ICE.
• It ensures that all the preconditions are tested, even when inlined, and that the program terminates with an error if they do not.
• Otherwise, it calls an auxiliary function func_aux that implements the user code and that asserts the postconditions.
• It warrants to callers (and in particular inliners) that the postconditions hold by testing them as assumptions.

Note that again preconditions that are known to hold in the calling context can effectively be optimized out at compile time without changing the semantics. Similarly, postconditions can provide valuable information for the calling context. For these optimization opportunities it is essential that contracts do not have side effects.

5.3 Semantics of the function implementation

The translation unit then provides two function symbols: the auxiliary function func_aux that is called by the inline version of func as given above, and the instantiation of func itself. As mentionned, the name func_aux is only for the example; it is a unique name that is not predictable for the user.

// translation unit
returnType func_aux(parameterTypeList) {
    returnType _ReturnValue;

    if (dec_pre₀ !predicate_pre₀) {
        static_assert(ICE_OR_TRUE(predicate_pre₀), "some string");
        unreachable();
    } else if (dec_pre₁ !predicate_pre₁) {
        static_assert(ICE_OR_TRUE(predicate_pre₁), "some string");
        unreachable();
    } else if (…) {
        ...
    } else if (dec_preₙ !predicate_preₙ) {
        static_assert(ICE_OR_TRUE(predicate_preₙ), "some string");
        unreachable();
    } else {

        _Defer {
            if (dec_post₀ !predicate_post₀) {
                static_assert(ICE_OR_TRUE(predicate_post₀), "some string");
                stdc_contract_terminate("some string");
            } else if (dec_post₁ !predicate_post₁) {
                static_assert(ICE_OR_TRUE(predicate_post₁), "some string");
                stdc_contract_terminate("some string");
            } else if (…) {
                ...
            } else if (dec_postₘ !predicate_postₘ) {
                static_assert(ICE_OR_TRUE(predicate_postₘ), "some string");
                stdc_contract_terminate("some string");
            }
        }
        replaced-function-body      // amend return with assignment
    }
}
typeof(func) func; // instantiation of func

The only function that is called by user code is func, either as the inline definition in the header file or via the external symbol; both types of calls have the same semantics.

In particular, func_aux, will never be called directly by user code.

• It warrants to the translator that the preconditions hold.
• It executes the function body under these assumptions.
• It asserts that the postconditions hold and terminates execution otherwise.

A non-optimized version of the instantiation of func would evaluate each predicate twice, once from the inline body of func and once from the body of funx_aux. Indeed, each predicate is first checked as an assertion (possibly calling stdc_contract_terminate()) and then as an assumption (running into unreachable()), so because the predicate cannot have side effects and has to evaluate the same in both contexts.

6 Implementation experience

It seems that in the advent of C++26, all major C++ compilers have implementations of C++ contracts with some of the semantics models mentioned above.

In C, there is now wide support for some form of “assume” feature, either as builtins (clang, MSV) or as an attribute (gcc). Together with C23’s unreachable, in C this helps to implement the semantics with shallow inline wrappers as described previously.

If there is no additional help from the compiler, the need to implement two consistent wrappers (the inline version of func and func_aux above) makes the approach a bit tedious and not very practical as an implementation strategy. Nevertheless, this already provides a way to test the semantics and to see how modern compilers are able to detect redundancies in chained contracts.

Our eĿlipsis preprocessor provides include files <ellipsis-contracts.h>, <ellipsis-interface.h> and <ellipsis-implementation.h> that uses a syntax that is relatively close to the proposed syntax for declarations with contracts, and uses them to implement the following features:

• Automatic generation of inline wrappers.
• Automatic generation of auxiliary names. These names contain a hash value for each contract specification, such that linking of TUs with inconsistent contracts produces an error.
• Automatic generation of the replication of the contracts in the auxiliary function (func_aux above).
• Automatic addition of assignments to _ReturnValue in return statements.
• Emulate C2Y’s if statement with declarations to implement the ghost state feature.
• Emulate the _Defer feature for a consistent implementation of postconditions.

The features _Pre, _Post and _Inv use static strings for the diagnostics that are forcibly embedded in the executable. These can be used to evaluate which of the contracts actually survived optimization. Thereby a detailed assessment of the particular optimization capabilities can be made. A small script is provided to facilitate such an analysis.

eĿlipsis’ sources also uses contracts as described themselves. This provides a lot of test cases for the abilities of modern compilers. Evaluations with gcc and clang show interesting level of optimization, as long as not too much aliasing analysis needed for the contracts.

Acknowledgments

Thanks to Martin Uecker, David Tarditi, Joseph Myers, and Ville Voutilainen for review and discussions.