daikon.inv
Class Invariant

Object
  Invariant

All Implemented Interfaces:

Serializable, Cloneable

Direct Known Subclasses:

BinaryInvariant, DiffDummyInvariant, DummyInvariant, Equality, Joiner, TernaryInvariant, UnaryInvariant

public abstract class Invariant
extends Object
implements Serializable, Cloneable

Base implementation for Invariant objects. Intended to be subclassed but not to be directly instantiated. Rules/assumptions for invariants:

For each program point's set of VarInfos, there exists exactly no more than one invariant of its type. For example, between variables a and b at PptTopLevel T, there will not be two instances of invariant I(a, b).

See Also:

Serialized Form

Nested Class Summary

static class	Invariant.ClassVarnameComparator
static class	Invariant.ClassVarnameFormulaComparator Orders invariants by class, then variable names, then formula.
static class	Invariant.InvariantComparatorForPrinting Compare based on arity, then printed representation.
static class	Invariant.Match Class used as a key to store invariants in a MAP where their equality depends on the invariant representing the same invariant (i.e., their class is the same) and the same internal state (when multiple invariants with the same class are possible) Note that this is based on the Invariant type (i.e., class) and the internal state and not on what ppt the invariant is in or what variables it is over.

Field Summary

static double	CONFIDENCE_JUSTIFIED The probability that this could have happened by chance alone.
static double	CONFIDENCE_NEVER -1 = delete this invariant; we know it's not true
static double	CONFIDENCE_UNJUSTIFIED (0..1) = greater to lesser likelihood of coincidence 0 = must have happened by chance
static Logger	debug General debug tracer.
static Logger	debugFlow Debug tracer for invariant flow.
static Logger	debugGuarding Debug tracer for guarding.
static Logger	debugIsObvious Debug tracer for isObvious checks.
static Logger	debugIsWorthPrinting Debug tracer for isWorthPrinting() checks.
static Logger	debugPrint Debug tracer for printing invariants.
static Logger	debugPrintEquality Debug tracer for printing equality invariants.
static double	dkconfig_confidence_limit Floating-point number between 0 and 1.
static double	dkconfig_fuzzy_ratio Floating-point number between 0 and 0.1, representing the maximum relative difference between two floats for fuzzy comparisons.
static boolean	dkconfig_simplify_define_predicates A boolean value.
protected boolean	falsified True exactly if the invariant has been falsified: it is guaranteed never to hold (and should be either in the process of being destroyed or about to be destroyed.
boolean	isGuardingPredicate
static int	min_mod_non_missing_samples At least this many samples are required, or else we don't report any invariant at all.
PptSlice	ppt The program point for this invariant; includes values, number of samples, VarInfos, etc.
static double	PROBABILITY_JUSTIFIED The probability that this could have happened by chance alone.
static double	PROBABILITY_NEVER 3 = delete this invariant; we know it's not true
static double	PROBABILITY_UNJUSTIFIED (0..1) = lesser to greater likelihood of coincidence 1 = must have happened by chance

Constructor Summary

protected	Invariant()
protected	Invariant(PptSlice ppt)

Method Summary

InvariantStatus	add_sample(ValueTuple vt, int count) Adds the specified sample to the invariant and returns the result.
static Class<? extends Invariant>	asInvClass(Object x)
void	clear_falsified() Clear the falsified flag.
Invariant	clone_and_permute(int[] permutation) Clones the invariant and then permutes it as specified.
Invariant	clone() Do nothing special, Overridden to remove exception from declaration
protected abstract double	computeConfidence() This method computes the confidence that this invariant occurred by chance.
static double	conf_is_ge(double x, double goal) Return Invariant.CONFIDENCE_JUSTIFIED if x≥goal.
static double	confidence_and(double c1, double c2) Return the confidence that both conditions are satisfied.
static double	confidence_and(double c1, double c2, double c3) Return the confidence that all three conditions are satisfied.
static double	confidence_or(double c1, double c2) Return the confidence that either condition is satisfied.
Invariant	createGuardedInvariant(boolean install) This procedure guards one invariant and returns the resulting guarded invariant (implication), without placing it in any slice and without modifying the original invariant.
Invariant	createGuardingPredicate(boolean install) Create a guarding predicate for a given invariant.
boolean	enabled() Returns whether or not this class of invariants are currently enabled
boolean	enoughSamples()
void	falsify() Marks the invariant as falsified.
static Invariant	find(Class<? extends Invariant> invclass, PptSlice ppt) Look up a previously instantiated Invariant.
String	format_too_few_samples(OutputFormat request, String attempt)
String	format_unimplemented(OutputFormat request)
abstract String	format_using(OutputFormat format)
String	format() For printing invariants, there are two interfaces: repr gives a low-level representation (repr_prop also prints the confidence), and format gives a high-level representation for user output.
static String	formatFuzzy(String method, VarInfo v1, VarInfo v2, OutputFormat format) Used throught Java family formatting of invariants.
VarComparability	get_comparability() Returns a single VarComparability that describes the set of variables used by this invariant.
NISuppressionSet	get_ni_suppressions() Returns the set of non-instantiating suppressions for this invariant.
double	getConfidence() Given that this invariant has been true for all values seen so far, this method returns the confidence that that situation has occurred by chance alone.
List<VarInfo>	getGuardingList()
static List<VarInfo>	getGuardingList(VarInfo[] varInfos)
boolean	hasUninterestingConstant() This is the test that's planned to replace the poorly specified "isInteresting" check.
protected Invariant	instantiate_dyn(PptSlice slice) Instantiates an invariant of the same class on the specified slice.
boolean	instantiate_ok(VarInfo[] vis) Checks to see if the invariant can reasonably be instantiated over the specified variables.
Invariant	instantiate(PptSlice slice) Instantiates this invariant over the specified slice.
boolean	is_false() Returns whether or not this invariant has been destroyed.
boolean	is_ni_suppressed() Returns whether or not this invariant is ni-suppressed.
boolean	isActive() Returns whether or not the invariant is currently active.
boolean	isAllPrestate()
boolean	isExact() Subclasses should override.
boolean	isExclusiveFormula(Invariant other)
boolean	isInteresting()
DiscardInfo	isObvious() Return true if this invariant is necessarily true from a fact that can be determined statically (i.e., the decls files) or dynamically (after checking data).
DiscardInfo	isObviousDynamically_SomeInEquality() Return true if this invariant and some equality combinations of its member variables are dynamically obvious.
protected DiscardInfo	isObviousDynamically_SomeInEqualityHelper(VarInfo[] vis, VarInfo[] assigned, int position) Recurse through vis (an array of leaders) and generate the cartesian product of their equality sets; in other words, every combination of one element from each equality set.
DiscardInfo	isObviousDynamically() Return true if this invariant is necessarily true from a fact that can be determined dynamically (after checking data).
DiscardInfo	isObviousDynamically(VarInfo[] vis) 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.
boolean	isObviousStatically_AllInEquality() Return true if this invariant and all equality combinations of its member variables are necessarily true from a fact that can be determined statically (i.e., the decls files).
DiscardInfo	isObviousStatically_SomeInEquality() Return true if this invariant and some equality combinations of its member variables are statically obvious.
protected DiscardInfo	isObviousStatically_SomeInEqualityHelper(VarInfo[] vis, VarInfo[] assigned, int position) Recurse through vis and generate the cartesian product of ...
DiscardInfo	isObviousStatically() Return true if this invariant is necessarily true from a fact that can be determined statically (i.e., the decls files) (e.g., by being from a certain derivation).
DiscardInfo	isObviousStatically(VarInfo[] vis) Return true if this invariant is necessarily true from a fact that can be determined statically -- for the given varInfos rather than the varInfos of this.
boolean	isReflexive() Return true if more than one of the variables in the invariant are the same variable.
boolean	isSameFormula(Invariant other)
boolean	isSameInvariant(Invariant inv2)
boolean	isValidEscExpression()
boolean	isValidExpression(OutputFormat format)
boolean	isWorthPrinting()
boolean	justified() A wrapper around getConfidence() or getConfidence().
void	log(Logger log, String msg) Logs a description of the invariant and the specified msg via the logger as described in Debug.log(Logger, Class, Ppt, VarInfo[], String).
boolean	log(String format, Object... args) Logs a description of the invariant and the specified msg via the logger as described in Debug.log(Logger, Class, Ppt, VarInfo[], String).
static boolean	logDetail() Returns whether or not detailed logging is on.
static boolean	logOn() Returns whether or not logging is on.
boolean	match(Invariant inv) Returns whether or not two invariants are of the same type.
Invariant	merge(List<Invariant> invs, PptSlice parent_ppt) Merge the invariants in invs to form a new invariant.
boolean	mergeFormulasOk() 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.
Invariant	permute(int[] permutation) Permutes the invariant as specified.
static double	prob_and(double p1, double p2) Return the probability that both conditions are satisfied.
static double	prob_and(double p1, double p2, double p3) Return the probability that all three conditions are satisfied.
static double	prob_is_ge(double x, double goal) Return Invariant.PROBABILITY_JUSTIFIED if x≥goal.
static double	prob_or(double p1, double p2) Return the probability that either condition is satisfied.
void	repCheck() Check the rep invariants of this.
String	repr_prob() For printing invariants, there are two interfaces: repr gives a low-level representation (repr_prop also prints the confidence), and format gives a high-level representation for user output.
String	repr() For printing invariants, there are two interfaces: repr gives a low-level representation (repr_prop also prints the confidence), and format gives a high-level representation for user output.
protected abstract Invariant	resurrect_done(int[] permutation) Called on the new invariant just before resurrect() returns it to allow subclasses to fix any information they might have cached from the old Ppt and VarInfos.
Invariant	resurrect(PptSlice new_ppt, int[] permutation) Take a falsified invariant and resurrect it in a new PptSlice.
static String	simplify_format_double(double d) Convert a floating point value into the weird Modula-3-like floating point format that the Simplify tool requires.
static String	simplify_format_long(long l) Conver a long integer value into a format that Simplify can use.
static String	simplify_format_string(String s) Convert a string value into the weird |-quoted format that the Simplify tool requires.
boolean	state_match(Object state) Returns whether or not the invariant matches the specified state.
String	toString()
static String	toString(Invariant[] invs)
Invariant	transfer(PptSlice new_ppt, int[] permutation) Take an invariant and transfer it into a new PptSlice.
boolean	usesVar(String name)
boolean	usesVar(VarInfo vi)
boolean	usesVarDerived(String name)
boolean	valid_types(VarInfo[] vis) Returns whether or not the invariant is valid over the basic types in vis.
String	varNames() Return a string representation of the variable names.

Methods inherited from class Object

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

Field Detail

debug

public static final Logger debug

General debug tracer.

debugPrint

public static final Logger debugPrint

Debug tracer for printing invariants.

debugFlow

public static final Logger debugFlow

Debug tracer for invariant flow.

debugPrintEquality

public static final Logger debugPrintEquality

Debug tracer for printing equality invariants.

debugIsWorthPrinting

public static final Logger debugIsWorthPrinting

Debug tracer for isWorthPrinting() checks.

debugGuarding

public static final Logger debugGuarding

Debug tracer for guarding.

debugIsObvious

public static final Logger debugIsObvious

Debug tracer for isObvious checks.

dkconfig_confidence_limit

public static double dkconfig_confidence_limit

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 --conf_limit switch to Daikon; refer to manual.)

