[cfe-dev] Memory regions as conservative alias analysis

[Guillem Marpons]

Hi Ted, thank you for your reply.

On 30 May 2012 01:24, Ted Kremenek <kremenek at apple.com> wrote:
>
> [...]
>
>> 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?
>
> The second assumption is correct.  The first one is not.
>
> If the memory space is "UnknownSpaceRegion", it means that we do not know the actual memory space.  For example, suppose you had code that looked like:
>
>  void *p;
>  void *q = foo(p);
>
> If we do not know anything about the implementation of 'foo', then we return a memory region wrapping a conjured symbol.  That memory region has an unknown memory space.  The name pretty much implies the ramifications.  It is entirely possible that 'p' and 'q' are aliases after these two lines of code execute.

Ok, to be more precise, if both regions are in a different memory
space, and these memory spaces are not Unknown, then can I be sure
that the regions do not overlap?

> [...]
>>
>> 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).
>
> That would be great!

I need to update my repo to generate the patch. I'll send it in a few days.

>> On the other hand, I never receive regions in 'HeapSpaceRegion'
>> for neither 'new' nor 'malloc'. Is the implementation for that
>> missing?
>
>
> HeapSpaceRegion was added during prototyping, and was never used.  We should probably remove it, and replace it with something more expressive, such as a symbolic memory space.  That way we can distinguish between different parts of the heap, e.g., memory returned by distinct allocators.  That may help with providing stronger aliasing guarantees.

That would be very helpful!

Regards,

--
Guillem