<div dir="ltr">I gave this some thought, and realized that we could divide the "should-not-have-happened" cases into 2 categories:<br><br><div>1. The unexplored block is within a function that the analyzer visited.</div><div>2. The unexplored block lies within a function that the analyzer didn't even visit.</div><div><br></div><div>For example:<br><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">01 int flag;</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">02 bool coin();</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">03 </span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">04 void foo() {</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">05 flag = coin();</span><span style="color:rgb(0,0,0);font-family:"Courier New";font-size:12px;white-space:pre-wrap"> // no note, but there should be one</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">06 }</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">07</span></p><p style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">08 void bar(int &i) {</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">09 if (flag) // assumed false</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">10 i = new int;</span></p><p style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">11 }</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">12 </span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">13 int main() {</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">14 int *x = 0; // x initialized to 0</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">15 flag = 1;</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">16 foo();</span><span style="color:rgb(0,0,0);font-family:"Courier New";font-size:12px;white-space:pre-wrap"> // no note, but there should be one</span></p><p style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">17 bar(x);</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">18 foo(); // no note, but there should be one</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">19 </span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">20 if (flag) // assumed true</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">21 *x = 5; // warn</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">22 }</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><br></p><p style="line-height:1.38;margin-top:0pt;margin-bottom:0pt">Observe the subtle difference that on line 17, function bar is called, and the first branch lies in that function. This is definitely a "category 1" case, since the analyzer inlined and visited <font face="courier new, monospace">bar()</font>, but again, failed the realize the importance of flag due to not visiting line 10, and makes no mention of line 16 in the bugreport.</p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><br class="gmail-Apple-interchange-newline">01 int flag;</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">02 bool coin();</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">03 </span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">04 void foo() {</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">05 flag = coin();</span><span style="color:rgb(0,0,0);font-family:"Courier New";font-size:12px;white-space:pre-wrap"> // no note, but there should be one</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">06 }</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">07</span></p><p style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">08 void bar(int &i) {</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">09 i = new int;</span></p><p style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">10 }</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">11 </span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">12 int main() {</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">13 int *x = 0; // x initialized to 0</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">14 flag = 1;</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">15 foo();</span><span style="color:rgb(0,0,0);font-family:"Courier New";font-size:12px;white-space:pre-wrap"> // no note, but there should be one</span></p><p style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><font color="#000000" face="Courier New"><span style="font-size:12px;white-space:pre-wrap">16 if (flag) // assumed false</span></font></p><p style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">17 bar(x);</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">18 foo(); // no note, but there should be one</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">19 </span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">20 if (flag) // assumed true</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">21 *x = 5; // warn</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">22 }</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><br></p><p style="line-height:1.38;margin-top:0pt;margin-bottom:0pt">In this example, the if statement stays, but the assignment to x is now found in bar(). In this case, the analyzer didn't explore <font face="courier new, monospace">bar(),</font> so it's a "category 2" case.</p><p style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><br></p><p style="line-height:1.38;margin-top:0pt;margin-bottom:0pt">Now, the reason why these categories are important is that if the analyzer actually explored a function, it solves the problem of parameters: for the example shown for "category 1", we can simply ask the analyzer whether <font face="courier new, monospace">x</font> in function <font face="courier new, monospace">main()</font> is the same as <font face="courier new, monospace">i</font> in function <font face="courier new, monospace">bar()</font>. This is, as stated in my previous letter, far more difficult for "category 2" cases.</p><p style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><br></p><p style="line-height:1.38;margin-top:0pt;margin-bottom:0pt">I think when I'm finished with the "must-have-happened" cases, I could start enhancing NoStoreFuncVisitor to gather conditions possibly worth tracking for "category 1" cases, see whether an intraprocedural slicing algorithm makes sense, could worry about resolving parameters for the other case one when I get there.</p><p style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><br></p><p style="line-height:1.38;margin-top:0pt;margin-bottom:0pt">Any thoughts on this approach? :)</p></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, 8 Jun 2019 at 01:59, Kristóf Umann <<a href="mailto:dkszelethus@gmail.com">dkszelethus@gmail.com</a>> wrote:<br></div><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">Hi!<br><br>I'm currently working on a GSoC project that aims to improve the description we provide for bug reports the Static Analyzer emits.<br><br><div>We divided the problem (that the bugreports didn't explain how the bug came about very well) into two parts:</div><div><br></div><div>1. The information is available in the bug path (basically parts of the code the analyzer actually explored on that particular path of execution). We refer to these as the "must-have-happened" case.</div><div>2. The information isn't available, possibly not even in the ExplodedGraph (parts of the program the analyzer explored on all paths of execution). We call this the "should-not-have-happened" case.</div><div><br></div><div><span id="gmail-m_-840552459534237689gmail-docs-internal-guid-832b5cb3-7fff-3777-21ce-4e1d0c7bc76e"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">01 int flag;</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">02 bool coin();</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">03 </span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">04 void foo() {</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">05 flag = coin();</span><span style="color:rgb(0,0,0);font-family:"Courier New";font-size:12px;white-space:pre-wrap"> // no note, but there should be one</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">06 }</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">07 </span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">08 int main() {</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">09 int *x = 0; // x initialized to 0</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">10 flag = 1;</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">11 foo();</span><span style="color:rgb(0,0,0);font-family:"Courier New";font-size:12px;white-space:pre-wrap"> // no note, but there should be one</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">12 if (flag) // assumed false</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">13 x = new int;</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">14 foo(); // no note, but there should be one</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">15 </span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">16 if (flag) // assumed true</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">17 *x = 5; // warn</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">18 }</span></p></span><br class="gmail-m_-840552459534237689gmail-Apple-interchange-newline"></div><div>The first branch is a good example for the "should-not-have-happened" case: the bug path doesn't contain line 13, so we don't really know whether the condition on line 12 is a big deal, which in this case it is (unlike if it only guarded a print of some sort)</div><div><br></div><div>The second branch is a good example for the "must-have-happened" case: we know that the condition on line 16 is very important.</div><div><br></div><div>I like to think that I made a very decent progress on the first part, as it's objectively a lot simpler. A great addition to the analyzer is that it now understands (at least, when my patches land) control dependencies in the CFG. With that, we can figure out that flag's value on line 16 is crucial, so we track it, resulting in notes being added on line 14, and on line 5, explaining that flag's value changed.</div><div><br></div><div>However, we are very unsure about how to tackle the second part on the project. I gave this a lot of thought, we had a couple meetings in private, and I'd like to share where I am with this.</div><div><br></div><div>My project proposed to implement a static backward program slicing algorithm which would definitely be amazing, but seems to be an unrealistic approach. Basically, any slicing algorithm that is interprocedural would require a system dependence graph, something we just simply don't have, not even for LLVM.</div><div><br></div><div>Whenever pointer semantics are in the picture, we have a really hard time: it's something that is super difficult to reason about without symbolic execution, and it would probably be a good idea not to tackle such cases until we come up with something clever (maybe the pset calculation Gábor Horváth is working on?). We should, however, being able to handle reference parameters.</div><div><br></div><div>So then, what's the goal exactly?</div><div><br></div><div>We'd like to teach the analyzer that some code blocks (even in other functions) could have written the variable that is responsible for the bug (x, in the included example), and is very important to the bug report. We could use this information to track variables similarly to the "must-have-happened" case: track conditions that prevented the write from happening.</div><div><br></div><div>To the specifics. I think it's reasonable to implement an <i>intraprocedural</i> slicing algorithm. For the included example, I think we should be able to discover the potential write to x on line 9. We don't need anything we already don't have to achieve this.</div><div><br></div><div>Reasoning across function boundaries could be achieved by inlining functions (as I understand it, simply insert the function's CFGBlocks), but there are big unknowns in this.</div><div><br></div><div>So my question is, do you think such inlining is possible? If not, should I just create a primitive variable-to-parameter mapping? Is there something else on the table?</div><div><br></div><div>Cheers!<br>Kristóf Umann</div></div>
</blockquote></div>