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

[Duncan Sands]

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?

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