[klee-dev] Does klee support c++?

[Felix Rath]

Hi Sang and everyone else,

yes, you are right, KLEE works on LLVM bitcode, so it can theoretically 
run any program compiled to this bitcode. However, in practice, not 
every feature available in LLVM bitcode is implemented in KLEE; A major 
example is exception handling, which is often present in LLVM bitcode 
compiled from C++. Additionally, the C++ standard library (libc++ is the 
one that is part of LLVM) makes it necessary to model some functions in 
KLEE. This had also been done for C programs, so KLEE can run programs 
relying on a libc (e.g., uclibc). Some (simple) C++ programs which don't 
use these features can already be executed in KLEE, but most mainstream 
software written in C++ relies on these "additional" features (such as, 
e.g., 'cout', as you have noticed).

We have been working on C++ support for KLEE (since we want to be able 
to analyze C++ programs), and it should be finished soon-ish. Here is a 
bug we found when executing z3 in our version of KLEE (with C++ 
support): https://github.com/Z3Prover/z3/pull/1613 so you can see that 
our implementation is already working, and that KLEE can run on "real" 
C++ programs. We plan to open-source our work.

A large part of supporting C++ programs in KLEE is integrating the 
libc++ into the build- and linking-process of target programs. We are 
currently improving the way this is done, to minimize friction and to 
have a stable way to do so. Once this is done we will open PRs on the 
KLEE github repository, and at that point you will already be able to 
try out the C++ support by pulling the PRs on your machine. We currently 
expect to open the PRs in the next 1-2 weeks (but can't really make 
guarantees).

I hope this made the issue clearer!

Best,
Felix

On 07/31/2018 01:39 AM, Sang Phan wrote:
> I tried KLEE with a couple of C++ programs before without any problem.
>
> Did you run KLEE with the -posix-runtime option?
>
> As I understand, KLEE works on LLVM bitcode, so it doesn't care what 
> is in the front-end, as long as they can be compiled.
>
> Sang
>
> On Sun, Jul 29, 2018 at 9:25 PM, 허희성 <gjgmltjd at naver.com 
> <mailto:gjgmltjd at naver.com>> wrote:
>
>     Hello all,
>
>     I tried to run a very simple c++ program, but immediately got
>     segmentation fault message.
>
>     #include <iostream>
>
>     #include <klee/klee.h>
>
>     using namespace std;
>
>     int main(void)
>
>     {
>
>        int a;
>
>        klee_make_symbolic(&a, sizeof(a), "a");
>
>        if (a == 1)
>
>           cout << "a ==1";
>
>        else
>
>           cout << "a != 1"
>
>        return 0;
>
>     }
>
>     Result:
>
>     clang -x c++ -c -g -emit-llvm main.cpp
>
>
>       ... some undefined reference library function msg ...
>
>
>     KLEE: ERROR: .../main.cpp:18 failed external call:
>     _ZStlsISt11char_traitsIcEERSt13basic_ostreamIcT_ES5_PKc
>
>     KLEE: NOTE: now ignoring this error at this location
>
>     Segmentation fault(core dumped)
>
>
>     I found that seg fault is occured when klee handle cout function.
>
>     When I replaced cout function to printf (I added stdio.h header),
>     klee made 2 path but still got segfaulted.
>
>     GDB core debugging result:
>
>     #0 ... in ??()
>
>     #1 in __run_exit_handlers (...) at exit.c:82
>
>     #2 in __ GI_exit (...) at exit.c:104 <tel:104>:
>
>     #3 in __libc_start_main (...)
>
>     #4 in __start()
>
>     It seems that klee doesn't support c++ properly.
>
>     If I remove iostream header & cout function from source code,
>     everything is fine.
>
>
>     _______________________________________________
>     klee-dev mailing list
>     klee-dev at imperial.ac.uk <mailto:klee-dev at imperial.ac.uk>
>     https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>     <https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
>
>
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

-- 
Felix Rath, M.Sc., Ph.D. Student
Chair of Communication and Distributed Systems
RWTH Aachen University, Germany
tel: +49 241 80 21418
web: https://www.comsys.rwth-aachen.de/team/felix-rath/

-------------- next part --------------
HTML attachment scrubbed and removed