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

[Andrew McGregor]

Ok, null transitions done (for both FreeMemAux and PreVisitBind).

Thanks for the comments,

Andrew

On Fri, Jul 30, 2010 at 3:33 AM, Ted Kremenek <kremenek at apple.com> wrote:

> 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/20100730/037b900b/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: clang-ownership-withtests-r6.patch
Type: application/octet-stream
Size: 33298 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20100730/037b900b/attachment.obj>