Next: Running Daikon, Previous: Installing Daikon, Up: Top [Contents][Index]

## 3 Example usage for Java, C/C++, C#/F#/Visual Basic, Perl, and Eiffel

Detecting invariants involves two steps:

1. Obtain one or more data trace files by running your program under the control of a front end (also known as an instrumenter or tracer) that records information about variable values. You can run your program over one or more inputs of your own choosing, such as regression tests or a typical user input session. You may choose to obtain trace data for only part of your program; this can avoid inundating you with output, and can also improve performance.
2. Run the Daikon invariant detector over the data trace files (see Running Daikon). This detects invariants in the recorded information. You can view the invariants textually, or process them with a variety of tools.

This section briefly describes how to obtain data traces for Java, C, C#, Perl, and Eiffel programs, and how to run Daikon. For detailed information about these and other front ends that are available for Daikon, see Front ends and instrumentation.

Next: Detecting invariants in C/C++ programs, Up: Example usage [Contents][Index]

### 3.1 Detecting invariants in Java programs

Before detecting invariants in Java programs, you must run `make -C ${DAIKONDIR}/java dcomp_rt.jar` (for more details, see Instrumenting the JDK with DynComp).

In order to detect invariants in a Java program, you will run the program twice — once using DynComp (see DynComp for Java) to create a `.decls` file and once using Chicory (see Chicory) to create a data trace file. Then, run Daikon on the data trace file to detect invariants. With the `--daikon` option to Chicory, a single command performs the last two steps.

For example, if you usually run

    java -cp myclasspath mypackage.MyClass arg1 arg2 arg3

then instead you would run these two commands:

    java -cp myclasspath:${DAIKONDIR}/daikon.jar daikon.DynComp mypackage.MyClass arg1 arg2 arg3
    java -cp myclasspath:${DAIKONDIR}/daikon.jar daikon.Chicory --daikon \
                        --comparability-file=MyClass.decls-DynComp \
                        mypackage.MyClass arg1 arg2 arg3

and the Daikon output is written to the terminal.

Next: Detecting invariants when running a Java program from a jar file, Up: Detecting invariants in Java programs [Contents][Index]

#### 3.1.1 StackAr example

The Daikon distribution contains some sample programs that will help you get practice in running Daikon.

To detect invariants in the `StackAr` sample program, perform the following steps after installing Daikon (see Installing Daikon).

