[Soot-list] LocalMustAliasAnalysis inaccuracy

[Eric Bodden]

This should be fixed now in SVN revision 3341.

I am not sure what we were thinking earlier when implementing this but
now at merge points I generate for every variable "x" a value that is
unique w.r.t. both values that "x" can have.

Merging "x=1 y=1 z=2" and "x=3 y=3 z=4" leads to something like "x=5
y=5 z=6".  (1,3) is different from (3,1), so if you merge "x=1 y=3
z=2" and "x=3 y=1 z=4" then the merge should result in something like
"x=5 y=6 z=7", i.e. x and y are *not* assigned the same number. I
think this should be correct now. I hope you agree.

Eric

2009/9/26 Eric Bodden <bodden at st.informatik.tu-darmstadt.de>:
> Thanks Arie, for reporting this.
>
> I think you are right and indeed we overlooked something there. I will
> look into this and report back to the list within the next days.
>
> Eric
>
> 2009/9/25 Arie Zilberstein <arie.zilberstein at gmail.com>:
>> Hi,
>>
>>
>>
>> I believe there is an inaccuracy in LocalMustAliasAnalysis with respect to
>> dataflow merges.
>>
>> The problem is that at a merge point, all merged values receive the same
>> (new) value number. However, this does not account for different variables
>> that are merged; only for different merge locations.
>>
>>
>>
>> Here's an example. Consider the following method:
>>
>>
>>
>> private static void merge1() {
>>
>>            Integer x, y;
>>
>>            if (Math.random() > 0.5) {
>>
>>                 x = new Integer(1);
>>
>>                 y = new Integer(2);
>>
>>            } else {
>>
>>                 x = new Integer(3);
>>
>>                 y = new Integer(4);
>>
>>            }
>>
>>            System.out.println(x);  /**/
>>
>>            System.out.println(y);
>>
>>      }
>>
>>
>>
>> The location that I marked with a comment is a merge point for two separate
>> variables: x and y. However, the merge logic for LocalMustAliasAnalysis
>> gives both x and y the same value number.
>>
>>
>>
>> Here's how the maps look at the beginning and end of the merge() method:
>>
>>
>>
>> inMap1: {$r0=4, $r1=UNKNOWN, x=3, y=4}
>>
>> inMap2: {$r0=2, $r1=UNKNOWN, x=1, y=2}
>>
>> outMap: {$r0=5, $r1=UNKNOWN, x=5, y=5}
>>
>>
>>
>> So, the algorithm deduces that x and y must alias at the merge location.
>> Which is the wrong result.
>>
>>
>>
>> Best,
>>
>> Arie
>>
>> _______________________________________________
>> Soot-list mailing list
>> Soot-list at sable.mcgill.ca
>> http://mailman.cs.mcgill.ca/mailman/listinfo/soot-list
>>
>>
>
>
>
> --
> Eric Bodden
> Software Technology Group, Technische Universität Darmstadt, Germany
> Tel: +49 6151 16-5478    Fax: +49 6151 16-5410
> Mailing Address: S2|02 A209, Hochschulstraße 10, 64289 Darmstadt
>



-- 
Eric Bodden
Software Technology Group, Technische Universität Darmstadt, Germany
Tel: +49 6151 16-5478    Fax: +49 6151 16-5410
Mailing Address: S2|02 A209, Hochschulstraße 10, 64289 Darmstadt