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