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

[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.

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