[cfe-dev] [analyzer] limits in reasoning about memory regions

[hao/NoQ via cfe-dev]

Hello,

> the analyzer cannot fully reason about a region in the following cases, as those are not represented as TypedRegions

Technically, there's a difference between reasoning about type and
reasoning about size of the region. Different mechanisms are
responsible for that.

It is true that reasoning about types is implemented by the means of
TypedValueRegion and its derived classes. Symbolic region, which
represents a region behind a symbolic pointer, is untyped, because
pointer can be casted arbitrarily - for example, you may allocate an
array of four chars with operator new[], and then treat it as a 32-bit
int (consider a custom allocator). Whenever access occurs inside a
SymbolicRegion, however, you are not seeing access to the
SymbolicRegion itself, but an ElementRegion of the necessary type
inside this SymbolicRegion, which is the way the analyzer represents
pointer casts.

Reasoning about region size, in bytes, is implemented via region
extent, obtained with SubRegion::getExtent(). This may be either a
symbol or a concrete value, depending on whether the analyzer can
reason about the extent of the region. To obtain a direct answer for
your question, you can see how the getExtent() method is implemented
for various region classes. For VarRegion, for example, the extent
would be the size of the variable. For SymbolicRegion, it would be a
symbol of type SymbolExtent, because SymbolicRegion is only based on a
pointer at start of it, and no information about the end of the region
is available.

There's good news, however: there may be various things that affect
range constraints for the extent symbols. One of such things is
MallocChecker. If you enable this checker, it would affect the program
state by applying constraints over the SymbolExtent for symbolic
regions explicitly allocated on the heap to mark it as known to be
equal to the actual amount of allocated memory. This allows you to
reason about extents of regions allocated on heap when such
information can actually be obtained during analysis.