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