[Soot-list] CFL Reachability with Jedd

[Ondrej Lhotak]

On Sat, Jan 21, 2006 at 01:56:12PM -0500, Saswat Anand wrote:
> Hi Ondrej,
> 
> I understand now what you mean by it is not clear how to express 
> context-sensitive field-sensitive points-to analysis in CFL. It has been 
> shown to be undecidable. So inspired by Manu's proposal in his recent 
> draft on context-sensitive analysis I have this rule to keep track of 
> context. My question is, can we evaluate such rules in Jedd efficiently.
> 
> o \in pointsTo(v, c), param(v, w, i)
> -------------------------------------
>       o \in pointsTo(w, c.i)
> 
> c is the callstring context. param(v,w,i) catures arg to param flows at 
> call site i. c.i represents i appended to c.
> 
> One naive way to encode this rule in Jedd will require retrieving the 
> tuples from BDD and change the "context" attribute values. But it seems 
> it  might involve some expensive operation. Is that true? In that case, 
> if you see some other alternatives, I would appreicate your hints very much.

The difficult operation here is the append operation (i.e. appending
i to c to get c.i). You can, of course, do this outside of BDDs, but
that's likely to be prohibitively expensive, especially when you start
getting exponential numbers of c's. Can it be done inside the BDD? That
depends on the details of your representation of context strings.
The crux of the ZCWL algorithm is the "adder circuit" which, given
a BDD with a bunch of elements in it, replaces each element with integer
representation i by an element with integer representation i+k, for some
constant k. The ZCWL algorithm defines a numbering of context strings
such that for each call site a, there exists an integer k, such that
for every call site string b, the integer representation of ba is k more
than the integer representation of b. With this numbering, appending
a call site a to a large number of call site strings can be done in the
BDD by using the adder operation to add k to every element. If you can
find a similar numbering for your problem, you can also do it this way.

The adder operation *is* implemented in Jedd, but it's unsupported and
undocumented, because it breaks the Jedd abstraction (the idea behind
Jedd was to avoid having to think in terms of bit strings and integer
operations, and the adder fundamentally requires that). You can find
its implementation in the method BuddyBackend.add() in Jedd, and
an example of its use in the ZhuContext class in Paddle. 

Ondrej

> 
> Thanks,
> Saswat
> 
> 
> 
> Ondrej Lhotak wrote:
> > Hi Saswat...
> > 
> > I'm not aware of any fundamental reasons that would prevent Jedd from
> > solving CFL reachability problems expressed in terms of relations. But,
> > since I haven't tried to implement such an analysis, there may be issues
> > that come up during implementation that I haven't thought of. If you do
> > decide to try it, I'd be interested in hearing about your experience.
> > 
> > Paddle, as you suggest, intentionally takes another (i.e.
> > non-CFL-reachability) approach. For the specific analyses that I wanted
> > to implement in Paddle, it's not clear how they could be expressed in
> > terms of CFL-reachability, even after the recent work in the area.
> > 
> > Ondrej
> > 
> > On Tue, Jan 17, 2006 at 05:36:35PM -0500, Saswat Anand wrote:
> > 
> >>Hi,
> >>
> >>I have a high-level question about Jedd and Paddle after reading 
> >>Ondrej's thesis. I would be appreciate it very much if somebody could 
> >>clarify my doubt.
> >>
> >>Context-sensitive analyzes can be formulated as Context-free language 
> >>(CFL) reachability problem. And a CFL formulation can be transformed to 
> >>a logic program, ie. in terms of relation and operations over them, and 
> >>which I think can then be solved using Jedd. But as far I understand, in 
> >>paddle context-sensitive points-to analysis is not formulated as CFL 
> >>reachability problem, or its logic program counterpart, which was what I 
> >>expected before starting to read the thesis. So I was wondering if my 
> >>understanding is incorrect, or Jedd  cannot solve CFL problems (which 
> >>may be because it assumes some constraints on the relations), or paddle 
> >>just intentionally takes another approach to context-sensitivity. I am 
> >>curious because I want to solve a CFL reachability problem, and was 
> >>planning to use Jedd to solve it.
> >>
> >>Thanks,
> >>Saswat
> >>
> >>
> >>
> >>
> >>_______________________________________________
> >>Soot-list mailing list
> >>Soot-list at sable.mcgill.ca
> >>http://mailman.cs.mcgill.ca/mailman/listinfo/soot-list
> >>
> > 
> > 
> > ----- End forwarded message -----
> > _______________________________________________
> > Soot-list mailing list
> > Soot-list at sable.mcgill.ca
> > 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
>