HACKING 20.1 KB
Newer Older
1 2 3 4
Bootstraping from the GIT repository
====================================

(If you are building from a tarball, skip this section.)
5

6 7 8 9 10 11 12 13
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

14
Some files in SPOT's source tree are generated.  They are distributed
Antoine Martin's avatar
Antoine Martin committed
15 16 17
so that users do not need to install tools to rebuild them, but we
don't keep all of them under GIT because it can generate lots of
changes or conflicts.
18

19
Here are the tools you need to bootstrap the GIT tree, or more
20
generally if you plan to regenerate some of the generated files.
21 22
(None of these tools are required by end users installing a tarball
since the generated files they produce are distributed.)
23

24
  GNU Autoconf >= 2.61
25
  GNU Automake >= 1.11
26
  GNU Libtool >= 2.4
27
  GNU Flex (the version seems to matters, we used 2.5.35)
28
  GNU Bison >= 3.0
29
  GNU Emacs (preferably >= 24 but it may work with older versions)
30 31
    Note that if you use Macports you should consider to install the
    swig-python package in addition to the swig package.
32 33 34 35
  org-mode >= 9.1 (the version that comes bundled with your emacs
    version is likely out-of-date; but distribution often have
    a separate and more recent org-mode package, or you can
    simply upgrade from ELPA).
36
  Groff (a.k.a. GNU troff) >= 1.20
37
  SWIG >= 3.0 (for its better C++11/C++14 support)
38
  Doxygen >= 1.4.0
39
  R   used by some examples in the documentation
40 41
  Perl, with its Gettext module (it might be called something like
    liblocale-gettext-perl or p5-locale-gettext in your distribution)
42 43
  A complete LaTeX distribution, including latexmk and extra fonts
    like dsfont.sty.
44
  ImageMagick
45
  Python >= 3.3, IPython >= 2.3
46
  GraphViz
47
  Java >= 1.7 (needed to run PlantUML while generating the doc)
48
  wget or curl (needed to download PlantUML)
49
  pdf2svg
50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70

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
  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.

71

72
Bootstrap the GIT tree by running
73

74
  % autoreconf -vfi
75

76
and then go on with the usual
77

78 79
  % ./configure
  % make
80

81

82 83 84
Tricks
======

85 86 87 88 89 90
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
91
don't have emacs, or you simply want not to rebuild these files, use:
92

93
  % touch doc/org-stamp
94

95

96 97 98 99
Silent Building with automake
-----------------------------

The classical makefiles generated by automake are very verbose during
100 101 102 103
build beacause they print the full command line of every stage.  This
verbosity is very usefull to help (remotely) users to compile Spot.
Nonetheless, these compilations lines may be annoying for some
developers.  To reduce this verbosity, just run:
104

105
  % make V=0
106

107 108 109 110 111

Executing a single test
-----------------------

All tests in subdirectories of tests/ are executed through the
112 113
tests/run script.  That script defines PATH and other environment
variables necessary so that shell and Python scripts will use the
114 115 116
version of Spot under development.  For instance to execute
tests/core/acc.test, do:

117 118
  % cd tests
  % ./run core/acc.test
119 120 121 122 123 124 125 126 127 128 129 130

A test run this way automatically executes in verbose mode.  Any
temporary file generated by the script can be found in
tests/core/acc.dir/.

Alternatively, if you use emacs, the .dir-locals.el configuration at
the top of the project redefines the C-c C-c key for all shell and
python scripts under the tests/ directory.  So if you are working on
tests/core/acc.test under emacs, hitting C-c C-c should be all you
need to execute it.


131 132 133
Debugging Libtool executables
-----------------------------

134
The executables generated in the various testsuite directories of Spot
135
are not real binaries.  Because we use libtool to compile the spot
136 137
library in a portable manner, these executables are just scripts that
run the actual binary after setting some environment variables so that
138 139
the OS can find the library in the build tree.

140 141
A consequence is that tools like gdb or valgrind, that expect to work
on a binary, will be confused by the script.  Example:
142

143
  % cd bin
144 145 146
  % file ltl2tgba
  ltl2tgba: POSIX shell script text executable
  % gdb -q ltl2tgba
147
  "/home/adl/git/spot/bin/ltl2tgba/ltl2tgba": not in executable format: File format not recognized
148 149
  (gdb) quit

150 151
The proper way to run any command on these fake binaries is via
libtool:
152 153

  % ../../libtool --mode=execute file ltl2tgba
154
  /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
