[klee-dev] Klee optimization and run error

[Cristian Cadar]

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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>