daikon
Class Daikon

Object
  Daikon

public final class Daikon
extends Object

The "main" method is the main entry point for the Daikon invariant detector. The "mainHelper" method is the entry point, when called programmatically.

Nested Class Summary

static class	Daikon.FileIOProgress Outputs FileIO progress information.
static class	Daikon.FileOptions
static class	Daikon.TerminationMessage Thrown to indicate that main should not print a stack trace, but only print the message itself to the user.

Field Summary

static PptMap	all_ppts
static boolean	check_program_types
static String	conf_limit_SWITCH
static String	config_option_SWITCH
static String	config_SWITCH
static Invariant	current_inv current invariant (used for debugging)
static String	debug_SWITCH
static String	debugAll_SWITCH
static Logger	debugEquality
static Logger	debugInit Debug tracer for ppt initialization.
static Logger	debugProgress
static Logger	debugStats Prints out statistics concerning equality sets, suppressions, etc.
static Logger	debugTrace Debug tracer.
static boolean	disable_modbit_check_error
static boolean	disable_modbit_check_message
static String	disc_reason_SWITCH
static boolean	dkconfig_calc_possible_invs Boolean.
static boolean	dkconfig_disable_splitting Boolean.
static boolean	dkconfig_enable_floats Boolean.
static String	dkconfig_guardNulls If "always", then invariants are always guarded.
static boolean	dkconfig_internal_check When true, perform detailed internal checking.
static boolean	dkconfig_output_conditionals Boolean.
static int	dkconfig_ppt_perc Integer.
static boolean	dkconfig_print_sample_totals Boolean.
static int	dkconfig_progress_delay The amount of time to wait between updates of the progress display, measured in milliseconds.
static int	dkconfig_progress_display_width The number of columns of progress information to display.
static boolean	dkconfig_quiet Boolean.
static boolean	dkconfig_show_stack_trace If true, show stack traces for errors such as file format errors.
static boolean	dkconfig_suppressSplitterErrors When true compilation errors during splitter file generation will not be reported to the user.
static boolean	dkconfig_undo_opts Boolean.
static boolean	dkconfig_use_dynamic_constant_optimization Whether to use the dynamic constants optimization.
static String	files_from_SWITCH
static String	format_SWITCH
static String	help_SWITCH
static boolean	ignore_comparability
static File	inv_file
static boolean	invariants_check_canBeMissing
static boolean	invariants_check_canBeMissing_arrayelt
static boolean	isInferencing Whether Daikon is in its inferencing loop.
static String	lineSep
static String	list_type_SWITCH
static String	mem_stat_SWITCH
static String	no_dataflow_hierarchy_SWITCH
static String	no_show_progress_SWITCH
static boolean	no_text_output
static String	no_text_output_SWITCH
static boolean	noversion_output Whether Daikon should print its version number and date.
static String	noversion_SWITCH
static boolean	omit_from_output When true, omit certain invariants from the output .inv file.
static String	omit_from_output_SWITCH
static boolean[]	omit_types An array of flags, indexed by characters, in which a true entry means that invariants of that sort should be omitted from the output .inv file.
static OutputFormat	output_format
static boolean	output_num_samples
static String	output_num_samples_SWITCH
static String	ppt_max_name If set, only ppts less than ppt_max_name are included.
static Pattern	ppt_omit_regexp
static String	ppt_omit_regexp_SWITCH
static Pattern	ppt_regexp
static String	ppt_regexp_SWITCH
static String	progress Human-friendly progress status message.
static ArrayList<Invariant>	proto_invs
static String	release_date
static String	release_string
static String	release_version
static File	server_dir
static String	server_SWITCH
static boolean	show_progress
static String	show_progress_SWITCH
static boolean	suppress_implied_controlled_invariants Whether to use the bottom up implementation of the dataflow hierarchy.
static boolean	suppress_implied_postcondition_over_prestate_invariants
static boolean	suppress_redundant_invariants_with_simplify
static String	suppress_redundant_SWITCH
static String	track_SWITCH
static boolean	use_dataflow_hierarchy Whether to associate the program points in a dataflow hierarchy, as via Nimmer's thesis.
static boolean	use_equality_optimization Whether to use the "new" equality set mechanism for handling equality, using canonicals to have instantiation of invariants only over equality sets.
static boolean	using_DaikonSimple Boolean.
static Pattern	var_omit_regexp
static String	var_omit_regexp_SWITCH
static Pattern	var_regexp
static String	var_regexp_SWITCH

