4 Running Daikon

This section describes how to run Daikon on a data trace (.dtrace) file, and describes Daikon’s command-line options. This section assumes you have already run a front end (e.g., an instrumenter) to produce a .dtrace file (and optionally .decls and .spinfo files); to learn more about that process, see Example usage, and see Front ends and instrumentation.

Run the Daikon invariant detector via the command

java -cp $DAIKONDIR/daikon.jar daikon.Daikon \
     [flags] dtrace-files... \
     [decls-files...] [spinfo-files...]

• The dtrace-files are data trace (.dtrace) files containing variable values from an execution of the target program.
• The decls-files are declaration (.decls) files containing program point declarations. Be sure to include all declaration files that are needed for the particular data trace file; the simplest way is to include every declaration file created when instrumenting the program.

  Not all Daikon front ends produce .decls files, since program point declarations may also appear in .dtrace files. For instance, the Chicory front end for Java (see Chicory) produces only .dtrace files. If there are no .decls files, then it is not necessary to include them on the command line to Daikon.

  Note that using a DynComp generated .decls file as input to Daikon will lead to a decl format error. The correct usage is to use the DynComp generated .decls file(s) as input to Chicory. See Detecting invariants in Java programs for more details.

• The spinfo-files are splitter info (.spinfo) files that enable detection of conditional invariants (see Conditional invariants); these are optional and may be created automatically or by hand.

The files may appear in any order; the file type is determined by whether the file name contains .decls, .dtrace, or .spinfo. As a special case, a file name of - means to read data trace information from standard input.

The optional flags are described in the sections that follow. For further ways to control Daikon’s behavior via configuration options, see Configuration options; also see the list of options to the front ends — such as DynComp (see DynComp for Java options), Chicory (see Chicory options) or Kvasir (see Kvasir options).

4.1 Options to control Daikon output

--help

Print usage message.

-o inv_file

Output serialized invariants to the specified file; they can later be postprocessed, compared, etc. Default: basename.inv.gz in the current directory, where the first data trace file’s basename starts with basename.dtrace. Default is no serialized output, if no such data trace file was supplied. If a data trace file was supplied, there is currently no way to avoid creating a serialized invariant file.

--no_text_output

Don’t print invariants as text output. This option may be used in conjunction with the -o option.

--format name

Produce output in the given format. For a list of the output formats supported by Daikon, see Invariant syntax.

--show_progress

--no_show_progress

Prints (respectively, suppresses) timing information as major portions of Daikon are executed.

--show_detail_progress

Like --show_progress but includes details about invariants.

--noversion

Suppress the printing of version information

--output_num_samples

Output numbers of values and samples for invariants and program points; this is a debugging flag. (That is, it helps you understand why Daikon produced the output that it did.)

The ‘Samples breakdown’ output indicates how many samples in the .dtrace file had a modified value (‘m’), had an unmodified value (‘u’), and had a nonsensical value (‘x’). The summary uses a capital letter if the sample had any of the corresponding type of variable, and a lower-case letter if it had none. These types affect statistical tests that determine whether a particular invariant (that was true over all the test runs) is printed.

Only variables that appear in both the pre-state and the post-state (variables that are in scope at both procedure exit and entry) are eligible to be listed as modified or unmodified. This is why the list of all variables is not the union of the modified and unmodified variables.

--files_from filename

Read a list of .decls, .dtrace, or .spinfo file names from the given text file, one filename per line, as an alternative to providing the file names on the command line.

--server dirname

Server mode for Daikon in which it reads files from dirname as they appear (sorted lexicographically) until it finds a file ending in ‘.end’, at which point it calculates and outputs the invariants.

--omit_from_output [0rs]

Omit some potentially redundant information from the serialized output file produced with -o. By default, the serialized output contains all of the data structures produced by Daikon while inferring invariants. Depending on the use to which the serialized output will later be put, the file can sometimes be significantly shortened by omitting information that is no longer needed. The flag should be followed by one or more characters each representing a kind of structures the can be omitted. The following characters are recognized:

