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