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

[klee-dev] KLEE with Non-linear integer constraint; warning about the external 'put'

[Zhoulai]

Hello,

I have two naive questions.

I thought KLEE relies on SMT solver on the theory of linear arithmetics and
therefore, it should be unable to explore path involving non-linear
relation.  But I am surprised by the results from testing a program with a
simple polynomial constraint:








*#include klee/klee.h#include stdio.hint foo(int x) {  int y =
x*x*x+x*x+x;  if (y == 1110){ ...  }*

*  return 0;*







*} int main() {  int a;  klee_make_symbolic(a, sizeof(a), a);  return
foo(a);} *
KLEE successfully triggers the branch 'y==1110', Why?

*Another question:* I got a warning from symbolically executing the program
above:

*KLEE: WARNING ONCE: calling external: puts(169520648)*

What does the warning mean?

Thanks for your ideas.
Zhoulai
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev