[PATCH] implement pre-c++20 contracts

Jeff Chapman jchapman@lock3software.com
Wed Nov 13 19:23:00 GMT 2019


Hello,

Attached is a patch that implements pre-c++20 contracts. This comes
from a long running development branch which included ChangeLog entries
as we went, which are included in the patch itself. The repo and
initial wiki are located here:
https://gitlab.com/lock3/gcc-new/wikis/GCC-with-Contracts

We've previously circulated a paper (P1680) which documents our
implementation experience which largely covers new flags and features.
http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2019/p1680r0.pdf

That paper documents our changes in depth, barring the recently added
-fcontracts flag which is a global opt-in for contracts functionality.
As an overview of what we've done is included below for convenience.

The following switches have been added:

-fcontracts
  enable contract features in general

Flags from the old Working Draft:

-fcontract-build-level=[off|default|audit]
  specify max contract level to generate runtime checks for

-fcontract-continuation-mode=[on|off]
  toggle whether execution resumes after contract failure

Flags from P1290:

-fcontract-assumption-mode=[on|off]
  enable treating axiom level contracts as compile time assumptions
  (default on)

Flags from P1429:

-fcontract-mode=[on|off]
  enable or disable all contract facilities (default on)

-fcontract-semantic=<level>:<semantic>
  specify the concrete semantics for a level

Flags from P1332:

-fcontract-role=<name>:<semantics>
  specify semantics for all levels in a role (default, review, or a
    custom role)
  (ex: opt:assume,assume,assume)

Additional flags:

-fcontract-strict-declarations=[on|off]
  toggle warnings on generalized redecl of member functions
    without contracts (default off)


One assert contract may be present on any block scope empty statement:
  [[ assert contract-mode_opt : conditional-expression ]]

Function declarations have an optional, ordered, list of pre and post
contracts:
  [[ pre contract-mode_opt : conditional-expression ]]
  [[ post contract-mode_opt identifier_opt : conditional-expression ]]


The grammar for the contract-mode_opt portion which configures the
concrete semantics of the contracts is:

contract-mode
  contract-semantic
  contract-level_opt contract-role_opt

contract-semantic
  ignore
  check_never_continue
  check_maybe_continue
  check_always_continue
  assume

contract-level
  default
  audit
  axiom

contract-role
  %default
  %identifier


Contracts are configured via concrete semantics or by an optional
level and role which map to one of the concrete semantics:

  ignore – The contract does not affect the behavior of the program.
  assume – The condition may be used for optimization.
  never_continue – The program terminates if the contract is
                   not satisfied.
  maybe_continue – A user-defined violation handler may terminate the
                   program.
  always_continue – The program continues even if the contract is not
                    satisfied.


-fcontracts enables generalized member function redeclaration. That is,
non-defining declarations of member functions are allowed outside the
initial class definition.

Contracts are not required on the initial declaration of a
(non-virtual) function as long as all TUs that see a set of contracts
eventually see the same set of contracts. All contracts must be present
on the first declaration for virtual functions to ensure we know to
split the function in all overrides.


Explicit template specializations have an independent set of contracts
than any other explicit specializations.


Functions with contracts (which we call guarded functions) are split
just before genericization. A wrapper which checks pre and post
contracts is emitted with the original function name, while the
original function body is emitted under a new unchecked name. This
means that calls to functions in TUs which never see the contract list
still call a checked version of the function (see insulated contracts
in P1680).

Having a checked and unchecked version of the function makes it
potentially easier to inline the checks into the caller, and prevents
the need to repeat the post contracts at all return statements in the
original function.


A custom contract violation handler can be installed by defining
  void handle_contract_violation(const std::contract_violation &)

(you must #include <contract> for this to work) or by using LD_PRELOAD.
An example of defining the handler in the main TU can be found in the
testsuite g++.dg/cpp2a/contracts16.C .

Examples of how to use LD_PRELOAD to install a custom violation handler
are available in the contracts folder inside the testsuite.


Bootstrapped and tested on x86_64-pc-linux-gnu. cmcstl2 compiles cleanly
and has no `make test` failures.


Please let me know if you have any questions or know what the next
steps will be.


Thank you,
Jeff Chapman II
-------------- next part --------------
A non-text attachment was scrubbed...
Name: 0001-Implement-pre-c-20-contracts.patch.gz
Type: application/gzip
Size: 95619 bytes
Desc: not available
URL: <http://gcc.gnu.org/pipermail/gcc-patches/attachments/20191113/c78b54cf/attachment.gz>


More information about the Gcc-patches mailing list