Method Summary

static void	cleanup() Cleans up static variables so that mainHelper can be called more than once.
static void	create_combined_exits(PptMap ppts) Create EXIT program points as needed for EXITnn program points.
static void	create_splitters(Set<File> spinfo_files)
static void	createUpperPpts(PptMap all_ppts) Creates upper program points by merging together the invariants from all of the lower points.
static void	init_ppt(PptTopLevel ppt, PptMap all_ppts) Create combined exit points, setup splitters, and add orig and derived variables,
static void	main(String[] args) The arguments to daikon.Daikon are file names.
static void	mainHelper(String[] args) This does the work of main, but it never calls System.exit, so it is appropriate to be called progrmmatically.
static void	ppt_stats(PptMap all_ppts) Print out basic statistics (samples, invariants, variables, etc) about each ppt
protected static Daikon.FileOptions	read_options(String[] args, String usage)
static void	setup_NISuppression() Initialize NIS suppression
static void	setup_proto_invs() Creates the list of prototype invariants for all Daikon invariants.
static void	setup_splitters(PptTopLevel ppt) Sets up splitting on all ppts.
static void	setupEquality(PptTopLevel ppt) Initialize the equality sets for each variable
static void	undoOpts(PptMap all_ppts) Undoes the invariants suppressed for the dynamic constant, suppression and equality set optimizations (should yield the same invariants as the simple incremental algorithm

Methods inherited from class Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

dkconfig_progress_delay

public static int dkconfig_progress_delay

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.

dkconfig_show_stack_trace

public static boolean dkconfig_show_stack_trace

If true, show stack traces for errors such as file format errors.

release_version

public static final String release_version

See Also:

Constant Field Values

release_date

public static final String release_date

See Also:

Constant Field Values

release_string

public static final String release_string

See Also:

Constant Field Values

dkconfig_output_conditionals

public static boolean dkconfig_output_conditionals

Boolean. Controls whether conditional program points are displayed.

dkconfig_enable_floats

public static boolean dkconfig_enable_floats

Boolean. Controls whether invariants are reported over floating-point values.

dkconfig_calc_possible_invs

public static boolean dkconfig_calc_possible_invs

Boolean. Just print the total number of possible invariants and exit.

dkconfig_ppt_perc

public static int dkconfig_ppt_perc

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.

dkconfig_print_sample_totals

public static boolean dkconfig_print_sample_totals

Boolean. Controls whether or not the total samples read and processed are printed at the end of processing.

lineSep

public static final String lineSep

dkconfig_disable_splitting

public static boolean dkconfig_disable_splitting

Boolean. Controls whether or not splitting based on the built-in splitting rules is 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.

dkconfig_quiet

public static boolean dkconfig_quiet

Boolean. Controls whether or not processing information is printed out. Setting this variable to true also automatically sets progress_delay to -1.

check_program_types

public static final boolean check_program_types

See Also:

Constant Field Values

invariants_check_canBeMissing

public static final boolean invariants_check_canBeMissing

See Also:

Constant Field Values

invariants_check_canBeMissing_arrayelt

public static final boolean invariants_check_canBeMissing_arrayelt

See Also:

Constant Field Values

disable_modbit_check_message

public static final boolean disable_modbit_check_message

See Also:

Constant Field Values

disable_modbit_check_error

public static final boolean disable_modbit_check_error

See Also:

Constant Field Values

no_text_output

public static boolean no_text_output

show_progress

public static boolean show_progress

use_equality_optimization

public static boolean use_equality_optimization

Whether to use the "new" equality set mechanism for handling equality, using canonicals to have instantiation of invariants only over equality sets.

dkconfig_use_dynamic_constant_optimization

public static boolean dkconfig_use_dynamic_constant_optimization

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.

dkconfig_undo_opts

public static boolean dkconfig_undo_opts

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.

using_DaikonSimple

public static boolean using_DaikonSimple

Boolean. Indicates to Daikon classes and methods that the methods calls should be compatible to DaikonSimple because Daikon and DaikonSimple share methods. Default value is 'false'.

dkconfig_guardNulls

public static String dkconfig_guardNulls

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).

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 (@pxref{Variable names}).) @cindex nonsensical values for variables, guarding

