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