[cfe-dev] Symbolic Extents

[Jordy Rose]

All right, time to go back to the drawing board with this one. So the
direction we're going is this (pseudocode):

(MallocChecker::MallocMemAux)
SVal Result = ValMgr.getConjuredSymbolVal(...)
SVal Extent = ValMgr.getExtent(Result) // or SVator.getExtent(Result)?
state->AssumeEQ(Extent, SizeArg)


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.

As for the extent symbols themselves, I'm not quite sure what to do.
Variable-length arrays aren't symbolic regions, so there's no "parent
symbol" for a SymbolDerived to attach to, but we do need to bound them
symbolically. So we'd at least need a new kind of symbol that attached
itself to regions, rather than other symbols.

Perhaps a MetadataRegion might be more appropriate? The advantage of a new
region over a new symbol is that it could be used for metadata that changes
as well. (I'm looking ahead to taking a stab at modeling C string length,
at least in simple cases.) Of course, this could wreak havoc with the
mythical FlatRegionStore, which would have no place to put this new
subregion.

As for tying SymExprs closer with SVals, it doesn't really make sense,
since SymExprs have more than one pointers' worth of data and thus don't
fit in SVals. Unless we wanted to make a new folding set manager, it's
probably not worth it to extract them from SymbolManager. (Unless we do end
up with a new base in klee.)

Thoughts on MetadataRegion?