[klee-dev] Problems around KLEE Recorded Paths

[Zekun Shen]

Hi there,

I am experiencing concolic execution with KLEE recently. Here is what I
want to achieve. I record the path by giving KLEE a concrete file input.
The -output-paths option will generate path files in klee-output folders.
Then, I want to replay the path but give KLEE a symbolic file input. At the
end, I want to get the symbolic path constraint that would generate the
path.

I find there is discordance between the paths. So I need some help with
KLEE.
First, I want to output the llvm assembly code at each node of path. In
this way, I can know where they diverge and try to reconcile the
concrete-run and symbolic-run paths. (My theory is that the code diverge
inside libc functions)

Second, I created an empty main function and compiled it to bytecode a.bc.
When I run $klee ... a.bc <concrete file>$ and $klee ... a.bc A
--sym-files...$ I would get different path files. What would be the reason
for that?

Thank you,
Zekun Shen
-------------- next part --------------
HTML attachment scrubbed and removed