forked from Geof23/Gklee
-
Notifications
You must be signed in to change notification settings - Fork 0
/
README
100 lines (70 loc) · 4.4 KB
/
README
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
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]