search

swtv-kaist / cs458-spring24

6 stars 0 forks source link

[Hw7] In Part 2 Problem 4, what is an "symbolic execution path" and how to show them? #46

Closed tncks0121 closed 3 months ago

tncks0121 commented 3 months ago

I think "execution path" can be interpreted as the sequence of nodes of the control flow graph visited in the real execution.

I also think the symbolic path formula can be obtained by collecting all necessary conditions to visit each node in the execution path.

However, I'm not sure what an "symbolic execution path" means exactly.

In particular, I'm not sure how to show them in Part 2 Problem 4. It would be nice if there is an example of a symbolic execution path for a very simple program like in https://github.com/swtv-kaist/cs458-spring24/blob/main/5-concolic-testing/lec33-crown-Examples-v2.pdf

swtv-kaist commented 3 months ago

You can find all information necessary for HW#7 from the crown tutorial lecture slides ;-) image

image

tncks0121 commented 3 months ago

I did read those slides, but there is no exact term "symbolic execution path", so I just wanted to be sure. Will specifying list of (branch id, condition) be enough?

Thanks for answering in such a late time, and I'm sorry if this issue interrupted

swtv-kaist commented 3 months ago

You can consider "symbolic path formula", "symbolic execution", "symbolic path", "symbolic execution path" as a same term.

Will specifying list of (branch id, condition) be enough?

Yes. You can write a symbolic execution path in a human readable format as shown in the output of print_execution Ex. (a >0 ) /\ (b > 0) /\ (c>0) /\ (a!=b) /\ (a==c)

tncks0121 commented 3 months ago

Thanks for the clarification!