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