From 52949d8150332edba6e7ba579552dbd8c2a856e1 Mon Sep 17 00:00:00 2001 From: Daniel Dunbar Date: Sun, 2 Aug 2009 23:12:39 +0000 Subject: Add instructions on how to build with POSIX/uClibc support to GetStarted page. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@77924 91177308-0d34-0410-b5e6-96231b3b80d8 --- www/GetStarted.html | 117 +++++++++++++++++++++++++++++++++------------------- 1 file changed, 75 insertions(+), 42 deletions(-) (limited to 'www/GetStarted.html') diff --git a/www/GetStarted.html b/www/GetStarted.html index 5c445059..ee78ff44 100644 --- a/www/GetStarted.html +++ b/www/GetStarted.html @@ -17,7 +17,7 @@ -

Building KLEE and Working with the Code

+

Building KLEE

If you would like to try KLEE, the current procedure for building is below.

@@ -25,64 +25,65 @@ KLEE is built on LLVM; the first steps are to get a working LLVM installation. See Getting Started with the LLVM System for more information. -

NOTE: KLEE is only currently tested on Linux and Darwin x86-32 targets, -using LLVM top-of-tree. KLEE will not work with an older LLVM (e.g., 2.5), and is -currently untested on any x86-64 target, although we hope to add support for -them soon.

+

NOTE: KLEE is only currently tested on Linux and Darwin x86-32 +targets, using LLVM top-of-tree. KLEE will not work with an older LLVM (e.g., +2.5). We are currently working on full support for Linux and Darwin x86-64 +targets.

    -
  1. Install llvm-gcc:
  2. - - -
  3. Checkout - and build LLVM from SVN head (LLVM 2.5 will not work): - -
    - svn co http://llvm.org/svn/llvm-project/llvm/trunk llvm
    - cd llvm
    - ./configure --enable-optimized
    - make -
    - -(the --enable-optimized configure argument is not -necessary, but KLEE runs very slowly in Debug mode). +
  4. Install llvm-gcc: +
      +
    • Download and install the LLVM 2.5 release of llvm-gcc + from here. Add + llvm-gcc to your PATH. It is important to do this first + so that llvm-gcc is found in subsequent configure + steps. llvm-gcc will be used later to compile programs that KLEE + can execute.
    • +
  5. +
  6. Checkout + and build LLVM from SVN head (LLVM 2.5 will not work): + +
    + $ svn co http://llvm.org/svn/llvm-project/llvm/trunk llvm
    + $ cd llvm
    + $ ./configure --enable-optimized
    + $ make +
    + + (the --enable-optimized configure argument is not necessary, but + KLEE runs very slowly in Debug mode). +
  7. +
  8. Checkout KLEE (to any path you like):
    - svn co http://llvm.org/svn/llvm-project/klee/trunk klee + $ svn co http://llvm.org/svn/llvm-project/klee/trunk klee
  9. Configure KLEE (from the KLEE source directory):
    - ./configure --with-llvm=path/to/llvm + $ ./configure --with-llvm=path/to/llvm

    This assumes that you compiled LLVM in-place. If you used a different directory for the object files then use:

    - ./configure --with-llvmsrc=path/to/llvm/src --with-llvmobj=path/to/llvm/obj + $ ./configure --with-llvmsrc=path/to/llvm/src --with-llvmobj=path/to/llvm/obj
  10. Build KLEE (from the KLEE source directory):
    - make ENABLE_OPTIMIZED=1 + $ make ENABLE_OPTIMIZED=1
  11. Run the regression suite to verify your build:
    - make check
    - make unittests
    + $ make check
    + $ make unittests
  12. @@ -90,16 +91,48 @@ necessary, but KLEE runs very slowly in Debug mode). to try KLEE.
- - - - - +

Building KLEE with POSIX runtime support

+ +

The steps above are enough for building and testing KLEE on closed programs +(programs that don't use any external code such as C library +functions). However, if you want to use KLEE to run real programs you will want +to enable the KLEE POSIX runtime, which is built on top of the uClibc C +library.

+ +
    +
  1. Download KLEE's uClibc: +
      +
    • + KLEE uses a version of uClibc which has + been modified slightly for use with KLEE. It is available for download + here: klee-uclibc-0.01.tgz. +
    • +
    +
  2. - - - - +
  3. Build uClibc with llvm-gcc: +
    + $ tar zxvf klee-uclibc-0.01.tgz
    + $ ./configure --with-llvm=path/to/llvm
    + $ make
    +
    + +

    NOTE: KLEE's uClibc is shipped in a pre-configured for x86-32. If + you are on a different target (e.g. x86-64), you will need to run 'make + config' and select the correct target. The defaults for the other uClibc + configuration variables should be fine.

    +

  4. + +
  5. Configure KLEE with uClibc/POSIX support: +
    + $ ./configure --with-llvm=path/to/llvm --with-uclibc=path/to/klee-uclibc --enable-posix-runtime +
    +
  6. + +
  7. Rebuild KLEE and run make check and verify that the POSIX tests + run correctly. +
  8. +
-- cgit 1.4.1