[PATCH] D62801: Add "willreturn" function attribute

[Johannes Doerfert via Phabricator via llvm-commits]

jdoerfert added a comment.

In D62801#1530475 <https://reviews.llvm.org/D62801#1530475>, @uenoku wrote:

> > two that do not have any but only unreachable exits (one positive, one negative).
>
> I couldn't understand this. What is a negative one?




1. Two unreachable exits, both preceded by an endless loop or call to a no-return function. This should not be `willreturn`.
2. Two unreachable exits, only terminating loops and `willreturn` calls. I guess this should be `willreturn`, though a very odd case.



================
Comment at: llvm/test/Transforms/FunctionAttrs/will-return.ll:25
+; FNATTR: Function Attrs: noinline nounwind readnone uwtable
+; FNATTR-NOT: "will-return"
+; FNATTR-NEXT: define i32 @fib(i32)
----------------
uenoku wrote:
> jdoerfert wrote:
> > uenoku wrote:
> > > jdoerfert wrote:
> > > > Add a FIXME: this function will eventually return, we could be able to detect that.
> > > I don't know the way for detecting this. Is there any tool to prove termination for LLVM IR function?
> > You are building it ;)
> I think if we want to prove termination for this kind of recursive function, we have to use a formal verification method, isn't' it?
We do not have to prove it now, meaning you don't have to. Having the test is good even if we don't work on the FIXME right now.

In case you want to look into it, I would start with common patterns, that is the recursions that have a single variable with a monotone evolution and which is used in a condition that breaks the recursion.


================
Comment at: llvm/test/Transforms/FunctionAttrs/will-return.ll:52
+; }
+; fact_maybe_not(-1) doesn't stop.
+
----------------
uenoku wrote:
> jdoerfert wrote:
> > It actually will terminate, eventually:
> > 
> > `n = -1, -2, ... INT_MIN, INT_MAX, INT_MAX - 1, INT_MAX - 2, ... 0`
> > 
> > you maybe want `return fact_maybe_not_halt( n > 0 ? n-1 : n) * n;`
> Oh, I thought this loop should be considered as an endless loop.
If it is a negative test, yes. But the problem is that it actually is not an endless loop. While it is "mathematically", e.g., if computations and numbers would be arbitrarily precise, it is not if we restrict numbers to the 2^32 modulo ring. If you decrement a variable often enough it will wrap around, become positive and eventually reach 0. However, if you want to make it potentially endless, decrement it by two instead of one. This way, an odd value will never reach 0.


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

https://reviews.llvm.org/D62801