[PATCH] D62801: Add "willreturn" function attribute

[Hideto Ueno via Phabricator via llvm-commits]

uenoku marked 5 inline comments as done and an inline comment as not done.
uenoku added a comment.

> two that do not have any but only unreachable exits (one positive, one negative).

I couldn't understand this. What is a negative one?



================
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)
----------------
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?


================
Comment at: llvm/test/Transforms/FunctionAttrs/will-return.ll:52
+; }
+; fact_maybe_not(-1) doesn't stop.
+
----------------
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.


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

https://reviews.llvm.org/D62801