[Soot-list] CFL Reachability with Jedd

[Saswat Anand]

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.

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
>