Source code

001// ***** This file is automatically generated from Bound.java.jpp
002
003package daikon.inv.unary.sequence;
004
005import daikon.*;
006import daikon.inv.*;
007
008  import daikon.inv.binary.twoSequence.*;
009  import daikon.inv.unary.scalar.*;
010
011import daikon.derive.unary.*;
012import daikon.inv.unary.*;
013import java.util.*;
014import org.checkerframework.checker.interning.qual.Interned;
015import org.checkerframework.checker.lock.qual.GuardSatisfied;
016import org.checkerframework.checker.nullness.qual.Nullable;
017import org.checkerframework.dataflow.qual.Pure;
018import org.checkerframework.dataflow.qual.SideEffectFree;
019import org.checkerframework.framework.qual.Unused;
020import org.plumelib.util.Intern;
021import typequals.prototype.qual.NonPrototype;
022import typequals.prototype.qual.Prototype;
023
024  /**
025   * Represents the invariant that each element of a sequence of double values is greater than or
026   * equal to a constant. Prints as {@code x[] elements >= c}.
027   */
028
029// One reason not to combine LowerBound and UpperBound into a single range
030// invariant is that they have separate justifications:  one may be
031// justified when the other is not.
032@SuppressWarnings("UnnecessaryParentheses")  // code generated by macros
033public class EltLowerBoundFloat extends SingleFloatSequence {
034  // We are Serializable, so we specify a version to allow changes to
035  // method signatures without breaking serialization.  If you add or
036  // remove fields, you should change this number to the current date.
037  static final long serialVersionUID = 20030822L;
038
039  // Variables starting with dkconfig_ should only be set via the
040  // daikon.config.Configuration interface.
041  /** Boolean. True iff EltLowerBoundFloat invariants should be considered. */
042  public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault;
043  /**
044   * Long integer. Together with the corresponding {@code maximal_interesting} parameter,
045   * specifies the range of the computed constant that is ``interesting'' --- the range that should
046   * be reported. For instance, setting {@code minimal_interesting} to -1 and
047   * {@code maximal_interesting} to 2 would only permit output of EltLowerBoundFloat invariants whose
048   * cutoff was one of (-1,0,1,2).
049   */
050  public static long dkconfig_minimal_interesting = -1;
051  /**
052   * Long integer. Together with the corresponding {@code minimal_interesting} parameter,
053   * specifies the range of the computed constant that is ``interesting'' --- the range that should
054   * be reported. For instance, setting {@code minimal_interesting} to -1 and
055   * {@code maximal_interesting} to 2 would only permit output of EltLowerBoundFloat invariants whose
056   * cutoff was one of (-1,0,1,2).
057   */
058  public static long dkconfig_maximal_interesting = 2;
059
060  @Unused(when=Prototype.class)
061  private LowerBoundCoreFloat core;
062
063  @SuppressWarnings("nullness") // circular initialization
064  private EltLowerBoundFloat(PptSlice slice) {
065    super(slice);
066    assert slice != null;
067    core = new LowerBoundCoreFloat(this);
068  }
069
070  private @Prototype EltLowerBoundFloat() {
071    super();
072    // do we need a core?
073  }
074
075  private static @Prototype EltLowerBoundFloat proto = new @Prototype EltLowerBoundFloat();
076
077  /** Returns the prototype invariant for EltLowerBoundFloat */
078  public static @Prototype EltLowerBoundFloat get_proto() {
079    return proto;
080  }
081
082  /** returns whether or not this invariant is enabled */
083  @Override
084  public boolean enabled() {
085    return dkconfig_enabled;
086  }
087
088  /** EltLowerBoundFloat is only valid on integral types. */
089  @Override
090  public boolean instantiate_ok(VarInfo[] vis) {
091
092    if (!valid_types(vis)) {
093      return false;
094    }
095
096    return vis[0].file_rep_type.baseIsFloat();
097    }
098
099  /** instantiate an invariant on the specified slice */
100  @Override
101  public EltLowerBoundFloat instantiate_dyn(@Prototype EltLowerBoundFloat this, PptSlice slice) {
102    return new EltLowerBoundFloat(slice);
103  }
104
105  @SideEffectFree
106  @Override
107  public EltLowerBoundFloat clone(@GuardSatisfied EltLowerBoundFloat this) {
108    EltLowerBoundFloat result = (EltLowerBoundFloat) super.clone();
109    result.core = core.clone();
110    result.core.wrapper = result;
111    return result;
112  }
113
114  public double min() {
115    return core.min();          // i.e., core.min1
116  }
117
118  @Override
119  public String repr(@GuardSatisfied EltLowerBoundFloat this) {
120    return "EltLowerBoundFloat" + varNames() + ": "
121      + core.repr();
122  }
123
124  @SideEffectFree
125  @Override
126  public String format_using(@GuardSatisfied EltLowerBoundFloat this, OutputFormat format) {
127
128    if (format.isJavaFamily()) {
129      return format_java_family(format);
130    }
131
132    if (format == OutputFormat.DAIKON) {
133      return format_daikon();
134    } else if (format == OutputFormat.SIMPLIFY) {
135      return format_simplify();
136    } else if (format == OutputFormat.ESCJAVA) {
137      return format_esc();
138    } else if (format == OutputFormat.CSHARPCONTRACT) {
139      return format_csharp_contract();
140    }
141
142    return format_unimplemented(format);
143  }
144  // ELTLOWEr || ELTUPPEr
145  public String format_daikon(@GuardSatisfied EltLowerBoundFloat this) {
146    PptTopLevel pptt = ppt.parent;
147    String name = var().name();
148
149    if (PrintInvariants.dkconfig_static_const_infer) {
150      for (VarInfo vi : pptt.var_infos) {
151        if (vi.isStaticConstant() && VarComparability.comparable(vi, var())) {
152          // If variable is a double, then use fuzzy comparison
153          if (vi.rep_type == ProglangType.DOUBLE) {
154            Double constantVal = (Double)vi.constantValue();
155            if (Global.fuzzy.eq(constantVal, (core.min1)) || (Double.isNaN(constantVal) && Double.isNaN( core.min1))) {
156              return name + " >= " + vi.name();
157            }
158          }
159          // Otherwise just use the equals method
160          else {
161            Object constantVal = vi.constantValue();
162            if (constantVal.equals(core.min1)) {
163              return name + " >= " + vi.name();
164            }
165          }
166        }
167      }
168    }
169
170    return var().name() + " elements >= " + core.min1;
171  }
172
173  public String format_esc(@GuardSatisfied EltLowerBoundFloat this) {
174    PptTopLevel pptt = ppt.parent;
175
176    if (PrintInvariants.dkconfig_static_const_infer) {
177      for (VarInfo vi : pptt.var_infos) {
178        if (vi.isStaticConstant() && VarComparability.comparable(vi, var())) {
179          // If variable is a double, then use fuzzy comparison
180          if (vi.rep_type == ProglangType.DOUBLE) {
181            Double constantVal = (Double)vi.constantValue();
182            if (Global.fuzzy.eq(constantVal, (core.min1)) || (Double.isNaN(constantVal) && Double.isNaN( core.min1))) {
183
184              String[] form = VarInfo.esc_quantify(var());
185              return form[0] + "(" + form[1] + " >= " + vi.name() + ")" + form[2];
186            }
187          }
188          // Otherwise just use the equals method
189            else {
190            Object constantVal = vi.constantValue();
191            if (constantVal.equals(core.min1)) {
192
193              String[] form = VarInfo.esc_quantify(var());
194              return form[0] + "(" + form[1] + " >= " + vi.name() + ")" + form[2];
195            }
196          }
197        }
198      }
199    }
200
201    String[] form = VarInfo.esc_quantify(var());
202    return form[0] + "(" + form[1] + " >= " + core.min1 + ")" + form[2];
203  }
204
205  public String format_csharp_contract(@GuardSatisfied EltLowerBoundFloat this) {
206    PptTopLevel pptt = ppt.parent;
207
208    if (PrintInvariants.dkconfig_static_const_infer) {
209      for (VarInfo vi : pptt.var_infos) {
210        if (vi.isStaticConstant() && VarComparability.comparable(vi, var())) {
211          // If variable is a double, then use fuzzy comparison
212          if (vi.rep_type == ProglangType.DOUBLE) {
213            Double constantVal = (Double)vi.constantValue();
214            if (Global.fuzzy.eq(constantVal, (core.min1)) || (Double.isNaN(constantVal) && Double.isNaN( core.min1))) {
215
216              String[] split = var().csharp_array_split();
217              return "Contract.ForAll(" + split[0] + ", x => x" + split[1] + " >= " + vi.name() + ")";
218            }
219          }
220          // Otherwise just use the equals method
221          else {
222            Object constantVal = vi.constantValue();
223            if (constantVal.equals(core.min1)) {
224
225              String[] split = var().csharp_array_split();
226              return "Contract.ForAll(" + split[0] + ", x => x" + split[1] + " >= " + vi.name() + ")";
227            }
228          }
229        }
230      }
231    }
232
233    String[] split = var().csharp_array_split();
234    return "Contract.ForAll(" + split[0] + ", x => x" + split[1] + " >= " + core.min1+ ")";
235  }
236
237  public String format_java_family(@GuardSatisfied EltLowerBoundFloat this, OutputFormat format) {
238    PptTopLevel pptt = ppt.parent;
239
240    if (PrintInvariants.dkconfig_static_const_infer) {
241      for (VarInfo vi : pptt.var_infos) {
242        if (vi.isStaticConstant() && VarComparability.comparable(vi, var())) {
243          // If variable is a double, then use fuzzy comparison
244          if (vi.rep_type == ProglangType.DOUBLE) {
245            Double constantVal = (Double)vi.constantValue();
246            if (Global.fuzzy.eq(constantVal, (core.min1)) || (Double.isNaN(constantVal) && Double.isNaN( core.min1))) {
247
248              return "daikon.Quant.eltsGTE(" + var().name_using(format) + ", " + vi.name() + ")";
249            }
250          }
251          // Otherwise just use the equals method
252          else {
253            Object constantVal = vi.constantValue();
254            if (constantVal.equals(core.min1)) {
255
256              return "daikon.Quant.eltsGTE(" + var().name_using(format) + ", " + vi.name() + ")";
257            }
258          }
259        }
260      }
261    }
262
263    return
264      "daikon.Quant.eltsGTE(" + var().name_using(format) + ", " + core.min1 + ")";
265
266  }
267
268  public String format_simplify(@GuardSatisfied EltLowerBoundFloat this) {
269
270    String value = simplify_format_double(core.min1);
271
272    String[] form = VarInfo.simplify_quantify(var());
273    return form[0] + "(>= " + form[1] + " " + value + ")"
274      + form[2];
275
276  }
277
278  @Override
279  public InvariantStatus add_modified(double @Interned [] value, int count) {
280    // System.out.println("EltLowerBoundFloat" + varNames() + ": "
281    //              + "add(" + value + ", " + modified + ", " + count + ")");
282
283    boolean changed = false;
284    InvariantStatus status = InvariantStatus.NO_CHANGE;
285    for (int i = 0; i < value.length; i++) {
286      if (!changed && core.wouldChange(value[i])) {
287        changed = true;
288        status = InvariantStatus.WEAKENED;
289      }
290      if (core.add_modified(value[i], count) ==
291          InvariantStatus.FALSIFIED) {
292        return InvariantStatus.FALSIFIED;
293      }
294    }
295    return status;
296  }
297
298  @Override
299  public InvariantStatus check_modified(double @Interned [] value, int count) {
300
301    for (int i = 0; i < value.length; i++) {
302      if (core.check(value[i]) == InvariantStatus.WEAKENED) {
303        return InvariantStatus.WEAKENED;
304      }
305    }
306    return InvariantStatus.NO_CHANGE;
307  }
308
309  @Override
310  public boolean enoughSamples(@GuardSatisfied EltLowerBoundFloat this) {
311    return core.enoughSamples();
312  }
313
314  @Override
315  protected double computeConfidence() {
316    return core.computeConfidence();
317  }
318
319  @Pure
320  @Override
321  public boolean isExact() {
322    return core.isExact();
323  }
324
325  @Pure
326  @Override
327  public boolean isSameFormula(Invariant other) {
328    return core.isSameFormula(((EltLowerBoundFloat) other).core);
329  }
330
331  @Override
332  public boolean hasUninterestingConstant() {
333    // If the constant bound is not in some small range of interesting
334    // values (by default {-1, 0, 1, 2}), call it uninteresting.
335    if ((core.min1 < dkconfig_minimal_interesting)
336        || (core.min1 > dkconfig_maximal_interesting)) {
337      return true;
338    }
339
340    else if (core.min1 != (int)core.min1) {
341      // Non-integer bounds are uninteresting even if small.
342      return true;
343    }
344
345    return false;
346  }
347
348  @Pure
349  @Override
350  public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) {
351    VarInfo var = vis[0];
352    if ((var.derived instanceof SequenceLength)
353         && (((SequenceLength) var.derived).shift != 0)) {
354      return new DiscardInfo(this, DiscardCode.obvious, "Bounds are preferrable over sequence lengths with no shift");
355    }
356
357    return super.isObviousStatically(vis);
358  }
359
360  @Pure
361  @Override
362  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
363    DiscardInfo super_result = super.isObviousDynamically(vis);
364    if (super_result != null) {
365      return super_result;
366    }
367
368    PptTopLevel pptt = ppt.parent;
369
370    // This check always lets invariants pass through (even if it is not within
371    // the default range of (-1 to 2) if it matches a static constant
372    // As noted below, this check really doesn't belong here, but should be
373    // moved to hasUninterestingConstant() whenever that is implemented
374    if (PrintInvariants.dkconfig_static_const_infer) {
375      if (core.matchConstant()) {
376        return null;
377      }
378    }
379
380    // if the value is not in some range (like -1,0,1,2) then say that it is obvious
381    if ((core.min1 < dkconfig_minimal_interesting)
382        || (core.min1 > dkconfig_maximal_interesting)) {
383      // XXX This check doesn't really belong here. However It
384      // shouldn't get removed until hasUninterestingConstant() is
385      // suitable to be turned on everywhere by default. -SMcC
386      // if the value is not in some range (like -1,0,1,2) then say that
387      // it is obvious
388      String discardString = "";
389      if (core.min1 < dkconfig_minimal_interesting) {
390        discardString = "MIN1="+core.min1+" is less than dkconfig_minimal_interesting=="
391          + dkconfig_minimal_interesting;
392      } else {
393        discardString = "MIN1="+core.min1+" is greater than dkconfig_maximal_interesting=="+
394          dkconfig_maximal_interesting;
395      }
396      return new DiscardInfo(this, DiscardCode.obvious, discardString);
397    }
398    EltOneOfFloat oo = EltOneOfFloat.find(ppt);
399    if ((oo != null) && oo.enoughSamples() && oo.num_elts() > 0) {
400      assert oo.var().isCanonical();
401      // We could also use core.min1 == oo.min_elt(), since the LowerBound
402      // will never have a core.min1 that does not appear in the OneOf.
403      if (core.min1 <= oo.min_elt()) {
404        String varName = vis[0].name();
405        String discardString = varName + "<=" + core.min1 + " is implied by " + varName + "<=" + oo.min_elt();
406        log("%s", discardString);
407        return new DiscardInfo(this, DiscardCode.obvious, discardString);
408      }
409    }
410
411    // NOT: "VarInfo v = var();" because we want to operate not on this
412    // object's own variables, but on the variables that were passed in.
413    VarInfo v = vis[0];
414
415    // Look for the same property over a supersequence of this one.
416    for (Iterator<Invariant> inv_itor = pptt.invariants_iterator(); inv_itor.hasNext(); ) {
417      Invariant inv = inv_itor.next();
418      if (inv == this) {
419        continue;
420      }
421      if (inv instanceof EltLowerBoundFloat) {
422        EltLowerBoundFloat other = (EltLowerBoundFloat) inv;
423        if (isSameFormula(other)
424            && SubSequenceFloat.isObviousSubSequenceDynamically(this, v, other.var())) {
425          String varName = v.name();
426          String otherName = other.var().name();
427          String discardString = varName + " is a subsequence of " + otherName + " for which the invariant holds.";
428          log("%s", discardString);
429          return new DiscardInfo(this, DiscardCode.obvious, discardString);
430        }
431      }
432    }
433
434    // For each sequence variable, if this is an obvious member/subsequence, and
435    // it has the same invariant, then this one is obvious.
436    for (int i = 0; i < pptt.var_infos.length; i++) {
437      VarInfo vi = pptt.var_infos[i];
438
439      if (SubSequenceFloat.isObviousSubSequenceDynamically(this, v, vi))
440      {
441        PptSlice1 other_slice = pptt.findSlice(vi);
442        if (other_slice != null) {
443          EltLowerBoundFloat eb = EltLowerBoundFloat.find(other_slice);
444          if ((eb != null)
445              && eb.enoughSamples()
446              && eb.min() == min()) {
447            String otherName = other_slice.var_infos[0].name();
448            String varName = v.name();
449            String discardString = varName+" is a subsequence of "+otherName+" for which the invariant holds.";
450            log("%s", discardString);
451            return new DiscardInfo(this, DiscardCode.obvious, discardString);
452          }
453        }
454      }
455    }
456
457    return null;
458  }
459
460  @Pure
461  @Override
462  public boolean isExclusiveFormula(Invariant other) {
463
464    // N.B. "x[] elements >= 200" is not mutually exclusive with "x[]
465    // elements <= 100"; they could both be true if x[] were always empty.
466
467    if (other instanceof OneOfFloat) {
468      return other.isExclusiveFormula(this);
469    }
470    return false;
471  }
472
473  // Look up a previously instantiated invariant.
474  public static @Nullable EltLowerBoundFloat find(PptSlice ppt) {
475    assert ppt.arity() == 1;
476    for (Invariant inv : ppt.invs) {
477      if (inv instanceof EltLowerBoundFloat) {
478        return (EltLowerBoundFloat) inv;
479      }
480    }
481    return null;
482  }
483
484  /**
485   * Bound can merge different formulas from lower points to create a single formula at an upper
486   * point. See merge() below.
487   */
488  @Override
489  public boolean mergeFormulasOk() {
490    return true;
491  }
492
493  /**
494   * Merge the invariants in invs to form a new invariant. Each must be a EltLowerBoundFloat invariant. This
495   * code finds all of the min/max values in each invariant, applies them to a new parent invariant
496   * and returns the merged invariant (if any).
497   *
498   * @param invs list of invariants to merge. The invariants must all be of the same type and should
499   *     come from the children of parent_ppt. They should also all be permuted to match the
500   *     variable order in parent_ppt.
501   * @param parent_ppt slice that will contain the new invariant
502   */
503  @Override
504  public @Nullable Invariant merge(List<Invariant> invs, PptSlice parent_ppt) {
505
506    // Create the initial parent invariant from the first child
507    EltLowerBoundFloat first = (EltLowerBoundFloat) invs.get(0);
508    EltLowerBoundFloat result= first.clone();
509    result.ppt = parent_ppt;
510
511    // Loop through the rest of the child invariants
512    for (int i = 1; i < invs.size(); i++ ) {
513      EltLowerBoundFloat lb = (EltLowerBoundFloat) invs.get(i);
514      result.core.add(lb.core);
515    }
516
517    result.log("Merged '%s' from %s child invariants", result.format(),invs.size());
518    return result;
519  }
520}