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

[Felix Rath]

Hi everyone,

our work on C++ is now complete enough to be used, so we opened PRs for 
KLEE that add C++ support. An overview of the PRs can be found in the PR 
that adds support for exception handling, which is 
https://github.com/klee/klee/pull/966.

If you want to try out the new C++ support, you can merge that PR 
locally, and build a libcxx which is compatible with KLEE. 
https://github.com/klee/klee/pull/965 contains a description of this 
process, but you will probably have to adjust it to your exact system.

We would be happy to hear about any feedback you have if you decide to 
give it a spin!

Best,
Felix

On 08/02/2018 11:06 AM, Felix Rath wrote:
> 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/
>
>
> _______________________________________________
> 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