daikon.inv.binary.twoScalar
Class NumericInt

Object
  Invariant
      BinaryInvariant
          TwoScalar
              NumericInt

All Implemented Interfaces:

Serializable, Cloneable

Direct Known Subclasses:

NumericInt.BitwiseAndZero, NumericInt.BitwiseComplement, NumericInt.BitwiseSubset, NumericInt.Divides, NumericInt.ShiftZero, NumericInt.Square, NumericInt.ZeroTrack

public abstract class NumericInt
extends TwoScalar

Baseclass for binary numeric invariants. Each specific invariant is implemented in a subclass (typically, in this file). The subclass must provide the methods instantiate(), check(), and format(). Symmetric functions should define is_symmetric() to return true.

See Also:

Serialized Form

Nested Class Summary

static class	NumericInt.BitwiseAndZero Represents the BitwiseAnd == 0 invariant between two long scalars; that is, x and y have no bits in common.
static class	NumericInt.BitwiseComplement Represents the bitwise complement invariant between two long scalars.
static class	NumericInt.BitwiseSubset Represents the bitwise subset invariant between two long scalars; that is, the bits of y are a subset of the bits of x.
static class	NumericInt.Divides Represents the divides without remainder invariant between two long scalars.
static class	NumericInt.ShiftZero Represents the ShiftZero invariant between two long scalars; that is, x right-shifted by y is always zero.
static class	NumericInt.Square Represents the square invariant between two long scalars.
static class	NumericInt.ZeroTrack Represents the zero tracks invariant between two long scalars; that is, when x is zero, y is also zero.

Nested classes/interfaces inherited from class Invariant

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

Field Summary

protected static NISuppressor	var1_eq_0
protected static NISuppressor	var1_eq_1
protected static NISuppressor	var1_eq_minus_1
protected static NISuppressor	var1_eq_var2
protected static NISuppressor	var1_ge_0
protected static NISuppressor	var1_le_var2
protected static NISuppressor	var1_ne_0
protected static NISuppressor	var2_eq_0
protected static NISuppressor	var2_eq_1
protected static NISuppressor	var2_eq_minus_1
protected static NISuppressor	var2_eq_var1
protected static NISuppressor	var2_ge_0
protected static NISuppressor	var2_ne_0
protected static NISuppressor	var2_valid_shift

Fields inherited from class TwoScalar

swap

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, isGuardingPredicate, min_mod_non_missing_samples, ppt, PROBABILITY_JUSTIFIED, PROBABILITY_NEVER, PROBABILITY_UNJUSTIFIED

Constructor Summary

protected	NumericInt(boolean swap)
protected	NumericInt(PptSlice ppt, boolean swap)

Method Summary

InvariantStatus	check_modified(long x, long y, int count) Calls the function specific equal check and returns the correct status.
abstract boolean	eq_check(long x, long y) Returns true if x and y don't invalidate the invariant.
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()
boolean	instantiate_ok(VarInfo[] vis) Returns true if it is ok to instantiate a numeric invariant over the specified slice.
DiscardInfo	is_subscript(VarInfo[] vis) Checks to see if 'x[a] op y[b]' where 'x[] op y[]' and 'a == b'.
boolean	isExact() Subclasses should override.
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.
InvDef[][]	obvious_checks(VarInfo[] vis) Returns an array of arrays of antecedents.
String	repr() Returns a representation of the class.

Methods inherited from class TwoScalar

add_modified, add_unmodified, add, check_unmodified, check, computeConfidence, get_swap, isSameFormula, resurrect_done_swapped, resurrect_done_unswapped, resurrect_done, valid_types, var1, var1, var2, var2

Methods inherited from class BinaryInvariant

add_unordered, check_unordered, find, is_symmetric

Methods inherited from class Invariant

add_sample, asInvClass, clear_falsified, clone_and_permute, clone, conf_is_ge, confidence_and, confidence_and, confidence_or, createGuardedInvariant, createGuardingPredicate, enabled, enoughSamples, falsify, find, format_too_few_samples, format_unimplemented, format, formatFuzzy, get_comparability, get_ni_suppressions, getConfidence, getGuardingList, getGuardingList, hasUninterestingConstant, instantiate_dyn, instantiate, is_false, is_ni_suppressed, isActive, isAllPrestate, isExclusiveFormula, isInteresting, isObvious, isObviousDynamically_SomeInEquality, isObviousDynamically_SomeInEqualityHelper, isObviousDynamically, isObviousStatically_AllInEquality, isObviousStatically_SomeInEquality, isObviousStatically_SomeInEqualityHelper, isObviousStatically, isObviousStatically, 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_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

Field Detail

var1_eq_0

protected static NISuppressor var1_eq_0

var2_eq_0

protected static NISuppressor var2_eq_0

var1_ge_0

protected static NISuppressor var1_ge_0

var2_ge_0

protected static NISuppressor var2_ge_0

var1_eq_1

protected static NISuppressor var1_eq_1

var2_eq_1

protected static NISuppressor var2_eq_1

var1_eq_minus_1

protected static NISuppressor var1_eq_minus_1

var2_eq_minus_1

protected static NISuppressor var2_eq_minus_1

var1_ne_0

protected static NISuppressor var1_ne_0

var2_ne_0

protected static NISuppressor var2_ne_0

var1_le_var2

protected static NISuppressor var1_le_var2

var1_eq_var2

protected static NISuppressor var1_eq_var2

var2_eq_var1

protected static NISuppressor var2_eq_var1

var2_valid_shift

protected static NISuppressor var2_valid_shift

Constructor Detail

NumericInt

protected NumericInt(PptSlice ppt,
                     boolean swap)

NumericInt

protected NumericInt(boolean swap)

Method Detail

instantiate_ok

public boolean instantiate_ok(VarInfo[] vis)

Returns true if it is ok to instantiate a numeric invariant over the specified slice.

Overrides:

instantiate_ok in class Invariant

See Also:

Invariant.valid_types(VarInfo[])

isExact

public boolean isExact()

Description copied from class: Invariant

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.

Overrides:

isExact in class Invariant

repr

public String repr()

Description copied from class: TwoScalar

Returns a representation of the class. This includes the classname, variables, and swap state.

Overrides:

repr in class TwoScalar

format_using

public String format_using(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 %varN% 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,
                                      long y,
                                      int count)

Calls the function specific equal check and returns the correct status.

Specified by:

check_modified in class TwoScalar

is_subscript

public DiscardInfo is_subscript(VarInfo[] vis)

Checks to see if 'x[a] op y[b]' where 'x[] op y[]' and 'a == b'. Doesn't catch the case where a = b+1.

isObviousDynamically

public 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

get_format_str

public abstract String get_format_str(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,
                                 long y)

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

obvious_checks

public InvDef[][] obvious_checks(VarInfo[] vis)

Returns an array of arrays of antecedents. If all of the antecedents in any array are true, then the invariant is obvious.

get_proto_all

public static List<Invariant> get_proto_all()