Klee optimization and run error

Cristian Cadar

2013-11-08 11:29:20 UTC

Hi Zhiyi,

There are a quite few issues with your experiments:
* many options are enabled by default, so for example your
non-optimization runs actually have most optimizations enabled :)
* KLEE is quite non-deterministic so different runs are not going to
issue the same instructions/queries. To measure the effect of
constraint solving optimizations, it is essential to take care of this.
* Running for less of a second is not going to give an accurate picture
of what's happening with constraint solving optimization in KLEE
* --disable-opt has nothing to do with constraint solving optimizations

You might want to take a look at our CAV'13 paper
(http://srg.doc.ic.ac.uk/publications/klee-multisolver-cav-13.html),
which discusses in more detail the constraint solving optimizations in
KLEE (and cex caching in particular) and also what we had to do to get
deterministic runs.

Cristian

Post by Zhiyi Zhang
I am doing an imperial study about constraint solver optimization
techniques. I use Klee and GUN Coreutils to do the experiments.
As you say in the paper (KLEE: Unassisted and Automatic Generation of
High-Coverage Tests for Complex Systems Programs)
<http://www.doc.ic.ac.uk/~cristic/papers/klee-osdi-08.pdf>, Klee have
five constraint optimization techniques,that are
1,constraint caching
2,constraint independence optimization
3,expression rewriting
4,constraint set simplification
5,Implied value concretization.
What I did is that I compared the time and the percent of the solver
(which I can see using $ klee-stats klee-last), when using different
optimization techniques during Klee running. I used the following
options when I run Klee. Take echo as an example.
for non-optimization: *klee.cde --disable-opt --libc=uclibc
--posix-runtime --init-env** ./echo.bc --sym-arg 3*
for only constraint caching: *klee.cde --use-cache --use-cex-cache
--libc=uclibc --posix-runtime v ./echo.bc --sym-arg 3*
for only constraint independence optimization:***klee.cde
--use-independent-solver --libc=uclibc
--posix-runtime --init-env** ./echo.bc --sym-arg 3*
for only expression rewriting: *klee.cde --rewriter=local --libc=uclibc
--posix-runtime --init-env** ./echo.bc --sym-arg 3*
for only Implied value concretization: *klee.cde
--make-concrete-symbolic=10 --libc=uclibc
--posix-runtime --init-env** ./echo.bc --sym-arg 3*
I have some questions about optimization techniques.
(1)*Does the options what I have used for optimization techniques are
right?*
(2) *What is the options only for constraint set simplification?*
*
*
(3) For only Implied value concretization, when I used *klee.cde
--make-concrete-symbolic=10 --libc=uclibc
--posix-runtime --init-env** ./echo.bc --sym-arg 3*, only I setted
*--make-concrete-symbolic=0 *could I get the result, otherwise Klee run
a long time and killed by SIGSeGV, like question 5.
(4) Here are some results(I have used all the GUN Coreutils and there
Inline image 1
Inline image 2
Inline image 3
As the result shows: many optimization techniques have *NOT* improve
efficiency. But the result in the paper(KLEE: Unassisted and Automatic
Generation of High-Coverage Tests for Complex Systems Programs)
<http://www.doc.ic.ac.uk/~cristic/papers/klee-osdi-08.pdf>is very good/.
/So I was surprise of the results. I did not know whether I used the
wrong options result in this results.
Also*there are good results*. For example: for program base64, when
using --use-cache --use-cex-cache, it only cost 0.5 second, compared
with 78 seconds using other optimization techniques or non-optimization.
But* the Solver(%) was down from 92%*(using other optimization
techniques or non-optimization) *to 55%*(optimization cache techniques)
*(I also want to know what the **Solver(%) means. I think it is
the percentage that the constrains set can be solved by STP*). And also,
*such examples are few*.
So could I have the conclusion:* for most programs, the optimization
techniques are not effective. But for some programs, the **effect is
very obvious.*
(5), When I did the experiments for some large programs, for example,
the hostid program, I used the following options which I found on the
* klee.cde --optimize --libc=uclibc --posix-runtime --init=env
./hostid.bc --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8
*
Inline image 2
I do not know why this happened. Does that mean my memory is too small
to run? I used 8GB memory.
Actually, I did not find the option -sym-args(or -sym arg) in the
klee.cde --help. I found -sym-agrv and -sym-agrv , so I use the options
* klee.cde --optimize --libc=uclibc --posix-runtime --init=env
./hostid.bc **--sym-argv 1 --sym-argvs 0 2 2 --sym-files 1 8*, but Klee
only found *one* path. As I know, there are 4799 paths for hostid.
I am very interesting in Klee. Hope for your reply.
Thank you very much.
Zhiyi Zhang
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev