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

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

>
> Hi,
>
> Thank you so much for giving me an explanation!
>


> I still have some questions. I initially thought that KLEE passes through
> all the path conditions that a seed goes through without invoking the
> solver. In this process, I understood that the feasibility(satisfiability)
> check of the true branch and the false branch is also omitted. Because
> there is no calls to the SMT solver with seed inputs, and the role of
> solver call when forking is to check satisfiability of both branches (True
> or False). However, I found the following passages in your paper, "Pending
> Constraints in Symbolic Execution for Better Exploration and Seeding":
>
> "More formally, an assignment is a mapping from symbolic variables to
> concrete values, e.g., {x ← 2, y ← 3}. The Substitute function takes a
> symbolic condition and an assignment and evaluates the condition under the
> assignment (line 4)."
>
> "In FastIsSat, we modify the GetAssignmentsForState function to return the
> seeds as assignments (line 2). As a result, only the states that satisfy
> the seeds are followed first, and there are no calls to the SMT solver
> until all the paths followed by the seeds are explored."
>
> With these phrases, my question is as follows:
>
> How does a seed skip the feasibility check of branches only using concrete
> values?
> For an easier example, let's assume a program like if (x < 3) { if (x > 4)
> { } }. In the first if statement, KLEE can check the feasibility of the
> branch x < 3 and the branch x >= 3. However, in the second if statement,
> the branch x < 3 ∧ x > 4 is not feasible.
>
> What if we use a seed input as x = 2, how does KLEE determine the
> feasibility of this without solver calls?


Thanks!
Sincerely,
ᐧ

2024년 4월 26일 (금) 오후 5:44, 소프트웨어학과/이재혁 <jaehyeok.lee at g.skku.edu>님이 작성:

> 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