<div dir="ltr">Hi Péter!<br><div><div class="gmail_extra"><br><div class="gmail_quote">On 28 August 2017 at 17:46, Péter Szécsi <span dir="ltr"><<a href="mailto:peterszecsi95@gmail.com" target="_blank">peterszecsi95@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div>Hello everyone,<br><br></div>I am working on loop modeling improvements in the Static Analyzer and sent recently some patches on loop widening. (<a href="https://reviews.llvm.org/D36690" target="_blank">D36690</a>)</div><div>There is already a widening solution (widen-loops config) which invalidates every MemRegion in the process. My version only widen loops which meets specific requirements (e.g. does not contain any pointers). It is hidden behind a new flag 'widen-loops-conservative'. (It is conservative in the sense that it only widen specific loops.)</div><div><br></div><div>In general case the difference of the 2 version is:<div class="m_-6706824923310058091gmail-m_7869373378371586527gmail-m_7873275108326179076gmail-remarkup-table-wrap"><table class="m_-6706824923310058091gmail-m_7869373378371586527gmail-m_7873275108326179076gmail-remarkup-table">
<tbody><tr><td>widen-loops</td><td>Invalidate everything</td></tr>
<tr><td>widen-loops-conservative</td><td>Only invalidate modified variables</td></tr>
</tbody></table></div><br></div><div>But a huge difference when there are pointers (most precisely if it encounters a statement which can result a modified variable but it is not handled yet):</div><div><div class="m_-6706824923310058091gmail-m_7869373378371586527gmail-m_7873275108326179076gmail-remarkup-table-wrap"><table class="m_-6706824923310058091gmail-m_7869373378371586527gmail-m_7873275108326179076gmail-remarkup-table">
<tbody><tr><td>widen-loops</td><td>Invalidate everything</td></tr>
<tr><td>widen-loops-conservative</td><td>Invalidate nothing (don't widen)</td></tr>
</tbody></table></div><br></div></div></blockquote><div><br></div><div>Just to bo clear, when you say you invalidate nothing, you mean to terminate the analysis on that particular path right? <br></div><div>What would be the effect of turning on both options? Is that a valid configuration?</div><div>E.g.: invalidating only modified variables when no pointer trickery is involved is way better than invalidate everything. But if one would like to maximize the coverage, it makes more sense to invalidate everything when pointers are involved.</div><div><br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>I thought the new flag is necessary since this two options are very different. However, Sean (who created the current version of widening in <a href="https://reviews.llvm.org/D12358" target="_blank">D12358</a>) suggested to replace the 'loop-widening' option with the new functionality. For considering this I collected the relevant statistics (note: the 'widen-loops' config encountered some crashes on C++ projects so the statistics are only collected on the files which has passed):<br></div><div><b>Widen </b>states for the current implementation<b>, Widen v2 </b>states for the new (<a href="https://reviews.llvm.org/D36690" target="_blank">D36690</a>) implementation.<br></div><div><br></div><div>Coverage measurements (% of reachable basic blocks statistics)<br>
<table width="606" height="82" cellspacing="0" border="0">
<colgroup width="107"></colgroup>
<colgroup width="92"></colgroup>
<colgroup width="111"></colgroup>
<colgroup width="80"></colgroup>
<colgroup width="97"></colgroup>
<colgroup width="80" span="2"></colgroup>
<tbody><tr>
<td valign="bottom" height="18" align="center"><font color="#000000"><br></font></td>
<td valign="bottom" align="center"><font color="#000000">curl </font></td>
<td valign="bottom" align="center"><font color="#000000">libpng</font></td>
<td valign="bottom" align="center"><font color="#000000">vim</font></td>
<td valign="bottom" align="center"><font color="#000000">bitcoin</font></td>
<td valign="bottom" align="center"><font color="#000000">ffmpeg</font></td>
<td valign="bottom" align="center"><font color="#000000">xerces</font></td>
</tr>
<tr>
<td valign="bottom" height="20" align="right"><font color="#000000">Normal</font></td>
<td valign="bottom" align="center"><font color="#000000">58.05</font></td>
<td valign="bottom" align="center"><font color="#000000">55.07</font></td>
<td valign="bottom" align="center"><font color="#000000">51.12</font></td>
<td valign="bottom" align="center"><font color="#000000">69.37</font></td>
<td valign="bottom" align="center"><font color="#000000">49.78</font></td>
<td valign="bottom" align="center"><font color="#000000">74.86</font></td>
</tr>
<tr>
<td valign="bottom" height="18" align="right"><font color="#000000">Widen</font></td>
<td valign="bottom" align="center"><font color="#000000">75.8</font></td>
<td valign="bottom" align="center"><font color="#000000">56.69</font></td>
<td valign="bottom" align="center"><font color="#000000">51.54</font></td>
<td valign="bottom" align="center"><font color="#000000">72.06</font></td>
<td valign="bottom" align="center"><font color="#000000">65.63</font></td>
<td valign="bottom" align="center"><font color="#000000">76.06</font></td>
</tr>
<tr>
<td valign="bottom" height="18" align="right"><font color="#000000">Widen v2</font></td>
<td valign="bottom" align="center"><font color="#000000">70.7</font></td>
<td valign="bottom" align="center"><font color="#000000">55.92</font></td>
<td valign="bottom" align="center"><font color="#000000">51.77</font></td>
<td valign="bottom" align="center"><font color="#000000">69.67</font></td>
<td valign="bottom" align="center"><font color="#000000">59.53</font></td>
<td valign="bottom" align="center"><font color="#000000">75.04</font></td>
</tr>
</tbody></table>
<br></div><div>The number of founded bugs:<br></div></div></blockquote><div><br></div><div>I believe founded is a typo here, you might want to correct that before you send this to the mailing list (in case that is your intention).<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div></div><div>
<table width="594" height="80" cellspacing="0" border="0">
<colgroup width="107"></colgroup>
<colgroup width="92"></colgroup>
<colgroup width="111"></colgroup>
<colgroup width="80"></colgroup>
<colgroup width="97"></colgroup>
<colgroup width="80" span="2"></colgroup>
<tbody><tr>
<td valign="bottom" height="18" align="center"><font color="#000000"><br></font></td>
<td valign="bottom" align="center"><font color="#000000">curl </font></td>
<td valign="bottom" align="center"><font color="#000000">libpng</font></td>
<td valign="bottom" align="center"><font color="#000000">vim</font></td>
<td valign="bottom" align="center"><font color="#000000">bitcoin</font></td>
<td valign="bottom" align="center"><font color="#000000">ffmpeg</font></td>
<td valign="bottom" align="center"><font color="#000000">xerces</font></td>
</tr>
<tr>
<td valign="bottom" height="18" align="right"><font color="#000000">Normal</font></td>
<td valign="bottom" align="center"><font color="#000000">35</font></td>
<td valign="bottom" align="center"><font color="#000000">32</font></td>
<td valign="bottom" align="center"><font color="#000000">81</font></td>
<td valign="bottom" align="center"><font color="#000000">9</font></td>
<td valign="bottom" align="center"><font color="#000000">375</font></td>
<td valign="bottom" align="center"><font color="#000000">52</font></td>
</tr>
<tr>
<td valign="bottom" height="18" align="right"><font color="#000000">Widen</font></td>
<td valign="bottom" align="center"><font color="#000000">35</font></td>
<td valign="bottom" align="center"><font color="#000000">36</font></td>
<td valign="bottom" align="center"><font color="#000000">94</font></td>
<td valign="bottom" align="center"><font color="#000000">12</font></td>
<td valign="bottom" align="center"><font color="#000000">456</font></td>
<td valign="bottom" align="center"><font color="#000000">57</font></td>
</tr>
<tr>
<td valign="bottom" height="18" align="right"><font color="#000000">Widen v2</font></td>
<td valign="bottom" align="center"><font color="#000000">27</font></td>
<td valign="bottom" align="center"><font color="#000000">34</font></td>
<td valign="bottom" align="center"><font color="#000000">84</font></td>
<td valign="bottom" align="center"><font color="#000000">10</font></td>
<td valign="bottom" align="center"><font color="#000000">369</font></td>
<td valign="bottom" align="center"><font color="#000000">51</font></td>
</tr>
</tbody></table>
</div><div><br></div></div></blockquote><div><br></div><div>Why do you lose findings with Widen v2 but not with Widen? You widen fewer loops in v2, so I would not expect it to use up the analysis budget more often than the original version. <br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>The new findings are mostly resulted by the invalidation process and not the coverage increasement. So in general they are false positives which was founded by invalidating the informations (on MemRegions) we have.<br></div></div></blockquote><div><br></div><div>What is the most frequent reson behind the false positives? Infeasible execution paths or something else? This might be interesting, because in the future we might add suppression heuristics to the most frequent cases. E.g. suppressing findings on paths that are created when we split the exploded graph as the result of the invalidation (e.g.: branching on a value that is no longer known due to the invalidation).<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><br></div><div>Although there is a small observable coverage loss it's offset by the number of the false positives not discovered.<br></div></div></blockquote><div><br></div><div>Do you mean compared to widen?<br></div><div><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div></div><div>In conclusion it would be beneficial to replace the current implementation of the 'widen-loops' option.<br><br></div><div>What do you think?<br><br></div><div>Cheers,<br></div><div>Peter<br></div></div>
</blockquote></div><br></div></div></div>