Source code

001package daikon.inv.unary.scalar;
002
003import daikon.PptSlice;
004import daikon.VarInfo;
005import daikon.derive.unary.SequenceLength;
006import daikon.inv.DiscardCode;
007import daikon.inv.DiscardInfo;
008import daikon.inv.Invariant;
009import daikon.inv.InvariantStatus;
010import daikon.inv.OutputFormat;
011import java.util.ArrayList;
012import java.util.Collection;
013import java.util.List;
014import java.util.function.Predicate;
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.MathPlume;
021import typequals.prototype.qual.NonPrototype;
022import typequals.prototype.qual.Prototype;
023
024/**
025 * Represents the invariant {@code x == r (mod m)} where {@code x} is a long scalar variable, {@code
026 * r} is the (constant) remainder, and {@code m} is the (constant) modulus.
027 */
028public class Modulus 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 Modulus invariants should be considered. */
034  public static boolean dkconfig_enabled = false;
035
036  long modulus = 0;
037  long remainder = 0;
038
039  // An arbitrarily-chosen value used for computing the differences among
040  // all the values.  Arbitrary initial value 2222 will be replaced by the
041  // first actual value seen.  Once `remainder` is set, this is of no interest.
042  long value1 = 2222;
043  // used for initializing value1
044  boolean no_samples_seen = true;
045
046  private Modulus(PptSlice ppt) {
047    super(ppt);
048  }
049
050  private @Prototype Modulus() {
051    super();
052  }
053
054  private static @Prototype Modulus proto = new @Prototype Modulus();
055
056  /** Returns the prototype invariant for Modulus. */
057  public static @Prototype Modulus get_proto() {
058    return proto;
059  }
060
061  @Override
062  public boolean enabled() {
063    return dkconfig_enabled;
064  }
065
066  @Override
067  public boolean instantiate_ok(VarInfo[] vis) {
068
069    if (!valid_types(vis)) {
070      return false;
071    }
072
073    return vis[0].file_rep_type.baseIsIntegral();
074  }
075
076  @Override
077  protected Modulus instantiate_dyn(@Prototype Modulus this, PptSlice slice) {
078    return new Modulus(slice);
079  }
080
081  @Override
082  public String repr(@GuardSatisfied Modulus this) {
083    return "Modulus" + varNames() + ": modulus=" + modulus + ",remainder=" + remainder;
084  }
085
086  @SideEffectFree
087  @Override
088  public String format_using(@GuardSatisfied Modulus this, OutputFormat format) {
089    String name = var().name_using(format);
090
091    if (format == OutputFormat.DAIKON) {
092      return var().name() + " == " + remainder + "  (mod " + modulus + ")";
093    }
094
095    if (format.isJavaFamily()) {
096      name = var().name_using(format);
097      if (var().type.isFloat()) {
098        return "daikon.Quant.fuzzy.eq(" + name + " % " + modulus + ", " + remainder + ")";
099      } else {
100        return name + " % " + modulus + " == " + remainder;
101      }
102    }
103
104    if (format == OutputFormat.CSHARPCONTRACT) {
105      return var().csharp_name() + " % " + modulus + " == " + remainder;
106    }
107
108    //   if (format == OutputFormat.JAVA
109    //     || format == OutputFormat.JML) {
110    //   return var().name.name() + " % " + modulus + " == " + remainder;
111    //  }
112
113    if (format == OutputFormat.SIMPLIFY) {
114      if (modulus > 0) {
115        return "(EQ (MOD "
116            + var().simplify_name()
117            + " "
118            + simplify_format_long(modulus)
119            + ") "
120            + simplify_format_long(remainder)
121            + ")";
122      } else {
123        return format_too_few_samples(format, null);
124      }
125    }
126
127    return format_unimplemented(format);
128  }
129
130  @Override
131  public InvariantStatus check_modified(long value, int count) {
132    if (modulus == 1) {
133      // We shouldn't ever get to this case; the invariant should have been
134      // destroyed instead.
135      throw new Error("Modulus = 1");
136    } else if (no_samples_seen) {
137      return InvariantStatus.NO_CHANGE;
138    } else if (value == value1) {
139      // no new information, so nothing to do
140      return InvariantStatus.NO_CHANGE;
141    } else if (modulus == 0) {
142      // only one value seen so far
143      // REACHABLE?
144      if (modulus == 1) {
145        return InvariantStatus.FALSIFIED;
146      }
147    } else {
148      long new_modulus_long = Math.abs(MathPlume.gcd(modulus, value1 - value));
149      int new_modulus;
150      if (new_modulus_long > Integer.MAX_VALUE || (new_modulus_long < Integer.MIN_VALUE)) {
151        new_modulus = 1;
152      } else {
153        new_modulus = (int) new_modulus_long;
154        assert new_modulus > 0;
155      }
156      if (new_modulus != modulus) {
157        if (new_modulus == 1) {
158          return InvariantStatus.FALSIFIED;
159        }
160      }
161    }
162    assert modulus != 1;
163    return InvariantStatus.NO_CHANGE;
164  }
165
166  @Override
167  public InvariantStatus add_modified(long value, int count) {
168    if (modulus == 1) {
169      // We shouldn't ever get to this case; the invariant should have been
170      // destroyed instead.
171      throw new Error(
172          String.format("Modulus = 1 for %s in add_modified(%d, %d)", this, value, count));
173      // assert falsified;
174      // // We already know this confidence fails
175      // return;
176    } else if (no_samples_seen) {
177      value1 = value;
178      no_samples_seen = false;
179      return InvariantStatus.NO_CHANGE;
180    } else if (value == value1) {
181      // no new information, so nothing to do
182      return InvariantStatus.NO_CHANGE;
183    } else if (modulus == 0) {
184      // only one value seen so far
185      long new_modulus = Math.abs(value1 - value);
186
187      if (new_modulus == 1) {
188        return InvariantStatus.FALSIFIED;
189      }
190      modulus = new_modulus;
191      remainder = MathPlume.modNonnegative(value, modulus);
192    } else {
193      long new_modulus_long = Math.abs(MathPlume.gcd(modulus, value1 - value));
194      int new_modulus;
195      if (new_modulus_long > Integer.MAX_VALUE || (new_modulus_long < Integer.MIN_VALUE)) {
196        new_modulus = 1;
197      } else {
198        new_modulus = (int) new_modulus_long;
199        assert new_modulus > 0;
200      }
201      if (new_modulus != modulus) {
202        modulus = new_modulus;
203        if (new_modulus == 1) {
204          return InvariantStatus.FALSIFIED;
205        } else {
206          remainder = remainder % new_modulus;
207        }
208      }
209    }
210    assert modulus != 1;
211    return InvariantStatus.NO_CHANGE;
212  }
213
214  @Override
215  protected double computeConfidence() {
216    if (modulus == 1) {
217      return Invariant.CONFIDENCE_NEVER;
218    }
219    if (modulus == 0) {
220      return Invariant.CONFIDENCE_UNJUSTIFIED;
221    }
222    double probability_one_elt_modulus = 1 - 1.0 / modulus;
223    // return 1 - Math.pow(probability_one_elt_modulus, ppt.num_mod_samples());
224    return 1 - Math.pow(probability_one_elt_modulus, ppt.num_samples());
225  }
226
227  @Pure
228  @Override
229  public boolean isSameFormula(Invariant other) {
230    Modulus otherModulus = (Modulus) other;
231
232    boolean thisMeaningless = (modulus == 0 || modulus == 1);
233    boolean otherMeaningless = (otherModulus.modulus == 0 || otherModulus.modulus == 1);
234
235    if (thisMeaningless && otherMeaningless) {
236      return true;
237    } else {
238      return (modulus != 1)
239          && (modulus != 0)
240          && (modulus == otherModulus.modulus)
241          && (remainder == otherModulus.remainder);
242    }
243  }
244
245  @Pure
246  @Override
247  public boolean isExclusiveFormula(Invariant other) {
248    if ((modulus == 0) || (modulus == 1)) {
249      return false;
250    }
251
252    // Weak test, can be strengthened.
253    //  * x = 1 mod 4  is exclusive with  x = 6 mod 8
254    //  * x = 1 mod 4  is exclusive with  x = 0 mod 2
255    //  * x = 0 mod 4  is exclusive with  1 <= x <= 3
256    if (other instanceof Modulus) {
257      return (modulus == ((Modulus) other).modulus) && (remainder != ((Modulus) other).remainder);
258    } else if (other instanceof NonModulus) {
259      return ((NonModulus) other).hasModulusRemainder(modulus, remainder);
260    }
261
262    return false;
263  }
264
265  // Look up a previously instantiated invariant.
266  public static @Nullable Modulus find(PptSlice ppt) {
267    assert ppt.arity() == 1;
268    for (Invariant inv : ppt.invs) {
269      if (inv instanceof Modulus) {
270        return (Modulus) inv;
271      }
272    }
273    return null;
274  }
275
276  /**
277   * Checks to see if this is obvious over the specified variables. Implements the following checks:
278   *
279   * <pre>
280   *    size(x[]) = r (mod m) &rArr; size(x[])-1 = (r-1) (mod m)
281   * </pre>
282   */
283  @Pure
284  @Override
285  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
286
287    // Do not show x-1 = a (mod b).  There must be a different mod
288    // invariant over x.  JHP: This should really find the invariant rather
289    // than presuming it is true.
290    VarInfo x = vis[0];
291    if ((x.derived instanceof SequenceLength) && (((SequenceLength) x.derived).shift != 0)) {
292      return new DiscardInfo(
293          this,
294          DiscardCode.obvious,
295          "The invariant "
296              + format()
297              + " is implied by a mod invariant "
298              + "over "
299              + x.name()
300              + " without the offset");
301    }
302    return null;
303  }
304
305  @Override
306  public @Nullable @NonPrototype Modulus merge(
307      @Prototype Modulus this, List<@NonPrototype Invariant> invs, PptSlice parent_ppt) {
308
309    long new_modulus = 0;
310    boolean some_value_set = false;
311    long some_value = 0;
312    for (Invariant inv : invs) {
313      Modulus m = (Modulus) inv;
314
315      if (!some_value_set && !m.no_samples_seen) {
316        some_value = m.value1;
317      }
318
319      if (m.modulus == 0) {
320        continue;
321      } else if (new_modulus == 0) {
322        new_modulus = m.modulus;
323      } else {
324        new_modulus = MathPlume.gcd(new_modulus, m.modulus);
325      }
326    }
327    if (new_modulus == 0 || new_modulus == 1) {
328      return null;
329    }
330
331    @SuppressWarnings("nullness") // super.merge does not return null
332    @NonNull Modulus result = (Modulus) super.merge(invs, parent_ppt);
333    result.modulus = new_modulus;
334    result.remainder = some_value % result.modulus;
335
336    for (Invariant inv : invs) {
337      Modulus m = (Modulus) inv;
338      if (!m.no_samples_seen) {
339        InvariantStatus status = result.add_modified(m.remainder, 1);
340        if (status == InvariantStatus.FALSIFIED) {
341          return null;
342        }
343      }
344    }
345
346    return result;
347  }
348
349  // TODO: Move this to plume-util.
350  /**
351   * Returns a new list containing only the elements for which the filter returns true. To modify
352   * the collection in place, use {@code Collection#removeIf}.
353   *
354   * <p>Using streams gives an equivalent list but is less efficient and more verbose:
355   *
356   * <pre>{@code
357   * coll.stream().filter(filter).collect(Collectors.toList());
358   * }</pre>
359   *
360   * @param <T> the type of elements
361   * @param coll a collection
362   * @param filter a predicate
363   * @return a new list with the elements for which the filter returns true
364   */
365  public static <T> List<T> listFilter(Collection<T> coll, Predicate<? super T> filter) {
366    List<T> result = new ArrayList<>();
367    for (T elt : coll) {
368      if (filter.test(elt)) {
369        result.add(elt);
370      }
371    }
372    return result;
373  }
374}