001package daikon.diff;
002
003import daikon.inv.Invariant;
004import java.io.PrintWriter;
005import java.io.StringWriter;
006import java.util.logging.Level;
007import java.util.logging.Logger;
008import org.checkerframework.checker.nullness.qual.NonNull;
009import org.checkerframework.checker.nullness.qual.Nullable;
010import org.checkerframework.dataflow.qual.SideEffectFree;
011import org.plumelib.util.ArraysPlume;
012import org.plumelib.util.StringsPlume;
013
014/**
015 * Computes statistics about the differences between the sets of invariants. The statistics can be
016 * printed as a human-readable table or a tab-separated list suitable for further processing.
017 */
018public class DetailedStatisticsVisitor extends DepthFirstVisitor {
019
020  public static final Logger debug = Logger.getLogger("daikon.diff.DetailedStatisticsVisitor");
021
022  private static final int FIELD_WIDTH = 5;
023  private static final int LABEL_WIDTH = 7;
024
025  /** The number of arities for invariants; equivalently, 1 more than the max arity. */
026  public static final int NUM_ARITIES = 4;
027
028  /** A string representations for each arity. Length = NUM_ARITIES. */
029  public static final String[] ARITY_LABELS = {"Nul", "Una", "Bin", "Ter"};
030
031  // Relationships between invariants
032  public static final int NUM_RELATIONSHIPS = 12;
033  // Both present, same invariant, justified in file1, justified in file2
034  public static final int REL_SAME_JUST1_JUST2 = 0;
035  // Both present, same invariant, justified in file1, unjustified in file2
036  public static final int REL_SAME_JUST1_UNJUST2 = 1;
037  // Both present, same invariant, unjustified in file1, justified in file2
038  public static final int REL_SAME_UNJUST1_JUST2 = 2;
039  // Both present, same invariant, unjustified in file1, unjustified in file2
040  public static final int REL_SAME_UNJUST1_UNJUST2 = 3;
041  // Both present, diff invariant, justification in file1, justified
042  // in file2
043  public static final int REL_DIFF_JUST1_JUST2 = 4;
044  // Both present, different invariant, justified in file1,
045  // unjustified in file2
046  public static final int REL_DIFF_JUST1_UNJUST2 = 5;
047  // Both present, different invariant, unjustified in file1,
048  // justified in file2
049  public static final int REL_DIFF_UNJUST1_JUST2 = 6;
050  // Both present, different invariant, unjustified in file1,
051  // unjustified in file2
052  public static final int REL_DIFF_UNJUST1_UNJUST2 = 7;
053  // Present in file1, justified in file1, not present in file2
054  public static final int REL_MISS_JUST1 = 8;
055  // Present in file1, unjustified in file1, not present in file2
056  public static final int REL_MISS_UNJUST1 = 9;
057  // Not present in file1, present in file2, justified in file2
058  public static final int REL_MISS_JUST2 = 10;
059  // Not present in file1, present in file2, unjustified in file2
060  public static final int REL_MISS_UNJUST2 = 11;
061
062  public static final String[] RELATIONSHIP_LABELS = {
063    "SJJ", "SJU", "SUJ", "SUU", "DJJ", "DJU", "DUJ", "DUU", "JM", "UM", "MJ", "MU"
064  };
065
066  /**
067   * Table of frequencies, indexed by arity of invariant, and relationship between the invariants.
068   *
069   * <p>Unfortunately, this is heterogeneous: some measurement are integers and others are doubles.
070   */
071  private double[][] freq = new double[NUM_ARITIES][NUM_RELATIONSHIPS];
072
073  private boolean continuousJustification;
074
075  public DetailedStatisticsVisitor(boolean continuousJustification) {
076    this.continuousJustification = continuousJustification;
077  }
078
079  @Override
080  public void visit(InvNode node) {
081    Invariant inv1 = node.getInv1();
082    Invariant inv2 = node.getInv2();
083    if (shouldAddFrequency(inv1, inv2)) {
084      addFrequency(node.getInv1(), node.getInv2());
085    }
086  }
087
088  /**
089   * Adds the difference between the two invariants to the appropriate entry in the frequencies
090   * table.
091   */
092  private void addFrequency(@Nullable Invariant inv1, @Nullable Invariant inv2) {
093    if (continuousJustification) {
094      addFrequencyContinuous(inv1, inv2);
095    } else {
096      addFrequencyBinary(inv1, inv2);
097    }
098  }
099
100  /**
101   * Treats justification as a binary value. The table entry is incremented by 1 regardless of the
102   * difference in justifications.
103   */
104  private void addFrequencyBinary(@Nullable Invariant inv1, @Nullable Invariant inv2) {
105    int arity = determineArity(inv1, inv2);
106    int relationship = determineRelationship(inv1, inv2);
107    freq[arity][relationship]++;
108  }
109
110  /**
111   * Treats justification as a continuous value. If one invariant is justified but the other is
112   * unjustified, the table entry is incremented by the difference in justifications.
113   */
114  private void addFrequencyContinuous(@Nullable Invariant inv1, @Nullable Invariant inv2) {
115    int arity = determineArity(inv1, inv2);
116    int relationship = determineRelationship(inv1, inv2);
117
118    switch (relationship) {
119      case REL_SAME_JUST1_UNJUST2:
120      case REL_SAME_UNJUST1_JUST2:
121        assert inv1 != null && inv2 != null
122            : "@AssumeAssertion(nullness)"; // application invariant about return value of
123        // determineRelationship
124        freq[arity][relationship] += calculateConfidenceDifference(inv1, inv2);
125        break;
126      default:
127        freq[arity][relationship]++;
128    }
129  }
130
131  /**
132   * Returns the difference in the probabilites of the two invariants. Confidence values less than 0
133   * (i.e. CONFIDENCE_NEVER) are rounded up to 0.
134   */
135  private static double calculateConfidenceDifference(Invariant inv1, Invariant inv2) {
136    assert inv1 != null && inv2 != null;
137    double diff;
138    double conf1 = Math.max(inv1.getConfidence(), 0);
139    double conf2 = Math.max(inv2.getConfidence(), 0);
140    diff = Math.abs(conf1 - conf2);
141    return diff;
142  }
143
144  /** Returns the arity of the invariant pair. */
145  public static int determineArity(@Nullable Invariant inv1, @Nullable Invariant inv2) {
146
147    // Set inv to a non-null invariant
148    @SuppressWarnings("nullness") // at least one argument is non-null
149    @NonNull Invariant inv = (inv1 != null) ? inv1 : inv2;
150
151    if (debug.isLoggable(Level.FINE)) {
152      debug.fine(
153          "visit: "
154              + ((inv1 != null) ? inv1.ppt.parent.name() : "NULL")
155              + " "
156              + ((inv1 != null) ? inv1.repr() : "NULL")
157              + " - "
158              + ((inv2 != null) ? inv2.repr() : "NULL"));
159    }
160
161    int arity = inv.ppt.arity();
162    if (debug.isLoggable(Level.FINE)) {
163      debug.fine("  arity: " + arity);
164    }
165    return arity;
166  }
167
168  /**
169   * Returns the relationship between the two invariants. There are twelve possible relationships,
170   * described at the beginning of this file.
171   */
172  public static int determineRelationship(@Nullable Invariant inv1, @Nullable Invariant inv2) {
173    int relationship;
174
175    if (inv1 == null) {
176      assert inv2 != null : "@AssumeAssertion(nullness): at least one argument is non-null";
177      relationship = inv2.justified() ? REL_MISS_JUST2 : REL_MISS_UNJUST2;
178    } else if (inv2 == null) {
179      relationship = inv1.justified() ? REL_MISS_JUST1 : REL_MISS_UNJUST1;
180    } else {
181      boolean justified1 = inv1.justified();
182      boolean justified2 = inv2.justified();
183      if (inv1.isSameInvariant(inv2)) {
184        if (justified1 && justified2) {
185          relationship = REL_SAME_JUST1_JUST2;
186        } else if (justified1 && !justified2) {
187          relationship = REL_SAME_JUST1_UNJUST2;
188        } else if (!justified1 && justified2) {
189          relationship = REL_SAME_UNJUST1_JUST2;
190        } else {
191          relationship = REL_SAME_UNJUST1_UNJUST2;
192        }
193      } else {
194        if (justified1 && justified2) {
195          relationship = REL_DIFF_JUST1_JUST2;
196        } else if (justified1 && !justified2) {
197          relationship = REL_DIFF_JUST1_UNJUST2;
198        } else if (!justified1 && justified2) {
199          relationship = REL_DIFF_UNJUST1_JUST2;
200        } else {
201          relationship = REL_DIFF_UNJUST1_UNJUST2;
202        }
203      }
204    }
205
206    return relationship;
207  }
208
209  /** Returns a tab-separated listing of its data, suitable for post-processing. */
210  public String repr() {
211    StringWriter sw = new StringWriter();
212    PrintWriter pw = new PrintWriter(sw);
213
214    for (int arity = 0; arity < NUM_ARITIES; arity++) {
215      for (int rel = 0; rel < NUM_RELATIONSHIPS; rel++) {
216        pw.println(
217            String.valueOf(arity)
218                + "\t"
219                + String.valueOf(rel)
220                + "\t"
221                + String.valueOf(freq[arity][rel]));
222      }
223    }
224
225    return sw.toString();
226  }
227
228  /** Returns a human-readable table of its data. */
229  @SuppressWarnings("NarrowingCompoundAssignment") // due to heterogeneous freq array
230  @SideEffectFree
231  public String format() {
232    StringWriter sw = new StringWriter();
233    PrintWriter pw = new PrintWriter(sw);
234
235    pw.println("STATISTICS");
236    pw.print("       ");
237    for (int rel = 0; rel < NUM_RELATIONSHIPS; rel++) {
238      pw.print(StringsPlume.rpad(RELATIONSHIP_LABELS[rel], FIELD_WIDTH));
239    }
240    pw.println(StringsPlume.rpad("TOTAL", FIELD_WIDTH));
241
242    for (int arity = 0; arity < NUM_ARITIES; arity++) {
243      pw.print(StringsPlume.rpad(ARITY_LABELS[arity], LABEL_WIDTH));
244      for (int rel = 0; rel < NUM_RELATIONSHIPS; rel++) {
245        int f = (int) freq[arity][rel];
246        pw.print(StringsPlume.rpad(f, FIELD_WIDTH));
247      }
248      int s = (int) ArraysPlume.sum(freq[arity]);
249      pw.print(StringsPlume.rpad(s, FIELD_WIDTH));
250      pw.println();
251    }
252
253    pw.print(StringsPlume.rpad("TOTAL", LABEL_WIDTH));
254    for (int rel = 0; rel < NUM_RELATIONSHIPS; rel++) {
255      int sum = 0;
256      for (int arity = 0; arity < NUM_ARITIES; arity++) {
257        sum += (int) freq[arity][rel];
258      }
259      pw.print(StringsPlume.rpad(sum, FIELD_WIDTH));
260    }
261    pw.print(StringsPlume.rpad((int) ArraysPlume.sum(freq), FIELD_WIDTH));
262
263    pw.println();
264
265    pw.println();
266
267    return sw.toString();
268  }
269
270  /**
271   * Returns the frequency of pairs of invariants we have seen with this arity and relationship. May
272   * be a non-integer, since we may be treating justification as a continuous value.
273   */
274  public double freq(int arity, int relationship) {
275    return freq[arity][relationship];
276  }
277
278  /**
279   * Returns true if the pair of invariants should be added to the frequency table, based on their
280   * printability.
281   */
282  private static boolean shouldAddFrequency(@Nullable Invariant inv1, @Nullable Invariant inv2) {
283    return (inv1 != null && inv1.isWorthPrinting()) || (inv2 != null && inv2.isWorthPrinting());
284  }
285}