<div class="gmail_quote">On Tue, Jul 6, 2010 at 1:48 AM, Duncan Sands <span dir="ltr"><<a href="mailto:baldrick@free.fr">baldrick@free.fr</a>></span> wrote:<br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">

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

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

<br>Nick<br> </div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">

> -        } else if (Name == "uname" ||<br>
> -                   Name == "unlink" ||<br>
> +        } else if (Name == "uname") {<br>
> +          if (FTy->getNumParams() != 1 ||<br>
> +              !FTy->getParamType(0)->isPointerTy())<br>
> +            continue;<br>
> +       setIsHalting(F);<br>
<br>
strange indentation.<br>
<br>
> +  // Definitions with weak linkage may be overridden at linktime with<br>
> +  // something that writes memory, so treat them like declarations.<br>
<br>
-> something that infinite loops, so treat them like declarations.<br>
<br>
Otherwise looks good to me.<br>
<br>
Ciao,<br>
<br>
Duncan.<br>
_______________________________________________<br>
llvm-commits mailing list<br>
<a href="mailto:llvm-commits@cs.uiuc.edu">llvm-commits@cs.uiuc.edu</a><br>
<a href="http://lists.cs.uiuc.edu/mailman/listinfo/llvm-commits" target="_blank">http://lists.cs.uiuc.edu/mailman/listinfo/llvm-commits</a><br>
</blockquote></div><br>