December 15, 2022·5 min read·engineeringcppcontractssafety

P2680R1 proposes stronger rules for evaluating contract predicates

The revised safety-focused contracts paper separates restricted predicates from an explicit relaxed form. It also addresses undefined behavior inside the checks themselves through proposed conveyor functions and arithmetic rules.

A runtime check cannot reliably protect a program if evaluating the check itself invokes undefined behaviour. Gabriel Dos Reis opens P2680R1, dated December 15, with an arithmetic example that makes this problem concrete. A compiler can reason through a function called by a precondition and eliminate a check based on assumptions about signed overflow.

The revision expands October's P2680R0, which argued for contract predicates with contained side effects. It now proposes restricted non-relaxed predicates, an explicit relaxed alternative, and functions whose operations satisfy additional constraints. The paper remains a proposal. These are suggested semantics for contracts, not rules available in ordinary standard C++ today.

I value C++'s ability to express precise obligations, but undefined behaviour can undermine an apparently straightforward check. A facility intended to improve safety needs an account of its own failure cases. This revision is interesting because it makes that requirement part of the proposed predicate model.

Arithmetic inside a check needs defined limits

The paper considers a function that adds 100 to an integer and a precondition comparing the result with the input. When the optimizer sees the function definition, the absence of signed overflow becomes a premise in its reasoning. Depending on the comparison, that reasoning can make the predicate unconditionally false or remove its check.

Dos Reis reports this behaviour from an experimental GCC contracts implementation and links the examples. The general point is about the language model. Signed arithmetic that would overflow does not acquire wraparound semantics merely because it appears in code intended to check another operation. The proposed contract facility must define its evaluation separately if it wants a stronger guarantee.

R1 discusses replacing some undefined arithmetic outcomes with implementation-defined behaviour. It suggests possibilities such as wrapping or saturation. Another section uses unspecified-result wording for overflow and underflow while still prohibiting undefined behaviour. Those formulations show the paper's design is still being developed. They do not establish one final arithmetic policy for every restricted predicate.

The distinction among these categories matters. Implementation-defined behaviour requires an implementation choice to be documented. Unspecified behaviour can permit several outcomes without the same documentation requirement. Both impose different limits from an unconstrained undefined operation, but a usable contract design still needs a coherent choice.

Relaxed predicates expose an escape route

The revision introduces a relaxed modifier for preconditions and postconditions that cannot satisfy the stronger model. Its example combines logging with a nonzero test. The relaxed predicate may have externally observable effects, while the separate ordinary predicate can retain the restricted guarantees.

This split lets the proposal describe an explicit concession. A predicate using the relaxed form does not receive the restrictions and protections defined for non-relaxed predicates. It is therefore misleading to describe every contract written under this design as free from the same classes of undefined behaviour.

The paper recommends separating expressions that violate the stronger restrictions into their own relaxed contracts. That makes the loss of guarantees more localized. It also preserves the earlier argument that work necessary to the program's intended behaviour belongs in its ordinary implementation, rather than relying on effects hidden inside a safety annotation.

Conveyor functions carry a restricted contract

R1 names a proposed category of helper function with the attribute [[conveyor]]. Conceptually, these functions keep effects within their body or argument list and restrict operations that might invoke undefined behaviour. A non-relaxed predicate may use those functions and the permitted builtin operations.

The rules are intentionally conservative. They restrict use of mutable namespace or class state and thread-local variables. Local variables require initialization. Allocation and deallocation expressions are excluded, as are coroutine await and yield expressions. Other restrictions address casts and operations involving pointers.

A conveyor function can still modify an argument under its own rules. The paper illustrates this with an incrementing function that takes an integer reference. A contract predicate has additional restrictions on how it passes the function's parameters, including const-reference or value access and no modifying operators on those parameters. The containment rule therefore depends on the evaluation boundary, not just the presence of the attribute.

This is a more structured proposal than simply accepting any helper returning bool. Library authors would have to identify which operations can participate and preserve those properties as part of the interface. A change to a helper that breaks its promised restricted use would affect callers relying on that contract.

Pointer validity cannot be reduced to non-nullness

The proposed object_address operation conservatively recognizes pointer expressions known to designate objects. The paper includes forms such as this, addresses of certain named objects, and values initialized from expressions already satisfying the property. A false result does not prove that a pointer is invalid. It means the restricted model did not establish the required fact.

That qualification is essential. A non-null pointer may still fail to designate an object whose lifetime permits access. Conversely, useful pointers may fall outside a deliberately narrow syntactic analysis. The proposed rule trades acceptance of some programs for a more constrained set of operations the implementation can analyze.

The paper also restricts builtin indexing to known array objects and constant in-range indices. It treats pointer arithmetic through similarly conservative conditions. These limits would exclude familiar general-purpose code, which is why the relaxed alternative and the possibility of later refinement are substantive parts of the proposal.

My preference is to assess those restrictions through the guarantees they actually support. A conservative predicate language may be valuable without expressing every application property. It still needs a clear account of which useful operations remain outside the guaranteed subset.

The design acknowledges incomplete coverage

R1 does not solve every source of undefined behaviour. Its discussion explicitly leaves general lifetime problems caused by aliasing outside scope. It also offers no particular solution to data races beyond reducing opportunities for them, and excludes undefined behaviour arising from specification gaps or implementation resource limits.

Those limitations qualify the paper's stated ideal of predicates free from undefined behaviour. The concrete proposal reduces particular risks through syntactic and semantic restrictions. Describing that as complete memory safety would overstate what the author says the current design achieves.

The revision also identifies work for standard-library participation. An audit would determine which operations can support non-relaxed predicates and whether their implementations satisfy the restrictions. The proposed guarantees consequently affect the helper functions a contract calls as well as the expression written at the declaration. A sound interface needs both pieces to agree before a compiler can treat predicate evaluation as belonging to the restricted model.