[klee-dev] Klee optimiztion

[Cristian Cadar]

Yes, the searchable list archives can be very useful in clarifying your 
questions.  You might also want to search for "may be slow and/or crash" 
to get more information about the error you're seeing.  As I pointed out 
last time, to measure the effect of various optimizations, it is 
important to make sure your runs are deterministic; see also the recent 
question from Hongxu Chen.

Best,
Cristian

On 13/11/2013 22:42, Paul Marinescu wrote:
> A very good starting point for reproducing the OSDI'08 experiments is to
> see the dedicate page at
> http://ccadar.github.io/klee/CoreutilsExperiments.html or search the
> list archive (http://www.mail-archive.com/klee-dev@imperial.ac.uk/) for
> 'reproduce' or 'reproducing'.
>
> 1. Most (all?) optimizations have a corresponding command line argument.
> Check klee --help
> 2. Solver(%) is the percentage of time spent solving constraints.
> 3. If your intention is to reproduce the OSDI'08 experiments, use the
> same command line arguments. See
> http://ccadar.github.io/klee/CoreutilsExperiments.html
> Paul
>
> On 13 Nov 2013, at 19:04, Zhiyi Zhang <xianlingzibiying at gmail.com
> <mailto:xianlingzibiying at gmail.com>> wrote:
>
>> Hi, all,
>> **
>> I have read your OSDI08' paper and want to reproduce the experiment in
>> Section 3.3(about query optimization). But I also have some questions
>> during the reproduction:
>> **
>> 1, How can I disable all optimization techniques when I run Klee?
>> Moreover, as your said in your OSDI08' paper, there are five
>> optimization techniques(1,constraint caching, 2,constraint
>> independence optimization, 3,expression rewriting, 4,constraint set
>> simplification, 5,Implied value concretization), how can I make the
>> five optimization techniques enabled respectively? (for example, only
>> use constraint independence when I run Klee)
>> *
>> *
>> 2, What does the Solver(%) (in the result)mean? Does that mean
>> the percentage of the constrains set can be solved by STP?
>> **
>> 3, When I run some large programs using Klee, for example, the hostid
>> program, I used the following options: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.
>> Klee was killed. The following figure shows some information. How to
>> solve this problem?
>> *<image.png>*
>> *
>> *
>> Thanks for your help again and Best Wishes.
>> Zhiyi Zhang
>> _______________________________________________
>> klee-dev mailing list
>> klee-dev at imperial.ac.uk <mailto:klee-dev at imperial.ac.uk>
>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>