[Soot-list] my StrongLocalMustAliasAnalysis gives unexpected results

[Zhoulai]

Hi， Eric,

Thanks for your quick reply. The results is shown in the screenshot for
this program below (with the loop condition 'i > 0' now)

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

It seems that the analysis makes correct answer for 'x' now. (in the
screenshot, it is 'l' that corresponds to 'l'). However, the analysis
infers that '$r0' always alias to itself now.

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' )*

In conclusion,  I guess that '$r0' should have been bound to 'UNKNOWN'
rather than '1' as in the screenshot.

I may have another question related to this one:

In your 2008's " object-representative " paper, '\bot' and '\top' are used
for uninitialized and unknown values respectively. But in your
implementation, I find that even the local variables of reference type are
set to 'UNKNOWN' initially.

I wonder whether this could make the analysis imprecise: local variable
might be better set to 'bot', only field variable or parameter variables
are supposed to be "UNKNOWN"?

What do you think?

Thank you for your ideas.

Zell.

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

> Hi Zell.
>
> Good question! Normally StrongLocalMustAliasAnalysis should tell you
> that x not must-alias itself. (That's why the analysis is called
> "strong".) To compute the right value, we use the class
> StronglyConnectedComponentsFast to find SCCs. I wonder if that
> implementation gets confused by your infinite loop. What happens if
> you have a loop that actually has a chance of terminating?
>
> Eric
>
> On 11 October 2012 09:46, Zhoulai <zell08v at orange.fr> wrote:
> > Hello,
> >
> > I probably wrongly understand the StrongLocalMustAliasAnalysis, but it
> gives
> > me some unexpected results. Where am I wrong?
> >
> > For this program, I expect that 'x' does not strongly must-alias with
> itself
> > in the scope of the method. This is because of the redefinition of 'x'.
> > (reference: Bodden et al 2008's  "Objects Representative"paper)
> >
> > ************* ******************
> >   static void test3(int i){
> >                 A x;
> >                 while (true){
> >                      x= new A();
> >                }
> >      }
> > *****************
> >
> > However, if my analysis driver program is correct,  my analysis says
>  that
> > 'x' must strongly alias with itself (see my attached screenshot)
> >
> > In the screenshot:
> >     -- on the right column is the Jimple statement
> >     -- on the left is  a mapping from local 'l' to
> > slmaa.instanceKeyString(l,s), where 'l' is the locals in the program, and
> > 's'is the statement, smlaa is declared  as  "  LocalMustAliasAnalysis
> slmaa
> > = new StrongLocalMustAliasAnalysis(unitGraph) " ;
> >
> > Any ideas? Thanks.
> > Zell.
> >
> > _______________________________________________
> > Soot-list mailing list
> > Soot-list at sable.mcgill.ca
> > http://mailman.cs.mcgill.ca/mailman/listinfo/soot-list
> >
>
>
>
> --
> 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/20121011/5e9d8ea0/attachment-0001.html 
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Screen shot 2012-10-11 at 11.05.04.png
Type: image/png
Size: 33888 bytes
Desc: not available
Url : http://mailman.cs.mcgill.ca/pipermail/soot-list/attachments/20121011/5e9d8ea0/attachment-0001.png