Hi,
I would first advise to use the latest version of KLEE, which has some
important improvements related to the seeding functionality.
In principle, KLEE should indeed not call the solver for the path
executed by the seed -- however, it still does so in a few places, which
we should fix. However, note that by default, KLEE will check the
feasibility of paths diverging from the seed, so that it can later
explore them. To disable this exploration, you should additionally use
--only-replay-seeds.
Best,
Cristian
On 26/04/2024 09:44, 소프트웨어학과/이재혁 wrote:
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,
ᐧ
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
