about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2020-09-30tests: support .test and introduce %klee-statsFrank Busse
2020-09-30Add check if KLEE is installedMartin Nowack
2020-09-30Use LLVM 6.0 for now on macOSMartin Nowack
C++ static destructors are currently not supported for newer LLVM version. Keep older LLVM version until issue is fixed.
2020-09-30[CMake][Z3] Check if function `Z3_get_error_msg` needs `context` using C++Martin Nowack
Linking with Z3 might fail if Z3 is built with UBSan as parts of Z3 are written in C++. Check explicitly with a C++ compiler.
2020-09-30Update Dockerfile to use LLVM 9.0 and newer Ubuntu versionMartin Nowack
2020-09-30Remove shebang from includeMartin Nowack
2020-09-30Fix LLVM 4.0 build patchMartin Nowack
2020-09-30Fix docker ID handling for sqliteMartin Nowack
2020-09-30Fix check if sqlite is installed under ubuntu as a systems packageMartin Nowack
2020-09-30Fix check if LLVM is installedMartin Nowack
2020-09-30Reduce compile time and size for LLVM buildMartin Nowack
* Just target x86 as architecture * do not build tests for clang * use optimized tablegen * only build required tools and libraries that are needed by KLEE
2020-09-30Reduce the size of the libcxx imageMartin Nowack
* re-use an existing LLVM directory if possible * only export the bitcode files
2020-09-30Remove explicit dependency on llvm and sanitizerMartin Nowack
Clang is just a compiler and can be provided by system-specific packages.
2020-09-30Fix detection of installed clangMartin Nowack
Any clang is fine as long as it is the right version. The current assumption is that it is suffixed with version.
2020-09-30Do not use `-lubsan` and `-fuse-ld=gold` for UBSan linkingMartin Nowack
These arguments are not required and let the link process fail. Instead, clang(++) should be used as a linker and it will take care of linking with the correct libraries.
2020-09-30Delete Docker instance after system detection ranMartin Nowack
Don't keep the docker instance for detecting the system around to avoid stale terminated containers.
2020-09-30Disable libc++ for LLVM 3.8 Travis CI targetMartin Nowack
The build support for libc++ for LLVM 3.8 is broken. It's not worth fixing.
2020-09-30Set default LLVM version to 9.0Martin Nowack
Use newer LLVM version 9.0 instead of 6.0. Update to newer Ubuntu base image.
2020-09-30Replace travis container build script with python-based versionMartin Nowack
2020-09-26Replace llvm::CallSite with llvm::CallBase on LLVM 8+Lukas Zaoral
This is in preparation for LLVM 11 as the llvm:CallSite class has been removed.
2020-09-25Add Cirrus CI statusCristian Cadar
2020-09-21Added a PR template, with a checklist documenting the most frequent issues ↵Cristian Cadar
we have encountered
2020-09-17Add test for klee-zestiTimotej Kapus
2020-09-17[gen-bout] Support multiple symbolic filesTimotej Kapus
2020-09-17Add klee-zesti a ZESTI like wrapper scriptTimotej Kapus
klee-zesti takes concrete arguments, files and stdin of the program under tests converts them to a seed and then runs klee with that seed. This emulates the interface of ZESTI.
2020-09-05Fix codecov uploadMartin Nowack
Argument `-y` has been removed from the upload script. https://github.com/codecov/codecov-bash/commit/c2f935a0dd0590d20296e95a759782e32b311b34 But `.codecov.yml` is now supported
2020-09-05Remove secure varsCristian Cadar
2020-09-04Update homebrew cacheMartin Nowack
2020-09-04Remove caching of homebrew-built packagesMartin Nowack
The new build script doesn't use that facility anymore. Remove it to avoid interfirence with ccache.
2020-09-04Use homebrew packages provided by TravisMartin Nowack
Recently, Homebrew packages can be installed via `.travis.yml`. Use this functionality instead of calling brew directly. Hopefully works around the build issue.
2020-09-04CirrusCI: Switch FreeBSD 11.3 to 11.4, remove old hack.Gleb Popov
2020-09-03Guard process-tree compression with a command-line switchSebastian Poeplau
2020-09-03Fix PTree::remove to clean the tree properlySebastian Poeplau
The previous version left unnecessary intermediate nodes behind, sometimes leading to very long paths in the tree.
2020-09-03Change the way bash is upgraded on macOS.Cristian Cadar
2020-09-02More robust handling of unknown intrinsicsAlastair Reid
- If an unknown intrinsic appears in the bitcode file, it is reported but execution can proceed. - If an unknown intrinsic is encountered during execution of some path, - the intrinsic is reported - this path is treated as an error - execution of other paths can proceed To be more precise, there is a list of "known unknown intrinsics". Intrinsics not on this list will prevent execution.
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-23klee-stats: check for a run.stats file in the klee-out directory, to prevent ↵Jordy Ruiz
outputting wrong data. When KLEE crashes, it produces an empty info file, so it is not enough to check for the existence of an info file. Previously, table columns would mismatch and return data labeled with the wrong directory names.
2020-08-19DiscretePDF: use IDs instead of pointers (see PR #739)Frank Busse
2020-08-14Updated README.md links from travis-ci.org to travis-ci.comCristian Cadar
2020-08-07Tweak LLVM version string parser: support rustAlastair Reid
This change allows KLEE to be configured to use the LLVM version that comes with the Rust compiler instead of a standard version. e.g., one might configure with -DLLVM_CONFIG_BINARY=${RUST_SRC}/build/x86_64-unknown-linux-gnu/llvm/bin/llvm-config For which typical output might be 10.0.1-rust-dev
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++.
2020-07-30[unittests] use static PTree::remove method in SearcherTestFrank Busse
2020-07-30introduce --rng-initial-seed=<unsigned>Frank Busse
* move global theRNG into Executor * pass theRNG via ctor to searchers * remove some type warnings from RNG.cpp Fixes #1023.
2020-07-29remove holes in Instruction-/FunctionInfoTable, add documentationFrank Busse
2020-07-01Clean-up and add documentationMartin Nowack
2020-07-01Remove state contructor with constraintsMartin Nowack
This constructor has been a hack and was wrongly used, use ConstraintManager instead. Allow copy-constructing states only via `ExecutionState::branch()` call.
2020-07-01Use constraint sets and separate metadata for timing solver invocationMartin Nowack
Decouple ExecutionState from TimingSolver Instead of providing an execution state to the timing solver use a set of constraints and an additional object for metadata. Fixes: * correct accounting of metadata to a specific state * accounting of all solver invocations (e.g. solver-getRange was not accounted) * allows to invoke the solver without a state (avoids costly copying of states/constraints)
2020-07-01Use `unique_ptr` for solver in timing solverMartin Nowack
2020-07-01Separate constraint set and constraint managerMartin Nowack
2020-07-01Move constraint implementation from header to cpp filesMartin Nowack
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-25 11:30:53 +0000