[cfe-dev] Symbolic Extents

[Ted Kremenek]

On Jun 28, 2010, at 11:35 PM, Jordy Rose wrote:

> The reason I wasn't doing this before is because the constraint manager
> wouldn't (currently) handle this case:
> 
> void symbolic1(size_t a) {
>  char *buf = (char*) malloc(a);
>  if (a == 1) {
>    buf[1] = 'b'; // expected-warning {{out-of-bound}}
>  } else {
>    buf[1] = 'b'; // no-warning
>  }
>  free(buf);
> }
> 
> Here, the value of the symbolic extent is not known until /after/ it is
> set. Our current constraint manager doesn't allow us to "alias" symbols in
> this way, though of course it should soon. But all right, let's not worry
> about that for now.

Yes, I completely understand how this limitation guided you to the other approach, but this is a fundamental problem that we need to solve anyway.  This is a limitation that I've really to address for a long time, but I also think it wouldn't be that hard to support symbol aliases (at least for the simple cases).  I know it's tempting to not try to think about this problem now (as we've deferred solving it for a long time), but unless we try to take the general approach with handling extents using SVals (including symbol aliasing), we are just going to hit the fundamental limitation of what extents can represent (e.g., simple constants, basic symbols) by the end of the summer.  At that point we'll need to solve this problem anyway.

Symbol aliasing is basically alpha-renaming.  We need to store on the side (within GRState) the set of alpha-renamed symbols, and when we assume that two symbols are aliased we need a callback into the Checkers so that they can decide if their current set of meta-data associated with a symbol is compatible with assuming that two symbols are equal.  The SValuator can be clever to always use an alpha-renamed symbol when building new expressions, thus folding the renaming into newly constructed SVals.