[Soot-list] my StrongLocalMustAliasAnalysis gives unexpected results

[Eric Bodden]

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