[klee-dev] 3 quick questions about KLEE

[Kirill Bogdanov]

Hello everyone!

I wonder if I could ask 3 quick questions, in case someone came across them
at some stage :)
Thank you very much in advance!

*Question 1. *
I am running integer version of KLEE and I am getting this error in my code
(followed by STP assertion):

valuewidth of lhs of EQ: 32
valuewidth of rhs of EQ: 64
indexwidth of lhs of EQ: 0
indexwidth of rhs of EQ: 0
Fatal Error: BVTypeCheck: terms in atomic formulas must be of equal length

332:(EQ
  198:0x00000006
  330:0x000000000000003F)


I have identified part of the code with this problem and created a small
example which can reproduce this problem:

#include <klee/klee.h>
#include <assert.h>
#include <iostream>

int main(int argc, char *argv[]){
         int x,z;
        klee_make_symbolic(&x, sizeof(x), "x");
        klee_make_symbolic(&z, sizeof(z), "z");
        klee_assume(x > 1000);
        klee_assume(x < 10000);
        klee_assume(z > 1000);
        klee_assume(z < 10000);

        int n = 100;
        int m = x;
        m = m / n;
        z = z / m;

        klee_assert(z > 20);
}

compiling with: llvm-gcc --emit-llvm -c -g kleeExample.cpp  (using -O3 does
not affect the error)
running: klee kleeExample.o

It looks like a compiler problem to me, I am only performing integer
computations. Can I rearrange my code to avoid this error ? Am I doing
something wrong here ?

*Question 2.*

Are there KLEE options or some method that would allow KLEE to generate
multiple test cases for one assertion ? (sorry if I missed it from some
tutorials)
Example:
I have a program that solves linear equations:  {   x+y<30 and x*y=42 } .
Code looks like this:

int main(int argc, char *argv[]){

int x = klee_range(0 , 100000, "x");
int y = klee_range(0 , 100000, "y");

if ((x+y < 30) && (x *y == 42)){
klee_assert(false);
}
return 0;
}


I am using DFS search and klee exits upon finding first solution x=6, y=7.
In reality there are more solutions to these equations, so can I "ask" KLEE
to keep searching for tests cases that will produce this assertion?
Alternatively if I found first set of solutions, I can go back and modify
original code by saying klee_assume( x!=6) and y!=7 and repeat these steps
every time I get new solutions, but this seems to be very slow process to
me. Perhaps KLEE will start running slower when I will add a lot of
constraints on x and y?
Is there any way to get multiple (perhaps all) possible test cases for one
assertion ?


*Question 3*

Could you please advise on nature of the following error:

*State:UpdateQueues for index State:UpdateQueues for index KLEE: WARNING
ONCE: flushing 80032 bytes on read, may be slow and/or crash:
MO10182[80032] allocated at main():  %10 = call i8* @_Znwm(i64 80032), !dbg
!3534*
*ERROR: STP did not return successfully.  Most likely you forgot to run
'ulimit -s unlimited'*

my ulimit is already set to unlimited and I have 20+GB of ram available, so
I just trying to understand general direction of what could be the cause.


Thanks a lot for your time!!
-------------- next part --------------
HTML attachment scrubbed and removed