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