On Tue, 3 Jun 2025 at 19:24, Tom Honermann <tom@honermann.net> wrote:

I think something like the following suffices for what was proposed.

double compute_sqrt(double arg) pre (arg > 0.0); inline double sqrt(double arg) { if (arg < -0.0) return std::numeric_limits<double>:: quiet_NaN(); if (arg == 0.0 /* or is +/- infinity or is a NaN*/) return arg; return compute_sqrt(arg); } double get_definite_positive_value() post(r: r >= 0.0); double f() { double d = get_definite_positive_value(); return sqrt(d); }

I understand that this doesn't address (some of) what the proposer wanted since it requires that the checks to be optimized away are exposed in the TU where the call is made. However, that constraint is also present in the technical specifications of the proposal.

When does that make a program containing those pre/post run faster
than a program that doesn't contain them?

Per [basic.contract.eval]p5 in the P2900 proposed wording, an implementation is not required to evaluate a contract predicate if it has some other means of knowing what the result of evaluation would be. A conforming implementation can elide checks when it has already identified constraints on the possible values a variable may hold such that a predicate evaluation would be unnecessary. This can occur when:

• The possible values are constrained by static analysis (e.g., a data flow analysis of get_definite_positive_value()), or
  
• The possible values are constrained by a previous evaluation (e.g., the evaluation of the postcondition of get_definite_positive_value()), or
• The possible values are constrained by an [[assume(expr)]] attribute. For example:
  double g() {
    double d = get_definite_positive_value();
    [[assume(d > 0.0)]];
    return sqrt(d);
  }

A non-conforming implementation can also provide an assume semantic whether or not WG21 approves of it.

The checks that the post author wanted to elide in this example are not contract checks; they are just typical condition checks and their evaluation is subject to the as-if rule. Explicit preconditions and postconditions inject facts (subject to verification) that may be used by an optimizer accordingly. I'm sure you recall SG21 discussion, and even some implementation reporting, regarding the potential for such injected facts to improve code generation and performance even when a checking contract semantic is selected. The presence of preconditions and postconditions can constrain the possible executions of the program such that some subset of all potential condition evaluations can be elided.

On, and I now see that I messed up the postcondition for get_definite_positive_value(). That should, of course, have been:

double get_definite_positive_value()
  post(r: r > 0.0);

Tom.