<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
I was distracted and never got to actually do this, but i still
think it's a good idea to try out. Your results look very promising,
yay. I totally agree that systems of mutually-canceling bugs are
worth untangling even if the amount of false positives temporarily
increases.<br>
<br>
P.S. A related issue - if i go for this, i'd probably start with
relaxing the C++ container inlining heuristic, i.e. replacing it
with visitor-based suppressions, so that to still enjoy the benefits
of inlining.<br>
<br>
P.P.S. Mildly related - i noticed that it shouldn't be all that hard
to model extents of bindings within RegionStore, so that bindings to
sub-structures didn't overwrite bindings to super-structures simply
because they have the same base region and the same offset. The only
problem here is to model extents of *integers* because we don't
represent casts as part of SymbolRefs. All other sorts of SVals have
well-defined extents (including, say, lazy compound values).<br>
<br>
P.P.P.S. Not really related - just wanted to share an example of a
curious false positive due to *lack* of invalidation that i've seen
recently:<br>
<br>
int test(int **x) {<br>
int *y = *x;<br>
<br>
if (*y == 0)<br>
invalidate(x);<br>
<br>
// should not warn<br>
return 1 / *y;<br>
}<br>
<br>
<br>
<div class="moz-cite-prefix">On 1/22/19 2:44 AM, Gábor Horváth
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAPRL4a0EC69RWjSr4H9-JHp0U2D+VxNk3w3qt+MaaASML8FcUw@mail.gmail.com">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<div dir="ltr">
<div dir="ltr">
<div dir="ltr">
<div>Hi!</div>
<div><br>
</div>
<div>What is the status of this?<br>
</div>
<div dir="ltr"><br>
<div class="gmail_quote">
<div dir="ltr"
class="gmail-m_4684937666676712888gmail_attr">On Mon,
27 Nov 2017 at 16:24, Artem Dergachev via cfe-dev <<a
href="mailto:cfe-dev@lists.llvm.org" target="_blank"
moz-do-not-send="true">cfe-dev@lists.llvm.org</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">
<br>
* Invalidating base region when a field is invalidated
(as the whole <br>
base region is reachable through safe pointer
arithmetic).<br>
</blockquote>
<div><br>
</div>
<div>I was doing a little experiment and for the
projects I tested the number of results was either the
same or increased. Sometimes when the number of
results are increased I also lost some results which
could be either due to different use of the time
budget or ruling out more infeasible paths. The
interesting part is, when I turn on refutation, for
some projects we can also refute some bugs that we
could not earlier. See the exact numbers [1] and
exact bugs [2].</div>
<div><br>
</div>
<div>After looking at the new results I found only one
FP where the root cause was the less invalidation. But
it was an implementation artifact (we should
invalidate the super region of a field region, when
the super region is a union). <br>
</div>
<div><br>
</div>
<div>So while having more reports could be annoying, if
the root cause of FPs are not likely to be the less
invalidation I think it would be worth to actually do
less invalidation and have an annotation for cases
where we actually need more. In my opinion, currently,
when the aggressive invalidation hides some FPs where
the root cause is something else, we are only giving
ourselves a false sense of quality.<br>
</div>
<div><br>
</div>
<div>What do you think? Should we pursue this?<br>
</div>
<div><br>
</div>
<div>[1]: <a
href="https://docs.google.com/spreadsheets/d/1inqGzSAXHfcP-cJ6BuTAv7QYEpADxRcFyIa4v6bda6c/edit?usp=sharing"
moz-do-not-send="true">https://docs.google.com/spreadsheets/d/1inqGzSAXHfcP-cJ6BuTAv7QYEpADxRcFyIa4v6bda6c/edit?usp=sharing</a></div>
<div>[2]: <a
href="http://cc.inf.elte.hu:15013/Default/#"
moz-do-not-send="true">http://cc.inf.elte.hu:15013/Default/#</a><br>
</div>
</div>
</div>
</div>
</div>
</div>
</blockquote>
</body>
</html>