Package daikon.inv.unary.scalar

Class RangeInt

Object

Invariant

UnaryInvariant

SingleScalar

RangeInt

All Implemented Interfaces:

Serializable, Cloneable

Direct Known Subclasses:

RangeInt.BooleanVal, RangeInt.Bound0_63, RangeInt.EqualMinusOne, RangeInt.EqualOne, RangeInt.EqualZero, RangeInt.Even, RangeInt.GreaterEqual64, RangeInt.GreaterEqualZero, RangeInt.PowerOfTwo

public abstract class RangeInt
extends SingleScalar

Baseclass for unary range based invariants. Each invariant is a special stateless version of bound or oneof. For example EqualZero, BooleanVal, etc). These are never printed, but are used internally as suppressors for ni-suppressions. Each specific invariant is implemented in a subclass (typically in this file).

See Also:

Serialized Form

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static class	RangeInt.BooleanVal	Internal invariant representing longs whose values are always 0 or 1.
static class	RangeInt.Bound0_63	Internal invariant representing longs whose values are between 0 and 63.
static class	RangeInt.EqualMinusOne	Internal invariant representing long scalars that are equal to minus one.
static class	RangeInt.EqualOne	Internal invariant representing long scalars that are equal to one.
static class	RangeInt.EqualZero	Internal invariant representing long scalars that are equal to zero.
static class	RangeInt.Even	Invariant representing longs whose values are always even.
static class	RangeInt.GreaterEqual64	Internal invariant representing long scalars that are greater than or equal to 64.
static class	RangeInt.GreaterEqualZero	Internal invariant representing long scalars that are greater than or equal to 0.
static class	RangeInt.PowerOfTwo	Invariant representing longs whose values are always a power of 2 (exactly one bit is set).

Nested classes/interfaces inherited from class Invariant

Invariant.ClassVarnameComparator, Invariant.ClassVarnameFormulaComparator, Invariant.InvariantComparatorForPrinting, Invariant.Match

Field Summary

Fields inherited from class Invariant

CONFIDENCE_JUSTIFIED, CONFIDENCE_NEVER, CONFIDENCE_UNJUSTIFIED, debug, debugFlow, debugGuarding, debugIsObvious, debugIsWorthPrinting, debugPrint, debugPrintEquality, dkconfig_confidence_limit, dkconfig_fuzzy_ratio, dkconfig_simplify_define_predicates, falsified, invariantEnabledDefault, isGuardingPredicate, min_mod_non_missing_samples, ppt, PROBABILITY_JUSTIFIED, PROBABILITY_NEVER, PROBABILITY_UNJUSTIFIED

Constructor Summary

Constructors

Modifier	Constructor	Description
protected	RangeInt()
protected	RangeInt(PptSlice ppt)

Method Summary

Modifier and Type	Method	Description
InvariantStatus	add_modified(long x, int count)	Similar to SingleScalar.check_modified(long, int) except that it can change the state of the invariant if necessary.
InvariantStatus	check_modified(long x, int count)	Presents a sample to the invariant.
protected double	computeConfidence()	This method computes the confidence that this invariant occurred by chance.
abstract boolean	eq_check(long x)	Returns true if x and y don't invalidate the invariant.
protected @Nullable OneOfScalar	find_oneof(VarInfo[] vis)	Looks for a OneOf invariant over vis.
String	format_using(OutputFormat format)	Returns a string in the specified format that describes the invariant.
abstract String	get_format_str(OutputFormat format)	Return a format string for the specified output format.
static List<Invariant>	get_proto_all()	Returns a list of prototypes of all of the range invariants.
boolean	instantiate_ok(VarInfo[] vis)	Check that instantiation is ok.
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.
@Nullable DiscardInfo	isObviousDynamically(VarInfo[] vis)	All range invariants except Even and PowerOfTwo are obvious since they represented by some version of OneOf or Bound.
boolean	isSameFormula(Invariant other)	Returns true iff the two invariants represent the same mathematical formula.

Methods inherited from class SingleScalar

