Add "willreturn" function attribute

[uenoku]

Summary

This patch proposes a new function attribute, willreturn, to indicate that a call of this function will either exhibit undefined behavior or comes back to the invoking call site.

This attribute guarantees that the function doesn't have any loop, recursion or terminating function like abort, exit.

We need an argue about handling an exception and invoke.

[lebedev.ri]

How is this different from noreturn attribute?

[uenoku]

How is this different from noreturn attribute?

noreturn indicates that the function never returns for any input or in any environment.
On the other hand, will-return indicates that the function always returns for any input or in any environment.

[jdoerfert]

In D62801#1527020, @lebedev.ri wrote:

How is this different from noreturn attribute?

This will eventually replace the CallChecks in llvm::isGuaranteedToTransferExecutionToSuccessor and it should be much more powerful as it directly tries to prove the property instead of deriving it from memory behavior.

[jdoerfert]

Can we have a test with some conditionals and multiple exits?

We also need more loop tests:

• Constant trip count
• Trip count known to be bounded (as you have one)
• Trip count potentially unbounded (for (unsigned i = s; i != e; i++) {})
• See als LoopDeletion.cpp as it basically has to prove similar things we are interested in

llvm/docs/LangRef.rst

1479

You should allow exceptions here, I think. That would make will-return and orthogonal to nounwind (aka. no-throw).

We can also think about removing the hypen, idk what is best.

llvm/test/Transforms/FunctionAttrs/will-return.ll

26

Add a FIXME: this function will eventually return, we could be able to detect that.

56

Same as above. FIXME missing.

103

Can we also have a conditional exit call test.

190

I think this should be will-return but I can be convinced will-return should be stronger.

[jdoerfert]

llvm/docs/LangRef.rst

1479

One idea to phrase it would be:

"the function will, after a finite amount of time, stop executing without ending execution of the program."

Or:

"either exhibit undefined behavior or comes back and continues execution at a point in the existing call stack that includes the current invocation."

[uenoku]

Add some test and change will-return to willreturn.

• constant trip count (test 11)
• unbound trip count (test 12)
• conditional and multiple exit (test 5)
• buggy recursive function (test 2.2)

[uenoku]

llvm/docs/LangRef.rst

1479

I prefer willreturn. I renamed it.

[uenoku]

llvm/test/Transforms/FunctionAttrs/will-return.ll

26

I don't know the way for detecting this. Is there any tool to prove termination for LLVM IR function?

[uenoku]

Fix patch.

[jdoerfert]

llvm/docs/LangRef.rst

1479

This attribute doesn't mean that the function never throw an exception.

Annotated functions may still raise an exception, i.a., `nounwind` is not implied.

1481

If an invocation of an annotated function does not return the control back to a point in the call stack, the behavior is undefined.

llvm/test/Transforms/FunctionAttrs/will-return.ll

26

You are building it ;)

311

I made a mistake here, it should be i+=2 or i+=stride (a new parameter)

[jdoerfert]

Maybe also a test which in IR has multiple returns, and two that do not have any but only unreachable exits (one positive, one negative).
You probably have to build them by hand and not from C.

llvm/test/Transforms/FunctionAttrs/will-return.ll

52

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;

[uenoku]

Add test

[uenoku]

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

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

llvm/test/Transforms/FunctionAttrs/will-return.ll

26

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?

52

Oh, I thought this loop should be considered as an endless loop.

[jdoerfert]

In 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.

llvm/test/Transforms/FunctionAttrs/will-return.ll

26

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.

52

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.

[uenoku]

Add unreachable exit (test 15)

[jdoerfert]

llvm/docs/LangRef.rst

1482

Style comments:

No comma after will in the first line.
Remove the "This attribute doesn't mean" sentence.
Remove "the" in front of "control back".

llvm/test/Transforms/FunctionAttrs/will-return.ll

46

This function does always return. Change the text and expected input or change the code.

76

Why negative?

205

-NOT line missing.

254

I think we did.

287

FIXME missing

[uenoku]

Address comments.

[jdoerfert]

All good except 2.2 (negative case). Did you change only the comment (C code) or also the IR?

You can work on the deduction now as well.

[uenoku]

Fix 2.2 LLVM IR.

[jdoerfert]

LGTM

[lebedev.ri]

This contains the langref changes, and the test+test changes.
But the actual code isn't here, and any other differentials aren't linked in "Stack"?

[jdoerfert]

