Revision as of 11:58, 17 November 2009

Source tree layout

• config
  • this directory holds m4 macro processor files and bits of the autotools build system
• contrib
  • this directory includes maintainer scripts and other things that aren't directly part of CVC4
• doc
  • documentation
• src
  • core
    • the core of CVC4: the expression package, the core engines, ...
  • include
    • most include files (some private include files are also in parser and sat)
  • parser
    • parsers for supported CVC4 input formats
  • sat
    • propositional parts of CVC4; these include imported minisat sources

Coding guidelines

File and directory names

1. Files should be all lowercase, with CamelCase classes in header files named camel_case.h (and their implementations in camel_case.cpp);
2. File extensions .cpp and .h are generally preferred, with .ypp and .lpp for yacc and lex inputs---an exception is made for headers when autotools wants to output parser definitions as (e.g.) pl.hpp;

1. Of course, STL type names are not CamelCase, and when implementing traits and STL-like typedefs (iterators for instance), you should match the STL style as closely as possible:

 class Foo {
   class Item;
   typedef Item*       iterator;
   typedef const Item* const_iterator;
 };

1. Acronyms inside type names should generally be lowercase after the first letter, such as in CVC4::SmtEngine. This is preferred to SMTEngine or SMT_Engine, but use judgment.

Member names

1. Data members are prefixed with d_, and are generally lowerCamelCase after that. For example:

 class Foo {
   int d_thisIsAnInt;
 };

1. Static members are prefixed with s_:

 class Foo {
   static int s_thisIsAStaticInt;
 };

Source file layout

Class header files

1. A class named ThisIsAClass is guarded by a preprocessor macro __CVC4_THIS_IS_A_CLASS_H. Its definition is in src/include/this_is_a_class.h.
2. Everything should be in the CVC4 namespace.

Class implementation files

1. A class named ThisIsAClass should have its implementation under src/ in this_is_a_class.cpp.

Imported sources

1. IMPORTANT: For imported sources, make sure to add an exclusion to the contrib/update-copyright.pl script so that a CVC4 copyright isn't added.

Source file headers

1. A common comment blurb heads all source files in CVC4: non-imported headers and sources, as well as yacc and flex inputs.
2. A script is used to maintain/update this comment blurb.

update-copyright.pl

1. You can run contrib/update-copyright.pl to update all sources with a new copyright template. (Some) efforts are made to throw away old boilerplate comment blurbs and keep file-specific comments.
2. PLEASE BE CAREFUL: this updates files in place without keeping a backup. The script is probably buggy. You have been warned. It's best to do this on a copy of your source tree, or on a fresh repository checkout. (The program will warn you too.)
3. Please consult "svn diff" before committing changes made by the script.

Using emacs

1. There's an emacs-lisp snippet available that you can drop in your ~/.emacs to conform to spacing, indentation, etc., in the CVC4 source tree.
2. See contrib/editing-with-emacs.

General guidelines

Comments

Whitespace/tabs

1. No tabs, please.
2. No whitespace between if, for, while, 'catch', etc., and the parentheses.
3. One space between closing paren and open curly brace (except if aligning to other nearby source lines).
4. One space around binary operators to avoid crowding, e.g.:

  x = y;
  z = y + 1;

1. In complicated arithmetic expressions, even when parentheses aren't required by operator order of evaluation, sometimes parentheses and extra spacing and alignment should be used for visual clarity, or to match more closely what is being implemented, what is described in associated source code comments, or both. For example:

  if( ( ( x1 + y1 ) - ( z  * 2 ) ) <=  4 ||
      ( ( x2 + y2 ) - ( zp * 2 ) ) >= -4 ) { ... }

1. Occasionally to emphasize a !, so it doesn't get visually lost, it's best followed or even surrounded by space. For example, this is bad:

  if(!(x + y > 4)) ...

• while this is much preferred:

  if( !( x + y > 4 ) ) { ... }

• (assuming that it's preferable not to rewrite this as x + y <= 4 for some other reason of course).

Increment/Decrement

1. Preincrement/decrement preferred over postincrement/-decrement, e.g.:

  for(int x = 0; x < 10; ++x) { ... }

Bracing

1. Braces not required around one-line blocks, but preferred in complicated cases especially with if (to avoid visually-ambiguous elses).

• • E.g. this is fine:

   if(extra_output)
     do_something();

• • But this is debatable (preferring braces on the if() but not the for():

   if(extra_output)
     for(int i = 0; i < 10; ++i)
       do_something();

• • And this is horrible:

   if(extra_output)
     do_something_simple();
   else
     while(!done)

1. Generally, if the then part of an if is complicated and braced, but the else part is simple, the else need not be braced but may be. But if the else part is complicated and braced then the then part should be (even if it's simple).
2. If in doubt, brace.
3. If anything is visually ambiguous, brace for clarity.

Indentation

1. Indentation level is 2.
2. No indentation under switch() {} or namespace {}
3. Labels and "private/public/protected" are recessed 2.
4. template <class T> generally belongs on its own line before a function declaration or definition. An exception is inside a class file where there's a long string of simple functions that are best not separated by vertical space.
5. Attempt to keep lines under 80 columns wide. Though if this makes things excessively ugly or confusing, it's probably ok.

Use of autotools: automake, autoconf, autoheader, libtool

1. Please don't check into the repository things generated by automake, autoconf, autoheader, for example: config.h.in, Makefile.ins, Makefiles, ylwrap/libtool/aclocal.m4/missing/config.guess, configure, etc.

Commits

1. Before you commit, everything should be documented and your code should conform to the coding guidelines.
2. An automated bot will review code commits and complain loudly to you if it doesn't like your documentation or coding style.
3. Clark will review all code commits for content.
4. Others in the group will review Clark's commits for content.
5. Unit tests should be included to test any new functionality included in your commit. These tests should pass the gcov coverage testing for CVC4.

Unit tests with cxxunit

There are two unit tests for modules:

1. those written by the main author of the module/piece of functionality (white-box)
2. those written by another group member to test the exported interface of the module (black-box)

GCov coverage testing

Every non-exceptional line of code should be tickled by a unit test.