Next: Editing, Previous: Daikon internals, Up: Top [Contents][Index]

## 5 Testing

Daikon has two sets of tests: unit tests (see Unit testing) and regression tests (see Regression tests). If there are any differences between the expected results and the ones you get, don’t check in your changes until you understand which is the desired behavior and possibly update the goals.

The Daikon distribution contains unit tests, but not regression tests (which would make the distribution much larger). The regression tests appear in Daikon’s version control repository (see Source code (version control repository)), within the `tests` subdirectory.

Next: Regression tests, Up: Testing [Contents][Index]

### 5.1 Unit testing

The unit tests are found in `daikon/java/daikon/test/`; they use the ‘`JUnit`’ unit testing framework. They take a few seconds to run. They are automatically run each time you compile Daikon (by running `make` in `${DAIKONDIR}/java` or any of its subdirectories). You can also run them explicitly via `make unit`. When you write new code or modify old code, please try to add unit tests.

Next: Sample Testing, Up: Unit testing [Contents][Index]

#### 5.1.1 Invariant format testing

This tests the formatting of invariants with specified input. The tests are configured in the file `InvariantFormatTest.commands` under `daikon/test/`. The `InvariantFormatTest.commands` file must be in the classpath when this tester is run.

The file is formatted as follows:

    <fully qualified class name> [<instantiate args>]
    <type string>
    <goal string>+ <- 1 or more goal strings
    <sample>* <- 0 or more samples

The file format should be the same regardless of blank or commented lines except in the samples area. No blank lines or comments should appear after the goal string before the first sample or between parts of samples (these lines are used to determine where sample lists end). This will be remedied in a future version of the tester.

`Instantiate args`

  These are optional additional arguments to the static instantiate method of the class. Each argument consists of the type (boolean or int) followed by the value. For example:

      boolean true
      int 37 boolean false

`Type string:`

  A type string must consist of one or more of the following literals: ‘`int`’, ‘`double`’, ‘`string`’, ‘`int_array`’, ‘`double_array`’, or ‘`string_array`’, separated by spaces. This string represents the types that an invariant is supposed to compare For instance, a binary integer comparison would have type string ‘`int int`’. A pairwise sequence comparison would have type string ‘`int_array int_array`’.

`Goal string:`

  The goal string must start with the prefix ‘`Goal` ’, and then continue with ‘`(<format type>):` ’, where format type is the format in which the invariant will print. After this the representation of the invariant must occur. It must represent the invariant result exactly as printed, even white space is significant (as proper formatting should be correct down to the whitespace). The first variable (the one corresponding to the first type in the type string) corresponds with ‘`a`’, the second with ‘`b`’ and so on. Format the type string accordingly. (In samples, the value of ‘`a`’ is read first, possibly followed by ‘`b`’, and then possibly ‘`c`’, depending on the arity of the invariant.)

      Example:
      Type string, Goals
       |             |
      \|/            |
      int           \|/
      Goal (daikon): a >= -6
      Goal (java): a >= -6
      Goal (esc): a >= -6
      Goal (ioa): a >= -6
      Goal (jml): a >= -6
      Goal (simplify): (>= |a| -6)

  Note that the spacing on the goal lines is exact, that is, no extra spaces are allowed and no spaces are allowed to be missing. So the exact format is again:

      Goal<1 space>(<format name>):<1 space><goal text>

`Samples:`

  Values formatted according to the type string, one value per line Make sure that the samples provided are actually instances of that particular invariant (That is, if the desired invariant is ‘`a < b`’, then the first number of each sample better be less than the second)

  Arrays and strings must be formatted according to the Daikon `.dtrace` file convention (for a full description, see File formats). This states that arrays must be surrounded in brackets (start with ‘`[`’, end with ‘`]`’), and entries must be separated by a space. Strings must be enclosed in quotes (‘`"`’). Quotes within a string can be represented by the sequence ‘`\"`’.

  For example:

      [1 2 3 4 5] - an array with the elements 1, 2, 3, 4, 5
      "aString" - a string
      "a string" - also legal as a string
      "\"" - the string with the value "
      ["a" "b" "c"] - an array of strings

      int int        <- type string
      Goal: a < b    <- goal string, no comment/blank lines after this
      1              <- or before this
      2
      2              <-|__ Pair of values (a = 2 , b = 3)
      3              <-|

  Other examples are in the existing test file (`InvariantFormatTest.commands`).

