[cfe-dev] Static Analyzer: pointer alias assignment

[Gábor Kozár]

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/61195fcc/attachment.html>