dkconfig_suppressSplitterErrors

public static boolean dkconfig_suppressSplitterErrors

When true compilation errors during splitter file generation will not be reported to the user.

use_dataflow_hierarchy

public static boolean use_dataflow_hierarchy

Whether to associate the program points in a dataflow hierarchy, as via Nimmer's thesis. Deactivate only for languages and analyses where flow relation is nonsensical.

suppress_implied_controlled_invariants

public static boolean suppress_implied_controlled_invariants

Whether to use the bottom up implementation of the dataflow hierarchy. This mechanism builds invariants initially only at the leaves of the partial order. Upper points are calculated by joining the invariants from each of their children points.

suppress_implied_postcondition_over_prestate_invariants

public static boolean suppress_implied_postcondition_over_prestate_invariants

suppress_redundant_invariants_with_simplify

public static boolean suppress_redundant_invariants_with_simplify

output_format

public static OutputFormat output_format

output_num_samples

public static boolean output_num_samples

ignore_comparability

public static boolean ignore_comparability

ppt_regexp

public static Pattern ppt_regexp

ppt_omit_regexp

public static Pattern ppt_omit_regexp

var_regexp

public static Pattern var_regexp

var_omit_regexp

public static Pattern var_omit_regexp

dkconfig_internal_check

public static boolean dkconfig_internal_check

When true, perform detailed internal checking. These are essentially additional, possibly costly assert statements.

ppt_max_name

public static String ppt_max_name

If set, only ppts less than ppt_max_name are included. Used by the configuration option dkconfig_ppt_percent to only work on a specified percent of the ppts.

inv_file

public static File inv_file

noversion_output

public static boolean noversion_output

Whether Daikon should print its version number and date.

isInferencing

public static boolean isInferencing

Whether Daikon is in its inferencing loop. Used only for assertion checks.

omit_from_output

public static boolean omit_from_output

When true, omit certain invariants from the output .inv file. Generally these are invariants that wouldn't be printed in any case; but by default, they're retained in the .inv file in case they would be useful for later processing. (For instance, we might at some point in the future support resuming processing with more data from an .inv file). These invariants can increase the size of the .inv file, though, so when only limited further processing is needed, it can save space to omit them.

omit_types

public static boolean[] omit_types

An array of flags, indexed by characters, in which a true entry means that invariants of that sort should be omitted from the output .inv file.

help_SWITCH

public static final String help_SWITCH

See Also:

Constant Field Values

no_text_output_SWITCH

public static final String no_text_output_SWITCH

See Also:

Constant Field Values

format_SWITCH

public static final String format_SWITCH

See Also:

Constant Field Values

show_progress_SWITCH

public static final String show_progress_SWITCH

See Also:

Constant Field Values

no_show_progress_SWITCH

public static final String no_show_progress_SWITCH

See Also:

Constant Field Values

noversion_SWITCH

public static final String noversion_SWITCH

See Also:

Constant Field Values

output_num_samples_SWITCH

public static final String output_num_samples_SWITCH

See Also:

Constant Field Values

files_from_SWITCH

public static final String files_from_SWITCH

See Also:

Constant Field Values

omit_from_output_SWITCH

public static final String omit_from_output_SWITCH

See Also:

Constant Field Values

conf_limit_SWITCH

public static final String conf_limit_SWITCH

See Also:

Constant Field Values

list_type_SWITCH

public static final String list_type_SWITCH

See Also:

Constant Field Values

no_dataflow_hierarchy_SWITCH

public static final String no_dataflow_hierarchy_SWITCH

See Also:

Constant Field Values

suppress_redundant_SWITCH

