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, 소프트웨어학과/이재혁
<[email protected] <mailto:[email protected]>>님이 작성:
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
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
