On Wed, 4 Jun 2025 at 00:48, Tom Honermann <tom_at_[hidden]> wrote:
> 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);

The fact that a pre/post injects, using the enforce semantic, is that
in the code following it, the predicate is true, because otherwise the
program would
have terminated.

That doesn't provide means to make the rest of the program, in
particular the calling code, faster. If that code has a condition
equivalent to the predicate,
the predicate can be elided, so adding it didn't make the program
slower. If such an equivalent condition isn't there, adding the
contract predicate
makes the program slower.

Relying on a hypothetical assume semantic doesn't help, especially
because using that makes it not the same program, the compiled-altered
program
has different semantics.

In other words, the answer to the question
> When does that make a program containing those pre/post run faster
> than a program that doesn't contain them?

is "it doesn't".