Source code

001// ***** This file is automatically generated from BoundCore.java.jpp
002
003package daikon.inv.unary;
004
005import org.checkerframework.checker.lock.qual.GuardSatisfied;
006import org.checkerframework.dataflow.qual.Pure;
007import org.checkerframework.dataflow.qual.SideEffectFree;
008import daikon.*;
009import daikon.inv.*;
010import java.io.Serializable;
011import java.text.DecimalFormat;
012
013// One reason not to combine LowerBound and Upperbound is that they have
014// separate justifications:  one may be justified when the other is not.
015
016// What should we do if there are few values in the range?
017// This can make justifying that invariant easier, because with few values
018// naturally there are more instances of each value.
019// This might also make justifying that invariant harder, because to get more
020// than (say) twice the expected number of samples (under the assumption of
021// uniform distribution) requires many samples.
022// Which of these dominates?  Is the behavior what I want?
023
024@SuppressWarnings("UnnecessaryParentheses")  // code generated by macros
025public class UpperBoundCore implements Serializable, Cloneable {
026  static final long serialVersionUID = 20030822L;
027
028  static final int required_samples = 5; // for enoughSamples
029  static final int required_samples_at_bound = 3; // for justification
030
031  // max1 > max2 > max3
032  public long max1 = Long.MIN_VALUE;
033  public int num_max1 = 0;
034  public long max2 = Long.MIN_VALUE;
035  public int num_max2 = 0;
036  public long max3 = Long.MIN_VALUE;
037  public int num_max3 = 0;
038  public long min = Long.MAX_VALUE;
039
040  int samples = 0;
041
042  public Invariant wrapper;
043
044  public UpperBoundCore(Invariant wrapper) {
045    this.wrapper = wrapper;
046  }
047
048  public long max() {
049    return max1;
050  }
051
052  @SideEffectFree
053  @Override
054  public UpperBoundCore clone(@GuardSatisfied UpperBoundCore this) {
055    try {
056      return (UpperBoundCore) super.clone();
057    } catch (CloneNotSupportedException e) {
058      throw new Error(); // can't happen
059    }
060  }
061
062  private static DecimalFormat two_decimals = new java.text.DecimalFormat("#.##");
063
064  public String repr(@GuardSatisfied UpperBoundCore this) {
065    long modulus = calc_modulus();
066    long range = calc_range();
067    double avg_samples_per_val = calc_avg_samples_per_val(modulus, (double)(range));
068    return "max1=" + max1
069      + ", num_max1=" + num_max1
070      + ", max2=" + max2
071      + ", num_max2=" + num_max2
072      + ", max3=" + max3
073      + ", num_max3=" + num_max3
074      + ", min=" + min + ", range=" + range + ", "
075      + "avg_samp=" + two_decimals.format(avg_samples_per_val);
076  }
077
078  private double calc_avg_samples_per_val(@GuardSatisfied UpperBoundCore this, long modulus, double range) {
079    // int num_samples = wrapper.ppt.num_mod_samples();
080    int num_samples = wrapper.ppt.num_samples();
081    double avg_samples_per_val =
082      ((double) num_samples) * modulus / range;
083    avg_samples_per_val = Math.min(avg_samples_per_val, 100);
084
085    return avg_samples_per_val;
086  }
087
088  private long calc_range(@GuardSatisfied UpperBoundCore this) {
089    // If I used Math.abs, the order of arguments to minus would not matter.
090    return -(min - max1) + 1;
091  }
092
093  private long calc_modulus(@GuardSatisfied UpperBoundCore this) {
094    // Need to reinstate this at some point.
095    // {
096    //   for (Invariant inv : wrapper.ppt.invs) {
097    //     if ((inv instanceof Modulus) && inv.enoughSamples()) {
098    //       modulus = ((Modulus) inv).modulus;
099    //       break;
100    //     }
101    //   }
102    // }
103    return 1;
104  }
105
106  /**
107   * Whether this would change if the given value was seen. Used to test for need of cloning and
108   * flowing before this would be changed.
109   */
110  public boolean wouldChange(long value) {
111    return (value > max1);
112  }
113
114  public InvariantStatus add_modified(long value, int count) {
115    samples += count;
116
117    // System.out.println("UpperBoundCore" + varNames() + ": "
118    //                    + "add(" + value + ", " + modified + ", " + count + ")");
119
120    long v = value;
121
122    if (v < min) {
123      min = v;
124    }
125
126    if (v == max1) {
127      num_max1 += count;
128    } else if (v > max1) {
129      max3 = max2;
130      num_max3 = num_max2;
131      max2 = max1;
132      num_max2 = num_max1;
133      max1 = v;
134      num_max1 = count;
135      return InvariantStatus.WEAKENED;
136    } else if (v == max2) {
137      num_max2 += count;
138    } else if (v > max2) {
139      max3 = max2;
140      num_max3 = num_max2;
141      max2 = v;
142      num_max2 = count;
143    } else if (v == max3) {
144      num_max3 += count;
145    } else if (v > max3) {
146      max3 = v;
147      num_max3 = count;
148    }
149    return InvariantStatus.NO_CHANGE;
150  }
151
152  public InvariantStatus check(long value) {
153    if (value > max1) {
154      return InvariantStatus.WEAKENED;
155    } else {
156      return InvariantStatus.NO_CHANGE;
157    }
158  }
159
160  public boolean enoughSamples(@GuardSatisfied UpperBoundCore this) {
161    return samples > required_samples;
162  }
163
164  // Convenience methods; avoid need for "Invariant." prefix.
165  private final double prob_is_ge(double x, double goal) {
166    return Invariant.prob_is_ge(x, goal);
167  }
168  private final double prob_and(double p1, double p2) {
169    return Invariant.prob_and(p1, p2);
170  }
171  private final double prob_or(double p1, double p2) {
172    return Invariant.prob_or(p1, p2);
173  }
174
175  public double computeConfidence() {
176    if (PrintInvariants.dkconfig_static_const_infer && matchConstant()) {
177      return Invariant.CONFIDENCE_JUSTIFIED;
178    }
179
180    return 1 - computeProbability();
181  }
182
183  public boolean matchConstant() {
184    PptTopLevel pptt = wrapper.ppt.parent;
185
186    for (VarInfo vi : pptt.var_infos) {
187      if (vi.isStaticConstant()) {
188        if (vi.rep_type == ProglangType.DOUBLE) {
189          // If variable is a double, then use fuzzy comparison
190          Double constantVal = (Double)vi.constantValue();
191          if (Global.fuzzy.eq(constantVal, (double)(max1)) || false) {
192            return true;
193          }
194        } else {
195          // Otherwise just use the equals method
196          Object constantVal = vi.constantValue();
197          if (constantVal.equals(max1)) {
198            return true;
199          }
200        }
201      }
202    }
203
204    return false;
205  }
206
207  // used by computeConfidence
208  public double computeProbability() {
209    // The bound is justified if both of two conditions is satisfied:
210    //  1. there are at least required_samples_at_bound samples at the bound
211    //  2. one of the following holds:
212    //      2a. the bound has five times the expected number of samples (the
213    //          number it would have if the values were uniformly distributed)
214    //      2b. the bound and the two next elements all have at least half
215    //          the expected number of samples.
216    // The expected number of samples is the total number of samples
217    // divided by the range of the samples; it is the average number
218    // of samples at each point.
219
220    // Value "1" from above.
221    double bound_samples_prob = prob_is_ge(num_max1, required_samples_at_bound);
222
223    long modulus = calc_modulus();
224
225    double range = calc_range();
226    double avg_samples_per_val = calc_avg_samples_per_val(modulus, range);
227
228    // Value "2a" from above
229    double trunc_prob = prob_is_ge(num_max1, 5 * avg_samples_per_val);
230
231    // Value "2b" from above
232    double unif_prob;
233    boolean unif_mod_OK = ((-(max3 - max2) == modulus)
234                           && (-(max2 - max1) == modulus));
235    if (unif_mod_OK) {
236      double half_avg_samp = avg_samples_per_val / 2;
237      double unif_prob_1 = prob_is_ge(num_max1, half_avg_samp);
238      double unif_prob_2 = prob_is_ge(num_max2, half_avg_samp);
239      double unif_prob_3 = prob_is_ge(num_max3, half_avg_samp);
240      unif_prob = Invariant.prob_and(unif_prob_1, unif_prob_2, unif_prob_3);
241      // System.out.println("Unif_probs: " + unif_prob + " <-- " + unif_prob_1 + " " + unif_prob_2 + " " + unif_prob_3);
242    } else {
243      unif_prob = 1;
244    }
245
246    // Value "2" from above
247    double bound_prob = prob_or(trunc_prob, unif_prob);
248
249    // Final result
250    return prob_and(bound_samples_prob, bound_prob);
251
252    // System.out.println("UpperBoundCore.computeProbability(): ");
253    // System.out.println("  " + repr());
254    // System.out.println("  ppt=" + wrapper.ppt.name()
255    //                    + ", wrapper.ppt.num_mod_samples()="
256    //                    + wrapper.ppt.num_mod_samples()
257    //                    // + ", values=" + values
258    //                    + ", avg_samples_per_val=" + avg_samples_per_val
259    //                    + ", result = " + result
260    //                    + ", bound_samples_prob=" + bound_samples_prob
261    //                    + ", bound_prob=" + bound_prob
262    //                    + ", trunc_prob=" + trunc_prob
263    //                    + ", unif_prob=" + unif_prob);
264    // PptSlice pptsg = (PptSlice) ppt;
265    // System.out.println("  " + ppt.name());
266
267  }
268
269  @Pure
270  public boolean isSameFormula(UpperBoundCore other) {
271    return max1 == other.max1;
272  }
273
274  @Pure
275  public boolean isExact() {
276    return false;
277  }
278
279  // Merge lbc into this.
280  public void add(UpperBoundCore lbc) {
281
282    // Pass each value and its count to this invariant's add_modified.  Since
283    // bound is never destroyed, we don't need to check the results.
284    if (lbc.num_max1 > 0) {
285      add_modified(lbc.max1, lbc.num_max1);
286    }
287    if (lbc.num_max2 > 0) {
288      add_modified(lbc.max2, lbc.num_max2);
289    }
290    if (lbc.num_max3 > 0) {
291      add_modified(lbc.max3, lbc.num_max3);
292    }
293    // num_max1 will be positive if and only if we've ever seen any
294    // real samples. Only then does min represent a real sample.
295    if (lbc.num_max1 > 0) {
296      add_modified(lbc.min, 1);
297    }
298    if (Debug.logDetail()) {
299      wrapper.log("Added vals %s of %s, %s of %s, %s of %s, %s from ppt %s",
300                   lbc.num_max1, lbc.max1, lbc.num_max2, lbc.max2,
301                   lbc.num_max3, lbc.max3,
302                   ((lbc.num_max1 > 0) ?  "1 of " + lbc.min : ""),
303                   lbc.wrapper.ppt.parent.ppt_name);
304    }
305  }
306}