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