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