[klee-dev] Klee optimization and run error

[Zhiyi Zhang]

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:
[image: Inline image 1]
Echo:
[image: Inline image 2]
Paste:
[image: 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:
[image: 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
-------------- next part --------------
HTML attachment scrubbed and removed
-------------- next part --------------
A non-text attachment was scrubbed...
Name: image.png
Type: image/png
Size: 6418 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20131108/f8e7d062/attachment.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: image.png
Type: image/png
Size: 5978 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20131108/f8e7d062/attachment-0001.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: image.png
Type: image/png
Size: 6137 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20131108/f8e7d062/attachment-0002.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: image.png
Type: image/png
Size: 21623 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20131108/f8e7d062/attachment-0003.png>