[cfe-dev] Symbolic Extents

[Jordy Rose]

Okay. I think my misunderstanding came from wondering when to pass around
a SymExpr vs. an SVal, since not all SVals map into SymExprs. (In
particular, you can't pass a SymExpr and an APSInt in the same variable.)
The answer seems to be "never" -- you always want an SVal for API that
faces the checkers -- because SymExpr is almost an implementation detail.
Does that sound right?

(usual qualification about exceptions to every rules)

I was also confused by the fact that SymExprs don't deal in SVals, but I
guess they don't need to. The nonloc types are either symbolic, constant,
or compound, and you can't do a symbolic operation to a compound value.


On Tue, 29 Jun 2010 10:36:43 -0700, Ted Kremenek <kremenek at apple.com>
wrote:
> 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.