[PATCH] D136055: [ValueTracking] Make !range metadata imply noundef for load & call results

Mon Oct 17 03:36:57 PDT 2022

nlopes added a comment.

In D136055#3861580 <https://reviews.llvm.org/D136055#3861580>, @nikic wrote:

> This is correct as specified, but I think there were plans to change `!range` and `!nonnull` to return poison, and require an additional `!noundef` to make them immediate UB, which is the way it works for attributes. I'm not sure what the state of that is though.

FWIW, Alive2 currently models !range as being UB iff !poison && range_is_violated.
This patch proposes to use poison || range_is_violated.
The Alive2 version is bogus in terms of composition of refinement (IPO) as it prevents changing poison to a value that violates the range. But in the past we realized that the proposed (strong UB) semantics didn't work (verification failed for a few optimizations; I don't remember the details).

There's an advantage of keeping poison disentangled, which is that it enables hoisting by dropping just !noundef. I think it's always best to yield poison whenever we can to make movement easier (of loads, calls is less important).

So I agree the best thing to do is to change the semantics, so that a range violation yields poison.

FWIW, there's already a patch for clang to add !noundef to loads by my GSoC student: https://reviews.llvm.org/D134410

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D136055/new/

https://reviews.llvm.org/D136055