[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
Detecting invariants involves two steps:
Often, you can run a single command that performs both steps. Among other benefits, this can avoid the need to create the data trace file by sending trace information directly from the instrumented program to Daikon, which is called “online execution” of Daikon.
This section briefly describes how to obtain data traces for Java, C, Perl, and Eiffel programs, and how to run Daikon. For detailed information about these and other front ends that are available for Daikon, Front ends (instrumentation).
3.1 Detecting invariants in Java programs | ||
3.2 Detecting invariants in C/C++ programs | ||
3.3 Detecting invariants in Perl programs | ||
3.4 Detecting invariants in Eiffel programs |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
In order to detect invariants in a Java program, run the program using the Chicory front end (see section Java front end Chicory) to create a data trace file, then run Daikon itself to detect invariants. With the ‘--daikon’ option to Chicory, a single command performs both steps.
For example, if you usually run
java mypackage.MyClass arg1 arg2 arg3 |
then instead you would run
java daikon.Chicory --daikon mypackage.MyClass arg1 arg2 arg3 |
and the Daikon output is written to the terminal.
3.1.1 StackAr example | ||
3.1.2 Using DynComp with Java programs | ||
3.1.3 Understanding the invariants | ||
3.1.4 Understanding DynComp | ||
3.1.5 A second Java example |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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.
cd examples/java-examples/StackAr javac -g DataStructures/*.java |
java daikon.Chicory --daikon 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 second step above into multiple steps. Then, the whole process would be as follows:
cd examples/java-examples/StackAr javac -g DataStructures/*.java |
java daikon.Chicory DataStructures.StackArTester |
java daikon.Daikon StackArTester.dtrace.gz |
Daikon can analyze multiple runs (executions) of the program. You can supply Daikon with multiple trace files:
java daikon.Chicory --dtrace-file=StackArTester1.dtrace.gz DataStructures.StackArTester java daikon.Chicory --dtrace-file=StackArTester2.dtrace.gz DataStructures.StackArTester java daikon.Chicory --dtrace-file=StackArTester3.dtrace.gz DataStructures.StackArTester java daikon.Daikon StackArTester*.dtrace.gz |
(In this example, all the runs are identical, so multiple runs yield the same invariants as one run.)
There are various ways to do this.
java daikon.PrintInvariants StackArTester.inv.gz |
For more options to the PrintInvariants program, see Printing invariants.
cd .. java 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.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
DynComp can help to filter Daikon's output by omitting invariants involving unrelated variables (see DynComp dynamic comparability (abstract type) analysis for Java). To do so, run DynComp on the target program first, then pass the resulting ‘.decls’ file to Chicory. The process would be as follows:
cd examples/java-examples/StackAr javac -g DataStructures/*.java |
java daikon.DynComp DataStructures.StackArTester |
java daikon.Chicory --daikon \ --comparability-file=StackArTester.decls-DynComp \ DataStructures.StackArTester |
You could split the third step into multiple steps, as described in StackAr example, to gain more control over the invariant detection process.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
This section examines some of the invariants for the StackAr example. For more help interpreting invariants, see Interpreting Daikon 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 first section of Daikon output.
====================================================================== StackAr:::OBJECT this.theArray != null this.theArray.getClass() == java.lang.Object[].class this.topOfStack >= -1 this.theArray[this.topOfStack+1..] elements == null this.theArray[0..this.topOfStack] elements != null this.topOfStack <= size(this.theArray[])-1 ====================================================================== |
These six annotations describe the representation invariant. The
array is never null, and its runtime type is Object[]
. The
topOfStack
index is at least -1 and is less than the length
of the array. Finally, the elements of the array are non-null if
their index is no more than topOfStack
and are null
otherwise.
Next, look at the invariants for the top()
method.
top()
has two different exit points, at lines 78 and 79
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 79.
====================================================================== StackAr.top():::EXIT79 return == this.theArray[this.topOfStack] this.theArray == orig(this.theArray) this.theArray[] == orig(this.theArray[]) this.topOfStack == orig(this.topOfStack) return != null this.topOfStack >= 0 this.theArray[this.topOfStack+1..] elements == this.theArray[-1] ====================================================================== |
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. The
array, the elements of the array, and topOfStack
are not
modified by this method — this method is an “observer”. The
last invariant is not particularly interesting.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
To get a sense of how DynComp helps eliminate uninteresting output, take
a look at the invariants for the exit point at line 32 of the
createItem(int)
method.
====================================================================== DataStructures.StackArTester.createItem(int):::EXIT32 this.phase == 4 return.getClass() == int[].class this.s.topOfStack < orig(i) this.phase < orig(i) this.phase != size(this.s.theArray[]) this.maxPhase < orig(i) ====================================================================== |
The value of phase
is always less than the value of
i
. While this is true for the observed executions, it is not a
helpful invariant, since phase
and i
represent different
abstract types; i
is a number to be pushed onto the stack, while
phase
is used for program flow control. Although they are both
int
s, comparing the two is not meaningful, so this invariant,
among others, is omitted from the output when Daikon is run with
DynComp.
====================================================================== DataStructures.StackArTester.createItem(int):::EXIT32 this.phase == 4 return.getClass() == int[].class this.s.topOfStack < orig(i) ====================================================================== |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
A second example is located in the ‘examples/java-examples/QueueAr’ subdirectory. Run this sample using the following steps:
cd examples/java-examples/QueueAr javac -g DataStructures/*.java |
java daikon.Chicory --daikon DataStructures.QueueArTester |
Alternately, you can split the second command into two parts:
java daikon.Chicory DataStructures.QueueArTester |
java daikon.Daikon QueueArTester.dtrace.gz |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
In order to detect invariants over C or C++ programs, you must first install a C/C++ front end (instrumenter). You can choose Kvasir (see section C/C++ front end Kvasir) or Mangel-Wurzel (see section Source-based C/C++ front end Mangel-Wurzel). We recommend the use of Kvasir, and this section gives examples using Kvasir.
To use the C/C++ front end Kvasir with your program, first make sure that
your program has been compiled with DWARF-2 format debugging
information, such as by giving the ‘-gdwarf-2’ flag to GCC when
compiling. Then, run your program as usual, but prepend
kvasir-dtrace
to the command line.
For more information about Kvasir, including more detailed documentation on its command-line options, see C/C++ front end Kvasir.
3.2.1 C examples | ||
3.2.2 Using DynComp with C programs | ||
3.2.3 Dealing with large examples |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
The Daikon distribution comes with several example C programs in the ‘examples/c-examples’ directory to enable users to become familiar with running Daikon on C programs.
To detect invariants for a program with Kvasir, you need to perform two basic tasks: run the program under Kvasir to create a data trace file (steps 1–2), and run Daikon over the data trace file to produce invariants (steps 3–4). The following instructions are for the wordplay example, which is a program for finding anagrams.
cd $DAIKONDIR/examples/c-examples/wordplay |
gcc -gdwarf-2 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-2’ when compiling each source file containing code you wish to see invariants about.
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 both variable declarations and values.
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 (http://www.valgrind.org/) with its regular memory checking tool; if they do not appear with that tool, they are probably spurious).
java daikon.Daikon \ --config_option daikon.derive.Derivation.disable_derived_variables=true \ 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 --dtrace-file=daikon-output/wordplay2.dtrace \ ./wordplay -f words.txt 'better results from multiple runs' kvasir-dtrace --dtrace-file=daikon-output/wordplay3.dtrace \ ./wordplay -f words.txt 'more testing equals better testing' java -Xmx256m daikon.Daikon daikon-output/wordplay*.dtrace |
or, 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 --dtrace-append --dtrace-file=daikon-output/wordplay-all.dtrace \ ./wordplay -f words.txt 'better results from multiple runs' kvasir-dtrace --dtrace-append --dtrace-file=daikon-output/wordplay-all.dtrace \ ./wordplay -f words.txt 'more testing equals better testing' java -Xmx256m daikon.Daikon daikon-output/wordplay-all.dtrace |
For help understanding the invariants, see Interpreting Daikon output.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
Optionally, the DynComp tool can be used along with Kvasir and Daikon. DynComp uses a dynamic analysis to infer which program variables can meaningfully be used together; Daikon can then use this information to restrict the invariants it considers, potentially improving both its performance and the usefulness of its results.
DynComp is enabled as an extra mode of Kvasir; when running with DynComp enabled, Kvasir produces two output files instead of one: in addition to a ‘.dtrace’ file containing a trace of a particular execution, the information about what variables and functions exist in a program, along with information grouping the variables into abstract types, is stored in a file with the extension ‘.decls’. Both of these files must be supplied to Daikon.
For instance, to repeat the wordplay example with DynComp, first rerun
kvasir-dtrace
giving it the option ‘--with-dyncomp’:
kvasir-dtrace --with-dyncomp \ ./wordplay -f words.txt 'daikon dynamic invariant detector' |
Then, supply the ‘.decls’ file when invoking Daikon:
java daikon.Daikon \ --config_option daikon.derive.Derivation.disable_derived_variables=true \ daikon-output/wordplay.decls daikon-output/wordplay.dtrace |
For instance, one effect of DynComp that can be seen in the wordplay
example concerns the global variables largestlet
,
rec_anag_count
, adjacentdups
, specfirstword
,
maxdepthspec
, and silent
.
These variables are all 0 in the sample execution (for instance, several
of them correspond to command-line options that are not enabled), so
without DynComp, Daikon gives the invariants that they are all equal.
However, DynComp's analysis finds that the variables are of different
abstract types, so it is not meaningful to compare them.
When DynComp information is provided, Daikon instead gives separate
invariants about the value of each variable.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
Since the default memory size used by Java virtual machines varies, we suggest that Daikon be run with at least 256 megabytes of memory (and perhaps much more), specified for many JVMs by the option ‘-Xmx256m’. 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 data trace (.dtrace) files.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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.
3.3.1 Instrumenting Perl programs | ||
3.3.2 Perl examples |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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 Perl front end dfepl.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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’.
cd examples/perl-examples |
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.
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.
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.
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 filename 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).
cd daikon-output |
java daikon.Daikon Birthday.decls test_bday-combined.dtrace |
java 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 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.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
CITADEL is an Eiffel front-end to the Daikon invariant detector. You can obtain Citadel and its documentation from http://se.inf.ethz.ch/people/polikarpova/citadel.html.
[ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
This document was generated by Daikon User on June, 23 2010 using texi2html 1.78.