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.
signature.asc
Description: PGP signature
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
