[Soot-list] my StrongLocalMustAliasAnalysis gives unexpected results

Eric Bodden eric.bodden at ec-spride.de
Sat Oct 20 08:34:43 EDT 2012 

Ok, I had another look. It now seems to me that even for the
while(true) example I am getting correct results. I wonder *where* you
are querying the analysis. I initially queried the analysis at the
last statement of the body (and maybe so did you). But that statement
is unreachable and therefore the analysis yields an undefined result
in this case. Maybe is that the source of your misunderstanding?

Eric


On 20 October 2012 14:21, Eric Bodden <eric.bodden at ec-spride.de> wrote:
> Hi Zell.
>
> I am afraid I can't quite follow. Using your example, I can indeed
> reproduce the problem but I can *only* reproduce it for a while(true)
> loop without a break. Such code does not really exist in reality, I
> guess, and hence if a fix is actually required.
>
> In cases of a while(true) loop it seems that the super class LocalMAA
> is actually already computing something incorrect. Your fix is hence
> not optimal in the sense that it's LocalMAA that should be fixed, not
> StrongLocalMAA.
>
> Eric
>
> On 19 October 2012 07:43, 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
>>>
>>>
>>
>
>
>
> --
> 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



-- 
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

More information about the Soot-list mailing list