[Soot-list] my StrongLocalMustAliasAnalysis gives unexpected results

[Eric Bodden]

Thanks a lot Zell.

I am not in the office today but I will check out your test case as soon as
I get the chance.

Eric
On Oct 19, 2012 7:43 AM, "Zhoulai" <zell08v at orange.fr> wrote:

> 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/172b00b5/attachment.html