[cfe-dev] Symbolic Extents

[Jordy Rose]

On Tue, 29 Jun 2010 17:23:20 -0700, Ted Kremenek <kremenek at apple.com>
wrote:
> On Jun 29, 2010, at 1:56 PM, Jordy Rose wrote:
> 
>> 
>> On Tue, 29 Jun 2010 10:44:47 -0700, Ted Kremenek <kremenek at apple.com>
>> wrote:
>>> 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.
>> 
>> Aliasing isn't so bad; it's the other constraints that would be harder
to
>> model with sym-sym relations. But maybe we just support aliasing for a
>> while, or aliasing+linear adjustment, and ignore constraints like "a <
b"
>> or "a != b".
> 
> 
> For "a < b" and such, isn't it a matter of unifying the constraints that
> already exist on 'a' and 'b'?


Something like that, but fully modeling it can get complicated very
quickly:

a < b
a < c
// a != MAX, but other than that we know nothing
b == 11
// at this point a < 11
c == 10
// now a < 10

In the long-term I think we're going to want to arbitrarily impose an
order on symbols, so that higher symbols depend on lower ones and not the
other way around. Alternately (or additionally?), we could have a
notification system of some kind: when a min or max value changes, ping any
dependent symbols.

Constraints can form arbitrarily complex graphs, in theory, and we do have
to limit that. Unifying the current constraints is certainly an improvement
over our current state.