What happens if an assumption, i.e. [[assume]] fails in a constant expression?

Question

In C++23, the [[assume(conditonal-expression)]] attribute makes it so that if conditional-expression doesn't evaluate to true, 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

As commenters have pointed out, this is not a required optimization; it's just what GCC happens to do with the information that anything but y == 1 would be UB.

It would be valid for compilers to completely ignore all assumptions.

But what about constant expressions?

Compilers are required to diagnose all undefined behavior in constant expressions¹⁾, but is this reasonable? For example:

constexpr bool extremely_complicated(int x) {
    bool result;
    // 10,000 lines of math ...
    return result;
}

constexpr int div(int x, int y) {
    // This should result in a compiler error when the compiler is unable to prove
    // what extremely_complicated(x) returns.
    // extremely_complicated(x) is not evaluated, so it needs to be able to
    // prove the result without evaluating the function.
    [[assume(extremely_complicated(x))]];
    return x / y;
}

constexpr int quotient = div(4, 2);

Is it still a problem even if the compiler has no way of proving whether an assumption would evaluate to true? It obviously can't solve the halting problem.

How exactly do assumptions and constant expressions interact? [dcl.attr.assume] doesn't have any wording on this.

---

¹⁾ Note: extremely_complicated(x) is not a constant expression, but it's located in an assumption whose failure would result in UB within a constant evaluation of div(4, 2), which is a constant expression. It is generally said that UB in a constant expression needs to be diagnosed.

Answer 1

There is a specific exception for assume in the final C++23 draft.

[expr.const]/5.8 (with references deciphered)

An expression E is a core constant expression unless the evaluation of E, following the rules of the abstract machine ([intro.execution]), would evaluate one of the following:

• ...
• an operation that would have undefined behavior as specified in [intro] through [cpp], excluding [dcl.attr.assume];

So a compiler doesn't need to judge the veracity of assumptions in order to judge the constantness of expressions. If you write

constexpr int g() {
    [[assume(false)]];
    return 5;
}

