Document number:   P2182R0
Date:   2020-06-15
Audience:   SG21
Reply-to:  
Andrzej Krzemieński <akrzemi1 at gmail dot com>
Ryan McDougall
Joshua Berne

Contract Support: Defining the Minimum Viable Feature Set

We observe that "C++20 contracts" consisted of two parts. One part was clear, well understood, widely agreed upon, and useful to various groups of C++ users. The other part rose a lot of controversies for various reasons and ultimately led to the removal of the entire feature.

In paper [P2114r0] we have listed a subset of use cases we believe represent useful improvements to the language, offer a incalculable positive value for most users, and reflect the uncontroversial part of "C++20 contracts". In this paper we provide the rationale for our choice. We wish to show that our selection:

Analysis

In this document we use the term C++20 Contracts to refer to contract support facilities in C++ Standard draft just before the removal — [N4820] (which is effectively equivalent to [P0542R5]) — as well as pieces of the associated proposals seen by EWG that had support in polling, such as:

[P2076r0] lists the points the disagreements about the previous incarnation of contracts design:

We claim that if we eliminated or reduced the use cases for the above features, the remainder would still be a valuable and usable feature that would offer a great help in enforcing program correctness. The value in preventing bugs and enforcing program correctness comes from being able to

  1. express preconditions, postconditions, and assertions as C++ predicates
  2. transform them into runtime-checks at an all-or-none granularity, leaving open the design of finer control to future work

In the reminder of the paper we elaborate on the features of MVP and show how they are motivated by the use cases nominated in [P2114r0]. We also discuss how the support for the remaining use cases can be added atop of MVP in subsequent phases.

Features in MVP

We selected the minimal use cases to allow the widest benefit for the most general section of users, without resorting to known points of contention. We had in mind a simple feature that consisted of the existing contract syntax, a single build option to enable or disable checks, and a (conditionally) user- definable violation handler that is invoked when checks are enabled and violated.

Contract declarations

The most important thing is the ability to express the predicates in function declarations as compiler-checked C++ expressions. This is uncontroversial. This enables:

In fact, this feature alone would already satisfy many users.

Use cases covered:

Turning on and off all runtime checks

We believe it is essential that we meet two somewhat contradictory requirements:

  1. A guarantee that some action is taken whenever a contract is violated
  2. A guarantee that there is no runtime overhead for encoded contracts

The former is a correctness requirement, and the latter is performance requirement (after assurance — further discussion about assurance can be found in [P1517R0]).

This suggests that there needs to be at least some control over what contracts can do at build time. For the MVP we suggest a single flag which turns checking "on" or "off", where:

This is a subset of what [P0542R5] offered, and should come with similar caveats that that proposal had for build modes — where mixing modes is only conditionally supported.

Finer-grained control and additional semantics to failed checks would be left to extensions and future proposals.

Use cases covered:

Reporting contract violation

On platforms where it makes sense, each contract violation detected at run-time should be reported to the users — including what failed and where in the source code.

Use cases covered:

Customizing how failures are reported

The semantics and implementation of contract violation handling has significant impact on the extensibility and usability of the feature. It may be premature to codify within an MVP, as it may reduce the applicability of the feature to a significant portion of use cases. For the MVP, we think that as offered in [P0542R5], implementations are not required to offer customizable violation handlers.

Note that in practice, it is expected that most implementations will allow users to define a custom violation handler. This will let users experiment with many variations before bringing them to the committee, and do so in a way that is portable across all compilers that do allow customizability. Compilers that do not allow user-defined violation handlers would instead document what their (default or other selectable) violation handler will do when invoked.

Other use cases related to contract semantics can be met or at least approximated with the choice of specific violation handlers, and we seek to avoid limiting that decision in this proposal. For this reason we would not propose requiring that user defined violation handlers be [[noreturn]], and we suggest no other behavior related to a violation other than the invocation of the violation handler

Use cases covered (implementation defined):

Features not in MVP

Continuation after failed run-time check

The use case that continuation mode was trying to address are sdev.maturity and large.newcompiler. They can be introduced on top of MVP as annotations on individual contract declarations (as described in [P1332R0]), and additionally requiring more build modes.

In addition to that, by only specifying that a violation handler is invoked and not extending that to any other fixed functionality associated with a violation (such as always terminating) we allow for users to remain in control of this decision when choosing compilers that provide selectable violation handlers.

Contract Levels

The use cases that contract levels, such as default and audit, tried to address are crit.more.coverage, dev.reason.cost and crit.production.checking. The goal was to indicate "this predicate is more expensive to evaluate than the function it protects", but the design of this feature had flaws:

They can be introduced on top of MVP as annotations indicating how expensive a contract statement is relative to the body of the function.

Global Toggles (also known as: external remapping controls)

If there are no levels in contract declarations in the MVP, there is no need for having build levels either, other than on/off switch. They can be added later if needed.

Literal Semantics (also known as: in-source controls)

They were never in the draft, but were discussed widely, and had some EWG support in polling. There were concerns that they

  1. would encourage the use of macros
  2. were not basic/necessary building blocks

However they can easily be added atop of MVP in future version by adding meta-information to contract declarations.

Assumptions or injected facts

This was highly controversial. An extended analysis can be found in [P2064r0]. Use cases covered: pdev.footgun and hardware.performance.

pdev.footgun can be handled by a separate feature, such as [P1774r3]. Alternatively, it could be implemented atop of MVP by adding special meta-information to individual contract declarations.

hardware.performance could be implemented atop of MVP by introducing a yet another build mode. Alternatively, users could achieve it with MVP by installing a custom violation handler with __builtin_unreachable().

Indicating inexpressible predicates

This woud cover use cases qdev.tooling.control and api.express.unimplementable. Controversies arose because of mixng inexpressibility with levels, and taking word "axiom" to mean __builtin_assume().

Can be implemented atop of MVP either as meta-information on contract declarations, or by annotating functions as inexpressible as described in [P2176r0].

Conclusion

While the proposed MVP is conservative, we believe that even the MVP may contain a number of unresolved small issues that will require time to polish. With EWG attention almost entirely consumed by controversial bits of C++20 contracts, the uncontroversial bits may not have been given sufficient consideration for attention. If we are to ship any contract programming support in C++23 time frame, we have to be sure that we have a small enough scope to be accommodated by the WG21 process.

The biggest advantage of this MVP is that we provide a standard notation for expressing preconditions and postconditions. This notation will be consumed by many tools, which are not necessarily compilers. The positive effect on the community is not necessarily in what compilers can do with it, but also what other automated tools can get from it. This is far beyond the scope of the C++ Standard.

References