[Soot-list] my StrongLocalMustAliasAnalysis gives unexpected results

[Eric Bodden]

Hi again.

Patrick I think according to the definition we had in the paper Zell
is correct. We have two analyses, a StrongMustAliasAnalysis which
gives you must-alias=false for all values re-defined in loops and a
normal MustAliasAnalysis which gives you true. In the paper we
described the difference with the scope/lifetime: if the scope is the
method's entire execution then it's indeed not guaranteed that the
values must-alias because we may be talking about different loop
interations. StrongMustAliasAnalysis models this.

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

On 21 October 2012 14:39, 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>
>>         <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>
>>
>>
>>
>>
>
> _______________________________________________
> Soot-list mailing list
> Soot-list at sable.mcgill.ca
> http://mailman.cs.mcgill.ca/mailman/listinfo/soot-list



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