[cfe-dev] Symbolic Extents

[Ted Kremenek]

On Jun 29, 2010, at 1:53 PM, Jordy Rose wrote:

> I was trying to think of a way to leverage the existing symbol/region
> liveness analysis -- subregions remain alive with the superregion, and
> region values remain alive with their regions. This shouldn't be a
> constraint on us, though -- a symbolic extent is just a (possibly conjured)
> value that remains live with the region.

Yes, symbols are also pruned from the state when they are no longer live.  This includes symbols derived from regions and symbols derived from other symbols.

> 
> I'll stop trying to plan ahead for C string length -- maybe that's
> solvable with the GDM anyway.
> 
> So, at this point I would picture extents for SymbolicRegions (and
> AllocaRegions, and maybe VLAs) as a cross between derived symbols and
> conjured symbols with tags, except for one possible issue -- they might be
> different on different paths through the CFG. With conjured symbols now we
> have a Count parameter to avoid this. Does this mean we can only
> getExtent() (or getExtentVal()) from a function with access to
> GRStmtNodeBuilder?

No, I think having access to SymbolManager would be enough, which is accessible from ValueManager.

> Also, it might be nice if getExtent() lived on MemRegion, instead of
> ValueManager or SValuator. Maybe?

I think having it in MemRegion would be fine, except you would need to pass a SymbolManager& argument for the case of generating derived symbols on demand.  More complicated extents would involve expressions that were already constructed by the SValuator and then equated (via ConstraintManager) to a symbol.