Source code

001// ***** This file is automatically generated from CommonSequence.java.jpp
002
003package daikon.inv.unary.sequence;
004
005import daikon.*;
006import daikon.inv.*;
007import java.util.Arrays;
008import java.util.List;
009import java.util.StringJoiner;
010import org.checkerframework.checker.interning.qual.Interned;
011import org.checkerframework.checker.lock.qual.GuardSatisfied;
012import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
013import org.checkerframework.checker.nullness.qual.NonNull;
014import org.checkerframework.checker.nullness.qual.Nullable;
015import org.checkerframework.dataflow.qual.Pure;
016import org.checkerframework.dataflow.qual.SideEffectFree;
017import org.plumelib.util.ArraysPlume;
018import org.plumelib.util.Intern;
019import typequals.prototype.qual.NonPrototype;
020import typequals.prototype.qual.Prototype;
021
022/**
023 * Represents sequences of long values that contain a common subset. Prints as
024 * {@code {e1, e2, e3, ...} subset of x[]}.
025 */
026
027public class CommonSequence extends SingleScalarSequence {
028  static final long serialVersionUID = 20030822L;
029
030  // Variables starting with dkconfig_ should only be set via the
031  // daikon.config.Configuration interface.
032  /** Boolean. True iff CommonSequence invariants should be considered. */
033  public static boolean dkconfig_enabled = false;
034
035  /** Boolean. Set to true to consider common sequences over hashcodes (pointers). */
036  public static boolean dkconfig_hashcode_seqs = false;
037
038  /** The number of samples observed. */
039  private int count = 0;
040
041  /** Null means no samples have been seen yet. Empty array means intersection is empty. */
042  private long @MonotonicNonNull @Interned [] intersect = null;
043
044  protected CommonSequence(PptSlice ppt) {
045    super(ppt);
046  }
047
048  protected @Prototype CommonSequence() {
049    super();
050  }
051
052  private static @Prototype CommonSequence proto = new @Prototype CommonSequence();
053
054  /** Returns the prototype invariant for CommonSequence */
055  public static @Prototype CommonSequence get_proto() {
056    return proto;
057  }
058
059  @Override
060  public boolean enabled() {
061    return dkconfig_enabled;
062  }
063
064  /** Sequences of hashcode values won't be consistent and are thus not printed by default. */
065  @Override
066  public boolean instantiate_ok(VarInfo[] vis) {
067
068    if (!valid_types(vis)) {
069      return false;
070    }
071
072    return dkconfig_hashcode_seqs || vis[0].file_rep_type.baseIsIntegral();
073  }
074
075  @Override
076  protected CommonSequence instantiate_dyn(@Prototype CommonSequence this, PptSlice slice) {
077    return new CommonSequence(slice);
078  }
079
080  // Don't define clone (use the Object version instead), because this.intersect is read-only.
081  // public Object clone();
082
083  @Override
084  public String repr(@GuardSatisfied CommonSequence this) {
085    return "CommonSequence " + varNames() + ": count=\"" + count;
086  }
087
088  private String printIntersect(@GuardSatisfied CommonSequence this) {
089    if (intersect == null) {
090      return "{}";
091    }
092
093    StringJoiner result = new StringJoiner(", ", "{", "}");
094    for (int i = 0; i < intersect.length; i++) {
095      result.add("" + intersect[i]);
096    }
097    return result.toString();
098  }
099
100  @SideEffectFree
101  @Override
102  public String format_using(@GuardSatisfied CommonSequence this, OutputFormat format) {
103    if (format == OutputFormat.DAIKON) {
104      return format_daikon();
105    }
106    if (format == OutputFormat.CSHARPCONTRACT) {
107      return format_csharp_contract();
108    }
109    if (format == OutputFormat.SIMPLIFY) {
110      return format_simplify();
111    }
112
113    return format_unimplemented(format);
114  }
115
116  public String format_daikon(@GuardSatisfied CommonSequence this) {
117    return printIntersect() + " subset of " + var().name();
118  }
119
120  public String format_csharp_contract(@GuardSatisfied CommonSequence this) {
121    if (intersect == null) {
122      return "()";
123    }
124
125    if (intersect.length == 1) {
126      String collection = var().csharp_collection_string();
127      return collection + ".Contains(" + intersect[0] + ")";
128    }
129
130    StringJoiner exp = new StringJoiner(", ", "(", ")");
131    for (long i : intersect) {
132      exp.add("" + i);
133    }
134
135    String[] split = var().csharp_array_split();
136    return "Contract.ForAll(" + split[0] + ", x => x" + split[1] + ".OneOf" + exp + ")";
137  }
138
139  private String format_simplify(@GuardSatisfied CommonSequence this) {
140    if (intersect == null || intersect.length == 0) {
141      return "(AND)";
142    }
143    String[] name = var().simplifyNameAndBounds();
144    if (name == null) {
145      return format_unimplemented(OutputFormat.SIMPLIFY);
146    }
147    String idx;
148    if (!name[0].equals("|i|")) {
149      idx = "i";
150    } else {
151      idx = "j";
152    }
153    StringBuilder pre_buf = new StringBuilder("");
154    StringBuilder end_buf = new StringBuilder("");
155    for (int i = 0; i < intersect.length; i++) {
156      pre_buf.append("(EXISTS ("+idx + i + ") (AND ");
157      pre_buf.append("(>= "+idx + i + " " + name[1] + ") ");
158      pre_buf.append("(<= "+idx + i + " " + name[2] + ") ");
159
160      // Based on the class name, I originally wrote this method as if
161      // the invariant represented a common subsequence between two
162      // sequences (i.e. where the match was required to be in
163      // order). In case an invariant like that is added in the
164      // future, use the following:
165//       if (i == 0)
166//         pre_buf.append("(>= "+idx + i + " 0) ");
167//       else if (i > 0)
168//          pre_buf.append("(> "+idx + i + " "+idx+(i-1) +") ");
169//       if (i == intersect.length - 1)
170//         pre_buf.append("(< "+idx + i + " (select arrayLength " + name[0] + ")) ");
171      pre_buf.append("(EQ (select (select elems " + name[0] + ") "+idx + i + ") "
172                     + simplify_format_long(intersect[i]) + ")");
173      if (i == intersect.length - 1) {
174        pre_buf.append(" ");
175      }
176      end_buf.append("))");
177    }
178    pre_buf.append(end_buf);
179    return pre_buf.toString();
180  }
181
182  @Override
183  public InvariantStatus check_modified(long @Interned [] a, int count) {
184    if (a == null) {
185      return InvariantStatus.FALSIFIED;
186    } else if (intersect == null) {
187      return InvariantStatus.NO_CHANGE;
188    } else {
189      for (int i = 0; i < a.length; i++) {
190        if (ArraysPlume.indexOf(intersect, a[i]) != -1) {
191          return InvariantStatus.NO_CHANGE;
192        }
193      }
194      return InvariantStatus.FALSIFIED;
195    }
196  }
197
198  @Override
199  public InvariantStatus add_modified(long @Interned [] a, int count) {
200    // System.out.println ("common: " + Arrays.toString (a));
201    if (a == null) {
202      return InvariantStatus.FALSIFIED;
203    } else if (intersect == null) {
204      intersect = a;
205      return InvariantStatus.NO_CHANGE;
206    }
207
208    long[] tmp = new long[intersect.length];
209    int size = 0;
210    for (int i = 0; i < a.length; i++) {
211      // if (a[i] in intersect) && !(a[i] in tmp), add a[i] to tmp
212      int ii = ArraysPlume.indexOf(intersect, a[i]);
213      if ((ii != -1)
214        && (ArraysPlume.indexOf(ArraysPlume.subarray(tmp,0,size), a[i]) == -1)) {
215        // System.out.println ("adding " + intersect[ii] + " at " + size);
216
217        // Carefully add the existing intersect value and not a[i].  These
218        // are not necessarily the same when fuzzy floating point
219        // comparisons are active.
220        tmp[size++] = intersect[ii];
221      }
222    }
223    if (size == 0) {
224      return InvariantStatus.FALSIFIED;
225    }
226
227    intersect = Intern.intern(ArraysPlume.subarray(tmp, 0, size));
228
229    /// Use a lesser count, because this invariant is frequently a false positive.
230    // this.count += count;
231    this.count++;
232    return InvariantStatus.NO_CHANGE;
233  }
234
235  @Override
236  protected double computeConfidence() {
237    return 1 - Math.pow(.9, count);
238  }
239
240  @Pure
241  @Override
242  public boolean isSameFormula(Invariant other) {
243    assert other instanceof CommonSequence;
244    return true;
245  }
246
247  @Override
248  public @Nullable @NonPrototype CommonSequence merge(
249    @Prototype CommonSequence this, List<@NonPrototype Invariant> invs, PptSlice parent_ppt) {
250    @SuppressWarnings("nullness") // super.merge does not return null
251    @NonNull CommonSequence result = (CommonSequence) super.merge(invs, parent_ppt);
252    for (int i=1; i<invs.size(); i++) {
253      CommonSequence inv = (CommonSequence) invs.get(i);
254      long @MonotonicNonNull @Interned [] invIntersect = inv.intersect;
255      if (invIntersect != null) {
256        InvariantStatus status = result.add_modified(invIntersect, inv.count);
257        if (status == InvariantStatus.FALSIFIED) {
258          return null;
259        }
260      }
261    }
262    return result;
263  }
264}