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

[Gabor Greif]

On Jul 6, 10:48 am, Duncan Sands <baldr... 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

Hi Nick, Duncan,

I assume by "looping" you also mean (mutually) recursive
tail-calling without ever returning?

What about recursive non-tail calling without return? This
will exhaust the stack and probably terminate then. Does
"halting" cover this situation?


Just my 2 cents!

   Gabor



>
> 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?
>
> > -        } 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-comm... at cs.uiuc.eduhttp://lists.cs.uiuc.edu/mailman/listinfo/llvm-commits