[Soot-list] my StrongLocalMustAliasAnalysis gives unexpected results

[Patrick Lam]

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>
>         <mailto:Soot-list at sable.__mcgill.ca
>         <mailto:Soot-list at sable.mcgill.ca>>
>         http://mailman.cs.mcgill.ca/__mailman/listinfo/soot-list
>         <http://mailman.cs.mcgill.ca/mailman/listinfo/soot-list>
>
>
>
>