13

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?

Jan Schultke
  • 17,446
  • 6
  • 47
  • 96

2 Answers2

12

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.

user17732522
  • 53,019
  • 2
  • 56
  • 105
  • What if an expression is one which cannot be proven to evaluate to true without evaluating it, e.g. because it's based upon the effect of accessing a volatile-qualified object? – supercat Sep 02 '23 at 05:43
  • Whether the assumed expression containing UB evaluates to `true` should not be specified, because the Standard doesn't place any requirement on undefined behavior. It may even yield a firmly documented result, which could be `true`, and this would still be conformant. – Ruslan Sep 02 '23 at 08:57
  • @supercat [\[dcl.type.cv\]/5](https://eel.is/c++draft/dcl.dcl#dcl.type.cv-5.sentence-1): "_The semantics of an access through a volatile glvalue are implementation-defined._" I suppose the implementation ought to make a choice and document it. – user17732522 Sep 02 '23 at 09:40
  • @Ruslan That's the second alternative interpretation I mentioned. Is there anything you see wrong in my answer or did you just want to affirm the second interpretation? – user17732522 Sep 02 '23 at 09:44
  • @user17732522: Implementations would generally only be expected to document how they process actions that are actually executed. Well-written specifications shouldn't base the correctness of a program on what "would" happen in a particular situation. The so-called "Formal specification of restrict" in C99 is based on hypotheticals which can end up being meaningless; I haven't yet worked out whether the "assume" would have such contradictions, but it's apt to be a poor fit for most tasks anyway. – supercat Sep 02 '23 at 17:40
6

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.

Nicol Bolas
  • 449,505
  • 63
  • 781
  • 982
  • 2
    Yeah, I was about to post a similar answer. It doesn't say explicitly what happens when an expression has undefined behavior, but an expression with undefined behavior has no specific value to which it evaluates, so it's not, by the standard, evaluating to true, and the compiler can do whatever it likes in response to the resulting undefined behavior. – ShadowRanger Sep 01 '23 at 15:19
  • _"The most reasonable answer is no, because its behavior is undefined"_ — this is not how UB works. It permits any behavior, including producing an unexpected—or expected and maybe even documented—result, so in this case it may just as easily produce `true`. E.g. suppose an implementation defines division by zero to always yield `1`. This would be totally OK from the point of view of the Standard. And then the assumption would evaluate to `true`, which is completely expected in this case. – Ruslan Sep 02 '23 at 08:41
  • @Ruslan: Remember: the question is "if it did happen, would the answer be true?" If behavior is undefined, then the most accurate answer would be "I don't know", since... you don't. You don't **know** if it produces true, so what "may" happen is irrelevant. As such, "I don't know" is not "yes", and is therefore functionally equivalent to "no" within this context. – Nicol Bolas Sep 02 '23 at 14:31
  • Well, OK, effectively you're right: if there's a possibility that this returns `false` (or doesn't return anything), then behavior is undefined—as per the Standard—even if this particular implementation guarantees otherwise. – Ruslan Sep 02 '23 at 15:08