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