[Soot-list] my StrongLocalMustAliasAnalysis gives unexpected results

[Zhoulai]

Hello,  Eric

Sure! It is my great pleasure to be useful for SOOT community.   I will fix
it next week.


Zell.



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

> Hi Zell.
>
> Hmm, this indeed looks like an implementation bug. Maybe could you use
> a debugger to step through the computation and see what goes wrong? I
> would be happy to accept a patch for this but I am afraid I have no
> time to debug this on my own right now.
>
> Eric
>
> On 11 October 2012 20:51, Zhoulai <zell08v at orange.fr> wrote:
> > 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
> >
> >
>
>
>
> --
> Eric Bodden, Ph.D., http://sse.ec-spride.de/ http://bodden.de/
> Head of Secure Software Engineering Group at EC SPRIDE
> Tel: +49 6151 16-75422    Fax: +49 6151 16-72051
> Room 3.2.14, Mornewegstr. 30, 64293 Darmstadt
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.cs.mcgill.ca/pipermail/soot-list/attachments/20121012/2c4ecebe/attachment-0001.html