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 org.checkerframework.checker.lock.qual.GuardSatisfied;
014import org.checkerframework.checker.nullness.qual.Nullable;
015import org.checkerframework.dataflow.qual.Pure;
016import org.checkerframework.dataflow.qual.SideEffectFree;
017import org.checkerframework.framework.qual.Unused;
018import typequals.prototype.qual.Prototype;
019
020/**
021 * Tracks every unique value and how many times it occurs. Prints as {@code x has values: v1 v2 v3
022 * ...}.
023 */
024public final class CompleteOneOfScalar extends SingleScalar {
025  // We are Serializable, so we specify a version to allow changes to
026  // method signatures without breaking serialization.  If you add or
027  // remove fields, you should change this number to the current date.
028  static final long serialVersionUID = 20091210L;
029
030  /** Information about each value encountered. */
031  public static class Info implements Serializable {
032    static final long serialVersionUID = 20091210L;
033    public long val;
034    public int cnt;
035
036    public Info(long val, int cnt) {
037      this.val = val;
038      this.cnt = cnt;
039    }
040  }
041
042  /** List of values seen. */
043  @Unused(when = Prototype.class)
044  @SuppressWarnings("serial")
045  public List<Info> vals;
046
047  /** Boolean. True iff CompleteOneOfScalar invariants should be considered. */
048  public static boolean dkconfig_enabled = false;
049
050  public CompleteOneOfScalar(PptSlice slice) {
051    super(slice);
052    vals = new ArrayList<Info>();
053  }
054
055  public @Prototype CompleteOneOfScalar() {
056    super();
057  }
058
059  private static @Prototype CompleteOneOfScalar proto = new @Prototype CompleteOneOfScalar();
060
061  /** Returns the prototype invariant for CompleteOneOFScalar. */
062  public static @Prototype CompleteOneOfScalar get_proto() {
063    return proto;
064  }
065
066  /** returns whether or not this invariant is enabled */
067  @Override
068  public boolean enabled() {
069    return dkconfig_enabled;
070  }
071
072  /** instantiate an invariant on the specified slice */
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      String out = var().name() + " has values: ";
084      for (Info val : vals) {
085        out += String.format(" %s[%d]", val.val, val.cnt);
086      }
087      return out;
088    } else {
089      return format_unimplemented(format);
090    }
091  }
092
093  /** Check to see if a only contains printable ascii characters. */
094  @Override
095  public InvariantStatus add_modified(long a, int count) {
096    return check_modified(a, count);
097  }
098
099  /** Check to see if a only contains printable ascii characters. */
100  @Override
101  public InvariantStatus check_modified(long a, int count) {
102    for (Info val : vals) {
103      if (val.val == a) {
104        val.cnt += count;
105        return InvariantStatus.NO_CHANGE;
106      }
107    }
108    vals.add(new Info(a, count));
109    // System.out.printf("check_modified %s%n", format());
110    return InvariantStatus.NO_CHANGE;
111  }
112
113  @Override
114  protected double computeConfidence() {
115    ValueSet vs = ppt.var_infos[0].get_value_set();
116    // System.out.printf("%s value set = %s%n", ppt.var_infos[0].name(), vs);
117    if (vs.size() > 0) {
118      return Invariant.CONFIDENCE_JUSTIFIED;
119    } else {
120      return Invariant.CONFIDENCE_UNJUSTIFIED;
121    }
122  }
123
124  /**
125   * Returns whether or not this is obvious statically. The only check is for static constants which
126   * are obviously printable (or not) from their values.
127   */
128  @Pure
129  @Override
130  public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) {
131    return super.isObviousStatically(vis);
132  }
133
134  /**
135   * Same formula if each value is the same and has the same count. Not implemented for now, just
136   * presumed to be false.
137   */
138  @Pure
139  @Override
140  public boolean isSameFormula(Invariant o) {
141    return false;
142  }
143}