The output of a test run can be converted into goals by using the `--generate_goals` switch to the tester as follows:

    java daikon.test.InvariantFormatTester --generate_goals

Note that this test is included in the set of tests performed by the master tester, and so it is not necessary to separately run this test except to generate goal files.

Furthermore, this framework cannot parse complex types from files unless they contain a `public Object valueOf(String s)` function. Otherwise the program has no was of knowing how to create such an object from a string. All primitives and the String type are already recognized.

Previous: Invariant format testing, Up: Unit testing [Contents][Index]

#### 5.1.2 Sample Testing

Sample testing tests various components of Daikon as samples are being processed. A file (normally `daikon/test/SampleTester.commands`) specifies a `.decls` file to use, the samples for each ‘`ppt/var`’, and assertions about Daikon’s state (such as whether or not a particular invariant exists).

Each line of the file specifies exactly one command. Blank lines and leading blanks are ignored. Comments begin with the number sign (‘`#`’) and extend to the end of the line. The type of command is specified as the first token on the line followed by a colon. The supported commands are:

SampleTester Command: decl: decl-file

  This command specifies the declaration file to use. This is a normal `.decls` file that should follow the format defined in the user manual.

SampleTester Command: ppt: ppt

  This command specifies the program point that will be used with following vars, data, and assert commands. The program point should be specified exactly as it appears in the `.decls` file.

SampleTester Command: vars: var1 var2...

  Specifies the variables that will be used on following data lines. Each variable must match exactly a variable in the `ppt`. Other variables will be treated as missing.

SampleTester Command: data: val1 val2...

  Specifies the values for each of the previously specified variables. The values must match the type of the variables. A single dash (-) indicates that a variable is missing.

SampleTester Command: assert: assertion

  Specifies an assertion that should be true at this point (see Assertions). The negation of an assertion can be specified by adding an exclamation point before the assertion (for example: `!inv("x > y", x, y`)).

Next: Example file, Up: Sample Testing [Contents][Index]

#### 5.1.2.1 Assertions

Assertions are formatted like function calls: `<name>(arg1, arg2, ...)`. The valid assertions for the assert: command are:

Assertion: inv format var1 ...

  The `inv` assertion asserts that the specified invariant exists in the current `ppt`. The format argument is the result of calling `format()` on the invariant. This is how the invariant is recognized. The remaining arguments are the variables that make up the invariants slice. These must match exactly variables in the `ppt`. The `inv` assertion returns true if and only if the slice exists and an invariant is found within that slice that matches format.

  Optionally, format can be replaced by the fully qualified class name of the invariant. In this case, it is only necessary for the class to match.

More assertions can easily be added to `SampleTester.java` as required.

Previous: Assertions, Up: Sample Testing [Contents][Index]

#### 5.1.2.2 Example file

The following is an simple example of sample testing.

    decl: daikon/test/SampleTesters.decls

    ppt: foo.f():::EXIT35
      vars: x y z
      data: 1 1 0
      data: 2 1 0
      assert: inv("x >= y", x, y)
      assert: inv(daikon.inv.binary.twoScalar.IntGreaterEqual,x,y)
      assert: !inv("x <= y", x, y)

Previous: Unit testing, Up: Testing [Contents][Index]

### 5.2 Regression tests

The regression tests run Daikon on many different inputs and compare Daikon’s output to expected output. They take about an hour to run.

The regression tests appear in the `${DAIKONDIR}/tests/` directory. Type `make` in that directory to see a list of Makefile targets. The most common target is `make diffs`; if any output file has non-zero size, the tests fail. You do not generally need to do `make clean`, which forces re-instrumentation (a possibly slow process) the next time you run the tests.

As when you install or compile Daikon, when you run the tests environment variable `DAIKONDIR` should be set.

