klee seems to crash when testing a simple program

Discussion:

陈厅

2013-02-21 18:02:15 UTC

Hi

I use klee to test a simple program, but klee seems to crash. Who knows the reason? The tested program is shown below:

int pointer_test(int x, int y) {
int a[4] = {0};
a[0] = x;
a[1] = 0;
a[2] = 1;
a[3] = 2;
if(a[x] == a[y] + 2)
return 1;
return 2;
}
int main() {
int a, b;
klee_make_symbolic(&a, sizeof(a), "a");
klee_make_symbolic(&b, sizeof(b), "b");
return pointer_test(a, b);
}

The program is in a file named pointer.c. So the command line to compile the program is:
llvm-gcc --emit-llvm -c -g pointer.c
I use this command to run this program:
klee pointer.o

But an error happened, below is the output in terminal:

KLEE: output directory = "klee-out-1"
klee: /home/ting/work/klee/include/klee/Expr.h:391: static klee::ref<klee::ConstantExpr> klee::ConstantExpr::create(uint64_t, klee::Expr::Width): Assertion `v == bits64::truncateToNBits(v, w) && "invalid constant"' failed.
0 klee 0x0000000000d5f39f
1 klee 0x0000000000d5f8a9
2 libpthread.so.0 0x00002b2c542edcb0
3 libc.so.6 0x00002b2c54f49425 gsignal + 53
4 libc.so.6 0x00002b2c54f4cb8b abort + 379
5 libc.so.6 0x00002b2c54f420ee
6 libc.so.6 0x00002b2c54f42192
7 klee 0x0000000000540a26
8 klee 0x00000000005a9898 klee::AddressSpace::resolve(klee::ExecutionState&, klee::TimingSolver*, klee::ref<klee::Expr>, std::vector<std::pair<klee::MemoryObject const*, klee::ObjectState const*>, std::allocator<std::pair<klee::MemoryObject const*, klee::ObjectState const*> > >&, unsigned int, double) + 4632
9 klee 0x000000000057fcfa klee::Executor::executeMemoryOperation(klee::ExecutionState&, bool, klee::ref<klee::Expr>, klee::ref<klee::Expr>, klee::KInstruction*) + 1930
10 klee 0x0000000000584fee klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 6910
11 klee 0x000000000058936b klee::Executor::run(klee::ExecutionState&) + 1883
12 klee 0x0000000000589de6 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1846
13 klee 0x00000000005611f7 main + 10071
14 libc.so.6 0x00002b2c54f3476d __libc_start_main + 237
15 klee 0x000000000056d3d1
Abandon(core dumped)

Thanks very much

Ting Chen

Chris Hobbs

2013-02-21 18:13:34 UTC

Permalink

Works OK for me. I copied your program and went through the same steps
as you. The result was:

KLEE: output directory = "klee-out-0"
KLEE: ERROR: /home/chobbs/tmp/tryit.c:7: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /home/chobbs/tmp/tryit.c:7: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location

KLEE: done: total instructions = 3835
KLEE: done: completed paths = 288
KLEE: done: generated tests = 273

I'm using

Low Level Virtual Machine (http://llvm.org/):
llvm version 2.7
Optimized build with assertions.
Built May 24 2011 (18:07:32).
Host: i386-pc-linux-gnu
Host CPU: i686

Registered Targets:
x86 - 32-bit X86: Pentium-Pro and above
x86-64 - 64-bit X86: EM64T and AMD64

Cheers

Chris Hobbs
QNX Software Systems

Post by éå
Hi
I use klee to test a simple program, but klee seems to crash. Who
int pointer_test(int x, int y) {
int a[4] = {0};
a[0] = x;
a[1] = 0;
a[2] = 1;
a[3] = 2;
if(a[x] == a[y] + 2)
return 1;
return 2;
}
int main() {
int a, b;
klee_make_symbolic(&a, sizeof(a), "a");
klee_make_symbolic(&b, sizeof(b), "b");
return pointer_test(a, b);
}
llvm-gcc --emit-llvm -c -g pointer.c
klee pointer.o
KLEE: output directory = "klee-out-1"
klee: /home/ting/work/klee/include/klee/Expr.h:391: static
klee::ref<klee::ConstantExpr> klee::ConstantExpr::create(uint64_t,
klee::Expr::Width): Assertion `v == bits64::truncateToNBits(v, w) &&
"invalid constant"' failed.
0 klee 0x0000000000d5f39f
1 klee 0x0000000000d5f8a9
2 libpthread.so.0 0x00002b2c542edcb0
3 libc.so.6 0x00002b2c54f49425 gsignal + 53
4 libc.so.6 0x00002b2c54f4cb8b abort + 379
5 libc.so.6 0x 00002b2c54f420ee
6 libc.so.6 0x00002b2c54f42192
7 klee 0x0000000000540a26
8 klee 0x00000000005a9898
klee::AddressSpace::resolve(klee::ExecutionState&,
klee::TimingSolver*, klee::ref<klee::Expr>,
std::vector<std::pair<klee::MemoryObject const*, klee::ObjectState
const*>, std::allocator<std::pair<klee::MemoryObject const*,
klee::ObjectState const*> > >&, unsigned int, double) + 4632
9 klee 0x000000000057fcfa
klee::Executor::executeMemoryOperation(klee::ExecutionState&, bool,
klee::ref<klee::Expr>, klee::ref<klee::Expr>, klee::KInstruction*) + 1930
10 klee 0x0000000000584fee
klee::Executor::executeInstruction(klee::ExecutionState&,
klee::KInstruction*) + 6910
11 klee 0x000000000058936b
klee::Executor::run(klee::ExecutionState&) + 1883
12 klee 0x0000000000589de6
klee::Executor::runFunctionAsMain(llvm::Function*, int, char**,
char**) + 1846
13 klee 0x00000000005611f7 main + 10071
14 libc.so.6 0x00002b2c54f3476d __libc_start_main + 237
15 klee 0x000000000056d3d1
Abandon(core dumped)
Thanks very much
Ting Chen
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Sandeep

