Package daikon

Class PrintInvariants

  • public final class PrintInvariants
extends Object
    PrintInvariants prints a set of invariants from a .inv file. For documentation, see section "Printing Invariants" in the Daikon manual. Invoke the program as follows: 
    java daikon.PrintInvariants [flags] inv-file
    For a list of cammand-line options, pass the "-h" flag to this program.

    • Field Detail

      • dkconfig_replace_prestate

        public static boolean dkconfig_replace_prestate
        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

      • dkconfig_print_inv_class

        public static boolean dkconfig_print_inv_class
        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.

      • dkconfig_print_all

        public static boolean dkconfig_print_all
        If true, print all invariants without any filtering.

      • dkconfig_true_inv_cnt

        public static boolean dkconfig_true_inv_cnt
        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.

      • dkconfig_remove_post_vars

        public static boolean dkconfig_remove_post_vars
        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.

      • dkconfig_old_array_names

        public static boolean dkconfig_old_array_names
        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.

      • dkconfig_static_const_infer

        public static boolean dkconfig_static_const_infer
        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.

      • dkconfig_print_implementer_entry_ppts

        public static boolean dkconfig_print_implementer_entry_ppts
        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.

      • debug

        public static final Logger debug
        Main debug tracer for PrintInvariants (for things unrelated to printing).

      • debugRepr

        public static final Logger debugRepr
        Debug tracer for printing.

      • debugPrintModified

        public static final Logger debugPrintModified
        Debug tracer for printing modified variables in ESC/JML/DBC output.

      • debugBound

        public static final Logger debugBound
        Debug tracer for variable bound information.

      • print_discarded_invariants

        public static boolean print_discarded_invariants
        Switch for whether to print discarded Invariants or not, default is false. True iff --disc_reason switch was supplied on the command line.

      • wrap_xml

        public static boolean wrap_xml
        If true, then each invariant is printed using the current OutputFormat, but it's wrapped inside xml tags, along with other information about the invariant. For example, if this switch is true and if the output format is JAVA, and the invariant prints as "x == null", the results of print_invariant would look something like: 
        
 <INVINFO>
 <INV> x == null </INV>
 <SAMPLES> 100 </SAMPLES>
 <DAIKON> x == null </DAIKON>
 <DAIKONCLASS> daikon.inv.unary.scalar.NonZero </DAIKONCLASS>
 <METHOD> foo() </METHOD>
 </INVINFO>
        The above output is actually all in one line, although in this comment it's broken up into multiple lines for clarity.

        Note the extra information printed with the invariant: the number of samples from which the invariant was derived, the daikon representation (i.e. the Daikon output format), the Java class that the invariant corresponds to, and the method that the invariant belongs to ("null" for object invariants).

    • Method Detail

      • resetPrestateExpressions

        public static void resetPrestateExpressions()
        See dkconfig_replace_prestate.

        Resets the prestate expression mapping. This is done between printing of each different program point.

      • addPrestateExpression

        public static String addPrestateExpression​(String expr)
        See dkconfig_replace_prestate.

        Return the variable name corresponding to expr. Create a new varname and an expr → varname mapping if there is not already one.

      • print_reasons

        public static void print_reasons​(PptMap ppts)
        Prints out all the discardCodes and discardStrings of the Invariants that will not be printed if the --disc_reason command-line option is used.

      • validateGuardNulls

        public static void validateGuardNulls()
        Validate guardNulls config option.

      • discReasonSetup

        public static void discReasonSetup​(String arg)
        Method used to setup fields if the --disc_reason command-line option is used if (arg==null) then show all discarded Invariants, otherwise just show the ones specified in arg, where arg = class-name<var1,var2,...>@ppt.name e.g.: OneOf<x>@foo():::ENTER would only show OneOf Invariants that involve x at the program point foo:::ENTER (any of the 3 params can be omitted, e.g. OneOf@foo:::ENTER)
        Throws:
        IllegalArgumentException - if arg is not of the proper syntax

      • print_invariants

        @RequiresNonNull("FileIO.new_decl_format")
public static void print_invariants​(PptMap all_ppts)

      • print_invariants_maybe

        @RequiresNonNull("FileIO.new_decl_format")
public static void print_invariants_maybe​(PptTopLevel ppt,
                                          PrintWriter out,
                                          PptMap all_ppts)
        Print invariants for a single program point and its conditionals. Does no output if no samples or no views.

      • print_sample_data

        @RequiresNonNull("FileIO.new_decl_format")
public static void print_sample_data​(PptTopLevel ppt,
                                     PrintWriter out)
        Prints the program point name. If Daikon.output_num_samples is enabled, prints the number of samples for the specified ppt. Also prints all of the variables for the ppt if Daikon.output_num_samples is enabled or the format is ESCJAVA, JML, or DBCJAVA.

      • count_global_stats

        public static void count_global_stats​(PptTopLevel ppt)
        Count statistics (via Global) on variables (canonical, missing, etc.)

      • parse_csharp_invariant_variable

        public static String parse_csharp_invariant_variable​(VarInfo varInfo,
                                                     boolean sort)
        Parses the variables from varInfo.
        Parameters:
        varInfo - the Daikon variable representation to parse
        sort - true to parse as a grouping variable, false to parse as a filtering variable
        Returns:
        the parsed variable string

      • get_csharp_invariant_variables

        public static void get_csharp_invariant_variables​(VarInfo[] vars,
                                                  Set<String> variables,
                                                  boolean sort)
        Parses the variables from vars.
        Parameters:
        vars - an array of Daikon variable representations
        variables - the set to store the parsed variables
        sort - true to parse as group variables, false to parse as filtering variables

      • get_csharp_invariant_variables

        public static void get_csharp_invariant_variables​(Invariant invariant,
                                                  Set<String> variables,
                                                  boolean group)
        Parses the invariant variables of invariant and stores them in variables If group is true the invariant's grouping variables are parsed (the variables which the invariant is grouped by in the contract list view). If group is false the invariant's filtering variables are parsed (the variables for which this invariant can be filtered by). In the case of implications, only variables on the right side of the implication are parsed.
        Parameters:
        invariant - the invariant to parse
        variables - the set to store the parsed variables
        group - true to parse group variables, false to parse filtering variables

      • get_csharp_inv_type

        public static String get_csharp_inv_type​(Invariant invariant)
        Gets the invariant type string (i.e. daikon.inv.binary.inv) of a Daikon invariant.
        Parameters:
        invariant - the Daikon invariant
        Returns:
        the invariant type string of the invariant

      • print_invariants

        @RequiresNonNull("FileIO.new_decl_format")
public static void print_invariants​(PptTopLevel ppt,
                                    PrintWriter out,
                                    PptMap ppt_map)
        Print invariants for a single program point, once we know that this ppt is worth printing.

      • print_all_ternary_invs

        public static void print_all_ternary_invs​(PptMap all_ppts)
        Prints all invariants for ternary slices (organized by slice) and all of the unary and binary invariants over the same variables. The purpose of this is to look for possible ni-suppressions. It's not intended as a normal output mechanism.

      • print_all_invs

        public static void print_all_invs​(@Nullable PptSlice slice,
                                  String indent)
        Prints all of the invariants in the specified slice.

      • print_true_inv_cnt

        @RequiresNonNull({"daikon.suppress.NIS.all_suppressions","daikon.suppress.NIS.suppressor_map"})
public static void print_true_inv_cnt​(PptMap ppts)