<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 27, 2017, at 7:35 PM, 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="">Some further measurements with the limit of 128 resulted better statistics!<br class=""></div><div class=""><div class=""><br class=""></div>Time measurements: (avg of 4 or 5 run depending on the project)<br class="">
<table border="0" width="668" cellspacing="0" height="81" class="">
<colgroup width="149" class=""></colgroup>
<colgroup width="111" class=""></colgroup>
<colgroup width="80" class=""></colgroup>
<colgroup width="97" class=""></colgroup>
<colgroup width="80" span="4" 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="">FFmpeg</td>
<td align="center" valign="bottom" class=""><font class="">xerces</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">LLVM</font></td>
</tr>
<tr class="">
<td style="text-align:right" valign="bottom" height="18" class=""><font class="">Normal</font></td>
<td align="center" valign="bottom" class=""><font class="">52.63</font></td>
<td align="center" valign="bottom" class=""><font class="">62.872</font></td>
<td align="center" valign="bottom" class=""><font class="">191.9225</font></td>
<td align="center" valign="bottom" class=""><font class="">208.25</font></td>
<td align="center" valign="bottom" class=""><font class="">526.215</font></td>
<td align="center" valign="bottom" class=""><font class="">229.9425</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">5044.62</font></td>
</tr>
<tr class="">
<td style="text-align:right" valign="bottom" height="18" class=""><font class="">Unroll_limit</font></td>
<td align="center" valign="bottom" class=""><font class="">54.402</font></td>
<td align="center" valign="bottom" class=""><font class="">59.946</font></td>
<td align="center" valign="bottom" class=""><font class="">198.5075</font></td>
<td align="center" valign="bottom" class=""><font class="">212.94</font></td>
<td align="center" valign="bottom" class=""><font class="">646.3325</font></td>
<td align="center" valign="bottom" class=""><font class="">234.045</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">5125.96</font></td>
</tr>
<tr class="">
<td style="text-align:right" valign="bottom" height="19" class=""><font class="">Unroll_limit_v2</font></td>
<td align="center" valign="bottom" class=""><font class="">51.952</font></td>
<td align="center" valign="bottom" class=""><font class="">58.908</font></td>
<td align="center" valign="bottom" class=""><font class="">193.2825</font></td>
<td align="center" valign="bottom" class=""><font class="">200.792</font></td>
<td align="center" valign="bottom" class=""><font class="">543.86</font></td>
<td align="center" valign="bottom" class=""><font class="">225.8675</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">4838.26</font></td>
</tr>
</tbody></table>
<div class="gmail_extra"><br class=""></div><div class="gmail_extra">Coverage measurements (% of reachable basic blocks statistics):<br class="">
<table border="0" width="658" cellspacing="0" height="86" class="">
<colgroup width="149" class=""></colgroup>
<colgroup width="111" class=""></colgroup>
<colgroup width="80" class=""></colgroup>
<colgroup width="97" class=""></colgroup>
<colgroup width="80" span="4" class=""></colgroup>
<tbody class=""><tr class="">
<td align="center" valign="bottom" height="20" 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="">FFmpeg</td>
<td align="center" valign="bottom" class=""><font class="">xerces</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">LLVM</font></td>
</tr>
<tr class="">
<td style="text-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.91</font></td>
<td align="center" valign="bottom" class=""><font class="">51.13</font></td>
<td align="center" valign="bottom" class=""><font class="">68.58</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>
<td style="text-align:center" valign="bottom" class=""><font class="">71.15</font></td>
</tr>
<tr class="">
<td style="text-align:right" valign="bottom" height="19" class=""><font class="">Unroll_limit</font></td>
<td align="center" valign="bottom" class=""><font class="">69.23</font></td>
<td align="center" valign="bottom" class=""><font class="">56.04</font></td>
<td align="center" valign="bottom" class=""><font class="">51.46</font></td>
<td align="center" valign="bottom" class=""><font class="">68.78</font></td>
<td align="center" valign="bottom" class=""><font class="">62.07</font></td>
<td align="center" valign="bottom" class=""><font class="">74.91</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">71.14</font></td>
</tr>
<tr class="">
<td style="text-align:right" valign="bottom" height="19" class=""><font class="">Unroll_limit_v2</font></td>
<td align="center" valign="bottom" class=""><font class="">69.14</font></td>
<td align="center" valign="bottom" class=""><font class="">56.04</font></td>
<td align="center" valign="bottom" class=""><font class="">51.53</font></td>
<td align="center" valign="bottom" class=""><font class="">68.7</font></td>
<td align="center" valign="bottom" class=""><font class="">52.46</font></td>
<td align="center" valign="bottom" class=""><font class="">74.91</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">71.13</font></td>
</tr>
</tbody></table>
<br class="">Summary table which contains the deviation in percent to the normal run.<br class=""></div><div class="gmail_extra">
<table border="0" width="676" cellspacing="0" height="101" class="">
<colgroup width="149" class=""></colgroup>
<colgroup width="111" class=""></colgroup>
<colgroup width="80" class=""></colgroup>
<colgroup width="97" class=""></colgroup>
<colgroup width="80" span="4" class=""></colgroup>
<tbody class=""><tr class="">
<td style="text-align:right" valign="bottom" height="18" class=""><font class=""><br class=""></font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">curl </font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">libpng</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">vim</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">bitcoin</font></td>
<td style="text-align:center" valign="bottom" class="">FFmpeg</td>
<td style="text-align:center" valign="bottom" class=""><font class="">xerces</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">LLVM</font></td>
</tr>
<tr class="">
<td style="text-align:right" valign="bottom" height="18" class=""><font class="">Unroll_limit – time</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">3.37</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">-4.7</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">3.43</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">2.25</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">22.8</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">1.78</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">1.61</font></td>
</tr>
<tr class="">
<td style="text-align:right" valign="bottom" height="19" class=""><font class="">Unroll_limit – cov</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">11.18</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">0.13</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">0.33</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">0.2</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">12.29</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">0.05</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">-0.01</font></td>
</tr>
<tr class="">
<td style="text-align:right" valign="bottom" height="18" class=""><font class="">Unroll_limit_v2 - time</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">-1.29</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">-6.31</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">0.71</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">-3.58</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">3.35</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">-1.78</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">-4.1</font></td>
</tr>
<tr class="">
<td style="text-align:right" valign="bottom" height="18" class=""><font class="">Unroll_limit_v2 – cov</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">11.09</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">0.13</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">0.4</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">0.12</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">2.68</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">0.05</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">-0.02</font></td>
</tr>
</tbody></table>
</div><div class="gmail_extra"><br class=""></div><div class="gmail_extra">So according to these numbers the coverage has increased for (almost) every project while the time of the analysis has not changed drastically. In some cases it even decreased.<br class=""><br class="">The number of findings:<br class="">
<table border="0" width="669" cellspacing="0" height="82" class="">
<colgroup width="92" class=""></colgroup>
<colgroup width="111" class=""></colgroup>
<colgroup width="80" class=""></colgroup>
<colgroup width="97" class=""></colgroup>
<colgroup width="80" span="4" 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="">FFmpeg</td>
<td align="center" valign="bottom" class=""><font class="">xerces</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">LLVM</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="">10</font></td>
<td align="center" valign="bottom" class=""><font class="">375</font></td>
<td align="center" valign="bottom" class=""><font class="">52</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">181</font></td>
</tr>
<tr class="">
<td align="right" valign="bottom" height="18" class=""><font class="">Unroll</font></td>
<td align="center" valign="bottom" class=""><font class="">27</font></td>
<td align="center" valign="bottom" class=""><font class="">33</font></td>
<td align="center" valign="bottom" class=""><font class="">81</font></td>
<td align="center" valign="bottom" class=""><font class="">10</font></td>
<td align="center" valign="bottom" class=""><font class="">368</font></td>
<td align="center" valign="bottom" class=""><font class="">52</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">184</font></td>
</tr>
<tr class="">
<td align="right" valign="bottom" height="20" class=""><font class="">Unroll v2</font></td>
<td align="center" valign="bottom" class=""><font class="">27</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="">10</font></td>
<td align="center" valign="bottom" class=""><font class="">369</font></td>
<td align="center" valign="bottom" class=""><font class="">52</font></td>
<td style="text-align:center" valign="bottom" class=""><font class="">184</font></td>
</tr>
</tbody></table>
</div><div class="gmail_extra"><br class=""></div><div class="gmail_extra">Most of the lost findings (Curl, FFmpeg) come from the fact that those bugs were found in complex function where the analysis reached the maximum node number of the ExplodedGraph. LoopUnrolling caused some more paths (more precisely some path was not aborted as before) so the analyzer could not find the remaining ones. Some other bugs (FFmpeg) could disappear because we inlined more functions (or at least other functions) so we did not find the bug which was only found by analyzing it as a top level function. However, this means that other functions happened to be analyzed as top level and these resulted some new findings other than the ones which come from the increased coverage caused by the unrolling.</div><div class="gmail_extra"><br class=""></div><div class="gmail_extra">In view of these measurements I would suggest enabling this feature by default or at least considering it. </div></div></div></div></blockquote><div><br class=""></div><div>What mode would you recommend turning on by default? Would you suggest setting the loop iteration limit to 128 and using unroll 2 (or something else)?</div><div class=""><br class=""></div><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div class=""><div class="gmail_extra">(The main counter-argument to this could be that the concrete implementation could be enhanced since it stores data in the State which could be stored in the LocationContext.</div></div></div></div></blockquote><div><br class=""></div><div>How much data are you storing in the state (info about each loop or just cases where the bound is known)? Storing data in the state might effect memory consumption, so it would be important to measure that it did not regress, especially, if you store additional information in most nodes. </div><br class=""><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div class=""><div class="gmail_extra"> But, I think that other than the implementation details, the functionality itself and the measurement results are great.)<br class=""></div><div class="gmail_extra"><br class=""></div><div class="gmail_extra">What do you think?<br class=""><br class=""></div></div></div></div></blockquote><div><br class=""></div><div>You’ve made a lot of progress during the summer. Good work!</div><div>Anna</div><div><br class=""></div></div><div><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div class=""><div class="gmail_extra">Peter<br class=""></div><div class="gmail_extra"><br class=""></div><div class="gmail_extra"><br class=""><div class="gmail_quote">2017-08-24 17:32 GMT+02:00 Péter Szécsi <span dir="ltr" class=""><<a href="mailto:peterszecsi95@gmail.com" target="_blank" class="">peterszecsi95@gmail.com</a>></span>:<br class=""><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr" class="">Hello everyone,<br class=""><br class=""><div class="">I am working on improving the loop modeling strategy of the Clang Static Analyzer.<br class=""></div><div class="">In
the current state of the analyzer it handles loops quite simple. It
unrolls it 4 time by default and than cut the analysis of that path
where the loop would have been unrolled more times.<br class=""><br class=""></div><div class="">One
motivation, if not anything else, can be that there were already
questions on this behaviour in the cfe-dev mailing list, even it was
thought as a bug.<br class=""></div><div class="">If we want to have a motivation goal
which can be expressed in a more objective way than the coverage of the
analysis is the closest what can show the impact of the modeling. Why?<br class=""></div><div class="">Because the naive loop handling (described above) can easily lead to unsimulated/unchecked code lines. A small example for that:<br class=""></div><div class=""><br class=""></div><div class=""><span style="font-family:monospace,monospace" class="">int f(){</span></div><div class=""><span style="font-family:monospace,monospace" class=""> int a[6];</span><br class=""></div><div class=""><font face="monospace,monospace" class=""> for(int i = 0; i < 6; i++)</font></div><div class=""><font face="monospace,monospace" class=""> a[i] = i+2;</font></div><div class=""><font face="monospace,monospace" class=""> //complex body</font></div><div class=""><font face="monospace,monospace" class="">}<br class=""></font></div><div class=""><font face="monospace,monospace" class=""><br class=""></font></div><div class="">In
this example the analysis will be stopped at the 4th step of the loop
and it would not be continued after the loop. So this cause a lot of
coverage loss in this case. For this problem I experimented with
identifying specific known bound loops which would be worth to
completely unroll. (eg. the above loop in <span style="font-family:monospace,monospace" class="">f()</span>)<br class=""><br class=""></div><div class="">At the moment a loop has to fulfill the following requirements to be worth unrolled:<br class="">- Currently only forStmts can be considered.<br class="">- The bound has to be an integer literal. (eg. i < 5, i >= MACRO_TO_LITERAL)<br class="">- The counter variable (i) has not escaped before/in the body of the loop and<br class=""> changed only in the increment statement corresponding to the loop. It also<br class=""> has to be initialized by a literal in the corresponding initStmt.<br class=""> - Does not contain goto, switch and returnStmt.<br class="">These version is marked as <b class="">Unroll</b> in the statistics.<br class=""><br class=""></div><div class="">In
addition to that I run the measurements with a twist. So whenever an
unrolled loop is creates new branches then we consider it as a normal
(non-unroll) loop in the further analysis. It is done because of the
exponential behaviour of the ExplodedGraph (symbolic execution) it could
create a lot of new paths which will be analysed but has only a few
difference to the one step ahead analyzed path. This is marked as <b class="">Unroll_v2</b> in the statistics.<br class=""></div><div class=""><br class=""></div><div class="">Time measurements: (avg of 5 run)<br class=""></div><div class="">
<table border="0" cellspacing="0" class="">
<colgroup width="80" span="3" class=""></colgroup>
<colgroup width="97" class=""></colgroup>
<colgroup width="80" span="3" 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 style="text-align:right" valign="bottom" height="18" class=""><font class="">Normal</font></td>
<td align="center" valign="bottom" class=""><font class="">50.168</font></td>
<td align="center" valign="bottom" class=""><font class="">62.128</font></td>
<td align="center" valign="bottom" class=""><font class="">180.404</font></td>
<td align="center" valign="bottom" class=""><font class="">197.385</font></td>
<td align="center" valign="bottom" class=""><font class="">501.14</font></td>
<td align="center" valign="bottom" class=""><font class="">227.6075</font></td>
</tr>
<tr class="">
<td style="text-align:right" valign="bottom" height="18" class=""><font class="">Unroll</font></td>
<td align="center" valign="bottom" class=""><font class="">54.562</font></td>
<td align="center" valign="bottom" class=""><font class="">64.186</font></td>
<td align="center" valign="bottom" class=""><font class="">205.468</font></td>
<td align="center" valign="bottom" class=""><font class="">1767.475</font></td>
<td align="center" valign="bottom" class=""><font class="">1127.076</font></td>
<td align="center" valign="bottom" class=""><font class="">248.5375</font></td>
</tr>
<tr class="">
<td style="text-align:right" valign="bottom" height="19" class=""><font class="">Unroll v2</font></td>
<td align="center" valign="bottom" class=""><font class="">52.892</font></td>
<td align="center" valign="bottom" class=""><font class="">63.866</font></td>
<td align="center" valign="bottom" class=""><font class="">203.476</font></td>
<td align="center" valign="bottom" class=""><font class="">198.025</font></td>
<td align="center" valign="bottom" class=""><font class="">693.486</font></td>
<td align="center" valign="bottom" class=""><font class="">237.87</font></td>
</tr>
</tbody></table>
</div><div class=""><br class=""></div><div class="">Coverage measurements (% of reachable basic blocks statistics)<br class=""></div><div class="">
<table border="0" cellspacing="0" class="">
<colgroup width="80" span="3" class=""></colgroup>
<colgroup width="97" class=""></colgroup>
<colgroup width="80" span="3" class=""></colgroup>
<tbody class=""><tr class="">
<td align="center" valign="bottom" height="20" 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 style="text-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.91</font></td>
<td align="center" valign="bottom" class=""><font class="">51.13</font></td>
<td align="center" valign="bottom" class=""><font class="">68.58</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 style="text-align:right" valign="bottom" height="20" class=""><font class="">Unroll</font></td>
<td align="center" valign="bottom" class=""><font class="">69.1</font></td>
<td align="center" valign="bottom" class=""><font class="">56.04</font></td>
<td align="center" valign="bottom" class=""><font class="">51.41</font></td>
<td align="center" valign="bottom" class=""><font class="">68.7</font></td>
<td align="center" valign="bottom" class=""><font class="">62.18</font></td>
<td align="center" valign="bottom" class=""><font class="">74.79</font></td>
</tr>
<tr class="">
<td style="text-align:right" valign="bottom" height="20" class=""><font class="">Unroll v2</font></td>
<td align="center" valign="bottom" class=""><font class="">69.19</font></td>
<td align="center" valign="bottom" class=""><font class="">56.04</font></td>
<td align="center" valign="bottom" class=""><font class="">51.61</font></td>
<td align="center" valign="bottom" class=""><font class="">68.83</font></td>
<td align="center" valign="bottom" class=""><font class="">52.41</font></td>
<td align="center" valign="bottom" class=""><font class="">74.8</font></td>
</tr>
</tbody></table>
</div><div class=""><br class=""></div><div class="">Summary table which contains the deviation (percentage) to the normal run.<br class=""></div><div class="">
<table border="0" cellspacing="0" class="">
<colgroup width="170" class=""></colgroup>
<colgroup width="111" class=""></colgroup>
<colgroup width="80" class=""></colgroup>
<colgroup width="97" class=""></colgroup>
<colgroup width="80" span="3" 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 style="text-align:right" valign="bottom" height="18" class=""><font class="">Unroll – time</font></td>
<td align="center" valign="bottom" class=""><font class="">8.76</font></td>
<td align="center" valign="bottom" class=""><font class="">3.31</font></td>
<td align="center" valign="bottom" class=""><font class="">13.89</font></td>
<td align="center" valign="bottom" class=""><font class="">795.445</font></td>
<td align="center" valign="bottom" class=""><font class="">124.9</font></td>
<td align="center" valign="bottom" class=""><font class="">9.19</font></td>
</tr>
<tr class="">
<td style="text-align:right" valign="bottom" height="20" class=""><font class="">Unroll – coverage</font></td>
<td align="center" valign="bottom" class=""><font class="">11.05</font></td>
<td align="center" valign="bottom" class=""><font class="">0.13</font></td>
<td align="center" valign="bottom" class=""><font class="">0.28</font></td>
<td align="center" valign="bottom" class=""><font class="">0.12</font></td>
<td align="center" valign="bottom" class=""><font class="">12.4</font></td>
<td align="center" valign="bottom" class=""><font class="">-0.07</font></td>
</tr>
<tr class="">
<td style="text-align:right" valign="bottom" height="20" class=""><font class="">Unroll v2 - time</font></td>
<td align="center" valign="bottom" class=""><font class="">5.43</font></td>
<td align="center" valign="bottom" class=""><font class="">2.8</font></td>
<td align="center" valign="bottom" class=""><font class="">12.79</font></td>
<td align="center" valign="bottom" class=""><font class="">0.324</font></td>
<td align="center" valign="bottom" class=""><font class="">38.38</font></td>
<td align="center" valign="bottom" class=""><font class="">4.5</font></td>
</tr>
<tr class="">
<td style="text-align:right" valign="bottom" height="18" class=""><font class="">Unroll v2 – cov</font></td>
<td align="center" valign="bottom" class=""><font class="">11.14</font></td>
<td align="center" valign="bottom" class=""><font class="">0.13</font></td>
<td align="center" valign="bottom" class=""><font class="">0.48</font></td>
<td align="center" valign="bottom" class=""><font class="">0.25</font></td>
<td align="center" valign="bottom" class=""><font class="">2.63</font></td>
<td align="center" valign="bottom" class=""><font class="">-0.06</font></td>
</tr>
</tbody></table>
</div><div class="">The most outstanding (negative) difference is
that the analysis time of project bitcoin increased and took 8x more
time than in the normal case. That was single handedly caused by one
benchmark file which contains a lot of for loop which makes ~10,000,000
step.<br class="">(An improvement can be to not allow unrolling loops which takes
N or more steps where N could be a well chosen number - I am running
some measurements at the moment with the version N = 128).</div><div class=""><br class=""></div><div class=""><br class=""></div><div class="">The number of findings:<br class="">
<table border="0" cellspacing="0" class="">
<colgroup width="89" class=""></colgroup>
<colgroup width="111" class=""></colgroup>
<colgroup width="80" class=""></colgroup>
<colgroup width="97" class=""></colgroup>
<colgroup width="80" span="3" 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="">10</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="">Unroll</font></td>
<td align="center" valign="bottom" class=""><font class="">27</font></td>
<td align="center" valign="bottom" class=""><font class="">33</font></td>
<td align="center" valign="bottom" class=""><font class="">81</font></td>
<td align="center" valign="bottom" class=""><font class="">10</font></td>
<td align="center" valign="bottom" class=""><font class="">367</font></td>
<td align="center" valign="bottom" class=""><font class="">48</font></td>
</tr>
<tr class="">
<td align="right" valign="bottom" height="18" class=""><font class="">Unroll v2</font></td>
<td align="center" valign="bottom" class=""><font class="">27</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="">10</font></td>
<td align="center" valign="bottom" class=""><font class="">363</font></td>
<td align="center" valign="bottom" class=""><font class="">52</font></td>
</tr>
</tbody></table>
<br class=""></div><div class="">Most of the time it hasn't changed the founded bugs. On FFmpeg there are new finding which come from the fact that we are able to unroll loops (and analyze the codelines after them). However the unrolling resulted some loss of the findings as well. Most of the time (curl, ffmpeg) these loss was because these bugs were founded in complex functions on long paths which analysis exhausted the maximum limit of the nodes in the ExplodedGraph even in the normal analysis. It happened "faster" with the unroll feature since we so these paths were not analyzed thus the bugs were not found.<br class=""><br class=""></div><div class="">In
conclusion the unrolling of the above defined specific loops can have a
positive impact on the coverage (% of reachable basic blocks), however,
it comes with the price that it affects the running time. In most
projects (all except curl) the time increase % was higher than the
coverage increase %.<br class=""></div><div class=""><br class=""></div><div class="">So all in all, I think it is a feature which can be useful for a more <span class="m_-992560215787692292gmail-m_-7125241899016141017m_8795779713071489574gmail-m_-981880197780097369gmail-m_-8185922259641316962gmail-prop_content m_-992560215787692292gmail-m_-7125241899016141017m_8795779713071489574gmail-m_-981880197780097369gmail-m_-8185922259641316962gmail-prop m_-992560215787692292gmail-m_-7125241899016141017m_8795779713071489574gmail-m_-981880197780097369gmail-m_-8185922259641316962gmail-freetext">thoroughgoing analysis but should not be used by default at the time.<br class=""></span></div><div class=""><br class=""></div><div class="">What do you think?<br class=""></div><div class=""><br class=""></div><div class="">Cheers,<br class=""></div>Peter<br class=""><br class="">Note: if you are interested in the detailed results they are available
on the following site: <a href="http://cc.elte.hu/szepet/loop_modeling/unrolling/" target="_blank" class="">http://cc.elte.hu/szepet/loop_<wbr class="">modeling/unrolling/</a></div>
</blockquote></div><br class=""></div></div></div>
</div></blockquote></div><br class=""></body></html>