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

[Andrew McGregor]

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?
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20100729/2485a9d8/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: clang-ownership-withtests-r5.patch
Type: application/octet-stream
Size: 33252 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20100729/2485a9d8/attachment.obj>