[Soot-list] my StrongLocalMustAliasAnalysis gives unexpected results

[Zhoulai]

Hello, Eric

I think I have found the reason of the problem. The problem should come
from the "Objective Representative" paper. In p7, subsection 5.1.3, I quote
two phrases here, itemed as [specification] and [implementation]
respectively:

 -- [Specification] "A strong representative only must-alias itself at the
same program location if it is guaranteed that this representative
represents a single run-time object."
 -- [Implementation] "We can extend our weak must-alias analysis ot a
strong must-alias analysis as follows: We first find a SCCs in a method's
CFG. If variable $v$ gets value number $i$ at an assignment statement
within some SCC, we invalidate $i$ and give $v$ the value number $\top$ a a
conservative approximation."

* In my humble opinion, the [implementation] only partially implements the
[specification].* At least the following three statement should be
considered \emph{apart}.
-- x = new A();
-- x = y[i]
-- x = foo();

For example,
while (true){
  A x= new A();
  A y = x;
}

Suppose that the numbering for 'new A() 'is K. This number should be
invalidated following the [specification] above, because 'K' is bound to
more than one run-time memory. However,   'K' is not invalidated following
the [Implementation] above: at the end of the first round, both variables
'x' and 'y' get the numbering 'K', but the merge will assign a new value to
variables 'x' and 'y', *so 'K' is escaped from being captured because of
the merge.
 *
This is the intuition. My debugging follows this heuristic. The
formalization of the above reasoning should be  very interesting because it
is quite similar to the formal reasoning of the SSA-based middle-end.
[Demange et al. ESOP12].
Since I am still suffering with my Ph.D, I 'll just content myself with an
informal understanding above. Below, a revised
StrongLocalMustAliasAnalysis.class is attached.  I used this following
testcase.
******************
    static void test4(){
        A x, y, z, w;
        A tmp = new A();
        while (true){
            x=new A();
            y =tmp;
            z = y;
            w  = x;
        }
    }
*************
Inside the loop, 'x' and 'w' should be bound to UNKNOWN.

I hope I was clear.
Zell.

On Fri, Oct 12, 2012 at 4:21 PM, Zhoulai <zell08v at orange.fr> wrote:

> 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/20121019/cc9b8a92/attachment.html 
-------------- next part --------------
A non-text attachment was scrubbed...
Name: StrongLocalMustAliasAnalysis.java
Type: application/octet-stream
Size: 4689 bytes
Desc: not available
Url : http://mailman.cs.mcgill.ca/pipermail/soot-list/attachments/20121019/cc9b8a92/attachment.obj