[cfe-dev] Symbolic Extents

[Ted Kremenek]

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

> 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.)


Tying SymExprs with SVals is actually an intrinsic part of their design.  Hopefully I can make that little clearer.

SVals and SymExprs are really part of a single feature.  The are used to represent the "expression semantics" of evaluating expressions.  When we see '(exp1) + (exp2)', we compute an SVal that represents the semantics of evaluating that expression.  In the beginning we only represented a very simple set of semantics which you can think of as a lattice/set of values: { Unknown, Undefined, Constant, Locations }.  SVals are just *handles* to values in this lattice.  This is really important.  We pass SVals around everywhere, but anytime they have real data associated with them we have a FoldingSet to unique that data.  For example, in the case of nonloc::ConcreteInt the SVal indicates that we have a Constant and the associated data is represented by an APSInt.

SymExprs are meant to just be values in this set of values.  They allow us to represent more complicated values, and they allow us to reason about computation more lazily by making the semantic expressions more symbolic.  SymExprs are intrinsically part of how SVals are intended to be used.

Another way to look at it is that we are defining a language to represent "semantic expressions".  That language consists of a grammar, with SVal just being a handle into an expression in that grammar.  More complicated expressions need to reference other expressions, but since SVals are just a single pointer they can't represent that directly.  Instead SVals are used as a generic handle to symbolic expressions, and SymExprs can be built (when needed) to represent the recursive nature of more complicated expressions.  Actually tying SVals and SymExprs closer together makes a lot of sense, because they are just meant to represent that grammar of expressions.

My suggestion for using parts from Klee was that Klee has its own expression language, similar to the notion of SymExprs.  Klee's expression language, however, is far more developed, although it has a different memory model.  We could bring in parts of Klee's expression language by potentially wrapping them in SVals.  The end goal, however, is that we define an expression language for defining the semantics of expressions.  That design is really clear to me, but it is represented very clearly in the code.