<div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote">On 31 March 2016 at 16:52, Artem Dergachev <span dir="ltr"><<a href="mailto:dergachev.a@samsung.com" target="_blank">dergachev.a@samsung.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div text="#000000" bgcolor="#FFFFFF"><span class="">
On 31.03.2016 15:54, Gábor Horváth wrote:<br>
<blockquote type="cite">
<div dir="ltr">
<div class="gmail_extra">
<div class="gmail_quote">I think that timestamps might not be
a general solution to this problem, see the next inline
response. But as a side not, do you plan to use timestamps
to use this problem:<br>
<br>
void bar(int *b) {<br>
foo(b); // [1] calling foo()<br>
}<br>
void foo(int *a) {<br>
*a = 0;<br>
if (a == 0) {<br>
// [2] warn: null-dereference<br>
}<br>
}<br>
</div>
</div>
</div>
</blockquote></span>
Oh, the check-after-use for delayed positives. We did not fix this
yet because we didn't agree on how much this is really unwanted. In
fact, for most kinds of bugs we'd like to have some kind of
check-after-use checks, but we should also be able to turn it off.
The solution we're having in mind is to consider the program state
in the delayed-check-node to see if the bug gets reproduced inside
it (we remember the whole node anyway for bug reporter purposes),
though we didn't think really deeply about it yet, so it may fail to
work. The current code produces such positives.<span class=""><br>
<blockquote type="cite">
<div dir="ltr">
<div class="gmail_extra">
<div class="gmail_quote">
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
On the other hand, i don't think that there are other
places that explicitly rely on assuming different symbols
to represent *different* values. It's only true for the
store, which expects different base-regions to
non-overlap, even when the regions are symbolic. Say, the
constraint manager, upon encountering "if (a == b)",
should split the state (we did enable SymSymExpr for this
to work), rather than produce always-false.<br>
</blockquote>
<div><br>
</div>
<div>How did you achieve this? For example:<br>
<br>
int a;<br>
void foo(int *x, int *y) {<br>
</div>
<div> int a;<br>
</div>
<div> int *b = &a;<br>
</div>
<div>
if (x == y) { } // I expect this to split the state.<br>
</div>
<div> if (b == &a) {} // I expect this not to split
the state<br>
</div>
<div>
}<br>
void bar() {<br>
foo(&a, &a);<br>
}<br>
<br>
</div>
<div>Does this work as expected?<br>
</div>
</div>
</div>
</div>
</blockquote></span>
Yeah, i guess it works pretty much as expected. In the
out-of-context analysis, we have two branches for foo(), depending
on range constraints for symbol 'reg_$0<x> == reg_$0<y>'
- in one branch it's [0, 0], in the other branch it's [1, something
like BOOL_MAX]. When calling foo(&a, &a) from bar(),
reg_$0<x> gets renamed to &a (as integer), reg_$0<y>
gets renamed to &a (as integer) (i don't remember if we still
keep the SymbolRegionAddress thing around, because i wanted to
replace it with the correct nonloc::LocAsInteger eventually, as it
seems more correct; it is more difficult to work with, but imho it
is "the" correct actualization), and finally the whole symbol gets
renamed to '&a (as integer) != &a (as integer)' and
collapses to 0 during evalBinOp, but because range [0, 0] of 0 does
not intersect with [1, something like BOOL_MAX], this branch is
discarded as unreachable. So when applying summary in-context we
have only one branch.<span class=""><br></span></div></blockquote><div><br></div><div>That is great!<br><br></div><div>What I wanted to emphasize here, do we still get only one branch for `<span class="">if (b == &a) {}`? Because that condition can be decided regardless of the context. </span></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 text="#000000" bgcolor="#FFFFFF"><span class="">
<blockquote type="cite">
<div dir="ltr">
<div class="gmail_extra">
<div class="gmail_quote">
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
And then actualization can take care of the rest. Say the
checker, upon encountering, say, "fclose(f1); fclose(f2);"
and then later, when applying the summary, finding out
that f1 and f2 is the same descriptor, would detect the
problem upon actualization of the respective symbols to
the same symbol. Or the store would correctly merge
bindings to different sub-regions of aliased regions even
if they were not aliased outside the context.<br>
</blockquote>
<div><br>
</div>
<div>I think I would prefer a way to do this automatically
instead of making checker writers consider aliasing
explicitly. But I may misunderstood your point.<br>
</div>
</div>
</div>
</div>
</blockquote></span>
Yeah, me too. But as long as the GDM is opaque for the analyzer
core, we cannot avoid relying on checkers for managing their info in
the state. Hence the recent buzzword in our discussions - the "smart
data map", which i'm dreaming of, but could not work on it yet.<br>
</div>
</blockquote></div><br></div></div>