Source code

001// ***** This file is automatically generated from SeqIndexComparison.java.jpp
002
003package daikon.inv.unary.sequence;
004
005import daikon.*;
006import daikon.Quantify.QuantFlags;
007import daikon.inv.*;
008import daikon.inv.binary.twoSequence.*;
009import daikon.suppress.*;
010import java.util.Arrays;
011import java.util.Iterator;
012import java.util.logging.Logger;
013import org.checkerframework.checker.interning.qual.Interned;
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.plumelib.util.Intern;
020import typequals.prototype.qual.NonPrototype;
021import typequals.prototype.qual.Prototype;
022
023/**
024 * Represents an invariant over sequences of long values between the index of an element of the
025 * sequence and the element itself. Prints as {@code x[i] != i}.
026 */
027public class SeqIndexIntNonEqual extends SingleScalarSequence {
028  // We are Serializable, so we specify a version to allow changes to
029  // method signatures without breaking serialization.  If you add or
030  // remove fields, you should change this number to the current date.
031  static final long serialVersionUID = 20040203L;
032
033  /** Debug tracer. */
034  public static final Logger debug =
035    Logger.getLogger("daikon.inv.unary.sequence.SeqIndexIntNonEqual");
036
037  // Variables starting with dkconfig_ should only be set via the
038  // daikon.config.Configuration interface.
039  /** Boolean. True iff SeqIndexIntNonEqual invariants should be considered. */
040  public static boolean dkconfig_enabled = false;
041
042  private @Prototype SeqIndexIntNonEqual() {
043    super();
044  }
045
046  protected SeqIndexIntNonEqual(PptSlice slice) {
047    super(slice);
048    assert slice != null;
049    assert var().rep_type == ProglangType.INT_ARRAY;
050  }
051
052  private static @Prototype SeqIndexIntNonEqual proto = new @Prototype SeqIndexIntNonEqual();
053
054  /** Returns the prototype invariant for SeqIndexIntNonEqual */
055  public static @Prototype SeqIndexIntNonEqual get_proto() {
056    return proto;
057  }
058
059  /** returns whether or not we are enabled */
060  @Override
061  public boolean enabled() {
062    return dkconfig_enabled && !dkconfig_SeqIndexDisableAll;
063  }
064
065  /** Check that SeqIndex comparisons make sense over these vars. */
066  @Override
067  public boolean instantiate_ok(VarInfo[] vis) {
068
069    if (!valid_types(vis)) {
070      return false;
071    }
072
073    // Don't compare indices to object addresses.
074    ProglangType elt_type = vis[0].file_rep_type.elementType();
075    if (!elt_type.baseIsIntegral()) {
076      return false;
077    }
078
079    // Make sure that the indices are comparable to the elements
080    VarInfo seqvar = vis[0];
081    assert seqvar.comparability != null;
082    VarComparability elt_compar = seqvar.comparability.elementType();
083    VarComparability index_compar = seqvar.comparability.indexType(0);
084    if (!VarComparability.comparable(elt_compar, index_compar)) {
085      return false;
086    }
087
088    return true;
089  }
090
091  /** Instantiate the invariant on the specified slice. */
092  @Override
093  public SeqIndexIntNonEqual instantiate_dyn(@Prototype SeqIndexIntNonEqual this, PptSlice slice) {
094    return new SeqIndexIntNonEqual(slice);
095  }
096
097  /** returns the ni-suppressions for SeqIndexIntNonEqual */
098  @Pure
099  @Override
100  public @Nullable NISuppressionSet get_ni_suppressions() {
101    return null;
102  }
103
104  protected Invariant resurrect_done_swapped() {
105
106      return this;
107  }
108
109  public String getComparator() {
110    return "!=";
111  }
112
113  @SideEffectFree
114  @Override
115  public String format_using(@GuardSatisfied SeqIndexIntNonEqual this, OutputFormat format) {
116    if (format.isJavaFamily()) {
117      return format_java_family(format);
118    }
119
120    // TODO: Eliminate the unnecessary format_xxx() below if the
121    // format_java_family() can handle all the Java family output.
122
123    if (format == OutputFormat.DAIKON) {
124      return format_daikon();
125    }
126    if (format == OutputFormat.ESCJAVA) {
127      return format_esc();
128    }
129    if (format == OutputFormat.CSHARPCONTRACT) {
130      return format_csharp_contract();
131    }
132    if (format == OutputFormat.SIMPLIFY) {
133      return format_simplify();
134    }
135
136    return format_unimplemented(format);
137  }
138
139  public String format_daikon(@GuardSatisfied SeqIndexIntNonEqual this) {
140
141    // If this is an array/container and not a subsequence
142    if (var().isDerivedSubSequenceOf() == null) {
143      return var().apply_subscript("i") + " != i";
144    } else {
145      return var().name() + " != (index)";
146    }
147  }
148
149  // Bad code here: if the first index is changed from i this breaks
150  public String format_esc(@GuardSatisfied SeqIndexIntNonEqual this) {
151    String[] form = VarInfo.esc_quantify(var());
152    return form[0] + "(" + form[1] + " != i)" + form[2];
153  }
154
155  public String format_csharp_contract(@GuardSatisfied SeqIndexIntNonEqual this) {
156    String[] split = var().csharp_array_split();
157    return "Contract.ForAll(0, " + split[0] + ".Count(), i => " + split[0] + "[i]" + split[1] + " != i)";
158  }
159
160  public String format_java_family(@GuardSatisfied SeqIndexIntNonEqual this, OutputFormat format) {
161    return "daikon.Quant.eltsNotEqualIndex("
162      + var().name_using(format) + ")";
163  }
164
165  public String format_simplify(@GuardSatisfied SeqIndexIntNonEqual this) {
166    String[] form = VarInfo.simplify_quantify(QuantFlags.include_index(),
167                                               var());
168    return form[0] + "(NEQ " + form[1] + " " + form[2] + ")"
169      + form[3];
170  }
171
172  @Override
173  public InvariantStatus check_modified(long @Interned [] a, int count) {
174    for (int i = 0; i < a.length; i++) {
175      if (!(a[i] != i)) {
176        return InvariantStatus.FALSIFIED;
177      }
178    }
179    return InvariantStatus.NO_CHANGE;
180  }
181
182  @Override
183  public InvariantStatus add_modified(long @Interned [] a, int count) {
184
185    if (logDetail()) {
186      log("Entered add_modified: ppt.num_values()==%s, sample==%s",
187           ppt.num_values(), Arrays.toString(a));
188    }
189    InvariantStatus stat = check_modified(a, count);
190    if (logDetail()) {
191      log("Exiting add_modified status = %s", stat);
192    }
193
194    return stat;
195  }
196
197  @Override
198  @SuppressWarnings("UnnecessaryParentheses")  // generated code, parentheses are sometimes needed
199  protected double computeConfidence() {
200
201    // Make sure there have been some elements in the sequence
202    ValueSet.ValueSetScalarArray vs = (ValueSet.ValueSetScalarArray) ppt.var_infos[0].get_value_set();
203    if (vs.elem_cnt() == 0) {
204      return Invariant.CONFIDENCE_UNJUSTIFIED;
205    }
206
207    int num_values = ppt.num_values();
208    if (num_values == 0) {
209      return Invariant.CONFIDENCE_UNJUSTIFIED;
210    }
211
212      int max_indx = vs.max_length() - 1;
213      if ((vs.min() > max_indx) || (vs.max() < 0)) {
214        return Invariant.CONFIDENCE_UNJUSTIFIED;
215      } else {
216        long overlap = (Math.min(vs.max(), max_indx) - Math.max(vs.min(), 0));
217
218        if (overlap < 0) {
219          return Invariant.CONFIDENCE_UNJUSTIFIED;
220        }
221        overlap++;
222        double range1 = (double)max_indx + 1;
223        double range2 = (double)(vs.max()) - vs.min() + 1;
224
225        // probability of being equal by chance
226        //  = (overlap/range1) * (overlap/range2) * (1/overlap)
227        //  = overlap/(range1 * range2)
228
229        double confidence_one_nonequal = ((double)overlap)/(range1 * range2);
230
231        // The factor of 2 is a hack, but this seems too stringent otherwise
232        confidence_one_nonequal = Math.min(1.0, 2.0 * confidence_one_nonequal);
233
234        assert ! Double.isNaN(confidence_one_nonequal)
235                          && confidence_one_nonequal >= 0
236                          && confidence_one_nonequal <= 1
237        : "overlap=" + overlap
238                          + ", range1=" + range1
239                          + ", range2=" + range2
240                          ;
241        return 1 - Math.pow(1 - confidence_one_nonequal, vs.elem_cnt());
242      }
243
244  }
245
246  @Pure
247  @Override
248  public boolean isSameFormula(Invariant other) {
249    return true;
250  }
251
252  @Pure
253  @Override
254  public boolean isExclusiveFormula(Invariant other) {
255    return false;
256  }
257
258  // Look up a previously instantiated invariant.
259  public static @Nullable SeqIndexIntNonEqual find(PptSlice ppt) {
260    assert ppt.arity() == 1;
261    for (Invariant inv : ppt.invs) {
262      if (inv instanceof SeqIndexIntNonEqual) {
263        return (SeqIndexIntNonEqual) inv;
264      }
265    }
266    return null;
267  }
268
269  /**
270   * Checks to see if this is obvious over the specified variables Implements the following checks:
271   *
272   * <pre>
273   *    (A[] subsequence B[]) ^ (B[i] op i) &rArr; A[i] op i
274   * </pre>
275   *
276   * JHP: Its not obvious (to me) that this is true except when the subsequence starts at index
277   * 0. If B[] = {0, 1, 2, 3, 4} and A[] = {2, 3, 4}, A[] is a subsequence of B[] and B[i] == i, but
278   * A[i] = i is not true.
279   */
280  @Pure
281  @Override
282  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
283
284    DiscardInfo super_result = super.isObviousDynamically(vis);
285    if (super_result != null) {
286      return super_result;
287    }
288
289    VarInfo seqvar = vis[0];
290
291    // For each other sequence variable, if it is a supersequence of this
292    // one and it has the same invariant, then this one is obvious.
293    // We have to check for the same equality set here, because
294    // isObviousDynamically is called for each member of the equality set.
295    // We don't want other members of our own equality set to make this obvious
296    PptTopLevel pptt = ppt.parent;
297    for (int i = 0; i < pptt.var_infos.length; i++) {
298      VarInfo vi = pptt.var_infos[i];
299      if (vi.equalitySet == seqvar.equalitySet) {
300        continue;
301      }
302      if (SubSequence.isObviousSubSequenceDynamically(this, seqvar, vi)) {
303        PptSlice1 other_slice = pptt.findSlice(vi);
304        if (other_slice != null) {
305          SeqIndexIntNonEqual other_sine = SeqIndexIntNonEqual.find(other_slice);
306          if ((other_sine != null) && other_sine.enoughSamples()) {
307            return new DiscardInfo(this, DiscardCode.obvious,
308                        "The invariant " + format() + " over var "
309                       + seqvar.name() + " also holds over "
310                       +" the supersequence " + vi.name());
311          }
312        }
313      }
314    }
315
316    return null;
317  }
318}