KLEE Symbolic Execution Engine

KLEE Symbolic Virtual Machine

Build Status Build Status Build Status Coverage

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

  1. 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/.

  2. 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.

Owner
KLEE
The KLEE Dynamic Symbolic Execution Engine and related projects
KLEE
Comments
  • Add support for exception handling (C++ 6/6)

    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.

  • Implement basic support for vectorized instructions.

    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.
  • Support UBSan-enabled binaries

    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.
  • IndependentSolver bug

    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.

  • [LLVM] Make KLEE compile against LLVM 3.7

    [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.

  • Restructured include/klee/

    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.

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

    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.
  • ExecutorTimers: replace signalling with synchronous checks

    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).

  • Various updates to gen-random-bout.cpp

    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
  • klee assertion at IndependentSolver.cpp:545

    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

  • Inline assembly support (external call)

    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.
  • does KLEE support union?

    does KLEE support union?

    To ask a question about KLEE:

    1. Please first check the documentation at http://klee.github.io/docs/
    2. Then check the searchable mailing list archive
    3. 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.

  • Question about how to link other libs?

    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?

  • Wrong variable name observed in `.ktest` file

    Wrong variable name observed in `.ktest` file

    Bug description

    Two symbolic variables array_0 and array_1 were defined. KLEE completed and exited successfully. However, variable names in .ktest files seemed to be broken.

    • .kquery: both array_0 and array_1 appeared (GOOD)
    • .ktest: 2 objects shared the same name array_1 (BAD)

    Example code

    #include <alloca.h>
    #include <stdio.h>
    #include <string.h>
    
    #include <klee/klee.h>
    
    int main() {
      int array[2];
    
      for (int i = 0; i < 2; i++) {
        char *s = (char *)alloca(50);
        sprintf(s, "%s", "array");
        sprintf(s + strlen(s), "_%d", i);
    
        int temp;
        klee_make_symbolic(&temp, sizeof(temp), s);
        array[i] = temp;
      }
    
      int identical = 0;
      if (array[0] == array[1])
        identical++;
    
      return 0;
    }
    

    Compiled with clang:

    clang-11 -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone main.c
    

    KLEE cmdline:

    klee --libc=uclibc --posix-runtime --write-kqueries main.bc
    

    Output of KLEE:

    KLEE: NOTE: Using POSIX model: /usr/local/lib/klee/runtime/libkleeRuntimePOSIX64_Debug+Asserts.bca
    KLEE: NOTE: Using klee-uclibc : /usr/local/lib/klee/runtime/klee-uclibc.bca
    KLEE: output directory is "/home/zyk/Projects/C/klee_examples/for_loop/klee-out-0"
    KLEE: Using Z3 solver backend
    KLEE: WARNING: executable has module level assembly (ignoring)
    KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 94780079623312) at klee/runtime/POSIX/fd.c:1012 10
    KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
    KLEE: WARNING ONCE: calling __klee_posix_wrapped_main with extra arguments.
    
    KLEE: done: total instructions = 39295
    KLEE: done: completed paths = 2
    KLEE: done: partially completed paths = 0
    KLEE: done: generated tests = 2
    

    Inspecting klee-last/test000001.ktest with ktest-tool:

    $ ktest-tool klee-last/test000001.ktest
    ktest file : 'klee-last/test000001.ktest'
    args       : ['main.bc']
    num objects: 3
    object 0: name: 'model_version'
    object 0: size: 4
    object 0: data: b'\x01\x00\x00\x00'
    object 0: hex : 0x01000000
    object 0: int : 1
    object 0: uint: 1
    object 0: text: ....
    object 1: name: 'array_1'
    object 1: size: 4
    object 1: data: b'\xff\x00\x00\x00'
    object 1: hex : 0xff000000
    object 1: int : 255
    object 1: uint: 255
    object 1: text: ....
    object 2: name: 'array_1'
    object 2: size: 4
    object 2: data: b'\x00\x00\x00\x00'
    object 2: hex : 0x00000000
    object 2: int : 0
    object 2: uint: 0
    object 2: text: ....
    

    Content of klee-last/test000001.kquery:

    array array_0[4] : w32 -> w8 = symbolic
    array array_1[4] : w32 -> w8 = symbolic
    array model_version[4] : w32 -> w8 = symbolic
    (query [(Eq 1
                 (ReadLSB w32 0 model_version))
             (Eq false
                 (Eq (ReadLSB w32 0 array_0)
                     (ReadLSB w32 0 array_1)))]
            false)
    

    This archive file contains the C source file along with bitcode and KLEE's output: for_loop.tar.gz

    Platform information

    OS version: Ubuntu 22.04.1 LTS

    Output of klee --version:

    KLEE 3.0-pre (https://klee.github.io)
      Build mode: RelWithDebInfo (Asserts: ON)
      Build revision: 667ce0f1ef33c32fbe2d1836fc1b334066e244ca
    
    LLVM (http://llvm.org/):
      LLVM version 11.1.0
      
      Optimized build.
      Default target: x86_64-pc-linux-gnu
      Host CPU: znver1
    
  • Track source-level program state when debug info is present

    Track source-level program state when debug info is present

    Context

    KLEE tracks program state at the LLVM IR level. For some applications, it would be helpful to know how this maps back to some source-level state in whichever language was compiled to IR.

    For example, the following C function...

    int example(int n) {
      int y = 0;
      for (unsigned int i = 0; i < n; i++) {
        y += 4 + n;
      }
      return y;
    }
    

    ...becomes something like the following IR using Clang 13 (-O1)...

    define i32 @example(i32 %0) local_unnamed_addr #0 {
      %2 = icmp eq i32 %0, 0
      br i1 %2, label %9, label %3
    
    3:                                                ; preds = %1
      %4 = add i32 %0, -1
      %5 = add i32 %0, 4
      %6 = mul i32 %4, %5
      %7 = add i32 %6, %0
      %8 = add i32 %7, 4
      br label %9
    
    9:                                                ; preds = %3, %1
      %10 = phi i32 [ 0, %1 ], [ %8, %3 ]
      ret i32 %10
    }
    

    ...which makes no mention of source-level variables like y, and KLEE is thus unable to follow them as it executes. This also means KLEE cannot report errors in terms of source-level variables either.

    Desired outcome

    Compilers like Clang can add debug info to the LLVM IR (enabled via the -g flag), which traditionally is emitted to a native binary and then read by debuggers like GDB, LLDB, etc. While current KLEE does use the file / line / column annotations in debug info when reporting stack traces, it could go further. As a future enhancement, it would be great for KLEE to use the variable debug info to map its IR-level program state up to source-level constructs when reporting to the user.

    Workaround

    While it's not the same as a real mapping of variables using debug info, you can get a modestly better view if your compiler names IR values based on source-level constructs. With Clang, you can add -fno-discard-value-names to achieve this, which gives something like the following...

    define i32 @example(i32 %n) local_unnamed_addr #0 {
    entry:
      %cmp7.not = icmp eq i32 %n, 0
      br i1 %cmp7.not, label %for.cond.cleanup, label %for.cond.cleanup.loopexit
    
    for.cond.cleanup.loopexit:                        ; preds = %entry
      %0 = add i32 %n, -1
      %1 = add i32 %n, 4
      %2 = mul i32 %0, %1
      %3 = add i32 %2, %n
      %4 = add i32 %3, 4
      br label %for.cond.cleanup
    
    for.cond.cleanup:                                 ; preds = %for.cond.cleanup.loopexit, %entry
      %y.0.lcssa = phi i32 [ 0, %entry ], [ %4, %for.cond.cleanup.loopexit ]
      ret i32 %y.0.lcssa
    }
    

    ...where some of the IR values (such as %n for the function argument) appear with their source-level names. To be clear, this only tweaks the names alone. An unoptimised version would also have a %y IR value for the source-level variable y, but that value was removed by the optimiser, so we no longer see that name here. Source-level variables move through numerous IR values and memory locations during computation, so this value naming workaround is not enough to follow source-level program state.

  • Compilation Fail

    Compilation Fail

    FAILED: lib/Module/CMakeFiles/kleeModule.dir/FunctionAlias.cpp.o
    /Library/Developer/CommandLineTools/usr/bin/c++ -DKLEE_UCLIBC_BCA_NAME=\"klee-uclibc.bca\" -D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -I/opt/local/include -I/Users/ dev/klee/build/include -I/Users/ dev/klee/include -I/usr/local/include -I/opt/homebrew/Cellar/stp/2.3.3_2/include -I/opt/homebrew/include -Wall -Wextra -Wno-unused-parameter -O2 -g -arch x86_64 -isysroot /Library/Developer/CommandLineTools/SDKs/MacOSX12.3.sdk -fno-exceptions -fno-rtti -fno-builtin-malloc -fno-builtin-calloc -fno-builtin-realloc -fno-builtin-free -std=gnu++17 -MD -MT lib/Module/CMakeFiles/kleeModule.dir/FunctionAlias.cpp.o -MF lib/Module/CMakeFiles/kleeModule.dir/FunctionAlias.cpp.o.d -o lib/Module/CMakeFiles/kleeModule.dir/FunctionAlias.cpp.o -c /Users/ dev/klee/lib/Module/FunctionAlias.cpp
    /Users/ dev/klee/lib/Module/FunctionAlias.cpp:140:17: error: no member named 'getElementType' in 'llvm::PointerType'
        type = ptr->getElementType();
               ~~~  ^
    1 error generated.
    [309/652] Building CXX object lib/Module/CMakeFiles/kleeModule.dir/IntrinsicCleaner.cpp.o
    /Users/ dev/klee/lib/Module/IntrinsicCleaner.cpp:100:56: warning: 'getPointerElementType' is deprecated: Deprecated without replacement, see https://llvm.org/docs/OpaquePointers.html for context and migration instructions [-Wdeprecated-declarations]
                  Builder.CreateLoad(castedSrc->getType()->getPointerElementType(),
                                                           ^
    /usr/local/include/llvm/IR/Type.h:377:5: note: 'getPointerElementType' has been explicitly marked deprecated here
      [[deprecated("Deprecated without replacement, see "
        ^
    /Users/ dev/klee/lib/Module/IntrinsicCleaner.cpp:109:44: warning: 'getPointerElementType' is deprecated: Deprecated without replacement, see https://llvm.org/docs/OpaquePointers.html for context and migration instructions [-Wdeprecated-declarations]
              auto pSrcType = pSrc->getType()->getPointerElementType();
                                               ^
    /usr/local/include/llvm/IR/Type.h:377:5: note: 'getPointerElementType' has been explicitly marked deprecated here
      [[deprecated("Deprecated without replacement, see "
        ^
    /Users/ dev/klee/lib/Module/IntrinsicCleaner.cpp:110:44: warning: 'getPointerElementType' is deprecated: Deprecated without replacement, see https://llvm.org/docs/OpaquePointers.html for context and migration instructions [-Wdeprecated-declarations]
              auto pDstType = pDst->getType()->getPointerElementType();
                                               ^
    /usr/local/include/llvm/IR/Type.h:377:5: note: 'getPointerElementType' has been explicitly marked deprecated here
      [[deprecated("Deprecated without replacement, see "
        ^
    3 warnings generated.
    ninja: build stopped: subcommand failed.
    

    I'm on

    clang version 16.0.0 (https://github.com/llvm/llvm-project.git ec83c7e358ecd7db9af2d980b6d528f5ea6865a4)
    Target: arm64-apple-darwin21.6.0
    Thread model: posix
    
  • Fixed some leaks in klee-replay

    Fixed some leaks in klee-replay

    Summary:

    These fixes some leaks in klee-replay reported in #1512. While these particular leaks are not important, we should get to a stage where LSan & ASan runs pass.

    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.
Maat is an open-source Dynamic Symbolic Execution and Binary Analysis framework
Maat is an open-source Dynamic Symbolic Execution and Binary Analysis framework

About Maat is an open-source Dynamic Symbolic Execution and Binary Analysis framework. It provides various functionalities such as symbolic execution,

Nov 17, 2022
SANM: A Symbolic Asymptotic Numerical Solver

SANM: A Symbolic Asymptotic Numerical Solver This repository is the official implementation of the SANM solver described in our paper to appear at SIG

Sep 22, 2022
Metamath - Meta mathematics. Symbolic functions and derivatives.

metamath Meta mathematic metamath is a tiny header-only library. It can be used for symbolic computations on single-variable functions, such as dynami

Nov 4, 2022
Mystikos is a set of tools for running applications in a hardware trusted execution environment (TEE)
Mystikos is a set of tools for running applications in a hardware trusted execution environment (TEE)

Mystikos is a set of tools for running applications in a hardware trusted execution environment (TEE). The current release supports Intel ® SGX while other TEEs may be supported in future releases. Linux is also a supported target, though only suitable for testing purposes as it provides no additional protection.

Nov 21, 2022
PoC for CVE-2021-28476 a guest-to-host "Hyper-V Remote Code Execution Vulnerability" in vmswitch.sys.
PoC for CVE-2021-28476 a guest-to-host

CVE-2021-28476: a guest-to-host "Microsoft Hyper-V Remote Code Execution Vulnerability" in vmswitch.sys. This is a proof of concept for CVE-2021-28476

Nov 26, 2022
A refactored Proof-of-concept originally developed in 2017 to print all function calls with their arguments data types and values using Ptrace during program execution.

print-function-args-debugger A refactored Proof-of-concept originally developed in 2017 to print all function calls with their arguments data types an

Jun 17, 2022
x64 Windows kernel code execution via user-mode, arbitrary syscall, vulnerable IOCTLs demonstration
x64 Windows kernel code execution via user-mode, arbitrary syscall, vulnerable IOCTLs demonstration

anycall x64 Windows kernel code execution via user-mode, arbitrary syscall, vulnerable IOCTLs demonstration Read: https://www.godeye.club/2021/05/14/0

Nov 19, 2022
Nov 19, 2022
New lateral movement technique by abusing Windows Perception Simulation Service to achieve DLL hijacking code execution.
New lateral movement technique by abusing Windows Perception Simulation Service to achieve DLL hijacking code execution.

BOF - Lateral movement technique by abusing Windows Perception Simulation Service to achieve DLL hijacking ServiceMove is a POC code for an interestin

Nov 14, 2022
Elven relativism -- relocation and execution of aarch64 ELF relocatable objects (REL)
Elven relativism -- relocation and execution of aarch64 ELF relocatable objects (REL)

elvenrel Elven Relativism -- relocation and execution of aarch64 ELF relocatable objects (REL) on Linux and macOS. Program loads a multitude of ELF RE

Oct 15, 2022
RR4J is a tool that records java execution and later allows developers to replay locally.
RR4J is a tool that records java execution and later allows developers to replay locally.

RR4J [Record Replay 4 Java] RR4J is a tool that records java execution and later allows developers to replay locally. The tool solves one of the chall

Oct 31, 2022
CPU Performance Evaluation and Execution Time Prediction Using Narrow Spectrum Benchmarking

This is a simple implementation of Saavedra-Barrera's paper SAAVEDRA-BARRERA R H. CPU Performance Evaluation and Execution Time Prediction Using Narrow Spectrum Benchmarking[D/OL]. UCB/CSD92-684. EECS Department, University of California, Berkeley, 1992.

Jan 27, 2022
A Windows user-mode shellcode execution tool that demonstrates various techniques that malware uses
A Windows user-mode shellcode execution tool that demonstrates various techniques that malware uses

Jektor Toolkit v1.0 This utility focuses on shellcode injection techniques to demonstrate methods that malware may use to execute shellcode on a victi

Sep 5, 2022
Inject dll to cmd.exe to prevent file execution.

Console-Process-Execution Inject dll to cmd.exe to prevent file execution. Requierments: Microsoft Detours Library - https://github.com/microsoft/Deto

Sep 25, 2022
A pre-boot execution environment for Apple boards built on top of checkra1n

archOS A pre-boot execution environment for Apple boards built on top of checkra1n - currently based off the Checkra1n/PongoOS Repo. Building on macOS

Jan 17, 2022
This is a very short tool that predicts the number of cycles and execution time in Fulcrum when the operands and operations are known.

fulcrum-analytical-tool This is a very short tool that predicts the number of cycles and execution time in Fulcrum when the operands and operations ar

Feb 6, 2022
A general solution to simulate execution of virtualized instructions (vmprotect/themida, etc.).
A general solution to simulate execution of virtualized instructions (vmprotect/themida, etc.).

vmp_runner A general solution to simulate execution of virtualized instructions (vmprotect/themida, etc.) based on Unicorn. 一个基于Unicorn模拟执行虚拟化指令(vmpro

Nov 7, 2022
Love 6's Regular Expression Engine. Support Concat/Select/Closure Basic function. Hope u can enjoy this tiny engine :)
Love 6's Regular Expression Engine. Support Concat/Select/Closure Basic function. Hope u can enjoy this tiny engine :)

Regex_Engine Love 6's Blog Website: https://love6.blog.csdn.net/ Love 6's Regular Expression Engine Hope u can love my tiny regex engine :) maybe a fe

May 24, 2022
Sword Engine is a fork of Psych Engine that plans on adding more features and quality of life improvements.
Sword Engine is a fork of Psych Engine that plans on adding more features and quality of life improvements.

⚠️ WARNING: This README is currently incomplete, This warning will be removed once it's complete. Friday Night Funkin' - Sword Engine Sword Engine is

Jul 9, 2022