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}