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

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

Hi, thank you for your prompt response.

I realize that my previous question may have been ambiguous, and I
apologize for any confusion this may have caused. Based on your reply, KLEE
skips solver calls for paths followed by the seeds. However, I came across
the following line in klee/Core/lib/Executor.cpp:

bool success = solver->evaluate(current, condition, res);
(Of course, this line has changed in the latest version with parameters'
name.)

According to the header file, the evaluate() function is described as
follows:
// evaluate() - Determine for a particular state if the query expression is
// provably true, provably false, or neither.

>From this description, I inferred that this function checks the
satisfiability of a given condition. If my understanding is incorrect,
please let me know.

Despite this, I noticed that KLEE executes this line regardless of the
seeding mode. This led to my question: "How does KLEE check the
satisfiability (feasibility) when seeding without a solver call?"

To illustrate, when executing the code:

if (x < 3) {
  if (x > 4) {
  }
}

with a seed input of x = 2, the input satisfies (x < 3) and (x <= 4).
Therefore, after seeding, states with conditions (x >= 3) and ((x < 3) and
(x > 4)) should be generated. However, KLEE does not generate a state for
the latter condition (it seems because the condition (x < 3) and (x > 4) is
unsatisfiable), indicating that satisfiability is being checked during
seeding.

Could you please point out the specific line of code where satisfiability
is checked without invoking the solver?

Thank you for your assistance.

Sincerely,

Jaehyeok Lee

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

> 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