p3487.tex

\input{wg21common}

% Footnotes at bottom of page:
 \usepackage[bottom]{footmisc} 

% Table going across a page: 
 \usepackage{longtable}

 % Start sections at 0
% \setcounter{section}{-1}

% color boxes
\usepackage{tikz,lipsum,lmodern}
\usepackage[most]{tcolorbox}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%TABLE OF CONTENTS SETTINGS

\usepackage{titlesec}
\usepackage{tocloft}

% Custom ToC layout because the default sucks
\cftsetindents{section}{0in}{0.24in}
\cftsetindents{subsection}{0.24in}{0.34in}
\cftsetindents{subsubsection}{0.58in}{0.44in}

% Needed later to reduce the ToC depth mid document
\newcommand{\changelocaltocdepth}[1]{%
  \addtocontents{toc}{\protect\setcounter{tocdepth}{#1}}%
  \setcounter{tocdepth}{#1}%
}

\setcounter{tocdepth}{3}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%POLLS

\definecolor{pollFrame}{rgb}{0,.718,0}
\definecolor{pollBG}{rgb}{.5,1,.5}

\newtcolorbox{wgpoll}[1]{colframe=pollFrame,colback=pollBG!20!white,title={#1}}

\newcommand{\wgpollresult}[5]{%

  \vspace{2mm}
  \begin{tabular}{c | c | c | c | c} %
  SF  & F  & N  & A  & SA \\ %
  \hline %
  #1 & #2 & #3 & #4 & #5 \\ %

  \end{tabular}
  \vspace{2mm}  \\ %
}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{document}
\title{Postconditions odr-using a parameter \\ that may be passed in registers}
\author{
Timur Doumler \small(\href{mailto:papers@timur.audio}{papers@timur.audio}) \\
Joshua Berne \small(\href{mailto:jberne4@bloomberg.net}{jberne4@bloomberg.net}) \\
}
\date{}
\maketitle

\begin{tabular}{ll}
Document \#: & P3487R0 \\
Date: &2024-11-07 \\
Project: & Programming Language C++ \\
Audience: & SG21, EWG
\end{tabular}

\begin{abstract}
This paper considers the case where a non-reference parameter is odr-used in the predicate of a precondition or postcondition assertion and is eligible to be passed via registers. To enable caller-side checking of preconditions and postconditions, we need to add a provision to the the Contracts MVP \cite{P2900R10} that allows the check to observe either the caller-side or the callee-side version of the parameter object. However, for postconditions, this can lead to surprising behaviour. We propose several alternatives for how to address this problem.
\end{abstract}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\tableofcontents*
%\pagebreak

%\section*{Revision history}

%Revision 0 (2024-04-16)
%\begin{itemize}
%\item Original version
%\end{itemize}

%\pagebreak

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

This paper is the second part of a trilogy of papers dealing with known issues in the Contracts MVP \cite{P2900R10} regarding postconditions odr-using non-reference function parameters:
\begin{itemize}
\item \cite{D3484R1} Postconditions odr-using a parameter modified in an overriding function;
\item \cite{D3487R0} Postconditions odr-using a parameter that may be passed in registers;
\item \cite{D3489R0} Postconditions odr-using a parameter of dependent type.
\end{itemize}
These issues should be considered together, and ideally resolved in a consistent way.

\section{Background}
\label{bg}

For efficiency reasons, the major ABIs used for implementations of C++ allow objects to be passed to a function and returned from a function via \emph{registers} when the type of the object satisfies certain requirements. The C++ Standard accommodates such passing and returning via registers in \href{https://timsong-cpp.github.io/cppwp/n4950/class.temporary#3}{[class.temporary]/3} as follows:

\begin{adjustwidth}{0.5cm}{0.5cm}
When an object of class type \tcode{X} is passed to or returned from a function, if \tcode{X} has at least one eligible copy or move constructor ([special]), each such constructor is trivial, and the destructor of \tcode{X} is either trivial or deleted, implementations are permitted to create a temporary object to hold the function parameter or result object. The temporary object is constructed from the function argument or return value, respectively, and the function's parameter or return object is initialised as if by using the eligible trivial constructor to copy the temporary (even if that constructor is inaccessible or would not be selected by overload resolution to perform a copy or move of the object).
\end{adjustwidth}

Effectively, such objects passed and returned via registers do not exist in memory and do not have an address; their value is instead accessed by materialising a temporary copy. In C++ today, this specification peculiarity causes no friction, because there is (with one minor exception\footnote{An object that meets the requirements to be passed in a register may still have a user-provide constructor that may observe its address through the use of \tcode{this}, and that address may then differ from the address seen for the parameter within the function body.}) no context where the pre-temporary copy versions of these objects could be directly observable by the user. 
The current wording does not say it explicitly, but there is an assumption within it that, once a temporary has been created to ``hold the function parameter or result object'', that temporary will be referred to whenever the name that denotes the object is used going forward.

In practice in C++ today, that is always the case. However, the Contracts MVP \cite{P2900R10} adds function-contract assertions (precondition and postcondition assertions). Depending on how we specify them, they could create a new context where the pre-temporary copy versions of  parameter objects and/or return objects are not only observable, but usable by name. We therefore must clarify exactly what semantics we want to allow in those cases, and what that means for implementations and for users.

\section{Discussion}

\subsection{Caller-side checking}

One of the design goals of \cite{P2900R10} is to allow the implementation to perform precondition and postcondition checks either callee-side or caller-side. A discussion of implementation strategies can be found in \cite{P3267R0} and \cite{P3321R0}; a discussion of the motivation and use cases for both caller-side and callee-side checks can be found in \cite{P3228R1}, \cite{P3264R1}, \cite{P3270R0}, \cite{P3321R0}, and references therein. We provide a very brief summary below,.

For callee-side checks, the compiler would emit code to perform the precondition and postcondition checks when compiling the definition of the function. For caller-side checks, the compiler would instead emit code around the function call to perform the checks. Note that the precondition and postcondition assertions are part of the function declaration and thus known at every call site.

Callee-side checks can be emitted in all cases. On the other hand, caller-side checks cannot be emitted in certain cases. One such case is an indirect call (e.g., through a pointer to function or pointer to member function), since the compiler does not know at the call site which concrete function will be called. Another such case is an ABI that requires function parameters to be destroyed callee-side (e.g., the Microsoft ABI), which means that postconditions cannot be checked caller-side without an ABI break, as postconditions must be evaluated before destruction of function parameters.

Even though not all checks can be performed caller-side in all cases, the ability to perform at least \emph{some} caller-side checks is important. With this ability, the user can enable contract checks to diagnose defects when working with a library that has been compiled with contract checks off (it can often be too costly or outright impossible to recompile the library with contract checks on and re-link the program). Caller-side checks also enable an implementation of contract checks on virtual functions as specified in \cite{P2900R10}: the caller-facing contract (that of the statically called function) can be checked caller-side, while the callee-facing contract (that of the final overrider selected by virtual dispatch) can be checked callee-side. Note that only the caller knows the caller-facing contract in this case.\footnote{How one could implement checking the caller-facing contract of a virtual function call on an ABI that requires function parameters to be destroyed callee-side, without forcing an ABI break, is currently still an open question, but this problem is only tangentially related to the problem discussed in this paper.}

\subsection{Preconditions and parameters}
\label{pre}

Precondition checks can only observe objects passed to a function, i.e., the function parameters, not objects returned from the function. \cite{P2900R10} currently does not contain an explicit provision that would allow precondition checks to observe the pre-temporary copy parameter objects. It follows therefore from [class.temporary] that precondition checks must observe the same parameter object as the function body. This makes caller-side precondition checks unimplementable with the current specification.

We can fix this problem by adding an explicit provision to \cite{P2900R10} that a precondition check is implicitly allowed to observe either the pre-temporary parameter object or the temporary copy. If the precondition check observes the pre-temporary object, it will do so before the copy is made to pass the object into a function. If it observes the temporary copy, it will observe the same object as the function body. In either case, there is no problem.

\subsection{Postconditions and the return object}

Unlike precondition checks, postcondition checks can observe both parameters and the return object. \cite{P2900R10} contains an explicit provision that allows postcondition checks to observe either the caller-side or the callee-side version of the return object:

\begin{adjustwidth}{0.5cm}{0.5cm}
If the implementation is permitted to introduce a temporary object for the return value
([class.temporary]), the result name may instead denote that temporary object.
\end{adjustwidth}

This provision is directly observable. Consider:

\begin{codeblock}
class X { /* ... */ };

X f(const X* ptr) post(r: &r == ptr) {
  return X{};
}

int main() {
  X x = f(&x);
}
\end{codeblock}

In the example above, if \tcode{X} is \emph{not} a type eligible to be passed via registers, the postcondition check of \tcode{f} is guaranteed to pass, because \tcode{r} must denote the return object \tcode{x} in \tcode{main()}; however, if \tcode{X} \emph{is} a type eligible to be passed via registers, the postcondition check may\footnote{In practice, whether this check fails will depend on both optimization levels and whether \tcode{f} is inlined into \tcode{main()}.} fail, because \tcode{r} may instead denote a temporary object.

This behaviour may be surprising to a user not familiar with the rules for returning objects via registers, but there is no actual problem --- this behaviour is an exact mirror image of parameters in postcondition assertions. Postcondition checks that refer to the return object may therefore be implemented either caller-side or callee-side with the current specification.

\subsection{Postconditions and parameters}

The third and last case to consider is a postcondition assertion odr-using a non-reference parameter:

\begin{codeblock}
X* ptr;

void f(const X x) post (ptr == &x) {
  ptr = &x;
}
\end{codeblock}

If \tcode{X} is a type eligible to be passed via registers, is this postcondition guaranteed to pass or not?

Just like for precondition assertions, \cite{P2900R10} currently does not contain an explicit provision that would allow postcondition checks to observe the pre-temporary copy parameter objects. It follows therefore from [class.temporary] that postcondition checks, like precondition checks, must observe the same parameter object as the function body; the postcondition assertion above is guaranteed to pass.

This makes caller-side precondition checks unimplementable with the current specification without an ABI break that changes the ABI to no longer pass parameters via registers (other reasons why they might be unimplementable, in particular an ABI that requires function parameters to be destroyed callee-side, notwithstanding).

Just like for the previous two cases, we could add an explicit provision to \cite{P2900R10} that a postcondition check is implicitly allowed to observe either the pre-temporary parameter object or the temporary copy. However, unlike for preconditions, for postconditions the fact that the addresses of the object that the contract assertion sees and the object that the function body sees might be different (which in itself is harmless) is no longer the only observable effect of such a provision. In addition to that, we now also run into the problem that the temporary copy is made when the function is called, but the postcondition assertion is evaluated when the function returns. There is a period in between during which arbitrary code could be executed that can change the state of the parameter object.

\cite{P2900R10} requires every parameter odr-used in a postcondition assertion  to be declared \tcode{const} on all declarations of the function, and requires that function to not be a coroutine, which guarantees that the parameter object that the function body observes is not modified between the function call and its return. However, if the parameter is passed in registers, and the postcondition observes the pre-temporary copy parameter object, these two versions of the parameter object could diverge. This has surprising consequences and renders the postcondition's actual meaning significantly more difficult to reason about. 

In particular, even if the parameter object is \tcode{const}, the function body could still modify any \tcode{mutable} subobjects of that object. If the postcondition assertion is allowed to observe the pre-temporary copy version of the object, it will not see such modifications.

Now, of course we should not write postconditions that directly depend on such mutable state anyway, and if we do, we have already shot ourselves in the foot. But the problem at hand is more subtle: we may have a type whose correctness is connected to that mutable state.

Consider a class \tcode{RandomInteger} holding a random integer value:

\begin{codeblock}
class RandomInteger {
  int _value = rand();
public:
  int value() const { 
    return _value; 
  }
};
\end{codeblock}

The value is computed once when an object of type \tcode{RandomInteger} is created and does not change afterwards. This value is accessible via a public \tcode{value()} member function, which is marked \tcode{const} because it does not change the \emph{observable} state of the object --- it always returns the same value throughout its lifetime.

As an implementation detail, we might compute the value lazily when \tcode{value()} is called for the first time, and cache it afterwards, with no observable change in behaviour:
 \begin{codeblock}
class RandomInteger {
  mutable bool _computed = false;
  mutable int  _value;
public:
  int value() const {
    if (!_computed) {
      _value = rand();
      _computed = true;
    }
    return _value;
  }
};
 \end{codeblock}
Note that our \tcode{RandomInteger} class, as defined above, has a trivial copy constructor and a trivial destructor and is therefore eligible to be passed via registers. This leads to a new footgun: 
 \begin{codeblock}
int f(const RandomInteger i)
post(r: r & i.value() == 0) {
  return ~i.value();
}
 \end{codeblock}
If there is no guarantee that the \tcode{i} in the postcondition assertion refers to the same object as the \tcode{i} in the function body, this code will break. The postcondition assertion will see a different integer value returned from \tcode{i.value()} than the body of the function, and thus fail where it should pass or vice versa, even though for any user reading this code without a deep understanding of objects being passed in registers will see nothing obviously incorrect with this code.

Such code works in C++ today because after the parameter object has been packed into registers and passed to the function,  the original object will never be touched by anything again (remember that the type also needs to have a trivial or deleted destructor, not just an eligible trivial copy or move constructor). However, allowing a postcondition check to observe the original object --- which is required to enable caller-side postcondition checks without an ABI break --- changes that, which creates the footgun above.

We are aware of eight possible options for dealing with this problem. These options are, from most to least restrictive:

% custom enumerators with R prefix:
\renewcommand\labelenumi{R\arabic{enumi}.}
\renewcommand\theenumi\labelenumi

\begin{enumerate}
\item Remove postcondition assertions from \cite{P2900R10} entirely.
\item Make it ill-formed to odr-use \emph{any} function parameter in a postcondition predicate.
\item Make it ill-formed to odr-use any \emph{non-reference} function parameter in a postcondition predicate.
\item  Add an explicit provision that, when a non-reference function parameter is odr-used in a postcondition predicate and the type of the parameter satisfies the requirements for being passed in registers, the corresponding \grammarterm{id-expression} may refer either to the same object as it does in the function body or to the temporary which had been created to initialize the parameter, thereby allowing caller-side checking of a postcondition predicate that odr-uses a non-reference function parameter without an ABI break. Make it ill-formed to odr-use a non-reference function parameter in a postcondition predicate unless the parameter is of scalar type.\footnote{Scalar types are arithmetic types, enumeration types, pointer types, pointer-to-member types, \tcode{std::nullptr_t}, and $cv$-qualified versions of these types. Arithmetic types are integral and floating-point types; integral types include character types and \tcode{bool}.}
\item Add the above provision. Make it ill-formed to odr-use a non-reference function parameter in a postcondition predicate if the type of the parameter satisfies the requirements for being passed via registers, unless it is of scalar type.
\item Add the above provision. Make it ill-formed to odr-use a non-reference function parameter in a postcondition predicate if the type of the parameter satisfies the requirements for being passed via registers and has at least one \tcode{mutable} subobject (applies recursively to all member subobjects, base class subobjects, and array elements).
\item Add the above provision and do nothing further. A postcondition may odr-use a non-reference function parameter of any type.
\item Do not add the above provision. Instead, clarify that when a non-reference function parameter is odr-used in a postcondition predicate, the corresponding \grammarterm{id-expression} must refer to the same object as it does in the function body (status quo in \cite{P2900R10}); caller-side checking of a postcondition predicate that odr-uses a non-reference function parameter remains impossible without an ABI break. A postcondition may odr-use a non-reference function parameter of any type.
\end{enumerate}

We enumerated the options with an ``R'' prefix (for ``registers''), to distinguish them from the options from \cite{D3484R1} that have a ``V'' prefix (for ``virtual'') and the options from \cite{D3489R0} that have a ``D'' prefix (for ``dependent'').

Below we discuss the tradeoffs of each option.

\subsection*{Option R1}

Option~R1 would be a rather drastic measure at this point. However, consider that postcondition assertions are significantly more difficult to specify than preconditions (see \cite{P1323R2}, \cite{P3007R0}, and \cite{P3098R0}), and unlike preconditions, postcondition assertions have so far already generated several known issues that needed fixing in the specification of \cite{P2900R10} (see \cite{P3387R0}, \cite{P3460R0}, \cite{P3483R0}, \cite{D3484R1}, and \cite{D3489R0}). Option~R1 would remove \emph{all} known and unknown footguns from postcondition assertions by removing the feature itself.

We believe that \cite{P2900R10} would still be viable and useful without postcondition assertions. Postcondition assertions have significantly fewer uses than precondition assertions, and their value can to a certain extent also be achieved with good unit test coverage. 

For the record, the option of removing postcondition assertions from the Contracts MVP was once before polled in SG21:

\begin{wgpoll}{SG21 Poll, Teleconference 2021-12-14}
Postconditions should be in the MVP at this time.
\wgpollresult{1}{7}{3}{4}{1}
Result: Marginal consensus (if at all).
\end{wgpoll}

\subsection*{Option R2}

Option~R2 is likewise less than ideal in our opinion, because it significantly limits the set of postconditions we can write, and thus significantly limits the usefulness of the feature, until we can add postconditions captures \cite{P3098R0} to the Standard.

This option becomes more appealing if we include \cite{P3098R0} in the first version of Contracts that we ship. Postcondition captures would never be referencing parameters in a place they cannot be referenced today, so they would not be impacted by this issue at all. However, capturing parameters for use in a postcondition predicate incurs the cost of a copy, which in many cases is not conceptually necessary, thus violating the ``do not pay for what you do not use'' design principle of C++ (see also \cite{D3484R1} Option~R1, which suffers from the same issue).


\subsection*{Option R3}

Option~R3 is similar to Option~R2, except that it allows reference parameters, which are not affected by any of the issues surrounding copies of objects and are not affected by postcondition captures as proposed in \cite{P3098R0}.

However, allowing only reference parameters still significantly limits the set of postconditions we can write. In addition, it encourages users to pass parameters by-reference instead by-value as this would be the only way to make the postcondition assertion compile, which can lead to more error-prone and less efficient code for types where we might normally recommend pass-by-value. We therefore do not consider Option~R3 to be an improvement over Option~R2.

\subsection*{Option R4}

Option~R4 allows by-value parameters of types that are not affected by the footgun and cannot be changed such that they would be affected by the footgun, i.e., scalar types. This would already enable many more useful postconditions compared to Options R1 --- R3.

However, if we were to change the type of a parameter from a built-in type to a user-defined type, for example from \tcode{int} to \tcode{BigInt}, or from \tcode{double} to \tcode{std::complex<double>}, the postcondition would stop compiling, with no workaround available. Additionally,  Option~R4 would make it significantly harder to add postconditions to generic code, including any templates designed to work with both built-in and user-defined types (which includes almost everything in the Standard Library and vast amounts of other generic libraries).

\subsection*{Option R5}

Option~R5 is a relaxation of Option~R4. It allows by-value parameters of scalar type (disallowing them would remove the ability to write many simple and useful postcondition assertions), and in addition, it allows by-value parameters of any type as long as they are \emph{not} eligible to be passed via registers and therefore cannot not affected by the footgun.

One downside of this approach is that most users will not be familiar with the rules around types eligible to be passed in registers, which means that the compiler error they get will likely be very confusing to them. Worse, the definition of user-defined types can change over time, which makes this option brittle. That a particular type is \emph{not} eligible to be passed via registers is not something that code should guarantee to its clients indefinitely in all cases; conversely, making a type trivially copyable and/or movable and trivially destructible should not break client code.

We made a similar choice to not discriminate on particular type traits in the postcondition assertions of a function when we decided that whether a type is trivially movable should not affect whether a non-reference parameter of that type can be odr-used in the postcondition assertion of a coroutine (i.e., when we rejected \cite{P3387R0} Option 5b). Choosing Option~R5 here would be inconsistent with that design choice.

\subsection*{Option R6}

Option~R6 is a further relaxation of Option~R5. It carves out the narrowest possible prohibition on parameter types that can be odr-used in a postcondition predicate --- any type is allowed as long as it does not have the exact property that can lead to the footgun: types that are eligible to be passed in registers \emph{and} have \tcode{mutable} subobjects.

Option R6 is the least prohibitive option that both avoids the footgun and allows implementing caller-side postcondition checks without an ABI break. However, it suffers from the same problem as Option~R5: a very specific and seemingly unrelated change to a type can lead to the postcondition no longer compiling. For Option~R6, the error would be even less obvious for Option~R5, as it would occur when the user decides to add a \tcode{mutable} member to a type that happens to be eligible to be passed in registers, e.g. when the user does a refactoring such as the one we did with \tcode{RandomInteger} above, which is a relatively common technique. The result is brittle code, a very hard-to-understand compiler error, and no good workaround.

\subsection*{Option R7}

Option~R7 makes the behaviour of postconditions with respect to objects passed to a function in registers consistent with the behaviour for objects returned from a function in registers, as well as with the behaviour of preconditions as proposed in Section~\ref{pre}. Option~R7 is therefore arguably the optimal choice with respect to having a straightforward specification and implementation of the feature, enabling caller-side checking, avoiding ABI issues, not making any user code unnecessarily ill-formed, and not imposing any unnecessary run-time cost on the user.

However, the tradeoff of Option~R7 is that it adds the above footgun to the C++ language. Note that the footgun only occurs in rare edge cases, in particular when a \tcode{const} object eligible to be passed via registers is used as a non-reference parameter and its type relies on mutable state for its correctness, and a postcondition assertion would break if it happens to observe an earlier version of that mutable state. Note further that such cases could potentially be mitigated by an implementation issuing a warning if a type eligible to be passed in registers has \tcode{mutable} subobjects, is used as the type of a non-reference function parameter, and that parameter is odr-used in a postcondition assertion of that function or another function that that function overrides.

\subsection*{Option R8}

Option~R8 is a confirmation of the status quo. It is the only solution that both avoids the above footgun and is not a breaking change to \cite{P2900R10}: postconditions odr-using a \tcode{const} non-reference parameter of a non-coroutine function remain well-formed. Option~R8 is therefore arguably the optimal choice with respect to the immediate user experience when dealing with code such as the above.

However, Option~R8 also comes with a high cost: implementing caller-side postcondition checks remains impossible without an ABI break. The necessary ABI break to enable caller-side postcondition checks --- and by extension, to implement full contract checks on virtual functions as specified by \cite{P2900R10} --- would consist of no longer passing function parameters via registers if they are odr-used in the postcondition assertion. However, imposing an ABI break on all users who wish to add postcondition assertions to their functions would arguably do significant harm to the adoption of Contracts in the C++ ecosystem, which is why one of the fundamental design principles of the Contracts MVP (\cite{P2900R10} Principle 16) is to avoid such an ABI break.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\pagebreak
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Proposal}

With regards to parameters odr-used in \emph{preconditions}, we propose to add a provision to \cite{P2900R10} that a precondition check is implicitly allowed to observe either the pre-temporary parameter object or the temporary copy, as discussed in Section~\ref{pre}.

With regards to parameters odr-used in \emph{postconditions}, we believe that Options R1 --- R8 are all worth considering, and propose all of them to determine which option has more consensus in SG21. A summary of the tradeoffs for each option can be found in Table~\ref{tradeoffs}.

Note that there are three requirements that are \emph{impossible} to satisfy simultaneously --- we need to choose two. These requirements are: allowing a postcondition predicate to odr-use non-reference parameters of \emph{any} type; avoiding the footgun created by parameter objects with \tcode{mutable} subobjects; and allowing caller-side checking of postconditions that odr-use non-reference parameters without an ABI break that removes passing via registers. If we are willing to abandon the first requirement, we can choose between Options R1 --- R6, which offer a spectrum between most restrictive and most brittle; if we are willing to abandon the second requirement, the optimal solution is Option~R7; if we are willing to abandon the third requirement, the optimal solution is Option~R8.

Options R1 --- R3 do not offer any advantage over Options R4 --- R6 with regards to the specific issues discussed in this paper. However, R1 --- R3 may still be interesting because they would remove the source of the issues discussed in the two companion papers \cite{D3484R1} and \cite{D3489R0}. 

Note further that all options except Option~R8 form a chain of successive relaxations of the previous option. Therefore, choosing Option~R1 would leave the door open to adopting Options R2 --- R7 without breaking changes at some point in the future; Option~R2 could be evolved towards Options R3 --- R7, but not R1, etc. On the other hand, Option~R8 is mutually exclusive with any of the other options: an evolution from any of the other options towards Option~R8, or in the other direction, is impossible without breaking changes.

Note finally that choosing Option R4 would be consistent with a possible relaxation of the rule for postconditions on coroutines to also accept non-reference parameters of scalar type.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\yes}{\includegraphics[width=4mm]{images/yes.png}}
\newcommand{\no}{\includegraphics[width=4mm]{images/no.png}}
\newcommand{\maybe}{\includegraphics[width=4mm]{images/maybe.png}}
%\vspace{4mm}
\begin{table}[b]
\begin{tabular}{|p{5.4cm}|p{0.9cm}|p{0.9cm}|p{0.9cm}|p{0.9cm}|p{0.9cm}|p{0.9cm}|p{0.9cm}|p{0.9cm}|}
\hline 
& R1 & R2 & R3 & R4 & R5 & R6 & R7 & R8 \\
\hline
Allows postcondition assertions in general & \no & \yes  & \yes  & \yes & \yes & \yes & \yes & \yes \\ \hline
Allows odr-using reference parameters & \no & \no  & \yes  & \yes & \yes & \yes & \yes & \yes \\ \hline
Allows odr-using non-reference parameters of at least scalar type& \no & \no  & \no  & \yes & \yes & \yes & \yes & \yes \\ \hline
Allows odr-using non-reference parameters of any type& \no & \no  & \no  & \no & \no & \no & \yes & \yes \\ \hline
Avoids brittle discrimination based on certain type traits& \yes & \yes  & \yes  & \maybe & \no & \no & \yes & \yes \\ \hline
Makes it impossible to shoot yourself with the footgun& \yes & \yes  & \yes  & \yes & \yes & \yes & \no & \yes \\ \hline
Allows caller-side postcondition checking without ABI break& \yes & \yes  & \yes  & \yes & \yes & \yes & \yes & \no \\ \hline
\end{tabular}
\vspace{2mm}
\caption{Main tradeoffs of proposed options R1 --- R8. Discriminating on whether the parameter is of scalar type (R4) is marked with a question mark because it is significantly less brittle than discriminating based on more complicated and non-obvious type traits (R5 and R6).}
\label{tradeoffs}
\end{table}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\pagebreak
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Wording}

The proposed wording changes are relative to the wording proposed in \cite{P2900R10}.

\subsection*{Preconditions}

Modify [dcl.contract.func] as follows:

\begin{adjustwidth}{0.5cm}{0.5cm}
\added{If the predicate of a precondition assertion of a function odr-uses ([basic.def.odr]) a non\-reference parameter of that function, and the implementation is permitted to introduce a temporary object for the parameter object value ([class.temporary]), it is unspecified whether the corresponding \grammarterm{id-expression} in the predicate of the precondition assertion denotes that temporary object or the original parameter object.} If the predicate of a postcondition assertion of a function odr-uses \removed{([basic.def.odr]) }a non\-reference parameter of that function, that parameter shall be declared \tcode{const} and shall not have array or function type. 
\begin{note}
This requirement applies even to declarations
that do not specify the \grammarterm{postcondition-specifier}. Arrays and functions are still usable when declared with the equivalent pointer types ([dcl.fct]).
\end{note}
\begin{example}
\tcode{[...]}
\end{example}
\end{adjustwidth}

\subsection*{Postconditions --- Option R1}

Remove all wording that relates to:
\begin{itemize}
\item The \tcode{post} identifier with special meaning;
\item The \emph{postcondition-specifier} and \emph{result-name-introducer} grammar non-terminals;
\item Postcondition assertions and result names;
\item The \tcode{post} enumeration value in \tcode{std::contracts::assertion_kind}.
\end{itemize}
The exact wording diff is not provided here due to its length.

\subsection*{Postconditions --- Option R2}

Modify [dcl.contract.func] as follows:

\begin{adjustwidth}{0.5cm}{0.5cm}
If the predicate of a postcondition assertion of a function odr-uses ([basic.def.odr]) a
\removed{non\-reference }parameter of that function, \removed{that parameter shall be declared \tcode{const} and shall not have array or function type}\added{the program is ill-formed}.
\begin{note}
This requirement applies even to declarations
that do not specify the \grammarterm{postcondition-specifier}. Arrays and functions are still usable when declared with the equivalent pointer types ([dcl.fct]).
\end{note}
\begin{example}
\tcode{[...]}
\end{example}
\end{adjustwidth}

\subsection*{Postconditions --- Option R3}

Modify [dcl.contract.func] as follows:

\begin{adjustwidth}{0.5cm}{0.5cm}
If the predicate of a postcondition assertion of a function odr-uses ([basic.def.odr]) a
non-reference parameter of that function, \removed{that parameter shall be declared \tcode{const} and shall not have array or function type}\added{the program is ill-formed}.
\begin{note}
This requirement applies even to declarations
that do not specify the \grammarterm{postcondition-specifier}. Arrays and functions are still usable when declared with the equivalent pointer types ([dcl.fct]).
\end{note}
\begin{example}
\tcode{[...]}
\end{example}
\end{adjustwidth}

\subsection*{Postconditions --- Option R4}

\begin{adjustwidth}{0.5cm}{0.5cm}
If the predicate of a postcondition assertion of a function odr-uses ([basic.def.odr]) a
non-reference parameter of that function, that parameter shall be declared \tcode{const} and shall \removed{not have array or function type}\added{have scalar type ([basic.types.general])}.
\begin{note}
This requirement applies even to declarations
that do not specify the \grammarterm{postcondition-specifier}.\removed{ Arrays and functions are still usable when declared with the equivalent pointer types ([dcl.fct]).}
\end{note}
\begin{example}
\tcode{[...]}
\end{example}

\added{If the implementation is permitted to introduce a temporary object for the parameter object value ([class.temporary]), it is unspecified whether the corresponding \emph{id-expression} in the predicate of a postcondition assertion denotes that temporary object or the original parameter object.}
\end{adjustwidth}

\subsection*{Postconditions --- Option R5}

\begin{adjustwidth}{0.5cm}{0.5cm}
If the predicate of a postcondition assertion of a function odr-uses ([basic.def.odr]) a
non-reference parameter of that function, that parameter shall be declared \tcode{const} and shall not have array or function type. \added{If the parameter has a type for which the implementation is permitted to create a temporary object to hold the function parameter ([class.temporary]), it shall have scalar type ([basic.types.general]).}
\begin{note}
This requirement applies even to declarations
that do not specify the \grammarterm{postcondition-specifier}. Arrays and functions are still usable when declared with the equivalent pointer types ([dcl.fct]).
\end{note}
\begin{example}
\tcode{[...]}
\end{example}

\added{If the implementation is permitted to introduce a temporary object for the parameter object value ([class.temporary]), it is unspecified whether the corresponding \emph{id-expression} in the predicate of a postcondition assertion denotes that temporary object or the original parameter object.}
\end{adjustwidth}

\subsection*{Postconditions --- Option R6}

Modify [dcl.contract.func] as follows:

\begin{adjustwidth}{0.5cm}{0.5cm}
If the predicate of a postcondition assertion of a function odr-uses ([basic.def.odr]) a
non-reference parameter of that function, that parameter shall be declared \tcode{const} and shall not have array or function type. \added{If the parameter has a type for which the implementation is permitted to create a temporary object to hold the function parameter ([class.temporary]), it shall not have any \tcode{mutable} subobjects ([dcl.stc]).}
\begin{note}
This requirement applies even to declarations
that do not specify the \grammarterm{postcondition-specifier}. Arrays and functions are still usable when declared with the equivalent pointer types ([dcl.fct]).
\end{note}
\begin{example}
\tcode{[...]}
\end{example}

\added{If the implementation is permitted to introduce a temporary object for the parameter object value ([class.temporary]), it is unspecified whether the corresponding \emph{id-expression} in the predicate of a postcondition assertion denotes that temporary object or the original parameter object.}
\end{adjustwidth}

\subsection*{Postconditions --- Option R7}

Modify [dcl.contract.func] as follows:

\begin{adjustwidth}{0.5cm}{0.5cm}
If the predicate of a postcondition assertion of a function odr-uses ([basic.def.odr]) a
non-reference parameter of that function, that parameter shall be declared \tcode{const} and shall not have array or function type.
\begin{note}
This requirement applies even to declarations
that do not specify the \grammarterm{postcondition-specifier}. Arrays and functions are still usable when declared with the equivalent pointer types ([dcl.fct]).
\end{note}
\begin{example}
\tcode{[...]}
\end{example}

\added{If the implementation is permitted to introduce a temporary object for the parameter object value ([class.temporary]), it is unspecified whether the corresponding \emph{id-expression} in the predicate of a postcondition assertion denotes that temporary object or the original parameter object. [ \emph{Note:} It follows that, for objects that can be passed in registers, the postcondition assertion might not see any modifications of \tcode{mutable} subobjects ([dcl.stc]) of the parameter object performed by the function or a function overriding it. --- \emph{end note} ]}
\end{adjustwidth}

\subsection*{Postconditions --- Option R8}

Modify [dcl.contract.func] as follows:

\begin{adjustwidth}{0.5cm}{0.5cm}
If the predicate of a postcondition assertion of a function odr-uses ([basic.def.odr]) a
non-reference parameter of that function, that parameter shall be declared \tcode{const} and shall not have array or function type.
\begin{note}
This requirement applies even to declarations
that do not specify the \grammarterm{postcondition-specifier}. Arrays and functions are still usable when declared with the equivalent pointer types ([dcl.fct]).
\added{An \emph{id-expression} that denotes a non-reference parameter in the predicate of a postcondition assertion denotes the same object as in the function body, even if the implementation is permitted to introduce a temporary object for the parameter object value ([class.temporary]).}
\end{note}
\begin{example}
\tcode{[...]}
\end{example}
\end{adjustwidth}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section*{Acknowledgements}
Thanks to Alisdair Meredith, John Lakos, Jens Maurer, and Mungo Gill for their helpful remarks during drafting of this paper. Thanks to Oliver Rosten for his review of the paper.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Remove ToC entry for bibliography
\renewcommand{\addcontentsline}[3]{}% Make \addcontentsline a no-op to disable auto ToC entry

%\renewcommand{\bibname}{References}  % custom name for bibliography
\bibliographystyle{abstract}
\bibliography{ref}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\end{document}