<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<br>
<br>
<div class="moz-cite-prefix">On 6/10/19 11:03 AM, Kristóf Umann
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAGcXOD497xUOSB4aDdFECn=m9ruNpOVAr6PLfvFASjHcQNj2Fw@mail.gmail.com">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<div dir="ltr">
<div dir="ltr"><br>
</div>
<br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On Mon, 10 Jun 2019 at
05:03, Artem Dergachev <<a
href="mailto:noqnoqneo@gmail.com" target="_blank"
moz-do-not-send="true">noqnoqneo@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 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>
</div>
</blockquote>
<div><br>
</div>
<div>I have explained myself poorly. I intend to implement an
<i>intraprocedural</i> slicing, but that would work <i>interprocedurally</i> by
resolving function calls with the help of the analyzer. This
is important, because for the by-the-book interprocedural
slicing you'd need a system dependence graph. Now, if a
function isn't inlined, we need to do this on our own. I see
a couple unknowns here (how deep do we explore such
functions? how to we resolve non-trivial parameter passing?
are we sure that tracking expressions here is actually
meaningful?) but I think tackling simple cases is
achievable.</div>
<div> </div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px
0.8ex;border-left:1px solid
rgb(204,204,204);padding-left:1ex">
<div bgcolor="#FFFFFF"> 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>
</div>
</blockquote>
<div><br>
</div>
<div>Would you agree that tracking flag however would be good?</div>
</div>
</div>
</blockquote>
<br>
Yes, totally.<br>
<br>
<blockquote type="cite"
cite="mid:CAGcXOD497xUOSB4aDdFECn=m9ruNpOVAr6PLfvFASjHcQNj2Fw@mail.gmail.com">
<div dir="ltr">
<div class="gmail_quote">
<div> </div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px
0.8ex;border-left:1px solid
rgb(204,204,204);padding-left:1ex">
<div bgcolor="#FFFFFF"> 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().</div>
</blockquote>
<blockquote class="gmail_quote" style="margin:0px 0px 0px
0.8ex;border-left:1px solid
rgb(204,204,204);padding-left:1ex">
<div bgcolor="#FFFFFF">
<div
class="m_3899269156412793041gmail-m_-8359532103913902229moz-cite-prefix">On
09.06.2019 17:50, Kristóf Umann wrote:<br>
</div>
<blockquote type="cite">
<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"
target="_blank" 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="m_3899269156412793041gmail-m_-8359532103913902229gmail-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="m_3899269156412793041gmail-m_-8359532103913902229gmail-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>
</div>
</blockquote>
</div>
</div>
</blockquote>
<br>
</body>
</html>