155
  % ../../libtool --mode=execute gdb -q ltl2tgba
156
  Reading symbols from /home/adl/git/spot/bin/.libs/lt-ltl2tgba...done.
157 158
  (gdb) quit

159 160 161 162 163
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
164 165 166 167
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.

168
There is an undocumented feature of libtool that allows you to
169
shorthand "libtool --mode=execute" as "libtool execute" or even
170 171 172 173 174 175 176 177
"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.)
178 179


180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196
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


197 198 199 200 201
Running coverage tests
----------------------

First, compile (and link) Spot with coverage enabled.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
202
  % ./configure CXX='g++ --coverage'
203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219
  % 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/.

220 221 222 223
Coverage tests are automatically performed by our continuous
integration builds.  You can find a report for each branch in the
artifacts of the debian-unstable-gcc-coverage job.

224

225 226 227
Link-time optimizations
-----------------------

228 229
This used to be bit tricky to setup, but is now quite well supported.
Our Debian packages are built with link-time optimization.
230 231

You need:
232
  1. a version of GCC (>= 4.9) with gold and pluging linker enabled.
233
  2. a version of Libtool that knows how to deal with
234
     -flto flags (Libtool 2.4.2 will work)
235

236 237
Here are example options to pass to configure to build a static
version with link-time optimization:
238

239
  ./configure CC=gcc-4.9 CXX=g++-4.9 \
240 241 242
              --disable-devel --disable-debug \
              CFLAGS='-flto' CXXFLAGS='-flto' LDFLAGS='-fuse-linker-plugin' \
              --disable-shared --enable-static
243

244 245
If you want to build a shared library, see in debian/rules how it is
done.
246 247


248 249 250 251 252
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
253 254 255
differently.  In the past, when we used teamcity (for continuous
integration) we changed the output format to something that teamcity
would understand with:
256

257
  make check LOG_DRIVER=$PWD/tools/test-driver-teamcity
258 259


260 261
Coding conventions
==================
262

263
Here some of the conventions we follow in Spot, so that the code looks
264 265 266 267 268 269
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).
270

271 272 273
Besides cosmetics, some of these conventions are also here
to prevent bugs and make it easier to devise safety checks.

274
The directory tests/sanity/ contains some scripts that are executed
275 276 277 278 279 280 281 282 283
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.

284

285
C++14
286 287
-----

288 289
  Spot uses some C++14 features, and therefore requires a C++14
  compiler.  g++ 5.x or clang++ 3.4 should be enough.
290

291 292
  We currently avoid C++17 features until C++17 compiler are widely
  available.
293

294 295 296 297 298
Encoding
--------

  * Use UTF-8 for non-ASCII characters.

299 300 301
  * Do not use tabs for indentation in C++ files.  Use only space to
    prevent issues with people assuming different tab widths.

302 303
  * If you edit files encoded in Latin-1 (the original default
    encoding for the project), feel free to convert them to UTF-8.
304 305
    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.
306

307 308 309 310
    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.

311 312 313 314 315 316 317 318 319 320
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>

321 322 323
  * 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.,
324

325
    #include "config.h"
326 327 328 329 330
    #include "utf8/utf8.hh"
    #include "spot/priv/trim.hh"

    This style of #include should never occur in public headers.

331 332 333 334
  * "config.h" should be the first file included by any *.cc or *.c
    file, as it setups several macros for replacing missing functions.


335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350
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
351
    directory (see for instance weight.hh in priv/Makefile.am).
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
352 353
    This will ensure that the header is not installed.
    Needless to say, no public header should include such a private
354 355
    header.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
356
  * The directory src/priv/ can be used to store files that are
Clément Gillard's avatar
Clément Gillard committed
357
    globaly private to the library, and that do not really belong to
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
358
    other directories.
359 360 361

  * Functions and classes that are public should be marked with
    the SPOT_API macro.  This macro is defined in misc/common.hh,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
362
    but you need not include it in a file that already includes
363 364 365 366 367
    another public header.

  * Do not make a symbol public just because you can.

  * Read http://www.akkadia.org/drepper/dsohowto.pdf for more
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
368
    information about how shared libraries work and why.
369

370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385
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.

386 387 388
Comments
--------

389
  * The language to use is American English.
390 391 392 393 394

  * 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.

