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
