-
Notifications
You must be signed in to change notification settings - Fork 0
/
HACKING
623 lines (454 loc) · 19.4 KB
/
HACKING
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
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
Bootstraping from the GIT repository
====================================
(If you are building from a tarball, skip this section.)
Spot's gitlab page is at
https://gitlab.lrde.epita.fr/spot/spot
The GIT repository can be cloned with
git clone https://gitlab.lrde.epita.fr/spot/spot.git
Some files in SPOT's source tree are generated. They are distributed
so that users do not need to tools to rebuild them, but we don't keep
all of them under GIT because it can generate lots of changes or
conflicts.
Here are the tools you need to bootstrap the GIT tree, or more
generally if you plan to regenerate some of the generated files.
(None of these tools are required by end users installing a tarball
since the generated files they produce are distributed.)
GNU Autoconf >= 2.61
GNU Automake >= 1.11
GNU Libtool >= 2.4
GNU Flex (the version seems to matters, we used 2.5.35)
GNU Bison >= 3.0
GNU Emacs (preferably >= 24 but it may work with older versions)
Groff (a.k.a. GNU troff) >= 1.20
SWIG >= 3.0 (for its better C++11 support)
Doxygen >= 1.4.0
Perl, with its Gettext module (it might be called something like
liblocale-gettext-perl or p5-locale-gettext in your distribution)
A complete LaTeX distribution, including latexmk and extra fonts
like dsfont.sty.
ImageMagick
Python >= 3.3, IPython >= 2.3
GraphViz
Java >= 1.7 (needed to run PlantUML while generating the doc)
wget or curl (needed to download PlantUML)
The following additional tools are used if they are present, or
only for certain operations (like releases):
pandoc used during Debian packaging for the conversion of
IPython notebooks to html
optipng used during "make dist" if present, to optimize
distributed png images
R used by some example in the documentation (the
documentation will still compile without R, but that
example will appear broken)
ltl2ba used in the generated documentation and the test suite
ltl2dstar likewise
ltl3dra likewise
spin likewise
glucose >= 3.0 likewise
lbtt >= 1.2.1a used in the test suite (ltlcross is now more
powerful, but additional tests do not hurt)
If you use Debian or a similar distribution, the Dockerfile at
https://github.com/adl/spot-docker/blob/master/debuild/Dockerfile
lists all the Debian packages that should be installed to build
Debian packages out of the GIT tree. Additionally, the script
https://github.com/adl/spot-docker/blob/master/debuild/install.sh
installs the third-party tools that do not have Debian packages.
Bootstrap the GIT tree by running
% autoreconf -vfi
and then go on with the usual
% ./configure
% make
Tricks
======
Avoiding Doxygen runs
---------------------
When there is no documentation built (e.g., after a fresh checkout
of the GIT tree), when the configure.ac file has changed, or when
the Doxygen configuration has changed, the doc will be rebuilt.
This can take quite some time, even though recent version of Doxygen
have started to parallelize things. If you have no interest
in generating the documentation, just use the "magic touch":
touch doc/stamp
Do that right before running make. The timestamp of doc/stamp
is compared to configure.ac and Doxygen.in to decide if the
documentation is out-of-date. The above command pretends the
documentation has just been built.
Avoiding org-mode runs
----------------------
The files in doc/org/ are org-mode files (a mode of Emacs that we use
to author documents that embed executable snippets), they are used to
generate the doc/userdoc/ HTML documentation. If for some reason you
don't have emacs, or you simply want not to rebuild these files, use
another "magic touch":
touch doc/org-stamp
Silent Building with automake
-----------------------------
The classical makefiles generated by automake are very verbose during
build beacause they prints the full command line of every stage. This
verbosity is very usefull to help (remotely) users to compile
Spot. Nonetheless, for developpers, these compilations lines may be
annoying. To reduce this verbosity, just run:
make V=0
Debugging Libtool executables
-----------------------------
The executables generated in the various testsuite directories of Spot
are not real binaries. Because we use libtool to compile the spot
library in a portable manner, these executables are just scripts that
run the actual binary after setting some environment variables so that
the OS can find the library in the build tree.
A consequence is that tools like gdb or valgrind, that expect to work
on a binary, will be confused by the script. Example:
% cd bin
% file ltl2tgba
ltl2tgba: POSIX shell script text executable
% gdb -q ltl2tgba
"/home/adl/git/spot/bin/ltl2tgba/ltl2tgba": not in executable format: File format not recognized
(gdb) quit
The proper way to run any command on these fake binaries is via
libtool:
% ../../libtool --mode=execute file ltl2tgba
/home/adl/git/spot/bin/.libs/lt-ltl2tgba: ELF 32-bit LSB executable, Intel 80386, version 1 (SYSV), dynamically linked (uses shared libs), for GNU/Linux 2.6.18, not stripped
% ../../libtool --mode=execute gdb -q ltl2tgba
Reading symbols from /home/adl/git/spot/bin/.libs/lt-ltl2tgba...done.
(gdb) quit
You can see that libtool turns ltl2tgba into .libs/lt-ltl2tgba, but it
also sets environment variables so that the dependent shared libraries
will be found.
If you are building Spot from the GIT repository, the libtool script
generated the root of the build tree should be the same as the libtool
script that is installed on your system. So you can simply run
libtool instead of ../../libtool.
There is an undocumented feature of libtool that allows you to
shorthand "libtool --mode=execute" as "libtool execute" or even
"libtool e". But you might also find convenient to define an alias, a
function, or a script to make that invocation even shorter.
For instance:
alias le='libtool --mode=execute '
(The trailing space makes it possible to follow this command by
another aliased command.)
Profiling with callgrind
------------------------
Install valgrind and kcachegrind.
Then run the command you want to profile through valgrind's callgrind
tool. For instance:
% libtool e valgrind --tool=callgrind ltl2tgba -f 'GFa & GFb'
This will output a file called 'callgrind.PID' where PID is the
process ID printed during valgrind's run. Load this file with
kcachegrind to get a graphical summary.
% kcachegrind ./callgrind.PID
Running coverage tests
----------------------
First, compile (and link) Spot with coverage enabled.
% ./configure CXX='g++ --coverage'
% make
Then run the test suite (or any program you want to study).
% make check
Executing programs using Spot will generate a lot of *.gc* files
everywhere. Collect these using lcov:
% lcov --capture --directory src --output spot.info
Finally generate a coverage report in HTML:
% genhtml --legend --demangle-cpp --output-directory html spot.info
This should create the directory html/.
Link-time optimizations
-----------------------
This is currently a bit tricky to setup, because the toolchain is not
mature enough. However this is getting better and better. The Debian
packages we build nightly are mostly built with link-time optimization
(the shared library uses link-time optimization, but the command-line
binary are built without because of some bug with exception
propagation).
You need:
1. a version of GCC (>= 4.9) with gold and pluing linker enabled.
2. a version of Libtool that knows how to deal with
-flto flags (Libtool 2.4.2 will work)
Here are example options to pass to configure to build a static
version with link-time optimization:
./configure CC=gcc-4.9 CXX=g++-4.9 \
--disable-devel --disable-debug \
CFLAGS='-flto' CXXFLAGS='-flto' LDFLAGS='-fuse-linker-plugin' \
--disable-shared --enable-static
If you want to build a shared library, see in debian/rules how it is
done.
Log driver for testsuite
------------------------
The PASS/FAIL status for each test of the testsuite is printed by
tools/test-driver. This script can be changed to format the output
differently. When we use Teamcity (for continuous integration) we
change the output format to something that Teamcity will understand
with:
make check LOG_DRIVER=$PWD/tools/test-driver-teamcity
Coding conventions
==================
Here some of the conventions we follow in Spot, so that the code looks
homogeneous. Please follow these strictly. Since this is free
software, uniformity of the code matters a lot. Most of these
conventions are derived from the GNU Coding Standards
(http://www.gnu.org/prep/standards.html) with the notable exception
that we do not put a space before the opening parenthesis in function
calls (this is hardly readable when chaining method calls).
Besides cosmetics, some of these conventions are also here
to prevent bugs and make it easier to devise safety checks.
The directory tests/sanity/ contains some scripts that are executed
during 'make check' or 'make installcheck' to check some of the
conventions discussed below.
For instance we have a check to ensure that any header can be included
twice, and we have another check to ensure that any header contains a
include guard that follow our naming convention. This way we do not
forget guards, and we do not forget to rename them when a file is
copied into another one.
C++11
-----
Spot uses some C++11 features, and therefore requires a C++11
compiler. The code relies on features that are not available in
version of g++ older than 4.8, so this is our minimum requirement
for now. Avoid features that require 4.9.
Reasonably recent versions of clang should work as well. Our
build farm has clang++ 3.5.
Encoding
--------
* Use UTF-8 for non-ASCII characters.
* Do not use tabs for indentation in C++ files. Use only space to
prevent issues with people assuming different tab widths.
* If you edit files encoded in Latin-1 (the original default
encoding for the project), feel free to convert them to UTF-8.
In emacs the simplest way to convert the file is to add a comment
with -*- coding: utf-8 -*- at the top or bottom of the file.
There is some check in tests/sanity/ that will ensure that -*-
coding: utf-8 -*- is used for all C++ files, but try to use it for
all text files if they contain non-ascii characters.
Includes
--------
* Use #include with angle-brackets to refer to public headers
of Spot; i.e., those that will be installed, or system
headers that are already installed. E.g.,
#include <spot/misc/version.hh>
#include <iostream>
* Use #include with double quotes to refer to private headers that
are distributed with Spot. Those can be from Spot itself, or from
third-party libraries that we ship. E.g.,
#include "utf8/utf8.hh"
#include "spot/priv/trim.hh"
#include "config.h"
This style of #include should never occur in public headers.
Exporting symbols
-----------------
Since we are building a library, it is important to make a clear
distinction between what is private and what is public. In our
setup, everything is private by default and has to be explicitely
made public.
* If a private symbol is needed only by one module, keep it inside
the *.cc file, in an anonymous namespace. Also mark it as static
if it is a function or variable. This is the best way to let the
compiler and linker know that the symbol is not used elsewhere.
* If a symbol could be used by several modules of the library but
should still be private to the library, use a *.hh/*.cc pair of
files, but list both files in the _SOURCES variable of that
directory (see for instance weight.hh in tgbaalgos/Makefile.am).
This will ensure that the header is not installed.
Needless to say, no public header should include such a private
header.
* The directory src/priv/ can be used to store files that are
globaly private the library, and that do not really belongs to
other directories.
* Functions and classes that are public should be marked with
the SPOT_API macro. This macro is defined in misc/common.hh,
but you need not include it in a file that already includes
another public header.
* Do not make a symbol public just because you can.
* Read http://www.akkadia.org/drepper/dsohowto.pdf for more
information about how shared libraries work and why.
Assertions
----------
* There are different types of assertions. Plain assert() is OK for
invariants or post-conditions. When asserting a pre-condition,
carefully consider who the caller might be: if it can be in
user-code (either in C++ or Python), throw an exception
(std::runtime_error, std::invalid_argument, and spot::parse_error
are the three exception types catched by the Python bindings).
* Do not call assert() in public *.hh files: even if the installed
libspot has been compiled with -DNDEBUG, the *.hh files will be
recompiled by users, probably without -DNDEBUG. So use
SPOT_ASSERT() instead of assert(), this ensure asserts are only
used inside libspot for debug builds.
Comments
--------
* The language to use is American English.
* When comments are sentences, they should start with a capital and
end with a dot. Dots that end sentences should be followed by two
spaces (i.e., American typing convention), like in this paragraph.
* Prefer C++-style comments (// foo) to C-style comments (/* foo */).
Use /// for Doxygen comments.
Formating
---------
* Braces around instruction blocks are always on their own line.
Braces around initializers lists need not be on their own.
* Text within braces is two-space indented.
{
f(12);
}
* Anything after a control statement is two-space indented. This
includes braces.
if (test)
{
f(123);
while (test2)
g(456);
}
* Braces from function/structure/enum/class/namespace definitions
are not indented.
class foo
{
public:
Foo();
protected:
static int get_mumble();
};
* The above corresponds to the `gnu' indentation style under Emacs.
* Put a space before the opening parenthesis in control statements
if (test)
{
do
{
something();
}
while (0);
}
* No space before parentheses in function calls.
(`some()->foo()->bar()' is far more readable than
`some ()->foo ()->bar ()')
* No space after opening or before closing parentheses, however
put a space after commas (as in english).
func(arg1, arg2, arg3);
* No useless parentheses in return statements.
return 2; (not `return (2);')
* Spaces around infix binary or ternary operators:
2 + 2;
a = b;
a <<= (3 + 5) * 3 + f(67 + (really ? 45 : 0));
* No space after prefix unary operators, or before postfix unary
operators:
if (!test && y++ != 0)
{
++x;
}
* When an expression spans over several lines, prefer splitting it
before operators. If it's inside a parenthesis, the following
lines should be 1-indented w.r.t. the opening parenthesis.
if (foo_this_is_long && bar > win(x, y, z)
&& !remaining_condition)
{
...
}
* `else if' can be put as-is on a single line.
* No line should be larger than 80 columns.
If a line takes more than 80 columns, split it or rethink it.
This makes it easier to print the code, allow people to work on
small screens, makes it possible to display two files (or an
editor and a terminal) side-by-side, ...
This also puts some pressure on the programmer who writes code
that has too much nested blocks: if you find yourself having to
code between columns 60 and 80 because of identation, consider
writing helper functions to simplify the structure of your code.
* Labels or case statements are back-indented by two spaces,
without space before the `:'.
if (something)
{
top:
bar = foo();
switch (something_else)
{
case first_case:
f();
break;
case second_case:
g();
break;
default:
goto top;
}
}
* Pointers and references are part of the type, and should be put
near the type, not near the variable.
int* p; // not `int *p;'
list& l; // not `list &l;'
void* magic(); // not `void *magic();'
* Do not declare many variables on one line.
Use
int* p;
int* q;
instead of
int *p, *q;
The former declarations also allow you to comment each variable.
* The include guard for src/somedir/foo.hh is
SPOT_SOMEDIR_FOO_HH
Naming
------
* Functions, methods, types, classes, etc. are named with lowercase
letters, using an underscore to separate words.
int compute_this_and_that();
class this_is_a_class;
typedef int int_array[];
That is the style used in STL.
* Private members end with an underscore.
class my_class
{
public:
...
int get_val() const;
private:
int name_;
};
* Identifiers (even internal) starting with `_' are best avoided
to limit clashes with system definitions.
* Template arguments use capitalized name, with joined words.
template <class T, int NumberOfThings>
class foo
{
...
};
* Enum members also use capitalized name, with joined words.
* C Macros are all uppercase.
* Use *.hxx for the implementation of templates that are private to
Spot (i.e., not installed) and need to be included multiple times.
SPOT macros
-----------
A few macros are defined in misc/common.hh notably:
* SPOT_FALLTHROUGH should be used to mark fall-throughs in switches:
switch (foo)
{
case 1:
f();
SPOT_FALLTHROUGH;
case 2:
g();
break;
}
* Use SPOT_UNREACHABLE() to mark places that are not reachable but
that a compiler might not see as unreachable.
* Use SPOT_API in front of functions and class that should be
exported by the shared library. See "Exporting symbolss" above.
* Use SPOT_ASSERT(...) if you ever have to put an assertion in
some header file. See "Assertions" above.
* Use SPOT_LIKELY / SPOT_UNLIKELY in case you need to help the
compiler figure out the commont output of a test. Do not abuse
this without checking the assembly output to make sure the effect
is what you desired.
Other style recommandations
---------------------------
* The original C++98 code used 0 for null pointers (and never NULL).
Feel free to replace these by uses of C++11's nullptr instead.
* Limit the scope of local variables by defining them as late as
possible. Do not reuse a local variables for two different things.
* Do not systematically initialize local variables with 0 or other
meaningless values. This hides errors to valgrind.
* Avoid <iostream>, <ostream>, etc. in headers whenever possible.
Prefer <iosfwd> when predeclarations are sufficient, and then
for instance use just <ostream> in the corresponding .cc file.
(A plain <iostream> is needed when using std::cout, std::cerr, etc.)
* Always declare helper functions and other local class definitions
(used in a single .cc files) in anonymous namespaces. (The risk
otherwise is to declare two classes with the same name: the linker
will ignore one of the two silently. The resulting bugs are often
difficult to understand.)
* Always code as if the person who ends up maintaining your code is
a violent psychopath who knows where you live.