6.170 / Spring 2004 / Daikon Invariant Detector

Handout S5

Contents:

Overview

The Daikon invariant detector reports properties that appear to hold at certain points in a program. The reported properties are similar to ones you might write in an assert statement, a precondition ("requires" clause), or postcondition ("effects" clause); for example, "x == abs(y)", "i < myArray.length", or "myArray is sorted". These invariants can be useful in program understanding and a host of other applications. Daikon operates by running the program and examining the values it computes, looking for patterns and relationships among those values. It reports properties that were true for all the executions that it observed, but there is no guarantee that those properties will hold on future runs.

You can obtain more information about Daikon from its website. In particular, you can read its manual (HTML, PDF) or download it. If you have any problems with Daikon, please send mail to daikon-developers@pag.lcs.mit.edu and/or ask a 6.170 staff member.

Running Daikon

Daikon is provided for you in the 6.170 locker. Running daikon without any arguments will display usage information: 
  athena% daikon
  Usage: daikon [OPTIONS] <CLASS TO OBSERVE> <TEST DRIVER> [MAIN ARGUMENTS]
  Options:
    -o, --output FILE   Save invariants in FILE.inv
    ...
The "CLASS TO OBSERVE" variable specifies the class file Daikon will observe for invariant detection while running your test driver. For the test driver, you must supply the name of a "main" class which provides the method "public static void main(String[] args)". Daikon will run this class to exercise your program. See the command line options section for details on the available options for daikon.

Command line options

-o, --output FILE
Save invariants in FILE.inv and source in FILE.src.tar.gz. If no name is given, a name is automatically generated and used.

-t, --textfile
Save a textual listing of invariants to a .txt file.

-v, --verbose
Display progress messages while running.

-c, --cleanup
Remove files left over from an interrupted session before starting. Should be used only when daikon detects left-over files and instructs you to use this option.

-n, --nogui
Create the invariants file (and .txt file, if -t is given), but do not start the GUI.

Understanding the invariants

The GUI (Graphical User Interface) shows a tree view of the results. On the first level, it shows a list of the classes under inspection. As each class is expanded, a list of program points is displayed.

Program points

A program point is usually associated with a specific place in the source code. For example, the ENTER point under the foo() node represents the preconditions upon entry to the foo() method.

The ENTER and EXIT program points identify points at the entry and exit of the given method. The OBJECT program point indicates representation invariants (sometimes called object invariants) that hold for any object of the given class, from the point of view of a client or user. These properties hold at entry to and exit from every public method of the class. The CLASS program point is like the OBJECT program point, but for static variables only.

Invariant syntax

A few parts of the syntax of displayed invariants may be confusing.

In the output, the application of orig(x) to a variable x refers to the original value of a formal parameter. orig() variables appear only at EXIT program points.

Negative array indices count backwards from the length of the array; for instance, a[-1] denotes the last element of array a; it is just syntactic sugar for a[a.length-1].

More details

For even more details on interpreting Daikon output, you can see the "Daikon output" chapter of the Daikon manual.

Running Daikon Manually

While the method given above will be sufficient for most users, some may want to explore further. This section describes how to use Daikon without the help of the wrapper script. One reason you might want to do this is because it lets you control invariant detection (for instance, which classes are examined and which are ignored). Another benefit is that you may edit and reinstrument some files without starting the whole process each time. Finally, by doing the steps individually, you will gain a better understanding of what is going on behind the scenes. More complete details (including an example of using Daikon) appear in the Daikon manual.

Detecting invariants involves three steps:

  1. Instrument the program to add instructions that output variable values.
  2. Run the program (probably using a test suite) to create data trace files.
  3. Run the Daikon invariant detector over the data trace files to detect invariants.

Step 1: Instrumentation

The front end modifies your program so that, in addition to performing its original task, it also writes variable values to a data trace file. The front end works on Java code that corresponds to any version of the Java language, from 1.0 to 1.3. As of February 2003, it does not work on Java 1.4 (but much code you will write does not use the Java 1.4 extensions).

Run dfej, the Daikon Front End for Java, on your Java source files: 

      dfej filename1.java filename2.java ...
The Daikon Front End for Java does two things:
  1. dfej writes instrumented versions of the files to a daikon-java/ directory.
  2. dfej creates declaration files named filename1.decls, etc. in a daikon-output/ directory.

Only the specified Java files will be instrumented; other files will be run uninstrumented. This permits you to control the scope of invariant detection.

Compile the generated files, e.g. 

        javac daikon-java/*.java

Step 2: Run the program

Run the program over some test suite in order to create a collection of data trace files. You can run the instrumented program in just the same way you did before; the only behavioral change will be writing a .dtrace file to the daikon-output/ subdirectory (which is created if it does not already exist). Only one .dtrace file is created, even though multiple .decls files might have been created (one for each source file) when the program was instrumented.

After instrumentation, there are two versions of the program: the original version, and the instrumented version which appears in the daikon-java/ directory. Make sure that the daikon-java/ directory appears on your class path before the directory containing the original Java code. You can do this by running the program from that directory, if "." (the current directory) appears early on your class path, or you can add the daikon-java/ directory to your class path explicitly.

Step 3: Detect invariants in the data trace files

Run the Daikon invariant detector via the command 

    java daikon.Daikon decl-files... trace-files...
The decl-files are declaration (.decl) files created at instrumentation time. The trace-files are data trace (.dtrace) files created by running the instrumented program. Be sure to include all declaration files that are needed for the particular data trace file; the simplest way is to include all the declaration files created when instrumenting the program that is read.

By default, Daikon produces a textual listing of invariants to standard output (the terminal); however, it can also produce a file that can be loaded in the GUI, using the -o option: 

    java daikon.Daikon -o foo.inv decl-files... trace-files...
Then, you may run the GUI on that file: 
    java daikon.gui.InvariantsGUI foo.inv
Back to the 6.170 home page.
For problems or questions regarding this page, contact: 6.170-webmaster@mit.edu.