Package daikon.inv.binary.twoSequence

Class PairwiseLinearBinary

  • All Implemented Interfaces:
    Serializable, Cloneable
    public class PairwiseLinearBinary
extends TwoSequence
    Represents a linear invariant (i.e., y = ax + b) between the corresponding elements of two sequences of long values. Each (x[i], y[i]) pair is examined. Thus, x[0] is compared to y[0], x[1] to y[1] and so forth. Prints as y[] = a * x[] + b.
    See Also:
    Serialized Form

    • Method Detail

      • enabled

        public boolean enabled()
        Returns whether or not this invariant is enabled.
        Specified by:
        enabled in class Invariant

      • clone

        @SideEffectFree
public PairwiseLinearBinary clone​(@GuardSatisfied PairwiseLinearBinary this)
        Description copied from class: Invariant
        Do nothing special, Overridden to remove exception from declaration.
        Overrides:
        clone in class Invariant

      • repr

        public String repr​(@GuardSatisfied PairwiseLinearBinary this)
        Description copied from class: TwoSequence
        Returns a representation of the class. This includes the classname, variables, and swap state.
        Overrides:
        repr in class TwoSequence
        Returns:
        a string representation of this

      • check_modified

        public InvariantStatus check_modified​(long @Interned [] x_arr,
                                      long @Interned [] y_arr,
                                      int count)
        Description copied from class: TwoSequence
        Presents a sample to the invariant. Returns whether the sample is consistent with the invariant. Does not change the state of the invariant.
        Specified by:
        check_modified in class TwoSequence
        count - how many identical samples were observed in a row. For example, three calls to check_modified with a count parameter of 1 is equivalent to one call to check_modified with a count parameter of 3.
        Returns:
        whether or not the sample is consistent with the invariant

      • isSameFormula

        @Pure
public boolean isSameFormula​(Invariant other)
        Description copied from class: TwoSequence
        Return true if both invariants are the same class and the order of the variables (swap) is the same.
        Overrides:
        isSameFormula in class TwoSequence
        Parameters:
        other - the invariant to compare to this one
        Returns:
        true iff the two invariants represent the same mathematical formula. Does not consider

      • isExclusiveFormula

        @Pure
public boolean isExclusiveFormula​(Invariant other)
        Description copied from class: Invariant
        Returns true iff the two invariants represent mutually exclusive mathematical formulas -- that is, if one of them is true, then the other must be false. This method does not consider the context such as variable names, confidences, sample counts, value counts, or related quantities.
        Overrides:
        isExclusiveFormula in class Invariant
        Parameters:
        other - the other invariant to compare to this one
        Returns:
        true iff the two invariants represent mutually exclusive mathematical formulas

      • isObviousDynamically

        @Pure
public @Nullable DiscardInfo isObviousDynamically​(VarInfo[] vis)
        Description copied from class: Invariant
        Return non-null if this invariant is necessarily true from a fact that can be determined dynamically (after checking data) -- for the given varInfos rather than the varInfos of this. Conceptually, this means, "Is this invariant dynamically obvious if its VarInfos were switched with vis?" Intended to be overriden by subclasses so they can filter invariants after checking; the overriding method should first call "super.isObviousDynamically(vis)". Since this method is dynamic, it should only be called after all processing.
        Overrides:
        isObviousDynamically in class Invariant

      • isActive

        @Pure
public boolean isActive()
        Description copied from class: Invariant
        Returns whether or not the invariant is currently active. This is used to identify those invariants that require a certain number of points before they actually do computation (eg, LinearBinary)

        This is used during suppresion. Any invariant that is not active cannot suppress another invariant.

        Overrides:
        isActive in class Invariant
        Returns:
        true if this invariant is currently active

      • mergeFormulasOk

        public boolean mergeFormulasOk()
        Description copied from class: Invariant
        Returns whether or not it is possible to merge invariants of the same class but with different formulas when combining invariants from lower ppts to build invariants at upper program points. Invariants that have this characteristic (eg, bound, oneof) should override this function. Note that invariants that can do this, normally need special merge code as well (to merge the different formulas into a single formula at the upper point.
        Overrides:
        mergeFormulasOk in class Invariant
        Returns:
        true if invariants with different formulas can be merged

      • merge

        public @Nullable Invariant merge​(List<Invariant> invs,
                                 PptSlice parent_ppt)
        Merge the invariants in invs to form a new invariant. Each must be a PairwiseLinearBinary invariant. The work is done by the LinearBinary core
        Overrides:
        merge in class Invariant
        Parameters:
        invs - list of invariants to merge. They should all be permuted to match the variable order in parent_ppt.
        parent_ppt - slice that will contain the new invariant
        Returns:
        the merged invariant or null if the invariants didn't represent the same invariant