forked from nidhugg/nidhugg
-
Notifications
You must be signed in to change notification settings - Fork 1
/
README
226 lines (159 loc) · 6.91 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
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
Nidhugg is a bug-finding tool which targets bugs caused by concurrency
and relaxed memory consistency in concurrent programs. It works on the
level of LLVM internal representation, which means that it can be used
for programs written in languages such as C or C++.
Currently Nidhugg supports the SC, TSO, PSO, POWER and ARM memory
models. Target programs should use pthreads for concurrency, and each
thread should be deterministic when run in isolation.
Documentation
*************
The main documentation can be found in the git repository at
https://github.com/nidhugg/nidhugg/blob/master/doc/manual.pdf , or in
the source at doc/manual.pdf, or if installed at
PREFIX/share/doc/nidhugg/manual.pdf .
Installation
************
Nidhugg can be compiled and installed on UNIX-like systems.
Requirements
============
1. A C++ compiler supporting C++14. For example g++ version 6 or
higher, or clang++ version 3.8 or higher. (For compiling the
tool Nidhugg.)
2. The C compiler clang. (For use by Nidhugg as a frontend for C
compilation.)
3. Standard C/C++ libraries.
4. GNU Autotools (autoconf & automake).
5. Python version 3.0 or higher.
6. The LLVM library and headers, version 3.8 or higher. If you are
compiling the LLVM library from sources, see Compiling LLVM
below.
7. Foreign Function Interface (libffi) library and headers.
8. Boost Unit Test Framework, version 1.64 or higher.
(9). pkg-config, for generating a fully-featured configure script,
capable of autodetecting the flags needed for libffi.
Optional, but recommended.
(10). Optional: Valgrind
(11). Optional: For documentation: pdflatex
(with packages article, inputenc, amssymb)
For Users of Debian-like Systems
--------------------------------
On a Debian-like Linux distribution (such as e.g. Ubuntu), satisfy
the requirements by installing the following packages:
Mandatory:
clang, libc6, libc6-dev, libstdc++6, autoconf, automake, python3,
llvm, llvm-dev, libffi-dev, libboost-test-dev, libboost-system-dev,
pkg-config
Optional:
valgrind, texlive-latex-base, texlive-base
Getting Nidhugg
===============
Git users can clone Nidhugg as follows:
$ git clone https://github.com/nidhugg/nidhugg.git
Non git users may find it easier to download the latest revision as
a zip archive:
https://github.com/nidhugg/nidhugg/archive/master.zip
Basic Installation
==================
The following assumes that you are in a shell in the main directory
of Nidhugg.
1. Use GNU Autotools to generate the configure script:
$ autoreconf --install
2. Build as usual. See Installation Options below for options about e.g.
installation location.
$ ./configure
$ make
3. Install:
$ make install
4. Optionally run test suite (Boost Unit Test Framework required):
$ make test
or (Valgrind required)
$ make valtest
Installation Options
====================
The configure script is built with GNU autotools, and should accept
the usual options and environment variables. This section outlines
some of the typical use cases.
Changing Installation Directory
-------------------------------
The command 'make install' will install Nidhugg and its
documentation in the directories which are standard on your
system. To override this behavior add the switch --prefix to the
'./configure' command:
$ ./configure --prefix=/your/desired/install/path
Specifying Compiler
-------------------
When the configure script is invoked, it will by GNU autotools
magic determine which C++ compiler will be used during
compilation. In case e.g. your default compiler does not support
C++14, but you have the compiler g++-6 installed at a
non-standard location you may want to override this. In order to do
so, specify the path to g++-6 in CXX when invoking the
'./configure' command:
$ ./configure CXX='/path/to/g++-6'
Specifying LLVM Installation
----------------------------
If the configure script does not find your LLVM installation, or
does not find the installation which you want to use (see output
from configure), you may specify the installation location of LLVM
with the --with-llvm switch. Below, /path/to/llvm should be the
path to the root of the LLVM installation, i.e. the directory which
contains bin/llvm-config and lib/libllvm.a .
$ ./configure --with-llvm='/path/to/llvm'
(Re)building PDF Documentation
------------------------------
By default, make will not rebuild the documentation from LaTeX
sources. This allows the typical user to simply use the latest PDF
pushed to the git repository. In order to force (re)building of the
documentation, configure with the switch
--enable-build-documentation . This requires LaTeX to be installed.
$ ./configure --enable-build-documentation
Compiling LLVM
==============
If you are a user of Nidhugg, we recommend you use a release build of
LLVM. You can also speed up the build by disabling all the backends.
$ cd llvm-*.src
$ mkdir build && cd build
$ cmake -DCMAKE_INSTALL_PREFIX=/your/llvm/install/path \
-DCMAKE_BUILD_TYPE=Release \
-DLLVM_TARGETS_TO_BUILD="" -DLLVM_LINK_LLVM_DYLIB=ON ..
$ make
$ make install
Compiling LLVM for Debugging or Developing Nidhugg
**************************************************
If you are developing Nidhugg or are troubleshooting a bug in
Nidhugg, we recommend you use a debug build of LLVM, as this will
allow you to build an assertions-enabled build of Nidhugg.
$ cd llvm-*.src
$ mkdir build && cd build
$ cmake -DCMAKE_INSTALL_PREFIX=/your/llvm/install/path \
-DCMAKE_BUILD_TYPE=RelWithDebInfo \
-DLLVM_ENABLE_ASSERTIONS=ON \
-DLLVM_TARGETS_TO_BUILD="" -DLLVM_LINK_LLVM_DYLIB=ON \
-DLLVM_OPTIMIZED_TABLEGEN=ON ..
$ make
$ make install
License
*******
Nidhugg is licensed under GPLv3. See COPYING.
Nidhugg is free software: you can redistribute it and/or modify it
under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
Nidhugg is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
General Public License for more details.
LLVM License
============
Part of the code in the files listed below originate in the LLVM
Compiler Framework (http://llvm.org, version 3.4.1). Those parts
are licensed under the University of Illinois/NCSA Open Source
License as well as under GPLv3. See LLVMLICENSE.TXT.
src/Interpreter.h
src/Interpreter.cpp
src/Execution.cpp
src/ExternalFunctions.cpp
Contact / Bug Report
********************
Feedback, questions or bug reports should be reported as issues on
Github.