[klee-dev] Concretization of a symbolic variable

[Cristian Cadar]

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