From e4ce97b38411de5d972ee4cf89cede342b7f82f0 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Mon, 1 Jul 2013 18:01:01 +0000 Subject: Developer's guide by Dan Liew, with a few changes from me. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@185351 91177308-0d34-0410-b5e6-96231b3b80d8 --- www/Documentation.html | 4 ++ www/GetInvolved.html | 14 ++++-- www/developers-guide.html | 114 ++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 127 insertions(+), 5 deletions(-) create mode 100644 www/developers-guide.html diff --git a/www/Documentation.html b/www/Documentation.html index 8c19b36e..538cada7 100644 --- a/www/Documentation.html +++ b/www/Documentation.html @@ -47,6 +47,10 @@ Some information about the Coreutils experiments presented in our KLEE OSDI'08 paper. +
  • + Developer's Guide: + A brief guide on working with the KLEE source code. +
    • diff --git a/www/GetInvolved.html b/www/GetInvolved.html index 0cde1299..2ff2b5ee 100644 --- a/www/GetInvolved.html +++ b/www/GetInvolved.html @@ -36,12 +36,16 @@ and also fill a bug report on Bugzilla u

    Working with the Code

    -

    KLEE developer documentation is written in doxygen and you may have it online here: - doxygen - (this is updated nightly from the source tree).

    +

    You should first check KLEE's developer's guide.

    + +

    Developer documentation is written in + doxygen. + +

    + +

    -

    Many parts of KLEE rely on the LLVM infrastructure, you can find more -information about programming for LLVM here: +

    Many parts of KLEE rely on the LLVM infrastructure, so you might also want to look at LLVM's General Programming Documentation.

    diff --git a/www/developers-guide.html b/www/developers-guide.html new file mode 100644 index 00000000..9c0ff719 --- /dev/null +++ b/www/developers-guide.html @@ -0,0 +1,114 @@ + + + + + KLEE - Getting Started + + + + + + + +
    + +

    KLEE Developer's Guide

    + +

    This guide covers several areas of KLEE that may not be imediately obvious to new developers.

    + +

    + 1. KLEE's Build System
    + 2. KLEE's Test Framework
    + 3. Miscellaneous
    +

    + +

    KLEE's Build System

    +

    KLEE uses LLVM's ability to build third-party projects, which is described here. The build system uses GNU Autoconf and AutoHeader to configure the build, but does not use the rest of GNU Autotools (e.g. automake).

    + +

    LLVM's build system supports out-of-source builds and therefore so does KLEE. It is highly recommended you take advantage of this. For example, you could create three builds (Release, Release with debug symbols, Debug) + that all use the same source tree. This allows you keep your source tree clean and allows multiple configurations to be tested from a single source tree.

    + +

    Setting up a debug build of KLEE

    +

    Setting up a debug build of KLEE (we'll assume it is an out-of-source build) is very similar to the build process described in Getting Started, with the exception of steps 6 and 7.

    + +
      +
    1. Now we will configure KLEE. Notice that we are forcing the compiler to produce unoptimised code, this isn't the default behaviour. +
      + $ mkdir path/to/build-dir
      + $ cd path/to/build-dir
      + $ CXXFLAGS="-g -O0" CFLAGS="-g -O0" path/to/source-dir/configure --with-llvm=path/to/llvm --with-stp=path/to/stp/install --with-uclibc=path/to/klee-uclibc --enable-posix-runtime --with-runtime=Debug+Asserts +
      + Note if you're using an out-of-source build of LLVM you will need to use --with-llvmsrc= and --with-llvmobj= configure options instead of --with-llvm= +
      2. +
    2. Now we can build KLEE. +
      + $ make -j +
      + Note that we are using the -j option of make to speed up the compilation process. +
      3. +
    + +

    Note that KLEE depends on LLVM and STP. If you need to debug KLEE's calls to that code, then you will need to build LLVM/STP with debug support too.

    + +

    Adding a class

    +

    Because KLEE uses LLVM's build system, adding a class to an existing library in KLEE is very simple. For example, to add a class to libkleaverExpr, the following steps would be followed: +

      +
    1. Create the header file (.h) for the class and place it somewhere inside include/ (the location isn't really important except that #include is relative to the include/ directory). +
      2. +
    2. Create the source file (.cpp) for the class place it in lib/Expr/. You can confirm that the library in which your new class will be included is kleaverExpr by looking at the Makefile in lib/Expr. +
      3. +
    + That's it! Now LLVM's build system will detect the new .cpp file and add it to the library that is generated when you run make. +

    + +

    Building code documentation

    +

    KLEE uses Doxygen to generate code documentation. To generate it yourself you can run the following from KLEE's build directory root. +

    + $ make doxygen +
    + This will generate documentation in path/to/build-dir/docs/doxygen/ folder. You can also find KLEE's latest official code documentation here +

    + + +

    KLEE's Test Framework

    +

    KLEE uses LLVM's testing infrastructure for its tests, which itself uses DejaGnu. These are the tests that are executed by the make check command. Some documentation on LLVM's testing infrastructure can be found here. +

    +

    KLEE's tests are currently divided into categories, each of which is a subdirectory in test/ in the source tree (e.g. test/Feature) . The dg.exp file in each subdirectory instructs the LLVM testing infrastructure which files in the subdirectory are to be used as tests. For example, test/Expr/dg.exp contains: +

    + load_lib llvm.exp

    + + RunLLVMTests [lsort [glob -nocomplain $srcdir/$subdir/*.{pc}]] +
    + This instructs the testing infrastructure that every .pc file in test/Expr should be used as a test. +

    +

    The actions performed in each test are specified by special comments in the file. For example, in test/Feature/ByteSwap.c the first two lines are +

    + // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
    + // RUN: %klee --libc=klee --exit-on-error %t1.bc
    +
    + This first runs llvm-gcc on the source file (%s) and generates a temporary file (%t1.bc). Then KLEE is executed on this generated temporary file. If either program returns a non-zero exit code (or crashes) then + test is considered to have failed. More information on the available substitution variables (such as %s) can be found here. +

    + +

    It is useful to be able to execute just a single test rather than all of them. KLEE provides a makefile target for doing so which can used as shown below. Note that category/test-name should be the test that one would like to execute, e.g. Feature/ByteSwap.c. +

    + $ cd path/to/build-dir/test
    + $ make check-one TESTONE=path/to/source-dir/test/category/test-name +
    +

    + + +

    Miscellaneous

    +

    Writing messages to standard error

    +

    The kleeCore library (lib/Core) provides several functions that can be used similarly to printf() in C. See lib/Core/Common.h for more information. +

    + +

    Adding a command line option to a tool

    +

    KLEE uses LLVM's CommandLine library for adding options to tools in KLEE, which is well documented here. See lib/core/Executor.cpp for examples.

    + +
    + +
    + + -- cgit 1.4.1