[klee-dev] klee seems to crash when testing a simple program

[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"
         >> ~/.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
-------------- next part --------------
HTML attachment scrubbed and removed