[klee-dev] KLEE+Z3 (an instance of KLEE-MultiSolver) still concretizes floating point expression to 0.

[Zhoulai]

Hello,

I am playing with the recent KLEE-MultiSolver, due to H. Palikareva and C.
Cadar,  trying to generate test inputs for floating point programs.  I have
just successfully installed the nice tool, with Z3 as well as a couple of
other solvers enabled.  My intention is to use KLEE+Z3, in which Z3 should
support both the floating point theory and the theory of real numbers.

However, my installed KLEE+Z3 fails to generate inputs for floating point
programs.  Below is the program under test, borrowed from the official
tutorial of KLEE, this time with a floating point input (rather than an
integer):



















*#include <klee/klee.h>int get_sign(double x) {  if (x == 0)     return 0;
  if (x < 0)     return -1;  else      return 1;} int main() {  double a;
klee_make_symbolic(&a, sizeof(a), "a");  return get_sign(a);} *
Then I run KLEE + Z3 with the commands:

> *       $  llvm-gcc --emit-llvm -c -g get_sign.c*
> *       $  klee --use-metasmt=z3 get_sign.o*
>

The message I got from Terminal:

Starting MetaSMTSolver(Z3) ...
> *KLEE: WARNING ONCE: silently concretizing (reason: floating point)
> expression (ReadLSB w64 0 a) to value 0
> (/home/parallels/Work/klee/examples/get_sign_fp/get_sign.c:8)*
>





*KLEE: done: total instructions = 27KLEE: done: completed paths = 1KLEE:
done: generated tests = 1*

Observe that KLEE + Z3  concretizes floating point expression to 0,
although Z3 is used; it finds only 1 single path instead of 3 that is
expected.

Is there a way to tell KLEE *not* to concretieze floating point expression
to 0 so KLEE + Z3 can be useful when handling floating point program?

Thanks,
Zhoulai
-------------- next part --------------
HTML attachment scrubbed and removed