[Soot-list] my StrongLocalMustAliasAnalysis gives unexpected results
Zhoulai
zell08v at orange.fr
Sat Oct 20 13:10:19 EDT 2012
Hi, Eric,
The following test-case is much more realistic
****************
static void test5(int i){
while (i>0){
A x = new A();
A y = x;
String s = "hello";
}
}
**************
Using the original strong must-alias analysis, the results before the line
"string s = "hello"" show that 'x', 'y' are both bound to 1, which should
be unsound. (see the highlighted line of the new attached screenshot ).
What do you think?
Zell.
On Sat, Oct 20, 2012 at 6:58 PM, Zhoulai <zell08v at orange.fr> wrote:
> Hi, Eric,
>
> My apologies for any misunderstandings!
>
> The attached scrrenshot shows the results obtained by the original Strong
> must-alias analyzer *before each statement (not only the end of the
> program)*.
>
> Let us check the results from the highlighted row of the screenshot. $r6
> and r2
> point to more than one run-time objects at this line, and are bound to 2
> here using the original must-alias analyzer. But they are expected to be
> bound to UNKNOWN, aren't they?
>
> The example with 'while(true)' is indeed badly chosen. I am not sure
> whether it can be ignored because it may happen when an optimization is
> switched on, like
>
> x = 10; while (x>0) {...}
>
> I'll see whether such situation can be produced by such less strange
> cases. Sorry for taking you so much time for this....
>
> Sincerely,
> Zell.
>
>
> For information, I used the following code fragment from a BodyTransformer
> for this output.
>
> ----------------
> ...
> LocalMustAliasAnalysis lmaa = new StrongLocalMustAliasAnalysis(ug);
> ....
> for (Unit u: ug.getBody().getUnits()){
> Collection<String> in=new ArrayList<String>();
> for (Local l: b.getLocals()){
> String s=l+"->"+lmaa.instanceKeyString(l, (Stmt) u);
> in.add(s);
> }
> System.out.printf("%s %s\n", in, u);
> }
> ...
> ---------------------------------
>
>
>
> On Sat, Oct 20, 2012 at 2:34 PM, Eric Bodden <eric.bodden at ec-spride.de>wrote:
>
>> Ok, I had another look. It now seems to me that even for the
>> while(true) example I am getting correct results. I wonder *where* you
>> are querying the analysis. I initially queried the analysis at the
>> last statement of the body (and maybe so did you). But that statement
>> is unreachable and therefore the analysis yields an undefined result
>> in this case. Maybe is that the source of your misunderstanding?
>>
>> Eric
>>
>>
>> On 20 October 2012 14:21, Eric Bodden <eric.bodden at ec-spride.de> wrote:
>> > Hi Zell.
>> >
>> > I am afraid I can't quite follow. Using your example, I can indeed
>> > reproduce the problem but I can *only* reproduce it for a while(true)
>> > loop without a break. Such code does not really exist in reality, I
>> > guess, and hence if a fix is actually required.
>> >
>> > In cases of a while(true) loop it seems that the super class LocalMAA
>> > is actually already computing something incorrect. Your fix is hence
>> > not optimal in the sense that it's LocalMAA that should be fixed, not
>> > StrongLocalMAA.
>> >
>> > Eric
>> >
>> > On 19 October 2012 07:43, Zhoulai <zell08v at orange.fr> wrote:
>> >> Hello, Eric
>> >>
>> >> I think I have found the reason of the problem. The problem should
>> come from
>> >> the "Objective Representative" paper. In p7, subsection 5.1.3, I quote
>> two
>> >> phrases here, itemed as [specification] and [implementation]
>> respectively:
>> >>
>> >> -- [Specification] "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."
>> >> -- [Implementation] "We can extend our weak must-alias analysis ot a
>> strong
>> >> must-alias analysis as follows: We first find a SCCs in a method's
>> CFG. If
>> >> variable $v$ gets value number $i$ at an assignment statement within
>> some
>> >> SCC, we invalidate $i$ and give $v$ the value number $\top$ a a
>> conservative
>> >> approximation."
>> >>
>> >> In my humble opinion, the [implementation] only partially implements
>> the
>> >> [specification]. At least the following three statement should be
>> considered
>> >> \emph{apart}.
>> >> -- x = new A();
>> >> -- x = y[i]
>> >> -- x = foo();
>> >>
>> >> For example,
>> >> while (true){
>> >> A x= new A();
>> >> A y = x;
>> >> }
>> >>
>> >> Suppose that the numbering for 'new A() 'is K. This number should be
>> >> invalidated following the [specification] above, because 'K' is bound
>> to
>> >> more than one run-time memory. However, 'K' is not invalidated
>> following
>> >> the [Implementation] above: at the end of the first round, both
>> variables
>> >> 'x' and 'y' get the numbering 'K', but the merge will assign a new
>> value to
>> >> variables 'x' and 'y', so 'K' is escaped from being captured because
>> of the
>> >> merge.
>> >>
>> >> This is the intuition. My debugging follows this heuristic. The
>> >> formalization of the above reasoning should be very interesting
>> because it
>> >> is quite similar to the formal reasoning of the SSA-based middle-end.
>> >> [Demange et al. ESOP12].
>> >> Since I am still suffering with my Ph.D, I 'll just content myself
>> with an
>> >> informal understanding above. Below, a revised
>> >> StrongLocalMustAliasAnalysis.class is attached. I used this following
>> >> testcase.
>> >> ******************
>> >> static void test4(){
>> >> A x, y, z, w;
>> >> A tmp = new A();
>> >> while (true){
>> >> x=new A();
>> >> y =tmp;
>> >> z = y;
>> >> w = x;
>> >> }
>> >> }
>> >> *************
>> >> Inside the loop, 'x' and 'w' should be bound to UNKNOWN.
>> >>
>> >> I hope I was clear.
>> >> Zell.
>> >>
>> >> On Fri, Oct 12, 2012 at 4:21 PM, Zhoulai <zell08v at orange.fr> wrote:
>> >>>
>> >>> Hello, Eric
>> >>>
>> >>> Sure! It is my great pleasure to be useful for SOOT community. I
>> will
>> >>> fix it next week.
>> >>>
>> >>>
>> >>> Zell.
>> >>>
>> >>>
>> >>>
>> >>>
>> >>> On Fri, Oct 12, 2012 at 11:40 AM, Eric Bodden <
>> eric.bodden at ec-spride.de>
>> >>> wrote:
>> >>>>
>> >>>> Hi Zell.
>> >>>>
>> >>>> Hmm, this indeed looks like an implementation bug. Maybe could you
>> use
>> >>>> a debugger to step through the computation and see what goes wrong? I
>> >>>> would be happy to accept a patch for this but I am afraid I have no
>> >>>> time to debug this on my own right now.
>> >>>>
>> >>>> Eric
>> >>>>
>> >>>> On 11 October 2012 20:51, Zhoulai <zell08v at orange.fr> wrote:
>> >>>> > Hello,
>> >>>> >
>> >>>> > Sorry for bothering again for this question. But I still find the
>> >>>> > results
>> >>>> > are strange:
>> >>>> >
>> >>>> >
>> >>>> > Input :
>> >>>> > static void test0(int i) {
>> >>>> > while (i>0){
>> >>>> > A x = new A();
>> >>>> > A y = x;
>> >>>> > (*) int z = 0;
>> >>>> > }
>> >>>> > }
>> >>>> >
>> >>>> >
>> >>>> > Using StrongLocalMustAliasAnalysis, I find StrongLocalMustAlias
>> infers
>> >>>> > -- Before (*), (x,x), (y,y), (x,y) must-alias
>> >>>> >
>> >>>> > I guess this is unsafe w.r.t the specification of
>> >>>> > StrongLocalMustAliasAnalysis. For example, the values of 'y' and
>> 'x'
>> >>>> > are
>> >>>> > different for different rounds of loop. I wonder whether you
>> encounter
>> >>>> > this
>> >>>> > kind of program for your typestate problems.
>> >>>> >
>> >>>> >
>> >>>> > Interestingly, if the last statement, i.e, z = 0, is removed, then
>> the
>> >>>> > results become correct. For the program
>> >>>> >
>> >>>> > static void test0(int i) {
>> >>>> > while (i>0){
>> >>>> > A x = new A();
>> >>>> > A y = x;
>> >>>> > }
>> >>>> > }
>> >>>> >
>> >>>> > it can be inferred that none of (x,x), (y,y), (x,y) strongly
>> must-alias
>> >>>> > at
>> >>>> > the end of the loop. This, after inspecting the transformed Jimple
>> >>>> > code, is
>> >>>> > a sort of coincidence because the end of the loop in the source
>> program
>> >>>> > corresponds to the merge point of the transformed Jimple code, and
>> this
>> >>>> > join
>> >>>> > makes 'x', 'y' take UNKNOWN.
>> >>>> >
>> >>>> > What do you think? Thanks.
>> >>>> > Zell.
>> >>>> >
>> >>>> >
>> >>>> >
>> >>>> >
>> >>>> >
>> >>>> > On Thu, Oct 11, 2012 at 11:49 AM, Eric Bodden
>> >>>> > <eric.bodden at ec-spride.de>
>> >>>> > wrote:
>> >>>> >>
>> >>>> >> Hello.
>> >>>> >>
>> >>>> >>
>> >>>> >> > If I understand well, the following contract holds for any
>> object
>> >>>> >> > 'slmaa' of
>> >>>> >> > the class StrongLocalMustAliasAnalysis:
>> >>>> >> >
>> >>>> >> > slmaa.instanceKey(loc, stmt) != UNKNOWN
>> >>>> >> > ===> 'loc' strongly must-alias with itself
>> >>>> >> > ( or equivalently, at most one run-time object can be bound to
>> >>>> >> > 'loc' )
>> >>>> >>
>> >>>> >> I think that may be the cause of the problem. Your assumption
>> does not
>> >>>> >> actually hold. There's an additional condition. See here in the
>> >>>> >> implementation:
>> >>>> >>
>> >>>> >> public boolean mustAlias(Local l1, Stmt s1, Local l2, Stmt
>> s2) {
>> >>>> >> Object l1n = getFlowBefore(s1).get(l1);
>> >>>> >> Object l2n = getFlowBefore(s2).get(l2);
>> >>>> >>
>> >>>> >> if (l1n == UNKNOWN || l2n == UNKNOWN ||
>> >>>> >> invalidInstanceKeys.contains(l1n) ||
>> >>>> >> invalidInstanceKeys.contains(l2n))
>> >>>> >> return false;
>> >>>> >>
>> >>>> >> return l1n == l2n;
>> >>>> >> }
>> >>>> >>
>> >>>> >> In your example, $r0 quite likely got invalidated.
>> >>>> >>
>> >>>> >> 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
>> >>>
>> >>>
>> >>
>> >
>> >
>> >
>> > --
>> > 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
>>
>>
>>
>> --
>> 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
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.cs.mcgill.ca/pipermail/soot-list/attachments/20121020/4ef89698/attachment-0001.html
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Screen shot 2012-10-20 at 19.06.52.png
Type: image/png
Size: 54357 bytes
Desc: not available
Url : http://mailman.cs.mcgill.ca/pipermail/soot-list/attachments/20121020/4ef89698/attachment-0001.png
More information about the Soot-list
mailing list