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, 허희성 <[email protected]
<mailto:[email protected]>> 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
[email protected] <mailto:[email protected]>
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
_______________________________________________
klee-dev mailing list
[email protected]
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
[email protected]
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
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
