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