You should generally run the regression tests before checking it a change (especially any non-trivial change). If any of the regression test diffs has a non-zero size, then your edits have changed Daikon’s output and you should not check in without carefully determining that the changes are intentional and desirable (in which case you should update the goal output files, so that the diffs are again zero).

There are several subdirectories under `${DAIKONDIR}/tests/`, testing different components of the Daikon distribution (such as Kvasir, see Kvasir in Daikon User Manual). Tests of the invariant detection engine itself appear in `${DAIKONDIR}/tests/daikon-tests/`.

Each Makefile under `${DAIKONDIR}/tests` includes `${DAIKONDIR}/tests/Makefile.common`, which contains the logic for all of the tests. `Makefile.common` is somewhat complicated, if only because it controls so many types of tests.

Next: Adding regression tests, Up: Regression tests [Contents][Index]

#### 5.2.1 Kvasir regression tests

The Kvasir (Daikon C front-end) tests appear in the `${DAIKONDIR}/tests/kvasir-tests` directory. These tests run Daikon to ensure that the Kvasir output is valid Daikon input. To run them, go to `${DAIKONDIR}/tests/kvasir-tests` or of its sub-directories and run `make summary-w-daikon`. If any tests return ‘`FAILED`’, then you should look at the appropriate `.diff` file. If you feel that the failure was actually a result of your Daikon changes and should be in fact correct output, then run `make update-inv-goals` to update the Daikon `invs.goal` file.

Previous: Kvasir regression tests, Up: Regression tests [Contents][Index]

#### 5.2.2 Adding regression tests

Most Daikon regression tests are in subdirectories of `${DAIKONDIR}/tests/daikon-tests/`. (There is also a `${DAIKONDIR}/tests/chicory-tests/` directory, but it is usually better to put tests in `${DAIKONDIR}/tests/daikon-tests/`, even if they are exercising Chicory-specific behavior.)

To create a new test, perform the following steps.

1. Create a new subdirectory of `${DAIKONDIR}/tests/daikon-tests/`.
2. Put the source files for the test under `${DAIKONDIR}/tests/sources/`, not in the test directory itself. Your test may be able to re-use existing Java source code that appears in that directory.
3. It is expedient to copy a Makefile from another subdirectory, such as `${DAIKONDIR}/tests/daikon-tests/StackAr/`, then modify it.

   The `Makefile` must contain at least the following entries.

   ‘`MAIN_CLASS`’

     Dot separated fully qualified name of the class that contains the main entry point for the test. For example,

         MAIN_CLASS := DataStructures.StackArTester.

   ‘`include ../../Makefile.common`’

     This includes the common portion of the test Makefiles that does most of the work. See it for more information on the details of regression testing.

   ‘`instrument-files-revise:`’

     A target that writes the list of files to instrument. For example,

         instrument-files-revise:
             echo "DataStructures/StackAr.java" >| ${INST_LIST_FILE}

   If you run `make` (without a target), you will see a description of all of the Makefile’s functionality. Most of that is inherited from `${DAIKONDIR}/tests/Makefile.common`.

4. The `.goal` files are the expected results of running Daikon and its associated tools.

   For example, the `StackAr` directory contains the following `.goal` files, among others:

       Makefile
       Stackar.spinfo-static.goal
       StackAr.txt-daikon.goal
       StackAr.txt-esc.goal
       StackAr.txt-jml.goal
       StackAr.txt-merge-esc.goal
       StackAr.txt-merge-jml.goal

   If you omit some `.goal` files, then the related tests will not be run. (If you can’t figure out how to ensure the tests are not run, it may be easier to just add the additional `.goal` files.)

   You can start out with the `.goal` files empty. Execute `make diffs`, to produce output; the tests will fail because the output is not identical to the empty `.goal` files. When the test output is satisfactory, execute `make update-goals` to copy the actual results to the `.goal` files. Then, commit the goal files, Makefile, and source files to the repository.

5. Make the new test be run by adding to the appropriate list (usually ‘`everything`’ or ‘`quick`’) in `${DAIKONDIR}/tests/daikon-tests/Makefile`.

For more information, see the comments in file `${DAIKONDIR}/tests/Makefile.common`.

Previous: Kvasir regression tests, Up: Regression tests [Contents][Index]