Next: Troubleshooting, Previous: Front ends and instrumentation, Up: Top [Contents][Index]
This chapter describes various tools that are included with the Daikon distribution.
| • Tools for manipulating invariants | ||
| • DtraceDiff utility | ||
| • Reading dtrace files |
Next: DtraceDiff utility, Up: Tools [Contents][Index]
This section gives information about tools that manipulate invariants (in the form of .inv files).
| • Printing invariants | ||
| • MergeInvariants | ||
| • Invariant Diff | ||
| • Annotate | ||
| • AnnotateNullable | ||
| • Runtime-check instrumenter | ||
| • InvariantChecker | ||
| • LogicalCompare |
Next: MergeInvariants, Up: Tools for manipulating invariants [Contents][Index]
Daikon provides many options for controlling how invariants are printed.
Often, you may want to print the same set of invariants several
different ways. However, you only want to run Daikon once, since it may
be very time consuming. The PrintInvariants utility prints a set of
invariants from a .inv file.
PrintInvariants is invoked as follows:
java -cp $DAIKONDIR/daikon.jar daikon.PrintInvariants [flags] inv-file
PrintInvariants shares many flags with Daikon.
These flags are only briefly summarized here.
For more information about these flags, see Configuration options.
In particular, see the configuration options whose names start with
daikon.PrintInvariants; see General configuration options.
Print usage message.
Produce output in the given format. See Invariant syntax.
Send output to the specified file rather than stdout.
Output numbers of values and samples for invariants and program points; for debugging.
Only outputs program points that match the specified regular expression
Load the configuration settings specified in the given file. See Configuration options, for details.
Specify a single configuration setting. See Configuration options, for details.
Enable debug loggers.
Track information on specified invariant class, variables and program point. For more information, see Track logging in Daikon Developer Manual.
Print extra info about invariants, and wrap in XML tags.
This is primarily for programmatic use and for debugging.
To add just the Java class of each invariant, use
--config_option daikon.PrintInvariants.print_inv_class=true.
Next: Invariant Diff, Previous: Printing invariants, Up: Tools for manipulating invariants [Contents][Index]
The MergeInvariants utility merges multiple serialized invariant files
to create a single serialized invariant file that contains the
invariants that are true across each of the input files. The results
of merging N serialized invariant files should be the same as running
Daikon on the N original .dtrace files.
MergeInvariants is invoked as follows:
java -cp $DAIKONDIR/daikon.jar daikon.MergeInvariants [flags]... file1 file2...
file1 and file2 are files containing serialized invariants produced by running Daikon. At least two invariant files must be specified.
MergeInvariants shares many flags with Daikon.
These flags are only briefly summarized here.
For more information about these flags, see Daikon configuration options.
Print usage message.
Output serialized invariants to the specified file; they can later be postprocessed, compared, etc. If not specified, the results are written to standard out.
Specify a single configuration setting. See Configuration options, for details.
Enable debug loggers.
Track information on specified invariant class, variables and program point. For more information, see Track logging in Daikon Developer Manual.
Next: Annotate, Previous: MergeInvariants, Up: Tools for manipulating invariants [Contents][Index]
The invariant diff utility is designed to output the differences between two sets of invariants. Invariant diff compares invariants at program points with the same name.
Invariant diff lets you compare the invariants generated by two versions of the same program, or compare the invariants generated by different runs of one program.
Invariant diff is invoked as follows:
java -cp $DAIKONDIR/daikon.jar daikon.diff.Diff [flags]... file1 [file2]
file1 and file2 are files containing serialized invariants produced by running Daikon or Diff with the -o flag. If file2 is not specified, file1 is compared with the empty set of invariants.
This section describes the optional flags.
Print usage message.
Display the tree of differing invariants (default). Invariants that are the same in file1 and file2 are not printed. At least one of the invariants must be justified. Does not print “uninteresting” invariants (currently some ‘OneOf’ and ‘Bound’ invariants).
Display the tree of all invariants. Includes invariants that are the same in file1 and file2, and unjustified invariants.
Include “uninteresting” invariants in the tree of differing invariants.
Include (statistically) unjustified invariants.
Compute (file1 - file2). This is all the invariants that appear in
file1 but not file2. Unjustified invariants are treated as if they
don’t exist. Output is written as a serialized ‘InvMap’ to the file
specified with the -o option. To view the contents of the serialized
‘InvMap’, run java daikon.diff.Diff file.
Compute (file1 XOR file2).
This is all the invariants that appear in
one file but not the other. Unjustified invariants are treated as if
they don’t exist. Output is written as a serialized ‘InvMap’ to the file
specified with the -o option. To view the contents of the serialized
‘InvMap’, run java daikon.diff.Diff file.
Compute (file1 UNION file2).
This is all the invariants that appear in
either file. If the same invariant appears in both files, the one with
the better justification is chosen. Output is written as a serialized
‘InvMap’ to the file specified with the -o option. To view the contents
of the serialized ‘InvMap’, run java daikon.diff.Diff file.
Used in combination with the -m or -x option. Writes the output as a serialized ‘InvMap’ to the specified file.
Examine all program points. By default, only procedure entries and combined procedure exits are examined. This option also causes conditional program points to be examined.
Print empty program points. By default, program points are not printed if they contain no differences.
Use the specified class as a custom comparator. A custom comparator can be used for any of 3 operations: sorting the first set of invariants, sorting the second set of invariants, and combining the two sets into the pair tree. The specified class must implement the Comparator interface, and accept objects of type Invariant.
Verbose output. Invariants are printed using the repr() method, instead
of the format() method.
For internal use only. Display the statistics between two sets of invariants. The pairs of invariants are placed in bins according to the type of the invariant and the type of the difference.
For internal use only. Display the same statistics as -s, but as a tab-separated list.
For internal use only. Treat justification as a continuous value when gathering statistics. By default, justification is treated as a binary value — an invariant is either justified or it is not. For example, assume invariant ‘I1’ has a probability of .01, and ‘I2’ has a probability of .5. By default, this will be a difference of 1, since ‘I1’ is justified but ‘I2’ is not. With this option, this will be a difference of .49, the difference in the probabilities. This only applies when one invariant is justified, and the other is unjustified.
For debugging use only. Prints logging information describing the state of the program as it runs.
Next: AnnotateNullable, Previous: Invariant Diff, Up: Tools for manipulating invariants [Contents][Index]
The Annotate program inserts Daikon-generated invariants into Java source code as annotations in DBC, ESC, Java or JML format. These annotations are comments that can be automatically verified or otherwise manipulated by other tools. The Daikon website has an example of code after invariant insertion: http://plse.cs.washington.edu/daikon/StackAr.html.
Invoke Annotate like this:
java -cp $DAIKONDIR/daikon.jar daikon.tools.jtb.Annotate Myprog.inv Myprog.java Myprog2.java ...
The first argument is a Daikon .inv or .inv.gz file produced by running Daikon with the -o command-line argument. All subsequent arguments are .java files. The original .java files are left unmodified, but Annotate produces new versions of the .java files (with names suffixed as -escannotated, -jmlannotated, or -dbcannotated) that include the Daikon invariants as comments.
The options are:
Produce output in the given format. See Invariant syntax.
Do not use reflection to find information about the classes being instrumented. This allows Annotate to run without having access to the class files. Since the class files are necessary to generate ‘also’ tags, those tags will be left out when this option is chosen.
Output at most count invariants per program point (which ones are chosen is not specified).
Each invariant is printed using the given format (ESC, JML or DBC), but the invariant expression is wrapped inside XML tags, along with other information about the invariant.
For example, if this switch is set, the output format is ESC,
and an invariant for method foo(int x) normally prints as
/* requires x != 0; */
Then the resulting output will look something like this (all in one line; we break it up here for clarity):
/* requires <INVINFO> <INV> x != 0 </INV> <SAMPLES> 100 </SAMPLES> <DAIKON> x != 0 </DAIKON> <DAIKONCLASS> daikon.inv.unary.scalar.NonZero </DAIKONCLASS> <METHOD> foo() </METHOD> </INVINFO> ; */
Note that the comment will no longer be a legal ESC/JML/DBC comment. To make it legal again, you must replace the XML tags with the string between the ‘<INV>’ tag.
Also note the extra information printed with the invariant: the number
of samples from which the invariant was inferred, the Daikon
representation (i.e., the Daikon output format), the Java class that
the invariant corresponds to, and the method that the invariant
belongs to (null for object invariants).
If Annotate issues a warning message of the form
Warning: Annotate: Daikon knows nothing about field ...
then the Annotate tool found a variable in the source code that was computed by Daikon. This can happen if Daikon was run omitting the variable, for instance due to --std-visibility. It can also happen due to a bug in Annotate or Daikon; if that is the case, please report it to the Daikon developers.
Next: Runtime-check instrumenter, Previous: Annotate, Up: Tools for manipulating invariants [Contents][Index]
By using the AnnotateNullable program, you can insert
@Nullable annotations into your source code.
The purpose of AnnotateNullable is to make it easier to annotate
programs for the
Nullness Checker
that is part of the
Checker Framework.
As background, the Nullness Checker
warns the programmer about possible null dereference errors.
This is useful, but it requires the programmer to write a @Nullable
annotation anywhere that a variable might contain null.
(An unannotated reference is assumed to never be
null at run time.)
The AnnotateNullable tool automatically and soundly determines a subset of the
proper @Nullable annotations, reducing the programmer’s burden.
Each annotation that AnnotateNullable infers is
correct. The programmer may need to write some additional
@Nullable annotations, but that is much easier than writing them all.
To insert @Nullable annotations in your program,
follow these steps:
@Nullable annotations AnnotateNullable will produce.
java -cp $DAIKONDIR/daikon.jar daikon.Chicory \
--dtrace-file=an.dtrace.gz mypackage.MyClass arg1 arg2 ...
java -cp $DAIKONDIR/daikon.jar daikon.Daikon an.dtrace.gz --no_text_output \
--config daikondir/java/daikon/annotate_nullable.config
AnnotateNullable tool to create an annotation index file.
AnnotateNullable writes its output to standard out, so you should
redirect its output to a .jaif file.
java -cp $DAIKONDIR/daikon.jar daikon.AnnotateNullable an.inv.gz > nullable-annotations.jaif
# To insert in class files:
insert-annotations mypackage.MyClass nullable-annotations.jaif
# To insert in source files:
insert-annotations-to-source nullable-annotations.jaif \
mypackage/MyClass.java annotated/mypackage/MyClass.java
AnnotateNullable is invoked as follows:
java -cp $DAIKONDIR/daikon.jar daikon.AnnotateNullable [flags] inv-file
The flags are:
Adds ‘NonNull’ annotations as well as ‘Nullable’ annotations. Unlike ‘Nullable’ annotations, ‘NonNull’ annotations are not guaranteed to be correct.
Next: InvariantChecker, Previous: AnnotateNullable, Up: Tools for manipulating invariants [Contents][Index]
The runtimechecker instrumenter inserts, into a Java file, instrumentation code that checks invariants as the program executes. For a full list of options, run:
java -cp $DAIKONDIR/daikon.jar daikon.tools.runtimechecker.Main help
The instrument command to runtimechecker creates a new directory
instrumented-classes containing a new version of the
user-specified Java files, instrumented to check invariants at run time
and to record a list of invariant violations in a Java data structure.
You can compile and run the instrumented version of your program.
Here is an example of using the runtime-check instrumenter to create a version of file ubs/BoundedStack.java that checks the invariants in invariant file BoundedStack.inv.gz:
java daikon.tools.runtimechecker.Main instrument BoundedStack.inv.gz \
ubs/BoundedStack.java
The instrumented Java code references classes in the
daikon.tools.runtimechecker package, so those classes must be
present in the classpath when the instrumented classes are compiled and
executed.
Invariants are evaluated at the program points at which they should hold. Three things can happen when evaluating an invariant:
daikon.tools.runtimechecker.Property is added to a list in the
class daikon.tools.runtimechecker.Runtime. A programmer can
obtain the growing list of violated invariants through the method
daikon.tools.runtimechecker.Runtime.getViolations(). (See
that class for other useful methods.)
Throwable (exception) is thrown when evaluating the
invariant. In this case, the throwable is added to the list
daikon.tools.runtimechecker.Runtime.internalInvariantEvaluationErrors.
The throwable is not rethrown.
Note that the instrumented program does not do anything with the list of violations; it merely creates the list. You will need to write your own code to process that list; see How to access violations.
| • How to access violations | ||
| • Problems compiling instrumented code |
The instrumented class handles violations silently:
it simply adds them to a list in the class
daikon.tools.runtimechecker.Runtime.
No “invariant violation” exceptions are thrown, and the violated
invariants can only be obtained dynamically (while the program is running)
by calling daikon.tools.runtimechecker.Runtime.getViolations().
To obtain a file of all the violations for a program execution, you can use
program daikon.tools.runtimechecker.WriteViolationFile.
For example, if you usually run
java MyProg arg1 arg2
then instead you would run
java -cp myclasspath:$DAIKONDIR/daikon.jar daikon.tools.runtimechecker.WriteViolationFile MyProg arg1 arg2
This will create a file called violations.txt in the
current directory, immediately before the program exits normally.
If the program under test calls System.exit, then no
violations.txt file is created. (JUnit is an example of a program
that calls System.exit.)
The following code snippet contains a method callMethod() which
presumably calls one of the methods in the instrumented class.
The code detects if any violations occurred, and if so, prints
a message.
daikon.tools.runtimechecker.Runtime.resetViolations();
daikon.tools.runtimechecker.Runtime.resetErrors();
callMethod();
List<Violation> vs = daikon.tools.runtimechecker.Runtime.getViolations();
if (!vs.isEmpty())
System.out.println("Violations occurred.");
In addition, the instrumenter adds the following two methods to the instrumented class:
isDaikonInstrumented(). Returns true (you could calling
this method to see if the class has been instrumented).
getDaikonInvariants(). Returns the array of properties being checked.
Previous: How to access violations, Up: Runtime-check instrumenter [Contents][Index]
When compiling the instrumented code, the Java compiler might emit an error such as:
error: longitude has private access in GeoPoint
If you receive the error above, then a variable in an invariant
(longitude in this case) has been declared private.
There are two ways to fix this. To check invariants that mention private variables, supply the --make_all_fields_public command-line option when running ‘java daikon.tools.runtimechecker.Main instrument ...’. To ignore invariants that mention private variables, rebuild the .dtrace file by rerunning Chicory using the --std-visibility command-line option.
Another error the Java compiler might emit is:
error: code too large for try statement
You get the above error if the combined size of the original source code, plus the instrumentation code, is larger than the JVM’s limit of 65536 bytes of bytecode per method.
You can correct the problem by using a smaller number of invariants when instrumenting. See Too much output.
(Eventually, it might be nice for the instrumenter to place its code in one or more separate methods so that no one of them is too large.)
Next: LogicalCompare, Previous: Runtime-check instrumenter, Up: Tools for manipulating invariants [Contents][Index]
The InvariantChecker program takes a set of invariants found by Daikon
and a set of data trace files. It checks each sample in the data trace
files against each of the invariants. Any sample that violates an invariant
is noted, via a message printed to standard output or to a specified
output file.
InvariantChecker is invoked as follows:
java -cp $DAIKONDIR/daikon.jar daikon.tools.InvariantChecker [options] invariant-file dtrace-files
The invariant-files are invariant files (.inv) created by running Daikon. The dtrace-files are data trace (.dtrace) files created by running the instrumented program. The files may appear in any order; the file type is determined by whether the file name contains .dtrace, or .inv.
The options are:
Print usage message.
Write any violations to the specified file.
Checks only invariants that are above the default confidence level.
Checks only invariants that are not filtered by the default filters.
Print all samples that violate an invariant. By default only the totals are printed.
Processes all invariant files in the given directory and reports the number of invariants that failed on any of the .dtrace files in that directory. We only process invariants above the default confidence level and invariants that have not been filtered out by the default filters.
These switches are the same as for Daikon. They are described in Running Daikon.
Previous: InvariantChecker, Up: Tools for manipulating invariants [Contents][Index]
Suppose you have two sets of invariants describing the operation of a software
module or describing two implementations of a module with the same
interface. Roughly, one set of invariants is “stronger” than
another if in any situation where the “stronger” invariants
hold, the “weaker” invariants also hold. The LogicalCompare tool
checks whether two sets of invariants satisfy this relationship.
In order to use LogicalCompare, Simplify must be installed
(see Installing Simplify).
An invocation of LogicalCompare has the following form:
java -cp $DAIKONDIR/daikon.jar daikon.tools.compare.LogicalCompare [options] \
weak-invs strong-invs [enter-ppt [exit-ppt]]
The LogicalCompare program takes two mandatory arguments, which are
.inv files containing invariants. LogicalCompare
checks whether the invariants in the first file are weaker
(implied by) the invariants in the second file.
LogicalCompare prints any exceptions to this implication,
preceded by the text “Invalid:”.
To be precise, for each
pair of program points representing a single method or function,
LogicalCompare will check that each precondition (:::ENTER point
invariant) in the “stronger” invariant set is implied by some
combination of invariants in the “weaker” invariant set, and that
each postcondition (:::EXIT point invariant) in the “weaker” invariant
set is implied by some combination of postconditions in the
“stronger” set and preconditions in the “weaker” set.
If no other regular arguments besides the two .inv files are supplied,
all the method or function program points that exist in both files
will be compared, with a exception message reported for each method
that exists in the “weaker” set but not the “stronger”.
Alternatively, one or two additional arguments may be supplied, which name an
:::ENTER program point and an :::EXIT program point to examine
(if only an :::ENTER program point is supplied,
the corresponding combined :::EXIT point
is selected automatically).
LogicalCompare accepts the following options:
Read additional assumptions about the behavior of compared routines
from the file file. The assumptions file should consist of lines
starting with ‘PPT_NAME’, followed by the complete name of an
:::ENTER program point, followed by lines each consisting of a Simplify
formula, optionally followed by a # and a human-readable
annotation. Blank lines and lines beginning with a # are
ignored. The assumption properties will be used as if they were
invariants true at the strong :::EXIT point when checking
weak :::EXIT point invariants.
Specify a single configuration setting. The available settings are the same as can be passed to Daikon’s --config_option option, though because the invariants have already been generated, some will have no effect. For a list of available options, see Configuration options.
Read configuration options from the file file. This file should have the same format as one passed to Daikon’s --config option, though because the invariants have already been generated, some will have no effect.
These options have the same effect as the --debug and --dbg options to Daikon, causing debugging logs to be printed.
Control which invariants are removed from consideration before
implications are checked. Note that except as controlled by this
option, LogicalCompare does not perform any of the filters that
normally control whether invariants are printed by Daikon. Also,
invariants that cannot be formatted for the Simplify automatic theorem
prover will be discarded in any case, as there would be no other way
to process them. Each letter controls a filter: an invariant is rejected
if it is rejected by any filter (or, equivalently, kept only if it
passes through every filter).
Discard upper-bound and lower-bound invariants (such as ‘x <= c’ and ‘x >= c’ for a constant c), when Daikon considers the constant to be uninteresting. Currently, Daikon has a configurable range of interesting constant: by default, -1, 0, 1, and 2 are interesting, and no other numbers are.
Discard all bound invariants, whether or not the constants in them are considered interesting.
Discard ‘one-of’ invariants (which signify that a variable always had one of a small set of values at run time), when the values that the variable took are considered uninteresting by Daikon.
Discard all ‘one-of’ invariants, whether or not the values involved are interesting.
Discard invariants for which it was never the case that all the variables involved in the invariant were present at the same time.
Discard invariants that Daikon determines to be statistically unjustified, according to its tests.
Discard invariants that refer to the values of pass-by-value parameters in the postcondition, or to the values of objects pointed to by parameters in postconditions, when the pointer is not necessarily the same as at the entrance to the method or function. Usually such invariants reflect implementation details that would not be visible to the caller of a method.
Discard implication invariants when they appear in :::ENTER program
points.
The default set of filters corresponds to the letters ijmp.
Print a brief summary of available command-line options.
If implication is not verified between two invariant sets after examining the preconditions, do not continue to check the implication involving postconditions. Because the postconditions aren’t formally meaningful outside the domain specified by the preconditions, this is the safest behavior, but in practice trivial precondition mismatches may prevent an otherwise meaningful postcondition comparison. See also --post-after-pre-failure.
For each implication among invariants that is verified, print a minimal set of conditions that establish the truth of the conclusion. The set is minimal, in the sense that if any condition were removed, the conclusion would no longer logically follow according to Simplify, but it is not the least such set: there may exist a smaller set of conditions that establish the conclusion, if that set is not a subset of the set printed. Beware that because this option uses a naive search technique, it may significantly slow down output.
Even if implication is not verified between two invariant sets after examining the preconditions, continue to check the implication involving postconditions. This is somewhat dangerous, in that if the implication does not hold between the preconditions, the invariant sets may be inconsistent, in which case reasoning about the postconditions is formally nonsensical, but the tool will attempt to ignore the contradiction and carry on in this case. This is now the default behavior, so the option has no effect, but it is retained for backward compatibility. See also --no-post-after-pre-failure.
Print a count of the number of invariants checked for implication.
For each invariant, show how it is represented as a logical formula passed to Simplify.
Rather than testing implications among invariants, simply print the
sets of weak and strong :::ENTER and :::EXIT point invariants that would
normally be compared. The invariants are selected and filtered as
implied by other options.
Print invariants that are verified to be implied (“valid”), as well as those for which the implication could not be verified (“invalid” invariants, which are always printed).
For each set of invariants checked, print the total time required for
the check. This time includes both processing done by LogicalCompare
directly, and time spent waiting for processing done by Simplify, but
does not include time spent deserializing the .inv input
files.
Next: Reading dtrace files, Previous: Tools for manipulating invariants, Up: Tools [Contents][Index]
DtraceDiff is a utility for comparing data trace (.dtrace) files.
It checks that the same program points are visited in the same order in
both files, and that the number, names, types, and values of variables
at each program point are the same. The differences are found using a
content-based, rather than text-based, comparison of the two files.
DtraceDiff stops by signaling an error when it finds a difference
between the two data trace files. (Once execution paths have
diverged, continuing to emit record-by-record differences is likely to
produce output that is far too voluminous to be useful.) It also
signals an error when it detects incompatible program point
declarations or when one file is shorter than the other.
DtraceDiff is invoked as follows:
java -cp $DAIKONDIR/daikon.jar daikon.tools.DtraceDiff [flags] \ [declsfiles1] dtracefile1 [declsfiles2] dtracefile2
Corresponding declarations (.decls) files can optionally be
specified on the command line before each of the two .dtrace
files. Multiple .decls files can be specified. If no
.decls file is specified, DtraceDiff assumes that the
declarations are included in the .dtrace file instead.
DtraceDiff supports the following Daikon command-line flags:
Print usage message.
Load the configuration settings specified in the given file. See Configuration options, for details.
Specify a single configuration setting. See Configuration options, for details.
Only process program points whose names match the regular expression.
Do not process program points whose names match the regular expression. This takes priority over the --ppt-select-pattern argument.
Only process variables (whether in the trace file or derived) whose names match the regular expression.
Ignore variables (whether in the trace file or derived) whose names match the regular expression, which uses Perl syntax. This takes priority over the --var-select-pattern argument.
DtraceDiff uses appropriate comparisons for the type of the variables in
each program point being compared. In particular:
Previous: DtraceDiff utility, Up: Tools [Contents][Index]
If you wish to write a program that manipulates .dtrace files, then see See Reading dtrace files in Daikon Developer Manual.
Previous: DtraceDiff utility, Up: Tools [Contents][Index]