0 (zero)

Omit information about program points that were declared, but for which no samples were found in any .dtrace file.

r

Omit reflexive invariants, those in which a variable appears more than once. Usually, such invariants are not interesting, because their meaning is duplicated by invariants with fewer variables: for instance, x = x - x and y = z + z can be expressed as x = 0 and y = 2 * z instead. However, Daikon generates and uses such invariants internally to decide what invariants to create when two previously equal variables turn out to be different.

s

Omit invariants that are suppressed by other invariants. Suppression refers to a particular optimization in which the processing of an invariant is postponed as long as certain other invariants that logically imply it hold.

For most uses of serialized output in the current version, it is safe to use the 0 and r omissions, but the s omission will cause subtle output changes. In many cases, the amount of space saved is modest (typically around 10%), but the savings can be more substantial for programs with many unused program points, or program points with many variables.

4.2 Options to control invariant detection

--conf_limit val

Set the confidence limit for justifying invariants. If the confidence level for a given invariant is larger than the limit, then Daikon outputs the invariant. This mechanism filters out invariants that are satisfied purely by chance. This is only relevant to invariants that were true in all observed samples; Daikon never outputs invariants that were ever false.

val must be between 0 and 1; the default is .99. Larger values yield stronger filtering.

Each type of invariant has its own rules for determining confidence. See the computeConfidence method in the Java source code for the invariant.

For example, consider the invariant a<b whose confidence computation is 1 - 1/2^numsamples, which indicates the likelihood that the observations of a and b did not occur by chance. If there were 3 samples, and a<b on all of them, then the confidence would be 7/8 = .875. If there were 6 samples, and a<b on only 5 on them, the confidence would be 0. If there were 9 samples, and a<b on all of them, then the confidence would be 1-1/2^9 = .998.

There are two ways to print the confidence of each invariant. You can use Diff (see Invariant Diff):

java -cp $DAIKONDIR/daikon.jar daikon.diff.Diff MyFile.inv.gz

or you can use PrintInvariants (see Printing invariants):

java -cp $DAIKONDIR/daikon.jar daikon.PrintInvariants --dbg daikon.PrintInvariants.repr \
     MyFile.inv.gz

To print the confidence of each invariant that is discarded, run Daikon with the --disc_reason all command-line option (see Daikon debugging options).

--list_type classname

Indicate that the given class implements the java.util.List interface. The preferred mechanism for indicating such information is the ListImplementors section of the .decls file. See ListImplementors declaration in Daikon Developer Manual.

--user-defined-invariant classname

Use a user-defined invariant that not built into Daikon but is defined in the given class. The classname should be in the fully-qualified format expected by Class.getName(), such as “mypackage.subpackage.ClassName”, and its .class file should appear on the classpath.

--disable-all-invariants

Disable all known invariants: all those that are built into Daikon, and all those that have been specified by --user-defined-invariant so far. An invariant may be re-enabled after this option is specified, see Options to enable/disable specific invariants.

--nohierarchy

Avoid connecting program points in a dataflow hierarchy. For example, Daikon normally connects the :::ENTER program points of class methods with the class’s :::CLASS program point, so that any invariant that holds on the :::CLASS program point is considered to hold true on the :::ENTER program point. With no hierarchy, each program point is treated independently. This is for using Daikon on applications that do not have a concept of hierarchy. It can also be useful when you wish to process unmatched enter point samples from a trace file that is missing some exit point samples.

--suppress_redundant

