Source code

001package daikon.inv.unary.scalar;
002
003import daikon.PptSlice;
004import daikon.VarInfo;
005import daikon.inv.Invariant;
006import daikon.inv.InvariantStatus;
007import daikon.inv.OutputFormat;
008import java.util.List;
009import java.util.NavigableSet;
010import java.util.TreeSet;
011import org.checkerframework.checker.lock.qual.GuardSatisfied;
012import org.checkerframework.checker.nullness.qual.NonNull;
013import org.checkerframework.checker.nullness.qual.Nullable;
014import org.checkerframework.dataflow.qual.Pure;
015import org.checkerframework.dataflow.qual.SideEffectFree;
016import org.plumelib.util.Intern;
017import org.plumelib.util.MathPlume;
018import typequals.prototype.qual.NonPrototype;
019import typequals.prototype.qual.Prototype;
020
021/**
022 * Represents long scalars that are never equal to {@code r (mod m)} where all other numbers in the
023 * same range (i.e., all the values that {@code x} doesn't take from {@code min(x)} to {@code
024 * max(x)}) are equal to {@code r (mod m)}. Prints as {@code x != r (mod m)}, where {@code r} is the
025 * remainder and {@code m} is the modulus.
026 */
027public class NonModulus extends SingleScalar {
028  static final long serialVersionUID = 20020122L;
029
030  // Variables starting with dkconfig_ should only be set via the
031  // daikon.config.Configuration interface.
032  /** Boolean. True iff NonModulus invariants should be considered. */
033  public static boolean dkconfig_enabled = false;
034
035  /** The values to be tested for the non-modulus property. */
036  @SuppressWarnings("serial")
037  NavigableSet<Long> elements = new TreeSet<>();
038
039  private long modulus = 0;
040  private long remainder = 0;
041  // The next two variables indicate whether the "modulus" and "result"
042  // fields are up to date.
043  // Indicates that no nonmodulus has been found; maybe with more
044  // samples, one will appear.
045  private boolean no_result_yet = false;
046  // We don't continuously keep the modulus and remainder field up to date.
047  // This indicates whether it is.
048  private boolean results_accurate = false;
049
050  private NonModulus(PptSlice ppt) {
051    super(ppt);
052  }
053
054  private @Prototype NonModulus() {
055    super();
056  }
057
058  private static @Prototype NonModulus proto = new @Prototype NonModulus();
059
060  /** Returns the prototype invariant for NonModulus. */
061  public static @Prototype NonModulus get_proto() {
062    return proto;
063  }
064
065  @Override
066  public boolean instantiate_ok(VarInfo[] vis) {
067
068    if (!valid_types(vis)) {
069      return false;
070    }
071
072    return vis[0].file_rep_type.baseIsIntegral();
073  }
074
075  @Override
076  public boolean enabled() {
077    return dkconfig_enabled;
078  }
079
080  @Override
081  protected NonModulus instantiate_dyn(@Prototype NonModulus this, PptSlice slice) {
082    return new NonModulus(slice);
083  }
084
085  @SideEffectFree
086  @Override
087  public NonModulus clone(@GuardSatisfied NonModulus this) {
088    NonModulus result = (NonModulus) super.clone();
089    result.elements = new TreeSet<Long>(this.elements);
090    return result;
091  }
092
093  @Override
094  public String repr(@GuardSatisfied NonModulus this) {
095    return "NonModulus" + varNames() + ": m=" + modulus + ",r=" + remainder;
096  }
097
098  @SideEffectFree
099  @Override
100  public String format_using(@GuardSatisfied NonModulus this, OutputFormat format) {
101    updateResults();
102    String name = var().name_using(format);
103
104    if (format == OutputFormat.DAIKON) {
105      if (no_result_yet) {
106        return name + " != ? (mod ?) ***";
107      }
108      return name + " != " + remainder + "  (mod " + modulus + ")";
109    }
110
111    if (no_result_yet) {
112      return format_too_few_samples(format, null);
113    }
114
115    if (format.isJavaFamily()) {
116
117      if (var().type.isFloat()) {
118        return "daikon.Quant.fuzzy.ne(" + name + " % " + modulus + ", " + remainder + ")";
119      } else {
120        return name + " % " + modulus + " != " + remainder;
121      }
122    }
123
124    if (format == OutputFormat.CSHARPCONTRACT) {
125      return name + " % " + modulus + " != " + remainder;
126    }
127
128    if (format == OutputFormat.SIMPLIFY) {
129      return "(NEQ (MOD "
130          + var().simplify_name()
131          + " "
132          + simplify_format_long(modulus)
133          + ") "
134          + simplify_format_long(remainder)
135          + ")";
136    }
137
138    return format_unimplemented(format);
139  }
140
141  // Set either modulus and remainder, or no_result_yet.
142  void updateResults(@GuardSatisfied NonModulus this) {
143    if (results_accurate) {
144      return;
145    }
146    if (elements.size() == 0) {
147      no_result_yet = true;
148    } else {
149      // Do I want to communicate back some information about the smallest
150      // possible modulus?
151      long[] result = MathPlume.nonmodulusStrictLong(elements.iterator());
152      if (result == null) {
153        no_result_yet = true;
154      } else {
155        remainder = result[0];
156        modulus = result[1];
157        no_result_yet = false;
158      }
159    }
160    results_accurate = true;
161  }
162
163  @Override
164  public InvariantStatus check_modified(long value, int count) {
165    return InvariantStatus.NO_CHANGE;
166  }
167
168  // XXX have to deal with flowing this; maybe it should live at all ppts?
169  @Override
170  public InvariantStatus add_modified(long value, int count) {
171    if (elements.add(Intern.internedLong(value))
172        && results_accurate
173        && !no_result_yet
174        && (MathPlume.modNonnegative(value, modulus) == remainder)) results_accurate = false;
175    return InvariantStatus.NO_CHANGE;
176  }
177
178  @Override
179  protected double computeConfidence() {
180    updateResults();
181    if (no_result_yet) {
182      return Invariant.CONFIDENCE_UNJUSTIFIED;
183    }
184    double probability_one_elt_nonmodulus = 1 - 1.0 / modulus;
185    // return 1 - Math.pow(probability_one_elt_nonmodulus, ppt.num_mod_samples());
186    return 1 - Math.pow(probability_one_elt_nonmodulus, ppt.num_samples());
187  }
188
189  @Pure
190  @Override
191  public boolean isSameFormula(Invariant o) {
192    NonModulus other = (NonModulus) o;
193
194    updateResults();
195    other.updateResults();
196
197    if (no_result_yet && other.no_result_yet) {
198      return true;
199    } else if (no_result_yet || other.no_result_yet) {
200      return false;
201    } else {
202      return (modulus == other.modulus) && (remainder == other.remainder);
203    }
204  }
205
206  /** Returns true if this has the given modulus and remainder. */
207  public boolean hasModulusRemainder(long modulus, long remainder) {
208    updateResults();
209    if (no_result_yet) {
210      return false;
211    }
212
213    return (modulus == this.modulus) && (remainder == this.remainder);
214  }
215
216  @Pure
217  @Override
218  public boolean isExclusiveFormula(Invariant o) {
219    updateResults();
220    if (no_result_yet) {
221      return false;
222    }
223    if (o instanceof NonModulus) {
224      NonModulus other = (NonModulus) o;
225      other.updateResults();
226      if (other.no_result_yet) {
227        return false;
228      }
229      return (modulus == other.modulus) && (remainder != other.remainder);
230    } else if (o instanceof Modulus) {
231      Modulus other = (Modulus) o;
232      return (modulus == other.modulus) && (remainder == other.remainder);
233    }
234
235    return false;
236  }
237
238  @Override
239  public @Nullable @NonPrototype NonModulus merge(
240      @Prototype NonModulus this, List<@NonPrototype Invariant> invs, PptSlice parent_ppt) {
241    @SuppressWarnings("nullness") // super.merge does not return null
242    @NonNull NonModulus result = (NonModulus) super.merge(invs, parent_ppt);
243    for (Invariant inv : invs) {
244      NonModulus r = (NonModulus) inv;
245      if (result.modulus != r.modulus
246          || result.remainder != r.remainder
247          || result.no_result_yet != r.no_result_yet
248          || result.results_accurate != r.results_accurate) {
249        return null;
250      }
251    }
252    return result;
253  }
254}