001package daikon.tools; 002 003import static java.util.logging.Level.FINE; 004import static java.util.logging.Level.INFO; 005 006import daikon.Daikon; 007import daikon.Debug; 008import daikon.FileIO; 009import daikon.Global; 010import daikon.PptConditional; 011import daikon.PptMap; 012import daikon.PptSlice; 013import daikon.PptTopLevel; 014import daikon.ValueTuple; 015import daikon.VarInfo; 016import daikon.inv.Invariant; 017import daikon.inv.InvariantStatus; 018import daikon.inv.filter.InvariantFilters; 019import daikon.split.PptSplitter; 020import gnu.getopt.*; 021import java.io.File; 022import java.io.FileNotFoundException; 023import java.io.FileOutputStream; 024import java.io.IOException; 025import java.io.OptionalDataException; 026import java.io.PrintStream; 027import java.io.StreamCorruptedException; 028import java.util.ArrayList; 029import java.util.HashSet; 030import java.util.LinkedHashMap; 031import java.util.LinkedHashSet; 032import java.util.List; 033import java.util.Map; 034import java.util.logging.Logger; 035import org.checkerframework.checker.mustcall.qual.Owning; 036import org.checkerframework.checker.nullness.qual.Nullable; 037import org.checkerframework.checker.nullness.qual.RequiresNonNull; 038import org.plumelib.util.StringsPlume; 039 040/** 041 * InvariantChecker reads an invariant file and trace file. It prints errors for any invariants that 042 * are violated by the trace file. 043 */ 044public class InvariantChecker { 045 private InvariantChecker() { 046 throw new Error("do not instantiate"); 047 } 048 049 public static final Logger debug = Logger.getLogger("daikon.tools.InvariantChecker"); 050 051 public static final Logger debug_detail = Logger.getLogger("daikon.tools.InvariantCheckerDetail"); 052 053 private static final String output_SWITCH = "output"; 054 private static final String dir_SWITCH = "dir"; 055 private static final String conf_SWITCH = "conf"; 056 private static final String filter_SWITCH = "filter"; 057 private static final String verbose_SWITCH = "verbose"; 058 059 /** The usage message for this program. */ 060 private static String usage = 061 StringsPlume.joinLines( 062 "Usage: java daikon.InvariantChecker [OPTION]... <inv_file> <dtrace_file>", 063 " -h, --" + Daikon.help_SWITCH, 064 " Display this usage message", 065 " --" + output_SWITCH + " output file", 066 " --" + conf_SWITCH, 067 " Checks only invariants that are above the default confidence level", 068 " --" + filter_SWITCH, 069 " Checks only invariants that are not filtered by the default filters", 070 " --" + dir_SWITCH + " directory with invariant and dtrace files", 071 " We output how many invariants failed for each invariant file. We check for" 072 + " failure against any sample in any dtrace file.", 073 " --" + verbose_SWITCH + " print all failing samples", 074 " --" + Daikon.config_option_SWITCH + " config_var=val", 075 " Sets the specified configuration variable. ", 076 " --" + Daikon.debugAll_SWITCH, 077 " Turns on all debug flags (voluminous output)", 078 " --" + Daikon.debug_SWITCH + " logger", 079 " Turns on the specified debug logger", 080 " --" + Daikon.track_SWITCH + " class<var1,var2,var3>@ppt", 081 " Print debug info on the specified invariant class, vars, and ppt"); 082 083 public static List<String> dtrace_files = new ArrayList<>(); 084 static @Owning PrintStream output_stream = System.out; 085 static int error_cnt = 0; 086 static int sample_cnt = 0; 087 088 static @Nullable File dir_file; // Yoav added 089 static boolean doFilter; 090 static boolean doConf; 091 static boolean quiet = true; 092 static HashSet<Invariant> failedInvariants = new HashSet<>(); // Yoav added 093 static HashSet<Invariant> testedInvariants = new HashSet<>(); // Yoav added 094 static HashSet<Invariant> activeInvariants = new HashSet<>(); // Yoav added 095 static LinkedHashSet<String> outputComma = new LinkedHashSet<>(); // Yoav added 096 097 public static void main(String[] args) 098 throws FileNotFoundException, 099 StreamCorruptedException, 100 OptionalDataException, 101 IOException, 102 ClassNotFoundException { 103 try { 104 if (args.length == 0) { 105 throw new Daikon.UserError(usage); 106 } 107 mainHelper(args); 108 } catch (Daikon.DaikonTerminationException e) { 109 Daikon.handleDaikonTerminationException(e); 110 } 111 } 112 113 /** 114 * This does the work of {@link #main(String[])}, but it never calls System.exit, so it is 115 * appropriate to be called progrmmatically. 116 * 117 * @param args command-line arguments, like those of {@link #main} 118 */ 119 public static void mainHelper(final String[] args) 120 throws FileNotFoundException, 121 StreamCorruptedException, 122 OptionalDataException, 123 IOException, 124 ClassNotFoundException { 125 daikon.LogHelper.setupLogs(INFO); 126 127 LongOpt[] longopts = 128 new LongOpt[] { 129 new LongOpt(Daikon.config_option_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 130 new LongOpt(output_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 131 new LongOpt(dir_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 132 new LongOpt(conf_SWITCH, LongOpt.NO_ARGUMENT, null, 0), 133 new LongOpt(filter_SWITCH, LongOpt.NO_ARGUMENT, null, 0), 134 new LongOpt(verbose_SWITCH, LongOpt.NO_ARGUMENT, null, 0), 135 new LongOpt(Daikon.debugAll_SWITCH, LongOpt.NO_ARGUMENT, null, 0), 136 new LongOpt(Daikon.debug_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 137 new LongOpt(Daikon.ppt_regexp_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 138 new LongOpt(Daikon.track_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 139 }; 140 Getopt g = new Getopt("daikon.tools.InvariantChecker", args, "h", longopts); 141 int c; 142 while ((c = g.getopt()) != -1) { 143 switch (c) { 144 case 0: 145 // got a long option 146 String option_name = longopts[g.getLongind()].getName(); 147 if (Daikon.help_SWITCH.equals(option_name)) { 148 System.out.println(usage); 149 throw new Daikon.NormalTermination(); 150 } else if (conf_SWITCH.equals(option_name)) { 151 doConf = true; 152 } else if (filter_SWITCH.equals(option_name)) { 153 doFilter = true; 154 } else if (verbose_SWITCH.equals(option_name)) { 155 quiet = false; 156 } else if (dir_SWITCH.equals(option_name)) { 157 dir_file = new File(Daikon.getOptarg(g)); 158 if (!dir_file.exists() || !dir_file.isDirectory()) { 159 throw new Daikon.UserError("Error reading the directory " + dir_file); 160 } 161 162 } else if (output_SWITCH.equals(option_name)) { 163 File output_file = new File(Daikon.getOptarg(g)); 164 output_stream = new PrintStream(new FileOutputStream(output_file)); 165 } else if (Daikon.config_option_SWITCH.equals(option_name)) { 166 String item = Daikon.getOptarg(g); 167 daikon.config.Configuration.getInstance().apply(item); 168 break; 169 } else if (Daikon.debugAll_SWITCH.equals(option_name)) { 170 Global.debugAll = true; 171 } else if (Daikon.debug_SWITCH.equals(option_name)) { 172 daikon.LogHelper.setLevel(Daikon.getOptarg(g), FINE); 173 } else if (Daikon.track_SWITCH.equals(option_name)) { 174 daikon.LogHelper.setLevel("daikon.Debug", FINE); 175 String error = Debug.add_track(Daikon.getOptarg(g)); 176 if (error != null) { 177 throw new Daikon.UserError( 178 "Error parsing track argument '" + Daikon.getOptarg(g) + "' - " + error); 179 } 180 } else { 181 throw new RuntimeException("Unknown long option received: " + option_name); 182 } 183 break; 184 case 'h': 185 System.out.println(usage); 186 throw new Daikon.NormalTermination(); 187 case '?': 188 break; // getopt() already printed an error 189 default: 190 System.out.println("getopt() returned " + c); 191 break; 192 } 193 } 194 195 { 196 File inv_file = null; 197 198 // Loop through each filename specified 199 for (int i = g.getOptind(); i < args.length; i++) { 200 201 // Get the file and make sure it exists 202 File file = new File(args[i]); 203 if (!file.exists()) { 204 throw new Error("File " + file + " not found."); 205 } 206 207 // These aren't "endsWith()" because there might be a suffix on the end 208 // (eg, a date). 209 String filename = file.toString(); 210 if (filename.indexOf(".inv") != -1) { 211 if (inv_file != null) { 212 throw new Daikon.UserError("multiple inv files specified" + Global.lineSep + usage); 213 } 214 inv_file = file; 215 } else if (filename.indexOf(".dtrace") != -1) { 216 dtrace_files.add(filename); 217 } else { 218 throw new Error("Unrecognized argument: " + file); 219 } 220 } 221 if (dir_file == null) { 222 if (inv_file == null) { 223 throw new Daikon.UserError("No inv file specified" + Global.lineSep + usage); 224 } 225 checkInvariants(inv_file); 226 return; 227 } 228 } 229 230 // Yoav additions: 231 File[] filesInDir = dir_file.listFiles(); 232 if (filesInDir == null || filesInDir.length == 0) { 233 throw new Daikon.UserError( 234 "The directory " + dir_file + " is empty" + Global.lineSep + usage); 235 } 236 ArrayList<File> invariants = new ArrayList<>(); 237 for (File f : filesInDir) { 238 if (f.toString().indexOf(".inv") != -1) { 239 invariants.add(f); 240 } 241 } 242 if (invariants.size() == 0) { 243 throw new Daikon.UserError( 244 "Did not find any invariant files in the directory " + dir_file + Global.lineSep + usage); 245 } 246 ArrayList<File> dtraces = new ArrayList<>(); 247 for (File f : filesInDir) { 248 if (f.toString().indexOf(".dtrace") != -1) { 249 dtraces.add(f); 250 } 251 } 252 if (dtraces.size() == 0) { 253 throw new Daikon.UserError( 254 "Did not find any dtrace files in the directory " + dir_file + Global.lineSep + usage); 255 } 256 257 System.out.println( 258 "Collecting data for invariants files " + invariants + " and dtrace files " + dtraces); 259 260 dtrace_files.clear(); 261 for (File dtrace : dtraces) { 262 dtrace_files.add(dtrace.toString()); 263 } 264 265 String commaLine = ""; 266 for (File inFile : invariants) { 267 String name = inFile.getName().replace(".inv", "").replace(".gz", ""); 268 commaLine += "," + name; 269 } 270 outputComma.add(commaLine); 271 272 commaLine = ""; 273 for (File inFile : invariants) { 274 File inv_file = inFile; 275 failedInvariants.clear(); 276 testedInvariants.clear(); 277 error_cnt = 0; 278 279 output_stream = 280 new PrintStream( 281 new FileOutputStream( 282 inFile.toString().replace(".inv", "").replace(".gz", "") 283 + ".false-positives.txt")); 284 checkInvariants(inv_file); 285 output_stream.close(); 286 287 int failedCount = failedInvariants.size(); 288 int testedCount = testedInvariants.size(); 289 String percent = toPercentage(failedCount, testedCount); 290 commaLine += "," + percent; 291 } 292 outputComma.add(commaLine); 293 294 System.out.println(); 295 for (String output : outputComma) { 296 System.out.println(output); 297 } 298 } 299 300 private static String toPercentage(int portion, int total) { 301 double s = portion * 100; 302 return String.format("%.2f", s / total) + "%"; 303 } 304 305 private static void checkInvariants(File inv_file) throws IOException { 306 // Read the invariant file 307 PptMap ppts = FileIO.read_serialized_pptmap(inv_file, true); 308 309 // Yoav: make sure we have unique invariants 310 InvariantFilters fi = InvariantFilters.defaultFilters(); 311 // Set<String> allInvariantsStr = new HashSet<>(); 312 // Set<Invariant> allInvariants = new HashSet<>(); 313 for (PptTopLevel ppt : ppts.all_ppts()) { 314 for (PptSlice slice : ppt.views_iterable()) { 315 for (Invariant inv : slice.invs) { 316 if (doConf && inv.getConfidence() < Invariant.dkconfig_confidence_limit) { 317 // System.out.printf("inv ignored (conf): %s:%s%n", inv.ppt.name(), 318 // inv.format()); 319 continue; 320 } 321 322 if (doFilter && fi.shouldKeep(inv) == null) { 323 // System.out.printf("inv ignored (filter): %s:%s%n", 324 // inv.ppt.name(), inv.format()); 325 continue; 326 } 327 activeInvariants.add(inv); 328 329 // String n = invariant2str(ppt, inv); 330 // if (!allInvariants.contains(inv) && allInvariantsStr.contains(n)) { 331 // throw new 332 // Daikon.UserError("Two invariants have the same ppt.name+inv.rep:"+n); 333 // } 334 // allInvariants.add(inv); 335 // allInvariantsStr.add(n); 336 } 337 } 338 } 339 340 // Read and process the data trace files 341 FileIO.Processor processor = new InvariantCheckProcessor(); 342 343 Daikon.FileIOProgress progress = new Daikon.FileIOProgress(); 344 progress.start(); 345 progress.clear(); 346 FileIO.read_data_trace_files(dtrace_files, ppts, processor, false); 347 progress.shouldStop = true; 348 System.out.println(); 349 System.out.printf( 350 "%s: %,d errors found in %,d samples (%s)%n", 351 inv_file, error_cnt, sample_cnt, toPercentage(error_cnt, sample_cnt)); 352 int failedCount = failedInvariants.size(); 353 int testedCount = testedInvariants.size(); 354 String percent = toPercentage(failedCount, testedCount); 355 System.out.println( 356 inv_file 357 + ": " 358 + failedCount 359 + " false positives, out of " 360 + testedCount 361 + ", which is " 362 + percent 363 + "."); 364 if (false) { 365 for (Invariant inv : failedInvariants) { 366 System.out.printf("+%s:%s%n", inv.ppt.name(), inv.format()); 367 } 368 } 369 } 370 371 /** Class to track matching ppt and its values. */ 372 static final class EnterCall { 373 374 public PptTopLevel ppt; 375 public ValueTuple vt; 376 377 public EnterCall(PptTopLevel ppt, ValueTuple vt) { 378 379 this.ppt = ppt; 380 this.vt = vt; 381 } 382 } 383 384 public static class InvariantCheckProcessor extends FileIO.Processor { 385 386 Map<Integer, EnterCall> call_map = new LinkedHashMap<>(); 387 388 /** 389 * process the sample by checking it against each existing invariant and issuing an error if any 390 * invariant is falsified or weakened. 391 */ 392 @RequiresNonNull("daikon.FileIO.data_trace_state") 393 @Override 394 public void process_sample( 395 PptMap all_ppts, PptTopLevel ppt, ValueTuple vt, @Nullable Integer nonce) { 396 397 debug.fine("processing sample from: " + ppt.name); 398 399 // Add orig and derived variables 400 FileIO.compute_orig_variables(ppt, vt.vals, vt.mods, nonce); 401 FileIO.compute_derived_variables(ppt, vt.vals, vt.mods); 402 403 // Intern the sample 404 vt = new ValueTuple(vt.vals, vt.mods); 405 406 // If this is an enter point, just remember it for later 407 if (ppt.ppt_name.isEnterPoint()) { 408 assert nonce != null : "@AssumeAssertion(nullness): nonce exists for enter & exit points"; 409 if (dir_file != null) { 410 // Yoav: I had to do a hack to handle the case that several dtrace files are concatenated 411 // together, and Sung's dtrace files have unterminated calls, and when concatenating two 412 // files you can have the same nonce. 413 // So I have to remove the nonce found from the call_map. 414 call_map.remove(nonce); 415 } else { 416 assert call_map.get(nonce) == null; 417 } 418 call_map.put(nonce, new EnterCall(ppt, vt)); 419 debug.fine("Skipping enter sample"); 420 return; 421 } 422 423 // If this is an exit point, process the saved enter point 424 if (ppt.ppt_name.isExitPoint()) { 425 assert nonce != null : "@AssumeAssertion(nullness): nonce exists for enter & exit points"; 426 EnterCall ec = call_map.get(nonce); 427 if (ec != null) { 428 call_map.remove(nonce); 429 debug.fine("Processing enter sample from " + ec.ppt.name); 430 add(ec.ppt, ec.vt, all_ppts); 431 } else { // didn't find the enter 432 if (!quiet) { 433 System.out.printf("couldn't find enter for nonce %d at ppt %s%n", nonce, ppt.name()); 434 } 435 return; 436 } 437 } 438 439 add(ppt, vt, all_ppts); 440 } 441 442 @RequiresNonNull("daikon.FileIO.data_trace_state") 443 private void add(PptTopLevel ppt, ValueTuple vt, PptMap all_ppts) { 444 // Add the sample to any splitters 445 if (ppt.has_splitters()) { 446 assert ppt.splitters != null; // because ppt.has_splitters() = true 447 for (PptSplitter ppt_split : ppt.splitters) { 448 PptConditional ppt_cond = ppt_split.choose_conditional(vt); 449 if (ppt_cond != null) { 450 add(ppt_cond, vt, all_ppts); 451 } else { 452 debug.fine(": sample doesn't pick conditional"); 453 } 454 } 455 } 456 457 // if this is a numbered exit, apply to the combined exit as well 458 if (!(ppt instanceof PptConditional) && ppt.ppt_name.isNumberedExitPoint()) { 459 PptTopLevel parent = all_ppts.get(ppt.ppt_name.makeExit()); 460 if (parent != null) { 461 parent.get_missingOutOfBounds(ppt, vt); 462 add(parent, vt, all_ppts); 463 } 464 } 465 466 // If the point has no variables, skip it 467 if (ppt.var_infos.length == 0) { 468 return; 469 } 470 471 // We should have received sample here before, or there is nothing to check. 472 // Yoav added: It can be that the different dtrace and inv files have different program points 473 // if (false && ppt.num_samples() <= 0) { 474 // assert ppt.num_samples() > 0 475 // : "ppt " + ppt.name + " has 0 samples and " + ppt.var_infos.length + " variables"; 476 // } 477 478 // Loop through each slice 479 slice_loop: 480 for (PptSlice slice : ppt.views_iterable()) { 481 if (debug_detail.isLoggable(FINE)) { 482 debug_detail.fine( 483 ": processing slice " + slice + "vars: " + Debug.toString(slice.var_infos, vt)); 484 } 485 486 // If any variables are missing, skip this slice 487 for (int j = 0; j < slice.var_infos.length; j++) { 488 VarInfo v = slice.var_infos[j]; 489 if (v.isMissing(vt)) { 490 if (debug_detail.isLoggable(FINE)) { 491 debug_detail.fine(": : Skipping slice, " + v.name() + " missing"); 492 } 493 continue slice_loop; 494 } 495 if (v.missingOutOfBounds()) { 496 if (debug_detail.isLoggable(FINE)) { 497 debug.fine(": : Skipping slice, " + v.name() + " out of bounds"); 498 } 499 continue slice_loop; 500 } 501 } 502 503 // Loop through each invariant 504 for (Invariant inv : slice.invs) { 505 if (debug_detail.isLoggable(FINE)) { 506 debug_detail.fine(": : Processing invariant: " + inv); 507 } 508 if (!inv.isActive()) { 509 if (debug_detail.isLoggable(FINE)) { 510 debug_detail.fine(": : skipped non-active " + inv); 511 } 512 continue; 513 } 514 515 // Yoav added 516 if (!activeInvariants.contains(inv)) { 517 // System.out.printf("skipping invariant %s:%s%n", inv.ppt.name(), 518 // inv.format()); 519 continue; 520 } 521 522 // String invRep = invariant2str(ppt, inv); 523 testedInvariants.add(inv); 524 525 // Store string representation of original invariant for verbose mode 526 String invRep = quiet ? null : inv.format(); 527 528 InvariantStatus status = inv.add_sample(vt, 1); 529 sample_cnt++; 530 if (status != InvariantStatus.NO_CHANGE) { 531 if (!quiet) { 532 output_stream.println( 533 "At ppt " 534 + ppt.name 535 + ", Invariant '" 536 + invRep 537 + "' invalidated by sample " 538 + Debug.toString(slice.var_infos, vt) 539 + "at line " 540 + FileIO.get_linenum() 541 + " in file " 542 + FileIO.data_trace_state.filename); 543 } 544 failedInvariants.add(inv); 545 activeInvariants.remove(inv); 546 error_cnt++; 547 } 548 } 549 } 550 } 551 } 552 553 @SuppressWarnings("UnusedMethod") // for debugging (which is currently commented out) 554 private static String invariant2str(PptTopLevel ppt, Invariant inv) { 555 return ppt.name + " == " + inv.repr() + inv.getClass() + inv.varNames() + ": " + inv.format(); 556 } 557}