add, add_unmodified, check, check_unmodified, valid_types, valid_types_static, var

Methods inherited from class UnaryInvariant

resurrect_done

Methods inherited from class Invariant

add_sample, asInvClass, checkRep, clear_falsified, clone, clone_and_permute, conf_is_ge, confidence_and, confidence_and, confidence_or, createGuardedInvariant, createGuardingPredicate, enabled, enoughSamples, falsify, find, format, format_classname, format_too_few_samples, format_unimplemented, formatFuzzy, get_comparability, get_ni_suppressions, getConfidence, getGuardingList, getGuardingList, hasUninterestingConstant, instantiate, instantiate_dyn, is_false, is_ni_suppressed, isActive, isAllPrestate, isEqualityComparison, isExact, isObvious, isObviousDynamically, isObviousDynamically_SomeInEquality, isObviousDynamically_SomeInEqualityHelper, isObviousStatically, isObviousStatically, isObviousStatically_AllInEquality, isObviousStatically_SomeInEquality, isObviousStatically_SomeInEqualityHelper, isReflexive, isSameInvariant, isValidEscExpression, isValidExpression, isWorthPrinting, justified, log, log, logDetail, logOn, match, merge, mergeFormulasOk, permute, prob_and, prob_and, prob_is_ge, prob_or, repCheck, repr, repr_prob, resurrect, simplify_format_double, simplify_format_long, simplify_format_string, state_match, toString, toString, transfer, usesVar, usesVar, usesVarDerived, varNames

Methods inherited from class Object

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

Constructor Detail

RangeInt

protected RangeInt(PptSlice ppt)

RangeInt

protected RangeInt()

Method Detail

instantiate_ok

public boolean instantiate_ok(VarInfo[] vis)

Check that instantiation is ok. The type must be integral (not boolean or hash code).

Overrides:

instantiate_ok in class Invariant

See Also:

Invariant.valid_types(VarInfo[])

format_using

@SideEffectFree
public String format_using(@GuardSatisfied RangeInt this,
                           OutputFormat format)

Returns a string in the specified format that describes the invariant. The generic format string is obtained from the subclass specific get_format_str(). Instances of %var1% are replaced by the variable name in the specified format.

Specified by:

format_using in class Invariant

check_modified

public InvariantStatus check_modified(long x,
                                      int count)

Description copied from class: SingleScalar

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 SingleScalar

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

add_modified

public InvariantStatus add_modified(long x,
                                    int count)

Description copied from class: SingleScalar

Similar to SingleScalar.check_modified(long, int) except that it can change the state of the invariant if necessary. If the invariant doesn't have any state, then the implementation should simply call SingleScalar.check_modified(long, int). This method need not check for falsification; that is done by the caller.

Specified by:

add_modified in class SingleScalar

computeConfidence

protected double computeConfidence()

Description copied from class: Invariant

This method computes the confidence that this invariant occurred by chance. Clients should call Invariant.getConfidence() instead.

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

Specified by:

computeConfidence in class Invariant

Returns:

confidence of this invariant

See Also:

Invariant.getConfidence()

isSameFormula

@Pure
public boolean isSameFormula(Invariant other)

Description copied from class: Invariant

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.

Specified by:

isSameFormula in class Invariant

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)

All range invariants except Even and PowerOfTwo are obvious since they represented by some version of OneOf or Bound.

Overrides:

isObviousDynamically in class Invariant

find_oneof

protected @Nullable OneOfScalar find_oneof(VarInfo[] vis)

Looks for a OneOf invariant over vis. Used by Even and PowerOfTwo to dynamically suppress those invariants if a OneOf exists.

get_format_str

public abstract String get_format_str(@GuardSatisfied RangeInt this,
                                      OutputFormat format)

Return a format string for the specified output format. Each instance of %varN% will be replaced by the correct name for varN.

eq_check

public abstract boolean eq_check(long x)

Returns true if x and y don't invalidate the invariant.

get_proto_all

public static List<Invariant> get_proto_all()

Returns a list of prototypes of all of the range invariants.