[klee-dev] Confused with KLEE options

[Jonathan Neuschäfer]

On Wed, Apr 24, 2013 at 10:37:48PM +0800, Hongxu Chen wrote:
> 
> 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.

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.

>      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

>      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".

>      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)

>      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;
  }

>      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