Klee optimiztion

[Zhiyi Zhang]

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: Inline image 2]*

Thanks for your help again and Best Wishes.
Zhiyi Zhang

[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-AQ/***@public.gmane.org/) 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

Post by Zhiyi Zhang
Hi, all,
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[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

Post by 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
'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

Post by Zhiyi Zhang
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
**
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev