Next: Editing, Previous: Daikon internals, Up: Top [Contents][Index]
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.
| • Unit testing | ||
| • Regression tests |
Next: Regression tests, Up: Testing [Contents][Index]
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.
| • Invariant format testing | ||
| • Sample Testing |
Next: Sample Testing, Up: Unit testing [Contents][Index]
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 argsThese 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]
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:
This command specifies the declaration file to use. This is a normal .decls file that should follow the format defined in the user manual.
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.
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.
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.
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)).
| • Assertions | ||
| • Example file |
Next: Example file, Up: Sample Testing [Contents][Index]
Assertions are formatted like function calls: <name>(arg1, arg2, ...).
The valid assertions for the assert: command are:
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]
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]
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.
| • Kvasir regression tests | ||
| • Adding regression tests |
Next: Adding regression tests, Up: Regression tests [Contents][Index]
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]
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.
The Makefile must contain at least the following entries.
Dot separated fully qualified name of the class that contains the main entry point for the test. For example,
MAIN_CLASS := DataStructures.StackArTester.
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.
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.
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.
For more information, see the comments in file $DAIKONDIR/tests/Makefile.common.
Previous: Kvasir regression tests, Up: Regression tests [Contents][Index]