[Soot-list] my StrongLocalMustAliasAnalysis gives unexpected results

[Richard Xiao]

Hi,

Yes, your example is the limitation of the flow sensitive analysis, which
is the major improvement a path sensitive analyzer tries to make.
You can find your example in section 3.1 of Aiken's paper:

http://theory.stanford.edu/~aiken/publications/papers/fse06.pdf

I personally think, if you want to use value numbering, only value
numbering over the paths can solve your problem, such as the method
described by Bodik.

http://www.eecs.berkeley.edu/~bodik/research/popl98.html

Or just try a path sensitive points-to analysis. But none of the solutions
are easy.

Hope it helps.

Regards,
Richard


On Tue, Oct 23, 2012 at 6:51 PM, Zhoulai <zell08v at orange.fr> wrote:

> Hi again,
>
> Eric, could you pls. send me your new StrongLocalMustAliasAnalysis.java so
> I can look at it more closely?
>
> Besides, another imprecision issue may be due to the merge of
> LocalMustAliasAnalysis. But I am not that sure whether I misunderstand your
> merge operation.
>
> Here is a code fragment  reproduces the imprecise results:
>
> if (...) { x = a; y = a ; }
> else  { x= b; y = b ; }
>
> The current  LocalMustAliasAnalysis associates different numbering for x
> and y and the end of the program, that is, the must-alias relation between
> x and y is not captured.
>
> Probably, you only wanted to capture must-alias over time, and must-alias
> between variables at the same control point is ignored ?
>
> Zell.
>
>
> On Mon, Oct 22, 2012 at 4:34 PM, Eric Bodden <eric.bodden at ec-spride.de>wrote:
>
>> Hi again.
>>
>> My apologies, apparently I misinterpreted what you wrote. I have
>> indeed found a small probleHi m with the implementation, which I have now
>>
>> fixed: While I was invalidating instance keys, I only checked the
>> after-flow, not the before-flow. I have now added checks for the
>> before-flow, too, which seems to solve the problems you reported.
>>
>> At the same time, I solved some imprecision caused by cases such as
>> the following:
>>
>> A b = new A(), c;
>> while (i>0){
>>   A a = new A();
>>   A x = a;
>>   c = b;
>> }
>>
>> In this case, the key for a,x should be invalidated, but not the key
>> for b,c. The refined implementation gives you this semantics. Zell can
>> you please double-check that it's doing the right thing?
>>
>> Eric
>>
>> On 22 October 2012 10:41, Zhoulai <zell08v at orange.fr> wrote:
>> > Hi, Eric
>> >
>> > Thanks for your clarifying this.
>> >
>> > However, I was not using value number (i.e.
>> > getFlowBefore.get(stmt).get(local)) as the indicator to decide whether
>> two
>> > locals strongly  must-alias or not.  We were using
>> instanceKeyString(stmt,
>> > local) to decide strong must alias.
>> >
>> >  If I understand correctly, StrongMustAliasAnalysis overrides the
>> > instanceKeyString of its super class LocalMustAliasAnalysis in such a
>> way
>> > that the invalid instanceKeys are bound to UNKNOWN. Below is the source
>> code
>> > from StrongMustAliasAnalysis
>> >
>> >     @Override
>> >     public String instanceKeyString(Local l, Stmt s) {
>> >         Object ln = getFlowBefore(s).get(l);
>> >         if(invalidInstanceKeys.contains(ln)) {
>> >             return UNKNOWN_LABEL;
>> >         }
>> >         return super.instanceKeyString(l, s);
>> >     }
>> >
>> > So I believe it is correct to conclude that StrongMustAliasAnalysis sole
>> > relies on instanceKeyString.  As you said, the value numbers are used to
>> > decide the weak must-alias, and not sufficient to decide the strong
>> > must-alias.
>> >
>> > Zell.
>> >
>> >> But Zell, I think you are still mistaken. As I explained earlier, it
>> >> is *not* enough to look at the value numbers! Yes, the variables may
>> >> be assigned the same numbers but still StrongMustAliasAnalysis will
>> >> probably return FALSE, as this value number would have been
>> >> invalidated. For StrongMustAliasAnalysis you must not solely rely on
>> >> the value numbers!
>> >>
>> >> 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
>>
>
>
> _______________________________________________
> Soot-list mailing list
> Soot-list at sable.mcgill.ca
> http://mailman.cs.mcgill.ca/mailman/listinfo/soot-list
>
>


-- 
Richard Xiao Xiao
PhD Student @ CSE @ Hong Kong University of Science and Technology
www.cse.ust.hk/~richardxx
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.cs.mcgill.ca/pipermail/soot-list/attachments/20121023/bf6c565d/attachment-0001.html