Dear all,
> - Did you implement any other heuristic?
in klee/lib/Core/Searcher.{h,cpp}, 9 different scheduling strategies
(Searcher) are reported:
http://t1.minormatter.com/~ddunbar/klee-doxygen/index.html
Did you compared them on a set of benchmarks? Which of these is/are
more promising?
Best regards,
Giuseppe
2010/4/28 Giuseppe Di Guglielmo <giuseppe.diguglielmo at gmail.com>:
> 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
>
>
>
>
>
>
>
>
--
Se non ci fosse l'ultimo momento non si riuscirebbe a fare niente.
