[cfe-dev] Extra join points in CFG?

[Ted Kremenek]

Brief update: I have looked at this, and it turns out to be a bit more complicated then I anticipated.  I discovered through investigation that the way we currently model '&&' and '||' in the CFG does not properly model C++ destructors at all, and fixing that may require changing some fairly pervasive invariants.  I think we need to do this, but it will take a bit longer than I originally anticipated...

On Dec 9, 2011, at 11:15 AM, Delesley Hutchins wrote:

> It's good to hear that a fix is planned.  BTW, I'm not in a huge hurry
> here; I just wanted to know if it was intended behavior.  :-)
> 
>  -DeLesley
> 
> On Fri, Dec 9, 2011 at 10:49 AM, Ted Kremenek <kremenek at apple.com> wrote:
>> Hi Delesley,
>> 
>> This is a known issue.  The CFG could (and should) certainly be refined here.  It's been on my queue for a while.  I'll try and take a look at it today, as the change will percolate to a bunch of analyses and the static analyzer.
>> 
>> Ted
>> 
>> On Dec 9, 2011, at 10:33 AM, Delesley Hutchins wrote:
>> 
>>> I am having an issue with joint points in the clang CFG.  I would
>>> expect the CFG for
>>> 
>>>  if (f() && g()) foo();
>>> 
>>> To look something like the following (I've simplified the syntax somewhat):
>>> 
>>>  [B1]
>>>  1: f();
>>>  T: if [B1.1] then B2 else B4
>>> 
>>>  [B2]
>>>  1: g();
>>>  T: if [B2.1] then B3 else B4
>>> 
>>>  [B3]
>>>  1: foo();
>>>  T: goto B4
>>> 
>>>  [B4]
>>> 
>>> That is to say, if the evaluation of f() yields false, it should
>>> short-circuit immediately to the point after the "if" statement.
>>> Instead, I get a CFG which looks like:
>>> 
>>>  [B1]
>>>  1: f();
>>>  T: if [B1.1] then B2 else B3
>>> 
>>>  [B2]
>>>  1: g();
>>>  T: goto B3
>>> 
>>>  [B3]
>>>  1: [B1.1] && [B2.1]
>>>  T: if [B3.1] then B4 else B5
>>> 
>>>  [B4]
>>>  1: foo();
>>>  goto B5
>>> 
>>>  [B5]
>>> 
>>> In this case, there is an extra join point in the CFG.  The case where
>>> f() yields false, and the case where f() yields true, both join at
>>> [B3], which comes before the body of the branch.  This is a problem
>>> for the analysis that I am doing, because my algorithm merges state at
>>> each join point, so having extra join points yields a false positive.
>>> In other words, I need to know when looking at foo() that f() yielded
>>> true, and I can't see that in the current CFG.  Moreover, I am not
>>> convinced the extra join point is even valid; it seems odd that [B3.1]
>>> refers to [B2.1], even though [B2] does not dominate [B3].
>>> 
>>> Would it be possible to update the CFG code so that it outputs the
>>> first case, rather than the second?
>>> 
>>>  -DeLesley
>>> 
>>> --
>>> DeLesley Hutchins | Software Engineer | delesley at google.com | 505-206-0315
>> 
> 
> 
> 
> -- 
> DeLesley Hutchins | Software Engineer | delesley at google.com | 505-206-0315