Concretization

[A Code]

Hi,

I have a question regarding how the SE engine handle 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.

[Vitaly Chipounov]

Hi,

Please find my answers below.

On Saturday, June 7, 2025 at 6:13:16 PM UTC+2 anac...@gmail.com wrote:

I have a question regarding how the SE engine handle 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).

I suppose by "a load from a address that is symbolic" you meant a concrete address that points to a symbolic value, not a symbolic address itself.

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.

No, nothing special will happen on a simple load or on any other instructions that involve general purpose CPU registers or physical RAM.

If execution encounters a branch that depends on a symbolic expression, the solver will be called to decide with path is valid. If both are, the execution engine would add a path constraint, but no concretization would occur.

Now, concretizations may happen because of S2E limitations, e.g,. when writing symbolic values to locations that do not support symbolic values (some CPU registers, virtual devices, etc).

In that case, the solver will be called, a value determined, a constraint added, then the concrete value actually written.

Note that S2E uses concolic execution, so the solver may not be called, instead the expression is evaluated with the concrete inputs compatible with the current path constraints, then the constraint is added.

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.

Yes

 

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

Yes 

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.

No. Symbolic expressions are shared between states, this cannot be done. You could of course do copy-on-write, but that's not how the current engine works. The challenge is to scan the memory for expressions and do the replacement efficiently.

 

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.

Vitaly