[Soot-list] <To sum up> my StrongLocalMustAliasAnalysis gives unexpected results

[Zhoulai]

To sum up after this long discussion,

-- The 2008 Object Representative paper gives me the impression that Strong
Must Alias Analysis associate UNKNOWN with variables that can be assigned
more than one values.

Quoted from the 2008 paper on object representative:
"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."

I thought, the StrongAliasAnalysis should associate UNKNOWN with x and y
before line 5.
         > > ****************
         > > 1:     static void test5(int i){
         > > 2:         while (i>0){
         > > 3:             A x = new A();
         > > 4:             A y = x;
         > > 5:             String s = "hello";
         > >          }
         > >      }
         > > **************
because both x and y are bound to more than objects during their lifetime.

-- However, Patrick gave me an extra condition:
    " variable redefinition only gives UNKNOWN if the
    redefinition is not mandatory. ",
and argued that x and y should not be associated with UNKNOWN, because the
redefinition is not mandatory.

The problem is still extremely confusing to me. I don't see how to
formalize and verify this last condition. Anyway, thanks again for the
patience of Patrick and Eric and others!

Zell.




On Sun, Oct 21, 2012 at 2:39 PM, Patrick Lam <plam at sable.mcgill.ca> wrote:

> No. If line 5 executes, line 3 has definitely executed. There is no other
> option.
>
>
> On 10/21/2012 07:39 AM, Zhoulai wrote:
>
>> We were talking about an example where thredefinition of variable 'x' is
>> not mandatory (see below the program) , but your StrongMustAliasAnalysis
>> associates with 'x' an integer , rather than UNKNOWN.
>>
>>  > > ****************
>>  > > 1:     static void test5(int i){
>>  > > 2:         while */(i>0)/*{
>>  > > 3:             A x = new A(); _// The re-assignment is NOT
>> mandatory here._
>>  > > 4:             A y = x;                       //_but 'x' is bound
>> to an integer value. This is not sound!_
>>
>>  > > 5:             String s = "hello";
>>  > >          }
>>  > >      }
>>  > > **************
>>
>> 'x' is /potentially/ re-assigned in the loop
>>
>> ==> 'x' is expected to be bound to "UNKNOWN" by your
>> StrongMustAliasAnalysis   (**)
>>
>> But, at line (5) your analyzer infers that x is bound to some integer
>> value  (*)
>>
>> So the expected (**) and the implemented (*)  contradict.
>>
>> Zell.
>>
>>
>> On Sun, Oct 21, 2012 at 1:04 PM, Patrick Lam <plam at sable.mcgill.ca
>> <mailto:plam at sable.mcgill.ca>> wrote:
>>
>>     As I said, variable redefinition only gives UNKNOWN if the
>>     redefinition is not mandatory.
>>
>>     pat
>>
>>
>>     On 10/21/2012 01:26 AM, Zhoulai wrote:
>>
>>         Thanks Patrick. I see your point. Don't forget that your
>>         StrongMustAliasAnalysis, as described by your 2008's paper, is
>>         supposed
>>         to consider variable redefinition in loops!
>>
>>         For the k-th iteration of the loop, a new object o_k is created
>> and
>>         bound to x (which overwrites its earlier state) , so the "*states
>>         history* "  related to x will be
>>
>>         x->o_0, x -> o_2, x->o_k....
>>         which mean that ***Over time*** x is bound to {o_0,o_1,o_2 ...}. I
>>
>>         believe this is the way your StrongMustAliasAnalysis in your paper
>>         reasons, right?
>>
>>         My apologies for any misunderstandings.
>>         Zell.
>>
>>         On Sun, Oct 21, 2012 at 6:33 AM, Patrick Lam
>>         <plam at sable.mcgill.ca <mailto:plam at sable.mcgill.ca>
>>         <mailto:plam at sable.mcgill.ca <mailto:plam at sable.mcgill.ca>>**>
>> wrote:
>>
>>              On 10/21/2012 12:25 AM, Zhoulai wrote:
>>          > > ****************
>>          > > 1:     static void test5(int i){
>>          > > 2:         while (i>0){
>>          > > 3:             A x = new A();
>>          > > 4:             A y = x;
>>          > > 5:             String s = "hello";
>>          > >          }
>>          > >      }
>>          > > **************
>>
>>          > By your specification in your paper, the strong
>>         representative only
>>          > must-alias itself at the same program location if it is not
>>              guaranteed
>>          > that this representative represents a single run-time object.
>>          >
>>          > Here variable 'x'' is associated with  more than 1 run-time
>>              objects.  It
>>          > is therefore expected to be bound to UNKNOWN.
>>
>>              x only points to one object at a time in this case. The
>>         only way that x
>>              might point to more than one object is if there are two
>>         different
>>              definitions that reach x (perhaps from different iterations
>>         of the
>>              loop), like if you had this program instead:
>>
>>                    A x = null;
>>                    if (...) x = new A();
>>                    A y = x;
>>
>>              Then you should not get UNKNOWN. But in the program you
>>         wrote, there's
>>              only one object that x could possibly contain.
>>
>>              pat
>>
>>              ______________________________**___________________
>>
>>              Soot-list mailing list
>>         Soot-list at sable.mcgill.ca <mailto:Soot-list at sable.**mcgill.ca<Soot-list at sable.mcgill.ca>
>> >
>>         <mailto:Soot-list at sable.__mcgi**ll.ca <http://mcgill.ca>
>>         <mailto:Soot-list at sable.**mcgill.ca <Soot-list at sable.mcgill.ca>>>
>>         http://mailman.cs.mcgill.ca/__**mailman/listinfo/soot-list<http://mailman.cs.mcgill.ca/__mailman/listinfo/soot-list>
>>         <http://mailman.cs.mcgill.ca/**mailman/listinfo/soot-list<http://mailman.cs.mcgill.ca/mailman/listinfo/soot-list>
>> >
>>
>>
>>
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.cs.mcgill.ca/pipermail/soot-list/attachments/20121021/34c6eba9/attachment.html