Developer's Guide

From CVC4
Revision as of 14:43, 4 March 2010 by Mdeters (Talk | contribs) (→‎Unit testing)

Jump to: navigation, search

In addition to this wiki, we also have a developer mailing list and Bugzilla database for this version of CVC. CVC3 resources have been kept separate, at this time, because of the different needs of CVC4 during active development.

Contents

Source tree layout

  • config - this directory holds m4 macro processor files (autoconf code) as well as bits of the autotools build system that go out as part of the distribution to smooth over platform differences.
  • 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)

Using CVC4's Subversion source control repository

CVC4 keeps a source control repository using Subversion, allowing us to track changes, effectively branch and merge, etc.

Accessing CVC4's repository

Access to CVC4's Subversion repository is restricted; you must have an AcSys-group CIMS account, or apply to us for outside collaborator access to the repository. Once you have access, you can: 

 svn --username $USERNAME checkout https://subversive.cims.nyu.edu/cvc4/cvc4/trunk cvc4

...where $USERNAME is your CIMS username (or the username you were given as an outside collaborator). If your username on the Windows/UNIX machine you're coming from is the same, you can leave out the --username $USERNAME part.

The above checks out /cvc4/cvc4/trunk to your local directory cvc4. This second argument (your local working directory for CVC4 development), you can of course call whatever you like. The first is the path in the repository. The initial /cvc4 is the base of our repository (other groups' repositories are hosted on the same server). The second /cvc4 in the path is the product (since we might decide to keep other, CVC4-related projects in the CVC4 repository even if they aren't directly part of CVC4. This includes things like useful benchmark suites (that aren't part of the source tree proper), benchmark-processing utilities, the nightly build system scripts, the webpage, etc. These things may not belong directly in the source tree, but are still worth keeping in the CVC4 repository. The third component of the path, /trunk, is the branch of CVC4 you're requesting. In Subversion terminology, trunk is the head of development: the most recent version of CVC4 that's been committed. The trunk is where most of our CVC4 mainline development will take place, for now. We may occasionally branch (see below) to develop and test new or experimental features, but generally these branches will be merged back into the trunk.

Once you've checked out a working directory, some helpful commands are:

  • svn update - updates your working directory to the most recent version, merging updates into your edits)
  • svn status - tells you what you've changed
  • svn diff - gives you a diff of what you've changed

Repository access from Eclipse

From Eclipse, you can go to File -> New -> Project... and then choose Project from SVN under the SVN category. Use the repository location https://subversive.cims.nyu.edu/cvc4/cvc4/trunk and click Finish. Your Eclipse CVC4 project is then associated to the repository and you can use the Subversion facilities of Eclipse to perform the operations in this section instead of the command line.

Browsing the repository

You can also browse CVC4 sources without checking them out from Subversion. Simply point your browser to: 

 https://subversive.cims.nyu.edu/cvc4/cvc4/trunk

Your browser may complain about the security certificate. Use your CIMS login and password, or the outside collaborator credentials we've given you.

Branching and merging

Branches live in the repository under /cvc4/cvc4/branches. You can see a list of all branches available (that haven't been deleted) by using svn ls: 

 svn --username $USERNAME ls https://subversive.cims.nyu.edu/cvc4/cvc4/branches

To check out a branch, you check out the branch path instead of the trunk: 

 svn --username $USERNAME checkout https://subversive.cims.nyu.edu/cvc4/cvc4/branches/experimental-quantifier-instantiation cvc4.quant

To get information about where a working directory came from, use svn info 

 [mdeters@adric ~]$ cd cvc4
 [mdeters@adric cvc4]$ svn info
 Path: .
 URL: https://subversive.cims.nyu.edu/cvc4/cvc4/trunk
 Repository Root: https://subversive.cims.nyu.edu/cvc4
 Repository UUID: 615e1583-3794-4256-8e52-04c157d34929
 Revision: 59
 Node Kind: directory
 Schedule: normal
 Last Changed Author: barrett
 Last Changed Rev: 59
 Last Changed Date: 2009-12-15 13:20:31 -0500 (Tue, 15 Dec 2009)
 
 [mdeters@adric cvc4]$

Creating a branch

To create a branch, you copy the source tree to another place: 

 svn --username $USERNAME cp https://subversive.cims.nyu.edu/cvc4/cvc4/trunk https://subversive.cims.nyu.edu/cvc4/cvc4/branches/my-branch

...though please use a more descriptive name for your branch than this! Then proceed by checking out the branch: 

 svn --username $USERNAME checkout https://subversive.cims.nyu.edu/cvc4/cvc4/branches/my-branch cvc4.mybranch

Before doing lots of development on it, please document why your branch exists in a file named README.<branchname> in the top-level directory: 

 [mdeters@adric ~]$ cd cvc4
 [mdeters@adric cvc4]$ vi README.my-branch
 [mdeters@adric cvc4]$ cat README.my-branch
 This branch is to test the ideas of Splitting On Demand in SMT:
 
   ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/BarNOT-LPAR-06.pdf
 
 -- Morgan Deters <mdeters@cs.nyu.edu>  Tue, 15 Dec 2009 17:31:01 -0500
 [mdeters@adric cvc4]$ svn add README.my-branch
 [mdeters@adric cvc4]$ svn commit

This makes it easy to see what each branch exists for (without even checking it out): 

 svn --username $USERNAME cat https://subversive.cims.nyu.edu/cvc4/cvc4/branches/my-branch/README.my-branch
 This branch is to test the ideas of Splitting On Demand in SMT:
 
   ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/BarNOT-LPAR-06.pdf
 
 -- Morgan Deters <mdeters@cs.nyu.edu>  Tue, 15 Dec 2009 17:31:01 -0500

Of course, the above example created a branch from the trunk. That need not be the case; you might create a branch from another branch (simply copy that branch instead of the trunk).

Merging a branch back to the trunk

Recent versions of Subversion make merging incredibly easy, because for versions of CVC4 with a common ancestral line (which you get from branching) have merge metadata stored regarding their merges. This makes it much, MUCH easier to merge than it used to be under CVS. Let's say you've created a branch my-branch from the CVC4 trunk, like above. First, commit all your changes to my-branch that you want. Then, get a clean copy of the CVC4 trunk: 

 [mdeters@adric ~]$ svn co https://subversive.cims.nyu.edu/cvc4/cvc4/trunk cvc4.clean
 [mdeters@adric ~]$ cd cvc4.clean
 [mdeters@adric cvc4.clean]$ svn merge https://subversive.cims.nyu.edu/cvc4/cvc4/branches/my-branch

That's all there is to it. Subversion will merge all of the differences between trunk and my-branch since the last merge into the working directory. That's the key part: since the last merge. It keeps track of this information for you. You can inspect the changes, do a test build, and when you're happy with the changes, commit them.

You might occasionally merge the other way, too. If you've been developing along a branch for a long time, you might want to get the newest bugfixes from other parts of CVC4 that have been committed to the trunk. You can merge changes in the trunk to my-branch as well: 

 [mdeters@adric ~]$ cd cvc4.my-branch
 [mdeters@adric cvc4.my-branch]$ svn merge https://subversive.cims.nyu.edu/cvc4/cvc4/trunk

Naturally, if you don't want to incorporate changes into/from the trunk, but rather another version, then specify that URL instead.

Symbolically tagging a version

Symbolically tagging a branch (for example, a release version) is very similar to branching, but put under /tags instead of /branches. For example: 

 svn --username $USERNAME cp https://subversive.cims.nyu.edu/cvc4/cvc4/trunk https://subversive.cims.nyu.edu/cvc4/cvc4/tags/cade2010

Just as with branching, please provide a README file: 

 
  [mdeters@adric ~]$ svn --username $USERNAME checkout https://subversive.cims.nyu.edu/cvc4/cvc4/tags/cade2010 cvc4.cade2010
  [mdeters@adric ~]$ cd cvc4.cade2010
  [mdeters@adric cvc4.cade2010]$ vi README.cade2010
  [mdeters@adric cvc4.cade2010]$ cat README.cade2010
  cade2010 version of CVC4
  ------------------------
  This version generated the results published in the CADE 2010 paper.
  
  -- Morgan Deters <mdeters@cs.nyu.edu>  Tue, 15 Dec 2009 17:39:05 -0500
  [mdeters@adric cvc4.cade2010]$ svn add README.cade2010
  [mdeters@adric cvc4.cade2010]$ svn commit

Branches versus tags

Use a branch when you plan to do major (and perhaps experimental) editing on the source tree and don't want to screw up the nightly builds, tests, or other developers with a work in progress. Use a tag when no development will occur on the source tree; it's merely a "bookmark" on a historical version of CVC4 in case we need to refer to it later in the repository.

Working with files and directories

Occasionally a class name might change (and its source file will therefore need renaming), or you want to move around files and directories in other ways. In the old days under the CVS version control system, you had to remove the files under the old name/location and add them anew under the new name/location, losing all of the history information. Not so under Subversion. You can mv files and directories just like under UNIX: 

 svn mv foo.cpp bar.cpp

You can mkdir: 

 svn mkdir newdir

If you already have the directory (and sources in it), you can svn add it: 

 svn add newdir

The same goes with new source files: 

 svn add new_source_file.cpp

And, also, if you want to remove a file from the repository, you can do so: 

 svn rm obsolete_test.h

Note that these commands operate on the working directory. This has two consequences:

  1. You don't need to use --username $USERNAME, because the working directory is already linked to your login credentials (it was stored in the working directory meta-information when you checked out the working copy).
  2. The changes aren't immediate. You still need to use svn commit to commit your changes (and leave a log in the commit history).

Reverting a file in a working directory

Sometimes you make a local edit to a file and decide you want to undo the edit (restoring the last version you retrieved from the repository via a checkout or update). To do that, use svn revert: 

 svn revert file.cpp

Reverting a commit

Sometimes you want to revert a commit previously done by you or someone else. Perhaps a bugfix actually caused more problems than it solved, or you want to back out of a refactoring decision that turned out to be a bad idea. Let's say that revision 120 was perfect but a bugfix committed as revision 121 broke something and you want to undo that change. Now the repository is at revision 130. No problem: 

[mdeters@adric ~]$ svn co https://subversive.cims.nyu.edu/cvc4/cvc4/trunk cvc4.clean
[mdeters@adric ~]$ cd cvc4.clean
[mdeters@adric cvc4.clean]$ svn merge . -r 121:120

Merge here means to merge the differences between two revisions; it's similar in some respects to the notion of merge between branches, but here there is no branch. Subversion computes a diff between revisions 121 and 120 (here, order is important---we're doing a rollback so the revision number goes down) and merges it into the working directory. The "." is the directory to be merged. Perhaps revision 121 committed a lot of things, and you only want to rollback the changes made to the context manager. No problem: 

[mdeters@adric cvc4.clean]$ svn merge src/context -r 121:120

Ignoring files

If you're familiar with CVS, you're probably familiar with .cvsignore files---these are committed to the repository but are special in that they instruct CVS to ignore certain files in the working directory (and not report them as ? when you update). In Subversion, an svn status is similar; it will complain about files that exist but aren't in the repository. You can tell Subversion to ignore some files if they shouldn't ever be committed to the repository by using the property system (specifically the svn:ignore property on directories). "svn proplist" lists the properties on a file/directory, "svn propget" and "svn propset" get and set a specific property value on a file or directory, "svn propdel" deletes a property, and "svn propedit" edits a property (using the current $EDITOR from your environment). For example: 

[mdeters@adric ~]$ cd cvc4
[mdeters@adric cvc4]$ EDITOR=vi svn propedit svn:ignore .

...edits the svn:ignore property on the top-level cvc4 source directory with the vi editor.

Changes to properties are versioned and tracked as well; changes must be committed just like a file.

Marking a file as executable in Subversion

Another property is used for the eXecute bit. If you want to make a file executable, you can set the svn:executable property: 

 svn propset svn:executable yes filename

Resolving conflicts in a working directory

Sometimes you do an svn update and the update procedure causes a conflict (because you made changes in the same place as someone else did). In such cases, Subversion punts: it doesn't know which change should override the other, or if they need to be combined in some (non-naïve) way.

Open the file with the conflict and edit it to remove the conflicts. If Subversion still thinks it's in conflict (it has a C mark when you run svn status), then you should inform it that the conflict has been resolved: 

svn resolved conflicting_file.cpp

For more information

Refer to the Subversion book for more information on Subversion and how to work with repositories.

The CVC4 build system

The build system behind CVC4 is pretty complex. It attempts to:

  1. be cross platform (automake, libtool, autoconf are used)
  2. support a set of standard build profiles (default, production, debug, competition) with standard settings for assertions, debugging symbols, etc.
  3. allow deviating from the standard build profile by overriding its settings
  4. keep separate object/library files and sources (doing ./configure from the source directory creates a build directory and configures it instead)
  5. support multiple builds at once in same source tree (build directory names are based on build profile, e.g., debug or production, and architecture)
  6. support building a different build profile (and overrides) without rerunning the configure script (a top-level Makefile runs configure automatically)
  7. support changing Makefile.am automake specifications without re-running a bootstrap script
  8. support (slightly) older versions of automake/autoconf
  9. support partial tree rebuilding from the source directories (Makefile in source directory delegates to "current" build directory)
  10. support partial tree rebuilding from the build directories (recursive make)

Due to these constraints, the build system of CVC4 resembles a recursive-make implementation using automake/autoconf/libtool, except that it's very nonstandard.

FIXME add content here.

Adding source and header files

To add a source file to CVC4, all you need to do is create the file, add the content, then: 

$ svn add source_file.cpp

to add it to the repository, and edit the appropriate Makefile.am (usually in that directory, or if not then in the immediate parent directory) to list the file under *_SOURCES for the correct convenience library. When you next build the project, the Makefile.am's new timestamp should trigger make to regenerate the Makefile.in (in the source directory) and the Makefile (in the build directory), remake dependencies for the source, and rebuild what's necessary.

To add a header file to CVC4, create the file, add the content, then: 

$ svn add header_file.h

to add it to the repository, and edit the appropriate Makefile.am to list the file under *_SOURCES for the correct convenience library. All the above should still apply.

If you have problems getting the Makefile.in/Makefile/dependencies rebuilt, or get a warning from the missing script, re-run autogen.sh in the top-level source directory, re-run configure, and then proceed.

Adding source directories

If you add a source directory to CVC4 (under src/ or test/), make sure it's pristine (that is, just as you want it in the repository), and then:

  1. Add it to SVN: 
    $ svn add newdir
  2. Make sure that the Makefile.am in the parent directory lists it in SUBDIRS in the correct order (e.g., if it depends on the build artifacts of another subdirectory, it should be listed after).
  3. Run contrib/addsourcedir path to auto-generate a basic Makefile and Makefile.am. You'll need to edit the Makefile.am, but this gives you a template to start with. Existing files are not overwritten. Alternatively, you can generate these two Makefiles yourself:
    1. Create Makefile.am in the new directory (using as a template another Makefile.am).
    2. Set up Makefile.am to build a convenience libtool library (noinst_LTLIBRARIES) with an appropriate lib*_la_SOURCES listing the headers and sources in the directory.
    3. Add the new convenience library to the *_LIBADD in the parent directory.
    4. Create a Makefile in the new directory (using other source Makefiles as a template).
  4. Add the new Makefiles to SVN.
  5. You may need to re-run autogen.sh in the top-level source directory.

The Makefile's sole purpose is to support typing "make" inside a source subdirectory. It needs to set up a few variables correctly and then include Makefile.subdirs from the top level. It looks like this: (but use a template from another source directory, it might be more up-to-date than this version) 

topdir = ../..
srcdir = src/expr
 
include $(topdir)/Makefile.subdir

First, topdir is the relative path to the root of the source tree. srcdir is the relative path from the root to this directory. builddir should have the same definition for every subdirectory; it gives the full relative path to the associated build directory. The include line gets the standard rules for running make from a source subdirectory.

Note also that when you add a convenience library you need to add it also to the unit testing makefile in test/unit/Makefile.am. This is because the testing framework links directly against the convenience libraries to avoid the symbols that are hidden by the linker.

Coding guidelines

The following sections attempt to standardize C++ coding and organizational style for the CVC4 project.

Note that many of these standards apply to unit tests under test/ as well, but many do not.

The guiding philosophy in the coding guidelines for CVC4 is to make the code readable and consistent throughout without getting in the way by being overly restrictive. Flexibility is afforded in edge cases where the developer should make his or her best effort to satisfy the guidelines, but not at the expense of making the code less readable or formatted poorly or insensibly.

File and directory names

  • File names are all lowercase. Class FooSolver has its definition in foo_solver.h and its implementation in foo_solver.cpp.
  • File extensions .cpp and .h are generally preferred, with .ypp and .lpp for yacc and lex inputs---an exception is made for headers when other tools have clashing preferences for generated sources; e.g., autotools wants to output parser definitions for the presentation language as pl.hpp.

Preprocessor macros

Preprocessor macros should be avoided when possible.

Preprocessor macro names are ALWAYS_UPPERCASE.

Binary macros

A binary macro is a symbol that has two states. There are two kinds of binary macros:

  • A macro that is either "defined" or "undefined." These macros should have names that are nouns or noun phrases. The should not be defined to have a value—their definition should be empty. For example:
 #define DEBUG

These macros can be tested using the #ifdef directive: 

 #ifdef DEBUG
 /* ... */
 #endif /* DEBUG */
  • A macro that has one of the values 0 or 1. These macros should have names that are verbs or verb phrases. For example:
 #define USE_MINISAT 1

These macros should be tested using if statements rather than preprocessor directives: 

 if(USE_MINISAT) {
   /* do something with minisat */
 } else {
   /* some non-minisat default behavior */
 }

Block macros

Macros that expand to multiple statements should use the do { ... } while(0). For example, a macro FOO that generates the statements S1; S2; should be defined using 

   #define FOO do { S1; S2; } while(0)

(Note that there is no semicolon after while(0).)

Miscellaneous

  • Since macro parameters may be expressions with side effects, they should not be used multiple times in a definition.
  • Remember these aren't hygienic macros! You can capture names:
  #define ADD(c, a, b) { int x = a, y = b; c = x + y; }
  int main() {
    int x = 5;
    // print out the value x + x ^ 2 (should be 30)
    int z;
    ADD(z, x, x * x);
    printf("%d\n", z); // does NOT print 30  :-(
  }

The usual way to combat this problem is to prefix the names in the macro with underscores: 

  #define ADD(c, a, b) { int __x = a, __y = b; c = x + y; }

Though it's best to use longer names and perhaps to mix in the name of the macro as well, to avoid any possible clash.

  • Except when you're playing clever/stupid tricks with macro expansion, you should guard against unwitting order-of-operations surprises by parenthesizing arguments when expanded in macro bodies:
  #define ADD(c, a, b) { int __add_x = (a), __add_y = (b); (c) = x + y; }

This approximates (in this case) macro-call-by-value.

  • There is an exception to the ALWAYS_UPPERCASE rule for CVC4::Assert() and friends.

Class names

  • Classes, and type names in general, are in CamelCase. There are exceptions to this rule, however, where lower case names with embedded underscores are acceptable:
    • 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;
 };
    • for low-level exception types (similar to STL's bad_alloc). However, for derived classes of CVC4::Exception, the names should be CamelCase.
    • Low-level unions and structs may be in a similar lower case form, e.g., low_level_struct.
  • Note that acronyms (SMT, CVC4) 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 on a case-by-case basis.

Namespaces

  • Everything is in the CVC4 namespace or a sub-namespace. Generally, the sub-namespace follows the module (and thus the source directory) structure. The name remains uncapitalized, and acronyms are all in lowercase letters (e.g. CVC4::smt, CVC4::main, CVC4::parser). However, certain base types go in CVC4 directly instead of a sub-namespace despite belonging to a module. These are user-visible (such as CVC4::Exception), core functionality classes, and utility classes from src/util/.

Member names

  • Data members are prefixed with d_, and are generally in lowerCamelCase after that. For example:
 class Foo {
   int d_thisIsAnInt;
 };
  • Static members are prefixed with s_:
 class Foo {
   static int s_thisIsAStaticInt;
 };
  • Union elements are prefixed with u_.
  • There is an exception to these rules for low-level struct types that have no member functions and no destructors (and only simple, initializing constructors). For an example see the definition of CVC4::Options in src/util/options.h.

Communicating with the user: the output classes

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

 #include "util/output.h"
 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.

Assertions

CVC4 Assertions: 

 #include "util/assert.h"
 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.

The above assertions can be turned off (with --disable-assertions at configure-time). You might want to have an assertion be checked even if assertions are off. For example:

  1. Unreachable code. If you have a section of code that is intended to be unreachable (you have, perhaps, proved on paper that the code should never enter this state), it costs nothing to check the assertion (it's essentially an assert(false)---always fail).
  2. Highly-compromised state. In cases where a wrong answer is unlikely and the assertion check is cheap and infrequently-run, you may consider leaving an assertion in. This is the case also with the above unreachable-code assertion.

For unreachable code, use the Unreachable() macro. It will throw a CVC4::UnreachableCodeException (a subclass of CVC4::AssertionException): 

 #include "util/assert.h"
 CVC4::Unreachable(); // flags (supposedly) unreachable code; fails even under --disable-assertions
 CVC4::Unreachable("error message"); // custom error message

Another special case is an unhandled case (for example, a default block in a switch that was designed to handle all cases). It will throw a CVC4::UnhandledCaseException (a subclass of CVC4::UnreachableCodeException): 

 #include "util/assert.h"
 CVC4::Unhandled(); // flags an unhandled case; fails even under --disable-assertions
 CVC4::Unhandled(the_case); // same but prints out the_case that's unhandled as well (which should be whatever is in the switch)
 CVC4::Unhandled("error message"); // custom error message
 CVC4::Unhandled(the_case, "error message"); // custom error message with the_case that is unhandled

For a strong assertion that's checked even with --disable-assertions, use an AlwaysAssert(). It throws a CVC4::AssertionException just as Assert() does. 

 #include "util/assert.h"
 CVC4::AlwaysAssert(condition);
 CVC4::AlwaysAssert(condition, "error message");

Doxygen comments

Exporting library symbols

When built with a GNU toolchain, libcvc4 hides all symbols by default (with -fvisibility-hidden). This is a good way to ensure that the public interface is complete, that no undocumented interface is used by anyone, and it also permits more aggressive optimization of the library. Those symbols intended to be the public interface to CVC4, however, must be explicitly exported.

Fortunately, this isn't difficult. To use a symbol, a user should have a header file anyway. Only a subset of CVC4 headers are installed with make install, and these all live in src/include/ and comprise the complete public interface. Public symbols are marked with CVC4_PUBLIC: 

 class CVC4_PUBLIC Expr {
   /* ... */
 public:
   Expr();
 };

Note here that types and private members need not be marked CVC4_EXPORT.

Now. What do you care? Well, if you ever forward-declare something that's public, you have to mark it PUBLIC in the forward-declaration too. (Is this true??)

Exception classes should all be marked CVC4_PUBLIC, because they might end up in user code (external to libcvc4) and their type_info information must be available to the catch block in user code. If you don't think your exception can (nor should by design) exit the library and end up in user code, then first double-check this, then triple-check it, then document that fact clearly at call site, the catch site (inside the library), and at the exception class definition.

See http://gcc.gnu.org/wiki/Visibility for more information on visibility.

Source file layout

Class header files

  • A class named AdjectiveNoun has its definition in adjective_noun.h. Each header file is guarded by a preprocessor macro to prevent duplicate declarations. For example, in adjective_noun.h:
   #ifndef __CVC4__ADJECTIVE_NOUN_H
   #define __CVC4__ADJECTIVE_NOUN_H
   
   ... declarations go here ...
   
   #endif /* __CVC4__ADJECTIVE_NOUN_H */

Generally all #includes of other headers should go inside the #ifndef guard. There is an exception though (with an #include going above the guard) for circular dependencies and other special circumstances. Such things should be documented in the code. All #includes should generally go at the top of the file, however, for inlined and template implementations following a class definition, sometimes additional files should be included after the class definition but before these member function definitions (again, when breaking circular dependencies).

If the class AdjectiveNoun is in the CVC4 namespace, the macro guard is named __CVC4__ADJECTIVE_NOUN_H. If it is in a sub-namespace Foo, then the macro guard is __CVC4__FOO__ADJECTIVE_NOUN_H. Note the two underscores for each :: and the two prefix underscores. One underscore is used between words in a type or namespace name.

  • Prefer forward-declaration of classes instead of #include'ing their header from another header, wherever this is possible.
  • Public headers (in src/include/), use preprocessor macro guard __CVC4_headername_H, for example, __CVC4_EXPR_H for cvc4_expr.h. Note here the one underscore between CVC4 and the name.
  • Other (non-class) header files should use a similar preprocessor macro guard, based on relevant module and header file name, as class header files do. In all cases, prefix the name of the guard with __CVC4_ and design it to be unlikely that it will ever conflict with any other (future) CVC4 header, whether it might be for internal use only or externally provided to a library user.
  • Everything should be in the CVC4 namespace, or a sub-namespace of CVC4 (based on module).
  • For test classes. Unit test classes (under test/unit/) are implemented as header files and do not need to be in a namespace, nor guarded by a preprocessor macro. The idea is to keep them as simple and clean as possible, so the tests can be easily read. They are special-purpose and compiled and linked individually, so they don't need these protections.

Class implementation files

  • A class named ThisIsAClass should have its implementation under src/ in this_is_a_class.cpp in the relevant module directory.

Imported sources

  • For imported sources. Make sure to add an exclusion to the contrib/update-copyright.pl script so that a CVC4 copyright isn't added when the script is run.

Source file headers

  • A common comment blurb heads all sources in CVC4 (including lex and yacc inputs and unit tests, but excluding imported sources).
  • A script, update-copyright.pl is used to maintain/update this comment blurb.

update-copyright.pl

  • 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 while keeping file-specific comments.
  • 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.)
  • Please consult svn diff before committing changes made by the script.
  • You can run the update script on specific files/directories by providing arguments to the script. By default it processes all sources in the src/ and test/ directories.

Using emacs

  • 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.
  • See contrib/editing-with-emacs.

Textual source layout

Whitespace/tabs

  • No tabs, please.
  • No whitespace between if, for, while, 'catch', etc., and their opening parenthesis.
  • One space between closing paren and open curly brace (except if aligning to other nearby source lines).
    • The matching right curly brace goes on a line by itself (possibly with an end-comment tagging the construct it's part of) in the same column as the first letter of the construct keyword. (That is, the right-brace lines up with the if, for, etc.)
  • One space around binary operators to avoid crowding, e.g.:
  x = y;
  z = y + 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 ) { ... }
  • 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 && z < x)) ...
  • while this is much preferred, since it emphasizes the negation of the entire condition:
  if( !( x + y > 4 && z < x ) ) { ... }
  • (assuming that it's preferable not to rewrite this as x + y <= 4 for some other reason of course).
  • Between type names and */& when declaring members and variables, to emphasize the introduced name is a pointer:
 Foo *a, *b;
  • 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);
  • 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/C++, the [] must come after the formal name and can't be attached to the type name, as it can be in Java). In particular:
 int main(int argc, char *argv[]);

