[klee-dev] Question Regarding Path-based Inductive Synthesis for Program Inversion

[Nguyễn Gia Phong]

On 2024-09-16 at 23:20-05:00, 陈小玉 wrote:
> Hello guys. I recently read article "Path-based Inductive Synthesis
> for Program Inversion" and found it very insightful.  However,
> I have encountered some questions regarding one of the principles
> discussed in the paper about symbolic execution.  I am writing
> to seek clarification on this point.
>
> As in Cond&Loop rule: Rule COND non-deterministically executes
> one of its branches.  Rule LOOP unrolls a loop one time.
> Does that mean in symbolic execution, for each iteration of the loop,
> it unrolls the loop into an “if” statement?

If I understand correctly, PINS ultilizes symbolic execution
to capture the program's logic from its path conditions.
>From the point of view of a symbolic executor (or any interpretor
including physical processing units), loop is not an important concept
and it needs not be identified.  Loops only helps optimization
and analysis, i.e. _go-to statements considered harmful_
(Edsger Dijkstra, 1968).

I like to view the program behaviors as combinations
of logic (conditions connecting the blocks)
and effects (I/O operations within the blocks).
Given a specific execution path, you can group all conditions
into a path constraint and likewise for the effects.

Therefore, at the end of a path, the constraint would contain
the conditions for each iteration of a loop.

On 2024-09-16 at 23:20-05:00, 陈小玉 wrote:
> Does it randomly choose to either execute the loop body
> or jump to the else branch (exit the loop), to just unroll
> the loop again and again util it not meet the requirements
> of “While” anymore?

>From my PoV, the two choices are essentially the same,
as loops don't really exist in lower-level representations
of a program.  It might help to think of a loop declaratively
instead of what the executor does at each step, think about
the end result: the (sub)set of possible program paths.

The mentioned non-determinism simply means from a state,
there are more than one state as an option to transition to,
i.e. the number of paths grows as the program is executed
symbolically, as opposed to a concrete execution with concrete inputs
would have only one determined path.  A loop could have a varied number
of iterations at running time depending on the value of the conditions,
not to be confused with compile-time loop unrolling
that removes the conditions from the generated program.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 248 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20240919/866a3cc0/attachment.sig>