In D62801#1533348, @lebedev.ri wrote:

This contains the langref changes, and the test+test changes.
But the actual code isn't here, and any other differentials aren't linked in "Stack"?

No code yet (I think). I asked @uenoku to write up the LangRef and tests first so we know what we actually want to derive.

[uenoku]

In D62801#1534105, @jdoerfert wrote:

In D62801#1533348, @lebedev.ri wrote:

This contains the langref changes, and the test+test changes.
But the actual code isn't here, and any other differentials aren't linked in "Stack"?

No code yet (I think). I asked @uenoku to write up the LangRef and tests first so we know what we actually want to derive.

@jdoerfert
Should I write the actual code now?

[uenoku]

Change test file name.

[uenoku]

Make willreturn enum attribute.

[uenoku]

Fix test.

[jdoerfert]

I was going to commit this but I realized the commit message needs a bit of polishing and we need to add it to test/Bitcodes/attributes.ll (see https://reviews.llvm.org/D62766#change-4ANgOAC3AzdR)

[uenoku]

Address comment.

[mehdi_amini]

llvm/docs/LangRef.rst

1479

"comes back and continues execution at a point in the existing call stack that includes the current invocation."

This sentence is not clear to me: what does "comes back" mean does not seem well defined. Also I don't understand: "at a point in the existing call stack that includes the current invocation", I assume you're trying to allow exceptions, but then the point at which the control would resume would *not* include the current invocation since it could be higher in the call stack.

(And I think that it should be "come back" instead of "comes back").

[jdoerfert]

This sentence is not clear to me: what does "comes back" mean does not seem well defined. Also I don't understand: "at a point in the existing call stack that includes the current invocation", I assume you're trying to allow exceptions, but then the point at which the control would resume would *not* include the current invocation since it could be higher in the call stack.

First, yes exceptions should be allowed. Second, an exception could be caught at the current invocation or any other one in the call stack and that is what the text already says.
The valid points to continue execution are all calls in the call stack including the one that is performed at this moment. Do you think this wording is somehow excluding any of these points or what is the problem you see?

(And I think that it should be "come back" instead of "comes back").

Could be, I couldn't say for sure. Maybe we can find a better term altogether?

llvm/docs/LangRef.rst

 ``noreturn``
     This function attribute indicates that the function never returns
     normally. This produces undefined behavior at runtime if the
     function ever does dynamically return.
 ``norecurse``
     This function attribute indicates that the function does not call itself
     either directly or indirectly down any possible call path. This produces
     undefined behavior at runtime if the function ever does recurse.
+``willreturn``
+    This function attribute indicates that a call of this function will,
+    either exhibit undefined behavior or comes back and continues execution 
+    at a point in the existing call stack that includes the current invocation.
+    This attribute doesn't mean that the function never throw an exception.
+    This produces undefined behavior at runtime if the function never comes back
+    to the call site.
 ``nounwind``
     This function attribute indicates that the function never raises an
     exception. If the function does raise an exception, its runtime
     behavior is undefined. However, functions marked nounwind may still
     trap or generate asynchronous exceptions. Exception handling schemes
     that are recognized by LLVM to handle asynchronous exceptions, such
     as SEH, will still provide their implementation defined semantics.
 ``"null-pointer-is-valid"``
    If ``"null-pointer-is-valid"`` is set to ``"true"``, then ``null`` address

llvm/test/Transforms/FunctionAttrs/will-return.ll

+; RUN: opt -functionattrs -S < %s | FileCheck %s --check-prefix=FNATTR
+
+target datalayout = "e-m:e-i64:64-f80:128-n8:16:32:64-S128"
+
+; Test cases specifically designed for the "willreturn" function attribute.
+; We use FIXME's to indicate problems and missing attributes.
+
+
+; TEST 1 (positive case)
+; FIXME: missing "willreturn"
+; FNATTR: Function Attrs: noinline norecurse nounwind readnone uwtable
+; FNATTR-NEXT: define void @only_return()
+define void @only_return() #0 {
+    ret void
+}
+
+
+; TEST 2 (positive & negative case)
+; 2.1 (positive case)
+; recursive function which will halt
+; int fib(int n){
+;    return n<=1? n : fib(n-1) + fib(n-2);
+; }
+
+; FIXME: missing "willreturn"
+; FNATTR: Function Attrs: noinline nounwind readnone uwtable
+; FNATTR-NEXT: define i32 @fib(i32)
+define i32 @fib(i32) local_unnamed_addr #0 {
+  %2 = icmp slt i32 %0, 2
+  br i1 %2, label %9, label %3
+
+; <label>:3:                                      ; preds = %1
+  %4 = add nsw i32 %0, -1
+  %5 = tail call i32 @fib(i32 %4)
+  %6 = add nsw i32 %0, -2
+  %7 = tail call i32 @fib(i32 %6)
+  %8 = add nsw i32 %7, %5
+  ret i32 %8
+
+; <label>:9:                                      ; preds = %1
+  ret i32 %0
+}
+
+; 2.2 (negative case)
+; recursive function which doesn't stop for some input.
+; int fact_maybe_not_halt(int n) {
+;   if (n==0) {
+;     return 1;
+;   }
+;   return fact_maybe_not_halt(n-1) * n;
+; }
+; fact_maybe_not(-1) doesn't stop.
+
+; FNATTR: Function Attrs: noinline norecurse nounwind readnone uwtable
+; FNATTR-NOT: "willreturn"
+; FNATTR-NEXT: define i32 @fact_maybe_not_halt(i32) local_unnamed_addr
+define i32 @fact_maybe_not_halt(i32) local_unnamed_addr #0 {
+  %2 = icmp eq i32 %0, 0
+  br i1 %2, label %9, label %3
+
+; <label>:3:                                      ; preds = %1, %3
+  %4 = phi i32 [ %6, %3 ], [ %0, %1 ]
+  %5 = phi i32 [ %7, %3 ], [ 1, %1 ]
+  %6 = add nsw i32 %4, -1
+  %7 = mul nsw i32 %4, %5
+  %8 = icmp eq i32 %6, 0
+  br i1 %8, label %9, label %3
+
+; <label>:9:                                      ; preds = %3, %1
+  %10 = phi i32 [ 1, %1 ], [ %7, %3 ]
+  ret i32 %10
+}
+
+
+; TEST 3 (negative case)
+; loop
+; int fact_loop(int n ){
+;   int ans = 1;
+;   for(int i = 1;i<=n;i++){
+;     ans *= i;
+;   }
+;   return ans;
+; }
+
+; FIXME: missing "willreturn"
+; FNATTR: Function Attrs: noinline norecurse nounwind readnone uwtable
+; FNATTR-NEXT: define i32 @fact_loop(i32)
+define i32 @fact_loop(i32) local_unnamed_addr #0 {
+  %2 = icmp slt i32 %0, 1
+  br i1 %2, label %3, label %5
+
+; <label>:3:                                      ; preds = %5, %1
+  %4 = phi i32 [ 1, %1 ], [ %8, %5 ]
+  ret i32 %4
+
+; <label>:5:                                      ; preds = %1, %5
+  %6 = phi i32 [ %9, %5 ], [ 1, %1 ]
+  %7 = phi i32 [ %8, %5 ], [ 1, %1 ]
+  %8 = mul nsw i32 %6, %7
+  %9 = add nuw nsw i32 %6, 1
+  %10 = icmp eq i32 %6, %0
+  br i1 %10, label %3, label %5
+}
+
+; TEST 4 (negative case)
+; mutual recursion
+; void mutual_recursion1(){
+;    mutual_recursion2();
+; }
+; void mutual_recursion2(){
+;     mutual_recursion1();
+; }
+
+; FNATTR: Function Attrs: noinline nounwind readnone uwtable
+; FNATTR-NOT: "willreturn"
+; FNATTR-NEXT: define void @mutual_recursion1()
+define void @mutual_recursion1() #0 {
+  call void @mutual_recursion2()
+  ret void
+}
+
+
+; FNATTR: Function Attrs: noinline nounwind readnone uwtable
+; FNATTR-NOT: "willreturn"
+; FNATTR-NEXT: define void @mutual_recursion2()
+define void @mutual_recursion2() #0 {
+  call void @mutual_recursion1()
+  ret void
+}
+
+
+; TEST 5 (negative case)
+; call exit/abort (has noreturn attribute)
+; FNATTR: Function Attrs: noreturn
+; FNATTR-NEXT: declare void @exit(i32) local_unnamed_addr
+declare void @exit(i32) local_unnamed_addr noreturn
+
+; FNATTR: Function Attrs: noinline nounwind uwtable
+; FNATTR-NOT: "willreturn"
+; FNATTR-NEXT: define void @only_exit()
+define void @only_exit() local_unnamed_addr #0 {
+  tail call void @exit(i32 0)
+  unreachable
+}
+
+; conditional exit
+; void conditional_exit(int cond, int *p){
+;     if(cond){
+;       exit(0);
+;     }
+;     if(*p){
+;       exit(1);
+;     }
+;     return;
+; }
+; FNATTR: Function Attrs: noinline nounwind uwtable
+; FNATTR-NOT: "willreturn"
+; FNATTR-NEXT: define void @conditional_exit(i32, i32* nocapture readonly) local_unnamed_addr 
+define void @conditional_exit(i32, i32* nocapture readonly) local_unnamed_addr #0 {
+  %3 = icmp eq i32 %0, 0
+  br i1 %3, label %5, label %4
+
+; <label>:4:                                      ; preds = %2
+  tail call void @exit(i32 0) 
+  unreachable
+
+; <label>:5:                                      ; preds = %2
+  %6 = load i32, i32* %1, align 4
+  %7 = icmp eq i32 %6, 0
+  br i1 %7, label %9, label %8
+
+; <label>:8:                                      ; preds = %5
+  tail call void @exit(i32 1) 
+  unreachable
+
+; <label>:9:                                      ; preds = %5
+  ret void
+}
+
+; TEST 6 (positive case)
+; Call intrinsic function
+; FNATTRS: Function Attrs: noinline readnone speculatable
+; FNATTRS-NEXT: declare float @llvm.floor.f32(float)
+declare float @llvm.floor.f32(float)
+
+; FIXME: missing "willreturn"
+; FNATTRS: Function Attrs: noinline nounwind uwtable
+; FNATTRS-NEXT: define void @call_floor(float %a)
+define void @call_floor(float %a) #0 {
+    tail call float @llvm.floor.f32(float %a)
+    ret void
+}
+
+
+; TEST 7 (negative case)
+; Call function declaration without "willreturn"
+
+; FNATTR: Function Attrs: noinline nounwind uwtable
+; FNATTR-NOT: "willreturn"
+; FNATTR-NEXT: declare void @maybe_noreturn()
+declare void @maybe_noreturn() #0
+
+; FNATTR: Function Attrs: noinline nounwind uwtable
+; FNATTR-NEXT: define void @call_maybe_noreturn()
+define void @call_maybe_noreturn() #0 {
+    tail call void @maybe_noreturn()
+    ret void
+}
+
+
+; TEST 8 (positive case)
+; Check propagation.
+
+; FNATTR: Function Attrs: "willreturn"
+; FNATTR-NEXT: declare void @will_return()
+declare void @will_return() "willreturn"
+
+; FIXME: missing "willreturn"
+; FNATTR: Function Attrs: noinline nounwind uwtable
+; FNATTR-NEXT: define void @f1()
+define void @f1() #0 {
+    tail call void @will_return()
+    ret void
+}
+
+; FIXME: missing "willreturn"
+; FNATTR: Function Attrs: noinline nounwind uwtable
+; FNATTR-NEXT: define void @f2()
+define void @f2() #0 {
+    tail call void @f1()
+    ret void
+}
+
+
+; TEST 9 (negative case)
+; call willreturn function in endless loop.
+
+; FNATTR: Function Attrs: noinline nounwind uwtable
+; FNATTR-NOT: "willreturn"
+; FNATTR-NEXT: define void @call_will_return_but_has_loop()
+define void @call_will_return_but_has_loop() #0 {
+  br label %label1
+label1:
+  tail call void @will_return()
+  br label %label2
+label2:
+  br label %label1
+}
+
+
+; TEST 10 (positive case?)
+; invoke a function with "willreturn"
+; FIXME: We need a more argue about exception and invoke instruction.
+
+; FNATTR: Function Attrs: noinline uwtable "willreturn"
+; FNATTR-NEXT: declare i1 @maybe_raise_exception()
+declare i1 @maybe_raise_exception() #1 "willreturn"
+
+; FIXME: missing "willreturn"
+; FNATTR: Function Attrs: nounwind
+; FNATTR-NEXT: define void @invoke_test()
+define void @invoke_test() personality i32 (...)* @__gxx_personality_v0 {
+  invoke i1 @maybe_raise_exception()
+      to label %N unwind label %F
+  N:
+    ret void
+  F:
+    %val = landingpad { i8*, i32 }
+                  catch i8* null
+    ret void
+}
+
+declare i32 @__gxx_personality_v0(...)
+
+
+; TEST 11 (positive case)
+; counstant trip count
+; int loop_constant_trip_count(int*p){
+;    int ans = 0;
+;    for(int i = 0;i<10;i++){
+;        ans += p[i];
+;    }
+;    return ans;
+; }
+
+; FNATTR: Function Attrs: noinline norecurse nounwind readonly uwtable
+; FNATTR-NEXT: define i32 @loop_constant_trip_count(i32* nocapture readonly)
+define i32 @loop_constant_trip_count(i32* nocapture readonly) #0 {
+  br label %3
+
+; <label>:2:                                      ; preds = %3
+  ret i32 %8
+
+; <label>:3:                                      ; preds = %3, %1
+  %4 = phi i64 [ 0, %1 ], [ %9, %3 ]
+  %5 = phi i32 [ 0, %1 ], [ %8, %3 ]
+  %6 = getelementptr inbounds i32, i32* %0, i64 %4
+  %7 = load i32, i32* %6, align 4
+  %8 = add nsw i32 %7, %5
+  %9 = add nuw nsw i64 %4, 1
+  %10 = icmp eq i64 %9, 10
+  br i1 %10, label %2, label %3
+}
+
+
+; TEST 12 (negative case)
+; unbounded trip count
+
+; int loop_trip_count_unbound(unsigned s,unsigned e, int *p){
+;     int ans = 0;
+;     for(unsigned i = s;i != e;i++){
+;         ans += p[i];
+;     }
+;     return ans;
+; }
+; FNATTR: Function Attrs: noinline norecurse nounwind readonly uwtable
+; FNATTR-NOT: "willreturn"
+; FNATTR-NEXT: define i32 @loop_trip_count_unbound(i32, i32, i32* nocapture readonly) local_unnamed_addr
+define i32 @loop_trip_count_unbound(i32, i32, i32* nocapture readonly) local_unnamed_addr #0 {
+  %4 = icmp eq i32 %0, %1
+  br i1 %4, label %5, label %7
+
+; <label>:5:                                      ; preds = %7, %3
+  %6 = phi i32 [ 0, %3 ], [ %13, %7 ]
+  ret i32 %6
+
+; <label>:7:                                      ; preds = %3, %7
+  %8 = phi i32 [ %14, %7 ], [ %0, %3 ]
+  %9 = phi i32 [ %13, %7 ], [ 0, %3 ]
+  %10 = zext i32 %8 to i64
+  %11 = getelementptr inbounds i32, i32* %2, i64 %10
+  %12 = load i32, i32* %11, align 4
+  %13 = add nsw i32 %12, %9
+  %14 = add i32 %8, 1
+  %15 = icmp eq i32 %14, %1
+  br i1 %15, label %5, label %7
+}
+
+
+; TEST 13 (positive case)
+; Function Attrs: norecurse nounwind readonly uwtable
+;  int loop_trip_dec(int n, int *p){
+;    int ans = 0;
+;    for(;n >= 0;n--){
+;        ans += p[n];
+;    }
+;    return ans;
+;  }
+
+
+; FIXME: missing "willreturn"
+; FNATTR: Function Attrs: noinline norecurse nounwind readonly uwtable
+; FNATTR-NEXT: define i32 @loop_trip_dec(i32, i32* nocapture readonly)
+
+define i32 @loop_trip_dec(i32, i32* nocapture readonly) local_unnamed_addr #0 {
+  %3 = icmp sgt i32 %0, -1
+  br i1 %3, label %4, label %14
+
+; <label>:4:                                      ; preds = %2
+  %5 = sext i32 %0 to i64
+  br label %6
+
+; <label>:6:                                      ; preds = %4, %6
+  %7 = phi i64 [ %5, %4 ], [ %12, %6 ]
+  %8 = phi i32 [ 0, %4 ], [ %11, %6 ]
+  %9 = getelementptr inbounds i32, i32* %1, i64 %7
+  %10 = load i32, i32* %9, align 4
+  %11 = add nsw i32 %10, %8
+  %12 = add nsw i64 %7, -1
+  %13 = icmp sgt i64 %7, 0
+  br i1 %13, label %6, label %14
+
+; <label>:14:                                     ; preds = %6, %2
+  %15 = phi i32 [ 0, %2 ], [ %11, %6 ]
+  ret i32 %15
+}
+
+attributes #0 = { nounwind uwtable noinline }
+attributes #1 = { uwtable noinline }