[klee-dev] Klee optimiztion

[Paul Marinescu]

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

-------------- next part --------------
HTML attachment scrubbed and removed