Discussion:
3 quick questions about KLEE
(too old to reply)
Kirill Bogdanov
2014-05-20 13:37:01 UTC
Permalink
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!!
Cristian Cadar
2014-05-20 15:01:13 UTC
Permalink
Post by Kirill Bogdanov
*Question 1. *
I am running integer version of KLEE and I am getting this error in my
What do you mean by the "integer version"?
Post by Kirill Bogdanov
computations. Can I rearrange my code to avoid this error ? Am I doing
something wrong here ?
I don't see this error, although I get a different one, in the CEX
caching code (which can be disabled with --use-cex-cache=false). I'm
using STP r940 (the one recommended on the website), what STP version
are you using? I suggest opening a bug report on GitHub.
Post by Kirill Bogdanov
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.
Take a look at
http://www.mail-archive.com/klee-dev%40imperial.ac.uk/msg00950.html

Best,
Cristian
小、   ̄洁
2014-06-02 15:53:20 UTC
Permalink
Dear Cristian,
Sorry to disturb you for a question.
About the file assembly.ll, i donot know how to read it ,because i did not know some rules. Where can i learn those rules which it needs to read the assembly.ll in Klee-last.?
Sincerely,
ZengJie




------------------ Original ------------------
From: "Cristian Cadar(2008 KLEE Author)"<***@imperial.ac.uk>;
Date: 2014Äê5ÔÂ20ÈÕ(ÐÇÆÚ¶þ) ÍíÉÏ11:01
To: "klee-dev"<klee-***@imperial.ac.uk>;
Subject: Re: [klee-dev] 3 quick questions about KLEE
Post by Kirill Bogdanov
*Question 1. *
I am running integer version of KLEE and I am getting this error in my
What do you mean by the "integer version"?
Post by Kirill Bogdanov
computations. Can I rearrange my code to avoid this error ? Am I doing
something wrong here ?
I don't see this error, although I get a different one, in the CEX
caching code (which can be disabled with --use-cex-cache=false). I'm
using STP r940 (the one recommended on the website), what STP version
are you using? I suggest opening a bug report on GitHub.
Post by Kirill Bogdanov
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.
Take a look at
http://www.mail-archive.com/klee-dev%40imperial.ac.uk/msg00950.html

Best,
Cristian

_______________________________________________
klee-dev mailing list
klee-***@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
.
Daniel Liew
2014-06-02 16:06:14 UTC
Permalink
Post by 小、   ̄洁
Dear Cristian,
Sorry to disturb you for a question.
About the file assembly.ll, i donot know how to read it ,because i did
not know some rules. Where can i learn those rules which it needs to read
the assembly.ll in Klee-last.?
Please DO NOT hijack other people's thread. I have already answered
your question in the other thread you hijacked[1]

[1] http://mailman.ic.ac.uk/pipermail/klee-dev/2014-June/000729.html
小、   ̄洁
2014-06-03 00:14:42 UTC
Permalink
Thanks very much!



------------------ Ô­ÊŒÓÊŒþ ------------------
·¢ŒþÈË: "Daniel Liew"<***@imperial.ac.uk>;
·¢ËÍʱŒä: 2014Äê6ÔÂ3ÈÕ(ÐÇÆÚ¶þ) Á賿0:06
ÊÕŒþÈË: "С¡¢¡¡¡¡£þœà"<***@qq.com>;
³­ËÍ: "Cristian Cadar(2008 KLEE Author)"<***@imperial.ac.uk>; "klee-dev"<klee-***@imperial.ac.uk>;
Ö÷Ìâ: Re: [klee-dev] 3 quick questions about KLEE
Post by 小、   ̄洁
Dear Cristian,
Sorry to disturb you for a question.
About the file assembly.ll, i donot know how to read it ,because i did
not know some rules. Where can i learn those rules which it needs to read
the assembly.ll in Klee-last.?
Please DO NOT hijack other people's thread. I have already answered
your question in the other thread you hijacked[1]

[1] http://mailman.ic.ac.uk/pipermail/klee-dev/2014-June/000729.html
.

Loading...