[klee-dev] [Question about process of seed in KLEE] For mechanism of detailed process when putting seed in KLEE

[소프트웨어학과/이재혁]

To Whom it may concern,

Hello, this is jaehyoek Lee, a master degree's student in computer science
in South Korea.

I have some questions about the detailed process of KLEE, especially the
seeding process, so I'd like to send this mail.

I'm using klee-2.1 under LLVM 6.0.0 version.

>From my understanding, if I put a seed file into KLEE using a command like
'--seed-file=***.ktest', then KLEE generates that seed file much more
quickly than generating that seed file before execution.
I found that code line in Klee/lib/Core/Executor.cpp as
      bool success =
        solver->getValue(current, siit->assignment.evaluate(condition),
res);
Siit means the SeedInfo file indicating the seed I put in KLEE.
In this case, here is my question.

1. If we put a test case in KLEE, KLEE gets a seed ktest file and uses that
information related to the generated test case. Then, when KLEE calls a
solver like the aforementioned code, does the solver try to check the path
condition of current state and state included in seed?
Actually, the point that I couldn't understand is what
assignment.evaluate(condition) does in this section.

2. I thought if I put a test case as seed in KLEE, KLEE doesn't have to
call a solver because the seed file already has all the information for
generating that seed file like state or path-conditions. Is that right? If
it's right, Is it okay to understand that Seed Mode doesn't have to call a
solver for the feasibility check that would be a very big problem in
Symbolic Execution called 'constraint solving cost problem', or solve the
path condition the seed file includes?
If it's wrong, then what solver calls are doing in Seed Mode?

Thank you so much.
Sincerely,
ᐧ
-------------- next part --------------
HTML attachment scrubbed and removed