[Soot-list] Reachability in CFGs

[Chris Pickett]

irem wrote:
> Ok, my mistake there. Sure the invoke instruction may raise an
> exception. True, this we are not ruling out. Bad example.

Well, if that's the case and you're actually happy with the current 
handling of INVOKE*, maybe you should see if you can find a different 
example.

Chris

> irem    
> 
> On Sun, 2007-11-04 at 16:51 -0500, Chris Pickett wrote:
>> irem wrote:
>>> First of all, thanks for the suggestions on visualizing the control flow
>>> graphs.
>>>
>>> Actually, the reason I was interested in various predecessors and
>>> successors of nodes in control graphs is that I am interested in
>>> reachability. 
>>>
>>> If we look at the following example:
>>>
>>> m1();
>>>
>>> try {
>>> m2();
>>> }
>>> catch (Exception e){
>>> m3();
>>> }
>>>
>>>
>>> A property such as "method m2 is always called before m3" holds for this
>>> program. But Soot constructs CFGs which concentrate on completed
>>> executions, hence there is an edge from the predecessor of the statement
>>> which calls m2 to the exception handler and it seems as if one can end
>>> up in the handler without calling m2. 
>> As an aside, what do you mean by "call"?  It is certainly possible for 
>> INVOKE* to throw an exception before m2 is actually entered.
>>
>> http://java.sun.com/docs/books/jvms/second_edition/html/Instructions2.doc6.html#invokeinterface
>>
>> I don't think that changes what you are trying to do below, but I 
>> thought I should mention it anyway.
>>
>> Chris
>>
>>> I think this was not the case for certain earlier versions, and I
>>> inherited a code that worked fine with them. But now I have to
>>> manipulate the CFGs given by soot to reflect reachability better.
>>>
>>> Anyway, right now, what I do is to construct the ExceptionalUnitGraph,
>>> and check 
>>> for each node in the graph:
>>>  	for each of its exceptional successors in the graph:
>>> 		whether the successor is a handler unit for one of the 
>>> 		ExceptionalDests of the node
>>> 		if this is so, 
>>> 			I keep the edge between the node and successor 
>>> 		else
>>> 			I delete the edge
>>>
>>>
>>>
>>> I have not tested this enough to see if it is correct. What does
>>> everyone think? 
>>> And would you think of integrating such an alternative graph to soot,
>>> i.e. through some option? I think many people may be interested in it.
>>>
>>> Irem Aktug
>>> Ph.D. Student
>>> Stockholm, Sweden
>>>
>>>
>>> _______________________________________________
>>> Soot-list mailing list
>>> Soot-list at sable.mcgill.ca
>>> http://mailman.cs.mcgill.ca/mailman/listinfo/soot-list
>