001package daikon.inv.unary.scalar; 002 003import daikon.PptSlice; 004import daikon.VarInfo; 005import daikon.inv.DiscardInfo; 006import daikon.inv.Invariant; 007import daikon.inv.InvariantStatus; 008import daikon.inv.OutputFormat; 009import daikon.inv.ValueSet; 010import java.io.Serializable; 011import java.util.ArrayList; 012import java.util.List; 013import java.util.StringJoiner; 014import org.checkerframework.checker.lock.qual.GuardSatisfied; 015import org.checkerframework.checker.nullness.qual.NonNull; 016import org.checkerframework.checker.nullness.qual.Nullable; 017import org.checkerframework.dataflow.qual.Pure; 018import org.checkerframework.dataflow.qual.SideEffectFree; 019import org.checkerframework.framework.qual.Unused; 020import typequals.prototype.qual.NonPrototype; 021import typequals.prototype.qual.Prototype; 022 023/** 024 * Tracks every unique value and how many times it occurs. Prints as either {@code x has no values} 025 * or as {@code x has values: v1 v2 v3 ...}. The set has no maximum size; it may be arbitrarily 026 * large. 027 */ 028public final class CompleteOneOfScalar extends SingleScalar { 029 static final long serialVersionUID = 20091210L; 030 031 /** Information about each value encountered. */ 032 public static class Info implements Serializable { 033 static final long serialVersionUID = 20091210L; 034 public long val; 035 public int cnt; 036 037 public Info(long val, int cnt) { 038 this.val = val; 039 this.cnt = cnt; 040 } 041 } 042 043 /** List of values seen. */ 044 // When the set of values seen is large, this representation is inefficient. 045 @Unused(when = Prototype.class) 046 @SuppressWarnings("serial") 047 public List<Info> vals; 048 049 /** Boolean. True iff CompleteOneOfScalar invariants should be considered. */ 050 public static boolean dkconfig_enabled = false; 051 052 public CompleteOneOfScalar(PptSlice slice) { 053 super(slice); 054 vals = new ArrayList<Info>(); 055 } 056 057 public @Prototype CompleteOneOfScalar() { 058 super(); 059 } 060 061 private static @Prototype CompleteOneOfScalar proto = new @Prototype CompleteOneOfScalar(); 062 063 /** Returns the prototype invariant for CompleteOneOFScalar. */ 064 public static @Prototype CompleteOneOfScalar get_proto() { 065 return proto; 066 } 067 068 @Override 069 public boolean enabled() { 070 return dkconfig_enabled; 071 } 072 073 @Override 074 public CompleteOneOfScalar instantiate_dyn(@Prototype CompleteOneOfScalar this, PptSlice slice) { 075 return new CompleteOneOfScalar(slice); 076 } 077 078 /** Return description of invariant. Only Daikon format is implemented. */ 079 @SideEffectFree 080 @Override 081 public String format_using(@GuardSatisfied CompleteOneOfScalar this, OutputFormat format) { 082 if (format == OutputFormat.DAIKON) { 083 if (vals.size() == 0) { 084 return var().name() + "has no values"; 085 } 086 StringJoiner out = new StringJoiner(" ", var().name() + " has values: ", ""); 087 for (Info val : vals) { 088 out.add(String.format("%s[%d]", val.val, val.cnt)); 089 } 090 return out.toString(); 091 } else { 092 return format_unimplemented(format); 093 } 094 } 095 096 @Override 097 public InvariantStatus add_modified(long a, int count) { 098 return check_modified(a, count); 099 } 100 101 @Override 102 public InvariantStatus check_modified(long a, int count) { 103 for (Info val : vals) { 104 if (val.val == a) { 105 val.cnt += count; 106 return InvariantStatus.NO_CHANGE; 107 } 108 } 109 vals.add(new Info(a, count)); 110 return InvariantStatus.NO_CHANGE; 111 } 112 113 @Override 114 protected double computeConfidence() { 115 ValueSet vs = ppt.var_infos[0].get_value_set(); 116 if (vs.size() > 0) { 117 return Invariant.CONFIDENCE_JUSTIFIED; 118 } else { 119 return Invariant.CONFIDENCE_UNJUSTIFIED; 120 } 121 } 122 123 /** 124 * Returns whether or not this is obvious statically. The only check is for static constants which 125 * are obviously printable (or not) from their values. 126 */ 127 @Pure 128 @Override 129 public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) { 130 return super.isObviousStatically(vis); 131 } 132 133 /** 134 * Same formula if each value is the same and has the same count. Not implemented for now, just 135 * presumed to be false. 136 */ 137 @Pure 138 @Override 139 public boolean isSameFormula(Invariant o) { 140 return false; 141 } 142 143 @Override 144 public @Nullable @NonPrototype CompleteOneOfScalar merge( 145 @Prototype CompleteOneOfScalar this, 146 List<@NonPrototype Invariant> invs, 147 PptSlice parent_ppt) { 148 @SuppressWarnings("nullness") // super.merge does not return null 149 @NonNull CompleteOneOfScalar result = (CompleteOneOfScalar) super.merge(invs, parent_ppt); 150 for (int i = 1; i < invs.size(); i++) { 151 for (Info info : ((CompleteOneOfScalar) invs.get(i)).vals) { 152 InvariantStatus status = result.add_modified(info.val, info.cnt); 153 if (status == InvariantStatus.FALSIFIED) { 154 return null; 155 } 156 } 157 } 158 return result; 159 } 160}