[Soot-list] my StrongLocalMustAliasAnalysis gives unexpected results
Zhoulai
zell08v at orange.fr
Sat Oct 20 12:58:13 EDT 2012
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/41b2e83f/attachment-0001.html
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Screen shot 2012-10-20 at 18.28.04.png
Type: image/png
Size: 49820 bytes
Desc: not available
Url : http://mailman.cs.mcgill.ca/pipermail/soot-list/attachments/20121020/41b2e83f/attachment-0001.png
More information about the Soot-list
mailing list