public static final String suppress_redundant_SWITCH

See Also:

Constant Field Values

ppt_regexp_SWITCH

public static final String ppt_regexp_SWITCH

See Also:

Constant Field Values

ppt_omit_regexp_SWITCH

public static final String ppt_omit_regexp_SWITCH

See Also:

Constant Field Values

var_regexp_SWITCH

public static final String var_regexp_SWITCH

See Also:

Constant Field Values

var_omit_regexp_SWITCH

public static final String var_omit_regexp_SWITCH

See Also:

Constant Field Values

server_SWITCH

public static final String server_SWITCH

See Also:

Constant Field Values

config_SWITCH

public static final String config_SWITCH

See Also:

Constant Field Values

config_option_SWITCH

public static final String config_option_SWITCH

See Also:

Constant Field Values

debugAll_SWITCH

public static final String debugAll_SWITCH

See Also:

Constant Field Values

debug_SWITCH

public static final String debug_SWITCH

See Also:

Constant Field Values

track_SWITCH

public static final String track_SWITCH

See Also:

Constant Field Values

disc_reason_SWITCH

public static final String disc_reason_SWITCH

See Also:

Constant Field Values

mem_stat_SWITCH

public static final String mem_stat_SWITCH

See Also:

Constant Field Values

server_dir

public static File server_dir

all_ppts

public static PptMap all_ppts

current_inv

public static Invariant current_inv

current invariant (used for debugging)

proto_invs

public static ArrayList<Invariant> proto_invs

debugTrace

public static final Logger debugTrace

Debug tracer.

debugProgress

public static final Logger debugProgress

debugEquality

public static final Logger debugEquality

debugInit

public static final Logger debugInit

Debug tracer for ppt initialization.

debugStats

public static final Logger debugStats

Prints out statistics concerning equality sets, suppressions, etc.

dkconfig_progress_display_width

public static int dkconfig_progress_display_width

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.

progress

public static String progress

Human-friendly progress status message. If fileio_progress is non-null, then this is ignored. So this is primarily for progress reports that are not IO-related.

Method Detail

main

public static void main(String[] args)

The arguments to daikon.Daikon are file names. Declaration file names end in ".decls", and data trace file names end in ".dtrace".

mainHelper

public static void mainHelper(String[] args)

This does the work of main, but it never calls System.exit, so it is appropriate to be called progrmmatically. Termination of the program with a message to the user is indicated by throwing TerminationMessage.

See Also:

main(String[]), Daikon.TerminationMessage

cleanup

public static void cleanup()

Cleans up static variables so that mainHelper can be called more than once.

read_options

protected static Daikon.FileOptions read_options(String[] args,
                                                 String usage)

setup_proto_invs

public static void setup_proto_invs()

Creates the list of prototype invariants for all Daikon invariants. New invariants must be added to this list

createUpperPpts

public static void createUpperPpts(PptMap all_ppts)

Creates upper program points by merging together the invariants from all of the lower points.

init_ppt

public static void init_ppt(PptTopLevel ppt,
                            PptMap all_ppts)

Create combined exit points, setup splitters, and add orig and derived variables,

create_combined_exits

public static void create_combined_exits(PptMap ppts)

Create EXIT program points as needed for EXITnn program points.

setup_splitters

public static void setup_splitters(PptTopLevel ppt)

Sets up splitting on all ppts. Currently only binary splitters over boolean returns or exactly two return statements are enabled by default (though other splitters can be defined by the user)

ppt_stats

public static void ppt_stats(PptMap all_ppts)

Print out basic statistics (samples, invariants, variables, etc) about each ppt

setup_NISuppression

public static void setup_NISuppression()

Initialize NIS suppression

setupEquality

public static void setupEquality(PptTopLevel ppt)

Initialize the equality sets for each variable

create_splitters

public static void create_splitters(Set<File> spinfo_files)
                             throws IOException

Throws:

IOException

undoOpts

public static void undoOpts(PptMap all_ppts)

Undoes the invariants suppressed for the dynamic constant, suppression and equality set optimizations (should yield the same invariants as the simple incremental algorithm