Search code examples
c++language-lawyerc++23assumption

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

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?

Solution

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