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

[Cristian Cadar]

Hi, as mentioned in that paragraph, we can only skip the solver calls 
for the paths followed by the seeds: "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."  Afterwards, we do 
need to start making solver calls.

Best,
Cristian

On 02/07/2024 08:15, 소프트웨어학과/이재혁 wrote:
>     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 <mailto: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,
>     ᐧ
> 
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev