Source code

001// ***** This file is automatically generated from EltNonZero.java.jpp
002
003package daikon.inv.unary.sequence;
004
005import daikon.*;
006import daikon.inv.*;
007import daikon.inv.ValueSet;
008import daikon.inv.binary.twoSequence.*;
009import daikon.inv.unary.scalar.*;
010import daikon.suppress.*;
011import java.util.*;
012import java.util.logging.Level;
013import java.util.logging.Logger;
014import org.checkerframework.checker.interning.qual.Interned;
015import org.checkerframework.checker.lock.qual.GuardSatisfied;
016import org.checkerframework.checker.nullness.qual.NonNull;
017import org.checkerframework.checker.nullness.qual.Nullable;
018import org.checkerframework.dataflow.qual.Pure;
019import org.checkerframework.dataflow.qual.SideEffectFree;
020import org.plumelib.util.Intern;
021import typequals.prototype.qual.NonPrototype;
022import typequals.prototype.qual.Prototype;
023
024/**
025 * Represents the invariant "x != 0" where x represents all of the elements of a sequence of
026 * double. Prints as {@code x[] elements != 0}.
027 */
028
029public final class EltNonZeroFloat extends SingleFloatSequence {
030  /** Debug tracer. */
031  public static final Logger debug =
032    Logger.getLogger("daikon.inv.unary.sequence.EltNonZeroFloat");
033
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 EltNonZero invariants should be considered. */
039  public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault;
040
041  EltNonZeroFloat(PptSlice ppt) {
042    super(ppt);
043  }
044
045  @Prototype EltNonZeroFloat() {
046    super();
047  }
048
049  private static @Prototype EltNonZeroFloat proto = new @Prototype EltNonZeroFloat();
050
051  /** Returns the prototype invariant for EltNonZeroFloat */
052  public static @Prototype EltNonZeroFloat get_proto() {
053    return proto;
054  }
055
056  @Override
057  public boolean enabled() {
058    return dkconfig_enabled;
059  }
060
061  @Override
062  protected EltNonZeroFloat instantiate_dyn(@Prototype EltNonZeroFloat this, PptSlice slice) {
063    return new EltNonZeroFloat(slice);
064  }
065
066  /** Returns whether or not the variable is a pointer. */
067  @Pure
068  private boolean is_pointer(@GuardSatisfied EltNonZeroFloat this) {
069    return !ppt.var_infos[0].type.baseIsFloat();
070  }
071
072  @Override
073  public String repr(@GuardSatisfied EltNonZeroFloat this) {
074    return "EltNonZeroFloat" + varNames() + ": "
075      + !falsified;
076  }
077
078  @SideEffectFree
079  @Override
080  public String format_using(@GuardSatisfied EltNonZeroFloat this, OutputFormat format) {
081    if (format.isJavaFamily()) {
082      return format_java_family(format);
083    }
084
085    if (format == OutputFormat.DAIKON) {
086      return format_daikon();
087    }
088    if (format == OutputFormat.ESCJAVA) {
089      return format_esc();
090    }
091    if (format == OutputFormat.CSHARPCONTRACT) {
092      return format_csharp_contract();
093    }
094    if (format == OutputFormat.SIMPLIFY) {
095      return format_simplify();
096    }
097
098    return format_unimplemented(format);
099  }
100
101  public String format_daikon(@GuardSatisfied EltNonZeroFloat this) {
102    return var().name() + " elements != "
103           + (is_pointer() ? "null" : "0");
104  }
105
106  // We are a special case where a ghost field can actually talk about
107  // array contents.
108  @Pure
109  @Override
110  public boolean isValidEscExpression() {
111    return true;
112  }
113
114  public String format_esc(@GuardSatisfied EltNonZeroFloat this) {
115    // If this is an entire array or Collection (not a slice), then
116    //  * for arrays: use \nonnullelements(A)
117    //  * for Collections: use collection.containsNull == false
118    //    (the latter also requires that ghost field to get set)
119
120    // if (var().isDerivedSubSequenceOf() == null) {
121    if (var().is_direct_non_slice_array()) {
122      VarInfo term = var().get_enclosing_var();
123      String esc_name;
124      if (term == null) {
125        // Only happenes in internal format tests
126        esc_name = var().name().replace("[]", "");
127      } else {
128        // System.out.printf("term = %s, var = %s%n", term.name, var().name);
129        esc_name = term.esc_name();
130      }
131      if (var().type.isArray()) {
132        return "\\nonnullelements(" + esc_name + ")";
133      } else {
134        return esc_name + ".containsNull == false";
135      }
136    }
137
138    // If this is just part of an array or Collection (var is a
139    // slice), then calling viname.esc_name() will always throw an
140    // exception, since var() is certainly a sequence.  So use the
141    // standard quantification.
142
143    String[] form = VarInfo.esc_quantify(var());
144    return form[0] + "(" + form[1] + " != "
145           + (is_pointer() ? "null" : "0") + ")" + form[2];
146  }
147
148  public String format_java_family(@GuardSatisfied EltNonZeroFloat this, OutputFormat format) {
149    String retval =
150      "daikon.Quant.eltsNotEqual(" + var().name_using(format)
151      + (is_pointer() ? ", null" : ", 0") + ")";
152
153    return retval;
154  }
155
156  public String format_csharp_contract(@GuardSatisfied EltNonZeroFloat this) {
157    String[] split = var().csharp_array_split();
158    return "Contract.ForAll(" + split[0] + ", x => x" + split[1] + " != " + (is_pointer() ? "null" : "0") + ")";
159  }
160
161  public String format_simplify(@GuardSatisfied EltNonZeroFloat this) {
162    String[] form = VarInfo.simplify_quantify(var());
163    return form[0] + "(NEQ " + form[1] + " "
164      + (is_pointer() ? "null" : "0") + ")" + form[2];
165  }
166
167  @Override
168  @SuppressWarnings("UnnecessaryParentheses")  // generated code, parentheses are sometimes needed
169  public InvariantStatus check_modified(double @Interned [] a, int count) {
170    for (int ai = 0; ai < a.length; ai++) {
171      double v = a[ai];
172
173      if (Global.fuzzy.eq(v, 0)) {
174        return InvariantStatus.FALSIFIED;
175      }
176    }
177    return InvariantStatus.NO_CHANGE;
178  }
179
180  @Override
181  public InvariantStatus add_modified(double @Interned [] a, int count) {
182
183    // if (logOn()) {
184    //  ValueSet.ValueSetFloatArray vs = (ValueSet.ValueSetFloatArray) ppt.var_infos[0].get_value_set();
185    //  log ("max=" + vs.max() + " array=" + Arrays.toString (a));
186    // }
187
188    return check_modified(a, count);
189  }
190
191  @Override
192  protected double computeConfidence() {
193    // Maybe just use 0 as the min or max instead, and see what happens:
194    // see whether the "nonzero" invariant holds anyway.  (Perhaps only
195    // makes sense to do if the {Lower,Upper}Bound invariant doesn't imply
196    // the non-zeroness.)  In that case, do still check for no values yet
197    // received.
198    ValueSet.ValueSetFloatArray vs = (ValueSet.ValueSetFloatArray) ppt.var_infos[0].get_value_set();
199    // log ("is_pointer()=" + is_pointer() + " vs.min=" + vs.min()
200    //       + " vs.max=" + vs.max());
201    if (!is_pointer() && ((vs.min() > 0) || (vs.max() < 0))) {
202      return Invariant.CONFIDENCE_UNJUSTIFIED;
203    } else {
204      double probability_one_elt_nonzero = 1 - confidence_one_elt_nonzero();
205      double result = 1 - Math.pow(probability_one_elt_nonzero, ppt.num_samples());
206      // if ((result < 0) || (result > 1))
207      //  System.err.println ("bad result: vs.max=" + vs.max() + " vs.min="
208      //                      + vs.min() + " conf="
209      //                      + confidence_one_elt_nonzero() + " range="
210      //                      + (vs.max() - vs.min() + 1)/ 1);
211      return result;
212    }
213  }
214
215  @SuppressWarnings("UnnecessaryParentheses")  // generated code, parentheses are sometimes needed
216  private double confidence_one_elt_nonzero() {
217    double range;
218    if (is_pointer()) {
219      range = 3;
220    } else {
221      int modulus = 1;
222
223      // I need to come back and make this work.
224      // {
225      //   for (Invariant inv : ppt.invs) {
226      //     if ((inv instanceof Modulus) && inv.enoughSamples()) {
227      //       modulus = ((Modulus) inv).modulus;
228      //       break;
229      //     }
230      //   }
231      // }
232
233      // Perhaps I ought to check that it's possible (given the modulus
234      // constraints) for the value to be zero; otherwise, the modulus
235      // constraint implies non-zero.
236      ValueSet.ValueSetFloatArray vs = (ValueSet.ValueSetFloatArray) ppt.var_infos[0].get_value_set();
237      range = (vs.max() - vs.min() + 1) / (modulus);
238    }
239    return 1.0/range;
240  }
241
242  @Pure
243  @Override
244  public boolean isSameFormula(Invariant other) {
245    assert other instanceof EltNonZeroFloat;
246    return true;
247  }
248
249  @Pure
250  @Override
251  public boolean isExclusiveFormula(Invariant other) {
252    if (other instanceof EltOneOfFloat) {
253      EltOneOfFloat eoo = (EltOneOfFloat) other;
254      if ((eoo.num_elts() == 1) && (((Double)eoo.elt()).doubleValue() == 0)) {
255        return true;
256      }
257    }
258    return false;
259  }
260
261  @Pure
262  @Override
263  public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) {
264    // This test doesn't seem right: the invariant is obvious if the
265    // elements don't have null, not if the collection doesn't have null.
266    if (!vis[0].aux.hasNull()) {
267      // If it's not a number and null doesn't have special meaning...
268      return new DiscardInfo(this, DiscardCode.obvious, "'null' has no special meaning for " + vis[0].name());
269    }
270    return super.isObviousStatically(vis);
271  }
272
273  @Pure
274  @Override
275  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
276    DiscardInfo super_result = super.isObviousDynamically(vis);
277    if (super_result != null) {
278      return super_result;
279    }
280
281    VarInfo v1 = vis[0];
282
283    // (a[] == []) ==> a[] != 0
284    if (ppt.parent.is_empty(v1)) {
285      return new DiscardInfo(this, DiscardCode.obvious, v1 + "is empty");
286    }
287
288    // (a[] > 0) v (a[] < 0) ==> a[] != 0
289    EltLowerBoundFloat lb = (EltLowerBoundFloat) ppt.parent.find_inv_by_class
290                                                    (vis, EltLowerBoundFloat.class);
291    if ((lb != null) && (lb.min() > 0)) {
292      return new DiscardInfo(this, DiscardCode.obvious, v1 + " > " + lb.min());
293    }
294    EltUpperBoundFloat ub = (EltUpperBoundFloat) ppt.parent.find_inv_by_class
295                                                    (vis, EltUpperBoundFloat.class);
296    if ((ub != null) && (ub.max() < 0)) {
297      return new DiscardInfo(this, DiscardCode.obvious, v1 + " < " + ub.max());
298    }
299
300    // For every other EltNonZero at this program point, see if there is a
301    // subsequence relationship between that array and this one.
302
303    if (debug.isLoggable(Level.FINE)) {
304      debug.fine("Testing isObviousDynamically for " + vis[0].name());
305    }
306
307    PptTopLevel parent = ppt.parent;
308    for (Iterator<Invariant> itor = parent.invariants_iterator(); itor.hasNext(); ) {
309      Invariant inv = itor.next();
310      if ((inv instanceof EltNonZeroFloat) && (inv != this) && inv.enoughSamples()) {
311        VarInfo v2 = inv.ppt.var_infos[0];
312        if (debug.isLoggable(Level.FINE)) {
313          debug.fine("  Have to test: " + inv.repr());
314        }
315
316        if (Debug.logOn()) {
317          Daikon.current_inv = this;
318        }
319        if (parent.is_subsequence(v1, v2)) {
320          return new DiscardInfo(this, DiscardCode.obvious, v1.name()
321                                  + " is a subsequence of " + v2.name());
322        }
323      }
324    }
325
326    return null;
327  }
328
329  // Look up a previously instantiated invariant.
330  public static @Nullable EltNonZeroFloat find(PptSlice ppt) {
331    assert ppt.arity() == 1;
332    for (Invariant inv : ppt.invs) {
333      if (inv instanceof EltNonZeroFloat) {
334        return (EltNonZeroFloat) inv;
335      }
336    }
337    return null;
338  }
339
340  /** NI suppressions, initialized in get_ni_suppressions() */
341  private static @Nullable NISuppressionSet suppressions = null;
342
343  /** returns the ni-suppressions for EltNonZeroFloat */
344  @Pure
345  @Override
346  public NISuppressionSet get_ni_suppressions() {
347    if (suppressions == null) {
348      NISuppressee suppressee = new NISuppressee(EltNonZeroFloat.class, 1);
349
350      // suppressor definitions (used in suppressions below)
351      NISuppressor v_eq_one = new NISuppressor(0, EltRangeFloat.EqualOne.class);
352      NISuppressor v_eq_minus_one = new NISuppressor(0, EltRangeFloat.EqualMinusOne.class);
353
354      suppressions = new NISuppressionSet(
355          new NISuppression[] {
356              // v == 1 ==> v != 0
357              new NISuppression(v_eq_one, suppressee),
358              // v == -1 ==> v != 0
359              new NISuppression(v_eq_minus_one, suppressee),
360          });
361    }
362
363    return suppressions;
364  }
365}