<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><br class=""><div><blockquote type="cite" class=""><div class="">On Aug 28, 2017, at 8:46 AM, Péter Szécsi <<a href="mailto:peterszecsi95@gmail.com" class="">peterszecsi95@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class=""><div class=""><div class="">Hello everyone,<br class=""><br class=""></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" class="">D36690</a>)</div><div class="">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 class=""><br class=""></div><div class="">In general case the difference of the 2 version is:<div class="gmail-m_7869373378371586527gmail-m_7873275108326179076gmail-remarkup-table-wrap"><table class="gmail-m_7869373378371586527gmail-m_7873275108326179076gmail-remarkup-table">
<tbody class=""><tr class=""><td class="">widen-loops</td><td class="">Invalidate everything</td></tr>
<tr class=""><td class="">widen-loops-conservative</td><td class="">Only invalidate modified variables</td></tr>
</tbody></table></div><br class=""></div><div class="">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 class=""><div class="gmail-m_7869373378371586527gmail-m_7873275108326179076gmail-remarkup-table-wrap"><table class="gmail-m_7869373378371586527gmail-m_7873275108326179076gmail-remarkup-table">
<tbody class=""><tr class=""><td class="">widen-loops</td><td class="">Invalidate everything</td></tr>
<tr class=""><td class="">widen-loops-conservative</td><td class="">Invalidate nothing (don't widen)</td></tr>
</tbody></table></div><br class="">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" class="">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 class=""></div><div class=""><b class="">Widen </b>states for the current implementation<b class="">, Widen v2 </b>states for the new (<a href="https://reviews.llvm.org/D36690" target="_blank" class="">D36690</a>) implementation.<br class=""></div><div class=""><br class=""></div><div class="">Coverage measurements (% of reachable basic blocks statistics)<br class="">
<table width="606" cellspacing="0" border="0" height="82" class="">
<colgroup width="107" class=""></colgroup>
<colgroup width="92" class=""></colgroup>
<colgroup width="111" class=""></colgroup>
<colgroup width="80" class=""></colgroup>
<colgroup width="97" class=""></colgroup>
<colgroup width="80" span="2" class=""></colgroup>
<tbody class=""><tr class="">
<td align="center" valign="bottom" height="18" class=""><font class=""><br class=""></font></td>
<td align="center" valign="bottom" class=""><font class="">curl </font></td>
<td align="center" valign="bottom" class=""><font class="">libpng</font></td>
<td align="center" valign="bottom" class=""><font class="">vim</font></td>
<td align="center" valign="bottom" class=""><font class="">bitcoin</font></td>
<td align="center" valign="bottom" class=""><font class="">ffmpeg</font></td>
<td align="center" valign="bottom" class=""><font class="">xerces</font></td>
</tr>
<tr class="">
<td align="right" valign="bottom" height="20" class=""><font class="">Normal</font></td>
<td align="center" valign="bottom" class=""><font class="">58.05</font></td>
<td align="center" valign="bottom" class=""><font class="">55.07</font></td>
<td align="center" valign="bottom" class=""><font class="">51.12</font></td>
<td align="center" valign="bottom" class=""><font class="">69.37</font></td>
<td align="center" valign="bottom" class=""><font class="">49.78</font></td>
<td align="center" valign="bottom" class=""><font class="">74.86</font></td>
</tr>
<tr class="">
<td align="right" valign="bottom" height="18" class=""><font class="">Widen</font></td>
<td align="center" valign="bottom" class=""><font class="">75.8</font></td>
<td align="center" valign="bottom" class=""><font class="">56.69</font></td>
<td align="center" valign="bottom" class=""><font class="">51.54</font></td>
<td align="center" valign="bottom" class=""><font class="">72.06</font></td>
<td align="center" valign="bottom" class=""><font class="">65.63</font></td>
<td align="center" valign="bottom" class=""><font class="">76.06</font></td>
</tr>
<tr class="">
<td align="right" valign="bottom" height="18" class=""><font class="">Widen v2</font></td>
<td align="center" valign="bottom" class=""><font class="">70.7</font></td>
<td align="center" valign="bottom" class=""><font class="">55.92</font></td>
<td align="center" valign="bottom" class=""><font class="">51.77</font></td>
<td align="center" valign="bottom" class=""><font class="">69.67</font></td>
<td align="center" valign="bottom" class=""><font class="">59.53</font></td>
<td align="center" valign="bottom" class=""><font class="">75.04</font></td>
</tr>
</tbody></table>
<br class=""></div><div class="">The number of founded bugs:<br class=""></div><div class="">
<table width="594" cellspacing="0" border="0" height="80" class="">
<colgroup width="107" class=""></colgroup>
<colgroup width="92" class=""></colgroup>
<colgroup width="111" class=""></colgroup>
<colgroup width="80" class=""></colgroup>
<colgroup width="97" class=""></colgroup>
<colgroup width="80" span="2" class=""></colgroup>
<tbody class=""><tr class="">
<td align="center" valign="bottom" height="18" class=""><font class=""><br class=""></font></td>
<td align="center" valign="bottom" class=""><font class="">curl </font></td>
<td align="center" valign="bottom" class=""><font class="">libpng</font></td>
<td align="center" valign="bottom" class=""><font class="">vim</font></td>
<td align="center" valign="bottom" class=""><font class="">bitcoin</font></td>
<td align="center" valign="bottom" class=""><font class="">ffmpeg</font></td>
<td align="center" valign="bottom" class=""><font class="">xerces</font></td>
</tr>
<tr class="">
<td align="right" valign="bottom" height="18" class=""><font class="">Normal</font></td>
<td align="center" valign="bottom" class=""><font class="">35</font></td>
<td align="center" valign="bottom" class=""><font class="">32</font></td>
<td align="center" valign="bottom" class=""><font class="">81</font></td>
<td align="center" valign="bottom" class=""><font class="">9</font></td>
<td align="center" valign="bottom" class=""><font class="">375</font></td>
<td align="center" valign="bottom" class=""><font class="">52</font></td>
</tr>
<tr class="">
<td align="right" valign="bottom" height="18" class=""><font class="">Widen</font></td>
<td align="center" valign="bottom" class=""><font class="">35</font></td>
<td align="center" valign="bottom" class=""><font class="">36</font></td>
<td align="center" valign="bottom" class=""><font class="">94</font></td>
<td align="center" valign="bottom" class=""><font class="">12</font></td>
<td align="center" valign="bottom" class=""><font class="">456</font></td>
<td align="center" valign="bottom" class=""><font class="">57</font></td>
</tr>
<tr class="">
<td align="right" valign="bottom" height="18" class=""><font class="">Widen v2</font></td>
<td align="center" valign="bottom" class=""><font class="">27</font></td>
<td align="center" valign="bottom" class=""><font class="">34</font></td>
<td align="center" valign="bottom" class=""><font class="">84</font></td>
<td align="center" valign="bottom" class=""><font class="">10</font></td>
<td align="center" valign="bottom" class=""><font class="">369</font></td>
<td align="center" valign="bottom" class=""><font class="">51</font></td>
</tr>
</tbody></table>
</div><div class=""><br class="">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 class=""><br class=""></div><div class="">Although there is a small observable coverage loss it's offset by the number of the false positives not discovered.<br class=""></div><div class="">In conclusion it would be beneficial to replace the current implementation of the 'widen-loops' option.<br class=""><br class=""></div><div class="">What do you think?<br class=""></div></div></div></blockquote><div><br class=""></div><div>I do not think the choice of flag you use matters much at this point as both features are very experimental. (If Sean is fine with you reusing the flag, that likely means no one else is using it.) The next step for this project is to design and implement primitives for loop modeling in the CFG. That will allow us to have a solid ground for this feature. Could you send out a design proposal of how loops will be modeled in the CFG to support widening? </div><div><br class=""></div><div>Would be happy to help you if you have questions!</div><div>Anna</div></div><div><br class=""><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div class=""><br class=""></div><div class="">Cheers,<br class=""></div><div class="">Peter<br class=""></div></div>
</div></blockquote></div><br class=""></body></html>