KLEE Symbolic Execution Engine

Last update: Dec 24, 2022

Related tags

Overview

KLEE Symbolic Virtual Machine

KLEE is a symbolic virtual machine built on top of the LLVM compiler infrastructure. Currently, there are two primary components:

The core symbolic virtual machine engine; this is responsible for executing LLVM bitcode modules with support for symbolic values. This is comprised of the code in lib/.
A POSIX/Linux emulation layer oriented towards supporting uClibc, with additional support for making parts of the operating system environment symbolic.

Additionally, there is a simple library for replaying computed inputs on native code (for closed programs). There is also a more complicated infrastructure for replaying the inputs generated for the POSIX/Linux emulation layer, which handles running native programs in an environment that matches a computed test input, including setting up files, pipes, environment variables, and passing command line arguments.

For further information, see the webpage.

Comments

Add support for exception handling (C++ 6/6)
This PR is part of a chain of PRs that adds C++-support to KLEE. This is the final (and 'main') PR of the chain, the other PRs are:

[x] ~~#961 - Adds basic support for memalign~~ (dropped; see the PR for infos; new PR: #988)

[x] ~~#962 - Adds support for newlocale and freelocale (e.g., required for cout).~~ (will be done in uclibc; see the PR for infos)

[x] #963 - ~~Implements some~~ Enables lowering of atomic LLVM instructions.

[x] #964 - Adds a hack to support landingpad instructions.

[x] ~~#965 - Adds capabilities to KLEE and KLEE's build system to allow linking against a libcxx.~~ Implemented in #1056.

