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
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
