Package daikon.inv.unary.stringsequence
Class OneOfStringSequence
- Object
-
- Invariant
-
- UnaryInvariant
-
- SingleStringSequence
-
- OneOfStringSequence
-
- All Implemented Interfaces:
OneOf
,Serializable
,Cloneable
public final class OneOfStringSequence extends SingleStringSequence implements OneOf
Represents String[] variables that take on only a few distinct values. Prints as eitherx == c
(when there is only one value) or asx one of {c1, c2, c3}
(when there are multiple values).- See Also:
- Serialized Form
-
-
Nested Class Summary
-
Nested classes/interfaces inherited from class Invariant
Invariant.ClassVarnameComparator, Invariant.ClassVarnameFormulaComparator, Invariant.InvariantComparatorForPrinting, Invariant.Match
-
-
Field Summary
Fields Modifier and Type Field Description static Logger
debug
Debugging logger.static boolean
dkconfig_enabled
Boolean.static int
dkconfig_size
Positive integer.-
Fields inherited from class Invariant
checkedMergeOverridden, CONFIDENCE_JUSTIFIED, CONFIDENCE_NEVER, CONFIDENCE_UNJUSTIFIED, 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
-
-
Method Summary
All Methods Static Methods Instance Methods Concrete Methods Modifier and Type Method Description InvariantStatus
add_mod_elem(@Interned String @Interned [] v, int count)
Adds a single sample to the invariant.InvariantStatus
add_modified(@Interned String @Interned [] a, int count)
Similar toSingleStringSequence.check_modified(java.lang.String[], int)
except that it can change the state of the invariant if necessary.InvariantStatus
check_mod_elem(@Interned String @Interned [] v, int count)
Checks a single sample to the invariant.InvariantStatus
check_modified(@Interned String @Interned [] a, int count)
Presents a sample to the invariant.OneOfStringSequence
clone()
Do nothing special, Overridden to remove exception from declaration.boolean
compare_rep(int num_other_elts, @Interned String @Interned [][] other_elts)
protected double
computeConfidence()
This method computes the confidence that this invariant occurred by chance.Object
elt()
The single value represented by the OneOf invariant.Object
elt(int index)
boolean
enabled()
Returns whether or not this class of invariants is currently enabled.static @Nullable OneOfStringSequence
find(PptSlice ppt)
String
format_csharp_contract()
String
format_daikon()
String
format_esc()
String
format_java_family(OutputFormat format)
String
format_simplify()
String
format_using(OutputFormat format)
Return a printed representation of this invariant, in the given format.static OneOfStringSequence
get_proto()
Returns the prototype invariant for OneOfStringSequenceboolean
hasUninterestingConstant()
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.OneOfStringSequence
instantiate_dyn(PptSlice slice)
Instantiates (creates) an invariant of the same class on the specified slice.boolean
is_boolean()
boolean
is_hashcode()
boolean
isExact()
Subclasses should override.boolean
isExclusiveFormula(Invariant o)
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)
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.@Nullable 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
isSameFormula(Invariant o)
Returns true iff the two invariants represent the same mathematical formula.boolean
isValidEscExpression()
Returns a conjuction of mapping the same function of our expresssions's VarInfos, in general.@Interned String @Interned []
max_elt()
@Nullable OneOfStringSequence
merge(List<Invariant> invs, PptSlice parent_ppt)
Merge the invariants in invs to form a new invariant.boolean
mergeFormulasOk()
Oneof can merge different formulas from lower points to create a single formula at an upper point.@Interned String @Interned []
min_elt()
int
num_elts()
The number of elements in the OneOf invariant.String
repr()
For printing invariants, there are two interfaces: repr gives a low-level representation (Invariant.repr_prob()
also prints the confidence), andInvariant.format()
gives a high-level representation for user output.void
set_one_of_val(@Interned String[][] vals)
Setup the invariant with the specified elements.boolean
state_match(Object state)
Returns true if every element in this invariant is contained in the specified state.-
Methods inherited from class SingleStringSequence
add, add_unmodified, check, check_unmodified, valid_types, var
-
Methods inherited from class UnaryInvariant
resurrect_done
-
Methods inherited from class Invariant
add_sample, asInvClass, checkRep, clear_falsified, clone_and_permute, conf_is_ge, confidence_and, confidence_and, confidence_or, createGuardedInvariant, createGuardingPredicate, enoughSamples, falsify, find, format, format_classname, format_too_few_samples, format_unimplemented, formatFuzzy, get_comparability, get_ni_suppressions, getConfidence, getGuardingList, getGuardingList, instantiate, instantiate_ok, is_false, is_ni_suppressed, isActive, isAllPrestate, isEqualityComparison, isObvious, isObviousDynamically, isObviousDynamically_SomeInEquality, isObviousDynamically_SomeInEqualityHelper, isObviousStatically, isObviousStatically_AllInEquality, isObviousStatically_SomeInEquality, isObviousStatically_SomeInEqualityHelper, isReflexive, isSameInvariant, isValidExpression, isWorthPrinting, justified, log, log, logDetail, logOn, match, permute, prob_and, prob_and, prob_is_ge, prob_or, repCheck, repr_prob, resurrect, simplify_format_double, simplify_format_long, simplify_format_string, toString, toString, transfer, usesVar, usesVar, usesVarDerived, varNames
-
-
-
-
Field Detail
-
dkconfig_enabled
public static boolean dkconfig_enabled
Boolean. True iff OneOf invariants should be considered.
-
dkconfig_size
public static int dkconfig_size
Positive integer. Specifies the maximum set size for this type of invariant (x is one ofsize
items).
-
-
Method Detail
-
get_proto
public static OneOfStringSequence get_proto()
Returns the prototype invariant for OneOfStringSequence
-
enabled
public boolean enabled()
Description copied from class:Invariant
Returns whether or not this class of invariants is currently enabled.Its implementation is almost always
return dkconfig_enabled;
.
-
instantiate_dyn
public OneOfStringSequence instantiate_dyn( OneOfStringSequence this, PptSlice slice)
Description copied from class:Invariant
Instantiates (creates) an invariant of the same class on the specified slice. Must be overridden in each class. Must be used rather thanInvariant.clone()
so that checks inInvariant.instantiate(daikon.PptSlice)
for reasonable invariants are done.The implementation of this method is almost always
return new <em>InvName</em>(slice);
- Specified by:
instantiate_dyn
in classInvariant
- Returns:
- the new invariant
-
is_boolean
@Pure public boolean is_boolean(@GuardSatisfied OneOfStringSequence this)
-
is_hashcode
@Pure public boolean is_hashcode(@GuardSatisfied OneOfStringSequence this)
-
clone
@SideEffectFree public OneOfStringSequence clone(@GuardSatisfied OneOfStringSequence this)
Description copied from class:Invariant
Do nothing special, Overridden to remove exception from declaration.
-
num_elts
public int num_elts()
Description copied from interface:OneOf
The number of elements in the OneOf invariant.
-
elt
public Object elt()
Description copied from interface:OneOf
The single value represented by the OneOf invariant. Throws an error if not exactly one value is represented by this.
-
compare_rep
public boolean compare_rep(int num_other_elts, @Interned String @Interned [][] other_elts)
-
repr
public String repr(@GuardSatisfied OneOfStringSequence this)
Description copied from class:Invariant
For printing invariants, there are two interfaces: repr gives a low-level representation (Invariant.repr_prob()
also prints the confidence), andInvariant.format()
gives a high-level representation for user output.
-
format_using
@SideEffectFree public String format_using(@GuardSatisfied OneOfStringSequence this, OutputFormat format)
Description copied from class:Invariant
Return a printed representation of this invariant, in the given format.- Specified by:
format_using
in classInvariant
-
format_daikon
public String format_daikon(@GuardSatisfied OneOfStringSequence this)
-
isValidEscExpression
@Pure public boolean isValidEscExpression()
Description copied from class:Invariant
Returns a 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.- Overrides:
isValidEscExpression
in classInvariant
- Returns:
- conjuction of mapping the same function of our expresssions's VarInfos
- See Also:
VarInfo.isValidEscExpression()
-
format_esc
public String format_esc(@GuardSatisfied OneOfStringSequence this)
-
format_csharp_contract
public String format_csharp_contract(@GuardSatisfied OneOfStringSequence this)
-
format_java_family
public String format_java_family(@GuardSatisfied OneOfStringSequence this, OutputFormat format)
-
format_simplify
public String format_simplify(@GuardSatisfied OneOfStringSequence this)
-
add_modified
public InvariantStatus add_modified(@Interned String @Interned [] a, int count)
Description copied from class:SingleStringSequence
Similar toSingleStringSequence.check_modified(java.lang.String[], 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 callSingleStringSequence.check_modified(java.lang.String[], int)
. This method need not check for falsification; that is done by the caller.- Specified by:
add_modified
in classSingleStringSequence
-
check_modified
public InvariantStatus check_modified(@Interned String @Interned [] a, int count)
Description copied from class:SingleStringSequence
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 classSingleStringSequence
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_mod_elem
public InvariantStatus add_mod_elem(@Interned String @Interned [] v, int count)
Adds a single sample to the invariant. Returns the appropriate InvariantStatus from the result of adding the sample to this.
-
check_mod_elem
public InvariantStatus check_mod_elem(@Interned String @Interned [] v, int count)
Checks a single sample to the invariant. Returns the appropriate InvariantStatus from the result of adding the sample to this.
-
computeConfidence
protected double computeConfidence()
Description copied from class:Invariant
This method computes the confidence that this invariant occurred by chance. Clients should callInvariant.getConfidence()
instead.This method need not check the value of field "falsified", as the caller does that.
- Specified by:
computeConfidence
in classInvariant
- Returns:
- confidence of this invariant
- See Also:
Invariant.getConfidence()
-
isObviousStatically
@Pure public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis)
Description copied from class:Invariant
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
- Overrides:
isObviousStatically
in classInvariant
- 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.
-
isObviousDynamically
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 classInvariant
-
mergeFormulasOk
public boolean mergeFormulasOk()
Oneof can merge different formulas from lower points to create a single formula at an upper point.- Overrides:
mergeFormulasOk
in classInvariant
- Returns:
- true if invariants with different formulas can be merged
-
isSameFormula
@Pure public boolean isSameFormula(Invariant o)
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 classInvariant
- Parameters:
o
- 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 o)
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 classInvariant
- Parameters:
o
- the other invariant to compare to this one- Returns:
- true iff the two invariants represent mutually exclusive mathematical formulas
-
hasUninterestingConstant
public boolean hasUninterestingConstant()
Description copied from class:Invariant
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.- Overrides:
hasUninterestingConstant
in classInvariant
-
isExact
@Pure 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.
-
find
public static @Nullable OneOfStringSequence find(PptSlice ppt)
-
merge
public @Nullable OneOfStringSequence merge(List<Invariant> invs, PptSlice parent_ppt)
Merge the invariants in invs to form a new invariant. Each must be a OneOfStringSequence invariant. This code finds all of the oneof values from each of the invariants and returns the merged invariant (if any).- Overrides:
merge
in classInvariant
- 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
-
set_one_of_val
public void set_one_of_val(@Interned String[][] vals)
Setup the invariant with the specified elements. Normally used when searching for a specified OneOf. The elements of vals are not necessarily interned; this method interns each element.
-
state_match
public boolean state_match(Object state)
Returns true if every element in this invariant is contained in the specified state. For example if x = 1 and the state contains 1 and 2, true will be returned.- Overrides:
state_match
in classInvariant
-
-