6.170 / Spring 2001 / Daikon Invariant Detector

Handout S3

Contents:

Overview

The Daikon invariant detector reports properties that are likely to hold at certain points in a program. The reported properties are arithmetic equations such as you might write in an assert statement, a precondition ("requires" clause), or postcondition ("effects" clause); for example, "x == abs(y)" or "i < myArray.length". 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.

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] <MAIN CLASS> [MAIN ARGUMENTS]
  Options:
    -o, --output FILE   Save invariants in FILE.inv
    ...
At minimum, 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 excercise 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. Shoult 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].

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.

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 should work on Java code which corresponds to any version of the Java language, from 1.0 to 1.3.

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.

After running your Java application, run modbit-munge.pl on the resulting .dtrace file: 

    modbit-munge.pl myprog.dtrace
This step fixes up some potential problems that may appear in the trace file.

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 declaratation (.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 proram that is read.

By default, Daikon produces a textual listing of invariants to stdandard output (the terminal); however, it can also produce a file which 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

Daikon homepage
$Id: daikon-6170.html,v 1.11 2001/02/09 10:04:52 mistere Exp $