<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">On sqlite there are 8 new reports and one removed reports.<div class=""><br class=""></div><div class="">I think it’s natural that the number is high. In many cases we are saving 3x of the analyzer budget,</div><div class="">which is then spent finding new bugs.<br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Jan 31, 2018, at 9:52 PM, Anna Zaks <<a href="mailto:ganna@apple.com" class="">ganna@apple.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><meta http-equiv="Content-Type" content="text/html; charset=utf-8" class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><br class=""><div class=""><br class=""><blockquote type="cite" class=""><div class="">On Jan 31, 2018, at 9:41 PM, George Karpenkov <<a href="mailto:ekarpenkov@apple.com" class="">ekarpenkov@apple.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><br class="Apple-interchange-newline"><br class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;"><blockquote type="cite" class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px;"><div class="">On Jan 31, 2018, at 8:46 PM, Anna Zaks <<a href="mailto:ganna@apple.com" class="">ganna@apple.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div class=""><br class=""><blockquote type="cite" class=""><div class="">On Jan 31, 2018, at 5:00 PM, George Karpenkov <<a href="mailto:ekarpenkov@apple.com" class="">ekarpenkov@apple.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;">The list did not like a posting with many images,<div class="">so I have posted an evaluation to phabricator:<span class="Apple-converted-space"> </span><a href="https://reviews.llvm.org/M1" class="">https://reviews.llvm.org/M1</a></div><div class=""><br class=""></div><div class="">The text part was:</div><div class=""><br class=""></div><div class=""><p class="" style="margin: 0px 0px 12px; padding: 0px; border: 0px; font-family: "Segoe UI", "Segoe UI Emoji", "Segoe UI Symbol", Lato, "Helvetica Neue", Helvetica, Arial, sans-serif; font-size: 13px;">After fixing a few bugs, another evaluation of the approach shows considerably better results.</p><p class="" style="margin: 0px 0px 12px; padding: 0px; border: 0px; font-family: "Segoe UI", "Segoe UI Emoji", "Segoe UI Symbol", Lato, "Helvetica Neue", Helvetica, Arial, sans-serif; font-size: 13px;">On openssl:</p><ul class="remarkup-list" style="margin: 12px 0px 12px 30px; padding: 0px; border: 0px; list-style-position: initial; list-style-image: initial; font-family: "Segoe UI", "Segoe UI Emoji", "Segoe UI Symbol", Lato, "Helvetica Neue", Helvetica, Arial, sans-serif; font-size: 13px;"><li class="remarkup-list-item" style="margin: 0px; padding: 0px; border: 0px; line-height: 1.7em;">9 reports added</li><li class="remarkup-list-item" style="margin: 0px; padding: 0px; border: 0px; line-height: 1.7em;">1 report removed</li></ul><p class="" style="margin: 0px 0px 12px; padding: 0px; border: 0px; font-family: "Segoe UI", "Segoe UI Emoji", "Segoe UI Symbol", Lato, "Helvetica Neue", Helvetica, Arial, sans-serif; font-size: 13px;">On postgresql:</p><ul class="remarkup-list" style="margin: 12px 0px 12px 30px; padding: 0px; border: 0px; list-style-position: initial; list-style-image: initial; font-family: "Segoe UI", "Segoe UI Emoji", "Segoe UI Symbol", Lato, "Helvetica Neue", Helvetica, Arial, sans-serif; font-size: 13px;"><li class="remarkup-list-item" style="margin: 0px; padding: 0px; border: 0px; line-height: 1.7em;">377 reports added</li><li class="remarkup-list-item" style="margin: 0px; padding: 0px; border: 0px; line-height: 1.7em;">43 reports removed</li></ul><p class="" style="margin: 0px 0px 12px; padding: 0px; border: 0px; font-family: "Segoe UI", "Segoe UI Emoji", "Segoe UI Symbol", Lato, "Helvetica Neue", Helvetica, Arial, sans-serif; font-size: 13px;">On sqlite3 + a few other misc files:</p><ul class="remarkup-list" style="margin: 12px 0px 12px 30px; padding: 0px; border: 0px; list-style-position: initial; list-style-image: initial; font-family: "Segoe UI", "Segoe UI Emoji", "Segoe UI Symbol", Lato, "Helvetica Neue", Helvetica, Arial, sans-serif; font-size: 13px;"><li class="remarkup-list-item" style="margin: 0px; padding: 0px; border: 0px; line-height: 1.7em;">239 reports added</li></ul></div></div></div></blockquote><div class="">This is a lot of additional reports! Are there actually that many bugs in that codebase that need to be fixed?</div></div></div></div></blockquote><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br class=""></div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">Out of 239 or in general? The 239 reports mostly come from non-sqlite files.</div></div></blockquote><div class=""><br class=""></div>Can you provide data just for sqlite?</div><div class=""><br class=""></div><div class="">For postgresql the number of additional reports also seems very high.</div><div class=""><br class=""><blockquote type="cite" class=""><div class=""><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">In general, for most practical purposes C codebases provide an infinite supply of bugs :P</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br class=""></div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">On a more serious note, I don’t think this is very surprising.</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">The previous emails in this chain have shown that for loops, the analyzer has a very high chance of entering</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">a degenerate behavior where the longest path through the loop will be evaluated first,</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">and a large chunk of the analyzer budget is then spent on going around the loop in circles.</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br class=""></div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">Under new exploration strategy, paths which increase coverage are explored first, and then we can actually find</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">bugs with the budget which is no longer spent going in circles.</div><br class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;"><blockquote type="cite" class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px;"><div class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div class=""><div class="">I think we need to manually evaluate these reports.</div></div></div></div></blockquote><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br class=""></div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">Yes, I’ve looked through quite a few of them, the false positive ratio seems to be actually getting lower,</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">as the probability of the report being a false positive grows with the path length,</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">and path lengths are getting much shorter.</div><br class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;"><blockquote type="cite" class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px;"><div class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div class="">Also, we have to make sure uniquing works. Do all regression tests pass?<br class=""></div></div></div></blockquote><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br class=""></div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">Yes.</div><blockquote type="cite" class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px;"><div class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div class=""><blockquote type="cite" class=""><div class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div class=""><ul class="remarkup-list" style="margin: 12px 0px 12px 30px; padding: 0px; border: 0px; list-style-position: initial; list-style-image: initial; font-family: "Segoe UI", "Segoe UI Emoji", "Segoe UI Symbol", Lato, "Helvetica Neue", Helvetica, Arial, sans-serif; font-size: 13px;"><li class="remarkup-list-item" style="margin: 0px; padding: 0px; border: 0px; line-height: 1.7em;">1 report removed</li></ul><p class="" style="margin: 0px 0px 12px; padding: 0px; border: 0px; font-family: "Segoe UI", "Segoe UI Emoji", "Segoe UI Symbol", Lato, "Helvetica Neue", Helvetica, Arial, sans-serif; font-size: 13px;">Note on histograms (here and below)</p><div class="" style="margin: 0px; padding: 0px; border: 0px; font-family: "Segoe UI", "Segoe UI Emoji", "Segoe UI Symbol", Lato, "Helvetica Neue", Helvetica, Arial, sans-serif; font-size: 13px;">-> Histograms only show the ratio for same bugs (compared using issue hash),<br class="" style="margin-top: 0px;">that is, if the histogram says “decrease by a factor of three”, it means the new approach finds the *same* bug<br class="">with a path size 1/3d of the original<br class="">-> Histograms omit data points where the path length has remained the same<br class="">(as otherwise they completely dominate the histogram)<br class="">-> Relative histograms are provided as both ratio and logarithm of the ratio.<br class="">Logarithms of the ratio are convenient as they are symmetric in case changes balance out<br class="">(e.g. log(1/2) = -log(2/1))</div><div class=""><br class=""><blockquote type="cite" class=""><div class="">On Jan 30, 2018, at 4:23 PM, George Karpenkov <<a href="mailto:ekarpenkov@apple.com" class="">ekarpenkov@apple.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div class="">Preliminary evaluation of a patch which prefers exploring nodes associated with statements which weren’t seen before first:</div><div class=""><br class=""></div>On openssl:<div class=""><br class=""></div><div class=""> - Adds four reports</div><div class=""> - Removes four reports </div><div class=""> - Path lengths before: 317, 75, 75, 72, 70, 58, 50, 50, 44, 36, 23, 23, 21, 21, 20, 20, 19, 19, 19, 19, 18, 18, 18, 16, 15, 15, 15, 14, 13, 13, 12, 11, 11, 9, 7, 7, 6, 4</div><div class=""> - Path lengths after: 72, 60, 59, 53, 53, 52, 46, 38, 37, 30, 29, 28, 23, 21, 20, 19, 19, 19, 19, 19, 18, 16, 15, 15, 15, 15, 13, 13, 12, 12, 11, 9, 8, 7, 7, 7, 6, 4</div><div class=""><br class=""></div><div class="">The quality of the added reports seems higher, mainly due to the fact that report length is shorter.</div><div class=""><br class=""></div><div class="">On postgresql:</div><div class=""><br class=""></div><div class=""> - Added 80 reports</div><div class=""> - Removed 154 reports</div><div class=""> -> Out of those, 72 are reports on the yacc/bison autogenerated files, so whatever the cause is, good thing they are gone</div><div class=""> - The overall number of reports is 1188</div><div class=""> - Path lengths are lower on overall, but not in such a dramatic way</div><div class=""> - For many reports, I am quite confused as to why they got removed</div><div class=""><br class=""></div><div class="">On sqlite:</div><div class=""><br class=""></div><div class=""> - 7 inserted, 7 removed</div><div class=""><br class=""></div><div class=""><div class=""><div class=""><blockquote type="cite" class=""><div class="">On Jan 30, 2018, at 1:10 PM, Artem Dergachev <<a href="mailto:noqnoqneo@gmail.com" class="">noqnoqneo@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><br class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;"><br class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;"><span class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; float: none; display: inline !important;">On 30/01/2018 12:40 PM, Gábor Horváth via cfe-dev wrote:</span><br class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;"><blockquote type="cite" class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;">Hi George, Artem,<br class=""><br class="">I am glad that you are looking into this problem!<br class=""><br class="">On 30 January 2018 at 01:12, George Karpenkov via cfe-dev <<a href="mailto:cfe-dev@lists.llvm.org" class="">cfe-dev@lists.llvm.org</a><span class="Apple-converted-space"> </span><<a href="mailto:cfe-dev@lists.llvm.org" class="">mailto:cfe-dev@lists.llvm.org</a>>> wrote:<br class=""><br class=""> Hi All,<br class=""><br class=""> I was investigating recently bug reports with very long analyzer<br class=""> paths (more than a few hundred nodes).<br class=""> In many of such cases the path is long for no good reason: namely,<br class=""> the analyzer would go 3 times around the loop before<br class=""> going further.<br class=""> The issue is surprisingly common, and it was exacerbated with a<br class=""> recent bump of analyzer thresholds.<br class=""><br class=""> The problem is reproduced on the following file:<br class=""><br class=""> ```<br class=""> extern int coin();<br class=""><br class=""> int foo() {<br class=""> int *x = 0;<br class=""> while (coin()) {<br class=""> if (coin())<br class=""> return *x;<br class=""> }<br class=""> return 0;<br class=""> }<br class=""><br class=""> void bar() {<br class=""> while(coin())<br class=""> if (coin())<br class=""> foo();<br class=""> }<br class=""> ```<br class=""><br class=""> While a shortest path to the error does not loop around, the<br class=""> current version of the analyzer<br class=""> will go around the loop three times before going further.<br class=""> (and we are quite fortunate that the unrolling limit for loops is<br class=""> three, otherwise it would keep going<br class=""> until the unrolling limit is reached).<br class=""><br class=""> Multiple issues were discovered during the investigation.<br class=""><br class=""> 1. Analyzer queue does not have a concept of priority, and<br class=""> performs a simple DFS by default.<br class=""> Thus if the successor of the if-branch under the loop in “bar"<br class=""> containing the desired destination is generated second,<br class=""> it will never be evaluated until the loop exploration limit is<br class=""> exhausted.<br class=""><br class=""> 2. The previous issue slows down the exploration, but is not<br class=""> enough to get a pathological behavior of ultra-long paths.<br class=""> The second problem is a combination of:<br class=""> a) Block counter is not a part of a node's identity, and node A<br class=""> with a small block counter can be merged into a node B with a<br class=""> large block counter,<br class=""> and the resulting node will have a block counter associated with B.<br class=""><br class=""><br class="">Sorry for the questions, just wanted to clarify some things. You mean ExplodedNodes? By merge, you mean the same thing as "caching-out"?<br class=""></blockquote><br class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;"><span class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; float: none; display: inline !important;">Yeah, George notices that if we construct the same ExplodedNode on two different paths that have different block counts, we'd cache-out on the latter path, while the worklist element of the first path would still possess the original block count.</span><br class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;"><br class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;"><span class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; float: none; display: inline !important;">Which happens a lot when we're evaluating foo() conservatively in this example.</span><br class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;"><br class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;"><span class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; float: none; display: inline !important;">This isn't directly related to our problem though, as i noticed in<span class="Apple-converted-space"> </span></span><a href="http://lists.llvm.org/pipermail/cfe-dev/2018-January/056719.html" class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;">http://lists.llvm.org/pipermail/cfe-dev/2018-January/056719.html</a><span class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; float: none; display: inline !important;"><span class="Apple-converted-space"> </span>.</span><br class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;"><br class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;"><br class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;"><blockquote type="cite" class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;"> b) The issue in (a) is triggered due to our heuristic to abandon<br class=""> the function’s exploration and switch to conservative evaluation<br class=""> if we are already *inside* the function and the block limit has<br class=""> been reached.<br class=""><br class=""> Issue (1) combined with (2-b) causes the problematic behavior: the<br class=""> issue is discovered on the longest path first,<br class=""> and by the time the shortest path gets to “bar”, the block limit<br class=""> is already reached, and the switch to conservative evaluation is<br class=""> performed.<br class=""><br class=""> Thus there are two mitigation strategies currently being evaluated:<br class=""><br class=""> i) Remove the heuristic in (2-b)<br class=""> ii) Use a priority queue to hold nodes which should be explored;<br class=""> prefer nodes which give new source code coverage over others<br class=""> (or alternatively prefer nodes with least depth of loop stack)<br class=""><br class=""> Me and Artem have evaluated the option (i) and the results were<br class=""> surprisingly good: some reports disappear, and slightly more<br class=""> reports reappear.<br class=""> The quality of the new reports seems to be slightly better, and I<br class=""> am still trying to figure out exact reasons.<br class=""> I suspect merges resulting from heuristic (2-b) cause us to lose<br class=""> some actually valid reports.<br class=""><br class=""><br class="">I also find the results surprising. If you have more information about the reasons please do not forget to follow up this thread. We are curious :)<br class=""><br class=""><br class=""> Option (ii) has not been evaluated fully yet, but current<br class=""> experiments show slightly more reports (5-10%), and a radical<br class=""> decline in report lengths<br class=""> (e.g. from 400+ to <100 for largest reports)<br class=""><br class=""> Are there any thoughts on the matter?<br class=""><br class=""> Personally I think we should do both (i) and (ii), even if they<br class=""> would shake up the results.<br class=""> - The original idea for heuristics (2-b) was to be able to produce<br class=""> a report even if we are out of budget, but since it actually<br class=""> results in less reports,<br class=""> I think the data does not validate the approach.<br class=""><br class=""> - Option (ii) is AFAIK how most similar engines work, and should<br class=""> get us much larger coverage (and shorter paths) for the same node<br class=""> budget,<br class=""> even at the cost of log(N) overhead of the priority queue.<br class=""> Moreover, not having the priority queue will bite us later if we<br class=""> ever decide to further<br class=""> increase the analyzer budget or to increase the unroll limit.<br class=""><br class=""><br class="">I wonder what will the performance implication be. But I also like the idea of having a priority queue. If we find that we get more and better report<br class="">but also have worse performance, we can also consider reducing the analysis budget slightly.<br class=""><br class="">Regards,<br class="">Gábor<br class=""><br class=""><br class=""> George<br class=""><br class=""><br class=""><br class=""> _______________________________________________<br class=""> cfe-dev mailing list<br class=""> <a href="mailto:cfe-dev@lists.llvm.org" class="">cfe-dev@lists.llvm.org</a><span class="Apple-converted-space"> </span><<a href="mailto:cfe-dev@lists.llvm.org" class="">mailto:cfe-dev@lists.llvm.org</a>><br class=""> <a href="http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev" class="">http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev</a><br class=""> <<a href="http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev" class="">http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev</a>><br class=""><br class=""><br class=""><br class=""><br class="">_______________________________________________<br class="">cfe-dev mailing list<br class=""><a href="mailto:cfe-dev@lists.llvm.org" class="">cfe-dev@lists.llvm.org</a><br class=""><a href="http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev" class="">http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev</a></blockquote></div></blockquote></div></div></div></div></div></blockquote></div></div></div></div></blockquote></div></div></div></blockquote></div></blockquote></div><br class=""></div></div></blockquote></div><br class=""></div></body></html>