[cfe-dev] Static Analyzer: pointer alias assignment

[Gábor Kozár]

I've been looking through the implementations of existing Clang Static
Analyzer checkers, and I now understand that ProgramState::assume returns a
nullptr for a state if that state is unfeasible because of existing
constraints. Some experimentation also showed that when
ProgramState::isNull says that a value is constrained to be null, then
ProgramState::assume on the value will also return nullptr for the non-null
state, and a valid state for the null case.

And so looking at DereferenceChecker.cpp lines 206-210, a warning should be
issued:

if (nullState) {
    if (!notNullState) {
      reportBug(nullState, S, C);
      return;
    }

I'll try to figure out tomorrow why not (something in reportBug()?) - but
please let me know if I'm missing/misunderstanding something.


2013/7/24 Gábor Kozár <kozargabor at gmail.com>

> Hi Ted,
>
>
> > *I think the problem should be looked at in a different fashion.  You
> should not need to reason about aliases at all.  The analyzer engine
> handles this for you.  It’s all symbolic execution.
>
> *
> Yes, I realize the Static Analyzer will recognize that the line p = q
> means that 'p' and 'q' now has the same value, but it does not copy the
> user state (REGISTER_*_WITH_PROGRAMSTATE data) - which makes total sense,
> since it does not know how that data is structured. Therefore, I need to
> record the fact the aliasing has happened using checkBind. This is where I
> encountered the problem described in my original e-mail.
>
> Reading through the checker dev manual<http://clang-analyzer.llvm.org/checker_dev_manual.html>,
> I found the relevant section:
> *"When x is evaluated, we first construct an SVal that represents the
> lvalue of x, in this case it is an SVal that references the MemRegion for
> x. Afterwards, when we do the lvalue-to-rvalue conversion, we get a new
> SVal, which references the value currently bound to x. That value is
> symbolic; it's whatever x was bound to at the start of the function."
>
> *
> I need the reverse: not the value currently bound to x, but the SVal that
> references the MemRegion for x itself. I searched the documentation, but
> all I could find was ProgramState::getLValue, none of whose overloads give
> me what I need. So how could I achieve this?
>
> Back to the aliasing problem: I think it would be very useful if the
> Static Analyzer exposes functions to retrieve aliasing information. For
> example, I would like to ask whether a given SVal is an alias of another.
> My original thought was that this alias-analysis could be implemented as a
> checker itself, which would dispatch an event when it detects an aliasing,
> but I do not see how it could expose methods to the other checkers (e.g.
> for them to be able to ask "is x an alias of y in this ProgramState?").
> Does this make sense?
>
>
> > *A null check might not always be redundant.  On some paths the null
> check may be redundant and others it won’t be.  Thus there is a dominance
> relationship here that needs to be checked.  Essentially, all paths need to
> show that the pointer is always non-null before the pointer is checked.
>  Otherwise you’ll get false positives.  Doing this correctly is hard,
> because not all paths are guaranteed to be traced.  You’ll need to handle
> that too.
>
> *
> Yes, this is a problem, but I have absolutely no clue as to how it could
> be solved. I would naturally want to keep the number of false-positive at
> minimum, even at the cost of some bugs going undetected.
>
>
> > *In this scheme, the pointer value is the symbolic region.  You’ll
> essentially want to monitor the actual null checks of a symbolic region,
> and see if that region is constrained to always be non-null.
>
> *
> My only vague idea is to use the checkEndAnalysis callback to explore the
> ExplodedGraph, but I don't even know how to get started on it, i.e. what I
> should look for. Any pointers (haha) you could give me would be extremely
> useful.
>
> Thanks for your answer!
>
> Gabor
>
>
> 2013/7/23 Ted Kremenek <kremenek at apple.com>
>
>> On Jul 23, 2013, at 10:33 AM, Gábor Kozár <kozargabor at gmail.com> wrote:
>>
>> I'm building a checker that detects inconsistent pointer usages, for
>> example when a pointer is dereferenced, then along the same path is
>> null-checked (without its value changing in between, obviously).
>>
>>
>> Hi Gabor,
>>
>> I think the problem should be looked at in a different fashion.  You
>> should not need to reason about aliases at all.  The analyzer engine
>> handles this for you.  It’s all symbolic execution.
>>
>> One way to reason about this problem is that a pointer *value* has a
>> notion of trust.
>>
>> If it is trusted, it is safe to dereference.  If it isn’t trusted, it
>> isn’t safe to dereference.  The trust level is a tri-state: { Trusted,
>> NotTrusted, Unknown }.  A pointer value needs to start in one of those
>> states.  It goes from { NotTrusted | Unknown } to { Trusted } by a null
>> pointer check.  The checker then fires if a { Trusted } pointer is checked
>> for null.
>>
>> There are details of course.  First, this formalism isn’t necessary to
>> model explicitly because the analyzer essentially already does this.
>>  “Trust” essentially means “constrained to be not-null”, “not trusted”
>> means “known to be null” and “unknown” means unconstrained.  Second, when
>> does the check fire?  A null check might not always be redundant.  On some
>> paths the null check may be redundant and others it won’t be.  Thus there
>> is a dominance relationship here that needs to be checked.  Essentially,
>> all paths need to show that the pointer is always non-null before the
>> pointer is checked.  Otherwise you’ll get false positives.  Doing this
>> correctly is hard, because not all paths are guaranteed to be traced.
>>  You’ll need to handle that too.
>>
>> In this scheme, the pointer value is the symbolic region.  You’ll
>> essentially want to monitor the actual null checks of a symbolic region,
>> and see if that region is constrained to always be non-null.
>>
>> Ted
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20130724/9d631551/attachment.html>