From 4ad66e2e348597ffb814c23232d2ca453785f9d6 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Thu, 5 Apr 2012 17:20:15 +0000 Subject: Updated and simplified installation instructions. Switched to LLVM 2.9 and to SVN version 940 of STP. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@154107 91177308-0d34-0410-b5e6-96231b3b80d8 --- www/GetStarted.html | 195 ++++++++++++++++++++++++---------------------------- 1 file changed, 88 insertions(+), 107 deletions(-) (limited to 'www/GetStarted.html') diff --git a/www/GetStarted.html b/www/GetStarted.html index 7ce750cc..6de3e429 100644 --- a/www/GetStarted.html +++ b/www/GetStarted.html @@ -20,8 +20,6 @@

1. Trying out KLEE without installing any dependencies
2. Building KLEE
-3. Building KLEE with POSIX runtime support
-4. Building KLEE with a more recent version of STP

@@ -54,24 +52,34 @@ The only requirement is that you are running a reasonably-modern x86-Linux distr

Building KLEE

-

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

-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 and x86-64 targets, using LLVM 2.8. KLEE will not work with an -older LLVM (e.g., 2.5), and might not work with newer versions of LLVM -(e.g., 2.9 or 3.0)

+

The current procedure for building is outlined below.

    +
  1. Build LLVM 2.9: + +

    +KLEE is built on top of LLVM; the first +steps are to get a working LLVM installation. +See Getting Started +with the LLVM System for more information. +

    + +

    +NOTE: KLEE is currently tested only on Linux x86-32 and x86-64 +targets, using LLVM 2.9. KLEE will not work with older LLVM +versions (e.g., 2.5), and might not work with newer versions (e.g., +3.0). +

    + + +
    1. Install llvm-gcc:
        -
      • Download and install the LLVM 2.8 release of llvm-gcc +
      • Download and install the LLVM 2.9 release of llvm-gcc from here. -
        Add llvm-gcc to your PATH. It +
        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 @@ -84,14 +92,11 @@ older LLVM (e.g., 2.5), and might not work with newer versions of LLVM
      2. -
    2. Download and build - LLVM 2.8 (you may also use SVN head, but klee may not always be - up-to-date with LLVM API changes). - +
    3. Download and build LLVM 2.9:
      - $ curl -O http://llvm.org/releases/2.8/llvm-2.8.tgz
      - $ tar zxvf llvm-2.8.tgz
      - $ cd llvm-2.8
      + $ curl -O http://llvm.org/releases/2.9/llvm-2.9.tgz
      + $ tar zxvf llvm-2.9.tgz
      + $ cd llvm-2.9
      $ ./configure --enable-optimized --enable-assertions
      $ make
      @@ -99,62 +104,44 @@ older LLVM (e.g., 2.5), and might not work with newer versions of LLVM (the --enable-optimized configure argument is not necessary, but KLEE runs very slowly in Debug mode).
      4. - -
    4. Checkout KLEE (to any path you like): -
      - $ svn co http://llvm.org/svn/llvm-project/klee/trunk klee -
      - Alternatively, if you prefer to use git there is also a - read-only git mirror, which syncs automatically with each - Subversion commit. You can do a git clone of KLEE via: -
      - $ git clone http://llvm.org/git/klee.git -
      -
      5. - -
    5. Configure KLEE (from the KLEE source directory): -
      - $ ./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 -
      -
      6. + +
    -
  2. Build KLEE (from the KLEE source directory): -
    - $ make ENABLE_OPTIMIZED=1 -
    -
    3. -
  3. Run the regression suite to verify your build: -
    - $ make check
    - $ make unittests
    -
    -
    4. +
  4. Build STP: -
  5. You're ready to go! Go to the Tutorials page - to try KLEE.
    6. -
+

KLEE is based on +the STP +constraint solver. STP does not make frequent releases, and its +Subversion repository is under constant development and may be +unstable. The instructions below are for a particular revision which +we have used successfully, but you can try a more recent revision by +changing or removing the -r argument to the svn co +command. (Please let us know if you have successfully and extensively +used KLEE with a more recent version of STP.) +

-

Building KLEE with POSIX runtime support

+
+ $ svn co -r 940 https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp stp
+ $ cd stp
+ $ ./scripts/configure --with-prefix=path/to/stp/install --with-cryptominisat2
+ $ make OPTIMIZE=-O2 CFLAGS_M32= install +
+ -

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.

+
  • [Optional] Build uclibc and the POSIX environment model: -
      -
    1. Download KLEE's uClibc: -
        -
      • - KLEE uses a version of uClibc - which has been modified slightly for use with KLEE. +

        +By default, KLEE works 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 our purposes.
          • A version that works on 32-bit Linux can be found here @@ -163,66 +150,60 @@ library.

            here
          -
          2. -
    2. Build uClibc with llvm-gcc:
      - $ tar zxvf klee-uclibc-0.01.tgz
      + $ tar zxvf klee-uclibc-0.02.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.

      +

      NOTE: If you are on a different target (i.e., not i386 + or x64), you will need to run make config and select the + correct target. The defaults for the other uClibc configuration + variables should be fine.

      3. -
    3. Configure KLEE with uClibc/POSIX support: +
    + + +
  • Checkout KLEE (to any path you like):
    - $ ./configure --with-llvm=path/to/llvm --with-uclibc=path/to/klee-uclibc --enable-posix-runtime + $ svn co http://llvm.org/svn/llvm-project/klee/trunk klee +
    + Alternatively, if you prefer to use git there is also a + read-only git mirror, which syncs automatically with each + Subversion commit. You can do a git clone of KLEE via: +
    + $ git clone http://llvm.org/git/klee.git
    • - -
  • Rebuild KLEE and run make check and verify that the POSIX tests - run correctly. + +
  • Configure KLEE: +

    From the KLEE source directory, run:

    +
    + $ ./configure --with-llvm=path/to/llvm --with-stp=path/to/stp/install --with-uclibc=path/to/klee-uclibc --enable-posix-runtime +
    + +

    NOTE: If you skipped step 3, simply remove the --with-uclibc and --enable-posix-runtime options.

    • - - -

    Building KLEE with a more recent version of STP

    -

    If your benchmarks are running slowly or not terminating it may -be worth trying a more recent version of KLEE's constraint solver -STP, -which offers performance improvements over the version supplied -with KLEE.

    - -

    STP does not make frequent releases, and its Subversion repository -is under constant development and may be unstable. The instructions -below are for a particular revision which is known to pass the KLEE -test suite, but you can try a more recent revision (at your own risk) -by changing or removing the -r argument to the svn -co command.

    - -
      -
    1. Download and build STP. +
    2. Build KLEE:
      - $ svn co -r 940 https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp stp
      - $ cd stp
      - $ scripts/configure --with-prefix=path/to/stp/inst --with-cryptominisat2
      - $ make OPTIMIZE=-O2 CFLAGS_M32= install + $ make ENABLE_OPTIMIZED=1
      3. -
    3. Configure KLEE: +
    4. Run the regression suite to verify your build:
      - $ ./configure --with-llvm=path/to/llvm --with-stp=path/to/stp/inst + $ make check
      +
      5. -
    5. Rebuild KLEE.
      6. +
    6. You're ready to go! Go to the Tutorials page + to try KLEE.
    -- cgit 1.4.1