This is an archive of the discontinued LLVM Phabricator instance.

Add "willreturn" function attribute
ClosedPublic

Authored by uenoku on Jun 3 2019, 12:57 AM.

Details

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.

Diff Detail

Repository
rL LLVM

Event Timeline

uenoku created this revision.Jun 3 2019, 12:57 AM
Herald added a project: Restricted Project. · View Herald TranscriptJun 3 2019, 12:57 AM
uenoku edited the summary of this revision. (Show Details)Jun 3 2019, 1:04 AM

How is this different from noreturn attribute?

uenoku added a comment.Jun 3 2019, 1:14 AM

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.

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.

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 ↗(On Diff #202658)

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
25 ↗(On Diff #202658)

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

55 ↗(On Diff #202658)

Same as above. FIXME missing.

102 ↗(On Diff #202658)

Can we also have a conditional exit call test.

189 ↗(On Diff #202658)

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

jdoerfert added inline comments.Jun 3 2019, 9:21 AM
llvm/docs/LangRef.rst
1479 ↗(On Diff #202658)

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 updated this revision to Diff 202872.EditedJun 4 2019, 1:32 AM
uenoku retitled this revision from Add "will-return" function attribute to Add "willreturn" function attribute.
uenoku edited the summary of this revision. (Show Details)

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 marked 5 inline comments as done.Jun 4 2019, 1:36 AM
uenoku added inline comments.
llvm/docs/LangRef.rst
1479 ↗(On Diff #202658)

I prefer willreturn. I renamed it.

uenoku marked an inline comment as done.Jun 4 2019, 1:43 AM
uenoku added inline comments.
llvm/test/Transforms/FunctionAttrs/will-return.ll
25 ↗(On Diff #202658)

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

uenoku updated this revision to Diff 202883.Jun 4 2019, 2:36 AM

Fix patch.

jdoerfert added inline comments.Jun 4 2019, 11:28 AM
llvm/docs/LangRef.rst
1479 ↗(On Diff #202883)

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 ↗(On Diff #202883)

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
25 ↗(On Diff #202658)

You are building it ;)

311 ↗(On Diff #202883)

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

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 ↗(On Diff #202883)

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 updated this revision to Diff 203080.Jun 4 2019, 10:57 PM

Add test

uenoku marked 5 inline comments as done and an inline comment as not done.Jun 4 2019, 11:14 PM

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
25 ↗(On Diff #202658)

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 ↗(On Diff #202883)

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

uenoku marked an inline comment as not done.Jun 4 2019, 11:22 PM

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
25 ↗(On Diff #202658)

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 ↗(On Diff #202883)

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 updated this revision to Diff 203186.Jun 5 2019, 9:55 AM

Add unreachable exit (test 15)

uenoku marked 5 inline comments as done.Jun 5 2019, 9:55 AM
jdoerfert added inline comments.Jun 5 2019, 6:57 PM
llvm/docs/LangRef.rst
1482 ↗(On Diff #203186)

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
45 ↗(On Diff #203186)

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

75 ↗(On Diff #203186)

Why negative?

204 ↗(On Diff #203186)

-NOT line missing.

253 ↗(On Diff #203186)

I think we did.

286 ↗(On Diff #203186)

FIXME missing

uenoku updated this revision to Diff 203280.Jun 5 2019, 7:52 PM
uenoku marked 7 inline comments as done.

Address comments.

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 updated this revision to Diff 203281.Jun 5 2019, 9:22 PM

Fix 2.2 LLVM IR.

This revision is now accepted and ready to land.Jun 6 2019, 3:40 PM

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"?

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 marked an inline comment as done.EditedJun 7 2019, 11:07 AM

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 updated this revision to Diff 205506.Jun 18 2019, 10:41 PM

Change test file name.

uenoku updated this revision to Diff 206474.Jun 25 2019, 9:51 AM

Make willreturn enum attribute.

uenoku updated this revision to Diff 206589.Jun 25 2019, 11:46 PM

Fix test.

jdoerfert requested changes to this revision.Jun 26 2019, 2:57 PM

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)

This revision now requires changes to proceed.Jun 26 2019, 2:57 PM
uenoku updated this revision to Diff 206779.Jun 26 2019, 10:29 PM

Address comment.

This revision was not accepted when it landed; it landed in state Needs Review.Jun 27 2019, 8:52 AM
This revision was automatically updated to reflect the committed changes.
mehdi_amini added inline comments.Jun 27 2019, 9:10 AM
llvm/docs/LangRef.rst
1479 ↗(On Diff #202658)

"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").

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?