[llvm-commits] patch: add 'halting' function attribute

[Nick Lewycky]

On Tue, Jul 6, 2010 at 1:48 AM, Duncan Sands <baldrick at free.fr> wrote:

> Hi Nick,
>
> > The attached patch adds a function attribute, "halting", which models
> > the assertion that a function does not have the side-effect of looping
> > indefinitely. This is for llvm.org/PR965
>
> yay!
>
> > +  <dt><tt><b>halting</b></tt></dt>
> > +  <dd>This attribute specifies that the function may be assumed to halt.
>  This
> > +      does not necessarily imply that it will return (it may terminate
> the
> > +      program instead),
> -> This does not necessarily imply that it will return, since terminating
> the
> program and unwinding an exception are also considered halting.
>
> Also, I think here you should end this sentence, and the following should
> be a
> new sentence:
>
> but the attribute may be applied for any language where
> > +      infinite loops are not considered a visible side-effect.
>
> -> A function that loops forever is not halting.  However languages where
> infinite loops are not considered a visible side-effect can indicate this
> by applying the halting attribute to such functions anyway.
>
> A loop is known
> > +      to be halting only if an upper limit on iterations is known before
> the
> > +      loop begins.</dd>
>
> This sounds like an implementation detail - should it be here?
>

Is it? Consider an I/O function that reads from the network until it
receives "00000", the 'end of communication' sigil. Is that function
halting?

The current definition makes the answer a clear no, because you can't set an
upper bound on the iteration count before entering the loop.

Now what if we did consider such a function halting? Do we risk having the
program being miscompiled? For some reason I thought there was a case that
came up like this where the answer was yes, but I can't think of it right
now.

Nick


> > -        } else if (Name == "uname" ||
> > -                   Name == "unlink" ||
> > +        } else if (Name == "uname") {
> > +          if (FTy->getNumParams() != 1 ||
> > +              !FTy->getParamType(0)->isPointerTy())
> > +            continue;
> > +       setIsHalting(F);
>
> strange indentation.
>
> > +  // Definitions with weak linkage may be overridden at linktime with
> > +  // something that writes memory, so treat them like declarations.
>
> -> something that infinite loops, so treat them like declarations.
>
> Otherwise looks good to me.
>
> Ciao,
>
> Duncan.
> _______________________________________________
> llvm-commits mailing list
> llvm-commits at cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/llvm-commits
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-commits/attachments/20100706/86bf1809/attachment.html>