is how the signature for the main function is written.

  • No trailing spaces please. M-x delete-trailing-whitespace in emacs might help.

Increment/Decrement

  • Preincrement/decrement preferred over postincrement/-decrement, e.g.:
  for(int x = 0; x < 10; ++x) { ... }

Bracing

  • Braces are 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)
       for(int i = 0; i < 10; ++i)
         if(a[i] < 5)
           a[i + 10] += a[i];
  • 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).
  • If in doubt, brace.
  • If anything is visually ambiguous, brace for clarity.

Indentation

  • Indentation level is 2.
  • No indentation under switch() {} or namespace {}
    • An exception is forward-declarations inside namespaces, where you do indent. For instance, from src/include/cvc4_expr.h:
  namespace CVC4 {
  
  namespace expr {
    class ExprValue;
  }/* CVC4::expr namespace */
  
  class Expr {
    /* ... */
  }/* class Expr */
  
  }/* CVC4 namespace */
  • Goto labels, case labels, and "private/public/protected" are recessed 2.
  • 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.
  • If something is templated in this way, the entire construct must be vertically separated from its surroundings with blank lines, and the template <> specification is on its own line.
  • Attempt to keep lines under 80 columns wide. Though if this makes things excessively ugly or confusing, it's probably ok to go over 80.
  • Indentation level is 2 for preprocessor directives as well, but the leading # is always in the first column. For example:
 #if A
 #  if B
 #    warning A B case
 #  else /* ! B */
 #    warning A -B case
 #  endif /* B */
 #else /* ! B */
 #  if B
 #    warning -A B case
 #  else /* ! B */
 #    warning -A -B case
 #  endif /* B */
 #endif /* A */

