Source code

001// ***** This file is automatically generated from NonZero.java.jpp
002
003package daikon.inv.unary.scalar;
004
005import daikon.*;
006import daikon.derive.unary.*;
007import daikon.inv.*;
008import daikon.inv.binary.sequenceScalar.*;
009import daikon.inv.unary.sequence.*;
010import java.util.*;
011import java.util.logging.Level;
012import java.util.logging.Logger;
013import org.checkerframework.checker.lock.qual.GuardSatisfied;
014import org.checkerframework.checker.nullness.qual.Nullable;
015import org.checkerframework.dataflow.qual.Pure;
016import org.checkerframework.dataflow.qual.SideEffectFree;
017import org.plumelib.util.Intern;
018import typequals.prototype.qual.NonPrototype;
019import typequals.prototype.qual.Prototype;
020
021// This also serves as NonNull.
022
023/**
024 * Represents long scalars that are non-zero. Prints as {@code x != 0}, or as {@code x !=
025 * null} for pointer types.
026 */
027
028public class NonZero extends SingleScalar {
029  // We are Serializable, so we specify a version to allow changes to
030  // method signatures without breaking serialization.  If you add or
031  // remove fields, you should change this number to the current date.
032  static final long serialVersionUID = 20030822L;
033
034  // Variables starting with dkconfig_ should only be set via the
035  // daikon.config.Configuration interface.
036  /** Boolean. True iff NonZero invariants should be considered. */
037  public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault;
038
039  /** Debug tracer. */
040  public static final Logger debug = Logger.getLogger("daikon.inv.unary.scalar.NonZero");
041
042  /** Maximum value ever used for max-min in confidence calculation. */
043  static long range_max = 50;
044
045  private NonZero(PptSlice ppt) {
046    super(ppt);
047  }
048
049  private @Prototype NonZero() {
050    super();
051  }
052
053  private static @Prototype NonZero proto = new @Prototype NonZero();
054
055  /** Returns the prototype invariant for NonZero */
056  public static @Prototype NonZero get_proto() {
057    return proto;
058  }
059
060  /** returns whether or not this invariant is enabled */
061  @Override
062  public boolean enabled() {
063    return dkconfig_enabled;
064  }
065
066  /** Make sure the NonZero make sense on these vars. */
067  @Override
068  public boolean instantiate_ok(VarInfo[] vis) {
069
070    if (!valid_types(vis)) {
071      return false;
072    }
073
074    if (vis[0].aux.isStruct()
075        || vis[0].aux.isNonNull()
076        || !vis[0].aux.hasNull())
077      return false;
078
079    return true;
080  }
081
082  /** instantiate an invariant on the specified slice */
083  @Override
084  public NonZero instantiate_dyn(@Prototype NonZero this, PptSlice slice) {
085    return new NonZero(slice);
086  }
087
088  private String zero(@GuardSatisfied @Prototype NonZero this, @SuppressWarnings("UnusedVariable") OutputFormat format) {
089
090    if (is_pointer()) {
091      return "null";
092    } else {
093      return "0";
094    }
095
096  }
097
098  @SideEffectFree
099  @Override
100  public String format_using(@GuardSatisfied @Prototype NonZero this, OutputFormat format) {
101    // // var() fails for prototype invariants
102    // if (ppt == null) {
103    //   return "Prototype NonZero invariant (ppt == null)";
104    // }
105
106    String name = var().name_using(format);
107
108    if (format.isJavaFamily()) {
109
110        return name + " != " + zero(format);
111    }
112
113    if ((format == OutputFormat.DAIKON)
114        || (format == OutputFormat.ESCJAVA)
115        || (format == OutputFormat.CSHARPCONTRACT)) {
116      return name + " != " + zero(format);
117    }
118
119    if (format == OutputFormat.SIMPLIFY) {
120      return "(NEQ " + var().simplifyFixup(name) + " " + zero(format) + ")";
121    }
122
123    return format_unimplemented(format);
124  }
125
126  @Override
127  public InvariantStatus check_modified(long v, int count) {
128    if (v == 0) {
129      return InvariantStatus.FALSIFIED;
130    } else {
131      return InvariantStatus.NO_CHANGE;
132    }
133  }
134
135  @Override
136  public InvariantStatus add_modified(long v, int count) {
137    InvariantStatus status = check_modified(v, count);
138    if (status == InvariantStatus.FALSIFIED) {
139      if (logOn()) {
140        log(debug, "falsified (value = " + v + ")");
141      }
142    } // else if (logDetail())
143      // log ("add_modified (" + v + ")");
144    return status;
145  }
146
147  /** Returns whether or not the variable is a pointer. */
148  @Pure
149  private boolean is_pointer(@GuardSatisfied NonZero this) {
150    return ppt.var_infos[0].file_rep_type == ProglangType.HASHCODE;
151  }
152
153  @Override
154  protected double computeConfidence() {
155    return 1 - computeProbability();
156  }
157
158  // used by computeConfidence
159  protected double computeProbability() {
160    assert ! falsified;
161    // This method works by looking at all sample values and
162    // calculating the probability that they were all non-zero by
163    // chance (assuming a uniform distribution).  If the variable is
164    // not a pointer, the range used is the observed range from sample
165    // data.  Further observed constraints are used to change the
166    // returned probability, such as all samples being congruent some
167    // modulus.
168
169    ValueSet.ValueSetScalar vs = (ValueSet.ValueSetScalar) ppt.var_infos[0].get_value_set();
170
171    // If greater than or less than 0, the bounds invariant will be more
172    // interesting
173    if (!is_pointer() && ((vs.min() > 0) || (vs.max() < 0))) {
174
175      // Maybe just use 0 as the min or max instead, and see what happens:
176      // see whether the "nonzero" invariant holds anyway.  (Perhaps only
177      // makes sense to do if the {Lower,Upper}Bound invariant doesn't imply
178      // the non-zeroness.)  In that case, do still check for no values yet
179      // received.
180      return Invariant.PROBABILITY_UNJUSTIFIED;
181    } else {
182      long range;
183      if (is_pointer()) {
184        range = 3;
185      } else {
186        long modulus = 1;
187        {
188          Modulus mi = Modulus.find(ppt);
189          if (mi != null) {
190            modulus = mi.modulus;
191          }
192        }
193        // Perhaps I ought to check that it's possible (given the modulus
194        // constraints) for the value to be zero; otherwise, the modulus
195        // constraint implies non-zero.
196        range = (vs.max() - vs.min() + 1) / modulus;
197      }
198      if ((range_max != 0) && (range > range_max)) {
199        range = range_max;
200      }
201
202      double probability_one_elt_nonzero = 1 - 1.0/range;
203      // This could underflow; so consider doing
204      //   double log_probability = self.samples*math.log(probability);
205      // then calling Math.exp (if the value is in the range that wouldn't
206      // cause underflow).
207      // return Math.pow(probability_one_elt_nonzero, ppt.num_mod_samples());
208      return Math.pow(probability_one_elt_nonzero, ppt.num_samples());
209    }
210  }
211
212  @Pure
213  @Override
214  public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) {
215    VarInfo var = vis[0];
216
217    if (var.aux.isStruct()) {
218      return new DiscardInfo(this, DiscardCode.obvious,
219                             var.name() + " is a struct");
220    }
221
222    if (var.aux.isNonNull()) {
223      return new DiscardInfo(this, DiscardCode.obvious,
224                             "aux information says " + var.name() + " is non-null");
225    }
226
227    if (!var.aux.hasNull()) {
228      return new DiscardInfo(this, DiscardCode.obvious,
229                     "'null' has no special meaning for " + var.name());
230    }
231
232    return super.isObviousStatically(vis);
233  }
234
235  @Pure
236  @Override
237  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
238    DiscardInfo super_result = super.isObviousDynamically(vis);
239    if (super_result != null) {
240      return super_result;
241    }
242
243    VarInfo var = vis[0];
244
245    Debug dlog = new Debug(getClass(), ppt, vis);
246
247    if (logOn()) {
248      dlog.log("Checking IsObviousDynamically");
249    }
250
251    // System.out.println("isObviousImplied: " + format());
252
253    // For every EltNonZero at this program point, see if this variable is
254    // an obvious member of that sequence.
255    PptTopLevel parent = ppt.parent;
256    for (Iterator<Invariant> itor = parent.invariants_iterator(); itor.hasNext(); ) {
257      Invariant inv = itor.next();
258      if ((inv instanceof EltNonZero) && inv.enoughSamples()) {
259        VarInfo v2 = inv.ppt.var_infos[0];
260        // System.out.println("NonZero.isObviousImplied: calling Member.isObviousMember(" + var.name + ", " + v2.name + ")");
261        // Don't use isEqualToObviousMember:  that is too subtle
262        // and eliminates desirable invariants such as "return != null".
263        if (Member.isObviousMember(var, v2)) {
264          // System.out.println("NonZero.isObviousImplied: Member.isObviousMember(" + var.name + ", " + v2.name + ") = true");
265          if (logOn()) {
266            dlog.log("isObvDyn- true, arg is member of nonzero sequence");
267          }
268          String discardString = var.name() + " is a member of the non-zero sequence " + v2.name();
269          if (logOn()) {
270            log("%s obviously implied from %s", format(), inv.format());
271          }
272          return new DiscardInfo(this, DiscardCode.obvious, discardString);
273        }
274      }
275    }
276
277    if ((var.derived != null)
278        && (var.derived instanceof SequenceInitial)) {
279      SequenceInitial si = (SequenceInitial) var.derived;
280      if (si.index == 0) {
281
282        // For each sequence variable, if var is an obvious member, and
283        // the sequence has the same invariant, then this one is obvious.
284        PptTopLevel pptt = ppt.parent;
285        for (int i = 0; i < pptt.var_infos.length; i++) {
286          VarInfo vi = pptt.var_infos[i];
287          if (Member.isObviousMember(var, vi)) {
288            PptSlice1 other_slice = pptt.findSlice(vi);
289            if (other_slice != null) {
290              SeqIndexIntNonEqual sine = SeqIndexIntNonEqual.find(other_slice);
291              if ((sine != null) && sine.enoughSamples()) {
292                // System.out.println("NonZero.isObviousImplied true due to: " + sine.format());
293                if (logOn()) {
294                  dlog.log("isObvDyn- true due to " + sine.format());
295                }
296                String discardString = var.name() + " is a member of the non-zero sequence " + vi.name();
297                return new DiscardInfo(this, DiscardCode.obvious, discardString);
298              }
299            }
300          }
301        }
302      }
303    }
304
305    return null;
306  }
307
308  @Pure
309  @Override
310  public boolean isSameFormula(Invariant other) {
311    assert other instanceof NonZero;
312    return true;
313  }
314
315  @Pure
316  @Override
317  public boolean isExclusiveFormula(Invariant other) {
318    if (other instanceof OneOfScalar) {
319      OneOfScalar oos = (OneOfScalar) other;
320      if ((oos.num_elts() == 1) && (((Long)oos.elt()).longValue() == 0)) {
321        return true;
322      }
323    }
324    return false;
325  }
326}