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
