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 LowerBoundCore 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  // min1 < min2 < min3
032  public long min1 = Long.MAX_VALUE;
033  public int num_min1 = 0;
034  public long min2 = Long.MAX_VALUE;
035  public int num_min2 = 0;
036  public long min3 = Long.MAX_VALUE;
037  public int num_min3 = 0;
038  public long max = Long.MIN_VALUE;
039
040  int samples = 0;
041
042  public Invariant wrapper;
043
044  public LowerBoundCore(Invariant wrapper) {
045    this.wrapper = wrapper;
046  }
047
048  public long min() {
049    return min1;
050  }
051
052  @SideEffectFree
053  @Override
054  public LowerBoundCore clone(@GuardSatisfied LowerBoundCore this) {
055    try {
056      return (LowerBoundCore) 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 LowerBoundCore 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 "min1=" + min1
069      + ", num_min1=" + num_min1
070      + ", min2=" + min2
071      + ", num_min2=" + num_min2
072      + ", min3=" + min3
073      + ", num_min3=" + num_min3
074      + ", max=" + max + ", range=" + range + ", "
075      + "avg_samp=" + two_decimals.format(avg_samples_per_val);
076  }
077
078  private double calc_avg_samples_per_val(@GuardSatisfied LowerBoundCore 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    if (min1 == 0) {
086      avg_samples_per_val /= 5;
087    }
088
089    return avg_samples_per_val;
090  }
091
092  private long calc_range(@GuardSatisfied LowerBoundCore this) {
093    // If I used Math.abs, the order of arguments to minus would not matter.
094    return (max - min1) + 1;
095  }
096
097  private long calc_modulus(@GuardSatisfied LowerBoundCore this) {
098    // Need to reinstate this at some point.
099    // {
100    //   for (Invariant inv : wrapper.ppt.invs) {
101    //     if ((inv instanceof Modulus) && inv.enoughSamples()) {
102    //       modulus = ((Modulus) inv).modulus;
103    //       break;
104    //     }
105    //   }
106    // }
107    return 1;
108  }
109
110  /**
111   * Whether this would change if the given value was seen. Used to test for need of cloning and
112   * flowing before this would be changed.
113   */
114  public boolean wouldChange(long value) {
115    return (value < min1);
116  }
117
118  public InvariantStatus add_modified(long value, int count) {
119    samples += count;
120
121    // System.out.println("LowerBoundCore" + varNames() + ": "
122    //                    + "add(" + value + ", " + modified + ", " + count + ")");
123
124    long v = value;
125
126    if (v > max) {
127      max = v;
128    }
129
130    if (v == min1) {
131      num_min1 += count;
132    } else if (v < min1) {
133      min3 = min2;
134      num_min3 = num_min2;
135      min2 = min1;
136      num_min2 = num_min1;
137      min1 = v;
138      num_min1 = count;
139      return InvariantStatus.WEAKENED;
140    } else if (v == min2) {
141      num_min2 += count;
142    } else if (v < min2) {
143      min3 = min2;
144      num_min3 = num_min2;
145      min2 = v;
146      num_min2 = count;
147    } else if (v == min3) {
148      num_min3 += count;
149    } else if (v < min3) {
150      min3 = v;
151      num_min3 = count;
152    }
153    return InvariantStatus.NO_CHANGE;
154  }
155
156  public InvariantStatus check(long value) {
157    if (value < min1) {
158      return InvariantStatus.WEAKENED;
159    } else {
160      return InvariantStatus.NO_CHANGE;
161    }
162  }
163
164  public boolean enoughSamples(@GuardSatisfied LowerBoundCore this) {
165    return samples > required_samples;
166  }
167
168  // Convenience methods; avoid need for "Invariant." prefix.
169  private final double prob_is_ge(double x, double goal) {
170    return Invariant.prob_is_ge(x, goal);
171  }
172  private final double prob_and(double p1, double p2) {
173    return Invariant.prob_and(p1, p2);
174  }
175  private final double prob_or(double p1, double p2) {
176    return Invariant.prob_or(p1, p2);
177  }
178
179  public double computeConfidence() {
180    if (PrintInvariants.dkconfig_static_const_infer && matchConstant()) {
181      return Invariant.CONFIDENCE_JUSTIFIED;
182    }
183
184    return 1 - computeProbability();
185  }
186
187  public boolean matchConstant() {
188    PptTopLevel pptt = wrapper.ppt.parent;
189
190    for (VarInfo vi : pptt.var_infos) {
191      if (vi.isStaticConstant()) {
192        if (vi.rep_type == ProglangType.DOUBLE) {
193          // If variable is a double, then use fuzzy comparison
194          Double constantVal = (Double)vi.constantValue();
195          if (Global.fuzzy.eq(constantVal, (double)(min1)) || false) {
196            return true;
197          }
198        } else {
199          // Otherwise just use the equals method
200          Object constantVal = vi.constantValue();
201          if (constantVal.equals(min1)) {
202            return true;
203          }
204        }
205      }
206    }
207
208    return false;
209  }
210
211  // used by computeConfidence
212  public double computeProbability() {
213    // The bound is justified if both of two conditions is satisfied:
214    //  1. there are at least required_samples_at_bound samples at the bound
215    //  2. one of the following holds:
216    //      2a. the bound has five times the expected number of samples (the
217    //          number it would have if the values were uniformly distributed)
218    //      2b. the bound and the two next elements all have at least half
219    //          the expected number of samples.
220    // The expected number of samples is the total number of samples
221    // divided by the range of the samples; it is the average number
222    // of samples at each point.
223
224    // Value "1" from above.
225    double bound_samples_prob = prob_is_ge(num_min1, required_samples_at_bound);
226
227    long modulus = calc_modulus();
228
229    double range = calc_range();
230    double avg_samples_per_val = calc_avg_samples_per_val(modulus, range);
231
232    // Value "2a" from above
233    double trunc_prob = prob_is_ge(num_min1, 5 * avg_samples_per_val);
234
235    // Value "2b" from above
236    double unif_prob;
237    boolean unif_mod_OK = (((min3 - min2) == modulus)
238                           && ((min2 - min1) == modulus));
239    if (unif_mod_OK) {
240      double half_avg_samp = avg_samples_per_val / 2;
241      double unif_prob_1 = prob_is_ge(num_min1, half_avg_samp);
242      double unif_prob_2 = prob_is_ge(num_min2, half_avg_samp);
243      double unif_prob_3 = prob_is_ge(num_min3, half_avg_samp);
244      unif_prob = Invariant.prob_and(unif_prob_1, unif_prob_2, unif_prob_3);
245      // System.out.println("Unif_probs: " + unif_prob + " <-- " + unif_prob_1 + " " + unif_prob_2 + " " + unif_prob_3);
246    } else {
247      unif_prob = 1;
248    }
249
250    // Value "2" from above
251    double bound_prob = prob_or(trunc_prob, unif_prob);
252
253    // Final result
254    return prob_and(bound_samples_prob, bound_prob);
255
256    // System.out.println("LowerBoundCore.computeProbability(): ");
257    // System.out.println("  " + repr());
258    // System.out.println("  ppt=" + wrapper.ppt.name()
259    //                    + ", wrapper.ppt.num_mod_samples()="
260    //                    + wrapper.ppt.num_mod_samples()
261    //                    // + ", values=" + values
262    //                    + ", avg_samples_per_val=" + avg_samples_per_val
263    //                    + ", result = " + result
264    //                    + ", bound_samples_prob=" + bound_samples_prob
265    //                    + ", bound_prob=" + bound_prob
266    //                    + ", trunc_prob=" + trunc_prob
267    //                    + ", unif_prob=" + unif_prob);
268    // PptSlice pptsg = (PptSlice) ppt;
269    // System.out.println("  " + ppt.name());
270
271  }
272
273  @Pure
274  public boolean isSameFormula(LowerBoundCore other) {
275    return min1 == other.min1;
276  }
277
278  @Pure
279  public boolean isExact() {
280    return false;
281  }
282
283  // Merge lbc into this.
284  public void add(LowerBoundCore lbc) {
285
286    // Pass each value and its count to this invariant's add_modified.  Since
287    // bound is never destroyed, we don't need to check the results.
288    if (lbc.num_min1 > 0) {
289      add_modified(lbc.min1, lbc.num_min1);
290    }
291    if (lbc.num_min2 > 0) {
292      add_modified(lbc.min2, lbc.num_min2);
293    }
294    if (lbc.num_min3 > 0) {
295      add_modified(lbc.min3, lbc.num_min3);
296    }
297    // num_min1 will be positive if and only if we've ever seen any
298    // real samples. Only then does max represent a real sample.
299    if (lbc.num_min1 > 0) {
300      add_modified(lbc.max, 1);
301    }
302    if (Debug.logDetail()) {
303      wrapper.log("Added vals %s of %s, %s of %s, %s of %s, %s from ppt %s",
304                   lbc.num_min1, lbc.min1, lbc.num_min2, lbc.min2,
305                   lbc.num_min3, lbc.min3,
306                   ((lbc.num_min1 > 0) ?  "1 of " + lbc.max : ""),
307                   lbc.wrapper.ppt.parent.ppt_name);
308    }
309  }
310}