Hi Seungbeom,
On Fri, Jun 4, 2010 at 4:10 PM, Seungbeom Kim <sbkim at stanford.edu> wrote:
> Hi,
>
> I find that #include <iostream> alone causes KLEE to segfault
> at the end of the run, but not with --libc=klee or --libc=uclibc.
First, let me start by saying that trying to run KLEE on C++ code
isn't expected to work yet. To start with, it is really only going to
be viable if you compile the stdc++ library itself to LLVM bitcode and
link it in, and that is a non-trivial amount of work in and of itself.
Note that we have recently added a new C++ standard library to the
LLVM project. I hope that eventually this can form the foundation for
running KLEE against C++ code...
>
> $ cat header.cc
> #include <iostream>
>
> int main(int, char**)
> {
> }
>
> $ klee --libc=none header.o
> ...
> KLEE: done: total instructions = 39
> KLEE: done: completed paths = 1
> KLEE: done: generated tests = 1
> 0 ? klee 0x089896a8
> Segmentation fault (core dumped)
>
> $ klee --libc=uclibc header.o
> ...
> KLEE: done: total instructions = 11118
> KLEE: done: completed paths = 1
> KLEE: done: generated tests = 1
>
> Why does this happen? I suspect this has to do with the initialization
> of the standard stream objects (std::cout, etc.), but the klee libc
> or uclibc doesn't have anything to do with the C++ standard library,
> does it?
No, but when running without a support library what is going to happen
is that external calls to the C++ library will get made, which refer
to objects which are inside a KLEE state. If they pass an address or
something which doesn't really "exist" from the perspective of the
external process, bad things will happen.
> (Anyway, segfault means a bug in klee that should be fixed. =D)
Not really. Running KLEE without any support library generally only
works on closed programs (programs which make no external function
calls).
- Daniel
>
> The following program:
>
> #include <ostream>
> #include <iostream>
>
> int main(int, char**)
> {
> ? ? std::cout << "Hello, world!\n";
> }
>
> runs fine with any of the --libc={none,klee,uclibc} options, i.e.
> prints the string on the terminal successfully, though --libc=none
> causes the same segfault at the end of the run. This seems to imply
> that std::cout is somewhere defined and initialized, but I cannot
> see where or how.
>
> Thanks in advance for any ideas or comments.
>
> --
> Seungbeom Kim
> _______________________________________________
> klee-dev mailing list
> klee-dev at keeda.stanford.edu
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
>
