[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
This chapter describes various tools that are included with the Daikon distribution.
8.1 Tools for manipulating invariants | ||
8.2 DtraceDiff utility |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
This section gives information about tools that manipulate invariants (in the form of ‘.inv’ files).
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [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 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 Daikon configuration options.
Print usage message.
Produce output in the given format. See Invariant syntax.
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 section Configuration options, for details.
Specify a single configuration setting. See section Configuration options, for details.
Enable debug loggers.
Track information on specified invariant class, variables and program point. For more information, also see (./developer)Track logging section `Track logging' in Daikon Developer Manual.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [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 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 section Configuration options, for details.
Enable debug loggers.
Track information on specified invariant class, variables and program point. For more information, also see (./developer)Track logging section `Track logging' in Daikon Developer Manual.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
The invariant diff utility is designed to output the differences between two sets of invariants. This is useful, for example, if you want to compare the invariants generated by two versions of the same program.
Invariant diff is invoked as follows:
java 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).
Include “uninteresting” invariants in the tree of differing invariants.
Include (statistically) unjustified invariants.
Display the tree of all invariants. Includes invariants that are the same in file1 and file2, and unjustified invariants.
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.
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.
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.
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.
Verbose output. Invariants are printed using the repr()
method, instead
of the format()
method.
For debugging use only. Prints logging information describing the state of the program as it runs.
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.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [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://pag.csail.mit.edu/daikon/StackAr.html.
Invoke Annotate like this:
java 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 Annnotate 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 is 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.
Known bug (logical shift in Java). Daikon's Java parser (adopted from javacc and JTB) accepts Java 1.5 syntax. An error in the new parser may produce illegal Java in the annotated file, if the source file to be annotated includes logical shift operators. See section Known bugs.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
AnnotateNullable determines which variables in a Java program were ever null during execution. Its primary use is for performing inference for a type system that detects null dereference errors. An example is the Nullness checker that is part of the Checker Framework.
The Nullness checker requires a programmer to annotate some references
with @Nullable
, meaning the variable might be null; references
that are left unannotated are never null at run time. (Alternately, the
checker can use @NonNull
for references that are never
null, and leave unannotated for references that might be null. The
Nullness checker supports either choice of default.) The checker
then warns the programmer about possible null dereference errors.
The Nullness checker is useful, but writing all the annotations is tedious.
The AnnotateNullable tool automatically and soundly determines a subset of the
proper @Nullable
annotations. Each annotation that it 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 are ever produced,
but more thorough runs produce a larger number of @Nullable
annotations.
java daikon.Chicory --dtrace-file=an.dtrace.gz your-command-and-options |
java daikon.Daikon an.dtrace.gz --no_text_output \ --config daikondir/java/daikon/annotate_nullable.config |
The example uses the ‘annotate_nullable.config’ configuration file that is included in the Daikon distribution. You may use any configuration file, or none, as long as the NonZero invariant is enabled. The ‘annotate_nullable.config’ enables only the NonZero invariant. This makes Daikon run much faster, but the resulting ‘.inv’ file is useful only for the AnnotateNullable tool.
java daikon.AnnotateNullable an.inv.gz > nullable-annotations.jaif |
insert-annotations mypackage.MyClass nullable-annotations.jaif insert-annotations-to-source nullable-annotations.jaif \ mypackage/MyClass.java annotated/mypackage/MyClass.java |
AnnotateNullable is invoked as follows:
java 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.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [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 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 runtime
and to record a list of invariant violations in a Java data structure.
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 Accessing violations.
Here is an example of use of the runtime-check instrumenter. To create a version of file ‘ubs/BoundedStack.java’ that checks the invariants in invariant file ‘BoundedStack.inv.gz’, do:
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.
8.1.6.1 Accessing violations |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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 from class
daikon.tools.runtimechecker.Runtime
.
A future release of Daikon will provide tools that process the list in the following ways:
daikon.tools.runtimechecker.WriteViolationFile
. If you
would ordinarily run your program as ‘java MyProg arg1 arg2’,
then running ‘java daikon.tools.runtimechecker.WriteViolationFile
MyProg arg1 arg2’ creates a file called ‘violations.txt’ in the
current directory. If the program under test calls
System.exit
, then no ‘violations.txt’ file is created.
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.
Known bug (logical shift in Java). Daikon's Java parser (adopted from javacc and JTB) accepts Java 1.5 syntax. An error in the new parser may produce illegal Java in the instrumented file, if the source file to be instrumented includes logical shift operators. See section Known bugs.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [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 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.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
Given two sets of invariants describing the operation of a software module, or describing two implementations of a module with the same interface, we can define one set of invariants to be “stronger” than another roughly if in any situation where the “stronger” invariants hold, the “weaker” invariants also hold. The LogicalCompare tool examines two sets of invariants, and checks using the Simplify automatic theorem prover whether they satisfy a precise version of this relationship.
Simplify must be separately obtained (from http://www.hpl.hp.com/downloads/crl/jtk/) and installed in order to use this program.
The LogicalCompare program takes two mandatory arguments, which are
‘.inv’ files containing invariants; the invariants will be
checked to verify if the invariants in the first file are weaker
(implied by) the invariants in the second file, and exceptions to this
implication are printed. If no other regular arguments 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). 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. In summary,
the syntax of an invocation of LogicalCompare will have the following
form:
java daikon.tools.compare.LogicalCompare [options] \ weak-invs strong-invs [enter-ppt [exit-ppt]] |
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 runtime), 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 de-serializing the ‘.inv’ input files.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [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 signalling 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 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 section Configuration options, for details.
Specify a single configuration setting. See section 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:
[ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
This document was generated by Daikon User on June, 23 2010 using texi2html 1.78.