What happens when an assumption, i.e. [[assume]] contains UB?

Question

In C++23, the [[assume(expression)]] attribute makes it so that if expression is false, the behavior is undefined. For example:

int div(int x, int y) {
    [[assume(y == 1)]];
    return x / y;
}

This compiles to the same code as if y was always 1.

div(int, int):
        mov     eax, edi
        ret

However, what happens if there is another level of undefined behavior?

int div(int x, int y) {
    [[assume(x / 0 == 1)]];
    return x / y;
}

Now there is UB inside the assumption, but the assumption is not evaluated. What does this mean? Is it just nonsense or can the compiler do anything with this assumption?

Answer 1

From [dcl.attr.assume]:

The expression is not evaluated.

So the undefined behavior of the expression does not immediately imply undefined behavior of the program with the given inputs.

However it continues:

If the converted expression would evaluate to true at the point where the assumption appears, the assumption has no effect. Otherwise, the behavior is undefined.

Either the evaluation of an expression that would have undefined behavior is not an evaluation of the expression that evaluates to true and the behavior of the program would be undefined per the "Otherwise" sentence as well, or alternatively, if you consider it unspecified whether or not "If the converted expression would evaluate to true at the point where the assumption appears" is satisfied if the evaluation would have undefined behavior, then it would still not be specified whether or not the "Otherwise" branch is taken and so there will again be undefined behavior overall, since undefined behavior for one choice of unspecified behavior implies undefined behavior overall.

This is specifically addressed in the proposal P1774 in chapter 4.3. as a subtle difference between the decision to make behavior undefined if the assumption does not evaluate to true vs. making the behavior undefined if the assumption evaluates to false.

This way it is for example possible to write assumptions like x + y == z without the compiler having to consider the special case of signed overflow, which might make the assumption unusable for optimization.

Answer 2

All the standard currently says is:

The expression is contextually converted to bool ([conv.general]). The expression is not evaluated. If the converted expression would evaluate to true at the point where the assumption appears, the assumption has no effect. Otherwise, the behavior is undefined.

Now, this sounds a bit contradictory, as if an expression is not evaluated, how can it "evaluate to true". But that's what "would" is about. The expression isn't evaluated, but if it was evaluated, would it result in "true"?

Here's the thing though: undefined behavior is undefined. The result of evaluating an expression that provoked UB is... undefined because that's what "undefined behavior" means:

However, if any such execution contains an undefined operation, this document places no requirement on the implementation executing that program with that input (not even with regard to operations preceding the first undefined operation).

So, would an expression with UB evaluate to "true"? The most reasonable answer is no, because its behavior is undefined. There are no requirements on any particular behavior. And if it does not result in "true", then the program has UB.