[klee-dev] klee seems to crash when testing a simple program
Tomasz Kuchta
t.kuchta at imperial.ac.uk
Wed Oct 30 16:25:05 GMT 2013
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
On 30/10/13 15:46, Sandeep wrote:
> 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 <sdasgup3 at illinois.edu> 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 <sdasgup3 at illinois.edu> 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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
More information about the klee-dev
mailing list