about summary refs log tree commit diff homepage
path: root/runtime/POSIX
AgeCommit message (Collapse)Author
2018-10-08add support for klee-replay on OSXFrank Busse
* also adds klee-replay as dependency for systemtests
2018-09-29Changed code to create up to 100 properly-numbered symbolic arguments, and ↵Cristian Cadar
add a corresponding check.
2018-09-29Add checks for correct usage of the POSIX model, together with an associated ↵Cristian Cadar
test.
2018-09-10POSIX: Add invocation of klee_init_env into wrapper before calling mainMartin Nowack
To enable the POSIX support, the former implementation instrumented the main function and inserted a call to `klee_init_env` at the beginning. This has multiple disadvantages: * debugging information was not correctly propagated leaving the call to `klee_init_env` without debug information * the main function always required `int arg, char**` as part of the function definition of `main` Based on the new linking infrastructure, we can now add an additional wrapper `__klee_posix_wraper(int, char**)` that gets always called when POSIX support is enabled. It executes `klee_init_env` and after that calls the `main` function. Enabling POSIX support only requires the renaming of the user provided `main` into `__klee_posix_wrapped_main` in addition to linking.
2018-09-06runtime: fix memory error in canonicalize_file_nameFrank Busse
Fixes #46 and reverts #47. As stated in #46, the solution works for musl, glibc etc. However, the code in stub.c is executed by uclibc and uclibc doesn't allocate the target buffer in realpath. The memory error occured while running df for 10min with DFS.
2018-05-07Fixed utimes() behavior for symbolic files when the second argument is NULLyxliang01
2018-05-05Fix handling of errno if external functions are invokedMartin Nowack
If an external function in KLEE is invoked, it might update errno. Previously, the errno specific variable in a state was only updated if it was part of the executed instructions. That opened up a timeframe that increased the likelihood of errno being overwritten by another method call. This patch fixes two issues: * the errno of the KLEE process state is updated before the external function call allowing to detect changes to it later on * after the external call, the memory object of errno is directly updated with its new value, reducing the likelihood to be overwritten by another call Additional features: * Add support for `errno()` for Darwin as well. * Simplified errno handling in POSIX layer
2017-10-04Remove Autoconf/Makefile build system and adjust the TravisCIDan Liew
configuration, TravisCI scripts and Dockerfile build appropriately. There are a bunch of clean ups this enables but this commit doesn't attempt them. We can do that in future commits.
2017-08-09Fixed a bug causing KLEE to generate files with no permissions bits set. ↵Cristian Cadar
This was introduced when we added the --readable-posix-inputs option.
2017-03-28Merge pull request #616 from jirislaby/glibc_225Cristian Cadar
runtime: POSIX, make it compile with glibc 2.25
2017-03-20runtime: POSIX, check path prior dereferenceJiri Slaby
clang warns about check-after-use in POSIX runtime: runtime/POSIX/fd.c:573:17: warning: nonnull parameter 'path' will evaluate to 'true' on first r [-Wpointer-bool-conversion] (path ? __concretize_string(path) : NULL), ^~~~ ~ path is dereferenced in __get_sym_file before this check. So add a check to __get_sym_file and handle NULL appropriatelly by returning NULL too. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2017-03-15runtime: POSIX, make it compile with glibc 2.25Jiri Slaby
With glibc 2.25, we see: runtime/POSIX/stubs.c:243:14: error: conflicting types for 'gnu_dev_major' unsigned int gnu_dev_major(unsigned long long int __dev) __attribute__((weak)); ^ /usr/include/sys/sysmacros.h:79:27: note: previous definition is here __SYSMACROS_DEFINE_MAJOR (__SYSMACROS_IMPL_TEMPL) ^ Glibc 2.25 switched from ULL to dev_t for gnu_dev_major, gnu_dev_minor, and gnu_dev_makedev. Handle by using an appropriate type according to the glibc version. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2016-12-28Changed preferred permissions from 0622 to the more standard 0644.Cristian Cadar
2016-11-07Implement a CMake based build system for KLEE.Dan Liew
This is based off intial work by @jirislaby in #481. However it has been substantially modified. Notably it includes a separate build sytem to build the runtimes which is inspired by the old build system. The reason for doing this is because CMake is not well suited for building the runtime: * CMake is configured to use the host compiler, not the bitcode compiler. These are not the same thing. * Building the runtime using `add_custom_command()` is flawed because we can't automatically get transitive depencies (i.e. header file dependencies) unless the CMake generator is makefiles. (See `IMPLICIT_DEPENDS` of `add_custom_command()` in CMake). So for now we have a very simple build system for building the runtimes. In the future we can replace this with something more sophisticated if we need it. Support for all features of the old build system are implemented apart from recording the git revision and showing it in the output of `klee --help`. Another notable change is the CMake build system works much better with LLVM installs which don't ship with testing tools. The build system will download the sources for `FileCheck` and `not` tools if the corresponding binaries aren't available and will build them. However `lit` (availabe via `pip install lit`) and GTest must already be installed. Apart from better support for testing a significant advantage of the new CMake build system compared to the existing "Autoconf/Makefile" build system is that it is **not** coupled to LLVM's build system (unlike the existing build system). This means that LLVM's autoconf/Makefiles don't need to be installed somewhere on the system. Currently all tests pass. Support has been implemented in TravisCI and the Dockerfile for building with CMake. The existing "Autoconf/Makefile" build system has been left intact and so both build systems can coexist for a short while. We should remove the old build system as soon as possible though because it creates an unnecessary maintance burden.
2016-08-19Added -save-all-writes to klee_init_env help messageAndrea Mattavelli
2016-05-31Merge pull request #405 from ccadar/timesCristian Cadar
Fixed the stub for times() not to dereference a NULL pointer when cal…
2016-05-27Improved help message for POSIX environment options.Cristian Cadar
2016-05-27Fixed the stub for times() not to dereference a NULL pointer when call with ↵Cristian Cadar
a NULL argument. In respose of issue https://github.com/klee/klee/issues/399
2016-05-24Split creation of symbolic files and stdin in two distinct optionsAndrea Mattavelli
2016-03-05Fix SELinux signatures in runtimeLaszlo Szekeres
The SELinux function signatures have changed between version 2.2 and 2.3. In particular, the type of the "security context" parameter was changed from char * to const char *, with the following patch: SELinuxProject/selinux@9eb9c9327563014ad6a807814e7975424642d5b9. Recent Linux distributions (e.g. Ubuntu 15.10) ship with the updated version of libselinux. This change makes the SELinux runtime compatible with the newer versions of the library by replacing security_context_t with its original char * definition and defining it as const only if the installed library does so. Whether the system uses const char * types is detected with the configure script. Fixes klee/klee#303.
2015-06-03Added an option --readable-posix-inputs which is used to turn on/off the CEX ↵Cristian Cadar
preferences added in the POSIX model. Removed option --prefer-cex which controlled all CEX preferences.
2015-04-25Clean up the installation/building of the runtime libraries.Dan Liew
* We don't need to build the native versions so that is now disabled * We don't need to install (and hence build) the bytecode archive library versions of klee-libc or kleeRuntimeIntrinsic for new versions of LLVM right now (this is kind of messy).
2014-09-14Replace fprintf with klee_warnings for POSIX libMartin Nowack
2013-11-15Merge branch 'master' of https://github.com/ccadar/kleeCristian Cadar
2013-11-15Removed testing-env file. As for testing-dir that was removed in aCristian Cadar
prior patch, this is part of the CU experiments and doesn't really belong here.
2013-11-14Remove unused testing-dirMartin Nowack
2013-11-14Fix lseek and getdentsMartin Nowack
Wrong data types and casts led to wrong values on 64 bit machines with high values filedescriptor positions. Fixes DirConsistency and DirSeek test case
2013-11-02Fix build of POSIX file descriptor functionsMartin Nowack
Build Large File System functions for 32bit and 64bit correctly
2013-10-18stubs.c: cleanupFrank Busse
2013-10-18stubs.c: fix use of undeclared identifier PATH_MAXFrank Busse
2013-10-11Compile separate version of fd files for 3.2 as well.Cristian Cadar
2013-09-25Merge pull request #25 from paulmar/masterCristian Cadar
Added some of the common *at functions & others to the model. Obey --max-forks in switch statements.
2013-09-21Merge pull request #17 from MartinNowack/LLVM33Cristian Cadar
Make KLEE compile with LLVM 2.3.
2013-09-18Compile separate version of fd files only for LLVM 3.3 or higherMartin Nowack
2013-09-02Fixed multiple definitions of POSIX file functionsMartin Nowack
Function like stat() were defined for 32bit and 64bit version. Added compile time based selection of appropriate version using GNUC macros __x86_64__ and __ppc64__.
2013-08-29Added some of the common *at functions to the modelPaul Marinescu
2013-08-28Disable redefinition of functionsMartin Nowack
2012-10-24Patch by Dan Liew: " Added "sys/resource.h" include to POSIX stubCristian Cadar
methods. This fixes build problems (at least on my machine glibc 2.16.0-2) The __priority_which_t and __rlimit_resource_t data types which functions set_priority(), setrlimit() and setrlimit64() need are not defined in any of the headers the runtime/POSIX/stubs.c includes. It appears in the past the "sys/resource.h" was included by "sys/wait.h" but in the recent version of glibc I am using it is not. So to fix this I've added the include." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166554 91177308-0d34-0410-b5e6-96231b3b80d8
2010-06-28Applied Stefan Bucur's patch fromCristian Cadar
http://llvm.org/bugs/show_bug.cgi?id=6690. The patch adds specialized versions of klee_get_value for different types, fixing the previous klee_get_value function that sometimes truncated 64bit parameters to 32bit. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@107006 91177308-0d34-0410-b5e6-96231b3b80d8
2009-08-01Fixes for building runtime on linux x86-64.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@77825 91177308-0d34-0410-b5e6-96231b3b80d8
2009-08-01A few type fixes for libc functions, for 64-bit.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@77822 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-23Make klee_init_env print some usage instructions with --help.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72338 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-22Add "name" argument to klee_make_symbolic, and kill off klee_make_symbolic_name.Daniel Dunbar
- For compatibility we still accept 2 argument form of klee_make_symbolic, but this will go away eventually. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72265 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-21Initial KLEE checkin.Daniel Dunbar
- Lots more tweaks, documentation, and web page content is needed, but this should compile & work on OS X & Linux. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8