[klee-dev] Concretization of a symbolic variable

[Cristian Cadar]

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 at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev