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