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}