[klee-dev] 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