[PATCH] D85393: [WIP] [IR] Adding noprogress as a LLVM IR attribute

[Ralf via Phabricator via llvm-commits]

RalfJung added a comment.

> I don't look at it as added or removed, for me it is a boolean flag, with a default that requires progress. It is more like nobuiltin, noduplicate, nomerge, returns_twice, .... The difference is that I don't see this being deduced. It is just a description of the input semantics, not a property we derive from the code (to describe the code). Unclear if the view makes a difference, let me know what u think :)

I don't think of any of these attributes as being deduced. ;) I don't care where the attributes come from, the important bit is how they affect the language semantics, the language here being LLVM IR of course. (It's almost as if I'm a programming language researcher. ;)

`nounwind` and friends affect the language semantics by saying things like: if this function unwinds, that's UB. (In the follows that if you can deduce that a function doesn't unwind, it is okay to add the attribute. But as with all optimizations and analysis, they are not the ground truth, they have to be justified against the language semantics.)
The *absence* of `noprogress` affects the language semantics by saying: if this function runs into a side-effect-free infinite loop, that's UB. (And something about infinite recursion, but that's a bit more tricky because multiple functions can be involved.) Adding `noprogress` disables that UB. (This makes me prefer "allownoprogress" as attribute name, if you want to keep its polarity.)

That's how this attribute is "the other way around" compared to the normal ones. Unfortunately I don't know what nobuiltin, nomerge etc mean, so I cannot say how they affect language semantics. I don't know what you mean by "input semantics".

`noprogress` could certainly be deduced like the others, it's just backwards again -- we have to deduce its absence. For a function that has `noprogress`, if the compiler can prove that there is no infinite loop, it may remove the attribute. (I am not sure if that's a useful thing to do, I am just saying it is possible.)


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D85393