Next: Daikon output, Previous: Example usage, Up: Top [Contents][Index]

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

Next: Options to control invariant detection, Up: Running Daikon [Contents][Index]

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

Next: Processing only part of the trace file, Previous: Options to control Daikon output, Up: Running Daikon [Contents][Index]

### 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 is 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.

Next: Daikon configuration options, Previous: Options to control invariant detection, Up: Running Daikon [Contents][Index]

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

Next: Daikon debugging options, Previous: Processing only part of the trace file, Up: Running Daikon [Contents][Index]

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

Previous: Daikon configuration options, Up: Running Daikon [Contents][Index]

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

Previous: Daikon configuration options, Up: Running Daikon [Contents][Index]