001package daikon.tools.compare; 002 003import static daikon.tools.nullness.NullnessUtil.*; 004import static java.util.logging.Level.FINE; 005import static java.util.logging.Level.INFO; 006 007import daikon.Daikon; 008import daikon.FileIO; 009import daikon.Global; 010import daikon.PptMap; 011import daikon.PptTopLevel; 012import daikon.VarInfo; 013import daikon.config.Configuration; 014import daikon.inv.EqualityComparison; 015import daikon.inv.GuardingImplication; 016import daikon.inv.Implication; 017import daikon.inv.Invariant; 018import daikon.inv.OutputFormat; 019import daikon.inv.unary.OneOf; 020import daikon.inv.unary.scalar.LowerBound; 021import daikon.inv.unary.scalar.LowerBoundFloat; 022import daikon.inv.unary.scalar.OneOfFloat; 023import daikon.inv.unary.scalar.UpperBound; 024import daikon.inv.unary.scalar.UpperBoundFloat; 025import daikon.inv.unary.sequence.EltLowerBound; 026import daikon.inv.unary.sequence.EltLowerBoundFloat; 027import daikon.inv.unary.sequence.EltUpperBound; 028import daikon.inv.unary.sequence.EltUpperBoundFloat; 029import daikon.inv.unary.string.OneOfString; 030import daikon.simplify.InvariantLemma; 031import daikon.simplify.Lemma; 032import daikon.simplify.LemmaStack; 033import daikon.simplify.SimplifyError; 034import gnu.getopt.*; 035import java.io.File; 036import java.io.FileInputStream; 037import java.io.FileNotFoundException; 038import java.io.IOException; 039import java.io.InputStream; 040import java.io.LineNumberReader; 041import java.util.ArrayList; 042import java.util.Collection; 043import java.util.Collections; 044import java.util.HashSet; 045import java.util.LinkedHashMap; 046import java.util.List; 047import java.util.Map; 048import java.util.Set; 049import java.util.TreeSet; 050import java.util.logging.Logger; 051import org.checkerframework.checker.mustcall.qual.Owning; 052import org.checkerframework.checker.nullness.qual.EnsuresNonNull; 053import org.checkerframework.checker.nullness.qual.KeyFor; 054import org.checkerframework.checker.nullness.qual.MonotonicNonNull; 055import org.checkerframework.checker.nullness.qual.NonNull; 056import org.checkerframework.checker.nullness.qual.RequiresNonNull; 057import org.plumelib.util.FilesPlume; 058import org.plumelib.util.StringsPlume; 059 060/** 061 * This is a standalone program that compares the invariants from two versions of (and/or runs of) a 062 * program, and determines using Simplify whether the invariants from one logically imply the 063 * invariants from the other. These are referred to below as the "test" and "application" 064 * invariants, and the conditions that are checked is that the each test precondition (ENTER point 065 * invariant) must be implied some combination of application preconditions, and that each 066 * application postcondition (EXIT point invariant) must be implied by some combination of test 067 * postconditions and application preconditions. 068 */ 069public class LogicalCompare { 070 private LogicalCompare() { 071 throw new Error("do not instantiate"); 072 } 073 074 public static final Logger debug = Logger.getLogger("daikon.tools.compare.LogicalCompare"); 075 076 // Options corresponding to command-line flags 077 private static boolean opt_proofs = false; 078 private static boolean opt_show_count = false; 079 private static boolean opt_show_formulas = false; 080 private static boolean opt_show_valid = false; 081 private static boolean opt_post_after_pre = true; 082 private static boolean opt_timing = false; 083 private static boolean opt_show_sets = false; 084 private static boolean opt_minimize_classes = false; 085 086 // TODO: both of these fields should be instance fields and the main 087 // method should create an instance. 088 089 /** key = ppt name */ 090 private static @MonotonicNonNull Map<String, List<Lemma>> extra_assumptions; 091 092 private static @Owning @MonotonicNonNull LemmaStack lemmas; 093 094 /** The usage message for this program. */ 095 private static String usage = 096 StringsPlume.joinLines( 097 "Usage: java daikon.tools.compare.LogicalCompare [options ...]", 098 " WEAK-INVS STRONG-INVS [ENTER-PPT [EXIT-PPT]]", 099 " -h, --" + Daikon.help_SWITCH, 100 " Display this usage message", 101 " --config-file FILE", 102 " Read configuration option file", 103 " --config_option OPTION=VALUE", 104 " Set individual configuration option", 105 " --" + Daikon.debugAll_SWITCH, 106 " Turns on all debug flags (voluminous output)", 107 " --" + Daikon.debug_SWITCH + " logger", 108 " Turns on the specified debug logger", 109 " --proofs", 110 " Show minimal sufficient conditions for valid invariants", 111 " --show-count", 112 " Print count of invariants checked", 113 " --show-formulas", 114 " Print Simplify representation of invariants", 115 " --show-valid", 116 " Show invariants that are verified as well as those that fail", 117 " --show-sets", 118 " Show, not test, all the invariants that would be considered", 119 " --post-after-pre-failure", 120 " Check postcondition match even if preconditions fail", 121 " --no-post-after-pre-failure", 122 " Don't check postcondition match if preconditions fail", 123 " --timing", 124 " Show time required to check invariants", 125 " --filters [bBoOmjpis]", 126 " Control which invariants are removed from consideration", 127 " --assume FILE", 128 " Read extra assumptions from FILE"); 129 130 // Filter options 131 // b discard uninteresting-constant bounds 132 // B discard all bounds 133 // o discard uninteresting-constant one-ofs 134 // O discard all one-ofs 135 // m discard invariants with only missing samples 136 // j discard statistically unjustified invariants 137 // p discard invariants over pass-by-value parameters 138 // i discard implication pre-conditions 139 // s discard suppressed invariants 140 141 private static boolean[] filters = new boolean[128]; 142 143 private static List<Invariant> filterInvariants(List<Invariant> invs, boolean isPost) { 144 List<Invariant> new_invs = new ArrayList<>(); 145 for (Invariant inv : invs) { 146 Invariant guarded_inv = inv; 147 // System.err.println("Examining " + inv.format()); 148 if (inv instanceof GuardingImplication) { 149 inv = ((Implication) inv).consequent(); 150 } 151 if (inv instanceof LowerBound 152 || inv instanceof UpperBound 153 || inv instanceof EltLowerBound 154 || inv instanceof EltUpperBound 155 || inv instanceof LowerBoundFloat 156 || inv instanceof UpperBoundFloat 157 || inv instanceof EltLowerBoundFloat 158 || inv instanceof EltUpperBoundFloat) { 159 if (filters['b'] && inv.hasUninterestingConstant()) { 160 continue; 161 } 162 if (filters['B']) { 163 continue; 164 } 165 } 166 if (inv instanceof OneOf || inv instanceof OneOfString || inv instanceof OneOfFloat) { 167 if (filters['o'] && inv.hasUninterestingConstant()) { 168 continue; 169 } 170 if (filters['O']) { 171 continue; 172 } 173 } 174 // test used to be "(filters['m'] && inv.ppt.num_mod_samples() == 0)" 175 if (filters['m'] && inv.ppt.num_samples() == 0) { 176 continue; 177 } 178 if (filters['j'] && !inv.justified()) { 179 continue; 180 } 181 if (filters['p'] && isPost && shouldDiscardInvariant(inv)) { 182 continue; 183 } 184 if (filters['i'] && !isPost && inv instanceof Implication) { 185 continue; 186 } 187 String simp = inv.format_using(OutputFormat.SIMPLIFY); 188 if (simp.indexOf("format_simplify") != -1 189 || simp.indexOf("OutputFormat:Simplify") != -1 190 || simp.indexOf("Simplify not implemented") != -1) { 191 // Noisy, since we should be able to handle most invariants now 192 System.out.println("Bad Simplify formatting:%n " + inv.format() + "%n " + simp); 193 continue; 194 } 195 if (inv.format_using(OutputFormat.DAIKON).indexOf("warning: too few samples") != -1) { 196 continue; 197 } 198 if (inv.isGuardingPredicate) { 199 continue; 200 } 201 // System.err.println("Keeping " + inv.format()); 202 new_invs.add(guarded_inv); 203 } 204 return new_invs; 205 } 206 207 // This is a modified version of the method with the same name from 208 // the DerivedParameterFilter, with an exception for invariants 209 // indicating that variables are unchanged (except that that 210 // exception is currently turned off) 211 private static boolean shouldDiscardInvariant(Invariant inv) { 212 for (int i = 0; i < inv.ppt.var_infos.length; i++) { 213 VarInfo vi = inv.ppt.var_infos[i]; 214 // ppt has to be a PptSlice, not a PptTopLevel 215 if (vi.isDerivedParamAndUninteresting()) { 216 // Exception: let invariants like "orig(arg) == arg" through. 217 if (inv.isEqualityComparison()) { 218 EqualityComparison comp = (EqualityComparison) inv; 219 VarInfo var1 = comp.var1(); 220 VarInfo var2 = comp.var2(); 221 boolean vars_are_same = 222 var1.prestate_name().equals(var2.name()) || var2.prestate_name().equals(var1.name()); 223 if (vars_are_same) { 224 return false; 225 } 226 } 227 // if (inv instanceof OneOf || inv instanceof OneOfString || 228 // inv instanceof OneOfString) 229 // return false; 230 // System.err.println("Because of " + vi.name.name() + ", discarding " 231 // + inv.format()); 232 return true; 233 } 234 } 235 return false; 236 } 237 238 // Translate a vector of Invariants into a vector of Lemmas, without 239 // changing the invariants. 240 private static List<Lemma> translateStraight(List<Invariant> invs) { 241 List<Lemma> lems = new ArrayList<>(); 242 for (Invariant inv : invs) { 243 lems.add(new InvariantLemma(inv)); 244 } 245 return lems; 246 } 247 248 // Translate a vector of Invariants into a vector of Lemmas, 249 // discarding any invariants that represent only facts about a 250 // routine's prestate. 251 private static List<Lemma> translateRemovePre(List<Invariant> invs) { 252 List<Lemma> lems = new ArrayList<>(); 253 for (Invariant inv : invs) { 254 if (!inv.isAllPrestate()) { 255 lems.add(new InvariantLemma(inv)); 256 } 257 } 258 return lems; 259 } 260 261 // Translate a vector of Invariants into a vector of Lemmas, adding 262 // orig(...) to each variable so that the invariant will be true 263 // about the precondition of a routine when it is examined in the 264 // poststate context. 265 // The arguments are invariants at the entry point, where no orig(...) variables exist. 266 private static List<Lemma> translateAddOrig(List<Invariant> invs) { 267 List<Lemma> lems = new ArrayList<>(); 268 for (Invariant inv : invs) { 269 lems.add(InvariantLemma.makeLemmaAddOrig(inv)); 270 } 271 return lems; 272 } 273 274 // // Print a vector of invariants and their Simplify translations, for 275 // // debugging purposes. 276 // private static void printInvariants(List<Invariant> invs) { 277 // for (Invariant inv : invs) { 278 // System.out.println(" " + inv.format()); 279 // System.out.println("(BG_PUSH " 280 // + inv.format_using(OutputFormat.SIMPLIFY) +")"); 281 // } 282 // } 283 284 private static String shortName(Class<?> c) { 285 String name = c.getName(); 286 return name.substring(name.lastIndexOf('.') + 1); 287 } 288 289 @RequiresNonNull("lemmas") 290 private static int checkConsequences(List<Lemma> assumptions, List<Lemma> consequences) { 291 Set<String> assumption_formulas = new HashSet<>(); 292 for (Lemma lem : assumptions) { 293 assumption_formulas.add(lem.formula); 294 } 295 296 int invalidCount = 0; 297 for (Lemma inv : consequences) { 298 char result; 299 boolean identical = false; 300 if (assumption_formulas.contains(inv.formula)) { 301 result = 'T'; 302 identical = true; 303 } else { 304 result = lemmas.checkLemma(inv); 305 } 306 307 if (opt_minimize_classes) { 308 if (result == 'T' && !identical) { 309 List<Set<Class<? extends Invariant>>> sets = lemmas.minimizeClasses(inv.formula); 310 for (Set<Class<? extends Invariant>> classes : sets) { 311 @SuppressWarnings( 312 "nullness") // application invariant: context; might be able to rewrite types to 313 // make consequences a List<InvariantLemma>" 314 @NonNull Class<? extends Invariant> inv_class = inv.invClass(); 315 System.out.print(shortName(inv_class) + ":"); 316 if (classes.contains(inv_class)) { 317 System.out.print(" " + shortName(inv_class)); 318 classes.remove(inv_class); 319 } 320 for (Class<? extends Invariant> c : classes) { 321 System.out.print(" " + shortName(c)); 322 } 323 System.out.println(); 324 } 325 System.out.println(inv.summarize()); 326 System.out.println(); 327 } 328 if (true) { 329 continue; 330 } 331 } 332 333 if (result == 'T') { 334 if (opt_proofs) { 335 if (identical) { 336 System.out.println("Identical"); 337 } else { 338 List<Lemma> assume = lemmas.minimizeProof(inv); 339 System.out.println(); 340 for (Lemma lem : assume) { 341 System.out.println(lem.summarize()); 342 } 343 System.out.println("----------------------------------"); 344 System.out.println(inv.summarize()); 345 if (opt_show_formulas) { 346 System.out.println(); 347 for (Lemma lem : assume) { 348 System.out.println(" " + lem.formula); 349 } 350 System.out.println(" ------------------------------------------"); 351 System.out.println(" " + inv.formula); 352 } 353 } 354 } else if (opt_show_valid) { 355 System.out.print("Valid: "); 356 System.out.println(inv.summary); 357 if (opt_show_formulas) { 358 System.out.println(" " + inv.formula); 359 } 360 } 361 } else if (result == 'F') { 362 invalidCount++; 363 if (opt_proofs) { 364 System.out.println(); 365 } 366 System.out.print("Invalid: "); 367 System.out.println(inv.summary); 368 if (opt_show_formulas) { 369 System.out.println(" " + inv.formula); 370 } 371 } else { 372 assert result == '?'; 373 if (opt_proofs) { 374 System.out.println(); 375 } 376 System.out.print("Timeout: "); 377 System.out.println(inv.summary); 378 if (opt_show_formulas) { 379 System.out.println(" " + inv.formula); 380 } 381 } 382 } 383 return invalidCount; 384 } 385 386 // Check that each of the invariants in CONSEQUENCES follows from 387 // zero or more of the invariants in ASSUMPTIONS. Returns the number 388 // of invariants that can't be proven to follow. 389 @RequiresNonNull("lemmas") 390 private static int evaluateImplications(List<Lemma> assumptions, List<Lemma> consequences) 391 throws SimplifyError { 392 int mark = lemmas.markLevel(); 393 lemmas.pushOrdering(); 394 lemmas.pushLemmas(assumptions); 395 if (lemmas.checkForContradiction() == 'T') { 396 if (opt_post_after_pre) { 397 // Shouldn't be reached anymore 398 lemmas.removeContradiction(); 399 System.out.println("Warning: had to remove contradiction(s)"); 400 } else { 401 System.out.println("Contradictory assumptions:"); 402 List<Lemma> min = lemmas.minimizeContradiction(); 403 LemmaStack.printLemmas(System.out, min); 404 throw new Error("Aborting"); 405 } 406 } 407 408 int invalidCount = checkConsequences(assumptions, consequences); 409 410 lemmas.popToMark(mark); 411 return invalidCount; 412 } 413 414 @RequiresNonNull("lemmas") 415 private static int evaluateImplicationsCarefully( 416 List<Lemma> safeAssumptions, List<Lemma> unsafeAssumptions, List<Lemma> consequences) 417 throws SimplifyError { 418 int mark = lemmas.markLevel(); 419 List<Lemma> assumptions = new ArrayList<>(); 420 lemmas.pushOrdering(); 421 lemmas.pushLemmas(safeAssumptions); 422 if (lemmas.checkForContradiction() == 'T') { 423 System.out.println("Contradictory assumptions:"); 424 List<Lemma> min = lemmas.minimizeContradiction(); 425 LemmaStack.printLemmas(System.out, min); 426 throw new Error("Aborting"); 427 } 428 assumptions.addAll(safeAssumptions); 429 430 int j = unsafeAssumptions.size(); 431 for (int i = 0; i < unsafeAssumptions.size(); i++) { 432 List<Lemma> unsafe = unsafeAssumptions.subList(i, j); 433 boolean safe = false; 434 while (!safe && unsafe.size() > 0) { 435 int innerMark = lemmas.markLevel(); 436 lemmas.pushLemmas(new ArrayList<Lemma>(unsafe)); 437 if (lemmas.checkForContradiction() == 'T') { 438 lemmas.popToMark(innerMark); 439 j = i + unsafe.size(); 440 unsafe = unsafe.subList(0, unsafe.size() / 2); 441 } else { 442 safe = true; 443 i += unsafe.size() - 1; 444 assumptions.addAll(unsafe); 445 } 446 } 447 if (!safe) { 448 assert unsafe.size() == 0; 449 j = unsafeAssumptions.size(); 450 } 451 } 452 453 int invalidCount = checkConsequences(assumptions, consequences); 454 455 lemmas.popToMark(mark); 456 return invalidCount; 457 } 458 459 // Initialize the theorem prover. Whichever mode we're in, we should 460 // only do this once per program run. 461 @EnsuresNonNull("lemmas") 462 private static void startProver() { 463 lemmas = new LemmaStack(); 464 } 465 466 // Comparare the invariants for enter and exit points between two 467 // methods (usually two sets of invariants for methods of the same 468 // name). 469 // For historical reasons, one set of invariants is called the app 470 // invariants (from running the app in practice) and the other set of 471 // invariants is called the test invariants (from running the app on its 472 // test suite). 473 @RequiresNonNull({"extra_assumptions", "lemmas"}) 474 private static void comparePpts( 475 PptTopLevel app_enter_ppt, 476 PptTopLevel test_enter_ppt, 477 PptTopLevel app_exit_ppt, 478 PptTopLevel test_exit_ppt) { 479 LemmaStack.clearInts(); 480 481 // app_enter_ppt.guardInvariants(); 482 // test_enter_ppt.guardInvariants(); 483 // app_exit_ppt.guardInvariants(); 484 // test_exit_ppt.guardInvariants(); 485 486 List<Invariant> a_pre = app_enter_ppt.invariants_vector(); 487 List<Invariant> t_pre = test_enter_ppt.invariants_vector(); 488 List<Invariant> a_post = app_exit_ppt.invariants_vector(); 489 List<Invariant> t_post = test_exit_ppt.invariants_vector(); 490 491 if (opt_timing) { 492 System.out.println("Starting timer"); 493 } 494 long processing_time_start = System.currentTimeMillis(); 495 496 a_pre = filterInvariants(a_pre, false); 497 t_pre = filterInvariants(t_pre, false); 498 a_post = filterInvariants(a_post, true); 499 t_post = filterInvariants(t_post, true); 500 501 if (opt_show_sets) { 502 System.out.println("Background assumptions:"); 503 LemmaStack.printLemmas(System.out, Lemma.lemmasList()); 504 System.out.println(""); 505 506 List<Lemma> v = new ArrayList<>(); 507 v.addAll(translateAddOrig(a_pre)); 508 System.out.println("Weak preconditions (Apre):"); 509 LemmaStack.printLemmas(System.out, v); 510 System.out.println(""); 511 512 v = new ArrayList<Lemma>(); 513 v.addAll(translateAddOrig(t_pre)); 514 System.out.println("Strong preconditions (Tpre):"); 515 LemmaStack.printLemmas(System.out, v); 516 System.out.println(""); 517 518 v = new ArrayList<Lemma>(); 519 v.addAll(translateRemovePre(t_post)); 520 System.out.println("Strong postconditions (Tpost):"); 521 LemmaStack.printLemmas(System.out, v); 522 System.out.println(""); 523 524 v = new ArrayList<Lemma>(); 525 v.addAll(translateRemovePre(a_post)); 526 System.out.println("Weak postconditions (Apost):"); 527 LemmaStack.printLemmas(System.out, v); 528 return; 529 } 530 531 if (opt_show_count) { 532 System.out.println("Strong preconditions consist of " + t_pre.size() + " invariants."); 533 } 534 List<Lemma> pre_assumptions = new ArrayList<>(); 535 pre_assumptions.addAll(translateStraight(a_pre)); 536 List<Lemma> pre_conclusions = new ArrayList<>(); 537 pre_conclusions.addAll(translateStraight(t_pre)); 538 Collections.sort(pre_conclusions); 539 540 System.out.println("Testing preconditions:"); 541 int bad_pre = evaluateImplications(pre_assumptions, pre_conclusions); 542 int num_checked = pre_conclusions.size(); 543 if (bad_pre > 0 && !opt_post_after_pre) { 544 System.out.println("Precondition failure, skipping postconditions"); 545 return; 546 } 547 548 System.out.println("Testing postconditions:"); 549 550 List<Lemma> post_assumptions_safe = new ArrayList<>(); 551 List<Lemma> post_assumptions_unsafe = new ArrayList<>(); 552 List<Lemma> post_conclusions = new ArrayList<>(); 553 554 post_assumptions_unsafe.addAll(translateAddOrig(a_pre)); 555 post_assumptions_safe.addAll(translateStraight(t_post)); 556 String ppt_name = test_enter_ppt.ppt_name.name(); 557 if (extra_assumptions.containsKey(ppt_name)) { 558 List<Lemma> assumptions = extra_assumptions.get(ppt_name); 559 post_assumptions_unsafe.addAll(assumptions); 560 } 561 562 post_conclusions.addAll(translateRemovePre(a_post)); 563 Collections.sort(post_conclusions); 564 565 if (opt_show_count) { 566 System.out.println( 567 "Weak postconditions consist of " + post_conclusions.size() + " invariants."); 568 } 569 570 evaluateImplicationsCarefully(post_assumptions_safe, post_assumptions_unsafe, post_conclusions); 571 long time_elapsed = System.currentTimeMillis() - processing_time_start; 572 num_checked += post_conclusions.size(); 573 if (opt_show_count) { 574 System.out.println("Checked " + num_checked + " invariants total"); 575 } 576 if (opt_timing) { 577 System.out.println("Total time " + time_elapsed + "ms"); 578 } 579 } 580 581 @RequiresNonNull("extra_assumptions") 582 private static void readExtraAssumptions(String filename) { 583 File file = new File(filename); 584 try (LineNumberReader reader = FilesPlume.newLineNumberFileReader(file)) { 585 String line; 586 String ppt_name = null; 587 while ((line = reader.readLine()) != null) { 588 line = line.trim(); 589 if (line.equals("") || line.startsWith("#")) { 590 continue; 591 } else if (line.startsWith("PPT_NAME")) { 592 ppt_name = line.substring("PPT_NAME".length()).trim(); 593 if (!extra_assumptions.containsKey(ppt_name)) { 594 extra_assumptions.put(ppt_name, new ArrayList<Lemma>()); 595 } 596 } else if (line.startsWith("(")) { 597 if (ppt_name == null) { 598 System.err.println("Must specify PPT_NAME before giving a formula"); 599 throw new Error(); 600 } 601 String formula, comment; 602 // XXX This should really read a balanced Simplify 603 // expression, then look for a comment after that. But that 604 // would involve counting parens and vertical bars and 605 // backslashes, which I'm too lazy to do right now. 606 if (line.indexOf("#") != -1) { 607 formula = line.substring(0, line.indexOf("#")); 608 comment = line.substring(line.indexOf("#") + 1); 609 } else { 610 formula = line; 611 comment = "User-supplied assumption"; 612 } 613 formula = formula.trim(); 614 comment = comment.trim(); 615 @SuppressWarnings( 616 "nullness") // map: on previous loop iteration, this key was added to map 617 @NonNull List<Lemma> assumption_vec = extra_assumptions.get(ppt_name); 618 assumption_vec.add(new Lemma(comment, formula)); 619 } else { 620 System.err.println("Can't parse " + line + " in assumptions file"); 621 System.err.println( 622 "Should be `PPT_NAME <ppt_name>' or a Simplify formula (starting with `(')"); 623 throw new Error(); 624 } 625 } 626 } catch (FileNotFoundException e) { 627 System.err.println("File not found: " + filename); 628 throw new Error(); 629 } catch (IOException e) { 630 System.err.println("IO error reading " + filename); 631 throw new Error(); 632 } 633 } 634 635 public static void main(String[] args) throws FileNotFoundException, IOException, SimplifyError { 636 try { 637 mainHelper(args); 638 } catch (Daikon.DaikonTerminationException e) { 639 Daikon.handleDaikonTerminationException(e); 640 } 641 } 642 643 /** 644 * This does the work of {@link #main(String[])}, but it never calls System.exit, so it is 645 * appropriate to be called progrmmatically. 646 * 647 * @param args command-line arguments, like those of {@link #main} 648 */ 649 public static void mainHelper(final String[] args) 650 throws FileNotFoundException, IOException, SimplifyError { 651 LongOpt[] longopts = 652 new LongOpt[] { 653 new LongOpt("assume", LongOpt.REQUIRED_ARGUMENT, null, 0), 654 new LongOpt("config_option", LongOpt.REQUIRED_ARGUMENT, null, 0), 655 new LongOpt("config-file", LongOpt.REQUIRED_ARGUMENT, null, 0), 656 new LongOpt(Daikon.debugAll_SWITCH, LongOpt.NO_ARGUMENT, null, 0), 657 new LongOpt(Daikon.debug_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 658 new LongOpt("filters", LongOpt.REQUIRED_ARGUMENT, null, 0), 659 new LongOpt("help", LongOpt.NO_ARGUMENT, null, 0), 660 new LongOpt("minimize-classes", LongOpt.NO_ARGUMENT, null, 0), 661 new LongOpt("no-post-after-pre-failure", LongOpt.NO_ARGUMENT, null, 0), 662 new LongOpt("post-after-pre-failure", LongOpt.NO_ARGUMENT, null, 0), 663 new LongOpt("proofs", LongOpt.NO_ARGUMENT, null, 0), 664 new LongOpt("show-count", LongOpt.NO_ARGUMENT, null, 0), 665 new LongOpt("show-formulas", LongOpt.NO_ARGUMENT, null, 0), 666 new LongOpt("show-sets", LongOpt.NO_ARGUMENT, null, 0), 667 new LongOpt("show-valid", LongOpt.NO_ARGUMENT, null, 0), 668 new LongOpt("timing", LongOpt.NO_ARGUMENT, null, 0), 669 }; 670 671 Configuration.getInstance().apply("daikon.inv.Invariant.simplify_define_predicates=true"); 672 Configuration.getInstance().apply("daikon.simplify.Session.simplify_max_iterations=2147483647"); 673 674 extra_assumptions = new LinkedHashMap<>(); 675 676 Getopt g = new Getopt("daikon.tools.compare.LogicalCompare", args, "h", longopts); 677 int c; 678 boolean user_filters = false; 679 while ((c = g.getopt()) != -1) { 680 switch (c) { 681 case 0: 682 // got a long option 683 String option_name = longopts[g.getLongind()].getName(); 684 if (Daikon.help_SWITCH.equals(option_name)) { 685 System.out.println(usage); 686 throw new Daikon.NormalTermination(); 687 } else if (option_name.equals("config-file")) { 688 String config_file = Daikon.getOptarg(g); 689 try (InputStream stream = new FileInputStream(config_file)) { 690 Configuration.getInstance().apply(stream); 691 } catch (IOException e) { 692 throw new RuntimeException("Could not open config file " + config_file); 693 } 694 } else if (option_name.equals("config_option")) { 695 String item = Daikon.getOptarg(g); 696 Configuration.getInstance().apply(item); 697 } else if (Daikon.debugAll_SWITCH.equals(option_name)) { 698 Global.debugAll = true; 699 } else if (Daikon.debug_SWITCH.equals(option_name)) { 700 daikon.LogHelper.setLevel(Daikon.getOptarg(g), FINE); 701 } else if (option_name.equals("proofs")) { 702 opt_proofs = true; 703 } else if (option_name.equals("show-count")) { 704 opt_show_count = true; 705 } else if (option_name.equals("show-formulas")) { 706 opt_show_formulas = true; 707 } else if (option_name.equals("show-valid")) { 708 opt_show_valid = true; 709 } else if (option_name.equals("show-sets")) { 710 opt_show_sets = true; 711 } else if (option_name.equals("post-after-pre-failure")) { 712 opt_post_after_pre = true; 713 } else if (option_name.equals("no-post-after-pre-failure")) { 714 opt_post_after_pre = false; 715 } else if (option_name.equals("timing")) { 716 opt_timing = true; 717 } else if (option_name.equals("filters")) { 718 String f = Daikon.getOptarg(g); 719 for (int i = 0; i < f.length(); i++) { 720 filters[f.charAt(i)] = true; 721 } 722 user_filters = true; 723 } else if (option_name.equals("assume")) { 724 readExtraAssumptions(Daikon.getOptarg(g)); 725 } else if (option_name.equals("minimize-classes")) { 726 opt_minimize_classes = true; 727 } else { 728 throw new Error(); 729 } 730 break; 731 case 'h': 732 System.out.println(usage); 733 throw new Daikon.NormalTermination(); 734 case '?': 735 // getopt() already printed an error 736 throw new Daikon.UserError("Bad argument"); 737 } 738 } 739 740 if (!user_filters) { 741 filters['i'] = filters['j'] = filters['m'] = filters['p'] = true; 742 } 743 744 // Set up debug traces; note this comes after reading command line options. 745 daikon.LogHelper.setupLogs(Global.debugAll ? FINE : INFO); 746 747 int num_args = args.length - g.getOptind(); 748 749 if (num_args < 2) { 750 throw new Daikon.UserError( 751 "Must have at least two non-option arguments" + Global.lineSep + usage); 752 } 753 754 String app_filename = args[g.getOptind() + 0]; 755 String test_filename = args[g.getOptind() + 1]; 756 757 PptMap app_ppts = 758 FileIO.read_serialized_pptmap( 759 new File(app_filename), true // use saved config 760 ); 761 PptMap test_ppts = 762 FileIO.read_serialized_pptmap( 763 new File(test_filename), true // use saved config 764 ); 765 if (num_args == 4 || num_args == 3) { 766 String enter_ppt_name = args[g.getOptind() + 2]; 767 String exit_ppt_name; 768 if (num_args == 4) { 769 exit_ppt_name = args[g.getOptind() + 3]; 770 } else { 771 exit_ppt_name = ""; // s/b nonexistent 772 } 773 startProver(); 774 775 System.out.println( 776 "Comparing " 777 + enter_ppt_name 778 + " and " 779 + exit_ppt_name 780 + " in " 781 + app_filename 782 + " and " 783 + test_filename); 784 785 PptTopLevel app_enter_ppt = app_ppts.get(enter_ppt_name); 786 PptTopLevel test_enter_ppt = test_ppts.get(enter_ppt_name); 787 if (app_enter_ppt == null) { 788 throw new Daikon.UserError( 789 String.format("Ppt %s not found in %s", enter_ppt_name, app_filename)); 790 } 791 if (test_enter_ppt == null) { 792 throw new Daikon.UserError( 793 String.format("Ppt %s not found in %s", enter_ppt_name, test_filename)); 794 } 795 796 PptTopLevel app_exit_ppt = app_ppts.get(exit_ppt_name); 797 PptTopLevel test_exit_ppt = test_ppts.get(exit_ppt_name); 798 if (app_exit_ppt == null) { 799 app_exit_ppt = app_ppts.get(app_enter_ppt.ppt_name.makeExit()); 800 if (app_exit_ppt == null) { 801 throw new Daikon.UserError( 802 String.format( 803 "Neither ppt %s nor ppt %s found in %s", 804 exit_ppt_name, app_enter_ppt.ppt_name.makeExit(), app_filename)); 805 } 806 } 807 if (test_exit_ppt == null) { 808 test_exit_ppt = test_ppts.get(test_enter_ppt.ppt_name.makeExit()); 809 if (test_exit_ppt == null) { 810 throw new Daikon.UserError( 811 String.format( 812 "Neither ppt %s nor ppt %s found in %s", 813 exit_ppt_name, test_enter_ppt.ppt_name.makeExit(), test_filename)); 814 } 815 } 816 817 comparePpts( 818 app_enter_ppt, test_enter_ppt, 819 app_exit_ppt, test_exit_ppt); 820 } else if (num_args == 2) { 821 startProver(); 822 823 Collection<@KeyFor("app_ppts.nameToPpt") String> app_ppt_names = app_ppts.nameStringSet(); 824 Collection<@KeyFor("test_ppts.nameToPpt") String> test_ppt_names = test_ppts.nameStringSet(); 825 // These are keys in both app_ppts and test_ppts. 826 Set<String> common_names = new TreeSet<>(); 827 828 for (String name : app_ppt_names) { 829 @SuppressWarnings("nullness") // map: iterating over keyset 830 @NonNull PptTopLevel app_ppt = app_ppts.get(name); 831 832 if (!app_ppt.ppt_name.isEnterPoint()) { 833 // an exit point, and we only want entries 834 continue; 835 } 836 if (app_ppt.num_samples() > 0) { 837 if (test_ppt_names.contains(name) 838 && castNonNull(test_ppts.get(name)).num_samples() 839 > 0) { // correlated maps: test_ppts.get(name) is non-null because 840 // test_ppt_names.contains(name) is true 841 common_names.add(name); 842 } else { 843 System.out.println(name + " was used but not tested"); 844 } 845 } 846 } 847 848 for (String name : common_names) { 849 System.out.println(); 850 System.out.println("Looking at " + name); 851 @SuppressWarnings("nullness") // map: iterating over subset of keySet 852 @NonNull PptTopLevel app_enter_ppt = app_ppts.get(name); 853 @SuppressWarnings("nullness") // map: iterating over subset of keySet 854 @NonNull PptTopLevel test_enter_ppt = test_ppts.get(name); 855 @SuppressWarnings("nullness") // map: exit should be in map if enter is 856 @NonNull PptTopLevel app_exit_ppt = app_ppts.get(app_enter_ppt.ppt_name.makeExit()); 857 @SuppressWarnings("nullness") // map: exit should be in map if enter is 858 @NonNull PptTopLevel test_exit_ppt = test_ppts.get(test_enter_ppt.ppt_name.makeExit()); 859 860 assert app_exit_ppt != null; 861 assert test_exit_ppt != null; 862 comparePpts( 863 app_enter_ppt, test_enter_ppt, 864 app_exit_ppt, test_exit_ppt); 865 } 866 } else { 867 throw new Daikon.UserError("Too many arguments" + Global.lineSep + usage); 868 } 869 } 870}