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