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