dkconfig_simplify_define_predicates

public static boolean dkconfig_simplify_define_predicates

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.

dkconfig_fuzzy_ratio

public static double dkconfig_fuzzy_ratio

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.

ppt

public PptSlice ppt

The program point for this invariant; includes values, number of samples, VarInfos, etc. Can be null for a "prototype" invariant.

falsified

protected boolean falsified

True exactly if the invariant has been falsified: it is guaranteed never to hold (and should be either in the process of being destroyed or about to be destroyed. This should never be set directly; instead, call destroy().

isGuardingPredicate

public boolean isGuardingPredicate

CONFIDENCE_JUSTIFIED

public static final double CONFIDENCE_JUSTIFIED

The probability that this could have happened by chance alone.
1 = could never have happened by chance; that is, we are fully confident that this invariant is a real invariant

See Also:

Constant Field Values

CONFIDENCE_UNJUSTIFIED

public static final double CONFIDENCE_UNJUSTIFIED

(0..1) = greater to lesser likelihood of coincidence
0 = must have happened by chance

See Also:

Constant Field Values

CONFIDENCE_NEVER

public static final double CONFIDENCE_NEVER

-1 = delete this invariant; we know it's not true

See Also:

Constant Field Values

PROBABILITY_JUSTIFIED

public static final double PROBABILITY_JUSTIFIED

The probability that this could have happened by chance alone.
0 = could never have happened by chance; that is, we are fully confident that this invariant is a real invariant

See Also:

Constant Field Values

PROBABILITY_UNJUSTIFIED

public static final double PROBABILITY_UNJUSTIFIED

(0..1) = lesser to greater likelihood of coincidence
1 = must have happened by chance

See Also:

Constant Field Values

PROBABILITY_NEVER

public static final double PROBABILITY_NEVER

3 = delete this invariant; we know it's not true

See Also:

Constant Field Values

min_mod_non_missing_samples

public static final int min_mod_non_missing_samples

At least this many samples are required, or else we don't report any invariant at all. (Except that OneOf invariants are treated differently.)

See Also:

Constant Field Values

Constructor Detail

Invariant

protected Invariant(PptSlice ppt)

Invariant

protected Invariant()

Method Detail

conf_is_ge

public static final double conf_is_ge(double x,
                                      double goal)

Return Invariant.CONFIDENCE_JUSTIFIED if x≥goal. Return Invariant.CONFIDENCE_UNJUSTIFIED if x≤1. For intermediate inputs, the result gives confidence that grades between the two extremes. See the discussion of gradual vs. sudden confidence transitions.

prob_is_ge

public static final double prob_is_ge(double x,
                                      double goal)

Return Invariant.PROBABILITY_JUSTIFIED if x≥goal. Return Invariant.PROBABILITY_UNJUSTIFIED if x≤1. For intermediate inputs, the result gives probability that grades between the two extremes. See the discussion of gradual vs. sudden probability transitions.

confidence_and

public static final double confidence_and(double c1,
                                          double c2)

Return the confidence that both conditions are satisfied.

confidence_and

public static final double confidence_and(double c1,
                                          double c2,
                                          double c3)

Return the confidence that all three conditions are satisfied.

confidence_or

public static final double confidence_or(double c1,
                                         double c2)

Return the confidence that either condition is satisfied.

prob_and

public static final double prob_and(double p1,
                                    double p2)

Return the probability that both conditions are satisfied.

prob_and

public static final double prob_and(double p1,
                                    double p2,
                                    double p3)

Return the probability that all three conditions are satisfied.

prob_or

public static final double prob_or(double p1,
                                   double p2)

Return the probability that either condition is satisfied.

enoughSamples

public boolean enoughSamples()

Returns:

true if the invariant has enough samples to have its computed constants well-formed. Is overridden in classes like LinearBinary/Ternary and Upper/LowerBound.

justified

public final boolean justified()

A wrapper around getConfidence() or getConfidence().

getConfidence

public final double getConfidence()

Given that this invariant has been true for all values seen so far, this method returns the confidence that that situation has occurred by chance alone. The result is a value between 0 and 1 inclusive. 0 means that this invariant could never have occurred by chance alone; we are fully confident that its truth is no coincidence. 1 means that the invariant is certainly a happenstance, so the truth of the invariant is not relevant and it should not be reported. Values between 0 and 1 give differing confidences in the invariant.

As an example, if the invariant is "x!=0", and only one value, 22, has been seen for x, then the conclusion "x!=0" is not justified. But if there have been 1,000,000 values, and none of them were 0, then we may be confident that the property "x!=0" is not a coincidence.

This method need not check the value of field "falsified", as the caller does that.

This method is a wrapper around computeConfidence(), which does the actual work.

See Also:

computeConfidence()

computeConfidence

protected abstract double computeConfidence()

This method computes the confidence that this invariant occurred by chance. Users should use getConfidence() instead.

See Also:

getConfidence()

isExact

public boolean isExact()

Subclasses should override. An exact invariant indicates that given all but one variable value, the last one can be computed. (I think that's correct, anyway.) Examples are IntComparison (when only equality is possible), LinearBinary, FunctionUnary. OneOf is treated differently, as an interface. The result of this method does not depend on whether the invariant is justified, destroyed, etc.

falsify

public void falsify()

Marks the invariant as falsified. Should always be called rather than just setting the flag so that we can track when this happens

clear_falsified

public void clear_falsified()

Clear the falsified flag.

is_false

public boolean is_false()

Returns whether or not this invariant has been destroyed.

clone

public Invariant clone()

Do nothing special, Overridden to remove exception from declaration

Overrides:

clone in class Object

transfer

public Invariant transfer(PptSlice new_ppt,
                          int[] permutation)

Take an invariant and transfer it into a new PptSlice.

Parameters:

new_ppt - must have the same arity and types

permutation - gives the varinfo array index mapping in the new ppt

clone_and_permute

public Invariant clone_and_permute(int[] permutation)

Clones the invariant and then permutes it as specified. Normally used to make child invariant match the variable order of the parent when merging invariants bottom up.

resurrect

public Invariant resurrect(PptSlice new_ppt,
                           int[] permutation)

Take a falsified invariant and resurrect it in a new PptSlice.

Parameters:

new_ppt - must have the same arity and types

permutation - gives the varinfo array index mapping

get_comparability

public VarComparability get_comparability()

Returns a single VarComparability that describes the set of variables used by this invariant. Since all of the variables in an invariant must be comparable, this can usually be the comparability information for any variable. The exception is when one or more variables is always comparable (comparable to everythign else). An always comparable VarComparability is returned only if all of the variables involved are always comparable. Otherwise the comparability information from one of the non always-comparable variables is returned.

merge

public Invariant merge(List<Invariant> invs,
                       PptSlice parent_ppt)

Merge the invariants in invs to form a new invariant. This implementation merely returns a clone of the first invariant in the list. This is correct for simple invariants whose equation or statistics don't depend on the actual samples seen. It should be overriden for more complex invariants (eg, bound, oneof, linearbinary, etc).

Parameters:

invs - List of invariants to merge. The invariants must all be of the same type and should come from the children of parent_ppt. They should also 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.

permute

public Invariant permute(int[] permutation)

Permutes the invariant as specified. Often creates a new invariant (with a different class)

resurrect_done

protected abstract Invariant resurrect_done(int[] permutation)

Called on the new invariant just before resurrect() returns it to allow subclasses to fix any information they might have cached from the old Ppt and VarInfos.

usesVar

public boolean usesVar(VarInfo vi)

usesVar

public boolean usesVar(String name)

usesVarDerived

public boolean usesVarDerived(String name)

varNames

public final String varNames()

Return a string representation of the variable names.

repr

public String repr()

For printing invariants, there are two interfaces: repr gives a low-level representation (repr_prop also prints the confidence), and format gives a high-level representation for user output.

repr_prob

public String repr_prob()

For printing invariants, there are two interfaces: repr gives a low-level representation (repr_prop also prints the confidence), and format gives a high-level representation for user output.

format

public String format()

For printing invariants, there are two interfaces: repr gives a low-level representation (repr_prop also prints the confidence), and format gives a high-level representation for user output.

format_using

public abstract String format_using(OutputFormat format)

isValidEscExpression

public boolean isValidEscExpression()

Returns:

conjuction of mapping the same function of our expresssions's VarInfos, in general. Subclasses may override if they are able to handle generally-inexpressible properties in special-case ways.

See Also:

VarInfo.isValidEscExpression()

isValidExpression

public boolean isValidExpression(OutputFormat format)

Returns:

true if this Invariant can be properly formatted for Java output.

format_unimplemented

public String format_unimplemented(OutputFormat request)

Returns:

standard "format needs to be implemented" for the given requested format. Made public so cores can call it.

format_too_few_samples

public String format_too_few_samples(OutputFormat request,
                                     String attempt)

Returns:

standard "too few samples for to have interesting invariant" for the requested format. For machine-readable formats, this is just "true". An optional string argument, if supplied, is a human-readable description of the invariant in its uninformative state, which will be added to the message.

simplify_format_double

public static String simplify_format_double(double d)

Convert a floating point value into the weird Modula-3-like floating point format that the Simplify tool requires.

simplify_format_long

public static String simplify_format_long(long l)

Conver a long integer value into a format that Simplify can use. If the value is too big, we have to print it in a weird way, then tell Simplify about its properties specially.

simplify_format_string

public static String simplify_format_string(String s)

Convert a string value into the weird |-quoted format that the Simplify tool requires. (Note that Simplify doesn't distinguish between variables, symbolic constants, and strings, so we prepend "_string_" to avoid collisions with variables and other symbols).

isSameFormula

public boolean isSameFormula(Invariant other)

Returns:

true iff the two invariants represent the same mathematical formula. Does not consider the context such as variable names, confidences, sample counts, value counts, or related quantities. As a rule of thumb, if two invariants format the same, this method returns true. Furthermore, in many cases, if an invariant does not involve computed constants (as "x>c" and "y=ax+b" do for constants a, b, and c), then this method vacuously returns true.

Throws:

RuntimeException - if other.getClass() != this.getClass()

mergeFormulasOk

public boolean mergeFormulasOk()

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

isSameInvariant

public boolean isSameInvariant(Invariant inv2)

Returns:

true iff the argument is the "same" invariant as this. Same, in this case, means a matching type, formula, and variable names.

isExclusiveFormula

public boolean isExclusiveFormula(Invariant other)

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.

find

public static Invariant find(Class<? extends Invariant> invclass,
                             PptSlice ppt)

Look up a previously instantiated Invariant.

get_ni_suppressions

public NISuppressionSet get_ni_suppressions()

Returns the set of non-instantiating suppressions for this invariant. May return null instead of an empty set. Should be overridden by subclasses with non-instantiating suppressions.

is_ni_suppressed

public boolean is_ni_suppressed()

Returns whether or not this invariant is ni-suppressed.

isWorthPrinting

public boolean isWorthPrinting()

isObviousStatically

public final DiscardInfo isObviousStatically()

Return true if this invariant is necessarily true from a fact that can be determined statically (i.e., the decls files) (e.g., by being from a certain derivation). Intended to be overridden by subclasses.

This method is final because children of Invariant should be extending isObviousStatically(VarInfo[]) because it is more general.

isObviousStatically

public DiscardInfo isObviousStatically(VarInfo[] vis)

Return true if this invariant is necessarily true from a fact that can be determined statically -- for the given varInfos rather than the varInfos of this. Conceptually, this means "is this invariant statically obvious if its VarInfos were switched with vis?" Intended to be overridden by subclasses. Should only do static checking. Precondition: vis.length == this.ppt.var_infos.length

Parameters:

vis - The VarInfos this invariant is obvious over. The position and data type of the variables is the *same* as that of this.ppt.var_infos.

isObviousStatically_AllInEquality

public boolean isObviousStatically_AllInEquality()

Return true if this invariant and all equality combinations of its member variables are necessarily true from a fact that can be determined statically (i.e., the decls files). For example, a == b, and f(a) is obvious, but f(b) is not. In that case, this method on f(a) would return false. If f(b) is also obvious, then this method would return true.

isObviousStatically_SomeInEquality

public DiscardInfo isObviousStatically_SomeInEquality()

Return true if this invariant and some equality combinations of its member variables are statically obvious. For example, if a == b, and f(a) is obvious, then so is f(b). We use the someInEquality (or least interesting) method during printing so we only print an invariant if all its variables are interesting, since a single, static, non interesting occurance means all the equality combinations aren't interesting.

Returns:

the VarInfo array that contains the VarInfos that showed this invariant to be obvious. The contains variables that are elementwise in the same equality set as this.ppt.var_infos. Can be null if no such assignment exists.

isObviousStatically_SomeInEqualityHelper

protected DiscardInfo isObviousStatically_SomeInEqualityHelper(VarInfo[] vis,
                                                               VarInfo[] assigned,
                                                               int position)

Recurse through vis and generate the cartesian product of ...

isObvious

public final DiscardInfo isObvious()

Return true if this invariant is necessarily true from a fact that can be determined statically (i.e., the decls files) or dynamically (after checking data). Intended not to be overriden, because sub-classes should override isObviousStatically or isObviousDynamically. Wherever possible, suppression, rather than this, should do the dynamic checking.

isObviousDynamically

public DiscardInfo isObviousDynamically(VarInfo[] vis)

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.

isReflexive

public boolean isReflexive()

Return true if more than one of the variables in the invariant are the same variable. We create such invariants for the purpose of equality set processing, but they aren't intended for printing; there should be invariants with the same meaning but lower arity instead. For instance, we don't need "x = x + x" because we have "x = 0" instead. Actually, this isn't strictly true: we don't have an invariant "a[] is a palindrome" corresponding to "a[] is the reverse of a[]", for instance.

isObviousDynamically

public final DiscardInfo isObviousDynamically()

Return true if this invariant is necessarily true from a fact that can be determined dynamically (after checking data). Since this method is dynamic, it should only be called after all processing.

This method is final because subclasses should extend isObviousDynamically(VarInfo[]) since that method is more general.

isObviousDynamically_SomeInEquality

public DiscardInfo isObviousDynamically_SomeInEquality()

Return true if this invariant and some equality combinations of its member variables are dynamically obvious. For example, a == b, and f(a) is obvious, so is f(b). We use the someInEquality (or least interesting) method during printing so we only print an invariant if all its variables are interesting, since a single, dynamic, non interesting occurance means all the equality combinations aren't interesting.

Returns:

the VarInfo array that contains the VarInfos that showed this invariant to be obvious. The contains variables that are elementwise in the same equality set as this.ppt.var_infos. Can be null if no such assignment exists.

isObviousDynamically_SomeInEqualityHelper

protected DiscardInfo isObviousDynamically_SomeInEqualityHelper(VarInfo[] vis,
                                                                VarInfo[] assigned,
                                                                int position)

Recurse through vis (an array of leaders) and generate the cartesian product of their equality sets; in other words, every combination of one element from each equality set. For each such combination, test isObviousDynamically; if any test is true, then return that combination. The combinations are generated via recursive calls to this routine.

isAllPrestate

public boolean isAllPrestate()

Returns:

true if this invariant is only over prestate variables .

isInteresting

public boolean isInteresting()

hasUninterestingConstant

public boolean hasUninterestingConstant()

This is the test that's planned to replace the poorly specified "isInteresting" check. In the future, the set of interesting constants might be determined by a static analysis of the source code, but for the moment, we only consider -1, 0, 1, and 2 as interesting. Intuitively, the justification for this test is that an invariant that includes an uninteresting constant (say, "size(x[]) < 237") is likely to be an artifact of the way the program was tested, rather than a statement that would in fact hold over all possible executions.

match

public boolean match(Invariant inv)

Returns whether or not two invariants are of the same type. To be of the same type, invariants must be of the same class. Some invariant classes represent multiple invariants (such as FunctionBinary). They must also be the same formula. Note that invariants with different formulas based on their samples (LinearBinary, Bounds, etc) will still match as long as the mergeFormulaOk() method returns true.

state_match

public boolean state_match(Object state)

Returns whether or not the invariant matches the specified state. Must be overriden by subclasses that support this. Otherwise, it returns true only if the state is null.

createGuardingPredicate

public Invariant createGuardingPredicate(boolean install)

Create a guarding predicate for a given invariant. Returns null if no guarding is needed.

getGuardingList

public List<VarInfo> getGuardingList()

getGuardingList

public static List<VarInfo> getGuardingList(VarInfo[] varInfos)

createGuardedInvariant

public Invariant createGuardedInvariant(boolean install)

This procedure guards one invariant and returns the resulting guarded invariant (implication), without placing it in any slice and without modifying the original invariant. Returns null if the invariant does not need to be guarded.

instantiate_dyn

protected Invariant instantiate_dyn(PptSlice slice)

Instantiates an invariant of the same class on the specified slice. Must be overridden in each class. Must be used rather than clone so that checks in instantiate for reasonable invariants are done.

Returns:

the new invariant

enabled

public boolean enabled()

Returns whether or not this class of invariants are currently enabled

valid_types

public boolean valid_types(VarInfo[] vis)

Returns whether or not the invariant is valid over the basic types in vis. This only checks basic types (scalar, string, array, etc) and should match the basic superclasses of invariant (SingleFloat, SingleScalarSequence, ThreeScalar, etc). More complex checks that depend on variable details can be implemented in instantiate_ok()

See Also:

instantiate_ok(VarInfo[])

instantiate_ok

public boolean instantiate_ok(VarInfo[] vis)

Checks to see if the invariant can reasonably be instantiated over the specified variables. Checks details beyond what is provided by valid_types. This should never be called without calling valid_types first (implementations should be able to presume that valid_types is true).

See Also:

valid_types(VarInfo[])

instantiate

public Invariant instantiate(PptSlice slice)

Instantiates this invariant over the specified slice. The slice must not be null and its variables must be valid for this type of invariant. Returns null if the invariant is not enabled or if the invariant is not reasonable over the specified variables. Otherwise returns the new invariant.

add_sample

public InvariantStatus add_sample(ValueTuple vt,
                                  int count)

Adds the specified sample to the invariant and returns the result.

repCheck

public void repCheck()

Check the rep invariants of this.

isActive

public boolean isActive()

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

logDetail

public static boolean logDetail()

Returns whether or not detailed logging is on. Note that this check is not performed inside the logging calls themselves, it must be performed by the caller.

See Also:

Debug.logDetail(), Debug.logOn(), Debug.log(Logger, Class, Ppt, String)

logOn

public static boolean logOn()

Returns whether or not logging is on.

See Also:

Debug.logOn()

log

public void log(Logger log,
                String msg)

Logs a description of the invariant and the specified msg via the logger as described in Debug.log(Logger, Class, Ppt, VarInfo[], String).

log

public boolean log(String format,
                   Object... args)

Logs a description of the invariant and the specified msg via the logger as described in Debug.log(Logger, Class, Ppt, VarInfo[], String).

Returns:

whether or not it logged anything

toString

public String toString()

Overrides:

toString in class Object

toString

public static String toString(Invariant[] invs)

formatFuzzy

public static String formatFuzzy(String method,
                                 VarInfo v1,
                                 VarInfo v2,
                                 OutputFormat format)

Used throught Java family formatting of invariants. Returns "plume.FuzzyFloat.method(v1_name, v2_name)" Where v1_name and v2_name are the properly formatted varinfos v1 and v2, under the given format. Author: Carlos Pacheco

asInvClass

public static Class<? extends Invariant> asInvClass(Object x)