Confused with KLEE options

[Hongxu Chen]

Hi all,

We have been doing some experiments on KLEE recently and find that some of
KLEE's options are a bit confusing.

1. `--optimized'
This option does not appear when using `klee --help-hidden', but in
this page:

http://klee.llvm.org/CoreutilsExperiments.html

the authors include it. And the running result by klee(r165499) is
really different if we added it(when we make symbolic a loop bound,
the time cost is significantly reduced). From the paper(osdi, 08)
we find that there are 2 important optimizations called `constraint
independence' and `counter-example-cache', and we find another
option called `--use-cex-cache'. We guess that the former
optimization is always executed in KLEE. So what exactly does
`--optimized' do? I also noticed there was an answer on
stackoverflow
(http://stackoverflow.com/a/12952881/528929), but failed to
understand it. What's more, in some of our cases, with this option
klee didn't generate the counter-example that fired the assertion.
Are there any docs about it?

2. --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdout

These options can still been seen from the `Coreutils Experiments'
page(What options did you run KLEE with?).
The paper tells that `--sym-args 1 10 10' means to use 0 to 3
command line arguments, and `1',`10', `10' is the length of the
args. But the options listed above contains the digit `0'; does it
have a special meaning? What's more, there are 2 `--sym-args', what
does each of them mean? Also, I am confused with the `--sym-stdout'
option.
I also have a question for this: Is `ls -la -d' treated as 2
arguments or 3 in KLEE's view?

3. Is there an option that makes klee stop on a SPECIAL kind of error?
From `Tutorial Two'(http://klee.llvm.org/Tutorial-2.html) I learn
that there would be several kinds of errors during the symbolic
execution and there is an option called `-exit-on-error' that can
be used to force klee to exit WHENEVER an error occurs. However
sometimes we only care about certain errors(say `div') and would
like it to exit on these errors, what can we do? Do we have to
change the source code of klee a bit(till now we haven't taken a
deep look at the src and feel that hacking it is not that easy)?

4. Do we need to add more options when we run the MINIX tr tool talked
about it the paper?

KLEE's api seems to have been changed a lot since the paper was
published. So I am wondering whether we need to add `--libc' and
`--posix-runtime' besides changing `--max-time'/`--max-fail' if we
expect to get similar results with the paper?

5. What does the result `klee-stats klee-last' indicate when the
`Instrs' is 0 whereas `ICount' is not?

This seems a bit odd, but we actually have met this case. Are we
using klee the wrong way or something else?


Any help is appreciated! Thanks.

Hongxu Chen

[Jonathan Neuschäfer]

Post by Hongxu Chen
Hi all,
We have been doing some experiments on KLEE recently and find that some of
KLEE's options are a bit confusing.
1. `--optimized'
This option does not appear when using `klee --help-hidden', but in
http://klee.llvm.org/CoreutilsExperiments.html
the authors include it.

I think you've misread the option's name:
| $ klee --help | grep optimized
| $ klee --help | grep optimize
| -optimize - Optimize before execution
| -stp-optimize-divides - Optimize constant divides into add/shift/multiplies before passing to STP (default=on)

AFAIK -optimize applies LLVM's optimization passes to the code, and is
quite unrelated to the other options you mentioned below.

Post by Hongxu Chen
And the running result by klee(r165499) is
really different if we added it(when we make symbolic a loop bound,
the time cost is significantly reduced). From the paper(osdi, 08)
we find that there are 2 important optimizations called `constraint
independence' and `counter-example-cache', and we find another
option called `--use-cex-cache'. We guess that the former
optimization is always executed in KLEE. So what exactly does
`--optimized' do? I also noticed there was an answer on
stackoverflow
(http://stackoverflow.com/a/12952881/528929), but failed to
understand it. What's more, in some of our cases, with this option
klee didn't generate the counter-example that fired the assertion.
Are there any docs about it?
2. --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdout
These options can still been seen from the `Coreutils Experiments'
page(What options did you run KLEE with?).

You can view a help text for these options by specifying --help on the
command line of a program run with the "posix runtime" under klee:

| $ cat > test.c
| int main(int argc, char **argv)
| { return argc; }
| $ llvm-gcc -emit-llvm -c test.c -o test.bc
| $ klee -posix-runtime test.bc --help
| KLEE: NOTE: Using model: /home/jonathan/dev/llvm/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca
| KLEE: output directory = "klee-out-3"
| KLEE: WARNING: undefined reference to function: __xstat64
| KLEE: ERROR: /home/jonathan/dev/llvm/klee/runtime/POSIX/klee_init_env.c:24: klee_init_env
|
| usage: (klee_init_env) [options] [program arguments]
| -sym-arg <N> - Replace by a symbolic argument with length N
| -sym-args <MIN> <MAX> <N> - Replace by at least MIN arguments and at most
| MAX arguments, each with maximum length N
| -sym-files <NUM> <N> - Make stdin and up to NUM symbolic files, each
| with maximum size N.
| -sym-stdout - Make stdout symbolic.
| -max-fail <N> - Allow up to <N> injected failures
| -fd-fail - Shortcut for '-max-fail 1'
|
|
| KLEE: NOTE: now ignoring this error at this location
|
| KLEE: done: total instructions = 100
| KLEE: done: completed paths = 1
| KLEE: done: generated tests = 1

Post by Hongxu Chen
The paper tells that `--sym-args 1 10 10' means to use 0 to 3
command line arguments, and `1',`10', `10' is the length of the
args.

This line seems to use an outdated --sym-args syntax. With the syntax
described in the help text above it would be: "-sym-arg 1 -sym-args 2 2 10".

Post by Hongxu Chen
But the options listed above contains the digit `0'; does it
have a special meaning? What's more, there are 2 `--sym-args', what
does each of them mean?

(see above)

Post by Hongxu Chen
Also, I am confused with the `--sym-stdout' option.

It is implemented here:
runtime/POSIX/klee_init_env.c:85 (klee_init_env)
runtime/POSIX/fd_init.c:103 (klee_init_fds)
runtime/POSIX/fd.c:301 (write)

fd.c, line 314 is especially interesting:
if (__exe_fs.max_failures && *__exe_fs.write_fail == n_calls) {
__exe_fs.max_failures--;
errno = EIO;
return -1;
}

Post by Hongxu Chen
I also have a question for this: Is `ls -la -d' treated as 2
arguments or 3 in KLEE's view?

If you plan to find "-la -d" through symbolic arguments, it will be two.

HTH,
Jonathan Neuschäfer