[Soot-list] CFL Reachability with Jedd

[Manu Sridharan]

Hey Saswat,

Let me just make clear that my formulation of context-sensitive 
points-to analysis will probably not scale to large programs if you're 
trying to compute points-to information for all variables in the 
program; we rely on focusing precision where the client needs it for 
scalability.  It might be a good idea to implement your analysis with 
context-insensitive points-to information (which is easily computed by 
Spark or Paddle already), work out the kinks, and then look more closely 
at where the points-to information is not precise enough.  You may find 
out that for your client,  Paddle already has a sufficiently precise 
scalable analysis you can use.

-Manu

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.
>
> 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