[cfe-dev] Ownership attribute for malloc checking, revised patch

[Ted Kremenek]

Actually, I think we need transitions for 'nullState' as well (per my comment in my other email).

On Jul 29, 2010, at 6:32 PM, Ted Kremenek wrote:

> Looks good!  Do you have commit access, or should I go and apply it?
> 
> On Jul 29, 2010, at 1:08 AM, Andrew McGregor wrote:
> 
>> Ok, here's a version that I think has the state transitions right.
>> 
>> Andrew
>> 
>> On Tue, Jul 27, 2010 at 10:45 PM, Ted Kremenek <kremenek at apple.com> wrote:
>> On Jul 27, 2010, at 3:11 PM, Andrew McGregor wrote:
>> 
>>>  
>>> 
>>> +
>>> +  SymbolRef Sym = val.getLocSymbolInBase();
>>> +  if (Sym) {
>>> +    const RefState *RS = state->get<RegionState>(Sym);
>>> 
>>> I think you want to use 'notNullState' here, since your assumption is that this transition occurs only when the value is non-null.  When 'nullState' is not null, you'll also probably want a transition so that path has consistent checking of the nullity of the symbol.
>>> 
>>> Not sure I understand... the RegionState is used because I'm getting at and assuming forward the semantics of the memory region being assigned away, and not touching the null or otherwise assumptions.  
>> 
>> But the non-nullness is a precondition for the checker state to change, so this should be recorded as part of the "assumptions".
>> 
>>> Should I be using notNullState to assert that the assignee is not null?
>> 
>> Yes basically.
>> 
>> I'll try and explain with an example.  Suppose we were analyzing:
>> 
>>   foo(p);
>>   bar(p);
>> 
>> and 'foo' and 'bar' modified some checker-state (like your checker does) associated with p, but only if p is not null.  Conceptually there are only two possible 'nullity' cases for 'p':
>> 
>> (1)
>> 
>>   foo(p); // we check if 'p' is null, and assume it is null
>>   bar(p); // 'p' is still null
>> 
>> (2)
>> 
>>   foo(p); // we check if 'p' is null, and assume it isn't; go modify checker state
>>   bar(p); // 'p' is not null; go modify checker state
>> 
>> However, with what you have, we basically have 4 possibilities; I'll list the two additional ones:
>> 
>> (3)
>> 
>>   foo(p); // we check if 'p' is null, and assume it is null
>>   bar(p); // we don't record that we checked if 'p' is null, we check again and assume that it isn't null; modify state
>> 
>> (4)
>> 
>>   foo(p); // we check if 'p' is null, and assume it isn't; go modify checker state
>>   bar(p); // we don't record that we checked if 'p' is null, we check again and assume that it is null and do nothing
>> 
>> What you are seeing from (3) and (4) is part of (I believe) the "frame problem" from AI.  By having the following statement use 'state' instead of 'notNullState', you are forgetting the nullity check:
>> 
>>    // We no longer own this pointer.
>>   state = state->set<RegionState>(Sym, RefState::getRelinquished(StoreE));
>> 
>> When you use the 'assume' function, 'state' is not modified.  Instead it returns two new states; one where the assumption is true and the other where it is false.  If your modification to the checker state implies that the pointer was non-null, you should be using the 'notNullState' here instead of 'state' as that is a requirement for the checker state to change.
>> 
>> Similarly, if you add a transition where 'notNullState' is non-null and don't add a transition for 'nullState', then you will prune out paths where 'p' is null.  Essentially this would prune out path (1).
>> 
>> Does this make any more sense?
>> 
>> <clang-ownership-withtests-r5.patch>
> 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20100729/21f52241/attachment.html>