<div dir="ltr">Hi<span style="font-size:12.8px"> </span><span style="font-size:12.8px">Venugopal,</span><br style="font-size:12.8px"><div><span style="font-size:12.8px"><br></span></div><div><span style="font-size:12.8px">> </span><span style="font-size:12.8px">Sean Eveson (cc’d) did some initial work on loop widening to mitigate this problem.</span></div><div><span style="font-size:12.8px"><br></span></div><div><span style="font-size:12.8px">I started to work on this, but have unfortunately not had time to take the next steps. There is a mode which does 'loop widening' which is off by default as the state after the loop is completely cleared which can lead to false positives. The idea is to improve on the widening, by changing it to only clear state that might be affected by the loop.</span></div><div><span style="font-size:12.8px"><br></span></div><div><span style="font-size:12.8px">To enable the loop widening pass: "-analyzer-config widen-loops=true".</span></div><div><span style="font-size:12.8px"><br></span></div><div><span style="font-size:12.8px">> </span><span style="color:rgb(0,0,0);font-family:tahoma;font-size:13.3333px">Maybe -analyzer-max-loop is interesting. It tells Clang analyzer how many times you want to go through loops. The bigger value the better analysis, but slower analysis.</span></div><div><span style="font-size:12.8px"><br></span></div><div><span style="font-size:12.8px">An issue you will run in to when changing </span><span style="color:rgb(0,0,0);font-family:tahoma;font-size:13.3333px">analyzer-max-loop is that it also affects variable-bound loops. If you set the max loop higher to work around your problem you will see some slow down for the concrete-bound loops, but you will see a lot more for the variable-bound ones.</span></div><div><span style="color:rgb(0,0,0);font-family:tahoma;font-size:13.3333px"><br></span></div><div><span style="color:rgb(0,0,0);font-family:tahoma;font-size:13.3333px">Example:</span></div><div><span style="color:rgb(0,0,0);font-family:tahoma;font-size:13.3333px">// Where the value of j is unknown.</span><span style="color:rgb(0,0,0);font-family:tahoma;font-size:13.3333px"><br></span></div><div><span style="color:rgb(0,0,0);font-family:tahoma;font-size:13.3333px">for (i = 0; i < j; ++i) {</span></div><div><span style="color:rgb(0,0,0);font-family:tahoma;font-size:13.3333px">  // ...</span></div><div><span style="color:rgb(0,0,0);font-family:tahoma;font-size:13.3333px">}</span></div><div><span style="color:rgb(0,0,0);font-family:tahoma;font-size:13.3333px">foo(i);</span></div><div><span style="color:rgb(0,0,0);font-family:tahoma;font-size:13.3333px"><br></span></div><div><span style="color:rgb(0,0,0);font-family:tahoma;font-size:13.3333px">As far as I remember, with a max loop of 1000 and no other limits on the analyzer, `foo` will be called for all the values between 0..~1000. This is because the analyzer will branch each time it reaches the loop condition.</span></div><div><span style="color:rgb(0,0,0);font-family:tahoma;font-size:13.3333px"><br></span></div><div><span style="color:rgb(0,0,0);font-family:tahoma;font-size:13.3333px">Regards,</span></div><div><span style="color:rgb(0,0,0);font-family:tahoma;font-size:13.3333px">Sean Eveson</span></div></div><div class="gmail_extra"><br clear="all"><div><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><span style="color:rgb(0,0,0);font-family:'Segoe UI','Segoe UI Web Regular','Segoe UI Symbol','Helvetica Neue',Helvetica,Arial,sans-serif;font-size:13px;line-height:18.85px">Sean Eveson</span><br style="color:rgb(0,0,0);font-family:'Segoe UI','Segoe UI Web Regular','Segoe UI Symbol','Helvetica Neue',Helvetica,Arial,sans-serif;font-size:13px;line-height:18.85px"><span style="color:rgb(0,0,0);font-family:'Segoe UI','Segoe UI Web Regular','Segoe UI Symbol','Helvetica Neue',Helvetica,Arial,sans-serif;font-size:13px;line-height:18.85px">SN Systems - Sony Computer Entertainment Group</span><br></div></div></div>
<br><div class="gmail_quote">On Fri, Feb 24, 2017 at 7:54 PM, Devin Coughlin <span dir="ltr"><<a href="mailto:dcoughlin@apple.com" target="_blank">dcoughlin@apple.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Venugopal,<br>
<span class=""><br>
> On Feb 23, 2017, at 7:07 PM, Venugopal Raghavan via cfe-dev <<a href="mailto:cfe-dev@lists.llvm.org">cfe-dev@lists.llvm.org</a>> wrote:<br>
><br>
> Hi,<br>
><br>
> I am re-sending the question I asked under a different thread so that the subject is more relevant to the topic.<br>
><br>
> I did not quite realize it earlier but it seems that the static analyzer unrolls a loop up to a certain number of times and then stops exploring paths beyond that. In the checker I have written, I get the message "Block count exceeded" and then state exploration stops. As a result, my checker give false positives and does not achieve what it sets out to do.<br>
<br>
</span>The analyzer makes no promises about exhaustivity and in many cases will drop flows and stop path exploration. If your analysis depends on full path exploration to prevent false positives (as compared to false negatives) then it is going to be an uphill battle to eliminate false positives.<br>
<br>
As you noted, for concrete-bound loops stopping path exploration can be particularly pernicious because after unrolling the loop N times the analyze simply stops. Any code dominated by the loop exit will simply not be explored, leading to false negatives.<br>
<br>
Sean Eveson (cc’d) did some initial work on loop widening to mitigate this problem. The basic idea there was rather than simply stopping, the analyzer would “forget” any specific information about a particular iteration through the loop and proceed analyzing after the loop without any assumptions about how many times the loop was unrolled. This would lose some precision but gain coverage for code after the loop. This feature not complete and is off by default, but you can see the beginnings of it at <<a href="https://reviews.llvm.org/D12358" rel="noreferrer" target="_blank">https://reviews.llvm.org/<wbr>D12358</a>><br>
<span class="HOEnZb"><font color="#888888"><br>
Devin<br>
<br>
</font></span></blockquote></div><br></div>