about summary refs log tree commit diff homepage
path: root/runtime
AgeCommit message (Collapse)Author
2024-02-08Explicitly build KLEE's exception handling runtime with C++11Martin Nowack
Currently, we assume C++11 support being used to by the tested software. This needs to change if newer C++ standards should be supported.
2024-02-08Fix `klee_eh_cxx.cpp` compiler errorMartin Nowack
2024-02-08Fix `klee-libc/memchr.c` compiler warningMartin Nowack
2024-02-08Add support for newer `libc++`; Simplify path detectionMartin Nowack
`libc++` include headers are now split between platform dependent and platform independent code. Before, only include files for the platform independent code were considered. Add support to automatically find platform dependent includes as well. Simplify the detection of libraries and paths. Instead of pointing to the `v1` directory, pointing to the include directory for `-DKLEE_LIBCXX_INCLUDE_PATH` is enough. Update build script to support this as well.
2023-06-11Rewrote has_permission in the POSIX runtime. We now only return with ↵Cristian Cadar
permission error a single time in symbolic execution mode. The rewrite also fixes a bug reported in #1230. Rewrote the FilePerm.c test accordingly.
2023-06-05config.h: include FSTATAT_PATH_ACCEPTS_NULLJulian Büning
This variable was introduced by d2f5906da4ae37a41ae257e5308d50e19689877b but not included in `config.h` before. As a result `#ifdef` would always fail. Moving the code is necessary to set the variable before `config.h` is created using `configure_file()` in CMakeLists.txt.
2023-04-14Modify name of variables in generated cvc files.ITWOI
2023-03-23fix unused variable warningDaniel Schemmel
2023-03-23Remove model_version from the POSIX runtime, as we have never used it.Cristian Cadar
2023-03-17Fix building of runtime library and klee-replayMartin Nowack
Former build system provided additional flags for building bitcode while they were not required, e.g. under BSD or MacOS.
2023-03-17[cmake] Use LLVM's CMake functionality onlyMartin Nowack
LLVM became more complex, use LLVM's CMake functionality directly instead of replicating this behaviour in KLEE's build system. Use the correct build flags provided by LLVM itself. This is influenced by the way LLVM is built in the first place. Remove older CMake support (< 3.0).
2023-03-16Fixed a bug in KLEE libc's implementation of strcmp: according to the C ↵Cristian Cadar
standard, characters should be compared as unsigned chars.
2022-09-14Add notes about how to keep in sync runtime with LLVM projectPavel
2022-09-14Add README to UBSan runtimePavel
2022-09-14Eliminate .undefined_behavior.err category and simplify testsPavel
2022-09-14Remove LLVM version < 9Pavel
2022-09-14Remove LLVM version < 6Pavel
2022-09-14Introduce separate categories for different kinds of undefined behaviorPavel
2022-09-14Support UBSan-enabled binariesPavel Yatcheniy
2022-08-19Corrected wrong usage of klee_report_error in __cxa_atexit handlerPavel
2022-07-07POSIX runtime: fstatat: check for nonnull path APIsFrank Busse
2022-06-27Define stat64 to be stat on MacOS. This fixes compilation on more recent ↵Cristian Cadar
macOS versions, where stat64 is not defined anymore.
2022-03-17remove LLVM < 6 from build/test scriptsFrank Busse
2022-01-04Use more precise version check for selecting swapoff() signature.Gleb Popov
2021-12-24Added correct signature for swapoff on FreeBSD (to solve recent CI failures)Cristian Cadar
2021-04-30posix runtime: add malloc checksFrank Busse
2021-02-22runtime/POSIX: fix failures with glibc-2.33Jiri Slaby
commit 8ed005daf0ab of glibc-2.33 (Remove stat wrapper functions, move them to exported symbols) removed renames of `__fxstat`, `__xstat`, and `__lxstat` to `__fxstat64`, `__xstat64`, and `__lxstat64`, respectively. But we relied on the renames to build `fd_64.c` properly. With glibc 2.33, we now see link failures of the POSIX runtime: error: Linking globals named '__xstat': symbol multiply defined! Rename the functions using `__REDIRECT_NTH` in the code as `__USE_FILE_OFFSET64` case (which we define at the top of the file by `#define _FILE_OFFSET_BITS 64`) did exactly that. Fixes #1384.
2020-12-23posix runtime: getcwd: check malloc and set errnoFrank Busse
* failing malloc was not handled before, now returns null/ENOMEM * when path is non-null and size is zero return null/EINVAL
2020-12-23klee-libc: simplify mempcpyFrank Busse
2020-12-23posix runtime: remove dead branchFrank Busse
2020-12-18fix cflags for runtime build typesJulian Büning
- `-DNDebug` -> `-DNDEBUG` - different flags for `Release{+Debug,}+Asserts` - `-g` is no longer part of common flags - `-D_DEBUG` is now only set for debug builds - removed unused `LIB_BC_FLAGS_{32,64}` - added example, architecture prefix for specific flags
2020-12-04Only build 32bit runtime libraries if supported by platformMartin Nowack
Automatically detect if 32bit bitcode files can be built. In this case, build runtime library with 32bit as well.
2020-12-04Declare mempcpy on macOS, to silence compiler warningsCristian Cadar
2020-11-09Added fortified library (for -D_FORTIFY_SOURCE), to be linked when uclibc is ↵Cristian Cadar
used.
2020-11-09Added fortified versions for the functions in the klee-libc libraryCristian Cadar
2020-11-09Since the runtime now contains fortified libc functions, it is important to ↵Cristian Cadar
compile it with -D_FORTIFY_SOURCE=0 to avoid infinite recursion.
2020-11-09Added fortified versions for the functions in the freestanding library.Cristian Cadar
2020-11-04Rename FreeStanding to Freestanding where appropriateMartin Nowack
2020-11-04[cmake] Add support to generate arbitrary runtime library configurationsMartin Nowack
Every runtime library can be build with multiple configurations. Replace the Makefile-based setup by cmake one. Currently, we generate 32bit and 64bit libraries simultaneously and can link against them.
2020-11-03fix: bcmp with n==0Alastair Reid
This was executing the loop when n==0 leading to an out of bound pointer error. Found while verifying Rust code that compares strings.
2020-10-30Call functions in __cxa_atexit in reverse orderTomas Jasek
2020-10-12address MartinNowack's remaining feedbackJulian Büning
2020-10-12Exception handling only for LLVM >= 8.0.0Julian Büning
2020-10-12fix cxa_exception include for older LLVM versionsJulian Büning
2020-10-12fix building klee-cxxabiJulian Büning
Co-authored-by: Felix Rath <felix.rath@comsys.rwth-aachen.de>
2020-10-12Implemented support for C++ ExceptionsFelix Rath
We implement the Itanium ABI unwinding base-API, and leave the C++-specific parts to libcxxabi. Co-authored-by: Lukas Wölfer <lukas.woelfer@rwth-aachen.de>
2020-10-06Ran clang-format on intrinsics.c and removed unneeded commentCristian Cadar
2020-10-06Added support for klee_open_merge and klee_close_merge in replay, together ↵Cristian Cadar
with a test case.
2020-08-28Definition of __cxa_thread_atexit_impl for the KLEE libc.Alastair Reid
This is a thread-local version of __cxa_atexit (but, in the absence of threads, it is sufficient to just call __cxa_atexit). The test is based on the existing test for atexit in test/Runtime/Uclibc/2008-03-04-libc-atexit-uses-dso-handle.c The motivation for adding this function is to support the Rust standard library that calls __cxa_thread_atexit_impl. This function is usually a weak symbol but, in KLEE, this behaves like a call to an unknown function and chaos ensues. Worse, it happens just as the program is cleanly shutting itself down, so programs that are cleanly exiting crash with the wrong message.
2020-08-07New intrinsic: klee_is_replayAlastair Reid
This instrinsic detects whether the program is being executed symbolically or concretely (i.e., using the libkleeRuntest library). The intended usage (illustrated in the test program) is to allow the test program to display the input values by invoking any libraries it wants to. This is especially valuable if you are constructing complex, structured values and for languages like Rust (or C++) that have rich libraries and print libraries. For example, you might pick a symbolic value N with the assumption "0 <= N < 10" and then pick N symbolic values and write them to an array. The resulting ktest file is a bit hard to understand compared with the output of the standard print function in Rust/C++.