GKLEE is a symbolic analyser and test generator tailored for CUDA C++ programs,
it supports almost all of CUDA intrinsic functions in kernel code and majority 
of CUDA runtimes in host code. For more details, please visit GKLEE's homepage:
www.cs.utah.edu/fv/GKLEE

Please refer to the tutorial on this wiki, located here:
https://github.com/Geof23/Gklee/wiki/flows_tutorial

This is a fork of the original Github version of GKLEE, https://github.com/PengPengHub/Gklee

=============== Obtain and Build GKLEE ToolChain, and REQUIREMENTS ============

1. Installing GKLEE requires that you have CMake installed on your system.
   Please be sure to have at least version 3.0.  You may download CMake
   from this location: http://www.cmake.org/download/.  Also, you must have
   git installed to obtain the sources.  Obviously, an internet connection
   is also needed.

2. Choose a location for the GKLEE source.  You may have already done so,
   but if not, obtain the GKLEE package from github.
   a. CD to the location that you'd like for the GKLEE directory
   b. execute 'git clone https://github.com/Geof23/Gklee

3. Choose a build directory (for the out-of-source build).  For convenience,
   you may do it within your top level GKLEE directory:  
   a. cd Gklee
   b. mkdir build && cd build
   
*** IMPORTANT ***
    If your system has multiple versions of gcc installed, you must tell CMake
    to use the most recent one.  Here's a procedure:
    a. from your terminal (running Bash) type 'gcc[tab - tab]'
    b. if you see a list that includes something like 'gcc gcc-[version number 1] 
       gcc-[version number 2]' you have multiple installations.
    (This problem will be eliminated in future versions of GKLEE)
    d. CSY: For machine with python3 as the defualt python interpreter, the CMakeLists.txt needed to be modified at Gklee/llvm/src/LLVM/CMakeLists.txt, line 290. Change the CMake variable 'PYTHON_EXECUTABLE' into 'python2'
***

4. Generate the Makefiles: 
   a. If you don't have multiple gcc versions, you may simply execute 'cmake ..'
      (assuming you created your build directory under the top level Gklee folder --
      otherwise 'cmake [path to Gklee top level folder]'
   b. If you do have multiple gcc versions, inform CMake by calling like this, 
      assuming your latest gcc version is gcc-4.9:
      'cmake gcc=gcc-4.9 g++=g++4.9 [path to Gklee]'
   c. CSY: modify Gklee/llvm/src/LLVM/projects/complier-rt/asan/asan_linux.cc after first make, add
      > #include <signal.h>  

5. Build Gklee: execute 'make -j [number of cores to build with]'

======================= Set Environment Variables =========================

1. After you finish the instalation, please customize the environment variables
   in the following two ways:
 
   -- Add the following lines to your /home/[username]/.bashrc file
   -- Create an environment file including the following lines

   export KLEE_HOME_DIR=/Path/To/Gklee
   export PATH=$KLEE_HOME_DIR/bin:$PATH


======================= Run GKLEE =========================

After building GKLEE and setting environment variables properly, you could run GKLEE.

1. Compile your CUDA programs into LLVM bytecode with the command: 

   gklee-nvcc xxx.cu [-o executable] [other options used in nvcc ...] 
   
   NOTE: if you do not specify a executable name, gklee-nvcc will use the prefix 
   of the CUDA program as the default name

2. Run your program with GKLEE command

   gklee executable [Normal Mode] 
   gklee --symbolic-config executable [Parametric Flow Mode] 

3. The test cases will be generated in the same dir where you execute gklee, 
   and appear as 'klee-out-[number]' and 'klee-last'.

======================== Using TaintAnalysis: Gklee 'SESA' ============================

The taint analyser consists of three llvm passes, which performs a combination of 
use-def chain analysis and alias analysis to perform taint analysis on CUDA kernels.

To run the analyser:

sesa < [input_llvm_bytecode] > [output_llvm_bytecode]

1. The taint analyser outputs informative messages on which variables shall 
be symbolized in a file named "summary.txt"

2. The taint analyser annotates the input llvm bytecode with LLVM metadata 
and generates the new llvm bytecode containing LLVM annotations that are used 
to prune redundant flows in the symbolic execution stage.

3. To run this annotated bytecode in Gklee, you need to add a command line option :

gklee --symbolic-config --race-prune [path to annotated bytecode]