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

[Cristian Cadar]

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 at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev