Source code

001// ***** This file is automatically generated from SeqIntComparison.java.jpp
002
003package daikon.inv.binary.sequenceScalar;
004
005import daikon.*;
006import daikon.derive.unary.*;
007import daikon.inv.*;
008import daikon.inv.binary.twoSequence.*;
009import daikon.inv.unary.sequence.*;
010import daikon.suppress.*;
011import java.util.*;
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.Nullable;
016import org.checkerframework.dataflow.qual.Pure;
017import org.checkerframework.dataflow.qual.SideEffectFree;
018import org.plumelib.util.Intern;
019import typequals.prototype.qual.NonPrototype;
020import typequals.prototype.qual.Prototype;
021
022/**
023 * Represents an invariant between a long scalar and a a sequence of long values. Prints
024 * as {@code x[] elements < y} where {@code x} is a long sequence and
025 * {@code y} is a long scalar.
026 */
027public final class SeqIntLessThan extends SequenceScalar {
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 = 20030822L;
032
033  // Variables starting with dkconfig_ should only be set via the
034  // daikon.config.Configuration interface.
035  /** Boolean. True iff SeqIntLessThan invariants should be considered. */
036  public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault;
037
038  public static final Logger debug =
039    Logger.getLogger("daikon.inv.binary.sequenceScalar.SeqIntLessThan");
040
041  static boolean debugSeqIntComparison = false;
042
043  SeqIntLessThan(PptSlice ppt) {
044    super(ppt);
045  }
046
047  @Prototype SeqIntLessThan() {
048    super();
049  }
050
051  private static @Prototype SeqIntLessThan proto = new @Prototype SeqIntLessThan();
052
053  /** Returns the prototype invariant for SeqIntLessThan */
054  public static @Prototype SeqIntLessThan get_proto() {
055    return proto;
056  }
057
058  /** Returns whether or not this invariant is enabled. */
059  @Override
060  public boolean enabled() {
061    return dkconfig_enabled;
062  }
063
064  /** Non-equal SeqIntComparison is only valid on integral types. */
065  @Override
066  public boolean instantiate_ok(VarInfo[] vis) {
067
068    if (!valid_types(vis)) {
069      return false;
070    }
071
072    VarInfo seqvar;
073    VarInfo sclvar;
074    if (vis[0].rep_type == ProglangType.INT_ARRAY) {
075      seqvar = vis[0];
076      sclvar = vis[1];
077    } else {
078      seqvar = vis[1];
079      sclvar = vis[0];
080    }
081
082    assert sclvar.rep_type == ProglangType.INT;
083    assert seqvar.rep_type == ProglangType.INT_ARRAY;
084
085      if (!seqvar.type.elementIsIntegral()) {
086        return false;
087      }
088
089    return true;
090  }
091
092  /** instantiates the invariant on the specified slice */
093  @Override
094  protected SeqIntLessThan instantiate_dyn(@Prototype SeqIntLessThan this, PptSlice slice) {
095    return new SeqIntLessThan(slice);
096  }
097
098  /**
099   * Checks to see if the comparison is obvious statically. Makes the following checks:
100   *
101   * <pre>
102   *    max(A[]) op A[]
103   *    min(A[]) op A[]
104   * </pre>
105   *
106   * JHP: Note that these are not strict implications, these are merely uninteresting comparisons
107   * (except when op is GreaterEqual for max and LessEqual for min).
108   */
109  @Pure
110  @Override
111  public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) {
112
113    SequenceMin seqmin = null;
114    SequenceMax seqmax = null;
115    VarInfo sclseq = null;
116    VarInfo sclvar = sclvar(vis);
117    if (sclvar.derived instanceof SequenceMin) {
118      seqmin = (SequenceMin) sclvar.derived;
119      sclseq = seqmin.base;
120    } else if (sclvar.derived instanceof SequenceMax) {
121      seqmax = (SequenceMax) sclvar.derived;
122      sclseq = seqmax.base;
123    }
124    if (seqvar(vis) == sclseq) {
125      return new DiscardInfo(this, DiscardCode.obvious, sclvar(vis).name() + " is min/max ");
126    }
127    return null;
128  }
129
130  @SideEffectFree
131  @Override
132  public SeqIntLessThan clone(@GuardSatisfied SeqIntLessThan this) {
133    SeqIntLessThan result = (SeqIntLessThan) super.clone();
134    return result;
135  }
136
137  @Override
138  public String repr(@GuardSatisfied SeqIntLessThan this) {
139    return "SeqIntLessThan" + varNames() + ": ,falsified=" + falsified;
140  }
141
142  @SideEffectFree
143  @Override
144  public String format_using(@GuardSatisfied SeqIntLessThan this, OutputFormat format) {
145
146    if (format.isJavaFamily()) {
147      return format_java_family(format);
148    }
149
150    if (format == OutputFormat.DAIKON) {
151      return format_daikon();
152    }
153    if (format == OutputFormat.ESCJAVA) {
154      return format_esc();
155    }
156    if (format == OutputFormat.SIMPLIFY) {
157      return format_simplify();
158    }
159    if (format == OutputFormat.CSHARPCONTRACT) {
160      return format_csharp_contract();
161    }
162
163    return format_unimplemented(format);
164  }
165
166  public String format_daikon(@GuardSatisfied SeqIntLessThan this) {
167    return seqvar().name() + " elements < " + sclvar().name();
168  }
169
170  public String format_esc(@GuardSatisfied SeqIntLessThan this) {
171    String[] form = VarInfo.esc_quantify(seqvar(), sclvar());
172    return form[0] + "(" + form[1] + " < " + form[2] + ")" + form[3];
173  }
174
175  public String format_simplify(@GuardSatisfied SeqIntLessThan this) {
176    String[] form = VarInfo.simplify_quantify(seqvar(), sclvar());
177    return form[0] + "(< " + form[1] + " " + form[2] + ")" + form[3];
178  }
179
180  public String format_java_family(@GuardSatisfied SeqIntLessThan this, OutputFormat format) {
181    return "daikon.Quant.eltsLT("
182        + seqvar().name_using(format)
183        + ", "
184        + sclvar().name_using(format)
185        + ")";
186  }
187
188  public String format_csharp_contract(@GuardSatisfied SeqIntLessThan this) {
189    String[] split = seqvar().csharp_array_split();
190    return "Contract.ForAll("
191        + split[0]
192        + ", x => x"
193        + split[1]
194        + " < "
195        + sclvar().csharp_name()
196        + ")";
197  }
198
199  @Override
200  public InvariantStatus check_modified(long @Interned [] a, long x, int count) {
201    /*if (logDetail() || debug.isLoggable(Level.FINE))
202      log(debug,"(< " + Arrays.toString(a)
203      + " " + x);*/
204    for (int i = 0; i < a.length; i++) {
205
206        // assert seqvar().type.elementIsIntegral();
207
208      if (!(a[i] < x)) {
209        return InvariantStatus.FALSIFIED;
210      }
211    }
212    return InvariantStatus.NO_CHANGE;
213  }
214
215  @Override
216  public InvariantStatus add_modified(long @Interned [] a, long x, int count) {
217    return check_modified(a, x, count);
218  }
219
220  @Override
221  protected double computeConfidence() {
222
223    // If there are no samples over our variables, its unjustified
224    if (ppt.num_samples() == 0) {
225      return CONFIDENCE_UNJUSTIFIED;
226    }
227
228    // If the array never has any elements, its unjustified
229    ValueSet.ValueSetScalarArray vs = (ValueSet.ValueSetScalarArray) seqvar().get_value_set();
230    if (vs.elem_cnt() == 0) {
231      return CONFIDENCE_UNJUSTIFIED;
232    }
233
234      // return 1 - Math.pow(.5, vs.elem_cnt());
235      return 1 - Math.pow(.5, ppt.num_samples());
236  }
237
238  @Pure
239  @Override
240  public boolean isExact() {
241
242      return false;
243  }
244
245  @Pure
246  @Override
247  public boolean isSameFormula(Invariant other) {
248    return true;
249  }
250
251  @Pure
252  @Override
253  public boolean isExclusiveFormula(Invariant other) {
254    return false;
255  }
256
257  // Look up a previously instantiated invariant.
258  public static @Nullable SeqIntLessThan find(PptSlice ppt) {
259    assert ppt.arity() == 2;
260    for (Invariant inv : ppt.invs) {
261      if (inv instanceof SeqIntLessThan) {
262        return (SeqIntLessThan) inv;
263      }
264    }
265    return null;
266  }
267
268  /**
269   * Checks to see if this is obvious over the specified variables. Implements the following checks:
270   *
271   * <pre>
272   *  (x op B[]) ^ (B[] subsequence A[]) &rArr; (x op A[])
273   *  (A[] == [])                        &rArr; (x op A[])
274   * </pre>
275   */
276  @Pure
277  @Override
278  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
279
280    DiscardInfo super_result = super.isObviousDynamically(vis);
281    if (super_result != null) {
282      return super_result;
283    }
284
285    VarInfo seqvar = seqvar(vis);
286    @SuppressWarnings("UnusedVariable")  // generated code, sometimes is necessary
287    VarInfo sclvar = sclvar(vis);
288    // Debug.log(getClass(), ppt, vis, "Considering  over" + seqvar.name()
289    //           + " and " + sclvar.name());
290
291    // Look for the same property over a supersequence of this one.  This
292    // doesn't need to explicitly ignore oher members of the equality set
293    // because those members won't have any invariants over them.
294    PptTopLevel pptt = ppt.parent;
295    for (Iterator<Invariant> inv_itor = pptt.invariants_iterator(); inv_itor.hasNext(); ) {
296      Invariant inv = inv_itor.next();
297      if (inv == this) {
298        continue;
299      }
300      if (inv instanceof SeqIntLessThan) {
301        SeqIntLessThan other = (SeqIntLessThan) inv;
302        // System.out.printf("considering %s seqvar=%s, other=%s%n", other.format(),
303        // seqvar().name(), other.seqvar().name());
304        if (pptt.is_subsequence(seqvar(), other.seqvar()) && (sclvar(vis) == other.sclvar())) {
305          // System.out.println ("is subsequence");
306          return new DiscardInfo(
307              this,
308              DiscardCode.obvious,
309              seqvar().name()
310                  + " is a subsequence of "
311                  + other.seqvar().name()
312                  + " and "
313                  + other.format()
314                  + " holds");
315        }
316      }
317    }
318
319    // JHP: handled in confidence test now
320    // (A[] == []) ==> A[] op x
321    if (false) {
322      if (pptt.is_empty(seqvar)) {
323        return new DiscardInfo(
324            this, DiscardCode.obvious, "The sequence " + seqvar.name() + " is always empty");
325      }
326    }
327
328    if (isExact()) {
329      return null;
330    }
331
332    // JHP: these presume that this invariant is true and should thus be
333    // moved to uninteresting or removed.
334    if (sclvar.isDerived() && (sclvar.derived instanceof SequenceLength)) {
335      // Sequence length tests
336      SequenceLength scl_seqlen = (SequenceLength) sclvar.derived;
337
338      if ((scl_seqlen != null) && (scl_seqlen.shift == 0)) {
339        // "x < size(a)"  ("x <= size(a)-1" would be more informative)
340        return new DiscardInfo(
341            this,
342            DiscardCode.obvious,
343            "An Invariant of the form x <= size(a)-1 would be more informative");
344      }
345
346    }
347
348    // JHP: this presumes that this invariant is true and should thus be
349    // moved to uninteresting or removed.
350    {
351      PptSlice1 seqslice = pptt.findSlice(seqvar);
352      if (seqslice != null) {
353        EltOneOf eoo = EltOneOf.find(seqslice);
354        if ((eoo != null) && eoo.enoughSamples() && (eoo.num_elts() == 1)) {
355          return new DiscardInfo(this, DiscardCode.obvious, "Obvious implied by " + eoo.format());
356        }
357      }
358    }
359
360    return null;
361  }
362
363  /** Returns a list of non-instantiating suppressions for this invariant. */
364  @Pure
365  @Override
366  public @Nullable NISuppressionSet get_ni_suppressions() {
367    return suppressions;
368  }
369
370  /** NI Suppressions for each type of comparison. */
371  private static @Nullable NISuppressionSet suppressions = null;
372
373}