[ ] This PR (#966) - Adds support for exception handling.

These PRs form a chain, therefore they need to be merged from the top (e.g., top one first, while this PR can only be merged last). If required, there is some room to change the merge order, but some hard dependencies exist.

The main PRs are the two last ones, those which add support for building against a libcxx and support for exception handling. However, while the others are smaller, they are still required in order to analyze programs built and linked against a libcxx and using exceptions.

This PR adds support for exception handling and unwinding to KLEE, also supporting nested exceptions. The new tests show the added capabilities.

This is implemented by keeping track of a current stack of exception frames per state once unwinding begins, i.e., __cxa_throw is called. When unwinding is invoked in LLVM, control flow will transfer to the next landingpad block in the current call chain. A landingpad can be specified in LLVM by using invoke instead of call, which takes the target landingpad - where control flow should resume in case of an exception - as an extra argument. Different eh_typeids can be used to continue control flow at different blocks depending on the type of the exception that is being thrown (e.g., when using different catch-blocks in C++).

When a new exception is thrown, KLEE keeps track of the bottom and top stack frame indices of this exception. If execution unwinds below the bottomStackFrameIndex, it is uncaught, and an error is raised. The topStackFrameIndex adds support for nested exceptions, e.g., when a new exception is thrown inside a catch-block. As long as this new exception is caught inside this catch-block, it is not an error. Therefore, nested catch-blocks need to be supported, as well as nested try-blocks. See the tests nested.cpp and nested_fail.cpp for examples of this.

This PR also adds tests for a lot more general C++ functionality.
opened by futile 50
Implement basic support for vectorized instructions.
We use LLVM's Scalarizer pass to remove most vectorized code so that the Executor only needs to support the InsertElement and ExtractElement instructions.

This pass was not available in LLVM 3.4 so to support that LLVM version the pass has been back ported.

There is no support for LLVM 2.9.

There are a few limitations to this implementation.

The InsertElement and ExtractElement index cannot be symbolic.

Due to the lack of proper floating point support the float_vector_constant_llvm*.ll tests currently do not pass.
opened by delcypher 50
Support UBSan-enabled binaries
This MR resolves #1376.

I am guessing, that KLEE had already been implemented some checks that UBSan provides. However, there are some cases that are hard to catch without code instrumentation (out of bound indexing, load of invalid enum value and others).

You can see implementation of missing UBSan's handles from there, each of them started with __ubsan_handle prefix. As was mentioned in issue, "UBSan distinguishes between __ubsan_handle_add_overflow and __ubsan_handle_add_overflow_abort". Currently, both of them are processed in the same way, i.e. are caught by Executor::terminateStateOnError.

And beyond that, there are some handles from there. They could not reasonably be implemented and absent in this MR. If you have ideas about them, let me know.

[x] The PR addresses a single issue. In other words, if some parts of a PR could form another independent PR, you should break this PR into multiple smaller PRs.

[x] There are no unnecessary commits. For instance, commits that fix issues with a previous commit in this PR are unnecessary and should be removed (you can find documentation on squashing commits here).

[x] Larger PRs are divided into a logical sequence of commits.

[x] Each commit has a meaningful message documenting what it does.

[x] The code is commented. In particular, newly added classes and functions should be documented.

[x] The patch is formatted via clang-format (see also git-clang-format for Git integration). Please only format the patch itself and code surrounding the patch, not entire files. Divergences from clang-formatting are only rarely accepted, and only if they clearly improve code readability.

[x] Add test cases exercising the code you added or modified. We expect system and/or unit test cases for all non-trivial changes. After you submit your PR, you will be able to see a Codecov report telling you which parts of your patch are not covered by the regression test suite. You will also be able to see if the Github Actions CI and Cirrus CI tests have passed. If they don't, you should examine the failures and address them before the PR can be reviewed.

[x] Spellcheck all messages added to the codebase, all comments, as well as commit messages.
opened by operasfantom 47

IndependentSolver bug

Hi all, I am running some experiments with KLEE on Coreutils 6.11 and I deterministically experience this crash on date and touch utility:

KLEE: HaltTimer invoked  
KLEE: halting execution, dumping remaining states  
klee: IndependentSolver.cpp:532: virtual bool IndependentSolver::computeInitialValues(const klee::Query&, const std::vector<const klee::Array*>&, std::vector<std::vector<unsigned char> >&, bool&): Assertion `assertCreatedPointEvaluatesToTrue(query, objects, values) && "should satisfy the equation"' failed.  
0  libLLVM-3.4.so.1 0x00007fca47c60d62 llvm::sys::PrintStackTrace(_IO_FILE*) + 50  
1  libLLVM-3.4.so.1 0x00007fca47c607bc  
2  libpthread.so.0  0x00007fca46cb8d10  
3  libc.so.6        0x00007fca45e41267 gsignal + 55  
4  libc.so.6        0x00007fca45e42eca abort + 362  
5  libc.so.6        0x00007fca45e3a03d  
6  libc.so.6        0x00007fca45e3a0f2  
7  klee             0x00000000004f24ac IndependentSolver::computeInitialValues(klee::Query const&, std::vector<klee::Array const*, std::allocator<klee::Array const*> > const&, std::vector<std::vector<unsigned char, std::allocator<unsigned char> >, std::allocator<std::vector<unsigned char, std::allocator<unsigned char> > > >&, bool&) + 8012  
8  klee             0x00000000004f8aa9 QueryLoggingSolver::computeInitialValues(klee::Query const&, std::vector<klee::Array const*, std::allocator<klee::Array const*> > const&, std::vector<std::vector<unsigned char, std::allocator<unsigned char> >, std::allocator<std::vector<unsigned char, std::allocator<unsigned char> > > >&, bool&) + 73  
9  klee             0x00000000004fd4b3 klee::Solver::getInitialValues(klee::Query const&, std::vector<klee::Array const*, std::allocator<klee::Array const*> > const&, std::vector<std::vector<unsigned char, std::allocator<unsigned char> >, std::allocator<std::vector<unsigned char, std::allocator<unsigned char> > > >&) + 35  
10 klee             0x00000000004b8d57 klee::TimingSolver::getInitialValues(klee::ExecutionState const&, std::vector<klee::Array const*, std::allocator<klee::Array const*> > const&, std::vector<std::vector<unsigned char, std::allocator<unsigned char> >, std::allocator<std::vector<unsigned char, std::allocator<unsigned char> > > >&) + 263  
11 klee             0x000000000048899b klee::Executor::getSymbolicSolution(klee::ExecutionState const&, std::vector<std::pair<std::string, std::vector<unsigned char, std::allocator<unsigned char> > >, std::allocator<std::pair<std::string, std::vector<unsigned char, std::allocator<unsigned char> > > > >&) + 763  
12 klee             0x0000000000480e4e KleeHandler::processTestCase(klee::ExecutionState const&, char const*, char const*) + 302  
13 klee             0x000000000048930a klee::Executor::terminateStateEarly(klee::ExecutionState&, llvm::Twine const&) + 394  
14 klee             0x00000000004989d1 klee::Executor::run(klee::ExecutionState&) + 1377  
15 klee             0x000000000049937c klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1644  
16 klee             0x0000000000476c2e main + 11326  
17 libc.so.6        0x00007fca45e2ca40 __libc_start_main + 240  
18 klee             0x000000000047e0f9 _start + 41  
Aborted (core dumped)

My setup: Ubuntu 15.10 LLVM 3.4 KLEE (built with uclibc) 2a0eca5 STP 3785148da15919de445e476a6f20b06c881cf50c Coreutils 6.11 built with whole-program-llvm (with clang as llvm compiler) and configured as in the KLEE tutorial page

I experience this bug also in this setup: Ubuntu 15.10 LLVM 2.9 KLEE (built with uclibc) 2a0eca5 STP 3785148da15919de445e476a6f20b06c881cf50c Coreutils 6.11 built with klee-gcc and configured as in the KLEE tutorial page

The commands I use: klee --libc=uclibc --posix-runtime -use-query-log=all:pc --simplify-sym-indices --output-module --max-memory=1000 --disable-inlining --optimize --use-forked-solver --max-sym-array-size=4096 --max-instruction-time=30. --max-time=3600. --max-memory-inhibit=false --max-static-fork-pct=1 --max-static-solve-pct=1 --max-static-cpfork-pct=1 --switch-type=internal --randomize-fork --search=random-path --search=nurs:covnew --use-batching-search --batch-instructions=10000 --use-cex-cache=false ../coreutils-6.11/obj-llvm/src/date.bc --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdout

klee --libc=uclibc --posix-runtime -use-query-log=all:pc --simplify-sym-indices --output-module --max-memory=1000 --disable-inlining --optimize --use-forked-solver --max-sym-array-size=4096 --max-instruction-time=30. --max-time=3600. --max-memory-inhibit=false --switch-type=internal --randomize-fork --search=random-path --search=nurs:covnew --use-batching-search --batch-instructions=10000 --use-cex-cache=false ../coreutils-6.11/obj-llvm/src/touch.bc --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdout

The counterexample cache is disabled as per issue #347. The assertion fails both with and without -optimize option. Moreover, the assertion fails deterministically not only in KLEE but also in KLEAVER for example with the following query:

array n_args[4] : w32 -> w8 = symbolic                                                                                                                                                                                                                                          
array n_args_1[4] : w32 -> w8 = symbolic                                                                                                                                                                                                                                        
array A-data-stat[144] : w32 -> w8 = symbolic                                                                                                                                                                                                                                   
array stdin-stat[144] : w32 -> w8 = symbolic                                                                                                                                                                                                                                    
(query [(Ult N0:(ReadLSB w32 0 n_args) 2)                                                                                                                                                                                                                                                                
(Slt 0 N0)
(Ult N1:(ReadLSB w32 0 n_args_1) 3)
(Slt 0 N1)
(Slt 1 N1)
(Eq false (Eq 0 (And w64 (ReadLSB w64 8 A-data-stat) 2147483647)))
(Ult (ReadLSB w64 56 A-data-stat) 65536)
(Eq false (Eq 0 (And w64 (ReadLSB w64 8 stdin-stat) 2147483647)))]
(Eq false (Ult (ReadLSB w64 56 stdin-stat) 65536)) [] [n_args])

KLEAVER does not crash when we do not ask for a counterexample.

I will try to figure out what is happening to KLEE by also looking into the core dump. I hope to find out something useful to fix the bug.

bug

opened by andreamattavelli 46

[LLVM] Make KLEE compile against LLVM 3.7

There are not that many changes in 3.7, so this should be quite easy to review.

There is no llvm 3.7 in travis to enable builds for. This 3.7 code is used by my llvm_38 port where I also enable build with llvm 3.8.
LLVM upgrade

opened by jirislaby 39
Restructured include/klee/

I think the Internal directory makes no sense, and having Module, Support directly under include/klee makes more sense. The patch changes lots of files but it's quite trivial.

opened by ccadar 34

Module/RaiseAsm: Support x86 (aka 32bit) as well

Summary:

Fixes:

$ cat test.c
int main(void) {}
$ clang -m32 -emit-llvm -c test.c -o test.bc
$ klee test.bc
KLEE: output directory is "/home/lukas/klee/klee-out-9"
KLEE: Using Z3 solver backend
LLVM ERROR: 64-bit code requested on a subtarget that doesn't support it!
 #0 0x00007fb59688bbf6 llvm::sys::PrintStackTrace(llvm::raw_ostream&, int) (/lib64/libLLVM-12.so+0xc07bf6)
 #1 0x00007fb596889ae4 llvm::sys::RunSignalHandlers() (/lib64/libLLVM-12.so+0xc05ae4)
 #2 0x00007fb596889c69 (/lib64/libLLVM-12.so+0xc05c69)
 #3 0x00007fb595772310 __restore_rt (/lib64/libc.so.6+0x3d310)
 #4 0x00007fb595772292 raise (/lib64/libc.so.6+0x3d292)
 #5 0x00007fb59575b8a4 abort (/lib64/libc.so.6+0x268a4)
 #6 0x00007fb5967d7b5e llvm::report_fatal_error(llvm::Twine const&, bool) (/lib64/libLLVM-12.so+0xb53b5e)
 #7 0x00007fb5967d7c8e (/lib64/libLLVM-12.so+0xb53c8e)
 #8 0x00007fb5990e1b26 (/lib64/libLLVM-12.so+0x345db26)
 #9 0x00007fb5990e2120 (/lib64/libLLVM-12.so+0x345e120)
#10 0x00007fb5990e5ac4 (/lib64/libLLVM-12.so+0x3461ac4)
#11 0x00000000004919ed klee::RaiseAsmPass::runOnModule(llvm::Module&) /home/lukas/klee/build/../lib/Module/RaiseAsm.cpp:102:31
#12 0x00007fb5969b1d02 llvm::legacy::PassManagerImpl::run(llvm::Module&) (/lib64/libLLVM-12.so+0xd2dd02)
#13 0x0000000000486cac klee::KModule::instrument(klee::Interpreter::ModuleOptions const&) /home/lukas/klee/build/../lib/Module/KModule.cpp:237:23
#14 0x000000000043562f klee::Executor::setModule(std::vector<std::unique_ptr<llvm::Module, std::default_delete<llvm::Module> >, std::allocator<std::unique_ptr<llvm::Module, std::default_delete<llvm::Module> > > >&, klee::Interpreter::ModuleOptions const&) /home/lukas/klee/build/../lib/Core/Executor.cpp:537:23
#15 0x0000000000417dd5 main /home/lukas/klee/build/../tools/klee/main.cpp:1411:46
#16 0x00007fb59575cb75 __libc_start_main (/lib64/libc.so.6+0x27b75)
#17 0x0000000000424d6e _start (build/bin/klee+0x424d6e)

Checklist:

[x] The PR addresses a single issue. If it can be divided into multiple independent PRs, please do so.
[x] The PR is divided into a logical sequence of commits OR a single commit is sufficient.
[x] There are no unnecessary commits (e.g. commits fixing issues in a previous commit in the same PR).
[x] Each commit has a meaningful message documenting what it does.
[x] All messages added to the codebase, all comments, as well as commit messages are spellchecked.
[x] The code is commented OR not applicable/necessary.
[x] The patch is formatted via clang-format OR not applicable (if explicitly overridden leave unchecked and explain).
[ ] There are test cases for the code you added or modified OR no such test cases are required.

opened by lzaoral 33

ExecutorTimers: replace signalling with synchronous checks

Prevent endless looping fork in STPSolver (fixes #831) by replacing the signal-based timer handling with synchronous checks.

Removes -max-instruction-time and introduces -timer-interval (default 1s).

opened by 251 32
Various updates to gen-random-bout.cpp
This is to keep it up-to-date with the current ktest format, so that the output can be used as a seed.

Added handling of --sym-arg

Resolved the crash when minimum and maximum number of arguments for --sym-args are equal

Replaced range with n_args produced by --sym-args

Added model_version variable (constrained to 1), to prevent klee complaining about insufficient input

Allow a single dash to prefix an option

Arrange the elements in the correct order: command-line arguments, files, stdin, and lastly stdout
opened by domainexpert 32
klee assertion at IndependentSolver.cpp:545

klee (with llvm 3.4) is consistently asserting (after a few hours) at the following point:

klee: IndependentSolver.cpp:545: virtual bool IndependentSolver::computeInitialValues(const klee::Query&, const std::vector<const klee::Array*>&, std::vector<std::vector >&, bool&): Assertion `assertCreatedPointEvaluatesToTrue(query, objects, values, retMap) && "should satisfy the equation"' failed.

It looks like klee is trying to fork a new branch, but the initial path constraint is false. Can anyone tell me if this is indeed the fault?

Also, any suggestions about what I might do about it?

Thanks! Rick Rutledge

byte code is attached, and klee ran with the following command line:

klee -libc=uclibc -posix-runtime -entry-point=klee_main main.bc

main.bc.zip

opened by naegling 31
Inline assembly support (external call)
Summary:

The wrapper (KCallable) was created for the objects (Function, InlineAsm) that can be called in LLVM IR. Now callExternalFunction takes the KCallable wrapper as an argument. In the ExternalDispatcherImpl::createDispatcher function was added a code branch to process inline assembler code (the llvm::IRBuilder<>.CreateCall function call with the InlineAsm object as a parameter).

Closes #1514.

Checklist:

[x] The PR addresses a single issue. If it can be divided into multiple independent PRs, please do so.

[x] The PR is divided into a logical sequence of commits OR a single commit is sufficient.

[x] There are no unnecessary commits (e.g. commits fixing issues in a previous commit in the same PR).

[x] Each commit has a meaningful message documenting what it does.

[x] All messages added to the codebase, all comments, as well as commit messages are spellchecked.

[x] The code is commented OR not applicable/necessary.

[x] The patch is formatted via clang-format OR not applicable (if explicitly overridden leave unchecked and explain).

[x] There are test cases for the code you added or modified OR no such test cases are required.
opened by mishok2503 29
Can klee support logic operation between two ConstraintSet?

Hi, author.

Right now I need to do such an operation between two CnstraintSet con1 and cond2, the operation is to evaluate the value of con1 && ~cond2, that an and operation between one Constraint and a negation operation.

But right now I don't find support for such feature, even simple and or negation operation for a Constraint set.

And also, I wish klee could support con1 || con2 into a new ConstraintSet. Could klee support this now?

So if klee doesn't support this, how to modify the code to do such operation?

opened by for-just-we 0
fix output check in test const_arr_opt1
Summary:

Fixes test Feature/const_array_opt1.

The grep command was not called since the RUN directive was missing. I fixed it by adding an equivalent FileCheck call that should also increase readability.

Checklist:

[x] The PR addresses a single issue. If it can be divided into multiple independent PRs, please do so.

[x] The PR is divided into a logical sequence of commits OR a single commit is sufficient.

[x] There are no unnecessary commits (e.g. commits fixing issues in a previous commit in the same PR).

[x] Each commit has a meaningful message documenting what it does.

[x] All messages added to the codebase, all comments, as well as commit messages are spellchecked.

[x] The code is commented OR not applicable/necessary.

[x] The patch is formatted via clang-format OR not applicable (if explicitly overridden leave unchecked and explain).

[x] There are test cases for the code you added or modified OR no such test cases are required.
opened by fwc 1
Fix arrayopt checks
Summary:

Some tests in the ArrayOpt folder were missing FileCheck invocations to check for the default CHECK directive. This PR adds those invocations and suggests fixes for most of the ensuing failures.

Two tests (test-mix.c and test_cache.c) still fail since the constraints introduced by the following branch condition are not optimized.

klee_make_symbolic(&k, sizeof(k), "k"); klee_assume(k < 5); klee_assume(k >= 0); // ... if (array[k] + k - 2 == 5) printf("Good\n");

Should the array optimizer be able to handle this?

Checklist:

[x] The PR addresses a single issue. If it can be divided into multiple independent PRs, please do so.

[x] The PR is divided into a logical sequence of commits OR a single commit is sufficient.

[ ] There are no unnecessary commits (e.g. commits fixing issues in a previous commit in the same PR).

[x] Each commit has a meaningful message documenting what it does.

[x] All messages added to the codebase, all comments, as well as commit messages are spellchecked.

[x] The code is commented OR not applicable/necessary.

[x] The patch is formatted via clang-format OR not applicable (if explicitly overridden leave unchecked and explain).

[x] There are test cases for the code you added or modified OR no such test cases are required.
opened by fwc 0
Batched concolic path constraints retrieval (seed mode)

Is your feature request related to a problem? Please describe. I'm using klee to generate path conditions for millions of inputs. I try seed-mode, and use the --seed-dir option to give a directory of ktest file as input. however, KLEE automatically merge these state and generate only houndreds of smt2 constraint files, but i need one smt2 constraint file per input ktest file as output. I wonder if this is easy to implement ? or can I realize this in current KLEE version?

BTW, I tried use klee to generate constraint for these ktest file one by one, but it's extremly slow, taking me one second to generate only 2~3 outputs.

opened by zhaoxuyang13 0
does KLEE support union?
To ask a question about KLEE:

Please first check the documentation at http://klee.github.io/docs/

Then check the searchable mailing list archive

If this still doesn’t answer your questions then please send an email to the klee-dev mailing list

We will normally not answer questions asked on GitHub.
opened by dongyuma 0
Question about how to link other libs?

Hi, author. Recently I tried to integrate machine learning based search strategy learch learch into klee-2.3. But I came across one problem.

I reimplement learch with libtorch (Which is C++ lib for pytorch) instead of interact with python. Which require me to link libraries in libtorch.

The libtorch code is only used in Searcher.h and Searcher.cpp. In another way, I only include header files in Searcher.h and Searcher.cpp. So how should I modify CMakeList.txt to correctly use libtorch?

opened by for-just-we 0

Releases(v2.3)

v2.3(Apr 4, 2022)
KLEE 2.3, 4 April 2022

Incorporating changes from 8 December 2020 to March 2022. Maintainers during this time span: @ccadar and @MartinNowack Documentation at http://klee.github.io/releases/docs/v2.3

LLVM support

Current recommended version is LLVM 11

Added support for LLVM 12 and 13 (@lzaoral)

Removed support for LLVM <6

KLEE 2.3 will be the last version with support for LLVM <9

Options, scripts and KLEE intrinsics added, changed or removed

Added --max-static-pct-check-delay to specify the number of forks after which the --max-static-*-pct checks are enforced (@ccadar)

In klee-stats, added --print-columns to print user-defined columns, e.g. --print-columns 'Path,Instrs,Time(s)' (@251)

Disabled Doxygen generation by default; it can be enabled via CMake option ENABLE_DOXYGEN=ON

Other changes

Introduced termination categories and branch types (@251)

Added support for more recent versions of Google Test (@jbuening)

Fixed --prefer-cex, which was crashing in some cases (@TarasBereznyak)

Added support for executing 32bit code, with some limitations (@lzaoral)

Improved exception handling (@jbuening)

Various improvements to klee-stats (@251)

Fixed UBSan reporting in the CI and fixed several errors reported by UBSan (@lzaoral)

Fixed path statistics with -dump-states-on-halt=false (@251)

Differentiate between partial and completed paths in the summary printed at the end (@251)

Improved determinism (@jbuening)

Added support for LLVM abs (except for the vector variants), llvm.roundeven and llvm.{s,u}{max,min} intrinsics (@lzaoral)

Fixed and improved model for getcwd (@251)

Fixed a silent concretization case in Executor::fork (@ccadar)

Added a large number of KLEE-related publications to the website (@251)

Fixed the memory usage computation on macOS (@ccadar)

Removed or updated obsolete Doxygen options and added Doxygen generation to the CI (@ccadar)

Smaller refactorings, fixes and improvements, test cases, maintenance, comments, web version, website, etc. (@251, @aesophor, @arrowd, @bathooman, @ccadar, @carlocab, @davidtr1037, @dependabot, @futile, @iangneal, @jbuening, @jirislaby, @jiseongg, @jordr, @lzaoral, @MartinNowack, @numinit, @operasfantom, @prncoprs)

Source code(tar.gz)
Source code(zip)
v2.2(Dec 7, 2020)
KLEE 2.2 on 7 December 2020

Incorporating changes from 4 March 2020 to 7 December 2020. Maintainers during this time span: @ccadar and @MartinNowack Documentation at http://klee.github.io/releases/docs/v2.2

Major features

Added support for C++ exceptions (@corrodedHash, @futile, @jbuening)

Correctly copy variadic arguments with byval attribute (@ccadar)

Modified the random path searcher to work on a subset of states (@kren1)

Added state IDs to improve determinism (@251)

Overhauled the (Travis CI) build scripts (@MartinNowack)

Restructured header files (@ccadar)

LLVM support

Current recommended version is LLVM 9

Added support for LLVM 11 (@lzaoral)

We have decided to extend support for LLVM 3.8 to 5, but KLEE 2.2 will be the last version with support for LLVM <6

Options, scripts and KLEE intrinsics added, changed or removed

Changed --debug-print-instructions to also print state IDs (@251)

Added -rng-initial-seed to set the seed for KLEE's random number generator (@251)

Added klee_is_replay intrinsic which returns whether the code is being executed symbolically or in replay mode (@alastairreid)

Added --compress-process-tree to remove intermediate nodes in the process tree when possible (@sebastianpoeplau)

Added klee-zesti, a ZESTI-like wrapper (@kren1)

Added --table-format=readable-csv/csv to klee-stats (@251)

Other changes

Fixed GlobalAlias initialization (@jbuening)

Enforced fork/branch limits in branch() and fix double termination (@251)

Enhanced POSIX runtime in the case where a symbolic file is given as an absolute path, i.e. /current/work/dir/A (@kren1)

Named jobs in Travis CI for better visualization of results (@ccadar)

Fixes and improvements in the statistics code including klee-stats (@251)

Added a simple model for GET/SET_LK (@kren1)

Fixed bug in the handling of vectorized code (@Warfley)

Fixed bug in the handling of STP array names (@MartinNowack)

Fixed bug in Z3Solver::getConstraintLog (@daniel-grumberg)

Added support for reading strings from the middle of objects in readStringAtAddress (@mchalupa)

Disabled asm lifting for memory fences with return values (@MartinNowack)

Fixed bug when the search requires MD2U (@adrianherrera)

Added support for fshr/fshl intrinsics (@alastairreid)

Refactored the constraint manager (@MartinNowack)

Changed DiscretePDF to use IDs instead of pointers to remove nondeterminism (@251)

Added a more robust handling of unknown intrinsics: if an unknown intrinsic is encountered on a path, that path is terminated but the others can proceed (@alastairreid)

Fixed PTree::remove to clean the tree properly (@sebastianpoeplau)

Added support for multiple symbolic files to gen-bout (@kren1)

Added a PR template, with a checklist documenting the most frequent issues we have encountered (@ccadar)

Fixed the behaviour of klee-stats for broken or empty DBs (@251)

Added support for klee_open_merge and klee_close_merge in replay (@ccadar)

Fixed the handling of global variables while validating direct call targets (@MartinNowack)

Fixed the handling of the fabs intrinsic (@dlaprell)

Added support for the fneg instruction (@jbuening)

Removed incompatibility between merging and the random path search (@251)

Fixed the behaviour of klee-libc to call the functions in __cxa_atexit in reverse order (@tomsik68)

Fixed the behaviour of bcmp in klee-libc (@alastairreid)

Added support for multi-version bitcode libraries (@MartinNowack)

Added support for several fortified functions, -D_FORTIFY_SOURCE (@ccadar)

Modernize ref<> and isa<> nullptr checks (@jbuening)

Switched CI from Travis CI to GitHub Actions (@MartinNowack, with thanks to @jordr)

Smaller refactorings, fixes and improvements, test cases, maintenance, comments, web version, website, etc. (@251, @adrianherrera, @alastairreid, @andrewvaughanj, @andronat, @arrowd, @ccadar, @dependabot, @i-ky, @jbuening, @jiseongg, @jordr, @kren1, @lahiri-phdworks, @MartinNowack, @yxliang01)

Source code(tar.gz)
Source code(zip)
v2.1(Mar 3, 2020)
KLEE 2.1, 3 March 2020

Incorporating changes from 20 March 2019 to 3 March 2020. Maintainers during this time span: @ccadar and @MartinNowack Documentation at http://klee.github.io/releases/docs/v2.1

Major features

New container-based architecture for KLEE Web (@Denis-Gavrielov, @andronat)

Changed the statistics framework to use SQL and improve klee-stats (@kren1, @251)

Added Grafana visualisation to klee-stats (@gdish, @KennyMacheka, @kren1)

Brought gen-random-bout up-to-date (@domainexpert)

Fixed support for FreeBSD (@arrowd)

Replaced signalling with synchronous checks for implementing timers (@251)

Improved reference handling (ref<>) (@MartinNowack)

LLVM support

Added support for LLVM 9 and 10 (@jbuening)

Removed support for LLVM <3.8 (@jbuening)

KLEE 2.1 will be the last version with support for LLVM <6

Options, scripts and KLEE intrinsics added, changed or removed

Replaced intrinsic klee_alias_function("foo", "bar") with option -function-alias=foo:bar, which supports regular expressions (@jbuening, @SolalPirelli)

Removed -max-instruction-time (@251)

Added -timer-interval (default 1s) to specify the minimum interval to check timers (@251)

Added nurs:rp searcher which uses non-uniform random search with 1/2^depth (@kren1)

Replaced the behavior of the nurs:depth searcher to use NURS with depth (@kren1)

klee-stats: new --grafana option (see above)

klee-stats: new --to-csv option for converting statistics to the CSV format (@251)

klee-stats: removed --sample-interval, --sort-by, --compare-by, --precision. These can be now simulated by querying the SQL database directly (@kren1)

klee-replay: added --keep-replay-dir option to keep the replay directory (@ccadar)

Other changes

Added support for llvm.fabs (@futile)

Added support for saturated arithmetic intrinsics (@mateon1)

Added support for llvm.objectsize (@MartinNowack)

Added support for llvm.is.constant (@arrowd)

Fixed bugs in --optimize-array (@kren1)

Removed statistics limit from istats (@MartinNowack)

Refactored PTree (@251)

Improved klee-replay and made it safe to run multiple instances in parallel (@ccadar)

Check if read-only objects are marked as symbolic (@MartinNowack)

Allow main() with 3 arguments (@ccadar)

Improved the structure of the codebase (@ccadar)

Improved KLEE's CI build scripts (@MartinNowack, @jbuening)

Smaller refactorings, fixes and improvements, test cases, maintenance, comments, web version, website, etc. (@251, @arrowd, @benquike, @ccadar, @cyberwookiee, @danielschemmel, @Denis-Gavrielov, @dependabot, @domainexpert, @futile, @gdish, @JasonPap, @jbuening, @jirislaby, @KennyMacheka, @kren1, @MartinNowack, @qurben)

Source code(tar.gz)
Source code(zip)
v2.0(Mar 19, 2019)
KLEE 2.0, 19 March 2019

Incorporating changes from 22 July 2017 to 19 March 2019 Maintainers during this time span: @AndreaMattavelli, @ccadar, @delcypher, @MartinNowack Documentation at http://klee.github.io/releases/docs/v2.0

Major features

Added support for KLEE array optimizations from ISSTA'17 paper Accelerating Array Constraints in Symbolic Execution (@AndreaMattavelli, @MartinNowack, @ccadar)

Added support for LibC++ (--libcxx flag) (@corrodedHash, @futile, @MartinNowack)

Added support for CVC4 and Yices2 via metaSMT (@hoangmle)

Added better path merging functionality via klee_open_merge and klee_close_merge (@corrodedHash, @futile)

Fixed support for vector instructions (@MartinNowack)

Support for recent LLVM versions (see LLVM support below)

New categorized --help menu, with LLVM options hidden by default (see "Options, scripts and intrinsics changed or removed" below)

LLVM support

Added support for LLVM 3.7 - 7.0 (@jirislaby)

Added support for LLVM 8.0 (@MartinNowack)

KLEE 2.0 will be the last release with support for LLVM 3.4 to 3.7

Removed support for LLVM <3.4 (@MartinNowack)

Options, scripts and intrinsics changed or removed

Renamed several options (@ccadar)

--environ to --env-file

--no-output to --write-no-tests

--red-zone-space to --redzone-size

--run-in to --run-in-dir

--seed-out to --seed-file

--seed-out-dir to --seed-dir

--stop-after-n-tests to --max-tests

--use-cache to --use-branch-cache

--use-construct-hash to --use-construct-hash-stp

--warn-all-externals to --warn-all-external-symbols

Replaced --no-externals and --allow-external-sym-calls with --external-calls (@ccadar)

Added --libcxx option to enable LibC++ support (see Major features above)

Added option --max-stack-frames to limit the number of stack frames used (@MartinNowack)

Added --klee-call-optimisation option, which can be set to false to disable some optimizations that interact incorrectly with the checks injected by KLEE. See https://github.com/klee/klee/pull/1059 for more details (@MartinNowack)

Added support for disabling --batch-instructions and --batch-time by setting them to zero (@ccadar)

Removed option --disable-opt (@ccadar)

Removed klee-gcc and klee-clang (@251, @MartinNowack)

Removed support for klee_make_symbolic with two arguments (@ccadar)

Allow NULL as name to klee_int, to create "unnamed" object (@251)

New time API used in options (@251)

Improved the output of ktest-tool and added an --extract option (@251)

Categorized options in --help, improved help messages, and hid LLVM options by default (@ccadar)

Other changes

Updated build system to detect whether STP, Z3, metaSMT are available (@delcypher)

Fixed test case counter: previously the number of test cases generated by KLEE was always incremented, even if a symbolic solution was not found (@andreamattavelli)

Added checks for div/mod by zero and overshifts in constant expressions (@ccadar)

Fixed a bug causing KLEE to generate files with no permissions bits set (@ccadar)

Added clean_doxygen target and a global clean_all target to the build system (@delcypher)

Fixed initialization of distance to uncovered instructions when KLEE relies on default searchers (@andreamattavelli)

Fixed assert in BFSSearcher that does not hold as part of interleaved searcher (@jbuening)

Fixed huge allocation size constant (@davidtr1037)

Added Codecov support (@andreamattavelli, @MartinNowack)

Store cex cache stats and report them in klee-stats (@helicopter88)

Fixed incorrectly incremented stats for dumped states (@251)

Fixed bug where KLEE would not output test cases when --exit-on-error is enabled (@buszk)

Added support for blockaddress and indirectbr instructions (@251)

Implemented klee_prefer_cex() and klee_abort() for replay mode (@Lysxia)

Fixed handling of errno when external functions are invoked (@MartinNowack)

Fixed utimes() behavior for symbolic files when the second argument is NULL (@yxliang01)

Improved handling of constant array in Z3 (@kren1)

Improved the handling of external calls with symbolic data (@kren1)

Abort execution if --only-output-states-covering-new is enabled but its dependency --output-istats is not (@ccadar)

Improved ConstantExpr performance (@kren1)

Improved linking and optimizations order (@MartinNowack)

Enabled TCMalloc by default (@kren1)

Disabled unit testing in default build (@AndreaMattavelli)

Added resolve time to klee-stats --print-all (@251)

Improved the startup sequence enabling the POSIX runtime (@MartinNowack)

Added ASan and UBSan flags to lit (@251)

Added support for handling multiple SIGSEGVs in external calls (@251)

Added checks for correct usage of the POSIX mode (@ccadar)

Added support for klee-replay on OSX (@251)

Added lowering pass for atomic instructions (@erzett, @futile)

Improved handling of metadata (@MartinNowack)

Improved efficiency of div/mod and shift checks by skipping unnecessary checks (@MartinNowack)

Added support for memalign (@corrodedHash)

Enable C++14 support (@MartinNowack)

Fixed issue with aliases that point to other aliases (@jbuening)

Added workaround for the LLVM bug PR39177 (@jbuening)

Updated dependency build system for KLEE (@MartinNowack)

Fixed the Docker deployment for KLEE (@MartinNowack)

Added support for compiling KLEE with MSan and UBSan's integer sanitizer (@MartinNowack)

Fixed representation of ReadExpr's into equivalent arrays (@MartinNowack)

Added support for debug information provided by newer LLVM versions (@MartinNowack)

Added many KLEE-related publications (@251)

Smaller refactorings, fixes and improvements, test cases, maintenance, comments, web version, website, etc. (@andronat, @251, @andreamattavelli, @ccadar, @corrodedHash, @danielschemmel, @delcypher, @itbot08, @jasondavies, @jbuening, @jirislaby, @kren1, @Lysxia, @MartinNowack, @Mic92, @odeits-vidder, @SolalPirelli, @szeyiuchau, @Tipwheal, @yannicnoller)

Source code(tar.gz)
Source code(zip)
v1.4.0(Jul 21, 2017)
KLEE 1.4.0, 21 July 2017

(Incorporating changes from 4 November 2016 up to and including 21 July 2017) Documentation at http://klee.github.io/releases/docs/v1.4.0/

This will be the last version supporting LLVM 2.9 and the autoconf build system.

New CMake build system (@delcypher, @jirislaby)

Added support for vectorized instructions (@delcypher)

Fixed and documents BFS searcher behaviour (@MartinNowack, @ccadar)

Renames .pc files to .kquery files (@holycrap872)

Removed option --randomize-fork (@ccadar)

Changed preferred permissions from 0622 to the more standard 0644 in the POSIX model (@ccadar)

New target name, "make systemtests", for running the system tests. This replaces "make test". Running the unit tests is still accomplished via "make unittests".

Better support for MacOS (@andreamattavelli, @delcypher)

Enabled support for ASan builds of KLEE (@delcypher)

Support long long values in --stop-after-n-instructions for LLVM > 2.9 (@andreamattavelli)

Teach KLEE to respect the requested memory alignment of globals and stack variables when possible (@delcypher)

Added new option --warnings-only-to-file which causes warnings to be written to warnings.txt only (@ccadar)

metaSMT improvements (@hoangmle)

KLEE-web improvements (@andronat, @helicopter88)

Fixed bug in the implementation of NotExpr (@delcypher)

Fixed a bug leading to data loss when writing into files (@ccadar, @gladtbx)

Some improvements and refactoring to the Expr library (@delcypher)

Added missing constant folding opportunity when handling constant arrays (@andreamattavelli, @delcypher)

Teach klee::getDirectCallTarget() to resolve weak aliases (@delcypher)

Fixed handling of internal forks (@gladtbx)

Improved replay using libkleeRuntest (@delcypher)

Added -debug-assignment-validating-solver feature to check the correctness of generated assignments (@delcypher)

Added -debug-z3-dump-queries, -debug-z3-validate-models and -debug-z3-verbosity options useful for debugging the interaction with Z3 (@delcypher)

Added geq/lt-llvm- configs in lit (@jirislaby)

Work on supporting newer LLVM versions (@jirislaby)

Fixed bug where stats would not be updated on early exit (@delcypher)

Reworked the external dispatching mechanism (@delcypher)

Added support for creating release documentation (@delcypher)

Smaller refactorings, fixes and improvements, test cases, maintenance, comments, website, etc. (@adrianherrera, @akshaynagpal, @AlexxNica, @andreamattavelli, @bananaappletw, @bigelephant29, @bunseokbot, @ccadar, @delcypher, @emlai, @hoangmle, @jirislaby, @kren1, @levex, @Manouchehri, @MartinNowack, @mechtaev, @Mic92, @omeranson, @rtrembecky, @thestr4ng3r, @tomek-kuchta)

Source code(tar.gz)
Source code(zip)
v1.3.0(Nov 30, 2016)
KLEE 1.3.0, 30 November 2016

(Incorporating changes from 1 April up to and including 3 November 2016)

Improved determinism of KLEE, an essential feature for experiments involving KLEE (@MartinNowack)

KLEE-web has been improved and refactored, and now available at http://klee.doc.ic.ac.uk/ (@giacomoguerci, @helicopter88, @andronat, @ccadar, based on work by @ains, @ben-chin, @ilovepjs, @JamesDavidCarr, Kaho Sato, Conrad Watt, @ccadar)

Renamed --replay-out to --replay-ktest and --replay-out-dir to replay-ktest-dir (@delcypher)

Split creation of symbolic files and stdin in two distinct options, documented at http://klee.github.io/docs/options/#symbolic-environment (@andreamattavelli)

Support for logging queries before invoking the solver via --log-partial-queries-early, useful for debugging solver crashes (@MartinNowack)

Added --stats-write-after-instructions and --istats-write-after-instructions to update each statistic after n steps (@MartinNowack)

Added --compress-log and --debug-compress-instructions to gzip-compress logs (@MartinNowack)

Added --exit-on-error-type option for stopping execution when certain error types are encountered (@jirislaby)

Updated and improved metaSMT support and added TravisCI targets (@hoangmle)

Added option --debug-crosscheck-core-solver to allow crosschecking of solvers (@delcypher)

Explicitly made division total in STP (@ccadar)

Extended support for assembler raising (@MartinNowack)

Disabled --solver-optimize-divides, as the optimization is currently buggy (@ccadar)

Improved --debug-print-instructions options with more logging options (@andreamattavelli)

Improved stub for times() not to trigger a NULL dereference (@ccadar)

Allow relocation of installed KLEE tree (@ShayDamir)

Fixed bug in independent solver (@delcypher)

Fixed alignement of varargs (@MartinNowack)

Fixed variable shifting behavior with different sizes and generation of STP shift operations with variable amounts (@MartinNowack)

Fixed handling of non-sized globals (@jirislaby)

Fixed klee_get_obj_size() crash on 64-bit (@hutoTUM)

Fixed bug in Kleaver's parser (@andreamattavelli)

Refactorings, small fixes and improvements, test cases, maintenance and website: (@andreamattavelli, @ccadar, @delcypher, @domainexpert, @giacomoguerci, @hoangmle, @helicopter88, @jirislaby, @Justme0, @kren1, @MartinNowack, @mchalupa)

Source code(tar.gz)
Source code(zip)
v1.2.0(Mar 31, 2016)
KLEE 1.2.0, 31 March 2016

Added native support for Z3 (@delcypher)

Made it possible to build KLEE without using STP and only MetaSMT (@delcypher)

Added support for tcmalloc, which allows KLEE to better track memory consumption (@MartinNowack)

Added support for lowering the llvm.objectsize intrinsic (@delcypher)

Added soname for Runtest dynamic library (@MartinNowack)

Added support to load libraries from command line (@omeranson)

Added command line flag --silent-klee-assume to suppress errors due to infeasible assumptions (Valentin Wüstholz, @wuestholz)

Changed code to print out arrays deterministically (@MartinNowack)

Improved klee-clang script (@msoos)

Added code to dump queries and assignments (@MartinNowack)

Code cleanup and refactorings (@delcypher, @MartinNowack)

Improvements to code infrastructure (@delcypher, @domainexpert, @MartinNowack, @mdimjasevic, @msoos)

Fixed several memory leaks (@delcypher)

Fixed a bug with how non-power of 2 values were written to memory (@kren1)

Fixed valueIsOnlyCalled() used by MD2U (@yotann)

Fixed SELinux signatures (@lszekeres)

Fixed incorrect position of Not in Expr::Kind (@delcypher)

Fixed wrong std::vector usage after reserve() call (@pollnossa)

Improved documentation (@bananaappletw, @ccadar, @delcypher, @mdimjasevic, @Teemperor, @ward, @wuestholz)

Source code(tar.gz)
Source code(zip)
v1.1.0(Nov 13, 2015)
KLEE 1.1.0, 13 November 2015

Made LLVM 3.4 and STP 2.1.0 the recommended versions for installing KLEE (Cristian Cadar, @ccadar; Dan Liew, @delcypher; Martin Nowack, @MartinNowack; Mate Soos, @msoos)

Added instructions for using the Docker images (Dan Liew, @delcypher)

Added NEWS file to keep track of changes for each release (Cristian Cadar, @ccadar)

Added coverage information for the current KLEE codebase (Timotej Kapus, @kren1)

Added -entry-point=FOO option, where FOO is the name of the function to use as the entry point for execution (Riccardo Schirone, @ret2libc)

Switched STP to v2.1.0 (instead of the old r940) in TravisCI (Martin Nowack, @MartinNowack)

Improved Dockerfiles to use specific dependency versions (Dan Liew, @delcypher)

Bug fix: Fixed signed division by constant 1/-1 (Martin Nowack, @MartinNowack, reported by Timotej Kapus, @kren1)

Bug fix: Generate SRrem expressions correctly (Martin Nowack, @MartinNowack, reported by Timotej Kapus, @kren1)

Bug fix: Allowed the generation of initial values for queries with empty constraint set (Martin Nowack, @MartinNowack)

Bug fix: Fixed assertion failure in getDirectCallTarget (Sean Bartell, @yotann)

Bug fix/test improvement: Use a temporary directory instead of /tmp in futimesat test (Andrew Chi, @andrewchi)

Various fixes and improvements to the website (Eric Rizzi, @holycrap872; Martin Nowack, @MartinNowack; Bheesham Persaud, @bheesham; Gu Zhengxiong, @NoviceLive; Cristian Cadar, @ccadar)

Source code(tar.gz)
Source code(zip)
v1.0.0(Aug 10, 2015)
First official release for KLEE.

Recent changes (from 2015)

Several performance improvements to the counterexample cache, including changing some default behaviour (Eric Rizzi, @holycrap872)

Computing coverage of KLEE code in Travis CI (Timotej Kapus, @kren1)

Added an option --readable-posix-inputs which is used to turn on/off the CEX preferences added in the POSIX model (Eric Rizzi, @holycrap872; Cristian Cadar, @ccadar)

Lots of improvements to the build process (Dan Liew, @delcypher)

Added klee-clang as alternative to klee-gcc (Martin Nowack, @MartinNowack)

Added Dockerfile for building a KLEE Docker image (Dan Liew, @delcypher)

Added a new option, --rewrite-equalities, which makes it possible to disable the optimisation that rewrites existing constraints when an equality with a constant is added (Cristian Cadar, @ccadar)

Cleaner, more efficient timestamps (Emil Rakadjiev, @erakadjiev)

Improved integer overflow detection (Luca Dariz, @luckyluke)

Source code(tar.gz)
Source code(zip)