[cfe-dev] Static Analyzer: pointer alias assignment

[Ted Kremenek]

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/20130723/c08fb738/attachment.html>