Suppress display of logically redundant invariants, using the Simplify automatic theorem prover. Daikon already suppresses most logically redundant output (this can be controlled by invariant filters; see Invariant filters. For example, if ‘x >= 0’ and ‘x > 0’ are both true, then Daikon outputs only ‘x > 0’. Use of the --suppress_redundant option tells Daikon to use Simplify to eliminate even more redundant output, and should be used if it is important that absolutely no redundancies appear in the output.

The Simplify program must be installed in order to take advantage of this option (see Installing Simplify). Beware that Simplify can run slowly; the amount of effort Simplify exerts for each invariant can be controlled using both the daikon.simplify.Session.simplify_max_iterations and daikon.simplify.Session.simplify_timeout configuration options.

4.3 Processing only part of the trace file

--ppt-select-pattern=ppt_regexp

Only process program points whose names match the regular expression. The --ppt-omit-pattern argument takes precedence over this argument.

--ppt-omit-pattern=ppt_regexp

Do not process program points whose names match the regular expression. This takes precedence over the --ppt-select-pattern argument.

--var-select-pattern=var_regexp

Only process variables (whether in the trace file or derived) whose names match the regular expression. The --var-omit-pattern argument takes precedence over this argument.

--var-omit-pattern=var_regexp

Ignore variables (whether in the trace file or derived) whose names match the regular expression. This takes priority over the --var-select-pattern argument.

All of the regular expressions used by Daikon use Java’s regular expression syntax. Multiple items can be matched by using the logical or operator (‘|’), for example var1|var2|var3. Java’s regular expression syntax is similar to Perl’s but not exactly the same.

The ...-omit-pattern arguments take precedence: if a name matches an omit pattern, it is excluded. If a name does not match an omit pattern, it is tested against the select pattern (if any). If any select patterns are specified, the name must match one of the patterns in order to be included. If no select patterns are specified, then any ‘ppt’ name that does not match the omit patterns is included.

Using --ppt-select-pattern and --ppt-omit-pattern can save time even if there are no samples for the excluded program points, as Daikon can skip the declarations and need not initialize data structures that would be used if samples were encountered.

Front ends such as Chicory (see Program points in Chicory output) and Kvasir (see Kvasir options), and other tools such as DynComp (see DynComp for Java options) and PrintInvariants (see Printing invariants), also support these command-line options (Kvasir names them slightly differently). Passing the command-line option to the front end means that the target program will run faster and the trace file will be smaller.

4.4 Daikon configuration options

--config filename

Load the configuration settings specified in the given file. See Configuration options, for details.

--config_option name=value

Specify a single configuration setting. See Configuration options, for details.

4.5 Daikon debugging options

Also see configuration options related to debugging (see Debugging options).

--dbg category

--debug

These debugging options cause output to be written to a log file (by default, to the terminal); in other words, they enable a Logger. The --dbg category option enables debugging output (logging output) for a specific part of Daikon; it may be specified multiple times, permitting fine-grained control over debugging output. The --debug option turns on all debugging flags. (This produces a lot of output!) Most categories are class or package names in the Daikon implementation, such as daikon.split or daikon.derive.binary.SequencesJoin. Only classes that check the appropriate categories are affected by the debug flags; you can determine this by looking for a call to Logger.getLogger in the specific class.

--track class<var1,var2,var3>@ppt

Turns on debugging information on the specified class, variables, and program point. In contrast to the --dbg option, track logging follows a particular invariant through Daikon. Multiple --track options can be specified. Each item (class, variables, and program point) is optional. Multiple classes can be specified separated by vertical bars (‘|’). Matching is a simple substring (not a regular expression) comparison. Each item must match in order for a printout to occur. For more information, see Track logging in Daikon Developer Manual.

--disc_reason inv_class<var1,var2,...>@ppt

Prints all discarded invariants of class inv_class at the program point specified that involve exactly the variables given, as well as a short reason and discard code explaining why they were not worthy of print. Any of the three parts of the argument may be made a wildcard by excluding it. For example, ‘inv_class’ and ‘<var1,var2,...>@ppt’ are valid arguments. Some concrete examples are ‘Implication<x,y>@foo():::EXIT’, ‘<x,y>@foo():::EXIT’, and ‘Implication<x,y>’. To print all discarded invariants, use the argument ‘all’.

--mem_stat

Prints memory usage statistics into a file named stat.out in the current directory.