Next: Front ends and instrumentation, Previous: Daikon output, Up: Top [Contents][Index]
| • Configuration options | ||
| • Conditional invariants | ||
| • Enhancing conditional invariant detection | ||
| • Dynamic abstract type inference (DynComp) | ||
| • Loop invariants |
Next: Conditional invariants, Up: Enhancing Daikon output [Contents][Index]
Many aspects of Daikon’s behavior can be controlled by setting various configuration parameters. These configuration parameters control which invariants are checked and reported, the statistical tests for invariants, which derived variables are created, and more.
There are two ways to set configuration options. You can specify a configuration setting directly on the command line, using the --config_option name=value option (which you may repeat as many times as you want). Or, you can create a configuration file and supplying it to Daikon on the command line using the --config filename option. Daikon applies all the command-line arguments in order. You may wish to use the supplied example configuration file daikon/java/daikon/config/example-settings.txt as an example when creating your own configuration files. (If you did not download Daikon’s sources, you must extract the example from daikon.jar to read it.)
You can also control Daikon’s output via its command-line options (see Running Daikon) and via the command-line options to its front ends — such as DynComp (see DynComp for Java options), Chicory (see Chicory options) or Kvasir (see Kvasir options).
The configuration options are different from the debugging flags --debug and --dbg category (see Daikon debugging options). The debugging flags permit Daikon to produce debugging output, but they do not affect the invariants that Daikon computes.
| • List of configuration options |
Up: Configuration options [Contents][Index]
This is a list of all Daikon configuration options.
The configuration option name contains the
Java class in which it is defined. (In the Daikon source code, the
configuration value is stored in a variable whose name contains a
dkconfig_ prefix, but that should be irrelevant to users.)
To learn more about a specific invariant or derived variable than
appears in this manual, see its source code.
Next: Options to enable/disable specific invariants, Previous: List of configuration options, Up: List of configuration options [Contents][Index]
These configuration options enable or disable filters that suppress printing
of certain invariants. Invariants are filtered if they are redundant.
See Invariant filters, for more information.
Also see configuration option daikon.PrintInvariants.print_all.
Boolean. If true, DerivedParameterFilter is initially turned on. The default value is ‘true’.
Boolean. If true, DotNetStringFilter is initially turned on. See its Javadoc. The default value is ‘false’.
Boolean. If true, ObviousFilter is initially turned on. The default value is ‘true’.
Boolean. If true, OnlyConstantVariablesFilter is initially turned on. The default value is ‘true’.
Boolean. If true, ParentFilter is initially turned on. The default value is ‘true’.
Boolean. If true, ReadonlyPrestateFilter is initially turned on. The default value is ‘true’.
Boolean. If true, SimplifyFilter is initially turned on. The default value is ‘true’.
Boolean. If true, UnjustifiedFilter is initially turned on. The default value is ‘true’.
Boolean. If true, UnmodifiedVariableEqualityFilter is initially turned on. The default value is ‘true’.
Next: Other invariant configuration parameters, Previous: Options to enable/disable filters, Up: List of configuration options [Contents][Index]
These options control whether Daikon looks for specific kinds of invariants. See Invariant list, for more information about the corresponding invariants.
Boolean. True iff Member invariants should be considered. The default value is ‘true’.
Boolean. True iff Member invariants should be considered. The default value is ‘true’.
Boolean. True iff SeqFloatEqual invariants should be considered. The default value is ‘true’.
Boolean. True iff SeqFloatGreaterEqual invariants should be considered. The default value is ‘true’.
Boolean. True iff SeqFloatGreaterThan invariants should be considered. The default value is ‘true’.
Boolean. True iff SeqFloatLessEqual invariants should be considered. The default value is ‘true’.
Boolean. True iff SeqFloatLessThan invariants should be considered. The default value is ‘true’.
Boolean. True iff SeqIntEqual invariants should be considered. The default value is ‘true’.
Boolean. True iff SeqIntGreaterEqual invariants should be considered. The default value is ‘true’.
Boolean. True iff SeqIntGreaterThan invariants should be considered. The default value is ‘true’.
Boolean. True iff SeqIntLessEqual invariants should be considered. The default value is ‘true’.
Boolean. True iff SeqIntLessThan invariants should be considered. The default value is ‘true’.
Boolean. True iff Member invariants should be considered. The default value is ‘true’.
Boolean. True iff FloatEqual invariants should be considered. The default value is ‘true’.
Boolean. True iff FloatGreaterEqual invariants should be considered. The default value is ‘true’.
Boolean. True iff FloatGreaterThan invariants should be considered. The default value is ‘true’.
Boolean. True iff FloatLessEqual invariants should be considered. The default value is ‘true’.
Boolean. True iff FloatLessThan invariants should be considered. The default value is ‘true’.
Boolean. True iff FloatNonEqual invariants should be considered. The default value is ‘true’.
Boolean. True iff IntEqual invariants should be considered. The default value is ‘true’.
Boolean. True iff IntGreaterEqual invariants should be considered. The default value is ‘true’.
Boolean. True iff IntGreaterThan invariants should be considered. The default value is ‘true’.
Boolean. True iff IntLessEqual invariants should be considered. The default value is ‘true’.
Boolean. True iff IntLessThan invariants should be considered. The default value is ‘true’.
Boolean. True iff IntNonEqual invariants should be considered. The default value is ‘true’.
Boolean. True iff LinearBinary invariants should be considered. The default value is ‘true’.
Boolean. True iff LinearBinary invariants should be considered. The default value is ‘true’.
Boolean. True iff divides invariants should be considered. The default value is ‘true’.
Boolean. True iff square invariants should be considered. The default value is ‘true’.
Boolean. True iff zero-track invariants should be considered. The default value is ‘false’.
Boolean. True iff BitwiseAndZero invariants should be considered. The default value is ‘false’.
Boolean. True iff bitwise complement invariants should be considered. The default value is ‘false’.
Boolean. True iff bitwise subset invariants should be considered. The default value is ‘false’.
Boolean. True iff divides invariants should be considered. The default value is ‘true’.
Boolean. True iff ShiftZero invariants should be considered. The default value is ‘false’.
Boolean. True iff square invariants should be considered. The default value is ‘true’.
Boolean. True iff zero-track invariants should be considered. The default value is ‘false’.
Boolean. True iff PairwiseIntComparison invariants should be considered. The default value is ‘true’.
Boolean. True iff PairwiseIntComparison invariants should be considered. The default value is ‘true’.
Boolean. True iff PairwiseIntComparison invariants should be considered. The default value is ‘true’.
Boolean. True iff PairwiseIntComparison invariants should be considered. The default value is ‘true’.
Boolean. True iff PairwiseIntComparison invariants should be considered. The default value is ‘true’.
Boolean. True iff PairwiseIntComparison invariants should be considered. The default value is ‘true’.
Boolean. True iff PairwiseIntComparison invariants should be considered. The default value is ‘true’.
Boolean. True iff PairwiseIntComparison invariants should be considered. The default value is ‘true’.
Boolean. True iff PairwiseIntComparison invariants should be considered. The default value is ‘true’.
Boolean. True iff PairwiseIntComparison invariants should be considered. The default value is ‘true’.
Boolean. True iff PairwiseLinearBinary invariants should be considered. The default value is ‘true’.
Boolean. True iff PairwiseLinearBinary invariants should be considered. The default value is ‘true’.
Boolean. True iff divides invariants should be considered. The default value is ‘true’.
Boolean. True iff square invariants should be considered. The default value is ‘true’.
Boolean. True iff zero-track invariants should be considered. The default value is ‘false’.
Boolean. True iff BitwiseAndZero invariants should be considered. The default value is ‘false’.
Boolean. True iff bitwise complement invariants should be considered. The default value is ‘false’.
Boolean. True iff bitwise subset invariants should be considered. The default value is ‘false’.
Boolean. True iff divides invariants should be considered. The default value is ‘true’.
Boolean. True iff ShiftZero invariants should be considered. The default value is ‘false’.
Boolean. True iff square invariants should be considered. The default value is ‘true’.
Boolean. True iff zero-track invariants should be considered. The default value is ‘false’.
Boolean. True iff SubString invariants should be considered. The default value is ‘false’.
Boolean. True iff PairwiseIntComparison invariants should be considered. The default value is ‘true’.
Boolean. True iff PairwiseIntComparison invariants should be considered. The default value is ‘true’.
Boolean. True iff PairwiseIntComparison invariants should be considered. The default value is ‘true’.
Boolean. True iff PairwiseIntComparison invariants should be considered. The default value is ‘true’.
Boolean. True iff PairwiseIntComparison invariants should be considered. The default value is ‘true’.
Boolean. True iff Reverse invariants should be considered. The default value is ‘true’.
Boolean. True iff Reverse invariants should be considered. The default value is ‘true’.
Boolean. True iff SeqSeqFloatEqual invariants should be considered. The default value is ‘true’.
Boolean. True iff SeqSeqFloatGreaterEqual invariants should be considered. The default value is ‘true’.
Boolean. True iff SeqSeqFloatGreaterThan invariants should be considered. The default value is ‘true’.
Boolean. True iff SeqSeqFloatLessEqual invariants should be considered. The default value is ‘true’.
Boolean. True iff SeqSeqFloatLessThan invariants should be considered. The default value is ‘true’.
Boolean. True iff SeqSeqIntEqual invariants should be considered. The default value is ‘true’.
Boolean. True iff SeqSeqIntGreaterEqual invariants should be considered. The default value is ‘true’.
Boolean. True iff SeqSeqIntGreaterThan invariants should be considered. The default value is ‘true’.
Boolean. True iff SeqSeqIntLessEqual invariants should be considered. The default value is ‘true’.
Boolean. True iff SeqSeqIntLessThan invariants should be considered. The default value is ‘true’.
Boolean. True iff SeqSeqStringEqual invariants should be considered. The default value is ‘true’.
Boolean. True iff SeqSeqStringGreaterEqual invariants should be considered. The default value is ‘true’.
Boolean. True iff SeqSeqStringGreaterThan invariants should be considered. The default value is ‘true’.
Boolean. True iff SeqSeqStringLessEqual invariants should be considered. The default value is ‘true’.
Boolean. True iff SeqSeqStringLessThan invariants should be considered. The default value is ‘true’.
Boolean. True iff SubSequence invariants should be considered. The default value is ‘false’.
Boolean. True iff SubSequence invariants should be considered. The default value is ‘false’.
Boolean. True iff SubSet invariants should be considered. The default value is ‘false’.
Boolean. True iff SubSet invariants should be considered. The default value is ‘false’.
Boolean. True iff SubSequence invariants should be considered. The default value is ‘false’.
Boolean. True iff SubSequence invariants should be considered. The default value is ‘false’.
Boolean. True iff SubSet invariants should be considered. The default value is ‘false’.
Boolean. True iff SubSet invariants should be considered. The default value is ‘false’.
Boolean. True iff SubString invariants should be considered. The default value is ‘false’.
Boolean. True iff StringEqual invariants should be considered. The default value is ‘true’.
Boolean. True iff StringGreaterEqual invariants should be considered. The default value is ‘true’.
Boolean. True iff StringGreaterThan invariants should be considered. The default value is ‘true’.
Boolean. True iff StringLessEqual invariants should be considered. The default value is ‘true’.
Boolean. True iff StringLessThan invariants should be considered. The default value is ‘true’.
Boolean. True iff StringNonEqual invariants should be considered. The default value is ‘true’.
Boolean. True if FunctionBinary invariants should be considered. The default value is ‘false’.
Boolean. True if FunctionBinaryFloat invariants should be considered. The default value is ‘false’.
Boolean. True iff LinearTernary invariants should be considered. The default value is ‘true’.
Boolean. True iff LinearTernary invariants should be considered. The default value is ‘true’.
Boolean. True iff CompleteOneOfScalar invariants should be considered. The default value is ‘false’.
Boolean. True iff IsPointer invariants should be considered. The default value is ‘false’.
Boolean. True iff LowerBound invariants should be considered. The default value is ‘true’.
Boolean. True iff LowerBoundFloat invariants should be considered. The default value is ‘true’.
Boolean. True iff Modulus invariants should be considered. The default value is ‘false’.
Boolean. True iff NonModulus invariants should be considered. The default value is ‘false’.
Boolean. True iff NonZero invariants should be considered. The default value is ‘true’.
Boolean. True iff NonZeroFloat invariants should be considered. The default value is ‘true’.
Boolean. True iff OneOf invariants should be considered. The default value is ‘true’.
Boolean. True iff OneOf invariants should be considered. The default value is ‘true’.
Boolean. True iff Positive invariants should be considered. The default value is ‘true’.
Boolean. True if Even invariants should be considered. The default value is ‘false’.
Boolean. True if PowerOfTwo invariants should be considered. The default value is ‘true’.
Boolean. True iff UpperBound invariants should be considered. The default value is ‘true’.
Boolean. True iff UpperBoundFloat invariants should be considered. The default value is ‘true’.
Boolean. True iff CommonSequence invariants should be considered. The default value is ‘false’.
Boolean. True iff CommonSequence invariants should be considered. The default value is ‘false’.
Boolean. True iff EltLowerBound invariants should be considered. The default value is ‘true’.
Boolean. True iff EltLowerBoundFloat invariants should be considered. The default value is ‘true’.
Boolean. True iff EltNonZero invariants should be considered. The default value is ‘true’.
Boolean. True iff EltNonZero invariants should be considered. The default value is ‘true’.
Boolean. True iff OneOf invariants should be considered. The default value is ‘true’.
Boolean. True iff OneOf invariants should be considered. The default value is ‘true’.
Boolean. True if Even invariants should be considered. The default value is ‘false’.
Boolean. True if PowerOfTwo invariants should be considered. The default value is ‘true’.
Boolean. True iff EltUpperBound invariants should be considered. The default value is ‘true’.
Boolean. True iff EltUpperBoundFloat invariants should be considered. The default value is ‘true’.
Boolean. True iff EltwiseIntComparison invariants should be considered. The default value is ‘true’.
Boolean. True iff EltwiseIntComparison invariants should be considered. The default value is ‘true’.
Boolean. True iff EltwiseIntComparison invariants should be considered. The default value is ‘true’.
Boolean. True iff EltwiseIntComparison invariants should be considered. The default value is ‘true’.
Boolean. True iff EltwiseIntComparison invariants should be considered. The default value is ‘true’.
Boolean. True iff EltwiseIntComparison invariants should be considered. The default value is ‘true’.
Boolean. True iff EltwiseIntComparison invariants should be considered. The default value is ‘true’.
Boolean. True iff EltwiseIntComparison invariants should be considered. The default value is ‘true’.
Boolean. True iff EltwiseIntComparison invariants should be considered. The default value is ‘true’.
Boolean. True iff EltwiseIntComparison invariants should be considered. The default value is ‘true’.
Boolean. True iff NoDuplicates invariants should be considered. The default value is ‘false’.
Boolean. True iff NoDuplicates invariants should be considered. The default value is ‘false’.
Boolean. True iff OneOf invariants should be considered. The default value is ‘true’.
Boolean. True iff OneOf invariants should be considered. The default value is ‘true’.
Boolean. True iff SeqIndexFloatEqual invariants should be considered. The default value is ‘false’.
Boolean. True iff SeqIndexFloatGreaterEqual invariants should be considered. The default value is ‘false’.
Boolean. True iff SeqIndexFloatGreaterThan invariants should be considered. The default value is ‘false’.
Boolean. True iff SeqIndexFloatLessEqual invariants should be considered. The default value is ‘false’.
Boolean. True iff SeqIndexFloatLessThan invariants should be considered. The default value is ‘false’.
Boolean. True iff SeqIndexFloatNonEqual invariants should be considered. The default value is ‘false’.
Boolean. True iff SeqIndexIntEqual invariants should be considered. The default value is ‘false’.
Boolean. True iff SeqIndexIntGreaterEqual invariants should be considered. The default value is ‘false’.
Boolean. True iff SeqIndexIntGreaterThan invariants should be considered. The default value is ‘false’.
Boolean. True iff SeqIndexIntLessEqual invariants should be considered. The default value is ‘false’.
Boolean. True iff SeqIndexIntLessThan invariants should be considered. The default value is ‘false’.
Boolean. True iff SeqIndexIntNonEqual invariants should be considered. The default value is ‘false’.
Boolean. True iff CompleteOneOfString invariants should be considered. The default value is ‘false’.
Boolean. True iff OneOf invariants should be considered. The default value is ‘true’.
Boolean. True iff PrintableString invariants should be considered. The default value is ‘false’.
Boolean. True iff CommonStringSequence invariants should be considered. The default value is ‘false’.
Boolean. True iff OneOf invariants should be considered. The default value is ‘true’.
Boolean. True iff OneOf invariants should be considered. The default value is ‘true’.
Next: Options to enable/disable derived variables, Previous: Options to enable/disable specific invariants, Up: List of configuration options [Contents][Index]
The configuration options listed in this section parameterize the behavior of certain invariants. See Invariant list, for more information about the invariants.
Floating-point number between 0 and 1. Invariants are displayed only if the confidence that the
invariant did not occur by chance is greater than this. (May also be set via the --conf_limit command-line option to Daikon; refer to manual.)
The default value is ‘0.99’.
Floating-point number between 0 and 0.1, representing the maximum relative difference between
two floats for fuzzy comparisons. Larger values will result in floats that are relatively
farther apart being treated as equal. A value of 0 essentially disables fuzzy comparisons.
Specifically, if abs(1 - f1/f2) is less than or equal to this value, then the two
doubles (f1 and f2) will be treated as equal by Daikon.
The default value is ‘1.0E-4’.
A boolean value. If true, Daikon’s Simplify output (printed when the --format simplify
flag is enabled, and used internally by --suppress_redundant) will include new
predicates representing some complex relationships in invariants, such as lexical ordering
among sequences. If false, some complex relationships will appear in the output as complex
quantified formulas, while others will not appear at all. When enabled, Simplify may be able to
make more inferences, allowing --suppress_redundant to suppress more redundant
invariants, but Simplify may also run more slowly.
The default value is ‘false’.
Boolean. True iff IntNonEqual invariants should be considered. The default value is ‘true’.
Regular expression to match against the class name of derived variables. Invariants that contain derived variables that match will be filtered out. If null, nothing will be filtered out. The default value is ‘null’.
Long integer. Together with the corresponding minimal_interesting parameter,
specifies the range of the computed constant that is “interesting” — the range that should
be reported. For instance, setting minimal_interesting to -1 and
maximal_interesting to 2 would only permit output of LowerBound invariants whose
cutoff was one of (-1,0,1,2).
The default value is ‘2’.
Long integer. Together with the corresponding maximal_interesting parameter,
specifies the range of the computed constant that is “interesting” — the range that should
be reported. For instance, setting minimal_interesting to -1 and
maximal_interesting to 2 would only permit output of LowerBound invariants whose
cutoff was one of (-1,0,1,2).
The default value is ‘-1’.
Long integer. Together with the corresponding minimal_interesting parameter,
specifies the range of the computed constant that is “interesting” — the range that should
be reported. For instance, setting minimal_interesting to -1 and
maximal_interesting to 2 would only permit output of LowerBoundFloat invariants whose
cutoff was one of (-1,0,1,2).
The default value is ‘2’.
Long integer. Together with the corresponding maximal_interesting parameter,
specifies the range of the computed constant that is “interesting” — the range that should
be reported. For instance, setting minimal_interesting to -1 and
maximal_interesting to 2 would only permit output of LowerBoundFloat invariants whose
cutoff was one of (-1,0,1,2).
The default value is ‘-1’.
Positive integer. Specifies the maximum set size for this type of invariant (x is one of
size items).
The default value is ‘3’.
Boolean. If true, invariants describing hashcode-typed variables as having any particular value
will have an artificial value substituted for the exact hashhode values. The artificial values
will stay the same from run to run even if the actual hashcode values change (as long as the
OneOf invariants remain the same). If false, hashcodes will be formatted as the application of
a hashcode uninterpreted function to an integer representing the bit pattern of the hashcode.
One might wish to omit the exact values of the hashcodes because they are usually
uninteresting; this is the same reason they print in the native Daikon format, for instance, as
var has only one value rather than var == 150924732.
The default value is ‘false’.
Positive integer. Specifies the maximum set size for this type of invariant (x is one of
size items).
The default value is ‘3’.
Long integer. Together with the corresponding minimal_interesting parameter,
specifies the range of the computed constant that is “interesting” — the range that should
be reported. For instance, setting minimal_interesting to -1 and
maximal_interesting to 2 would only permit output of UpperBound invariants whose
cutoff was one of (-1,0,1,2).
The default value is ‘2’.
Long integer. Together with the corresponding maximal_interesting parameter,
specifies the range of the computed constant that is “interesting” — the range that should
be reported. For instance, setting minimal_interesting to -1 and
maximal_interesting to 2 would only permit output of UpperBound invariants whose
cutoff was one of (-1,0,1,2).
The default value is ‘-1’.
Long integer. Together with the corresponding minimal_interesting parameter,
specifies the range of the computed constant that is “interesting” — the range that should
be reported. For instance, setting minimal_interesting to -1 and
maximal_interesting to 2 would only permit output of UpperBoundFloat invariants whose
cutoff was one of (-1,0,1,2).
The default value is ‘2’.
Long integer. Together with the corresponding maximal_interesting parameter,
specifies the range of the computed constant that is “interesting” — the range that should
be reported. For instance, setting minimal_interesting to -1 and
maximal_interesting to 2 would only permit output of UpperBoundFloat invariants whose
cutoff was one of (-1,0,1,2).
The default value is ‘-1’.
Boolean. Set to true to consider common sequences over hashcodes (pointers). The default value is ‘false’.
Boolean. Set to true to consider common sequences over hashcodes (pointers). The default value is ‘false’.
Long integer. Together with the corresponding minimal_interesting parameter,
specifies the range of the computed constant that is “interesting” — the range that should
be reported. For instance, setting minimal_interesting to -1 and
maximal_interesting to 2 would only permit output of EltLowerBound invariants whose
cutoff was one of (-1,0,1,2).
The default value is ‘2’.
Long integer. Together with the corresponding maximal_interesting parameter,
specifies the range of the computed constant that is “interesting” — the range that should
be reported. For instance, setting minimal_interesting to -1 and
maximal_interesting to 2 would only permit output of EltLowerBound invariants whose
cutoff was one of (-1,0,1,2).
The default value is ‘-1’.
Long integer. Together with the corresponding minimal_interesting parameter,
specifies the range of the computed constant that is “interesting” — the range that should
be reported. For instance, setting minimal_interesting to -1 and
maximal_interesting to 2 would only permit output of EltLowerBoundFloat invariants whose
cutoff was one of (-1,0,1,2).
The default value is ‘2’.
Long integer. Together with the corresponding maximal_interesting parameter,
specifies the range of the computed constant that is “interesting” — the range that should
be reported. For instance, setting minimal_interesting to -1 and
maximal_interesting to 2 would only permit output of EltLowerBoundFloat invariants whose
cutoff was one of (-1,0,1,2).
The default value is ‘-1’.
Boolean. If true, invariants describing hashcode-typed variables as having any particular value
will have an artificial value substituted for the exact hashhode values. The artificial values
will stay the same from run to run even if the actual hashcode values change (as long as the
OneOf invariants remain the same). If false, hashcodes will be formatted as the application of
a hashcode uninterpreted function to an integer representing the bit pattern of the hashcode.
One might wish to omit the exact values of the hashcodes because they are usually
uninteresting; this is the same reason they print in the native Daikon format, for instance, as
var has only one value rather than var == 150924732.
The default value is ‘false’.
Positive integer. Specifies the maximum set size for this type of invariant (x is one of
size items).
The default value is ‘3’.
Positive integer. Specifies the maximum set size for this type of invariant (x is one of
size items).
The default value is ‘3’.
Long integer. Together with the corresponding minimal_interesting parameter,
specifies the range of the computed constant that is “interesting” — the range that should
be reported. For instance, setting minimal_interesting to -1 and
maximal_interesting to 2 would only permit output of EltUpperBound invariants whose
cutoff was one of (-1,0,1,2).
The default value is ‘2’.
Long integer. Together with the corresponding maximal_interesting parameter,
specifies the range of the computed constant that is “interesting” — the range that should
be reported. For instance, setting minimal_interesting to -1 and
maximal_interesting to 2 would only permit output of EltUpperBound invariants whose
cutoff was one of (-1,0,1,2).
The default value is ‘-1’.
Long integer. Together with the corresponding minimal_interesting parameter,
specifies the range of the computed constant that is “interesting” — the range that should
be reported. For instance, setting minimal_interesting to -1 and
maximal_interesting to 2 would only permit output of EltUpperBoundFloat invariants whose
cutoff was one of (-1,0,1,2).
The default value is ‘2’.
Long integer. Together with the corresponding maximal_interesting parameter,
specifies the range of the computed constant that is “interesting” — the range that should
be reported. For instance, setting minimal_interesting to -1 and
maximal_interesting to 2 would only permit output of EltUpperBoundFloat invariants whose
cutoff was one of (-1,0,1,2).
The default value is ‘-1’.
Positive integer. Specifies the maximum set size for this type of invariant (x is one of
size items).
The default value is ‘3’.
Boolean. If true, invariants describing hashcode-typed variables as having any particular value
will have an artificial value substituted for the exact hashhode values. The artificial values
will stay the same from run to run even if the actual hashcode values change (as long as the
OneOf invariants remain the same). If false, hashcodes will be formatted as the application of
a hashcode uninterpreted function to an integer representing the bit pattern of the hashcode.
One might wish to omit the exact values of the hashcodes because they are usually
uninteresting; this is the same reason they print in the native Daikon format, for instance, as
var has only one value rather than var == 150924732.
The default value is ‘false’.
Positive integer. Specifies the maximum set size for this type of invariant (x is one of
size items).
The default value is ‘3’.
Boolean. Set to true to disable all SeqIndex invariants (SeqIndexIntEqual, SeqIndexFloatLessThan, etc). This overrides the settings of the individual SeqIndex enable configuration options. To disable only some options, the options must be disabled individually. The default value is ‘false’.
Positive integer. Specifies the maximum set size for this type of invariant (x is one of
size items).
The default value is ‘3’.
Positive integer. Specifies the maximum set size for this type of invariant (x is one of
size items).
The default value is ‘3’.
Positive integer. Specifies the maximum set size for this type of invariant (x is one of
size items).
The default value is ‘2’.
Next: Simplify interface configuration options, Previous: Other invariant configuration parameters, Up: List of configuration options [Contents][Index]
These options control whether Daikon looks for invariants involving certain forms of derived variables. Also see Variable names.
Boolean. If true, Daikon will not create any derived variables. Derived variables, which are
combinations of variables that appeared in the program, like array[index] if array and index appeared, can increase the number of properties Daikon finds,
especially over sequences. However, derived variables increase Daikon’s time and memory usage,
sometimes dramatically. If false, individual kinds of derived variables can be enabled or
disabled individually using configuration options under daikon.derive.
The default value is ‘false’.
Boolean. True iff SequenceFloatIntersection derived variables should be generated. The default value is ‘false’.
Boolean. True iff SequenceFloatSubscript derived variables should be generated. The default value is ‘true’.
Boolean. True iff SequenceFloatSubsequence derived variables should be generated. The default value is ‘false’.
Boolean. True iff SequenceFloatUnion derived variables should be generated. The default value is ‘false’.
Boolean. True iff SequenceScalarIntersection derived variables should be generated. The default value is ‘false’.
Boolean. True iff SequenceScalarSubscript derived variables should be generated. The default value is ‘true’.
Boolean. True iff SequenceScalarSubsequence derived variables should be generated. The default value is ‘false’.
Boolean. True iff SequenceScalarUnion derived variables should be generated. The default value is ‘false’.
Boolean. True iff SequenceStringIntersection derived variables should be generated. The default value is ‘false’.
Boolean. True iff SequenceStringSubscript derived variables should be generated. The default value is ‘true’.
Boolean. True iff SequenceStringSubsequence derived variables should be generated. The default value is ‘false’.
Boolean. True iff SequenceStringUnion derived variables should be generated. The default value is ‘false’.
Boolean. True iff SequencesConcat derived variables should be created. The default value is ‘false’.
Boolean. True iff SequencesJoin derived variables should be generated. The default value is ‘false’.
Boolean. True iff SequencesJoin derived variables should be generated. The default value is ‘false’.
Boolean. True if Daikon should only generate derivations on boolean predicates. The default value is ‘true’.
Boolean. True iff SequencesPredicate derived variables should be generated. The default value is ‘false’.
Boolean. True if Daikon should only generate derivations on fields of the same data structure. The default value is ‘true’.
Boolean. True if Daikon should only generate derivations on boolean predicates. The default value is ‘true’.
Boolean. True iff SequencesPredicate derived variables should be generated. The default value is ‘false’.
Boolean. True if Daikon should only generate derivations on fields of the same data structure. The default value is ‘true’.
Boolean. True iff SequenceFloatArbitrarySubsequence derived variables should be generated. The default value is ‘false’.
Boolean. True iff SequenceScalarArbitrarySubsequence derived variables should be generated. The default value is ‘false’.
Boolean. True iff SequenceStringArbitrarySubsequence derived variables should be generated. The default value is ‘false’.
Boolean. True iff SequenceInitial derived variables should be generated. The default value is ‘false’.
Boolean. True iff SequenceInitial derived variables should be generated. The default value is ‘false’.
Boolean. True iff SequenceLength derived variables should be generated. The default value is ‘true’.
Boolean. True iff SequencesMax derived variables should be generated. The default value is ‘false’.
Boolean. True iff SequenceMin derived variables should be generated. The default value is ‘false’.
Boolean. True iff SequenceSum derived variables should be generated. The default value is ‘false’.
Boolean. True iff StringLength derived variables should be generated. The default value is ‘false’.
Next: Splitter options, Previous: Options to enable/disable derived variables, Up: List of configuration options [Contents][Index]
The configuration options in this section are used to customize the interface to the Simplify theorem prover. See the description of the --suppress_redundant command-line option in Options to control invariant detection.
Boolean. Controls Daikon’s response when inconsistent invariants are discovered while running Simplify. If true, Daikon will print an error message to the standard error stream listing the contradictory invariants. This is mainly intended for debugging Daikon itself, but can sometimes be helpful in tracing down other problems. For more information, see the section on troubleshooting contradictory invariants in the Daikon manual. The default value is ‘false’.
Boolean. Controls Daikon’s response when inconsistent invariants are discovered while running Simplify. If false, Daikon will give up on using Simplify for that program point. If true, Daikon will try to find a small subset of the invariants that cause the contradiction and avoid them, to allow processing to continue. For more information, see the section on troubleshooting contradictory invariants in the Daikon manual. The default value is ‘true’.
Boolean. If true, ask Simplify to check a simple proposition after each assumption is pushed, providing an opportunity to wait for output from Simplify and potentially receive error messages about the assumption. When false, long sequences of assumptions may be pushed in a row, so that by the time an error message arrives, it’s not clear which input caused the error. Of course, Daikon’s input to Simplify isn’t supposed to cause errors, so this option should only be needed for debugging. The default value is ‘false’.
A non-negative integer, representing the largest number of iterations for which Simplify should
be allowed to run on any single conjecture before giving up. Larger values may cause Simplify
to run longer, but will increase the number of invariants that can be recognized as redundant.
The default value is small enough to keep Simplify from running for more than a few seconds on
any one conjecture, allowing it to verify most simple facts without getting bogged down in long
searches. A value of 0 means not to bound the number of iterations at all, though see also the
simplify_timeout parameter..
A non-negative integer, representing the longest time period (in seconds) Simplify should be
allowed to run on any single conjecture before giving up. Larger values may cause Simplify to
run longer, but will increase the number of invariants that can be recognized as redundant.
Roughly speaking, the time spent in Simplify will be bounded by this value, times the number of
invariants generated, though it can be much less. A value of 0 means to not bound Simplify at
all by time, though also see the option simplify_max_iterations. Beware that using this
option might make Daikon’s output depend on the speed of the machine it’s run on.
The default value is ‘0’.
Boolean. If true, the input to the Simplify theorem prover will also be directed to a file
named simplifyN.in (where N is a number starting from 0) in the current directory. Simplify’s
operation can then be reproduced with a command like Simplify -nosc <simplify0.in. This
is intended primarily for debugging when Simplify fails.
The default value is ‘false’.
Positive values mean to print extra indications as each candidate invariant is passed to
Simplify during the --suppress_redundant check. If the value is 1 or higher, a hyphen
will be printed when each invariant is passed to Simplify, and then replaced by a T if
the invariant was redundant, F if it was not found to be, and ? if Simplify
gave up because of a time limit. If the value is 2 or higher, a < or > will
also be printed for each invariant that is pushed onto or popped from from Simplify’s
assumption stack. This option is mainly intended for debugging purposes, but can also provide
something to watch when Simplify takes a long time.
The default value is ‘0’.
Next: Debugging options, Previous: Simplify interface configuration options, Up: List of configuration options [Contents][Index]
The configuration options in this section are used to customize the behavior of splitters, which yield conditional invariants and implications (see Conditional invariants).
Enumeration (integer). Specifies the granularity to use for callsite splitter processing. (That is, for creating invariants for a method that are dependent on where the method was called from.) 0 is line-level granularity; 1 is method-level granularity; 2 is class-level granularity. The default value is ‘1’.
Boolean. If true, the built-in splitting rules are disabled. The built-in rules look for implications based on boolean return values and also when there are exactly two exit points from a method. The default value is ‘false’.
Integer. A value of zero indicates that DummyInvariant objects should not be created. A value of one indicates that dummy invariants should be created only when no suitable condition was found in the regular output. A value of two indicates that dummy invariants should be created for each splitting condition. The default value is ‘0’.
Split bi-implications ("a <==> b") into two separate implications ("a ==> b"
and "b ==> a").
The default value is ‘false’.
When true, compilation errors during splitter file generation will not be reported to the user. The default value is ‘true’.
Positive integer. Specifies the Splitter compilation timeout, in seconds, after which the compilation process is terminated and retried, on the assumption that it has hung. The default value is ‘20’.
String. Specifies which Java compiler is used to compile Splitters. This can be the full path name or whatever is used on the command line. Uses the current classpath. The default value is ‘javac -nowarn -source 8 -target 8 -classpath /homes/gws/markro/jdk1.8.0_351/lib/tools.jar:/homes/gws/markro/jdk1.8.0_351/classes’.
Boolean. If true, the temporary Splitter files are deleted on exit. Set it to "false" if you are debugging splitters. The default value is ‘true’.
Boolean. Enables indiscriminate splitting (see Daikon manual, Indiscriminate splitting, for an explanation of this technique). The default value is ‘true’.
Next: Quantity of output, Previous: Splitter options, Up: List of configuration options [Contents][Index]
The configuration options in this section are used to cause extra output that is useful for debugging. Also see section "Daikon debugging options" (see Daikon debugging options).
When true, perform detailed internal checking. These are essentially additional, possibly costly assert statements. The default value is ‘false’.
Determines whether or not detailed info (such as from add_modified) is printed.
The default value is ‘false’.
Determines whether or not traceback information is printed for each call to log. The default value is ‘false’.
If true, show stack traces for errors such as file format errors. The default value is ‘false’.
Next: General configuration options, Previous: Debugging options, Up: List of configuration options [Contents][Index]
The configuration options in this section make Daikon print more or less output. They do not affect which invariants Daikon computes, only how it ouputs them. Also see the following section.
If "always", then invariants are always guarded. If "never", then invariants are never guarded. If "missing", then invariants are guarded only for variables that were missing ("can be missing") in the dtrace (the observed executions). If "default", then use "missing" mode for Java output and "never" mode otherwise.
Guarding means adding predicates that ensure that variables can be dereferenced. For
instance, if a can be null — that is, if a.b can be nonsensical — then the
guarded version of
a.b == 5
is
(a != null) -> (a.b == 5)
.
(To do: Some configuration option (maybe this one) should add guards for other reasons that
lead to nonsensical values (see Variable names).)
The default value is ‘default’.
Boolean. Controls whether conditional program points are displayed. The default value is ‘true’.
Boolean. Controls whether or not the total samples read and processed are printed at the end of processing. The default value is ‘false’.
The amount of time to wait between updates of the progress display, measured in milliseconds. A value of -1 means do not print the progress display at all. The default value is ‘1000’.
The number of columns of progress information to display. In many Unix shells, this can be set
to an appropriate value by --config_option
daikon.Daikon.progress_display_width=$COLUMNS.
The default value is ‘80’.
Boolean. Controls whether or not processing information is printed out. Setting this variable
to true also automatically sets progress_delay to -1.
The default value is ‘false’.
Boolean. When false, don’t count the number of lines in the dtrace file before reading. This will disable the percentage progress printout. The default value is ‘true’.
Long integer. If non-zero, this value will be used as the number of lines in (each) dtrace file input for the purposes of the progress display, and the counting of the lines in the file will be suppressed. The default value is ‘0’.
Boolean. When true, don’t print a warning about unmatched procedure entries, which are ignored
by Daikon (unless the --nohierarchy command-line argument is provided).
The default value is ‘false’.
Boolean. If true, prints the unmatched procedure entries verbosely. The default value is ‘false’.
If true, print all invariants without any filtering. The default value is ‘false’.
Print invariant classname with invariants in output of format() method. Normally used
only for debugging output rather than ordinary printing of invariants. This is especially
useful when two different invariants have the same printed representation.
The default value is ‘false’.
If true, print the total number of true invariants. This includes invariants that are redundant and would normally not be printed or even created due to optimizations. The default value is ‘false’.
Previous: Quantity of output, Up: List of configuration options [Contents][Index]
This section lists miscellaneous configuration options for Daikon.
Boolean. Just print the total number of possible invariants and exit. The default value is ‘false’.
Integer. Percentage of program points to process. All program points are sorted by name, and
all samples for the first ppt_perc program points are processed. A percentage of 100
matches all program points.
The default value is ‘100’.
Boolean. Controls whether the Daikon optimizations (equality sets, suppressions) are undone at the end to create a more complete set of invariants. Output does not include conditional program points, implications, reflexive and partially reflexive invariants. The default value is ‘false’.
Boolean. Controls which invariants are created for variables that are constant for the entire run. If true, create only OneOf invariants. If false, create all possible invariants.
Note that setting this to true only fails to create invariants between constants. Invariants between constants and non-constants are created regardless.
A problem occurs with merging when this is turned on. If a var_info is constant at one child slice, but not constant at the other child slice, interesting invariants may not be merged because they won’t exist on the slice with the constant. This is thus currently defaulted to false. The default value is ‘false’.
Whether to use the dynamic constants optimization. This optimization doesn’t instantiate invariants over constant variables (i.e., that that have only seen one value). When the variable receives a second value, invariants are instantiated and are given the sample representing the previous constant value. The default value is ‘true’.
Boolean. When false, set modbits to 1 iff the printed representation has changed. When true, set modbits to 1 if the printed representation has changed; leave other modbits as is. The default value is ‘true’.
Boolean. When true, suppress exceptions related to file reading. This permits Daikon to continue even if there is a malformed trace file. Use this with care: in general, it is better to fix the problem that caused a bad trace file, rather than to suppress the exception. The default value is ‘false’.
When true, just ignore exit ppts that don’t have a matching enter ppt rather than exiting with an error. Unmatched exits can occur if only a portion of a dtrace file is processed. The default value is ‘false’.
Integer. Maximum number of lines to read from the dtrace file. If 0, reads the entire file. The default value is ‘0’.
Boolean. When true, only read the samples, but don’t process them. Used to gather timing information. The default value is ‘false’.
If true, modified all ppt names to remove duplicate routine names within the ppt name. This is used when a stack trace (of active methods) is used as the ppt name. The routine names must be separated by vertical bars (|). The default value is ‘false’.
Boolean. Controls whether the object-user relation is created in the variable hierarchy. The default value is ‘false’.
If true, create one equality set for each variable. This has the effect of turning the equality optimization off, without actually removing the sets themselves (which are presumed to exist in many parts of the code). The default value is ‘false’.
Boolean. If true, create implications for all pairwise combinations of conditions, and all pairwise combinations of exit points. If false, create implications for only the first two conditions, and create implications only if there are exactly two exit points. The default value is ‘false’.
Remove invariants at lower program points when a matching invariant is created at a higher program point. For experimental purposes only. The default value is ‘false’.
In the new decl format, print array names as ’a[]’ as opposed to ’a[..]’ This creates names that are more compatible with the old output. This option has no effect in the old decl format. The default value is ‘true’.
If false, don’t print entry method program points for methods that override or implement another method (i.e., entry program points that have a parent that is a method). Microsoft Code Contracts does not allow contracts on such methods. The default value is ‘true’.
If true, remove as many variables as possible that need to be indicated as ’post’. Post variables occur when the subscript for a derived variable with an orig sequence is not orig. For example: orig(a[post(i)]) An equivalent expression involving only orig variables is substitued for the post variable when one exists. The default value is ‘false’.
This option must be given with "–format Java" option.
Instead of outputting prestate expressions as "\old(E)" within an invariant, output a variable name (e.g. ‘v1’). At the end of each program point, output the list of variable-to-expression mappings. For example: with this option set to false, a program point might print like this:
foo.bar.Bar(int):::EXIT \old(capacity) == sizeof(this.theArray)
With the option set to true, it would print like this:
foo.bar.Bar(int):::EXIT v0 == sizeof(this.theArray) prestate assignment: v0=capacity
The default value is ‘true’.
This enables a different way of treating static constant variables. They are not created into invariants into slices. Instead, they are examined during print time. If a unary invariant contains a value which matches the value of a static constant varible, the value will be replaced by the name of the variable, "if it makes sense". For example, if there is a static constant variable a = 1. And if there exists an invariant x <= 1, x <= a would be the result printed. The default value is ‘false’.
If true, treat 32 bit values whose high bit is on, as a negative number (rather than as a 32 bit unsigned). The default value is ‘false’.
If true, the treat static constants (such as MapQuick.GeoPoint.FACTOR) as fields within an object rather than as a single name. Not correct, but used to obtain compatibility with VarInfoName. The default value is ‘true’.
If true, then variables are only considered comparable if they are declared with the same type. For example, java.util.List is not comparable to java.util.ArrayList and float is not comparable to double. This may miss valid invariants, but significant time can be saved and many variables with different declared types are not comparable (e.g., java.util.Date and java.util.ArrayList). The default value is ‘true’.
When true, apply orig directly to variables, do not apply orig to derived variables. For example, create ’size(orig(a[]))’ rather than ’orig(size(a[]))’. The default value is ‘false’.
Enable experimental techniques on static constants. The default value is ‘false’.
Boolean. If true, enable non-instantiating suppressions. The default value is ‘true’.
Int. Less and equal to this number means use the falsified method in the hybrid method of processing falsified invariants, while greater than this number means use the antecedent method. Empirical data shows that number should not be more than 10000. The default value is ‘2500’.
Boolean. If true, skip variables of file rep type hashcode when creating invariants
over constants in the antecedent method.
The default value is ‘true’.
Specifies the algorithm that NIS uses to process suppressions. Possible selections are ’HYBRID’, ’ANTECEDENT’, and ’FALSIFIED’. The default is the hybrid algorithm which uses the falsified algorithm when only a small number of suppressions need to be processed and the antecedent algorithm when a large number of suppressions are processed. The default value is ‘HYBRID’.
Boolean. If true, use the specific list of suppressor related invariant prototypes when creating constant invariants in the antecedent method. The default value is ‘true’.
Next: Enhancing conditional invariant detection, Previous: Configuration options, Up: Enhancing Daikon output [Contents][Index]
Conditional invariants are invariants that are true only part of the time. For instance, consider the absolute value procedure. Its postcondition is
if arg < 0 then return == -arg else return == arg
The invariant return == -arg is a conditional invariant because
it depends on the predicate arg < 0 being true. An
implication is a compound invariant that includes both the
predicate and the conditional invariant (also called the consequent);
an example of an implication is arg < 0 ==> return == -arg.
Another type of implication is a context-sensitive invariant — a
fact about method A that is true only when A is called by method B, but
not true in general about A.
You can use the configuration option
daikon.split.ContextSplitterFactory.granularity to control creation
of context-sensitive invariants.
Alternately, you can use implications to construct
context-sensitive invariants: set a variable that depends on the call
site, then compute an implication whose predicate tests that variable.
For an example, see the paper Selecting, refining, and evaluating
predicates for program analysis
(http://plse.cs.washington.edu/daikon/pubs/predicates-tr914-abstract.html).
Daikon must be supplied with the predicate for an implication. Daikon has
certain built-in predicates that it uses for finding conditional invariants;
examples are which return statement was executed in a procedure and whether a
boolean procedure returns true or false. Additionally, Daikon can read
predicates from a file called a splitter info (.spinfo) file and find
implications based on those predicates. The splitter info file can be produced
automatically, such as by static analysis of the program using the CreateSpinfo
and CreateSpinfoC programs (see Static analysis for splitters)
or by cluster analysis of the
traced values in the data trace file. Details of these techniques and usage
guides can be found in Enhancing conditional invariant detection. Users
can also create splitter info files themselves or can augment
automatically-created ones.
To detect conditional invariants and implications:
java -cp $DAIKONDIR/daikon.jar daikon.Daikon Foo.decls Foo.spinfo Foo.dtrace
The term splitter comes from Daikon’s technique for detecting implications and conditional invariants. For each predicate, Daikon creates two conditional program points — one for program executions that satisfy the condition and one for those that don’t — and splits the data trace into two parts. Invariant detection is then performed on the conditional program points (that is, the parts of the data trace) separately and any invariants detected are reported as conditional invariants (as implications).
To be precise, we say that an invariant holds exclusively if it is discovered on one side of a split, and its negation is discovered on the opposite side. Daikon creates conditional invariants whose predicates are invariants that hold exclusively on one side of a split, and whose consequents are invariants that hold on that side of the split but not on the unsplit program point. If Daikon finds multiple exclusive conditions, it will create biconditional (“if and only if”) invariants between the equivalent conditions. Within the context of the program, each of the exclusive conditions is equivalent to the splitting condition. In particular, if both the splitting condition and its negation are within the grammar of invariants that Daikon detects, the splitting condition may appear as the predicate of the generated conditional invariants. On the other hand, if other equivalent conditions are found, or if the splitting condition is not expressible in Daikon’s grammar, it might not appear in the generated implications.
In some cases, the default policy of selecting predicates from Daikon’s output may be insufficient. For instance, Daikon might not detect any invariant equivalent to the splitting condition, if the splitting condition is sufficiently complex or application-specific. In such situations, Daikon can also use the splitting condition itself, as what is called a dummy invariant. To use dummy invariants, set the configuration option daikon.split.PptSplitter.dummy_invariant_level to a non-zero value (see List of configuration options).
| • Splitter info file format | ||
| • Indiscriminate splitting | ||
| • Example splitter info file |
Next: Indiscriminate splitting, Up: Conditional invariants [Contents][Index]
A splitter info file contains the conditions that Daikon should use to create conditional invariants. Each section in the .spinfo file consists of a sequence of non-blank lines; sections are separated by blank lines. There are two types of sections: program point sections and replacement sections. See Example splitter info file, for an example splitter info file.
| • Program point sections | ||
| • Replacement sections |
Next: Replacement sections, Up: Splitter info file format [Contents][Index]
Program point sections have a line specifying a program point name followed by lines specifying the condition(s) associated with that program point, each condition on its own line. Additional information about a condition may be specified on indented lines. For example, a typical entry is
PPT_NAME pptname
condition1
condition2
DAIKON_FORMAT string
ESC_FORMAT string
condition3
...
pptname can be any string that matches a part of the desired
program point name as printed in the .decls file. In finding matching
program points, Daikon uses the first program point that matches
pptname. Caution is necessary when dealing with method names
that are prefixes of other method names. For instance, if the class
List has methods add and addAll, specifying
‘PPT_NAME List.add’ might select either method, depending on
which was encountered first. Instead writing ‘PPT_NAME
List.add(’ will match only the add method.
Each condition is a Java expression of boolean type. All variables that appear in the condition must also appear in the declaration of the program point in the .decls file. (In other words, all the variables must be in scope at the program point(s) where the Splitter is intended to operate.) The automatically generated Splitter source code fails to compile (but Daikon proceeds without it) if a variable name in a condition is not found at the matching program point.
An indented lines beginning with ‘DAIKON_FORMAT’, ‘JAVA_FORMAT’, ‘ESC_FORMAT’, or ‘SIMPLIFY_FORMAT’ specifies how to print the condition. These are optional; for any Daikon output format that is omitted, the Java condition itself is used. The alternate printed representation is used when the splitting condition is used as a dummy invariant; see configuration option daikon.split.PptSplitter.dummy_invariant_level.
Previous: Program point sections, Up: Splitter info file format [Contents][Index]
Ordinarily, a splitting condition may not invoke user-defined methods, because when Daikon reads data trace files, it does not have access to the program source. A replace section of the splitter info file can specify the bodies of methods, permitting conditions to invoke those methods. The format is as follows:
REPLACE procedure1 replacement1 procedure2 replacement2 ...
where replacementi is a Java expression for the body of procedurei. In each condition, Daikon replaces procedure calls by their replacements. A replace section may appear anywhere in the splitter info file.
Next: Example splitter info file, Previous: Splitter info file format, Up: Conditional invariants [Contents][Index]
Each condition in an .spinfo is associated with a program point. The condition can be used at only that program point by placing the following line in a file that is passed to Daikon via the --config flag (see Daikon configuration options):
daikon.split.SplitterList.all_splitters = false
The default, called indiscriminate splitting, is to use every condition at every program point, regardless of where in the .spinfo file the condition appeared.
The advantage of indiscriminate splitting is that a condition that is useful at one program point may also be useful at another — if the same variables are in scope or other variables of the same name are in scope. The disadvantage of indiscriminate splitting is that it slows Daikon down.
Daikon uses a condition only where it can be used. For example, the
condition myArray.length == x is applicable only at program points
that have variables named myArray and x. To see
warnings about places a splitting condition cannot be used (reported as
failure to compile splitters at those locations), place the following line
in a file that is passed to Daikon via the --config flag
(see Daikon configuration options):
daikon.split.SplitterList.all_splitters_errors = true
Previous: Indiscriminate splitting, Up: Conditional invariants [Contents][Index]
Below is an implementation of a simple Queue for positive integers and
a corresponding .spinfo file. The splitter info file is like
the one that CreateSpinfo would create for that class, but
also demonstrates some other features.
| • Example class | ||
| • Resulting .spinfo file |
Next: Resulting .spinfo file, Up: Example splitter info file [Contents][Index]
class simpleStack {
private int[] myArray;
private int currentSize;
public simpleStack(int capacity) {
myArray = new int[capacity];
currentSize = 0;
}
/** Adds an element to the back of the stack, if the stack is
* not full.
* Returns true if this succeeds, false otherwise. */
public String push(int x) {
if ( !isFull() && x >= 0) {
myArray[currentSize] = x;
currentSize++;
return true;
} else {
return false;
}
}
/** Returns the most recently inserted stack element.
* Returns -1 if the stack is empty. */
public int pop() {
if ( !isEmpty() ) {
currentSize--;
return myArray[currentSize];
} else {
return -1;
}
}
/** Returns true if the stack is empty, false otherwise. */
private boolean isEmpty() {
return (currentSize == 0);
}
/** Returns true if the stack is full, false otherwise. */
private boolean isFull() {
return (currentSize == myArray.length);
}
}
Previous: Example class, Up: Example splitter info file [Contents][Index]
REPLACE
isFull()
currentSize == myArray.length
isEmpty()
currentSize == 0
PPT_NAME simpleStack.push
!isFull() && x >= 0
DAIKON_FORMAT !isFull() and x >= 0
SIMPLIFY_FORMAT (AND (NOT (isFull this)) (>= x 0))
PPT_NAME simpleStack.pop
!isEmpty()
PPT_NAME simpleStack.isFull
currentSize == myArray.length - 1
PPT_NAME simpleStack.isEmpty
currentSize == 0
Next: Dynamic abstract type inference (DynComp), Previous: Conditional invariants, Up: Enhancing Daikon output [Contents][Index]
The built-in mechanisms (see Conditional invariants) have limitations in the invariants they can find. By supplying splitting conditions to Daikon via a splitter info file, the user can infer more conditional invariants. To ease this task, there are methods to automatically create splitter info files for use by Daikon.
| • Static analysis for splitters | ||
| • Cluster analysis for splitters | ||
| • Random selection for splitters |
Next: Cluster analysis for splitters, Up: Enhancing conditional invariant detection [Contents][Index]
In static analysis, all boolean statements in the program source are extracted and used as splitting conditions. The assumption is that conditions that are explicitly tested in the program are likely to affect the program’s behavior and could lead to useful conditional invariants. The simple heuristic of using these conditional statements as predicates for conditional invariant detection is often quite effective.
| • Static analysis of Java for splitters | ||
| • Static analysis of C for splitters |
The CreateSpinfo program takes Java source code as input and creates a
splitter info file for each Java file; for instance,
java -cp $DAIKONDIR/daikon.jar daikon.tools.jtb.CreateSpinfo Foo.java Bar.java
creates the splitter info files Foo.spinfo and
Bar.spinfo.
Given an -o filename argument, CreateSpinfo puts all the
splitters in the specified file instead.
The resulting splitter info file(s) contains each
boolean expression that appears in the source code.
If you get an error such as
jtb.ParseException: Encountered ";" at line 253, column 8. Was expecting one of: "abstract" ...
then you may have encountered a bug in the JTB library on which
CreateSpinfo is built. It does not permit empty declarations in a
class body. Remove the extra semicolon in your Java file (at the
indicated position) and re-rerun CreateSpinfo.
Previous: Static analysis of Java for splitters, Up: Static analysis for splitters [Contents][Index]
The CreateSpinfoC program performs the same function for
C source code as CreateSpinfoC does for Java.
CreateSpinfoC can only be run on postprocessed source
files—that is, source files contain no CPP commands. CPP commands
are lines starting with ‘#’, such as ‘#include’. To
expand CPP commands into legal C, run either cpp -P or
gcc -P -E. For instance, here is how you could use CreateSpinfoC:
cpp -P foo.c foo.c-expanded
cpp -P bar.c bar.c-expanded
java -cp $DAIKONDIR/daikon.jar daikon.tools.jtb.CreateSpinfoC \
foo.c-expanded bar.c-expanded
WARNING: The names produced by CreateSpinfoC sometimes differ
from the names produced by Kvasir. For example, suppose you have a C
file that contains a function ‘foo’. Then CreateSpinfoC
may create a .spinfo file that mentions a program point named
‘std.foo’, whereas Kvasir creates a .dtrace file that
mentions a program point named ‘..foo’. Such a mismatch will cause
Daikon to produce no conditional invariants for the given program point.
This is a bug that needs to be fixed! (Patches are welcome.) In the
meanwhile, you can edit the generated .spinfo file to conform to the
.dtrace file’s naming conventions.
If you get an error such as
... Lexical error at line 5, column 1. Encountered: "#" (35), after : ""
then you forgot to run CPP before running CreateSpinfoC.
If you get an error such as
CreateSpinfoC encountered errors during parse.
Encountered "__extension__ typedef struct { ...
then your program uses non-standard C syntax. The ‘__extension__’
keyword is supported only by the gcc compiler, and isn’t handled by
the CreateSpinfoC program. You could extend the CreateSpinfoC program
to handle non-standard gcc extensions, or you could remove non-standard
gcc extensions from your program. The extensions might also result from
standard libraries rather than your own program — removing a
directives such as ‘#include <stdio.h>’ when preprocessing may also
resolve the problem.
Next: Random selection for splitters, Previous: Static analysis for splitters, Up: Enhancing conditional invariant detection [Contents][Index]
Cluster analysis is a statistical method that finds groups or clusters in data. The clusters may indicate conditional properties in the program. The cluster analysis mechanism finds clusters in the data trace file, infers invariants over any clusters that it finds, and writes these invariants into a splitter info file. Then, you supply the splitter info file to Daikon in order to infer conditional invariants.
To find splitting conditions using cluster analysis, run the
runcluster.pl program (found in the $DAIKONDIR/scripts
directory) in the following way:
runcluster.pl [options] dtrace_file ... decls_files ...
The options are:
ALG specifies a clustering algorithm. Current options are ‘km’ (for kmeans), ‘hierarchical’, and ‘xm’ (for xmeans). The default is ‘xm’.
The number of clusters to use (for algorithms which require this input, which is everything except xmeans). The default is 4.
Don’t delete the temporary files created by the clustering process. This is a debugging flag.
The runcluster.pl script currently supports three clustering
programs. They are implementations of the kmeans algorithm,
hierarchical clustering, and the xmeans algorithm (kmeans algorithm
with efficient discovery of the number of clusters). The kmeans and
hierarchical clustering tools are provided in the Daikon
distribution. The xmeans code and executable are publicly available at
http://www.cs.cmu.edu/~dpelleg/kmeans.html (fill in the license
form and mail it in).
Previous: Cluster analysis for splitters, Up: Enhancing conditional invariant detection [Contents][Index]
Random selection can create representative samples of a data set with
the added benefit of finding conditional properties and eliminating
outliers. Given trace data, the TraceSelect tool creates several
small subsets of the data by randomly selecting parts of the original
trace file. Any invariant that is discovered in the smaller samples but
not found over the entire data is a conditional invariant.
To find splitting conditions using random selection, run the
daikon.tools.TraceSelect program in the following way:
java -cp $DAIKONDIR/daikon.jar daikon.tools.TraceSelect \
num_reps sample_size [options] \
dtrace_file decls_files ... [daikon_options]
num_reps is the number of subsets to create, and sample_size is the number of invocations to collect for each method.
The daikon_options are the same options that can be provided to the
daikon.Daikon program.
The options for TraceSelect are:
Don’t delete the temporary trace samples created by the random selection process. This can help for debugging or for using the tool solely to create trace samples instead of calculating invariants over the samples.
Allows random selection to choose method invocations that entered the method successfully but did not exit normally; either from a thrown Exception or abnormal termination.
Creates an .spinfo file for generating conditional invariants and implications by reporting the invariants that appear in at least one of the samples but not over the entire data set.
Next: Loop invariants, Previous: Enhancing conditional invariant detection, Up: Enhancing Daikon output [Contents][Index]
Abstract types group variables that are used for related purposes in a
program.
For example, suppose that some int variables in your program
are array indices, and other int variables
represent time. Even though these variables have the same type
(int) in the programming language, they have different abstract
types.
Abstract types can be provided as input to Daikon, so that it only infers invariants between values of the same abstract type. This has two benefits. First, it improves Daikon’s performance, often by over an order of magnitude, because it reduces the number of potential invariants that must be checked. Second, it reduces spurious output caused by invariants over unrelated variables. You are strongly recommended to supply abstract types when running Daikon; Daikon does not produce satisfactory output without abstract type information.
Abstract type inference is performed by the front-ends, before Daikon runs. The Daikon distribution includes three tools that infer abstract types (also called comparability types) from program executions.
Previous: Dynamic abstract type inference (DynComp), Up: Enhancing Daikon output [Contents][Index]
Daikon does not by default output loop invariants. Daikon can detect invariants at any location where it is provided with variable values, but currently Daikon’s front ends do not supply Daikon with variable values at loop heads.
You could extend a front end to output more variable values, or you could write a new front end.
Alternately, here is a way to use the current front ends to produce loop invariants. This workaround requires you to change your program, but it requires no change to Daikon or its front ends.
At the top of a loop (or at any other location in the program at which you would like to obtain invariants), insert a call to a dummy procedure that does no work but returns immediately. Pass, as arguments to the dummy procedure, all variables of interest (including local variables). Daikon will produce (identical) preconditions and postconditions for the dummy procedure; these are properties that held at the call site.
For instance, you might change the original code
public void calculate(int x) {
int tmp = 0;
while (x > 0) {
// you desire to compute an invariant here
tmp=tmp+x;
x=x-1;
}
}
into
public void calculate(int x) {
int tmp = 0;
while (x > 0) {
calculate_loophead(x, tmp);
tmp=tmp+x;
x=x-1;
}
}
// dummy procedure
public void calculate_loophead(int x, int tmp) {
}
Previous: Dynamic abstract type inference (DynComp), Up: Enhancing Daikon output [Contents][Index]