One more thing: in that paper, it's enough to read the first ~2.5 pages
that describe the forking model used by KLEE to deal with certain types
of symbolic pointer dereferences (when execution cannot continue fully
symbolically, which can be seen as a form of concretisation, although
perhaps this is not the best term to use in this case).
You might also be interested in how KLEE deals with external calls,
where a more standard concretisation takes place in some cases:
https://klee-se.org/docs/options/#external-call-policy
Best,
Cristian
On 19/06/2025 22:24, Cristian Cadar wrote:
Hi Frank,
KLEE can support loads/stores from symbolic addresses, although there
are limitations. For instance, if p is a symbolic pointer pointing
somewhere within a certain memory object, then *p does not trigger any
concretisation. For a discussion of cases that do trigger
concretisations, I recommend this paper:
https://srg.doc.ic.ac.uk/files/papers/segmem-esecfse-19.pdf
Best,
Cristian
On 08/06/2025 04:06, A Code wrote:
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.
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