Misc C++

  • int foo(void) -- (void) unnecessary
  • An array reference a[i] in C++ may also be reversed as i[a], due to a symmetric definition of operator[] when applied to array and integral types in C. In CVC4, array indexing should be done in the standard way.
  • never use "using" in header files
  • enums require operator<<

Intentionally not covered

  • 0 vs NULL

Use of autotools: automake, autoconf, autoheader, libtool

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

Commit policy

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

Unit tests with CxxTest

There are two unit tests for modules:

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

Coverage testing with gcov

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

Other coding guidelines (as yet uncategorized)

  • No using or using namespace in header files, please!
  • 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 preferable to avoid memory allocation in this case).
  • Traditionally long declaration blocks (classes, namespaces, #endifs) should have an associated comment, even when they are short:
 namespace CVC4 {
 class Foo {
   /* pages
    * and
    * pages
    * go
    * by
    */
 };/* class Foo */
 }/* CVC4 namespace */

Others (if, while, switch, function definitions, etc.) should be close-commented for clarity where necessary. No space exists between the last token of the declaration or definition and the start of the close-comment.

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 2, but that the leading # is always in the first column, and that the #else takes the negation of the condition as a comment (but #endif takes the non-negated one). Here, note that the else-comment and close-comment is preceded by a single space. 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
  • Code and preprocessor indentation levels need not match unless it makes sense for them to.
  • ALWAYS COMMENT FALL-THROUGH CASES IN switch() {}:
 switch(foo) {
 case THIS_ONE:
   printf("this!\n");
   /* fall through */
 case THAT_ONE:
   printf("that!\n");
 }

Vertical spacing

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.

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

Unit testing

First, 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 --with-cxxtest-dir=~/cxxtest

Now, make check will run the CxxTest unit tests under test/.

Running unit tests

The simplest way to run all unit tests (and regressions and system tests) is to run make check in the top-level source directory. If you specifically want to run units and not other kinds of tests, make check in just the unit tests directory: 

$ make -C test/unit check

There is also experimental support for running unit tests related to a specific package. If you specifically want to run units for the expr package, for example, make check in the source directory for expr (not in the test directory): 

$ make -C src/expr check

Types of unit tests

There are three kinds of unit tests:

  • white tests test the system from a white-box point of view: they have access to the private functionality of classes (that is, usual C++ access restrictions do not apply), and they are written (typically by the author of the tested class) to test the internal functions and invariants of a class implementation. If the implementation details of a class change, one or more tests will likely change too.
    • By convention, white tests are named *_white.h. For example, for the Node class, which is in the CVC4::expr namespace, the test is under the expr/ directory in node_white.h.
  • black tests test the system from a black-box point of view: they have access only to the public functionality of classes (that is, usual C++ access restrictions do apply), and they are written (typically not by the author of the tested class) to test the external interface and invariants of a class. If the implementation details of a class change, the tests do not change; if the external interface of a class change, the test should be updated.
    • By convention, black tests are named *_black.h. For example, for the Node class, which is in the CVC4::expr namespace, the test is under the expr/ directory in node_black.h.
    • a subcategory of black tests are public tests; these test the system from a public point of view: they have access only to the public, functionality of libraries---the exported symbols of various libraries. Usual C++ access restrictions apply, as do the usual linking procedures against the library. Essentially, these public tests are black tests that test the public functionality of a public class. It is useful to separate them from the black tests in order to test that the exported symbols of a library are adequate. Public tests are named *_public.h.

Adding unit tests

To add a new test, create a test header file under test/unit (possibly in a subdirectory based on the relevant CVC4 module). If your test is a white-box test (it calls private functionality of the tested class directly and was written knowing the implementation details), its name should include White, e.g., NodeWhite, and it should be in a file like test/unit/expr/node_white.h, and you should add it to TESTS_WHITE in test/unit/Makefile.am. If your test is a black-box test (it calls only the public functionality of the tested class and was written knowing the interface only), its name should include Black, e.g., NodeBlack, and it should be in a file like test/unit/expr/node_black.h, and you should add it to TESTS_BLACK in test/unit/Makefile.am. If your test is a public test (it calls only the public functionality of the tested class, which is exported in the public-facing interface of the library), its name should include Public, e.g., ExprPublic, and it should be in a file like test/unit/expr/expr_public.h, and you should add it to TESTS_PUBLIC in test/unit/Makefile.am.

If you add your test to the correct TESTS_* block in test/unit/Makefile.am, and you're using the GNU C++ compiler, it will be compiled and linked correctly: that is, if it's a white-box test, the compiler will ignore access restrictions; if it's a black-box test, it can still access hidden symbols; and if it's a public test, it must only access the public-facing, exported symbols of the appropriate library.

Test implementations

Your test methods are named test*, e.g., testNull(). They return void and take no arguments.

There are numerous testing assertions you can make inside your testing code. For example: 

TS_ASSERT( 1 + 1 > 1 );
TS_ASSERT_EQUALS( 1 + 1, 2 );

There's also a TS_FAIL() that fails unconditionally: 

void testSomething() {
  TS_FAIL( "I don't know how to test this!" );
}

...and a TS_WARN(): 

void testSomething() {
  TS_WARN( "TODO: This test still needs to be written!" );
}

The users' guide is here for your reference.

Debugging unit tests

In order to run, CxxTest takes a header file, generates from that a new cpp file, and then then compiles the cpp file into a binary. The binaries for the unit tests live in the builds directory. If a unit test had the path 

 cvc4/test/unit/foo/bar.h

then the binary will have the path cvc4/builds/test/unit/foo/bar. (The CxxTest cpp file will have the path cvc4/builds/test/unit/foo/bar.cpp.)

If you have compiled cvc4 in debug mode, then the unit tests binaries can be run in gdb.

Tests are executed in the order that they appear in the header file. Moving a broken test to the top of the class definition (temporarily) makes it execute before the other tests. This is a useful trick for making debugging with gdb easier.

To recompile all of the tests, you can run make check in cvc4/. If you just run make after changing the source of cvc4 or a unit test, the test will not be recompiled.

Test rebuilding

bug 44 states:

As our unit-test database is growing the time to compile all the tests is getting increasingly unbearable, specially as every change in the source spawns recompilation of all tests. I know it might be impossible, but I would be wonderful if we could get around this somehow.

Regression testing

Regression tests in CVC4 are tests of the CVC4 binary.

To add a regression test, drop the file (which should have extension .smt or .cvc in test/regress/regressN/ (for N the regression level it should be in) and add it under TESTS to test/regress/regressN/Makefile.am. Then add it to subversion: 

 $ svn add test/regress/my_test.cvc

In the case of a .cvc benchmark, add one or more % EXPECT: output lines in the file (either at the top or scattered throughout). This is the expected output of CVC4 (running without -q or -v or debugging or anything). Any differences in output from the expected are flagged as test errors. See other .cvc regression tests for examples. If there are no EXPECT lines, the run_regression script flags an error. An EXIT line indicates the expected exit code of CVC4, but is optional; if omitted, CVC4 may have any exit status.

In the case of an .smt benchmark, make sure it has :status sat or :status unsat. This is used to determine if the output is correct and if CVC4 exits with the correct exit code.

This should be all that's necessary. Before committing to the repository, you should re-run autogen.sh in the root directory so that your commit includes the newest Makefile.in.

Multi-level regression testing

The directories

  • test/regress/regress0
  • test/regress/regress1
  • test/regress/regress2
  • test/regress/regress3

contain benchmarks at different regression levels. More difficult or longer-running benchmarks are typically placed in higher regression levels.

A simple make check at the top-level source directory (or top-level build or test source or build directories) does regression testing at level 0. For a specific level, use make regressN: this runs all tests at levels less than or equal to N. (At the top-level, the regressN target implies the check target, so you can make regress3 to run all unit tests, system tests, and also regressions at all levels.)

To run a specific level of regressions, e.g., regressions at level 2, without running regressions at lower levels, run a make check inside that specific directory. For example: 

 $ make -C test/regress/regress2 check

System testing

System, or API, testing is a form of regression testing on CVC4 libraries rather than the driver. Rather than .cvc and .smt instances as input, a system test is a source file that is built and linked against the cvc4 libraries and uses its API, bypassing the usual CVC4 driver. These tests are located under test/system/.

FIXME expand this section.

Command-line options

To add a new command-line option to CVC4, open up src/main/getopt.cpp. Add an entry to the cmdlineOptions array:

  • the first item is the long name of the command-line option. For example, verbose for --verbose.
  • the second item is required_argument, optional_argument, or no_argument, depending on whether the option takes an argument, an optional argument, or does not take an argument.
  • the third item should be NULL.
  • the last item should be the equivalent short option (a char), or a member of the OptionValue enumeration if there isn't an equivalent short option.

Next, if you don't have an equivalent short option, add the appropriate item to the OptionValue enumeration. If you do have an equivalent short option, append the short option to the string passed to getopt_long() in parseOptions(). Your option character should be followed by a single colon if an argument is required, or two colons if an argument is optional.

Next, modify the switch() construct in parseOptions() to handle your short option character (or the value from the OptionValue enumeration). If you need a new field in the CVC4::Options structure, add it in src/util/options.h.

Finally, change the usage string in src/main/usage.h.

NodeBuilders

FIXME. ADD CONTENT.

Attributes

What does this mean? 

/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/debug/../../../src/expr/attribute.h: In member function �$-1òøvoid CVC4::expr::AttributeManager::setAttribute(const CVC4::Node&, const AttrKind&, const typename AttrKind::value_type&) [with AttrKind = TestFlag6]òù:
/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/debug/../../../src/expr/node_manager.h:128:   instantiated from �$-1òøvoid CVC4::NodeManager::setAttribute(const CVC4::Node&, const AttrKind&, const typename AttrKind::value_type&) [with AttrKind = TestFlag6]òù
/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/debug/../../../src/expr/node.h:291:   instantiated from �$-1òøvoid CVC4::Node::setAttribute(const AttrKind&, const typename AttrKind::value_type&) [with AttrKind = TestFlag6]òù
/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/debug/../../../test/unit/expr/node_white.h:113:   instantiated from here
/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/debug/../../../src/expr/attribute.h:753: error: invalid use of undefined type �$-1òøstruct CVC4::expr::getTable<FooBar>òù
/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/debug/../../../src/expr/attribute.h:508: error: declaration of �$-1òøstruct CVC4::expr::getTable<FooBar>òù
/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/debug/../../../src/expr/attribute.h:755: error: invalid use of undefined type �$-1òøstruct CVC4::expr::getTable<FooBar>òù
/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/debug/../../../src/expr/attribute.h:508: error: declaration of �$-1òøstruct CVC4::expr::getTable<FooBar>òù
/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/debug/../../../src/expr/node_manager.h:128:   instantiated from �$-1òøvoid CVC4::NodeManager::setAttribute(const CVC4::Node&, const AttrKind&, const typename AttrKind::value_type&) [with AttrKind = TestFlag6]òù
/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/debug/../../../src/expr/node.h:291:   instantiated from �$-1òøvoid CVC4::Node::setAttribute(const AttrKind&, const typename AttrKind::value_type&) [with AttrKind = TestFlag6]òù
/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/debug/../../../test/unit/expr/node_white.h:113:   instantiated from here
/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/debug/../../../src/expr/attribute.h:755: error: invalid use of undefined type �$-1òøstruct CVC4::expr::getTable<FooBar>òù
/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/debug/../../../src/expr/attribute.h:508: error: declaration of �$-1òøstruct CVC4::expr::getTable<FooBar>òù
make[5]: *** [expr/node_white] Error 1

It means that the Attribute value-type (in this case FooBar), is invalid; there's no hashtable of appropriate kind to put it in. You probably want FooBar*.

Retrieved from "http://cvc4.cs.stanford.edu/w/index.php?title=Developer%27s_Guide&oldid=1222"