[cfe-dev] Memory regions as conservative alias analysis

[Guillem Marpons]

Hi,

I'm evaluating the possibility of using the memory regions computed by
the static analyzer as a *conservative* alias analysis (i.e.: I want
to be able to guarantee that two given pointers are never going to
alias, in any path). I'm aware that the analyzer is mainly oriented
towards bug finding, and that false negatives are acceptable in that
particular application. On the contrary, I think that a conservative
approach is necessary in many cases for the application I'm thinking
of (coding rule validation). If the analysis is precise enough, I
think it can be also useful in this other way. I'd like to know if you
think this is not feasible for some reason.

In order to define my checks, I need to know what guarantees the
analyzer can give me, e.g:
- If two pointers point to regions contained in different memory
spaces, they are not aliased. (Memory spaces are always disjoint,
right?)
- If two pointers point to different stack frames, they are not aliased.
- etc.
Are those guesses correct? What other certainties can I have?

I've been trying to write some toy checkers, looking at the examples
that come with clang, but the number of concepts/classes involved is
quite intimidating. I'd really appreciate some document explaining the
general design of the analyzer and the different pieces that can be
replaced (StoreManager, ConstraintManager, etc.). I've already read
the paper "A Memory Model for Static Analysis of C Programs", by Xu,
Kremenek, and Zhang, and
http://clang.llvm.org/docs/AnalyzerRegions.html, but I find difficult
to jump from those documents to the API documentation.

As a side note: I wrote some example checkers to determine the memory
space of some variables, only to receive an "<Unknown Region>" for
almost every region in my code. The cause was not that the analyzer
was incapable of assigning meaningful memory spaces, but that most of
'MemSpaceRegion' subclasses don't re-implement the 'dumpToSream'
method. It'd be a trivial patch to implement those methods but that
would greatly improve debugging (I can contribute the patch, if you
want). On the other hand, I never receive regions in 'HeapSpaceRegion'
for neither 'new' nor 'malloc'. Is the implementation for that
missing?

--
Guillem