001package daikon.inv;
002
003import daikon.Debug;
004import daikon.Global;
005import daikon.PptSlice;
006import daikon.PptTopLevel;
007import daikon.Quantify.QuantFlags;
008import daikon.ValueTuple;
009import daikon.VarComparability;
010import daikon.VarInfo;
011import java.util.ArrayList;
012import java.util.Collection;
013import java.util.Collections;
014import java.util.Iterator;
015import java.util.List;
016import java.util.Set;
017import java.util.TreeSet;
018import java.util.logging.Level;
019import java.util.logging.Logger;
020import org.checkerframework.checker.initialization.qual.UnknownInitialization;
021import org.checkerframework.checker.lock.qual.GuardSatisfied;
022import org.checkerframework.checker.nullness.qual.Nullable;
023import org.checkerframework.dataflow.qual.Pure;
024import org.checkerframework.dataflow.qual.SideEffectFree;
025import typequals.prototype.qual.NonPrototype;
026import typequals.prototype.qual.Prototype;
027
028// Note that this Invariant is used in a *very* different way from
029// the same-named one in V2.  In V2, this is just for printing.  In V3,
030// this does all the canonicalizing, etc.
031
032// This is a Java (not Javadoc) comment because the Daikon user manual
033// reproduces the Javadoc but doesn't need all these implementation
034// details.
035//
036// During checking, Equality keeps track of variables that are
037// comparable and equal, so we only need to instantiate (other)
038// invariants for one member of each Equal set, the leader.
039//
040// During postProcessing, each instance of Equality instantiates into
041// displaying several EqualityComparison invariants ("x == y", "x ==
042// z").  Equality invariants have leaders, which are the canonical
043// forms of their variables.  In the previous example, x is the
044// leader.  Equality invariants sort their variables by index ordering
045// during checking.  During printing, however, equality invariants may
046// "pivot" -- that is, switch leaders if the current leader wouldn't
047// be printed because it was not an interesting variable.  Notice that
048// when pivoting, all the other invariants based on this.leader also
049// need to be pivoted.
050
051/**
052 * Keeps track of sets of variables that are equal. Other invariants are instantiated for only one
053 * member of the Equality set, the leader. If variables {@code x}, {@code y}, and {@code z} are
054 * members of the Equality set and {@code x} is chosen as the leader, then the Equality will
055 * internally convert into binary comparison invariants that print as {@code x == y} and {@code x ==
056 * z}.
057 */
058public final /*(at)Interned*/ class Equality extends Invariant {
059  static final long serialVersionUID = 20021231L;
060
061  public static final Logger debug = Logger.getLogger("daikon.inv.Equality");
062
063  public static final Logger debugPostProcess = Logger.getLogger("daikon.inv.Equality.postProcess");
064
065  /** How many samples this has seen. */
066  private int numSamples;
067
068  public void setSamples(int sample_cnt) {
069    numSamples = sample_cnt;
070  }
071
072  public int numSamples(@GuardSatisfied Equality this) {
073    return numSamples;
074  }
075
076  /**
077   * The Set of VarInfos that this represents equality for. Can change over time as this invariant
078   * weakens. Sorted by index until pivoting.
079   */
080  private TreeSet<VarInfo> vars;
081
082  /** Returns the number of variables in the set. */
083  @Pure
084  public int size(@GuardSatisfied Equality this) {
085    return vars.size();
086  }
087
088  /** Returns the variables in their index order. Unmodifiable. */
089  public Set<VarInfo> getVars() {
090    return Collections.unmodifiableSet(vars);
091  }
092
093  /**
094   * Creates a new Equality invariant.
095   *
096   * @param variables variables that are equivalent, with the canonical one first
097   * @param ppt the program point
098   */
099  @SuppressWarnings("initialization.field.write.initialized") // weakness of FBC type system
100  public Equality(Collection<VarInfo> variables, PptSlice ppt) {
101    super(ppt);
102    if (debug.isLoggable(Level.FINE)) {
103      debug.fine("Creating at " + ppt.parent.name() + " vars: ");
104    }
105
106    numSamples = 0;
107    vars = new TreeSet<VarInfo>(VarInfo.IndexComparator.theInstance);
108    vars.addAll(variables);
109    VarInfo leader = leader();
110
111    // Ensure well-formedness and set equality slots.
112    assert !variables.isEmpty();
113    assert vars.size() == variables.size();
114
115    for (VarInfo vi : variables) {
116      if (debug.isLoggable(Level.FINE)) {
117        debug.fine("  " + vi.name() + " [" + vi.comparability + "]");
118      }
119      assert vi.ppt == leader.ppt;
120      assert vi.comparableNWay(leader);
121      assert VarComparability.comparable(leader, vi)
122          : "not comparable " + leader.name() + " " + vi.name() + " at ppt " + ppt.parent.name();
123      assert vi.rep_type.isArray() == leader.rep_type.isArray();
124      vi.equalitySet = this;
125    }
126  }
127
128  // ////////////////////////
129  // Accessors
130
131  private @Nullable VarInfo leaderCache = null;
132
133  /**
134   * Returns the canonical VarInfo of this. Note that the leader never changes.
135   *
136   * @return the canonical VarInfo of this
137   */
138  @SuppressWarnings("all:purity") // set cache field
139  @Pure
140  public VarInfo leader(@GuardSatisfied @UnknownInitialization(Equality.class) Equality this) {
141    if (leaderCache == null) {
142      leaderCache = vars.iterator().next();
143    }
144    return leaderCache;
145  }
146
147  public boolean hasNonCanonicalVariable() {
148    throw new Error("Illegal operation on Equality invariant");
149  }
150
151  /**
152   * Always return JUSTIFIED because we aggregate EqualityComparison invariants that are all
153   * justified to the confidence_limit threshold.
154   */
155  @Override
156  public double computeConfidence() {
157    return Invariant.CONFIDENCE_JUSTIFIED;
158  }
159
160  // ////////////////////////
161  // Printing
162
163  // The format methods aren't called, because for output, we
164  // convert to normal two-way IntEqual type invariants.  However,
165  // they can be called if desired.
166
167  @Override
168  public String repr(@GuardSatisfied Equality this) {
169    return "Equality: size="
170        + size()
171        + " leader: "
172        + leader().name()
173        + " with "
174        + format_daikon()
175        + " samples: "
176        + numSamples();
177  }
178
179  @SideEffectFree
180  @Override
181  public String format_using(@GuardSatisfied Equality this, OutputFormat format) {
182
183    if (format.isJavaFamily()) {
184      return format_java_family(format);
185    }
186
187    if (format == OutputFormat.DAIKON) {
188      return format_daikon();
189    }
190    if (format == OutputFormat.ESCJAVA) {
191      return format_esc();
192    }
193    // Commented out by MDE 7/27/2003.  I can't figure out whether
194    // to just change JAVA_IDENTIFIER to IDENTIFIER, or whether other
195    // changes are also necessary.
196    // if (format == OutputFormat.JAVA_IDENTIFIER) {
197    //   return format_java();
198    // }
199    if (format == OutputFormat.SIMPLIFY) {
200      return format_simplify();
201    }
202    return format_unimplemented(format);
203  }
204
205  public String format_daikon(@GuardSatisfied Equality this) {
206    StringBuilder result = new StringBuilder();
207    boolean start = true;
208    for (VarInfo var : vars) {
209      if (!start) {
210        result.append(" == ");
211      } else {
212        start = false;
213      }
214      result.append(var.name());
215      result.append("[" + var.varinfo_index + "]");
216      // result.append("[" + var.comparability + "]");
217      if (var == leader()) {
218        result.append("L");
219      }
220    }
221    return result.toString();
222  }
223
224  public String format_java() {
225    VarInfo leader = leader();
226    String leaderName = leader.name();
227    List<String> clauses = new ArrayList<>();
228    for (VarInfo var : vars) {
229      if (leader == var) {
230        continue;
231      }
232      clauses.add(String.format("(%s == %s)", leaderName, var.name()));
233    }
234    return String.join(" && ", clauses);
235  }
236
237  public String format_esc(@GuardSatisfied Equality this) {
238    String result = "";
239
240    List<VarInfo> valid_equiv = new ArrayList<>();
241    List<VarInfo> invalid_equiv = new ArrayList<>();
242
243    List<VarInfo> equal_vars = new ArrayList<>();
244
245    for (VarInfo other : vars) {
246      if (other.isDerivedSequenceMinMaxSum()) {
247        break;
248      }
249      if (other.isValidEscExpression()) {
250        valid_equiv.add(other);
251      } else {
252        invalid_equiv.add(other);
253      }
254    }
255    // Choose a leader, preferring the valid variables.
256    VarInfo leader;
257    if (!valid_equiv.isEmpty()) {
258      leader = valid_equiv.get(0);
259    } else {
260      assert !invalid_equiv.isEmpty();
261      leader = invalid_equiv.get(0);
262    }
263    // Print the equality statements, stating expressible ones first.
264    equal_vars.clear();
265    equal_vars.addAll(valid_equiv);
266    equal_vars.addAll(invalid_equiv);
267    int numprinted = 0;
268    for (int j = 0; j < equal_vars.size(); j++) {
269      VarInfo other = equal_vars.get(j);
270      if (other == leader) {
271        continue;
272      }
273      if (leader.prestate_name().equals(other.name())) {
274        continue;
275      }
276      if (other.prestate_name().equals(leader.name())) {
277        continue;
278      }
279      if (numprinted > 0) {
280        result += Global.lineSep;
281      }
282      numprinted++;
283      if (j >= valid_equiv.size()) {
284        result =
285            result + "warning: method Equality.format_esc() needs to be implemented: " + format();
286      }
287      if (leader.rep_type.isArray()) {
288        String[] form = VarInfo.esc_quantify(leader, other);
289        result = result + form[0] + "( " + form[1] + " == " + form[2] + " )" + form[3];
290      } else {
291        result = result + leader.esc_name() + " == " + other.esc_name();
292      }
293    }
294    return result;
295  }
296
297  // When A and B are pointers, don't say (EQ A B); instead say (EQ
298  // (hash A) (hash B)).  If we said the former, Simplify would
299  // presume that A and B were always interchangeable, which is not
300  // the case when your programming language involves mutation.
301  private String format_elt(@GuardSatisfied Equality this, String simname) {
302    String result = simname;
303    if (leader().is_reference()) {
304      result = "(hash " + result + ")";
305    }
306    return result;
307  }
308
309  public String format_simplify(@GuardSatisfied Equality this) {
310    StringBuilder result = new StringBuilder("(AND");
311    VarInfo leader = leader();
312    String leaderName = leader.simplify_name();
313    if (leader.rep_type.isArray()) {
314      for (VarInfo var : vars) {
315        if (var == leader) {
316          continue;
317        }
318        String[] form = VarInfo.simplify_quantify(QuantFlags.element_wise(), leader, var);
319        String a = format_elt(form[1]);
320        String b = format_elt(form[2]);
321        result.append(" ");
322        result.append(form[0]);
323        result.append("(EQ ");
324        result.append(a);
325        result.append(" ");
326        result.append(b);
327        result.append(")");
328        result.append(form[3]);
329      }
330    } else {
331      for (VarInfo var : vars) {
332        if (var == leader) {
333          continue;
334        }
335        String a = format_elt(leaderName);
336        String b = format_elt(var.simplify_name());
337        result.append(" (EQ ");
338        result.append(a);
339        result.append(" ");
340        result.append(b);
341        result.append(")");
342      }
343    }
344    result.append(")");
345    return result.toString();
346  }
347
348  public String shortString() {
349    return format_daikon();
350  }
351
352  public String format_java_family(@GuardSatisfied Equality this, OutputFormat format) {
353    VarInfo leader = leader();
354    String leaderName = leader.name_using(format);
355    List<String> clauses = new ArrayList<>();
356    for (VarInfo var : vars) {
357      if (leader == var) {
358        continue;
359      }
360      if (leader.rep_type.isArray()) {
361        clauses.add(
362            String.format(
363                "(daikon.Quant.pairwiseEqual(%s, %s)", leaderName, var.name_using(format)));
364      } else {
365        if (leader.type.isFloat()) {
366          clauses.add("(" + Invariant.formatFuzzy("eq", leader, var, format) + ")");
367        } else {
368          if ((leaderName.indexOf("daikon.Quant.collectObject") != -1)
369              || (var.name_using(format).indexOf("daikon.Quant.collectObject") != -1)) {
370            clauses.add(
371                "(warning: it is meaningless to compare hashcodes for values "
372                    + "obtained through daikon.Quant.collect... methods.");
373          } else {
374            clauses.add(String.format("(%s == %s)", leaderName, var.name_using(format)));
375          }
376        }
377      }
378    }
379    return String.join(" && ", clauses);
380  }
381
382  @SideEffectFree
383  @Override
384  public String toString(@GuardSatisfied Equality this) {
385    return repr();
386  }
387
388  // //////////////////////////////////////////////////////////////////////
389  // Processing of data
390
391  /**
392   * Returns a List of VarInfos that do not fit into this set anymore.
393   *
394   * <p>Originally (8/14/2003), this did not check for the modified bits. It seems however, quite
395   * wrong to leave variables in the same equality set when one is missing and the other is not.
396   * It's possible we should go farther and break out of the equality set any variable that is
397   * missingOutOfBounds (JHP).
398   *
399   * @param vt the newly-observed sample
400   * @param count the number of times the sample is seen
401   * @return a List of VarInfos that do not fit into this set anymore
402   */
403  public List<VarInfo> add(ValueTuple vt, int count) {
404    // Need to handle specially if leader is missing.
405    VarInfo leader = leader();
406    Object leaderValue = leader.getValueOrNull(vt);
407    int leaderMod = leader.getModified(vt);
408    boolean leaderOutOfBounds = leader.missingOutOfBounds();
409    if (leader.isMissing(vt)) {
410    } else {
411      numSamples += count;
412    }
413
414    List<VarInfo> result = new ArrayList<>();
415    if (debug.isLoggable(Level.FINE)) {
416      debug.fine("Doing add at " + this.ppt.parent.name() + " for " + this);
417    }
418    for (Iterator<VarInfo> i = vars.iterator(); i.hasNext(); ) {
419      VarInfo vi = i.next();
420      if (vi == leader) {
421        continue;
422      }
423      assert vi.comparableNWay(leader);
424      Object viValue = vi.getValueOrNull(vt);
425      int viMod = vi.getModified(vt);
426      // The following is possible because values are interned.  The
427      // test also takes into account missing values, since they are
428      // null.
429      if ((leaderValue == viValue)
430          && (leaderMod == viMod)
431          && !leaderOutOfBounds
432          && !vi.missingOutOfBounds()
433          // If the values are NaN, treat them as different.
434          && !((leaderValue instanceof Double) && ((Double) leaderValue).isNaN())) {
435        // The values are the same.
436        continue;
437      }
438      // The values differ.  Remove this from the equality set.
439
440      //       if (debug.isLoggable(Level.FINE)) {
441      //         debug.fine ("  vi name: " + vi.name.name());
442      //         debug.fine ("  vi value: " + viValue);
443      //         debug.fine ("  le value: " + leaderValue);
444      //       }
445      if (Debug.logOn()) {
446        Debug.log(
447            getClass(),
448            ppt.parent,
449            Debug.vis(vi),
450            "Var "
451                + vi.name()
452                + " ["
453                + viValue
454                + ","
455                + viMod
456                + "] split from leader "
457                + leader.name()
458                + " ["
459                + Debug.toString(leaderValue)
460                + ","
461                + leaderMod
462                + "]");
463      }
464
465      result.add(vi);
466      i.remove();
467    }
468
469    return result;
470  }
471
472  //  This method isn't going to be called, but it's declared abstract in Invariant.
473  @Override
474  protected Invariant resurrect_done(int[] permutation) {
475    throw new UnsupportedOperationException();
476  }
477
478  //  This method isn't going to be called, but it's declared abstract in Invariant.
479  @Pure
480  @Override
481  public boolean isSameFormula(Invariant other) {
482    throw new UnsupportedOperationException(
483        "Equality.isSameFormula(): this method should not be called");
484  }
485
486  /**
487   * Convert Equality invariants into normal IntEqual type for filtering, printing, etc. Add these
488   * to parent.
489   *
490   * <p>If the leader was changed to not be the first member of the group adds leader == leader
491   * invariant as well since that invariant is used in suppressions and obvious tests.
492   */
493  public void postProcess() {
494    if (this.numSamples() == 0) {
495      // All were missing or not present
496      return;
497    }
498    PptTopLevel parent = this.ppt.parent;
499    VarInfo[] varArray = this.vars.toArray(new VarInfo[0]);
500    if (debugPostProcess.isLoggable(Level.FINE)) {
501      debugPostProcess.fine("Doing postProcess: " + this.format_daikon());
502      debugPostProcess.fine("  at: " + this.ppt.parent.name());
503    }
504    VarInfo leader = leader();
505
506    if (debugPostProcess.isLoggable(Level.FINE)) {
507      debugPostProcess.fine("  var1: " + leader.name());
508    }
509    for (int i = 0; i < varArray.length; i++) {
510      if (varArray[i] == leader) {
511        continue;
512      }
513      if (debugPostProcess.isLoggable(Level.FINE)) {
514        debugPostProcess.fine("  var2: " + varArray[i].name());
515      }
516
517      // Guard to prevent creating unnecessary Equality invariants related to
518      // purity method black boxing
519      if (leader.function_args != null
520          && varArray[i].function_args != null
521          && leader.function_args.size() > 1
522          && leader.function_args.size() == varArray[i].function_args.size()) {
523        boolean allEqual = true;
524        for (int j = 0; j < leader.function_args.size(); j++) {
525          if (!leader.function_args.get(j).isEqualTo(varArray[i].function_args.get(j))) {
526            allEqual = false;
527            break;
528          }
529        }
530        if (allEqual) {
531          continue;
532        }
533      }
534
535      parent.create_equality_inv(leader, varArray[i], numSamples());
536    }
537  }
538
539  /**
540   * Switch the leader of this invariant, if possible, to a more canonical VarInfo: a VarInfo that
541   * is not isDerived() is better than one that is; one that is not isDerivedParamAndUninteresting()
542   * is better than one that is; and other things being equal, choose the least complex name. Call
543   * this only after postProcess has been called. We do a pivot so that anything that's interesting
544   * to be printed gets printed and not filtered out. For example, if a == b and a is the leader,
545   * but not interesting, we still want to print f(b) as an invariant. Thus we pivot b to be the
546   * leader. Later on, each relevant PptSlice gets pivoted. But not here.
547   */
548  public void pivot() {
549    VarInfo newLeader = null;
550    for (VarInfo var : vars) {
551      // System.out.printf("  processing %s%n", var);
552      if (newLeader == null) {
553        newLeader = var;
554      } else if (newLeader.isDerivedParamAndUninteresting()
555          && !var.isDerivedParamAndUninteresting()) {
556        // System.out.printf("%s derived and uninteresting, %s is leader%n",
557        //                   newLeader, var);
558        newLeader = var;
559      } else if (var.isDerivedParamAndUninteresting()
560          && !newLeader.isDerivedParamAndUninteresting()) {
561        // do nothing
562      } else if (var.derivedDepth() < newLeader.derivedDepth()) {
563        // System.out.printf("%s greater depth, %s is leader%n",
564        //                    newLeader, var);
565        newLeader = var;
566      } else if (var.derivedDepth() > newLeader.derivedDepth()) {
567        // do nothing
568      }
569      // if we got here, this is the "all other things being equal" case
570      else if (var.complexity() < newLeader.complexity()) {
571        // System.out.printf("%s greater complexity, %s is leader%n",
572        //                   newLeader, var);
573        newLeader = var;
574      }
575    }
576    // System.out.printf("%s complexity = %d, %s complexity = %d%n", leaderCache,
577    //                    leaderCache.complexity(), newLeader,
578    //                    newLeader.complexity());
579    leaderCache = newLeader;
580  }
581
582  @Override
583  public void repCheck() {
584    super.repCheck();
585    VarInfo leader = leader();
586    for (VarInfo var : vars) {
587      assert VarComparability.comparable(leader, var)
588          : "not comparable: " + leader.name() + " " + var.name() + " at ppt " + ppt.parent.name();
589    }
590  }
591
592  @Override
593  public boolean enabled(@Prototype Equality this) {
594    throw new Error("do not invoke " + getClass() + ".enabled()");
595  }
596
597  @Override
598  public boolean valid_types(@Prototype Equality this, VarInfo[] vis) {
599    throw new Error("do not invoke " + getClass() + ".valid_types()");
600  }
601
602  @Override
603  protected @NonPrototype Equality instantiate_dyn(@Prototype Equality this, PptSlice slice) {
604    throw new Error("do not invoke " + getClass() + ".instantiate_dyn()");
605  }
606
607  @Override
608  public @Nullable @NonPrototype Equality merge(
609      @Prototype Equality this, List<@NonPrototype Invariant> invs, PptSlice parent_ppt) {
610    throw new Error("Don't merge Equality invariants");
611  }
612}