1. Compile the program with the `-g` switch to enable debugging symbols. (The program and test suite appear in the `DataStructures` subdirectory.)

       cd examples/java-examples/StackAr
       javac -g DataStructures/*.java

2. Run the program under the control of DynComp to generate comparability information in the file `StackArTester.decls-DynComp`.

       java -cp .:${DAIKONDIR}/daikon.jar daikon.DynComp DataStructures.StackArTester

3. Run the program a second time, under the control of the Chicory front end. Chicory observes the variable values and passes the information to Daikon. Daikon infers invariants, prints them, and writes a binary representation of them to file `StackArTester.inv.gz`.

       java -cp .:${DAIKONDIR}/daikon.jar daikon.Chicory --daikon \
            --comparability-file=StackArTester.decls-DynComp \
            DataStructures.StackArTester

   Alternately, replacing the `--daikon` argument by `--daikon-online` has the same effect, but does not write a data trace file to disk.

   If you wish to have more control over the invariant detection process, you can split the third step above into multiple steps. Then, step 3 would become:

   1. Run the program under the control of the Chicory front end in order to create a trace file named `StackArTester.dtrace.gz`.

          java -cp .:${DAIKONDIR}/daikon.jar daikon.Chicory \
               --comparability-file=StackArTester.decls-DynComp \
               DataStructures.StackArTester

   2. Run Daikon on the trace file.

          java -cp ${DAIKONDIR}/daikon.jar daikon.Daikon StackArTester.dtrace.gz

4. Examine the invariants. (They were also printed to standard out by the previous step.)

   There are various ways to do this.

   - Examine the output from running Daikon. (You may find it convenient to capture the output in a file; add ‘`> StackAr.txt`’ to the end of the command that runs Daikon.)
   - Use the `PrintInvariants` program to display the invariants.

         java -cp ${DAIKONDIR}/daikon.jar daikon.PrintInvariants StackArTester.inv.gz

     For more options to the `PrintInvariants` program, see Printing invariants.

   - Use the Annotate program to insert the invariants as comments into the Java source program.

         java -cp .:${DAIKONDIR}/daikon.jar daikon.tools.jtb.Annotate StackArTester.inv.gz \
              DataStructures/StackAr.java

     Now examine file `DataStructures/StackAr.java-escannotated`. For more information about the Annotate program, see Annotate.

Daikon can analyze multiple runs (executions) of the program. You can supply Daikon with multiple trace files:

    java -cp .:${DAIKONDIR}/daikon.jar daikon.Chicory \
         --dtrace-file=StackArTester1.dtrace.gz \
         --comparability-file=StackArTester.decls-DynComp DataStructures.StackArTester
    java -cp .:${DAIKONDIR}/daikon.jar daikon.Chicory \
         --dtrace-file=StackArTester2.dtrace.gz \
         --comparability-file=StackArTester.decls-DynComp DataStructures.StackArTester
    java -cp .:${DAIKONDIR}/daikon.jar daikon.Chicory \
         --dtrace-file=StackArTester3.dtrace.gz \
         --comparability-file=StackArTester.decls-DynComp DataStructures.StackArTester
    java -cp ${DAIKONDIR}/daikon.jar daikon.Daikon StackArTester*.dtrace.gz

(In this example, all the runs are identical, so multiple runs yield the same invariants as one run.)

Next: Understanding the invariants, Previous: StackAr example, Up: Detecting invariants in Java programs [Contents][Index]

#### 3.1.2 Detecting invariants when running a Java program from a jar file

If your Java program is run directly from a `jar` file, such as either of:

    java mypackage.jar arguments
    java -cp myclasspath mypackage.jar arguments

then to detect invariants in that Java program, run these two commands:

    java -cp myclasspath:${DAIKONDIR}/daikon.jar daikon.DynComp <MyMain> arguments
    java -cp myclasspath:${DAIKONDIR}/daikon.jar daikon.Chicory --daikon \
         --comparability-file=<MyMain>.decls-DynComp <MyMain> arguments

where `<MyMain>` is the Main-class of the `jar` file, which you can determine by running the command:

    unzip -p mypackage.jar META-INF/MANIFEST.MF | grep '^Main-Class:'

Next: Second Java example, Previous: Detecting invariants when running a Java program from a jar file, Up: Detecting invariants in Java programs [Contents][Index]

#### 3.1.3 Understanding the invariants

This section examines some of the invariants for the `StackAr` example. For more help interpreting invariants, see Interpreting output.

The `StackAr` example is an array-based stack implementation. Take a look at `DataStructures/StackAr.java` to get a sense of the implementation. Now, look at the sixth section of Daikon output.

    ======================================================================
    StackAr:::OBJECT
    this.theArray != null
    this.theArray.getClass().getName() == java.lang.Object[].class
    this.topOfStack >= -1
    this.topOfStack <= size(this.theArray[])-1
    ======================================================================

These four annotations describe the representation invariant. The array is never null, and its run-time type is `Object[]`. The `topOfStack` index is at least -1 and is less than the length of the array.

Next, look at the invariants for the `top()` method. `top()` has two different exit points, at lines 74 and 75 in the original source. There is a set of invariants for each exit point, as well as a set of invariants that hold for all exit points. Look at the invariants when `top()` returns at line 75.

    ======================================================================
    StackAr.top():::EXIT75
    return == this.theArray[this.topOfStack]
    return == this.theArray[orig(this.topOfStack)]
    return == orig(this.theArray[post(this.topOfStack)])
    return == orig(this.theArray[this.topOfStack])
    this.topOfStack >= 0
    return != null
    ======================================================================

The return value is never null, and is equal to the array element at index `topOfStack`. The top of the stack is at least 0.

Previous: Understanding the invariants, Up: Detecting invariants in Java programs [Contents][Index]

#### 3.1.4 A second Java example

A second example is located in the `examples/java-examples/QueueAr` subdirectory. Run this sample using the following steps:

- Compile

      cd examples/java-examples/QueueAr
      javac -g DataStructures/*.java

- Trace file generation and invariant detection

      java -cp .:${DAIKONDIR}/daikon.jar daikon.DynComp DataStructures.QueueArTester
      java -cp .:${DAIKONDIR}/daikon.jar daikon.Chicory --daikon \
           --comparability-file=QueueArTester.decls-DynComp \
           DataStructures.QueueArTester

Alternately, you can split the very last command into two parts:

- Trace file generation

      java -cp .:${DAIKONDIR}/daikon.jar daikon.Chicory \
           --comparability-file=QueueArTester.decls-DynComp \
           DataStructures.QueueArTester

- Invariant detection

      java -cp ${DAIKONDIR}/daikon.jar daikon.Daikon QueueArTester.dtrace.gz

Next: Detecting invariants in C# programs, Previous: Detecting invariants in Java programs, Up: Example usage [Contents][Index]

### 3.2 Detecting invariants in C/C++ programs

In order to detect invariants over C or C++ programs, you must first install a C/C++ front end (instrumenter). We recommend that you use Kvasir (see Kvasir), and this section gives examples using Kvasir. By default, Kvasir also runs the DynComp tool to improve Daikon’s performance and Daikon’s output by filtering out invariants involving unrelated variables (see DynComp for C/C++).

To use the C/C++ front end Kvasir with your program, first compile your program. (If you use `gcc` to compile your program, use the following command-line arguments: `-gdwarf-3 -no-pie`. Also use `-fno-stack-clash-protection` if your `gcc` supports it. Note that if your build system separates the compile and link steps, then `-no-pie` needs to be on the link step.) Then, run your program as usual, but prepend `kvasir-dtrace` to the command line.

Kvasir will produce two output files: a `.dtrace` file containing a trace of a particular execution, and a `.decls` file that contains information about what variables and functions exist in a program, along with information grouping the variables into abstract types. You will supply both of these files to Daikon.

For more information about Kvasir, including more detailed documentation on its command-line options, see Kvasir.

Next: Dealing with large examples, Up: Detecting invariants in C/C++ programs [Contents][Index]

#### 3.2.1 C examples

The Daikon distribution comes with several example C programs to enable users to become familiar with running Daikon on C programs. These examples are located in the `examples/c-examples` directory.

To detect invariants for a program with Kvasir, you need to perform two basic tasks: run the program under Kvasir to create a trace and declaration files (steps 1–3), and run Daikon over these files to produce invariants (step 4). The following instructions are for the wordplay example, which is a program for finding anagrams.

1. Change to the directory containing the program.

       cd ${DAIKONDIR}/examples/c-examples/wordplay

2. Compile the program with DWARF-2 or DWARF-3 debugging information enabled (and all optimizations disabled).

       gcc -gdwarf-3 -no-pie wordplay.c -o wordplay

   Kvasir can also be used for programs constructed by compiling a number of `.c` files separately, and then linking them together; in such a program, specify `-gdwarf-3` when compiling each source file containing code you wish to see invariants about.

3. Run the program just as you normally would, but prepend `kvasir-dtrace` to the command line.

       kvasir-dtrace ./wordplay -f words.txt 'Daikon Dynamic Invariant Detector'

   Any options to the program can be specified as usual; here, for instance, we give commands to look for anagrams of the phrase “Daikon Dynamic Invariant Detector” using words from the file `words.txt`.

   Executing under Kvasir, the program runs normally, but Kvasir executes additional checks and collects trace information (for this reason, the program will run more slowly than usual). Kvasir creates a directory named `daikon-output` under the current directory, and creates the `wordplay.dtrace` file, which lists variable values, and the `wordplay.decls` file that contains information about what variables and functions exist in a program, along with information grouping the variables into abstract types.

   Kvasir will also print messages if it observes your program doing something with undefined effects; these may indicate bugs in your program, or they may be spurious. (If they are bugs, they can also be tracked down by using Valgrind (https://valgrind.org/) with its regular memory checking tool; if they do not appear with that tool, they are probably spurious).

4. Run Daikon on the trace and declaration files.

       java -cp ${DAIKONDIR}/daikon.jar daikon.Daikon \
            --config_option daikon.derive.Derivation.disable_derived_variables=true \
            daikon-output/wordplay.decls daikon-output/wordplay.dtrace

   The invariants are printed to standard output, and a binary representation of the invariants is written to `wordplay.inv.gz`. Note that the example uses a configuration option to disable the use of derived variables; it can also run without that option, but takes significantly longer.

   Daikon can analyze multiple runs (executions) of the program. You can supply Daikon with multiple trace files:

       kvasir-dtrace --dtrace-file=daikon-output/wordplay1.dtrace \
           ./wordplay -f words.txt 'daikon dynamic invariant detector'
       kvasir-dtrace --no-dyncomp --dtrace-file=daikon-output/wordplay2.dtrace \
           ./wordplay -f words.txt 'better results from multiple runs'
       kvasir-dtrace --no-dyncomp --dtrace-file=daikon-output/wordplay3.dtrace \
           ./wordplay -f words.txt 'more testing equals better testing'
       java -Xmx7g -cp ${DAIKONDIR}/daikon.jar daikon.Daikon \
           daikon-output/wordplay*.dtrace daikon-output/wordplay.decls

   Note that this example makes the assumption that the DynComp `.decls` information for `wordplay` does not vary from run to run. Thus it specifies `--no-dyncomp` on subsequent runs to improve performance. (This assumption may not be true for other programs.)

   Alternatively, you can append information from multiple runs in a single trace file:

       kvasir-dtrace --dtrace-file=daikon-output/wordplay-all.dtrace \
           ./wordplay -f words.txt 'daikon dynamic invariant detector'
       kvasir-dtrace --no-dyncomp --dtrace-append \
           --dtrace-file=daikon-output/wordplay-all.dtrace \
           ./wordplay -f words.txt 'better results from multiple runs'
       kvasir-dtrace --no-dyncomp --dtrace-append \
           --dtrace-file=daikon-output/wordplay-all.dtrace \
           ./wordplay -f words.txt 'more testing equals better testing'
       java -Xmx7g -cp ${DAIKONDIR}/daikon.jar daikon.Daikon \
           daikon-output/wordplay-all.dtrace daikon-output/wordplay.decls

5. Examine the invariants. As described in StackAr example, there are several ways to do this:
   - Examine the output from running Daikon.
   - Use the `PrintInvariants` program to display the invariants.

   For help understanding the invariants, see Interpreting output.

There is a second example C program in the `bzip2` directory. It may be run in a similar fashion as the `wordplay` example, but it is a more complex program and the `kvasir-dtrace` step may take several minutes.

Previous: C examples, Up: Detecting invariants in C/C++ programs [Contents][Index]

#### 3.2.2 Dealing with large examples

Since the default memory size used by a Java virtual machine varies, we suggest that Daikon be run with at least 256 megabytes of memory (and perhaps much more). For many JVMs, specify a maximum heap size of 7 GB by using `-Xmx7g`. For more information about specifying the memory usage for Daikon, see Out of memory.

Disk usage can be reduced by specifying that the front end should compress its output `.dtrace` files.

In some cases, the time and space requirements of the examples can be reduced by reducing the length of the program run. However, Daikon’s running time depends on both the length of the test run and the size of the program data (such as its use of global variables and nested data structures). The examples also demonstrate disabling derived variables, which significantly improves Daikon’s performance at the cost of producing fewer invariants. For more techniques for using Daikon with large programs and long program runs, see Large dtrace files.

Next: Detecting invariants in Perl programs, Previous: Detecting invariants in C/C++ programs, Up: Example usage [Contents][Index]

### 3.3 Detecting invariants in C#, F#, and Visual Basic programs

The Daikon front end for .NET languages (C#, F#, and Visual Basic) is called Celeriac.

Please see its documentation at https://github.com/codespecs/daikon-dot-net-front-end.

Next: Detecting invariants in Eiffel programs, Previous: Detecting invariants in C# programs, Up: Example usage [Contents][Index]

### 3.4 Detecting invariants in Perl programs

The Daikon front end for Perl is called `dfepl`.

Using the Perl front end is a two-pass process: first you must run the annotated program so that the runtime system can dynamically infer the kind of data stored in each variable, and then you must re-annotate and re-run the program with the added type information. This is necessary because Perl programs do not contain type declarations.

`dfepl` requires version 5.8 or later of Perl.

Next: Perl examples, Up: Detecting invariants in Perl programs [Contents][Index]

#### 3.4.1 Instrumenting Perl programs

Perl programs must be instrumented twice. First they must be instrumented without type information. Then, once the first instrumented version has been run to produce type information, they must be instrumented again taking the type information into account.

To instrument a stand-alone Perl program, invoke `dfepl` with the name of the program as an argument.

    dfepl program.pl

To instrument a Perl module or a collection of modules, invoke `dfepl` either with the name of each module, or with the name of a directory containing the modules. To instrument all the modules in the current directory, give `dfepl` the argument `.`. For instance, if the current directory contains a module `Acme::Trampoline` in `Acme/Trampoline.pm` and another module `Acme::Date` in `Acme/Date.pm`, they can be annotated by either of the following two commands:

    dfepl Acme/Trampoline.pm Acme/Date.pm
    dfepl .

Once type information is available, run the instrumentation command again with the `-T` or `-t` options added to use the produced type information.

For more information about `dfepl`, see dfepl.

Previous: Instrumenting Perl programs, Up: Detecting invariants in Perl programs [Contents][Index]

#### 3.4.2 Perl examples

The Daikon distribution includes sample Perl programs suitable for use with Daikon in the `examples/perl-examples` directory.

Here are step-by-step instructions for examining a simple module, `Birthday.pm`, as used by a test script `test-bday.pl`.

1. Change to the directory containing the `Birthday.pm` module.

       cd examples/perl-examples

2. Instrument the `Birthday.pm` file.

       dfepl Birthday.pm

   This command creates a directory `daikon-untyped`, and puts the instrumented version of `Birthday.pm` into `daikon-untyped/Birthday.pm`. As the directory name implies, this instrumented version doesn’t contain type information.

3. Run a test suite using the instrumented `Birthday.pm` file.

       dtype-perl test_bday.pl 10

   The `dtype-perl` is a script that runs Perl with the appropriate command line options to find the modules used by the Daikon Perl runtime tracing modules, and to use the instrumented versions of modules in `daikon-untyped` in preference to their original ones. The number 10 is an argument to the `test_bday.pl` script telling it to run a relatively short test.

   This will also generate a file `daikon-instrumented/Birthday.types` recording the type of each variable seen during the execution of the instrumented program.

4. Re-annotate the module using the type information.

       dfepl -T Birthday.pm

   This step repeats step 2, except that the `-T` flag to `dfepl` tells it to use the type information generated in the previous step, and to put the output in the directory `daikon-instrumented`. `dfepl` also converts the type information into a file `daikon-output/Birthday.decls` containing subroutine declarations suitable for Daikon.

5. Run the full test suite with the type-instrumented `Birthday.pm`.

       dtrace-perl test_bday.pl 30

   Here we run another test suite, which happens to be the same `test_bday.pl`, but running for longer. (The example will also work with a smaller number). The script `dtrace-perl` is similar to `dtype-perl` mentioned earlier, but looks for instrumented source files in `daikon-instrumented`.

   This creates `daikon-output/test_bday-combined.dtrace`, a trace file containing the values of variables at each invocation. (The file name is formed from the name of the test program, with `-combined` appended because it contains the trace information from all the instrumented modules invoked from the program).

6. Change to the `daikon-output` directory to analyze the output.

       cd daikon-output

7. Run Daikon on the trace file

       java -cp ${DAIKONDIR}/daikon.jar daikon.Daikon Birthday.decls test_bday-combined.dtrace

8. Examine the invariants. They are printed to standard output, and they are also saved to file `Birthday.inv.gz`, which you can manipulate with the `PrintInvariants` program and other Daikon tools. For example:

       java -cp ${DAIKONDIR}/daikon.jar daikon.PrintInvariants Birthday.inv.gz

   Invariants produced from Perl programs can be examined using the same tools as other Daikon invariants.

In the example above, the script `test_bday.pl` was not itself instrumented; it was only used to test the instrumented code. The Perl front end can also be used to instrument stand-alone Perl programs. The following sequence of commands, similar to those above, show how Daikon can be used with the stand-alone program `standalone.pl`, also in the `examples/perl-examples` directory.

    dfepl standalone.pl
    dtype-perl daikon-untyped/standalone.pl
    dfepl -T standalone.pl
    dtrace-perl daikon-instrumented/standalone.pl
    cd daikon-output
    java -cp ${DAIKONDIR}/daikon.jar daikon.Daikon -o standalone.inv standalone-main.decls \
         standalone-combined.dtrace

Note two differences when running a stand-alone program. First, the instrumented versions of the program, in the `daikon-untyped` or `daikon-instrumented` directory, are run directly. Second, the declarations file is named after the package in which the subroutines were declared, but since every stand-alone program uses the `main` package, the name of the program is prepended to the `.decls` file name to avoid collisions.

Next: Detecting invariants in Simulink/Stateflow programs, Previous: Detecting invariants in Perl programs, Up: Example usage [Contents][Index]

### 3.5 Detecting invariants in Eiffel programs

CITADEL is an Eiffel front-end to the Daikon invariant detector. You can obtain Citadel from https://se.inf.ethz.ch/people/polikarpova/citadel/.

Previous: Detecting invariants in Eiffel programs, Up: Example usage [Contents][Index]

### 3.6 Detecting invariants in Simulink/Stateflow programs

Hynger (HYbrid iNvariant GEneratoR) instruments Simulink/Stateflow (SLSF) block diagrams to generate Daikon input (`.dtrace` files). Hynger was created by Taylor Johnson, Stanley Bak, and Steven Drager. You can obtain Hynger from https://github.com/verivital/hynger.

Previous: Detecting invariants in Eiffel programs, Up: Example usage [Contents][Index]