On 6/4/25 8:48 AM, Ville Voutilainen wrote:
> 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.
Yes, agreed.
>
> 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.
I agree that a checked predicate won't affect the calling code, but as
you noted, it can cause later branches to be elided that otherwise would
not have been thereby leading to a faster program. This isn't novel or
specific to contracts, it is a consequence of constraining possible
values along more control flows. This isn't an in-principle argument
since a whole program analysis can do the same. In practice, it could
improve optimization; to what extent I don't know though.
>
> 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.

The semantics are only different, discounting side effects of contract
predicate evaluation, if an assume semantic is violated.

We already have what is effectively an assume semantic though it has a
weird spelling. It is written as an assumption that repeats all of a
function's contracts (to the extent that is possible) prior to each call
to the function.

>
> 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".

I guess we'll see.

Tom.