[cfe-dev] [analyzer] Summary IPA thoughts

[Artem Dergachev via cfe-dev]

Hello,

Yeah, there's one particular known-issue with aliasing, which i 
mentioned earlier 
(http://lists.llvm.org/pipermail/cfe-dev/2015-October/045704.html):

    int a;
    void foo(int *x, int *y) {
      *x = 0;
      *y = 1;
    }
    void bar() {
      foo(&a, &a);
      clang_analyzer_eval(a); // expected-warning{{TRUE}}
    }

Here we may randomly get TRUE or FALSE, kind of race condition.

We didn't fix it yet, and it can be fixed by adding timestamps to 
stores, i.e. which bind was earlier.

With timestamps, i think the store would be fine.

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.

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.

So, apart from the issues that boil down to the example above, i'm not 
instantly aware of aliasing problems yet.

On 31.03.2016 14:37, Gábor Horváth wrote:
> Hi!
>
> I was thinking about the actualization process that you are describing
> here, and I think there might be some issues with it. As far as I
> remember, when you analyze a function without context the analyzer
> assumes that none of the arguments are aliased. So only those paths will
> be available in the ExpoldedGraph that does not imply aliasing. This way
> you can both loose coverage or take impossible branches. What do you think?