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