[klee-dev] Effect of --optimize

[Eduardo R B Marques]

Hi,

Klee's “—optimize” switch  "optimizes the code before execution by running various compiler optimization passes”.
However, it does seem to hurt the state-space exploration severely. For instance consider the simple regular expression tutorial <https://klee.github.io/tutorials/testing-regex/> where
the use of “—optimize” causes klee to find only one (!) path.

Why is this so?  I am getting this type of behavior with other programs too and in the work of a student of mine it’d be relevant
to check the sensitivity of klee (and other testing/fuzzing tools) to code optimisation.

1) Compilation (as in the tutorial): 

$ clang -I ../../include -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone Regexp.c

2) Normal execution (as in the tutorial): 

$ klee --only-output-states-covering-new Regexp.bc
…
KLEE: Using STP solver backend
KLEE: ERROR: regexpr0.c:23: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: regexpr0.c:25: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location

KLEE: done: total instructions = 4848112
KLEE: done: completed paths = 6675
KLEE: done: partially completed paths = 763
KLEE: done: generated tests = 16

3) Execution with —optimize

$ klee --optimize --only-output-states-covering-new Regexp.bc
…
KLEE: Using STP solver backend

KLEE: done: total instructions = 5
KLEE: done: completed paths = 1
KLEE: done: partially completed paths = 0
KLEE: done: generated tests = 1

(Btw similar behavior occurs if I remove —optimize but the bitcode is previously optimised with -O2 in step 1 above).

For reference klee —version reports:

KLEE 2.3-pre (https://klee.github.io)
  Build mode: RelWithDebInfo (Asserts: TRUE)
  Build revision: df04aeadefb4e1c34c7ef8b9123947ff045a34d9

LLVM (http://llvm.org/):
  LLVM version 11.1.0
  Optimized build with assertions.
  Default target: x86_64-unknown-linux-gnu
  Host CPU: skylake

Best,
Eduardo Marques
-------------- next part --------------
HTML attachment scrubbed and removed