Dear all,
I wrote the hereby attached example for stressing the KLEE execution. The
aim of the code is creating as many executions paths as possible with a
simple example. You can play with the SIZE constant to increase the number
of paths.
// This function checks if the provided sequence is strictly increasing.
// Return 0 if increasing, 1 otherwise.
int exec (int a[])
{
int flag = 0;
int i;
for (i = 1; i < SIZE; i++)
if (a[i-1] >= a[i])
flag = flag | 1;
return flag;
}
I have several questions starting from this case study:
1)
If I use different optimization for clang (-O0 or -O1) and the number of
execution paths is respectively reduced from 2^(SIZE-1) to 2. I am assuming
this is related to some optimization done on the llvm byte code for the
specific example.
For example with SIZE=10 and -O0 flag (no optimization)
KLEE: done: total instructions = 21490
KLEE: done: completed paths = 512
KLEE: done: generated tests = 512
while with SIZE=10 and -O1
KLEE: done: total instructions = 128
KLEE: done: completed paths = 2
KLEE: done: generated tests = 2
In the attached PDF file, I summarized the results as a graphical
representation of the execution paths.
Are these kind of optimizations related to KLEE or they are simply an
LLVM/clang inheritance on the low level representation of the design?
2)
The example emits an assert if a "strictly ascending sequence" is found. In
this way I tried to represent a deep (artificial) bug in the code, higher is
the value of SIZE, deeper is the bug in my code (or much more difficult is
to find it).
- I noticed that the assert is detected pretty soon with respect to the
simulation duration, are you addressing the "assert" statements in some way
in the llvm code?
- According to the OSDI 2009 paper there are at least two strategies for
state scheduling: the random path selection and the coverage optimized
search. How are these heuristics enabled during the simulation? I found the
klee flag -use-random-path I am assuming that this one disable the optimized
search but I am not sure. Could you please clarify the approach?
- Did you implement any other heuristic?
- Can I trace/print the execution paths? For example the klee flag
-write-paths produces a file .path for each testcase. This file contains a
sequence of 0 and 1, I am assuming that this sequence represents the
left/right true/false selection on each branch (but I am not sure). How can
I analyze the execution tree and the related .path file. Does exist any
graphical interface or a more explicit description of the path?
Best regards,
Giuseppe
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20100428/107e3918/attachment-0001.html
-------------- next part --------------
A non-text attachment was scrubbed...
Name: paths.pdf
Type: application/pdf
Size: 221696 bytes
Desc: not available
Url :
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20100428/107e3918/attachment-0001.pdf
-------------- next part --------------
A non-text attachment was scrubbed...
Name: rei01.c
Type: application/octet-stream
Size: 529 bytes
Desc: not available
Url :
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20100428/107e3918/attachment-0001.obj