then g() may or may not be a core constant expression (it is unspecified whether [[assume(E)]]; disqualifies an expression for being constant if E both is allowed in the constexpr context and doesn't return true). If you further write

int main() {
    constexpr int x = g();
}

there are two cases. If the implementation has decided g() is not a core constant expression (as it is free to do so), it is required to give a diagnostic. If the implementation has decided g() is a core constant expression, the program has undefined behavior.

So you see that compilers have been given an out. A false assumption in a constexpr context can be undefined behavior and not a diagnostic at the implementation's choosing. An implementation could just choose to never check the assumptions in constant expressions. If an assumption then turns out to be false, the program appearing to compile and run successfully (if incorrectly) is just a manifestation of the resulting undefined behavior.

Answer 2

First of all, even if the compiler can't solve the Collatz Conjecture and the Halting Problem, it is undefined behavior if those expressions don't evaluate to true.

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.

- [dcl.attr.assume]

The compiler might not be able to do anything with an assumption, but that doesn't matter to the C++ standard. However, since some assumptions are obviously too complex to diagnose, the standard has this paragraph:

It is unspecified whether [the expression] E is a core constant expression if E satisfies the constraints of a core constant expression, but evaluation of E would evaluate

• [...]
• a statement with an assumption whose converted conditional-expression, if evaluated where the assumption appears, would not disqualify E from being a core constant expression and would not evaluate to true.

[Note: E is not disqualified from being a core constant expression if the hypothetical evaluation of the converted conditional-expression would disqualify E from being a core constant expression. — end note]

- [expr.const] p5.33

What this means is:

• [[assume( (std::exit(0), B) )]] does not disqualify E from being a core constant expression, regardless whether B is true or false
• it is unspecified whether [[assume(extremely_complicated(x))]] disqualifies div from being a core constant expression
  • however, only if a hypothetical evaluation wouldn't exceed implementation-defined limits for constant expressions; if so, it cannot disqualify E

Compilers can implement this very simply, by either

• ignoring assumptions in constant expressions, so that none disqualify E from being a core constant expression, or
• selectively evaluating some assumptions¹⁾, and if they don't evaluate to false, don't disqualify E, otherwise raise an error

---

¹⁾ This cannot change observed behavior, such as by blowing an implementation-defined limit. An evaluation can take place, but it needs to behave as if it was a hypothetical evaluation.

Answer 3

Here's the tl;dr of what happens if the assumption predicate is not true during constant evaluation:

1. If the predicate of the assumption would disqualify the enclosing evaluation from being a constant evaluation, then the compiler ignores the assumption and continues the constant evaluation as if the statement with the assumption were not evaluated;
2. Otherwise, suppose the constant evaluation is occurring in a context that requires a constant evaluation—a so-called "manifestly constant-evaluated" context. Then, the compiler may do one of the following, and it is not specified which:
   1. ignore the assumption;
   2. notice that the assumption predicate evaluates to false and issue a diagnostic because the evaluation is not a constant expression; or
   3. notice that the assumption predicate evaluates to false and not issue a diagnostic. In this case, the behavior is undefined, because of the fact that it involves the evaluation of a statement that has undefined behaviour. (This is a particularly unhelpful implementation choice, so I don't think that real-world implementations will do this.)
3. Otherwise, suppose the constant evaluation is occurring in a context in which a constant expression is not required, such as the initialization of a variable of const integral type. Then, the compiler may do one of the following during constant evaluation, and it is not specified which:
   1. ignore the assumption, which results in the variable being constant-initialized;
   2. notice that the assumption predicate evaluates to false, conclude that constant evaluation has failed, and defer the initialization to runtime, in which case the runtime behavior will be undefined if the assumption is reached at runtime and the predicate again fails to be true; or
   3. notice that the assumption predicate evaluates to false and conclude that the constant evaluation has undefined behavior. This is the same as the previous bullet 3, but in this case, it might be useful for compilers to use the compile-time UB to issue a diagnostic and terminate translation, rather than deferring the initialization to runtime.

---

Let's now see how the wording justifies the above claims.

Here's the wording of [expr.const]/5.33:

It is unspecified whether E is a core constant expression if E satisfies the constraints of a core constant expression, but evaluation of E would evaluate

• [...]
• a statement with an assumption ([dcl.attr.assume]) whose converted conditional-expression, if evaluated where the assumption appears, would not disqualify E from being a core constant expression and would not evaluate to true.
  [Note 5: E is not disqualified from being a core constant expression if the hypothetical evaluation of the converted conditional-expression would disqualify E from being a core constant expression. — end note]

Now, the predicate of an assumption is not allowed to be evaluated. However, as a special case, if the assumption is reached during constant evaluation, then the compiler can choose to evaluate the predicate anyway, because the compiler can always detect whether the evaluation is about to have a side effect. If that side effect would make it not a constant evaluation (e.g. calling an I/O function), the compiler would have to stop evaluating the predicate. If the side effect is the modification of an object that was created during the constant evaluation, on the other hand, the compiler could either stop evaluating it, or it could continue evaluating it but then "undo" all such mutations when it's done evaluating the predicate, so that the as-if rule is satisfied. However, under no circumstances is the compiler ever obligated to evaluate the assumption predicate, since, after all, the standard says that it isn't evaluated. So the freedom to not evaluate the predicate justifies bullets 2.1 and 3.1 above.

The condition "would not disqualify E from being a core constant expression" implies that if the hypothetical evaluation of the assumption predicate would disqualify E from being a core constant expression, e.g., because it calls a non-constexpr function, then [expr.const]/5.33 does not apply. E is still a core constant expression, and the assumption predicate is not evaluated (because it never is). This justifies Note 5 and bullet 1 above.

If the evaluation of the assumption predicate would not disqualify E from being a core constant expression, then, as [expr.const]/5.33 says, it is unspecified whether E is still a core constant expression. That means:

• the compiler can decide that it's not a core constant expression, which justifies subbullets 2.2 and 3.2 above; or
• the compiler can decide that it's still a core constant expression, which means that instead of aborting the constant evaluation, it considers the program to still contain the evaluation of the failed assumption, resulting in UB. This justifies subbullets 2.3 and 3.3 above.