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
On 08/11/2013 00:52, Zhiyi Zhang wrote:
Hi All:
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
are only some examples):
Cat:
Inline image 1
Echo:
Inline image 2
Paste:
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 website:
* 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
*
There is an error as the following figure shows:
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
[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
