<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
The problem we're solving is *entirely* about inter-procedural
analysis. Like, as long as there are no inlined calls on the path
(and therefore no pruning is being done), then there's no problem at
all: the user can easily see that the value is untouched by direct
observation.<br>
<br>
In this sense i find the lack of note in example 2 completely
non-problematic (as long as control dependency tracking lands). It's
not a problem that the user isn't told that bar() could have
initialized 'x', because the user already knows that bar() is not
even called in the first place.<br>
<br>
However, there may be a combination of category 1 and category 2
that is much more interesting: what if main() unconditionally calls
foo() that conditionally calls bar() that unconditionally
initializes the value? Eg.:<br>
<br>
void bar(int *x) {<br>
*x = 1; // the interesting event that doesn't happen<br>
}<br>
<br>
void foo(int *x) {<br>
if (rand()) // control dependency of the interesting event<br>
bar(x);<br>
}<br>
<br>
int main() {<br>
int x;<br>
foo(&x);<br>
use(x); // use of uninitialized value<br>
}<br>
<br>
In this case it is essential to highlight the path within foo() so
that to explain how it fails to call bar().<br>
<br>
<div class="moz-cite-prefix">On 09.06.2019 17:50, Kristóf Umann
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAGcXOD6y+5nRo-C4HuS48FC56phD=ohQHE6oF0WG-LvZvfe+xA@mail.gmail.com">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<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">
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
face="Courier New" color="#000000"><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"
moz-do-not-send="true">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>
</blockquote>
<br>
</body>
</html>