<div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote">On 31 March 2016 at 14:30, 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">Hello,<br>
<br>
Yeah, there's one particular known-issue with aliasing, which i mentioned earlier (<a href="http://lists.llvm.org/pipermail/cfe-dev/2015-October/045704.html" rel="noreferrer" target="_blank">http://lists.llvm.org/pipermail/cfe-dev/2015-October/045704.html</a>):<span class=""><br></span></blockquote><div><br></div><div>Oh, I see. I just started to catch up with the conversation and did not reach that point yet.<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"><span class="">
<br>
int a;<br>
void foo(int *x, int *y) {<br>
*x = 0;<br>
*y = 1;<br>
}<br>
void bar() {<br>
foo(&a, &a);<br>
clang_analyzer_eval(a); // expected-warning{{TRUE}}<br>
}<br>
<br></span>
Here we may randomly get TRUE or FALSE, kind of race condition.<br>
<br>
We didn't fix it yet, and it can be fixed by adding timestamps to stores, i.e. which bind was earlier.<br>
<br>
With timestamps, i think the store would be fine.<br></blockquote><div><br></div><div>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><br></div><div>Or is this solved already? What did you do about this in that case?<br></div><div><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>
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><span class=""> int a;<br>
void foo(int *x, int *y) {<br></span></div><div><span class=""> int a;<br></span></div><div><span class=""> int *b = &a;<br></span></div><div><span class="">
if (x == y) { } // I expect this to split the state.<br></span></div><div><span class=""> if (b == &a) {} // I expect this not to split the state<br></span></div><div><span class="">
}<br>
void bar() {<br>
foo(&a, &a);<br>
}<br><br></span></div><div><span class="">Does this work as expected?<br></span></div><div><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">
<br>
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><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<br>
So, apart from the issues that boil down to the example above, i'm not instantly aware of aliasing problems yet.<br>
<br>
On <a href="tel:31.03.2016%2014" value="+13103201614" target="_blank">31.03.2016 14</a>:37, Gábor Horváth wrote:<br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
Hi!<span class=""><br>
<br>
I was thinking about the actualization process that you are describing<br>
here, and I think there might be some issues with it. As far as I<br>
remember, when you analyze a function without context the analyzer<br>
assumes that none of the arguments are aliased. So only those paths will<br>
be available in the ExpoldedGraph that does not imply aliasing. This way<br>
you can both loose coverage or take impossible branches. What do you think?<br>
</span></blockquote>
</blockquote></div><br></div></div>