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, 허희성 <gjgml...@naver.com
<mailto:gjgml...@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@imperial.ac.uk <mailto:klee-dev@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@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@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
