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

Thu Aug 16 10:01:48 BST 2018

Hi Felix,

That's a very useful contribution, thanks for submitting those PRs!  We 
will try to review them in the next few weeks.

Best,
Cristian

On 15/08/18 17:04, Felix Rath wrote:
> 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/
> 
> 
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
> 