Kirill Bogdanov

2014-05-20 13:37:01 UTC

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!!

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!!