Revision as of 12:47, 19 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/context
  • context manager, context-dependent object/collection sources
• src/expr
  • the expression package
• src/include
  • public includes (installed in /usr/local or whatever on a users' machines)
• src/main
  • source for the main cvc4 binary
• src/parser
  • parsers for supported CVC4 input formats
• src/prop
  • propositional parts of CVC4; these include imported minisat sources and the PropEngine
• src/smt
  • SmtEngine
• src/theory
  • the TheoryEngine and all theory solvers
• src/util
  • utility classes, debugging macros, the Exception class, etc.
• test
  • CxxTest unit tests (invoked by make check)

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. An exception is naming for low-level exception types. However, for derived classes of CVC4::Exception, the names should be CamelCase.

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, or a subnamespace of CVC4 (based on module).

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

1. Between type names and */& when declaring members and variables, to emphasize the introduced name is a pointer:

 Foo *a, *b;

1. NOT between type names and */& when in an argument list or return type, to emphasize that the type is a pointer:

 Bar* fooToBar(Foo* f);

1. There is an exception for array types, since "char *argv[]" is actually an array of pointers, it doesn't make sense to attach * to the type in this case (in C++, the [] must come after the formal name). In particular:

 int main(int argc, char *argv[]);

is how the signature for the main function is written.

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.

Other coding guidelines (as yet uncategorized)

1. All exceptions thrown by CVC4 should be types publicly derived from CVC4::Exception, unless the exception is very low-level (similar to std::bad_alloc) and there's a compelling reason to avoid the CVC4 infrastructure (this is true, for instance, for non-exceptional signals that are thrown internally by CVC4 and never escape the library; it's best to avoid memory allocation in this case).
2. Traditionally long declaration blocks (classes, namespaces, #endifs) should have an associated comment:

 namespace CVC4 {
 class Foo {
   /* pages
    * and
    * pages
    * go
    * by
    */
 };/* class Foo */
 }/* CVC4 namespace */

Always end with a comment that matches the declaration ("struct Foo", "class Foo", "enum Foo"), except for namespaces, where it's the "Foo namespace." Comment preprocessor macros similarly:

 #ifdef SOMETHING
 # ifdef OTHERTHING
 #  error You can't do that.
 # else /* !OTHERTHING */
 #  warning This is experimental code.
 #  define FOO(x) x
 # endif /* OTHERTHING */
 #else /* SOMETHING */
 # define FOO(x)
 #endif /* SOMETHING */

Note that the indentation level for preprocessor macros is 1, not 2, and that the #else takes the negation of the condition as a comment (but #endif takes the non-negated one). In cases where these blocks are long and you want to include additional context information about what macros are true, please do:

 #ifdef SOMETHING
 /* lots of
  * code here
  */
 #else /* !SOMETHING */
 /* lots of
  * code here
  */
 # ifdef OTHERTHING /* && !SOMETHING */
 /* code... */
 # endif
 #endif

1. Vertical spacing: depends on context. Logically group statements. Debugging bits should generally be offset from the rest of the code by blank lines. switch() {} blocks should generally leave a space between a case label and the preceding break.
2. No trailing spaces please. M-x delete-trailing-whitespace in emacs might help.
3. ALWAYS COMMENT FALL-THROUGH CASES IN switch() {}:

 switch(foo) {
 case THIS_ONE:
   printf("this!\n");
   /* fall through */
 case THAT_ONE:
   printf("that!\n");
 }

1. ALL OUTPUT through Debug and Trace and Notice and Warning functionality please! Very easy:

 CVC4::Debug("arith", "foo!"); // prints "foo!" if arith debugging is on
 CVC4::Warning("Equivalence classes didn't get merged."); // prints unless user gave -q or in SMT-COMP mode
 CVC4::Notice("Hi, so you don't get bored, here are some statistics: " + stats); // if user gives -v
 CVC4::Chat("I feel like doing some theory propagation.");// if user gives -vv
 CVC4::Trace("arith", "<ralph>I'm now calling a function!</ralph>");// if user gives -vvv

Chatting in particular should be useful for tuning/strategy things. Parts of the code that aren't conditional on particular settings in CVC4 should avoid Chat and use Trace or Debug. Tracing is tagged with the module to which it's relevant. The above add a \n for you. If you don't want that, you can use a printf() interface:

 CVC4::Debug::printf("arith", "foo!"); // no line termination

or the stream interface:

 CVC4::Debug("arith") << "foo!"; // also no line termination

For non-debug builds, CVC4::Debug is a no-op and everything will be inlined away.

1. CVC4 Assertions:

 CVC4::Assert(condition); // asserts condition is true
 CVC4::Assert(condition, "error message on fail"); // asserts condition is true, custom error message

Note that Assert is a macro (in order to collect source line and file and expression-string information from the C preprocessor). A CVC4::AssertionException is thrown if it fails. When assertions are turned off, this is a no-op and everything is inlined away.

Intentionally not covered

• 0 vs NULL
• int foo(void) -- (void) unnecessary

Binary compatibility: what is it and why do we care?

• http://sources.redhat.com/autobook/autobook/autobook_91.html
• http://www.linux.org/docs/ldp/howto/Program-Library-HOWTO/shared-libraries.html
• http://ispras.linux-foundation.org/index.php/ABI_compliance_checker_Downloads
• http://tldp.org/HOWTO/Program-Library-HOWTO/shared-libraries.html

Unit testing

• Get CxxTest from here:
  • http://cxxtest.tigris.org/files/documents/6421/43281/cxxtest-3.10.1.tar.gz
• Unpack it in, say, your home directory.
• Then, just point CVC4's configure to it:
  • ./configure CXXTEST=~/cxxtest
• Now, make check will run the CxxTest unit tests under test/.
• To add a new test, create a test header file under test/ (possibly in a subdirectory based on the relevant CVC4 module and whether it's white/black-box testing). Then add it to TESTS in test/Makefile.am.