2013-10-29 22:38:40 UTC

Permalink

I am still getting the error that /Ting Chen/ reported. Also the llvm
build version that I am using is LLVM build 2.9 as prescribed at

http://thread.gmane.org/gmane.comp.compilers.llvm.klee/923

Please let me know what is the actual issue.

--
*With Thanks and Regards,*
Sandeep Dasgupta
Graduate ( PhD ) in Computer Science
Room : 1218 Siebel Center for Computer Science

Daniel Liew

2013-10-29 23:50:36 UTC

Permalink

I don't remember seeing this before.

I'm afraid I can't reproduce the issue on my machine so there's
nothing I can do.

If you really want to you can add the issue to the issue tracker (
https://github.com/ccadar/klee/issues?page=1&state=open ) but if no
developers can reproduce the issue there's not much we can do.

As you can see from the error message the problem is in
ConstantExpr::create() . Whatever value is being passed is being is
either too big to be represented by the requested width OR there is a
bug in Bits64::truncateToNBits().

Get in there with a debugger (e.g. gdb) and find out what values are
causing the assertion failure.

Out of curiosity...

What architecture are you using (hardware and software wise - i.e.
32-bit or 64-bit)? I'm using 64-bit. I have a sneaking suspicion
you're using 32-bit
What distro are you using?
What kernel version are you using?

I am still getting the error that Ting Chen reported. Also the llvm build
version that I am using is LLVM build 2.9 as prescribed at
http://thread.gmane.org/gmane.comp.compilers.llvm.klee/923
Please let me know what is the actual issue.
--
With Thanks and Regards,
Sandeep Dasgupta
Graduate ( PhD ) in Computer Science
Room : 1218 Siebel Center for Computer Science

Daniel Liew

2013-10-30 15:13:36 UTC

Permalink

Please make sure you use "reply-all" to ensure the mailing list sees
your response as well as me.

Oh so you are running 64-bit then, so that rules that possibility out.
I took your even simpler program and executed that and I still cannot
reproduce your issue. That is a very very old kernel you are running
so I guess you might be running some other old stuff too. What
compiler did you use to compiler KLEE? My guess is gcc, if so then run

$ gcc --version to get your version information.

You are going to need debug KLEE yourself because I cannot reproduce
the issue. I'm assuming the error is still in
ConstantExpr::create(uint64_t v, Width w) , so as a starting point do
the following.

$ gdb klee
(gdb) run your-bitcodefile.bc

... At some point you'll get the assertion failure

then use commands "bt", "up", "down" or "frame" to navigate the stack
frame until you get to ConstantExpr::create()

then you can run "info args" to see what arguments were passed. That
will be a good starting point for debugging.

Hope that helps,
Dan.

For the benefit of those on the mailing list Sandeep's response is
shown in full below.

Hi Daniel,
Thanks for your comments.
Kernel Version
$uname -mrs
Linux 2.6.32-358.6.2.el6.x86_64 x86_64
Distribution
$lsb_release -a
:base-4.0-amd64:base-4.0-noarch:core-4.0-amd64:core-4.0-noarch:graphics-4.0-amd64:graphics-4.0-noarch:printing-4.0-amd64:printing-4.0-noarch
Distributor ID: Scientific
Description: Scientific Linux release 6.4 (Carbon)
Release: 6.4
Codename: Carbon
Just to let you know the simplest code with which I am getting the error is
int main(void) {
int i,t, a[4] = {1,0,5,2};
klee_make_symbolic(&i, sizeof(i), "my_i");
t = a[i];
}
Thanks
Sandeep
I don't remember seeing this before.
I'm afraid I can't reproduce the issue on my machine so there's
nothing I can do.
If you really want to you can add the issue to the issue tracker (
https://github.com/ccadar/klee/issues?page=1&state=open ) but if no
developers can reproduce the issue there's not much we can do.
As you can see from the error message the problem is in
ConstantExpr::create() . Whatever value is being passed is being is
either too big to be represented by the requested width OR there is a
bug in Bits64::truncateToNBits().
Get in there with a debugger (e.g. gdb) and find out what values are
causing the assertion failure.
Out of curiosity...
What architecture are you using (hardware and software wise - i.e.
32-bit or 64-bit)? I'm using 64-bit. I have a sneaking suspicion
you're using 32-bit
What distro are you using?
What kernel version are you using?
I am still getting the error that Ting Chen reported. Also the llvm build
version that I am using is LLVM build 2.9 as prescribed at
http://thread.gmane.org/gmane.comp.compilers.llvm.klee/923
Please let me know what is the actual issue.
--
With Thanks and Regards,
Sandeep Dasgupta
Graduate ( PhD ) in Computer Science
Room : 1218 Siebel Center for Computer Science
--
With Thanks and Regards,
Sandeep Dasgupta
Graduate ( PhD ) in Computer Science
Room : 1218 Siebel Center for Computer Science

Sandeep

2013-10-30 15:46:38 UTC

Permalink

Thanks Daniel for the valuable input on debugging. I really appreciate that.
Surely I have to debug the klee.

$gcc --version
gcc (GCC) 4.4.7 20120313 (Red Hat 4.4.7-3)
Copyright (C) 2010 Free Software Foundation, Inc.
This is free software; see the source for copying conditions. There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.

Just an FYI: This is how I build the klee

mkdir work
cd work

wget http://llvm.org/releases/2.9/llvm-gcc-4.2-2.9-i686-linux.tgz
tar zxfv llvm-gcc-4.2-2.9-i686-linux.tgz
echo "export PATH=\$PATH:~/work/llvm-gcc-4.2-2.9-i686-linux/bin"

Post by Daniel Liew

~/.bashrc

echo "export PATH=\$PATH:~/work/klee/Release+Asserts/bin" >>
~/.bashrc
echo "export C_INCLUDE_PATH=/usr/include/i386-linux-gnu" >>
~/.bashrc
source ~/.bashrc

curl -O http://llvm.org/releases/2.9/llvm-2.9.tgz
tar zxvf llvm-2.9.tgz
cd llvm-2.9
./configure --enable-optimized --enable-assertions
make -j $(grep -c processor /proc/cpuinfo)

cd ..

svn co -r 940
https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp
stp
cd stp
./scripts/configure
--with-prefix=/home/$(whoami)/work/stp_install --with-cryptominisat2
make -j $(grep -c processor /proc/cpuinfo) OPTIMIZE=-O2
CFLAGS_M32= install

cd ..

svn co http://llvm.org/svn/llvm-project/klee/trunk klee
cd klee
./configure --with-llvm=/home/$(whoami)/work/llvm-2.9
--with-stp=/home/$(whoami)/work/stp_install
make -j $(grep -c processor /proc/cpuinfo) ENABLE_OPTIMIZED=1
make unittests

Post by Daniel Liew
Please make sure you use "reply-all" to ensure the mailing list sees
your response as well as me.
Oh so you are running 64-bit then, so that rules that possibility out.
I took your even simpler program and executed that and I still cannot
reproduce your issue. That is a very very old kernel you are running
so I guess you might be running some other old stuff too. What
compiler did you use to compiler KLEE? My guess is gcc, if so then run
$ gcc --version to get your version information.
You are going to need debug KLEE yourself because I cannot reproduce
the issue. I'm assuming the error is still in
ConstantExpr::create(uint64_t v, Width w) , so as a starting point do
the following.
$ gdb klee
(gdb) run your-bitcodefile.bc
... At some point you'll get the assertion failure
then use commands "bt", "up", "down" or "frame" to navigate the stack
frame until you get to ConstantExpr::create()
then you can run "info args" to see what arguments were passed. That
will be a good starting point for debugging.
Hope that helps,
Dan.
For the benefit of those on the mailing list Sandeep's response is
shown in full below.

--
*With Thanks and Regards,*
Sandeep Dasgupta
Graduate ( PhD ) in Computer Science
Room : 1218 Siebel Center for Computer Science

Tomasz Kuchta

2013-10-30 16:25:05 UTC

Permalink

Hi Sandeep,

I'm not sure if that could help, but I would also try with the 64 bit
version of llvm-gcc. In can be found at
http://llvm.org/releases/2.9/llvm-gcc4.2-2.9-x86_64-linux.tar.bz2
for LLVM 2.9.

Hope that helps,
Best regards,
Tomek

Post by Sandeep
Thanks Daniel for the valuable input on debugging. I really appreciate that.
Surely I have to debug the klee.
$gcc --version
gcc (GCC) 4.4.7 20120313 (Red Hat 4.4.7-3)
Copyright (C) 2010 Free Software Foundation, Inc.
This is free software; see the source for copying conditions. There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
Just an FYI: This is how I build the klee
mkdir work
cd work
wget http://llvm.org/releases/2.9/llvm-gcc-4.2-2.9-i686-linux.tgz
tar zxfv llvm-gcc-4.2-2.9-i686-linux.tgz
echo "export PATH=\$PATH:~/work/llvm-gcc-4.2-2.9-i686-linux/bin"

Post by Daniel Liew

~/.bashrc

echo "export PATH=\$PATH:~/work/klee/Release+Asserts/bin" >>
~/.bashrc
echo "export C_INCLUDE_PATH=/usr/include/i386-linux-gnu" >>
~/.bashrc
source ~/.bashrc
curl -O http://llvm.org/releases/2.9/llvm-2.9.tgz
tar zxvf llvm-2.9.tgz
cd llvm-2.9
./configure --enable-optimized --enable-assertions
make -j $(grep -c processor /proc/cpuinfo)
cd ..
svn co -r 940
https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp
stp
cd stp
./scripts/configure
--with-prefix=/home/$(whoami)/work/stp_install --with-cryptominisat2
make -j $(grep -c processor /proc/cpuinfo) OPTIMIZE=-O2
CFLAGS_M32= install
cd ..
svn co http://llvm.org/svn/llvm-project/klee/trunk klee
cd klee
./configure --with-llvm=/home/$(whoami)/work/llvm-2.9
--with-stp=/home/$(whoami)/work/stp_install
make -j $(grep -c processor /proc/cpuinfo) ENABLE_OPTIMIZED=1
make unittests

--
*With Thanks and Regards,*
Sandeep Dasgupta
Graduate ( PhD ) in Computer Science
Room : 1218 Siebel Center for Computer Science
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Hongxu Chen

2013-10-30 03:11:20 UTC

Permalink

I feel strange that although klee runs ok on my machine it generates a
different result from yours(I run it for several times, and the statistics
are the same).

KLEE: done: total instructions = 1222
KLEE: done: completed paths = 92
KLEE: done: generated tests = 84

Also, there are 2 memory error ktests generated.

Here I used the simple command line "klee test.bc" without any additional
options(also, without any optimizations when using llvm-gcc generating llvm
IR). When using "klee -optimize test.bc", there are still 2 memory
errors(the other statistics are changed since llvm IR is different).

So is there any inconsistency?

I also notice that there is something weired when change "int main(void)"
to "int main(int argc, char** argv)": KLEE will run *much slower* on my
machine for this case. Is it because the search strategy is changed?

Best Regards,
Hongxu Chen

Works OK for me. I copied your program and went through the same steps as
KLEE: output directory = "klee-out-0"
KLEE: ERROR: /home/chobbs/tmp/tryit.c:7: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /home/chobbs/tmp/tryit.c:7: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: done: total instructions = 3835
KLEE: done: completed paths = 288
KLEE: done: generated tests = 273
I'm using
llvm version 2.7
Optimized build with assertions.
Built May 24 2011 (18:07:32).
Host: i386-pc-linux-gnu
Host CPU: i686
x86 - 32-bit X86: Pentium-Pro and above
x86-64 - 64-bit X86: EM64T and AMD64
Cheers
Chris Hobbs
QNX Software Systems
Hi
I use klee to test a simple program, but klee seems to crash. Who
int pointer_test(int x, int y) {
int a[4] = {0};
a[0] = x;
a[1] = 0;
a[2] = 1;
a[3] = 2;
if(a[x] == a[y] + 2)
return 1;
return 2;
}
int main() {
int a, b;
klee_make_symbolic(&a, sizeof(a), "a");
klee_make_symbolic(&b, sizeof(b), "b");
return pointer_test(a, b);
}
llvm-gcc --emit-llvm -c -g pointer.c
klee pointer.o
KLEE: output directory = "klee-out-1"
klee: /home/ting/work/klee/include/klee/Expr.h:391: static
klee::ref<klee::ConstantExpr> klee::ConstantExpr::create(uint64_t,
klee::Expr::Width): Assertion `v == bits64::truncateToNBits(v, w) &&
"invalid constant"' failed.
0 klee 0x0000000000d5f39f
1 klee 0x0000000000d5f8a9
2 libpthread.so.0 0x00002b2c542edcb0
3 libc.so.6 0x00002b2c54f49425 gsignal + 53
4 libc.so.6 0x00002b2c54f4cb8b abort + 379
5 libc.so.6 0x 00002b2c54f420ee
6 libc.so.6 0x00002b2c54f42192
7 klee 0x0000000000540a26
8 klee 0x00000000005a9898
klee::AddressSpace::resolve(klee::ExecutionState&, klee::TimingSolver*,
klee::ref<klee::Expr>, std::vector<std::pair<klee::MemoryObject const*,
klee::ObjectState const*>, std::allocator<std::pair<klee::MemoryObject
const*, klee::ObjectState const*> > >&, unsigned int, double) + 4632
9 klee 0x000000000057fcfa
klee::Executor::executeMemoryOperation(klee::ExecutionState&, bool,
klee::ref<klee::Expr>, klee::ref<klee::Expr>, klee::KInstruction*) + 1930
10 klee 0x0000000000584fee
klee::Executor::executeInstruction(klee::ExecutionState&,
klee::KInstruction*) + 6910
**11 klee 0x000000000058936b
klee::Executor::run(klee::ExecutionState&) + 1883**
12 klee 0x0000000000589de6
klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) +
1846
13 klee 0x00000000005611f7 main + 10071
14 libc.so.6 0x00002b2c54f3476d __libc_start_main + 237
15 klee 0x000000000056d3d1
Abandon(core dumped)
Thanks very much
Ting Chen
_______________________________________________
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev