Package daikon.derive

Class Derivation

  • All Implemented Interfaces:
    Serializable, Cloneable
    Direct Known Subclasses:
    BinaryDerivation, TernaryDerivation, UnaryDerivation
    public abstract class Derivation
extends Object
implements Serializable, Cloneable
    Structure that represents a derivation; can generate values and derived variables from base variables. A Derivation has a set of base VarInfo from which the Derivation is derived. Use getVarInfo() to get the VarInfo representation of this Derivation. When we want the actual value of this derivation, we pass in a ValueTuple; the Derivation picks out the values of its base variables and finds the value of the derived variable. Use computeValueandModified() to get value. Derivations are created by DerivationFactory.
    See Also:
    Serialized Form

    • Field Detail

      • dkconfig_disable_derived_variables

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

      • debug

        public static final Logger debug
        Debug tracer.

    • Method Detail

      • getBases

        @SideEffectFree
public abstract VarInfo[] getBases()
        Returns array of the VarInfos this was derived from.
        Returns:
        array of the VarInfos this was derived from

      • getBase

        @Pure
public abstract VarInfo getBase​(int i)
        Returns the ith VarInfo this was derived from.
        Parameters:
        i - index into the array of Varinfos this was derived from
        Returns:
        the ith VarInfo this was derived from

      • computeValueAndModified

        public abstract ValueAndModified computeValueAndModified​(ValueTuple full_vt)
        Returns a pair of: the derived value and whether the variable counts as modified.
        Parameters:
        full_vt - the set of values in a program point that will be used to derive the value
        Returns:
        a pair of: the derived value and whether the variable counts as modified

      • getVarInfo

        public VarInfo getVarInfo()
        Get the VarInfo that this would represent. However, the VarInfo can't be used to obtain values without further modification -- use computeValueAndModified() for this.
        Returns:
        the VarInfo hat this would represent
        See Also:
        computeValueAndModified(daikon.ValueTuple)

      • makeVarInfo

        protected abstract VarInfo makeVarInfo()
        Used by all child classes to actually create the VarInfo this represents, after which it is interned for getVarInfo().

      • isParam

        @Pure
protected abstract boolean isParam()

      • missingOutOfBounds

        public boolean missingOutOfBounds()
        True if we have encountered to date any missing values in this derivation due to array indices being out of bounds. This can happen with both simple subscripts and subsequences. Note that this becomes true as we are running, it cannot be set in advance (which would require a first pass).

      • derivedDepth

        public abstract int derivedDepth()
        Returns how many levels of derivation this Derivation is based on. The depth counts this as well as the depths of its bases.

      • isSameFormula

        @Pure
public abstract boolean isSameFormula​(Derivation other)
        Returns true iff other and this represent the same derivation (modulo the variable they are applied to). Default implentation will just checks run-time type, but subclasses with state (e.g. SequenceInitial index) should match that, too.
        Parameters:
        other - the Derivation to compare to
        Returns:
        true iff other and this represent the same derivation

      • get_lower_bound

        public Quantify.Term get_lower_bound()
        Returns the lower bound of a slice. Throws an error if this is not a slice. Slices should override.

      • get_upper_bound

        public Quantify.Term get_upper_bound()
        Returns the lower bound of a slice. Throws an error if this is not a slice. Slices should override.

      • get_array_var

        public VarInfo get_array_var()
        Returns the array variable that underlies this slice. Throws an error if this is not a slice. Slices should override.

      • esc_name

        @SideEffectFree
public String esc_name​(String index)
        Returns the name of this variable in ESC format. If an index is specified, it is used as an array index. It is an error to specify an index on a non-array variable.

      • jml_name

        public String jml_name​(String index)
        Returns the name of this variable in JML format. If an index is specified, it is used as an array index. It is an error to specify an index on a non-array variable.

      • csharp_name

        @SideEffectFree
public String csharp_name​(String index)
        Returns the name of this variable in CSHARPCONTRACT format. If an index is specified, it is used as an array index. It is an error to specify an index on a non-array variable.

      • simplify_name

        @SideEffectFree
public String simplify_name()
        Returns the name of this variable in simplify format.

      • is_prestate_version

        @Pure
public boolean is_prestate_version​(Derivation d)
        Returns true if d is the prestate version of this. Returns true if this and d are of the same derivation with the same formula and have the same bases.

      • complexity

        public int complexity()
        Return the complexity of this derivation. This is only for the derivation itself and not for the variables included in the derivation. The default implementation returns 1 (which is the added complexity of an derivation). Subclasses that add additional complexity (such as an offset) should override.

      • shift_str

        protected String shift_str​(int shift)
        Returns a string that corresponds to the specified shift.
        Parameters:
        shift - how much to shift the string
        Returns:
        the shifted string

      • inside_esc_name

        protected String inside_esc_name​(VarInfo vi,
                                 boolean in_orig,
                                 int shift)
        Returns the esc name of a variable which is included inside an expression (such as orig(a[vi])). If the expression is orig, the orig is implied for this variable.

      • inside_jml_name

        protected String inside_jml_name​(VarInfo vi,
                                 boolean in_orig,
                                 int shift)
        Returns the jml name of a variable which is included inside an expression (such as orig(a[vi])). If the expression is orig, the orig is implied for this variable.

      • inside_csharp_name

        protected String inside_csharp_name​(VarInfo vi,
                                    boolean in_orig,
                                    int shift)
        Returns the csharp name of a variable which is included inside an expression (such as orig(a[vi])). If the expression is orig, the orig is implied for this variable.