001package daikon.test.inv; 002 003import static daikon.inv.Invariant.asInvClass; 004import static java.nio.charset.StandardCharsets.UTF_8; 005import static org.junit.Assert.assertEquals; 006import static org.junit.Assert.assertFalse; 007import static org.junit.Assert.assertNotNull; 008import static org.junit.Assert.fail; 009 010import daikon.*; 011import daikon.config.Configuration; 012import daikon.inv.*; 013import daikon.inv.binary.*; 014import daikon.inv.ternary.threeScalar.ThreeScalar; 015import daikon.inv.unary.*; 016import java.io.BufferedReader; 017import java.io.BufferedWriter; 018import java.io.File; 019import java.io.FileInputStream; 020import java.io.FileNotFoundException; 021import java.io.IOException; 022import java.io.InputStreamReader; 023import java.io.LineNumberReader; 024import java.io.UncheckedIOException; 025import java.lang.reflect.Field; 026import java.lang.reflect.Method; 027import java.nio.file.Files; 028import java.util.ArrayList; 029import java.util.Arrays; 030import java.util.List; 031import java.util.StringTokenizer; 032import junit.framework.*; 033import org.checkerframework.checker.interning.qual.Interned; 034import org.checkerframework.checker.nullness.qual.Nullable; 035import org.checkerframework.checker.signature.qual.BinaryName; 036import org.checkerframework.dataflow.qual.Pure; 037import org.junit.Test; 038import typequals.prototype.qual.Prototype; 039 040/** 041 * This is a tester for the results of adding or checking an sample to an invariant. It can test 042 * practically any invariant in the Daikon system given the appropriate commands. The test are 043 * configured from the {@code InvariantTest.commands} file and errors that occur are written to the 044 * InvariantTest.diffs file. For conveince a partcailly complete file InvariantTest.input can be 045 * used to generate a complete commands file. To generate InvariantTest.commands from 046 * InvariantTest.input run this class's main method with option "--generate_goals". 047 * 048 * <p>Each test case starts with a line containing the full name of the invariant then a second line 049 * containing the types of the arguments to the invariant's check and add method (excluding the 050 * count argument). After the test case's header any number of command lines may be included in a 051 * command file. Finally, after all command lines, the key work "end" must appear on its own line. 052 * 053 * <p>Each command line is starts with a command: "add:" or "check:". Following the command comes 054 * the arguments to be checked or added to the invariant. These arguments should be in the same 055 * format as in a dtrace file. Next comes the InvariantStatus that is expected to be returned by the 056 * check or add command on checking or adding the arguments. Finally, the expected format of the 057 * Invariant after checking or adding the arguments is included. (The format of the invariant is 058 * given by "Invariant.format_using(OutputFormat.DAIKON)") 059 * 060 * <p>A full example test case is as follows: 061 * 062 * <pre> 063 * daikon.inv.binary.twoSequence.PairwiseIntEqual 064 * int_array int_array 065 * add: [ 1 2 3 ]; [1 2 3 ]; no_change; a[] == b[] (elementwise) 066 * add: [ 10 -1 6 ]; [10 -1 6 ]; no_change; a[] == b[] (elementwise) 067 * add: [ -3 -3 -9 ]; [-3 6 -9 ]; falsified; a[] == b[] (elementwise) 068 * end 069 * </pre> 070 * 071 * Alternatively, this class can be used to generate a test case when given command lines that do 072 * not include expected InvariantStatus or invariant format. The proper input to generate the test 073 * above would be: 074 * 075 * <pre> 076 * daikon.inv.binary.twoSequence.PairwiseIntEqual 077 * int_array int_array 078 * add: [ 1 2 3 ]; [1 2 3 ] 079 * add: [ 10 -1 6 ]; [10 -1 6 ] 080 * add: [ -3 -3 -9 ]; [-3 6 -9 ] 081 * end 082 * </pre> 083 * 084 * To run a test case the method runTest should be used. To generate a test case the method 085 * generateTest should be used. 086 * 087 * <p>Note: no test case should contain the character ';' in any way other than to divide arguments 088 * with in a command line. 089 */ 090@SuppressWarnings("nullness") // test code 091public class InvariantAddAndCheckTester { 092 093 /** Indicates a string that when it starts a line signifies that the line is a comment. */ 094 public static final String COMMENT_STARTER_STRING = "#"; 095 096 /** A list containing all of the test formats. */ 097 public static final List<String> TEST_FORMAT_LIST = getTestFormatList(); 098 099 /** Allows for the configuring of Daikon options. */ 100 static Configuration config = Configuration.getInstance(); 101 102 private static final String commandsFileName = "daikon/test/inv/InvariantTest.commands"; 103 private static final String diffFileName = "daikon/test/inv/InvariantTest.diffs"; 104 105 private static final String lineSep = Global.lineSep; 106 107 /** 108 * This function produces the format list for intialization of the static format list variable. 109 */ 110 static List<String> getTestFormatList() { 111 List<String> result = new ArrayList<>(); 112 113 // Add test formats - hard coded in 114 result.add("daikon"); 115 result.add("java"); 116 result.add("esc"); 117 result.add("jml"); 118 result.add("dbc"); 119 result.add("simplify"); 120 121 return result; 122 } 123 124 /** This function is the actual function performed when this class is run through JUnit. */ 125 @Test 126 public void testFormats() { 127 128 // Don't care about comparability info because we are only 129 // creating variables for the purpose of being compared (thus they 130 // should all be comparable) 131 Daikon.ignore_comparability = true; 132 133 // run the actual test 134 135 if (!execute()) { 136 fail( 137 "At least one test failed." 138 + " Inspect java/daikon/test/InvariantAddAndCheckTest.diffs for error report."); 139 } 140 } 141 142 /** 143 * Returns the next non-comment, non-whitespace line of the input buffer. 144 * 145 * @param input the input buffer 146 * @return the next non-comment, non-whitespace line of the input buffer or null if the end of the 147 * buffer is reached before such a line can be found 148 */ 149 static @Nullable String getNextRealLine(BufferedReader input) { 150 String currentLine = ""; 151 152 try { 153 while (currentLine != null) { 154 currentLine = input.readLine(); 155 if (currentLine != null && !isComment(currentLine) && !isWhitespace(currentLine)) { 156 return currentLine; 157 } 158 } 159 } catch (IOException e) { 160 throw new RuntimeException(e.toString()); 161 } 162 return null; 163 } 164 165 /** 166 * This function performs the testing for a particular format indicated by the format string. It 167 * subsequently sets up appropriate input and output streams for the format test, performs the 168 * test, and the compares the test results to the goals. If the goals differ from the actual 169 * results the test fails. 170 * 171 * @return false if any tests fail 172 */ 173 private static boolean execute() { 174 String output; 175 try (LineNumberReader commandReader = getCommands()) { 176 output = performTest(commandReader); 177 } catch (IOException e) { 178 throw new UncheckedIOException(e); 179 } 180 181 if (output == null) { // no errors 182 return true; 183 } else { 184 BufferedWriter diffsOutput = getDiffsOutputWriter(); 185 try { 186 diffsOutput.write(output, 0, output.length()); 187 diffsOutput.close(); 188 } catch (IOException e) { 189 throw new RuntimeException("Could not output generated diffs"); 190 } 191 return false; 192 } 193 } 194 195 /** 196 * This function performs an individual formatting test after the input and output streams have 197 * been created. 198 * 199 * @param commands the input that decides which tests to perform 200 * @return a String holding the error messages for any failed tests, or null if no tests are 201 * failed 202 */ 203 private static @Nullable String performTest(LineNumberReader commands) { 204 StringBuilder output = new StringBuilder(); 205 // List invariantTestCases = new ArrayList(); 206 boolean noTestFailed = true; 207 208 while (true) { 209 // Create a new test case 210 // FormatTestCase currentCase = FormatTestCase.readFromFile(commands, generateGoals); 211 212 // if (currentCase == null) 213 // break; 214 // else { 215 // invariantTestCases.add(currentCase); 216 String results = AddAndCheckTestCase.runTest(commands); 217 if (results == null) { 218 break; 219 } 220 if (!(results.length() == 0)) { 221 // output.print(currentCase.getDiffString()); 222 output.append(results); 223 noTestFailed = false; 224 } 225 } 226 if (noTestFailed) { 227 return null; 228 } else { 229 return output.toString(); 230 } 231 } 232 233 /** 234 * Returns a reader for the {@code InvariantTest.commands} resource. 235 * 236 * @return a reader for the {@code InvariantTest.commands} resource 237 */ 238 private static LineNumberReader getCommands() { 239 // Calculate input file locations 240 // URL inputFileLocation = 241 // ClassLoader.getSystemClassLoader().getSystemResource("InvariantTest.commands"); 242 243 // if (inputFileLocation == null) 244 // fail("Input file for invariant format tests missing." + 245 // " (Should be in InvariantTest.commands" + 246 // " and it must be within the classpath)"); 247 248 // String inputFile = inputFileLocation.getFile(); 249 // System.out.println(System.getProperty("user.dir")); 250 LineNumberReader commands; 251 try { 252 commands = 253 new LineNumberReader(new InputStreamReader(new FileInputStream(commandsFileName), UTF_8)); 254 } catch (FileNotFoundException e) { 255 fail( 256 "Unexpected FileNotFoundException (very strange since the URL of the file was found" 257 + " earlier)"); 258 throw new Error("Unreachable control flow"); 259 } 260 return commands; 261 } 262 263 private static BufferedWriter getDiffsOutputWriter() { 264 try { 265 return Files.newBufferedWriter(new File(diffFileName).toPath(), UTF_8); 266 } catch (IOException e) { 267 throw new RuntimeException("Cannot write output into " + diffFileName); 268 } 269 } 270 271 /** 272 * Determines whether a line is a comment or not. 273 * 274 * @param line the line in question 275 * @return true if the line is a comment (that is, not to be interpretted as a command); false 276 * otherwise 277 */ 278 @Pure 279 static boolean isComment(String line) { 280 return line.startsWith(COMMENT_STARTER_STRING); 281 } 282 283 /** 284 * Determines whether a given line is made only of whitespcae. 285 * 286 * @param line the line in question 287 * @return true if the line is made up only of whitespace, false otherwise 288 */ 289 @Pure 290 static boolean isWhitespace(String line) { 291 for (int x = 0; x < line.length(); x++) { 292 if (!Character.isWhitespace(line.charAt(x))) { 293 return false; 294 } 295 } 296 return true; 297 } 298 299 private static class AddAndCheckTestCase { 300 301 /** The Invariant object to be tested. */ 302 private static Invariant invariantToTest; 303 304 /** 305 * The types of the arguments to invariantToTest's check and add commands (not including the 306 * count argument). 307 */ 308 private static ProglangType[] types; 309 310 /** invariantToTest's addModified method. */ 311 private static Method addModified; 312 313 /** invariantToTest's checkModified method. */ 314 private static Method checkModified; 315 316 /** invariantToTest's format_using method. */ 317 private static Method outputProducer; 318 319 /** Contains error messages if any test commands fail. */ 320 private static StringBuilder results; 321 322 /** The token that divides the different arguments to a test command. */ 323 private static final String argDivider = ";"; 324 325 /** 326 * Returns a string containing error messages for any failed cases. Returns the empty string if 327 * there are no failed cases. Returns null if commands is empty (there are no more test cases 328 * and the end of the file has been reached). 329 * 330 * @return a string containing error messages for any failed cases 331 */ 332 public static @Nullable String runTest(LineNumberReader commands) { 333 boolean endOfFile = initFields(commands, false); 334 if (endOfFile) { 335 return null; 336 } 337 while (true) { 338 String commandLine = getNextRealLine(commands); 339 int lineNumber = commands.getLineNumber(); 340 if (InvariantAddAndCheckTester.isComment(commandLine)) { 341 continue; 342 } else if (isTestTerminator(commandLine)) { 343 break; 344 } else if (isAddCommand(commandLine) || isCheckCommand(commandLine)) { 345 executeCheckOrAddCommand(commandLine, lineNumber); 346 } else if (isCompareCommand(commandLine)) { 347 } else { 348 throw new RuntimeException("unrecognized command"); 349 } 350 } 351 return results.toString(); 352 } 353 354 /** 355 * Returns a String containing the proper add and check commands for this input lines of this 356 * test case. 357 * 358 * @return a String containing the proper add and check commands for this input lines of this 359 * test case 360 */ 361 @SuppressWarnings("UnusedMethod") 362 public static @Nullable String generateTest(LineNumberReader commands) { 363 boolean endOfFile = initFields(commands, true); 364 if (endOfFile) { 365 return null; 366 } 367 while (true) { 368 String commandLine = getNextLine(commands).trim(); 369 int lineNumber = commands.getLineNumber(); 370 if (InvariantAddAndCheckTester.isComment(commandLine)) { 371 results.append(commandLine + lineSep); 372 } else if (isTestTerminator(commandLine)) { 373 results.append(commandLine + lineSep + lineSep); 374 break; 375 } else if (isAddCommand(commandLine) || isCheckCommand(commandLine)) { 376 generateCheckOrAddCommand(commandLine, lineNumber); 377 } else if (isCompareCommand(commandLine)) { 378 // generateCompareCommand(commandLine); 379 } else { 380 throw new RuntimeException("unrecognized command"); 381 } 382 } 383 return results.toString(); 384 } 385 386 /** 387 * Initializes the fields of this class based on the first two lines of a case which include the 388 * class name and parameter types. 389 * 390 * @return true is end of file is reached 391 */ 392 private static boolean initFields(LineNumberReader commands, boolean generatingCommands) { 393 394 results = new StringBuilder(); 395 396 @SuppressWarnings("signature") // user input, should be checked 397 @BinaryName String className = getNextRealLine(commands); 398 399 // End of file reached 400 if (className == null) { 401 return true; 402 } 403 404 // Load the class from file 405 Class<? extends Invariant> classToTest = asInvClass(getClass(className)); 406 407 try { 408 @SuppressWarnings("UnusedVariable") 409 Field ignore = classToTest.getField("dkconfig_enabled"); // Enable if needs to be done 410 InvariantAddAndCheckTester.config.apply(className + ".enabled", "true"); 411 } catch (NoSuchFieldException e) { // Otherwise do nothing 412 } 413 414 if (generatingCommands) { 415 results.append(className + lineSep); 416 } 417 418 // Instantiate variables to be used as the names in the 419 // invariants, variables are labeled a,b,c and so on as they 420 // appear 421 String typeString = getNextRealLine(commands); 422 423 types = getTypes(typeString); 424 425 VarInfo[] vars = getVarInfos(classToTest, types); 426 PptSlice sl = createSlice(vars, daikon.test.Common.makePptTopLevel("Test:::OBJECT", vars)); 427 428 // Create an actual instance of the class 429 invariantToTest = instantiateClass(classToTest, sl); 430 431 addModified = getAddModified(invariantToTest.getClass()); 432 checkModified = getCheckModified(invariantToTest.getClass()); 433 outputProducer = getOutputProducer(invariantToTest.getClass()); 434 435 assertEquals(types.length, getArity(invariantToTest.getClass())); 436 437 if (generatingCommands) { 438 results.append(typeString + lineSep); 439 } 440 return false; 441 } 442 443 /** 444 * Given a line from a command file, generates and executes the appropriate check or add 445 * command, and checks the results against the goal. If the results and goal do not match, a 446 * message is added to the results string buffer. 447 */ 448 private static void executeCheckOrAddCommand(String command, int lineNumber) { 449 450 // remove the command 451 String args = command.substring(command.indexOf(":") + 1); 452 453 StringTokenizer tokens = new StringTokenizer(args, argDivider); 454 if (tokens.countTokens() != types.length + 2) { 455 throw new RuntimeException( 456 "Number of arguments to add command on line " 457 + lineNumber 458 + " is: " 459 + tokens.countTokens() 460 + " but should be: " 461 + (types.length + 2)); 462 } 463 Object[] params = getParams(tokens); 464 InvariantStatus goalStatus = parseStatus(tokens.nextToken().trim()); 465 tokens.nextToken(); // executed for side effect 466 assertFalse(tokens.hasMoreTokens()); 467 InvariantStatus resultStatus; 468 try { 469 if (isCheckCommand(command)) { 470 resultStatus = getCheckStatus(params); 471 } else { 472 resultStatus = getAddStatus(params); 473 } 474 } catch (Exception e) { 475 throw new Error( 476 String.format( 477 "Problem with \"%s\" on line %d of %s", command, lineNumber, commandsFileName), 478 e); 479 } 480 if (resultStatus != goalStatus) { 481 results.append( 482 "Error on line " 483 + lineNumber 484 + ":" 485 + lineSep 486 + "Expected InvariantStatus: " 487 + goalStatus 488 + lineSep 489 + "Found InvariantStatus: " 490 + resultStatus 491 + lineSep); 492 } 493 } 494 495 /** Given a line from an input file, generates appropriate check or add command. */ 496 private static void generateCheckOrAddCommand(String command, int lineNumber) { 497 // remove the command 498 String args = command.substring(command.indexOf(":") + 1); 499 500 StringTokenizer tokens = new StringTokenizer(args, argDivider); 501 if (tokens.countTokens() != types.length) { 502 throw new RuntimeException( 503 "Number of arguments to generate an add command on line: " 504 + lineNumber 505 + " is: " 506 + tokens.countTokens() 507 + " but should be: " 508 + types.length); 509 } 510 Object[] params = getParams(tokens); 511 assertFalse(tokens.hasMoreTokens()); 512 InvariantStatus goalStatus; 513 if (isCheckCommand(command)) { 514 goalStatus = getCheckStatus(params); 515 } else { 516 goalStatus = getAddStatus(params); 517 } 518 String invariantFormat = getInvariantFormat(); 519 results.append( 520 command 521 + argDivider 522 + " " 523 + goalStatus.toString() 524 + argDivider 525 + " " 526 + invariantFormat 527 + lineSep); 528 } 529 530 /** 531 * Returns an array of the arguments to be passed into check_modified or add_modified produced 532 * from tokens. 533 * 534 * @return an array of the arguments to be passed into check_modified or add_modified produced 535 * from tokens 536 */ 537 private static Object[] getParams(StringTokenizer tokens) { 538 // add one for the "count" argument 539 Object[] params = new Object[types.length + 1]; 540 for (int i = 0; i < types.length; i++) { 541 params[i] = types[i].parse_value(tokens.nextToken().trim(), null, null); 542 } 543 params[params.length - 1] = 1; // the "count" argument 544 return params; 545 } 546 547 /** 548 * Returns the InvariantStatus produced by invoking invariantToTest's add_modified method on the 549 * arguments represented by params. 550 * 551 * @return the InvariantStatus produced by invoking invariantToTest's add_modified method on the 552 * arguments represented by params 553 */ 554 private static InvariantStatus getAddStatus(Object[] params) { 555 try { 556 return (InvariantStatus) addModified.invoke(invariantToTest, params); 557 } catch (Exception e) { 558 throw new RuntimeException( 559 "getAddStatus: error invoking addModified(" 560 + Arrays.toString(params) 561 + ") on " 562 + invariantToTest.getClass() 563 + "; commandsFileName=" 564 + commandsFileName, 565 e); 566 } 567 } 568 569 /** 570 * Returns the InvariantStatus produced by invoking invariantToTest's check_modified method on 571 * the arguments represented by params. 572 * 573 * @return the InvariantStatus produced by invoking invariantToTest's check_modified method on 574 * the arguments represented by params 575 */ 576 private static InvariantStatus getCheckStatus(Object[] params) { 577 try { 578 return (InvariantStatus) checkModified.invoke(invariantToTest, params); 579 } catch (Exception e) { 580 throw new RuntimeException(" error in " + invariantToTest.getClass() + ": " + e); 581 } 582 } 583 584 /** 585 * Returns a String representation of the invariantToTest. This String is produced by invoking 586 * the invariant's format_using with method with the argument {@code OutputFormat.Daikon}. 587 * 588 * @return a String representation of the invariantToTest 589 */ 590 private static String getInvariantFormat() { 591 try { 592 return (String) outputProducer.invoke(invariantToTest, new Object[] {OutputFormat.DAIKON}); 593 } catch (Exception e) { 594 throw new RuntimeException(invariantToTest + " " + outputProducer); 595 } 596 } 597 598 /** 599 * Returns an InvariantStatus that the string status parses to. 600 * 601 * @param status the string representation of an InvariantStatus 602 * @return an InvariantStatus that the string status parses to 603 */ 604 private static InvariantStatus parseStatus(String status) { 605 status = status.trim(); 606 if (status.equals("no_change")) { 607 return InvariantStatus.NO_CHANGE; 608 } else if (status.equals("falsified")) { 609 return InvariantStatus.FALSIFIED; 610 } 611 if (status.equals("weakened")) { 612 return InvariantStatus.WEAKENED; 613 } else { 614 throw new RuntimeException("Unrecognized InvariantStatus: " + status); 615 } 616 } 617 618 /** 619 * This function returns the add_modified method from the class type provided. 620 * 621 * @param theClass the class in which to find the add_modified method 622 * @return the add_modified method if it exists, null otherwise 623 * @throws RuntimeException if check_modified does not exist 624 */ 625 private static Method getAddModified(Class<? extends Invariant> theClass) { 626 Method[] methods = theClass.getMethods(); 627 628 Method currentMethod; 629 for (int i = 0; i < methods.length; i++) { 630 currentMethod = methods[i]; 631 if (currentMethod.getName().lastIndexOf("add_modified") != -1) { 632 return currentMethod; 633 } 634 } 635 throw new RuntimeException("Cannot find add_modified method"); 636 } 637 638 /** 639 * This function returns the check_modified method from the class type provided. 640 * 641 * @param theClass the class in which to find the check_modified method 642 * @return the check_modified method if it exists 643 * @throws RuntimeException if check_modified does not exist 644 */ 645 private static Method getCheckModified(Class<? extends Invariant> theClass) { 646 Method[] methods = theClass.getMethods(); 647 648 Method currentMethod; 649 for (int i = 0; i < methods.length; i++) { 650 currentMethod = methods[i]; 651 if (currentMethod.getName().lastIndexOf("check_modified") != -1) { 652 return currentMethod; 653 } 654 } 655 throw new RuntimeException("Cannot find check_modified method"); 656 } 657 658 /** 659 * Returns the method of invariant named by theClass that produces a String representation of 660 * the invariant. 661 * 662 * @return the method of invariant named by theClass that produces a String representation of 663 * the invariant 664 */ 665 private static Method getOutputProducer(Class<? extends Invariant> theClass) { 666 Method[] methods = theClass.getMethods(); 667 668 Method currentMethod; 669 for (int i = 0; i < methods.length; i++) { 670 currentMethod = methods[i]; 671 672 // Method should be called format_using 673 if (currentMethod.getName().lastIndexOf("format_using") != -1) { 674 return currentMethod; 675 } 676 } 677 throw new RuntimeException("Cannot find format_using method"); 678 } 679 680 /** 681 * This function loads a class from file into the JVM given its fully-qualified name. 682 * 683 * @param classInfo the fully-qualified class name 684 * @return a Class object representing the class name if such a class is defined, otherwise null 685 */ 686 private static Class<?> getClass(@BinaryName String classInfo) { 687 try { 688 return ClassLoader.getSystemClassLoader().loadClass(classInfo); 689 } catch (ClassNotFoundException e) { 690 throw new RuntimeException(e.toString()); 691 } 692 } 693 694 /** 695 * This function is an alias for the {@link #getNextRealLine(BufferedReader) getNextRealLine} 696 * method. 697 */ 698 static String getNextRealLine(BufferedReader buffer) { 699 return InvariantAddAndCheckTester.getNextRealLine(buffer); 700 } 701 702 @Pure 703 private static boolean isTestTerminator(String command) { 704 String commandTrimmed = command.trim(); 705 return commandTrimmed.startsWith("end"); 706 } 707 708 @Pure 709 private static boolean isAddCommand(String command) { 710 String commandTrimmed = command.trim(); 711 return commandTrimmed.startsWith("add"); 712 } 713 714 @Pure 715 private static boolean isCheckCommand(String command) { 716 String commandTrimmed = command.trim(); 717 return commandTrimmed.startsWith("check"); 718 } 719 720 @Pure 721 private static boolean isCompareCommand(String command) { 722 String commandTrimmed = command.trim(); 723 return commandTrimmed.startsWith("compare"); 724 } 725 726 /** 727 * This function creates an array of VarInfo objects that can represent a set of program 728 * language types provided by the caller. Their names carry no meaning except for the type. 729 * 730 * @param classToTest the invariant class for which the VarInfos must be determined 731 * @param types the types that the VarInfos must have 732 * @return an array of VarInfo objects that have the types corresponding to those in types 733 */ 734 private static VarInfo[] getVarInfos( 735 Class<? extends Invariant> classToTest, ProglangType[] types) { 736 int numInfos = getArity(classToTest); 737 738 if (numInfos == -1) { 739 throw new RuntimeException("Class arity cannot be determined."); 740 } 741 742 VarInfo[] result = new VarInfo[numInfos]; 743 744 for (int i = 0; i < numInfos; i++) { 745 result[i] = getVarInfo(types[i], i); 746 } 747 748 return result; 749 } 750 751 /** 752 * This function returns a VarInfo of the given type. The name is the ith letter of the 753 * alphabet. (Produces variables such that i=0 → name=a, i=1 → name=b, ...) 754 * 755 * @param type the desired type that the VarInfo will represent 756 * @param i a unique identifier that determines the name to be used 757 * @return a VarInfo object that described the type 758 */ 759 private static VarInfo getVarInfo(ProglangType type, int i) { 760 assertNotNull(type); 761 762 String arrayModifier = ""; 763 764 if (type == ProglangType.INT_ARRAY 765 || type == ProglangType.DOUBLE_ARRAY 766 || type == ProglangType.STRING_ARRAY) { // Is it an array ? 767 arrayModifier = "[]"; 768 } 769 770 // Create the new VarInfoName dependent on a couple factors: 771 // - If it is an array, attach [] to the name to make parse return 772 // the correct thing 773 // - The base part of the name will be "a" for the first var in an 774 // invariant, "b" for the second, and so on 775 // - The ProglangType will be specified in the parameters 776 // - The comparability will be none 777 @SuppressWarnings("interning") 778 @Interned VarInfo result = 779 new VarInfo( 780 new String(new char[] {(char) ('a' + i)}) + arrayModifier, 781 type, 782 type, 783 VarComparabilityNone.it, 784 VarInfoAux.getDefault()); 785 return result; 786 } 787 788 /** 789 * This function determines the arity of a given invariant given its class. 790 * 791 * @param classToTest the invariant type in question 792 * @return the arity of the invariant if it can be determined, -1 otherwise 793 */ 794 private static int getArity(Class<? extends Invariant> classToTest) { 795 if (UnaryInvariant.class.isAssignableFrom(classToTest)) { 796 return 1; 797 } 798 if (BinaryInvariant.class.isAssignableFrom(classToTest)) { 799 return 2; 800 } 801 if (ThreeScalar.class.isAssignableFrom(classToTest)) { 802 return 3; 803 } 804 805 return -1; 806 } 807 808 /** 809 * This function parses a format string -- a space separated list of types -- and determines the 810 * types of objects to be collected. 811 * 812 * @param typeNames the type string for an invariant 813 * @return an array of ProglangTypes representing the data in typeNames 814 */ 815 private static ProglangType[] getTypes(String typeNames) { 816 StringTokenizer stok = new StringTokenizer(typeNames); 817 ProglangType[] result = new ProglangType[stok.countTokens()]; 818 819 for (int i = 0; i < result.length; i++) { 820 String typeName = stok.nextToken(); 821 822 // A way of doing the same thing as below in fewer lines of code 823 // Doesn't seem to work... 824 // result[i] = ProglangType.parse(typeName); 825 826 if (typeName.equalsIgnoreCase("int")) { 827 result[i] = ProglangType.INT; 828 } else if (typeName.equalsIgnoreCase("double")) { 829 result[i] = ProglangType.DOUBLE; 830 } else if (typeName.equalsIgnoreCase("string")) { 831 result[i] = ProglangType.STRING; 832 } else if (typeName.equalsIgnoreCase("int_array")) { 833 result[i] = ProglangType.INT_ARRAY; 834 } else if (typeName.equalsIgnoreCase("double_array")) { 835 result[i] = ProglangType.DOUBLE_ARRAY; 836 } else if (typeName.equalsIgnoreCase("string_array")) { 837 result[i] = ProglangType.STRING_ARRAY; 838 } else { 839 return null; 840 } 841 842 assertNotNull(result[i]); 843 } 844 845 return result; 846 } 847 848 /** 849 * This function creates an appropriate PptSlice for a given set of VarInfos and a PptTopLevel. 850 * 851 * @param vars an array of VarInfo objects for which the slice is to be created 852 * @param ppt the PptTopLevel object representing the program point 853 * @return a new PptSlice object if the creation of one is possible, else throws a 854 * RuntimeException 855 */ 856 private static PptSlice createSlice(VarInfo[] vars, PptTopLevel ppt) { 857 if (vars.length == 1) { 858 assertNotNull(vars[0]); 859 return new PptSlice1(ppt, vars); 860 } else if (vars.length == 2) { 861 assertNotNull(vars[0]); 862 assertNotNull(vars[1]); 863 return new PptSlice2(ppt, vars); 864 } else if (vars.length == 3) { 865 assertNotNull(vars[0]); 866 assertNotNull(vars[1]); 867 assertNotNull(vars[2]); 868 return new PptSlice3(ppt, vars); 869 } else { 870 throw new RuntimeException( 871 "Improper vars passed to createSlice (length = " + vars.length + ")"); 872 } 873 } 874 875 /** 876 * This function instantiates an invariant class by using the {@code <type>(PptSlice)} 877 * constructor. 878 * 879 * @param theClass the invariant class to be instantiated 880 * @param sl the PptSlice representing the variables about which an invariant is determined 881 * @return an instance of the class in theClass if one can be constructed, else throw a 882 * RuntimeException 883 */ 884 private static Invariant instantiateClass(Class<? extends Invariant> theClass, PptSlice sl) { 885 try { 886 Method get_proto = theClass.getMethod("get_proto", new Class<?>[] {}); 887 Invariant proto = (@Prototype Invariant) get_proto.invoke(null, new Object[] {}); 888 Invariant inv = proto.instantiate(sl); 889 return inv; 890 } catch (Exception e) { 891 e.printStackTrace(System.out); 892 throw new RuntimeException( 893 "Error while instantiating invariant " + theClass.getName() + ": " + e.toString()); 894 } 895 } 896 897 private static String getNextLine(LineNumberReader input) { 898 try { 899 return input.readLine(); 900 } catch (IOException e) { 901 throw new RuntimeException("Exception reading next line"); 902 } 903 } 904 } 905}