395 396 397
  * Prefer C++-style comments (// foo) to C-style comments (/* foo */).
    Use /// for Doxygen comments.

398 399 400 401 402 403 404
  * When mentioning an issue number, in comments as well as in commit
    messages, use one of the following forms so that we can configure
    our editors to turn these into hyperlinks.

       Issue #123 / issue #123 / Fixes #123 / fixes #123

    (When gitlab sees a commit message containing "Fixes #123" or
405 406 407
    "fixes #123" pushed to branch "next", it should automatically
    close the issue.  But these days, it does not seem to work and
    often require manual closing.)
408

409 410 411
Formating
---------

412 413
  * Braces around instruction blocks are always on their own line.
    Braces around initializers lists need not be on their own.
414 415 416 417 418

  * Text within braces is two-space indented.

    {
      f(12);
419

420 421 422 423 424 425 426 427 428 429 430 431
    }

  * Anything after a control statement is two-space indented.  This
    includes braces.

    if (test)
      {
        f(123);
	while (test2)
	  g(456);
      }

432
  * Braces from function/structure/enum/class/namespace definitions
433 434 435 436 437 438 439 440 441 442 443
    are not indented.

    class foo
    {
    public:
      Foo();
    protected:
      static int get_mumble();
    };

  * The above corresponds to the `gnu' indentation style under Emacs.
444 445

  * Put a space before the opening parenthesis in control statements
446 447 448 449 450 451 452 453 454 455 456 457

    if (test)
      {
        do
	  {
	    something();
	  }
	while (0);
      }

  * No space before parentheses in function calls.
    (`some()->foo()->bar()' is far more readable than
458
    `some ()->foo ()->bar ()')
459 460 461

  * No space after opening or before closing parentheses, however
    put a space after commas (as in english).
462

463
    func(arg1, arg2, arg3);
464

465 466 467 468 469 470 471 472 473
  * 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));
474

Alexandre Duret-Lutz's avatar
typo  
Alexandre Duret-Lutz committed
475 476
  * No space after prefix unary operators, or before postfix unary
    operators:
477 478 479 480 481 482

    if (!test && y++ != 0)
      {
        ++x;
      }

483 484 485
  * 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.
486 487 488 489 490 491 492

    if (foo_this_is_long && bar > win(x, y, z)
        && !remaining_condition)
      {
        ...
      }

493 494
  * `else if' can be put as-is on a single line.

495 496
  * No line should be larger than 80 columns.
    If a line takes more than 80 columns, split it or rethink it.
497

498 499 500 501 502 503 504 505 506
    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.

507
  * Labels or case statements are back-indented by two spaces,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
508
    without space before the `:'.
509

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526
    if (something)
      {
      top:
        bar = foo();
        switch (something_else)
	  {
	  case first_case:
	    f();
	    break;
	  case second_case:
	    g();
	    break;
	  default:
	    goto top;
	  }
      }

527 528 529 530 531 532 533 534 535 536 537 538 539
  * 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;
540
    The former declarations also allow you to comment each variable.
541 542 543 544

  * The include guard for src/somedir/foo.hh is
    SPOT_SOMEDIR_FOO_HH

545
Naming
546
------
547 548 549 550 551 552 553

  * 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;
554

555 556 557 558
      typedef int int_array[];

    That is the style used in STL.

559
  * Private members end with an underscore.
560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580

    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
    {
      ...
    };

581
  * Enum members also use capitalized name, with joined words.
582 583 584

  * C Macros are all uppercase.

585 586
  * Use *.hxx for the implementation of templates that are private to
    Spot (i.e., not installed) and need to be included multiple times.
587

588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608
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
609
    exported by the shared library.  See "Exporting symbols" above.
610 611 612 613 614

  * 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
Antoine Martin's avatar
Antoine Martin committed
615
    compiler figure out the common output of a test.  Do not abuse
616 617 618
    this without checking the assembly output to make sure the effect
    is what you desired.

619
Other style recommandations
620
---------------------------
621

622 623
  * 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.
624

625
  * Limit the scope of local variables by defining them as late as
Antoine Martin's avatar
Antoine Martin committed
626
    possible.  Do not reuse a local variable for two different things.
627

628
  * Do not systematically initialize local variables with 0 or other
629
    meaningless values.  This hides errors to valgrind.
630 631 632

  * Avoid <iostream>, <ostream>, etc. in headers whenever possible.
    Prefer <iosfwd> when predeclarations are sufficient, and then
633
    for instance use just <ostream> in the corresponding .cc file.
634
    (A plain <iostream> is needed when using std::cout, std::cerr, etc.)
635 636 637 638 639 640

  * 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.)
641 642 643

  * Always code as if the person who ends up maintaining your code is
    a violent psychopath who knows where you live.