[bddbddb-devel] Thread escape analysis

[Suman <sum...@gm...>]

Hi all,

I am using thread escape analysis from Algorithm 7 in  [1][3]. When I tried
to run it, I found that the relations H_T and vP0_t  are not generated by
joeq anymore( I ran gen-relations with the -cs, -partial and -fly options).
A little digging into joeq code showed that joeq doesn't generate those
relations anymore.

I also found some remains of a datalog syntax experiment in the the BDD[2]
directory of joeq cvs. It looked like it was performing an escape
analysis[4]. Even this doesn't seem to work because,  While all relations
existed, it looks like the definition of vP0 has changed from
vP0 ( vc:C, v:V , h:H  )
to
vP0 ( v:V , h:H ).

Here are the questions I have. I would be glad if anyone can answer them.

1) Is there a new version of thread escape escape analysis some where in the
bddbddb examples? Or is there a version that works with current bddbddb?
2) What do the relations mC and mV mean?
3) What flags do I need to use to generate IEcs relation?  ( -cs doesn't
seem to work)
4) I am using java 6 to run bddbddb. This seems to work. Is there any reason
I should be only using 1.5?

Thanks for your time,
-S-


[1]*  Cloning-based context-sensitive pointer alias analysis using binary
decision diagrams<http://portal.acm.org/citation.cfm?id=996841.996859&coll=GUIDE&dl=GUIDE&CFID=3883283&CFTOKEN=17384313>
* <bdd...@li...>
[2] /joeq_core/joeq/Compiler/Analysis/BDD/*escape* files
[3] Thread escape analysis from the paper.
 ### Thread escape analysis from Whaley's thesis.

.basedir "/home/suman/installs/joeq/bankExample/bin/results/"
.include "fielddomains.pa"

# Relations

# From algo 1
vP0        (variable: V, heap: H) input
S     (base : V, field : F, source: V) input
L     (base: V, field : F, dest : V) input
A    (dest : V, source : V) input
vP (variable : V, heap: H)
hP (base: H, field : H, target : H)

# From algo 2
vT (variable : V, type : T) input
hT (heap: H, type : T1) input
aT (supertype : T0, subtype:T1) input
vPfilter (variable : V, heap : H)

# From algo 7
HT (c:C, heap: H) input
vP0T (cv : C, variable: V, ch : C, heap : H) input
vPT (cv : C, variable : V, ch : C, heap : H) output
hPT (cb : C, base : H, field : F, ct : C, target : H) output

# Rules
#

# computing vP and hP
vP(v,h) :- vP0(v,h).
vP(v1,h) :- A(v1,v2),vP(v2,h).
hP(h1,f,h2) :- S(v1,f,v2), vP(v1,h1), vP(v2,h2).
vP(v2,h2) :- L(v1,f,v2), vP(v1,h1), hP(h1,f,h2).

# Computing vPT and hPT
vPfilter(v, h)  :- vT(v,tv), hT(h,th), aT(tv,th).
vPT(c1,v,c2,h)  :- vP0T(c1,v,c2,h).
vPT(c,v,c2,h)    :- vP0(v,h),HT(c,h), equal(c,c2).
vPT(c2,v1,ch,h) :- A(v1,v2), vPT(c2,v2,ch,h), vPfilter(v1,h).
hPT(c1,h1,f,c2,h2) :- S(v1,f,v2),vPT(c,v1,c1,h1),vPT(c,v2,c2,h2).
vPT(c,v2,c2,h2) :- L(v1,f,v2),vPT(c,v1,c2,h1),hPT(c1,h1,f,c2,h2),
vPfilter(v2,h2).

[4] Thread escape analysis from joeq's cvs

### Thread escape analysis from joeq sources

.basedir "/home/suman/installs/joeq/bankExample/bin/results/"
.include "fielddomains.pa"

# Relations

# escape 1
mC (method:M, context:C) input
IE0 (ccaller:C, invoke:I, ccallee:C, target:M) input
mI (method:M, invoke:I, name:N) input
mV (method:M, var:V) input

mVc ( method:M , cmethod:C , var:V , cvar:C )

# escape 2

# This relation doesn't exist
vP0 ( vc:C, v:V , h:H  ) input
#This may print too many tuples
escape ( h:H , ccaller:C, m:M  )  outputtuples

### Rules

# escape 1
mVc(m,c1,v,c2) :- mV(m,v), mC(m,c1), c1 = c2.
mVc(m1,c1,v3,c3) :- IE0(c1,i1,c2,m2), mI(m1,i1,_), mVc(m2,c2,v3,c3). split

# escape 2
escape(h,c0,m) :- mV(m2,v), vP0(cv,v,h), mC(m2,cv), !mVc(m,c0,v,cv).