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}