<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/18/19 3:44 PM, Gábor Horváth
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAPRL4a0Xk-8TKi=mNsYFjHc1H1v5kJPV-_HxtxRJBR=xMj7cSg@mail.gmail.com">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<div dir="ltr">
<div dir="ltr">
<div>Hi Kristóf,</div>
<div><br>
</div>
<div>Thanks for the report. I have been thinking about what
kind of user experience should we pursue. While my ideas
might be a bit opinionated, see my comments inline. <br>
</div>
</div>
<br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On Tue, 18 Jun 2019 at
20:47, 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>
This is an update on my GSoC project, "Enhancing bug
reports in the Clang Static Analyzer". We had some
discussions on phabricator, and some in private meetings,
and I think it's due to share how things are looking right
now.
<div><br>
</div>
<div>In my previous mail [1], I detailed the two distinct
categories we defined, the "must-have-happened" case
where every information is already in the bug path, and
the "should-not-have-happened" case when the information
isn't found in the bugpath. I divided the latter into
two subcategories, the "Inlined category" (initially
referred to as "category 1"), and the "Not inlined
category" (initally referred to as "category 2").</div>
<div><br>
</div>
<div>These categorizations are used to teach the analyzer
incrementally about which nodes in the bugpath deserve
special attention. For now, I plan to use this
information exclusively for finding control dependencies
to these nodes, and tracking their condition. Now, what
we mean under "tracking an expression value", is that to
add notes to the bug report relevant to that expression
value.</div>
<div><br>
</div>
<div>Ultimately, this means that my project depends
greatly on condition tracking yielding meaningful
addition of notes to the bug report, without adding
unimportant ones. Since I more-or-less finished my work
on the must-have-happened case (meaning that the
analyzer can now figure out control dependencies to
nodes contained in the bugpath), I'd like to detail how
I plan to work on this.</div>
<div><br>
</div>
<div>While evaluating an early prototype solution to the
"must-have-happened" case where the same expression
value tracking was used for both the bug-causing
variable and for the conditions, I found that in many
cases, the growth of bug length was intolerable. This
is, in part, caused by conditions being tracked to a
condition recursively, the conditions of asserts being
tracked, and that notes about a condition are not as
interesting as notes about the bug causing variable
(calls to operator bool for instance).</div>
<div><br>
</div>
<div>Fixing any of these requires me to teach the analyzer
the difference in between "THE value" and "just a
condition". The details are a little more complicated,
so I'll show some examples that point out certain cases:</div>
<div><b><br>
</b></div>
<div><b>Example 1.:</b></div>
<div><br>
</div>
<div><span
id="gmail-m_8684261205520343446gmail-m_-3381093670081869542gmail-docs-internal-guid-4371bc51-7fff-dc4f-3cfb-1e3c0d0fbc66">
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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.2;margin-top:0pt;margin-bottom:0pt"><span style="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.2;margin-top:0pt;margin-bottom:0pt"><span style="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.2;margin-top:0pt;margin-bottom:0pt"><span style="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.2;margin-top:0pt;margin-bottom:0pt"><span style="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></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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.2;margin-top:0pt;margin-bottom:0pt"><span style="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.2;margin-top:0pt;margin-bottom:0pt"><span style="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.2;margin-top:0pt;margin-bottom:0pt"><span style="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;</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 foo();</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 if (flag) // assumed true</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 *x = 5; // warn</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 }</span></p>
</span><b><br
class="gmail-m_8684261205520343446gmail-m_-3381093670081869542gmail-Apple-interchange-newline">
</b></div>
<div>In this example, it'd be great to see notes placed on
line 10 and 5, because if flag wasn't invalidated, the
bug would not have occurred (since flag is global, and
is initialized to 0). The analyzer normally wouldn't
place notes there, so we definitely should track flag up
to line 5.</div>
<div><b><br>
</b></div>
<div><b>Example 2.:</b></div>
<div><b><br>
</b></div>
<div><span style="background-color:transparent;color:rgb(0,0,0);font-family:"Courier New";white-space:pre-wrap">01 int flag;</span></div>
<span
id="gmail-m_8684261205520343446gmail-m_-3381093670081869542gmail-docs-internal-guid-af141fcb-7fff-5805-158d-0af705abc2d5">
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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.2;margin-top:0pt;margin-bottom:0pt"><span style="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.2;margin-top:0pt;margin-bottom:0pt"><span style="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.2;margin-top:0pt;margin-bottom:0pt"><span style="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 coin();</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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.2;margin-top:0pt;margin-bottom:0pt"><span style="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.2;margin-top:0pt;margin-bottom:0pt"><span style="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.2;margin-top:0pt;margin-bottom:0pt"><span style="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;</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 foo();</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 if (flag)</span><span style="color:rgb(0,0,0);font-family:"Courier New";white-space:pre-wrap"> // assumed true</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 *x = 5;</span><span style="color:rgb(0,0,0);font-family:"Courier New";white-space:pre-wrap"> // warn</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 }</span></p>
</span>
<div><br>
</div>
<div>This case is very similar, with the only difference
being that the analyzer conservatively assumed that coin
may have written flag (as it's a global variable). We
should track until line 5.</div>
</div>
</blockquote>
<div><br>
</div>
<div>I am not sure about this example. While the invalidation
of the global flag is definitely playing a role in this bug
report the point where the flag is actually invalidated
could seem quite arbitrary for the user. We might get the
invalidation when we first see a function that is not
defined in this TU, when we reach the maximum call stack
depth and so on. My point is, I am not sure if we actually
help the user by pinpointing the first function call where
the invalidation happens. A more user friendly way to think
about this problem is how could the user solve this false
positive? As far as I understand the cannonical solution
would be to add an assertion, so it would be better to put a
node close to the place where the user would change the
code, so I would put it in the stack frame of the bug. For
example we could generate a note for the call foo(), that
somewhere in that call stack the analyzer could no longer
track the value of flag, thus invalidated its contents. <a
class="gmail_plusreply" id="plusReplyChip-0"
href="mailto:adergachev@apple.com" tabindex="-1"
moz-do-not-send="true">@Artem Dergachev</a> what do you
think?<br>
</div>
</div>
</div>
</blockquote>
<br>
This is definitely one of the most annoying kinds of false positives
we have due to infeasible paths and over-eager assumption chains.
Like, you can add an assertion here, but it's going to look super
ugly:<br>
<br>
bool tmp_flag = flag;<br>
coin(); // why would anybody believe it touches flag in the first
place???<br>
assert(flag == tmp_flag && "sanity check");<br>
<br>
And even if the user would actually like to add something like that
to his code, it would require a powerful constraint solver to even
handle this assertion correctly.<br>
<br>
These are not very common, but they're so annoying that i probably
wouldn't be against marking reports as invalid immediately when we
see that an important control dependency relies on such invalidation
(we'll have to gather experimental data on that, of course).<br>
<br>
<blockquote type="cite"
cite="mid:CAPRL4a0Xk-8TKi=mNsYFjHc1H1v5kJPV-_HxtxRJBR=xMj7cSg@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 dir="ltr"><br
class="gmail-m_8684261205520343446gmail-m_-3381093670081869542gmail-Apple-interchange-newline">
<div><b>Example 3.:</b></div>
<div><b><br>
</b></div>
<div><span
id="gmail-m_8684261205520343446gmail-m_-3381093670081869542gmail-docs-internal-guid-7904e5bc-7fff-83e0-6794-7060f31972aa">
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="background-color:transparent;color:rgb(0,0,0);font-family:"Courier New";white-space:pre-wrap">01 void f(int flag) {</span><br>
</p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 int *x = 0;</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 if (flag)</span><span style="color:rgb(0,0,0);font-family:"Courier New";white-space:pre-wrap"> // assumed true</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 *x = 5;</span><span style="color:rgb(0,0,0);font-family:"Courier New";white-space:pre-wrap"> // warn</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 }</span></p>
</span><br
class="gmail-m_8684261205520343446gmail-m_-3381093670081869542gmail-Apple-interchange-newline">
</div>
<div>Here, the user could simply follow the arrows that
shows the path of execution: it isn't really important
what flag was initialized on the first line.</div>
<div><br>
</div>
<div><b>Example 4.:</b></div>
<div><b><br>
</b></div>
<div><span
id="gmail-m_8684261205520343446gmail-m_-3381093670081869542gmail-docs-internal-guid-6d80ef0f-7fff-a248-86b1-e6e82a5757ba">
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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.2;margin-top:0pt;margin-bottom:0pt"><span style="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</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 int getInt();</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 int main() {</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 int *x = 0;</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 int y = getInt();</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 flag = y;</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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)</span><span style="color:rgb(0,0,0);font-family:"Courier New";white-space:pre-wrap"> // assumed true</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 *x = 5;</span><span style="color:rgb(0,0,0);font-family:"Courier New";white-space:pre-wrap"> // warn</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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>
</span><br
class="gmail-m_8684261205520343446gmail-m_-3381093670081869542gmail-Apple-interchange-newline">
</div>
<div>Again, the user could see there was a write made to
flag on line 8 -- the question is, whether we should
explain y better. Right now, we're thinking that we
shouldn't, leading to the conclusion that flag here
shouldn't be tracked at all.</div>
</div>
</blockquote>
<div><br>
</div>
<div>Finding the place where flag was modified in a really big
function can still be challenging. While generating a note
would be an overkill I wonder if some middle ground like
highlighting the statement without additional text would
actually make sense for this case.<br>
</div>
</div>
</div>
</blockquote>
<br>
<br>
When it's in the same function, you can simply search for the
variable name to see all writes into it. It's not that hard. Even if
the variable is written into by pointer, you can see that its
address is taken and search for the pointer variable as well (though
annoying if there are too many levels of indirection).<br>
<br>
But, hmm, if the address is taken in a different stack frame, this
becomes much harder. I guess, writes that are made through pointers
should be highlighted, and we should also do our tracking to explain
why do we think that this pointer points to that variable.<br>
<br>
<br>
<blockquote type="cite"
cite="mid:CAPRL4a0Xk-8TKi=mNsYFjHc1H1v5kJPV-_HxtxRJBR=xMj7cSg@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 dir="ltr">
<div><br>
</div>
<div><b>Example 5.:</b></div>
<div><b><br>
</b></div>
<div><span
id="gmail-m_8684261205520343446gmail-m_-3381093670081869542gmail-docs-internal-guid-6d80ef0f-7fff-a248-86b1-e6e82a5757ba">
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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.2;margin-top:0pt;margin-bottom:0pt"><span style="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</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 int getInt();</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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</span></p>
<p
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 void foo() {</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 int y = getInt();</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 flag = y;</span></p>
<p
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 }</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 int main() {</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 int *x = 0;</span></p>
<p
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 foo();</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 if (flag)</span><span style="color:rgb(0,0,0);font-family:"Courier New";white-space:pre-wrap"> // assumed true</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 *x = 5;</span><span style="color:rgb(0,0,0);font-family:"Courier New";white-space:pre-wrap"> // warn</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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.2;margin-top:0pt;margin-bottom:0pt"><span style="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">
</span></p>
<p
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><font face="arial, sans-serif">Like Example 1-2, we should explain that flag was written on line 7, but like in Example 4., we shouldn't track y.</font></span></p>
</span></div>
</div>
</blockquote>
<div><br>
</div>
<div>Again, from the user's point of view, I think the
ultimate solution would be to have an interface, where we
does not present the part where y was tracked by default,
but the user could click on a button to actually expand that
part of the path in case she consider it interesting. This,
of course, is not part of you GSoC, I am just wondering what
is the ideal that we would like to pursue in the long run. <br>
</div>
</div>
</div>
</blockquote>
<br>
A more powerful UI could have indeed solved a lot of these problems
by telling users to do our work. But given that it comes with a
fairly large cost of developing such UIs for every tool that
integrates the Static Analyzer, i'd definitely try to push our own
effort of stuffing exactly as much information as necessary into the
report as far as possible.<br>
<br>
<blockquote type="cite"
cite="mid:CAPRL4a0Xk-8TKi=mNsYFjHc1H1v5kJPV-_HxtxRJBR=xMj7cSg@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 dir="ltr">
<div>
<div><b><br
class="gmail-m_8684261205520343446gmail-m_-3381093670081869542gmail-Apple-interchange-newline">
Example 6.:</b></div>
<div>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="background-color:transparent;color:rgb(0,0,0);font-family:"Courier New";white-space:pre-wrap">
01 void f(int flag) {</span><br>
</p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 int *x = 0;</span></p>
<p
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 assert(flag);</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 if (flag)</span><span style="color:rgb(0,0,0);font-family:"Courier New";white-space:pre-wrap"> // assumed true</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 *x = 5;</span><span style="color:rgb(0,0,0);font-family:"Courier New";white-space:pre-wrap"> // warn</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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>
</div>
</div>
<div><br>
</div>
<div>Currently, we mention nothing about line 3, yet we
say "Taking the true branch" on line 4, rather then
"Assuming the condition is true". This is because the
collapse point (point at which we constrain flag's value
to be true or false) isn't on line 4: the analysis only
continued past the assert since the analyzer assumed
flag to be non-zero. In this case, we would like to
track flag to the assert to explain why we are so
confident on line 5 that flag is non-zero.</div>
</div>
</blockquote>
<div><br>
</div>
<div>What do you mean by tracking tha flag back to the assert?
The reason why a note is useful because in this case either
the assert is wrong or the bug is a true positive. But
again, when the assert is in the same function we might not
want to generate additional note for this as this info might
easily be inferred by following the arrows in the report
(but we might highlight the assertion line, see my previous
comments). In case the assert is in a separate (inlined)
function it would make much more sense to generate a note.<br>
</div>
</div>
</div>
</blockquote>
<br>
Wouldn't the assert already contain a (prunable) note saying
"Assuming 'flag' is true"? I guess the only problem here is that the
note is prunable, so it won't be shown if the assert is wrapped into
a nested function call.<br>
<br>
<blockquote type="cite"
cite="mid:CAPRL4a0Xk-8TKi=mNsYFjHc1H1v5kJPV-_HxtxRJBR=xMj7cSg@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 dir="ltr">
<div><b><br
class="gmail-m_8684261205520343446gmail-m_-3381093670081869542gmail-Apple-interchange-newline">
Example 7.:</b></div>
<div>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="background-color:transparent;color:rgb(0,0,0);font-family:"Courier New";white-space:pre-wrap">
</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="background-color:transparent;color:rgb(0,0,0);font-family:"Courier New";white-space:pre-wrap">01 int getInt();</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="background-color:transparent;color:rgb(0,0,0);font-family:"Courier New";white-space:pre-wrap">02
03 void f(int flag) {</span><br>
</p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 int *x = 0;</span></p>
<p
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 = getInt();</span></p>
<p
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 assert(flag);</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 if (flag)</span><span style="color:rgb(0,0,0);font-family:"Courier New";white-space:pre-wrap"> // assumed true</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 *x = 5;</span><span style="color:rgb(0,0,0);font-family:"Courier New";white-space:pre-wrap"> // warn</span></p>
<p dir="ltr"
style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="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 }</span></p>
</div>
<div><br>
</div>
<div>Like Example 6, we should explain why know that flag
is non-zero on line 7 by tracking it back to line 6.
Like in the case of Example 4., the user could see where
flag was written, so we wouldn't like to see a note on
line 5.</div>
<div><br>
</div>
<div>So what's the takeaway? </div>
<div><br>
</div>
<div>After teaching the analyzer the difference in between
a condition and a "regularly tracked expression", I plan
to implement the following two rules:</div>
<div><br>
</div>
<div>Track a condition only if</div>
<div>a.) The collapse point doesn't coincide with the
condition point</div>
<div>b.) It was written in a nested stack frame.</div>
</div>
</blockquote>
<div><br>
</div>
<div>Do you mane a) or b), or a) and b)? Also, what to do with
"multiple collapse point" events like:</div>
<div><br>
</div>
<div><span style="font-family:courier new,monospace">if ( a
< 10 ) ;</span></div>
<div><span style="font-family:courier new,monospace">if ( a
< 5) // Here we do add new constraints to a, but we
also had other constraints before. Do you consider this to
coincide or not?<br>
</span></div>
<div><span style="font-family:courier new,monospace"> ...</span><br>
</div>
</div>
</div>
</blockquote>
<br>
I'd rather track the condition *until* we cover those points (which
implies not tracking it at all when there are no b.)-points and the
a.)-point coincide with the current terminator), rather than track
it forever if we have those points.<br>
<br>
By collapse point i meant the point where the (bool)condition
collapses to a constant-false or a constant-true (in the true case
the condition itself doesn't necessarily collapse to a constant 1).
It doesn't happen every time we introduce a constraint.<br>
<br>
<br>
<blockquote type="cite"
cite="mid:CAPRL4a0Xk-8TKi=mNsYFjHc1H1v5kJPV-_HxtxRJBR=xMj7cSg@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 dir="ltr">
<div><br>
</div>
<div>We hope that by implementing this, tracking
conditions to conditions would be kept at bay without a
counter to limit the depth of recursion, and the
intolerable growth of bug length with drastically
shorten. I do expect skeletons to fall out of the
closet, but I am confident that this is a good initial
approach.</div>
<div><br>
</div>
<div>As explained earlier, this is mission number one, so
I'll prioritize getting it right before pursuing the
"should-not-have-happened" case.</div>
<div><br>
</div>
<div>One thing I did not touch on just yet, is the case
where an assert was (correctly, by the way) regarded as
a control dependency, and it's condition was tracked.
This is undoubtedly undesirable, but figuring out
whether the condition is found in an assert is rather
difficult. Asserts are often implemented as a macro, and
could have a very, for a lack of a better word, esoteric
implementations on certain platforms. We discussed
trying to tinker with the control dependency calculator,
namely skipping over nodes that have two successors and
one of them leads to noreturn node, but I still need
time to figure out something reliable.</div>
</div>
</blockquote>
<div><br>
</div>
<div>Some asserts consists of more basic blocks. Having two
successors where one of them is a <span
style="font-family:courier new,monospace">noreturn</span>
block is not a sufficient condition. Consider for example <span
style="font-family:courier new,monospace">assert(a
&& b); </span>Here the basic block for evaluating
<span style="font-family:courier new,monospace">a</span>
will either go to the next line after assertion or to the
evaluation of<span style="font-family:courier new,monospace">
b</span> which is not a <span style="font-family:courier
new,monospace">noreturn</span> block. While it is true
that from node a we will either go to the next non-assert
block or end up in a <span style="font-family:courier
new,monospace">noreturn</span> block, the <span
style="font-family:courier new,monospace">noreturn</span>
block might not be an immediate successor of node <span
style="font-family:courier new,monospace">a</span>. <br>
</div>
</div>
</div>
</blockquote>
<br>
Forgot to mention, i have a history with the CFG for asserts that's
mostly contained in <a class="moz-txt-link-freetext" href="https://reviews.llvm.org/D28023">https://reviews.llvm.org/D28023</a> and
<a class="moz-txt-link-freetext" href="https://reviews.llvm.org/D35673">https://reviews.llvm.org/D35673</a>. This is the reason why i believe
that some implementation of assert() have a lot of CFG blocks on
their own, regardless of how many CFG blocks does it take to
evaluate the assert condition.<br>
<br>
<blockquote type="cite"
cite="mid:CAPRL4a0Xk-8TKi=mNsYFjHc1H1v5kJPV-_HxtxRJBR=xMj7cSg@mail.gmail.com">
<div dir="ltr">
<div class="gmail_quote">
<div><br>
</div>
<div>Regards,</div>
<div>Gabor<br>
</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 dir="ltr">
<div><br>
</div>
<div>Thanks to everyone who helped me along: Artem
Dergachev, Gábor Horváth, Ádám Balogh, Jakub Kuderski,
and Zoltán Porkoláb!</div>
<div><br>
</div>
<div>Cheers,</div>
<div>Kristóf</div>
<div><br>
</div>
<div>[1] <a
href="http://lists.llvm.org/pipermail/cfe-dev/2019-June/062535.html"
target="_blank" moz-do-not-send="true">http://lists.llvm.org/pipermail/cfe-dev/2019-June/062535.html</a> </div>
</div>
</blockquote>
</div>
</div>
</blockquote>
<br>
</body>
</html>