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/[email protected]/) 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 <[email protected]
<mailto:[email protected]>> 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
[email protected] <mailto:[email protected]>
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
