[klee-dev] Concretization of a symbolic variable

[A Code]

Hi,

I have a question regarding how the SE engine handles symbolic addresses
during memory operations. Specifically, what takes place under
"concretization".

Suppose two initial symbolic variables x and y, and execution encounters a
load from an address that is symbolic, a read from address: f(x). My
understanding is that, at this point, the engine may query the SMT solver
to choose a concrete value for x, effectively concretizing the *symbol x* in
order to proceed.

Which of the following actions are taken by the engine as part of
concretization?

*a.* Substitute the concrete value from the solver (e.g., say 3) to resolve
f(x) to a concrete address and complete the load operation.

*b.* Add a path constraint x = 3 to the current path.

*c.* Scan the symbolic state and replace all expressions involving x with
the corresponding concrete value. For example, if a memory cell contains
the symbolic expression x + 10, is it updated to 3 + 10=13 and the cell is
no longer symbolic. If a memory cell contains the symbolic expression x +
y, it is updated to 3 + y.

Specifically, I’m unsure about (c) as intuitively (c) is not needed when
the new constraint (x = 3) has been added under (b). During concretization,
is such replacement typically performed by the SE engine, or is the
symbolic state retained as it is, with the engine continuing execution
under the new constraint? Please help clarify.

Thanks,

Frank J.
-------------- next part --------------
HTML attachment scrubbed and removed