How does [[assume]] affect an assert?

The user defined attribute [[assumes(expression)]]

Specifies that the given expression is assumed to always evaluate to true at a given point in order to allow compiler optimizations based on the information given.

where if the expression is false, it invokes runtime undefined behavior.

However, the same page says:

One correct way to use them is to follow assertions with assumptions:

assert(x > 0);     // trigger an assertion when NDEBUG is not defined and x > 0 is false
[[assume(x > 0)]]; // provide optimization opportunities when NDEBUG is defined

I'm confused by this statement. If NDEBUG is not defined, and x > 0 is false, the condition in the assume would be false, which triggers undefined behavior.

As far as I understand this, it means the compiler can assume that the expression is true, and remove the assert entirely. That would mean the "correct" usage isn't actually correct, so I suspect I'm misunderstanding something here. Is the UB invoked by [[assume]] not permitted to "time-travel" like UB usually is?

How does [[assume]] work exactly?

Solution

How does [[assume]] work exactly?

It is roughly equivalent to

if (!(x > 0)) {
    std::unreachable(); // trigger UB
}

Is the UB invoked by [[assume]] not permitted to "time-travel" like UB usually is?

It is allowed, but assert prevents the UB from being reached:

assert(x > 0);     // trigger an assertion when NDEBUG is not defined and x > 0 is false
[[assume(x > 0)]]; // provide optimization opportunities when NDEBUG is defined

is roughly equivalent to:

#ifndef NDEBUG
if (!(x > 0)) {
   warn_user_assert_break("x > 0");
   std::abort(); // No return function
}
#endif
[[assume(x > 0)]];

#ifndef NDEBUG
if (!(x > 0)) {
   warn_user_assert_break("x > 0");
   std::abort(); // No return function
}
#endif
if (!(x > 0)) {
    std::unreachable(); // trigger UB
}

So, when NDEBUG is not defined, and the precondition fails, then std::abort is executed, and you don't reach the assume (which would break the precondition too and trigger UB). Compiler might even make the assumption by itself with the above if.

When NDEBUG is defined, there is only [[assume(x > 0)]], and if the precondition fails, you have UB, and time-travel can indeed happen.