[klee-dev] 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
-------------- next part --------------
HTML attachment scrubbed and removed
-------------- next part --------------
A non-text attachment was scrubbed...
Name: image.png
Type: image/png
Size: 21623 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20131114/204fc7b4/attachment.png>