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"
>> ~/.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
On 10/30/2013 10:13 AM, Daniel Liew wrote:
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.
On 30 October 2013 01:00, Sandeep <[email protected]> wrote:
Hi Daniel,
Thanks for your comments.
Here are the specification:
Kernel Version
$uname -mrs
Linux 2.6.32-358.6.2.el6.x86_64 x86_64
Distribution
$lsb_release -a
LSB Version:
: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
On 10/29/2013 06:50 PM, Daniel Liew wrote:
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?
On 29 October 2013 22:38, Sandeep <[email protected]> wrote:
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
--
*With Thanks and Regards,*
Sandeep Dasgupta
Graduate ( PhD ) in Computer Science
Room : 1218 Siebel Center for Computer Science
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
