[Soot-list] my StrongLocalMustAliasAnalysis gives unexpected results

[Zhoulai]

Hello,

Sorry for bothering again for this question. But I still find the results
are strange:


Input :
    static void  test0(int i) {
        while (i>0){
            A x = new A();
            A y = x;
  (*)      int z = 0;
        }
    }


Using StrongLocalMustAliasAnalysis, I find  StrongLocalMustAlias infers
  -- Before (*), (x,x), (y,y), (x,y) must-alias

 I guess this is unsafe w.r.t the specification of
StrongLocalMustAliasAnalysis. For example, the values of 'y' and 'x' are
different for different rounds of loop.  I wonder whether you encounter
this kind of program for your typestate problems.


Interestingly, if the last statement, i.e, z = 0, is removed, then the
results become correct.  For the program

static void  test0(int i) {
        while (i>0){
            A x = new A();
            A y = x;
        }
    }

it can be inferred that none of (x,x), (y,y), (x,y) strongly must-alias at
the end of the loop. This, after inspecting the transformed  Jimple code,
is a sort of coincidence because the end of the loop in the source program
corresponds to the merge point of the transformed Jimple code, and this
join makes 'x', 'y' take UNKNOWN.

What do you think? Thanks.
Zell.




On Thu, Oct 11, 2012 at 11:49 AM, Eric Bodden <eric.bodden at ec-spride.de>wrote:

> Hello.
>
>
> > If I understand well, the following contract holds for any object
> 'slmaa' of
> > the  class StrongLocalMustAliasAnalysis:
> >
> >           slmaa.instanceKey(loc, stmt) != UNKNOWN
> > ===> 'loc' strongly must-alias with itself
> >  ( or equivalently, at most one run-time object can be bound to 'loc' )
>
> I think that may be the cause of the problem. Your assumption does not
> actually hold. There's an additional condition. See here in the
> implementation:
>
>     public boolean mustAlias(Local l1, Stmt s1, Local l2, Stmt s2) {
>         Object l1n = getFlowBefore(s1).get(l1);
>         Object l2n = getFlowBefore(s2).get(l2);
>
>         if (l1n == UNKNOWN || l2n == UNKNOWN ||
>             invalidInstanceKeys.contains(l1n) ||
> invalidInstanceKeys.contains(l2n))
>             return false;
>
>         return l1n == l2n;
>     }
>
> In your example, $r0 quite likely got invalidated.
>
> Eric
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.cs.mcgill.ca/pipermail/soot-list/attachments/20121011/881fd8ca/attachment.html