001package daikon.inv.unary.string; 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.IOException; 011import java.io.ObjectInputStream; 012import java.io.Serializable; 013import java.util.ArrayList; 014import java.util.List; 015import org.checkerframework.checker.interning.qual.Interned; 016import org.checkerframework.checker.lock.qual.GuardSatisfied; 017import org.checkerframework.checker.nullness.qual.Nullable; 018import org.checkerframework.dataflow.qual.Pure; 019import org.checkerframework.dataflow.qual.SideEffectFree; 020import org.checkerframework.framework.qual.Unused; 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" ...}. 026 */ 027public final class CompleteOneOfString extends SingleString { 028 // We are Serializable, so we specify a version to allow changes to 029 // method signatures without breaking serialization. If you add or 030 // remove fields, you should change this number to the current date. 031 static final long serialVersionUID = 20091210L; 032 033 /** Information about each value encountered. */ 034 public static class Info implements Serializable { 035 static final long serialVersionUID = 20091210L; 036 public String val; 037 public int cnt; 038 039 public Info(String val, int cnt) { 040 this.val = val.intern(); 041 this.cnt = cnt; 042 } 043 044 private void readObject(ObjectInputStream in) throws IOException, ClassNotFoundException { 045 in.defaultReadObject(); 046 if (val != null) val = val.intern(); 047 } 048 } 049 050 /** List of values seen. */ 051 @Unused(when = Prototype.class) 052 @SuppressWarnings("serial") 053 public List<Info> vals; 054 055 /** Boolean. True iff CompleteOneOfString invariants should be considered. */ 056 public static boolean dkconfig_enabled = false; 057 058 public CompleteOneOfString(PptSlice slice) { 059 super(slice); 060 vals = new ArrayList<Info>(); 061 } 062 063 public @Prototype CompleteOneOfString() { 064 super(); 065 } 066 067 private static @Prototype CompleteOneOfString proto = new @Prototype CompleteOneOfString(); 068 069 /** Returns the prototype invariant for CompleteOneOFString. */ 070 public static @Prototype CompleteOneOfString get_proto() { 071 return proto; 072 } 073 074 /** returns whether or not this invariant is enabled */ 075 @Override 076 public boolean enabled() { 077 return dkconfig_enabled; 078 } 079 080 /** instantiate an invariant on the specified slice */ 081 @Override 082 public CompleteOneOfString instantiate_dyn(@Prototype CompleteOneOfString this, PptSlice slice) { 083 return new CompleteOneOfString(slice); 084 } 085 086 /** Return description of invariant. Only Daikon format is implemented. */ 087 @SideEffectFree 088 @Override 089 public String format_using(@GuardSatisfied CompleteOneOfString this, OutputFormat format) { 090 if (format == OutputFormat.DAIKON) { 091 if (vals.size() == 0) { 092 return var().name() + "has no values"; 093 } 094 StringBuilder out = new StringBuilder(vals.get(0).val.length() * vals.size()); 095 out.append(var().name() + " has values: "); 096 for (Info val : vals) { 097 out.append(String.format(" %s[%d]", val.val, val.cnt)); 098 } 099 return out.toString(); 100 } else { 101 return format_unimplemented(format); 102 } 103 } 104 105 /** Check to see if a only contains printable ascii characters. */ 106 @Override 107 public InvariantStatus add_modified(@Interned String a, int count) { 108 return check_modified(a, count); 109 } 110 111 /** Check to see if a only contains printable ascii characters. */ 112 @Override 113 public InvariantStatus check_modified(@Interned String a, int count) { 114 for (Info val : vals) { 115 if (val.val.equals(a)) { 116 val.cnt += count; 117 return InvariantStatus.NO_CHANGE; 118 } 119 } 120 vals.add(new Info(a, count)); 121 return InvariantStatus.NO_CHANGE; 122 } 123 124 @Override 125 protected double computeConfidence() { 126 ValueSet vs = ppt.var_infos[0].get_value_set(); 127 if (vs.size() > 0) { 128 return Invariant.CONFIDENCE_JUSTIFIED; 129 } else { 130 return Invariant.CONFIDENCE_UNJUSTIFIED; 131 } 132 } 133 134 /** 135 * Returns whether or not this is obvious statically. The only check is for static constants which 136 * are obviously printable (or not) from their values. 137 */ 138 @Pure 139 @Override 140 public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) { 141 return super.isObviousStatically(vis); 142 } 143 144 /** 145 * Same formula if each value is the same and has the same count. Not implemented for now, just 146 * presumed to be false. 147 */ 148 @Pure 149 @Override 150 public boolean isSameFormula(Invariant o) { 151 return false; 152 } 153}