001package daikon.config; 002 003import com.sun.source.doctree.DocCommentTree; 004import com.sun.source.doctree.DocTree; 005import com.sun.source.util.DocTrees; 006import java.io.PrintWriter; 007import java.lang.reflect.Field; 008import java.lang.reflect.Modifier; 009import java.util.ArrayList; 010import java.util.Arrays; 011import java.util.Collections; 012import java.util.HashMap; 013import java.util.List; 014import java.util.Locale; 015import java.util.Map; 016import java.util.Set; 017import java.util.regex.Pattern; 018import javax.lang.model.SourceVersion; 019import javax.lang.model.element.Element; 020import javax.lang.model.element.ElementKind; 021import javax.lang.model.element.TypeElement; 022import javax.tools.Diagnostic; 023import jdk.javadoc.doclet.Doclet; 024import jdk.javadoc.doclet.DocletEnvironment; 025import jdk.javadoc.doclet.Reporter; 026import org.checkerframework.checker.nullness.qual.KeyFor; 027import org.checkerframework.checker.nullness.qual.Nullable; 028import org.checkerframework.checker.signature.qual.ClassGetName; 029import org.plumelib.reflection.ReflectionPlume; 030import org.plumelib.util.CollectionsPlume; 031import org.plumelib.util.FilesPlume; 032 033/** 034 * ParameterDoclet is a JavaDoc doclet that collects information about the run-time configuration 035 * options for the Daikon tools. Refer to the {@code --config} command-line option in the Daikon 036 * manual for an introduction to the configuration system. 037 */ 038@SuppressWarnings("nullness") // need help with this 039public class ParameterDoclet implements Doclet { 040 041 /** A value that indicates a method completed successfully. */ 042 private static final boolean OK = true; 043 044 /** A value that indicates a method did not complete successfully. */ 045 private static final boolean FAILED = false; 046 047 /** File name of destination for output. */ 048 private @Nullable String outFilename = null; 049 050 /** If true, then output format is Texinfo. */ 051 private boolean formatTexinfo = false; 052 053 /** The DocTrees instance assocated with the DocletEnvironment. */ 054 private DocTrees docTrees; 055 056 /** Used to report errors. */ 057 private Reporter reporter; 058 059 /** A data structure for the document categories. */ 060 protected DocCategory[] categories; 061 062 /////////////////////////////////////////////////////////////////////////// 063 /// Doclet-specific methods 064 /// 065 066 @Override 067 public void init(Locale locale, Reporter reporter) { 068 this.reporter = reporter; 069 } 070 071 @Override 072 public String getName() { 073 return getClass().getSimpleName(); 074 } 075 076 @Override 077 public Set<? extends Doclet.Option> getSupportedOptions() { 078 return docletOptions; 079 } 080 081 @Override 082 public SourceVersion getSupportedSourceVersion() { 083 return SourceVersion.latest(); 084 } 085 086 /** Entry point for this doclet (invoked by javadoc). */ 087 @Override 088 public boolean run(DocletEnvironment denv) { 089 090 postprocessOptions(); 091 docTrees = denv.getDocTrees(); 092 initDocCategories(); 093 094 // Save a list of class elements for subsequent processing 095 List<TypeElement> clazzes = new ArrayList<>(); 096 for (Element item : denv.getSpecifiedElements()) { 097 if (!isTypeElement(item)) { 098 throw new Error( 099 String.format("Unexpected specified element of kind %s: %s", item.getKind(), item)); 100 } 101 clazzes.add((TypeElement) item); 102 } 103 104 // go through the list of classes and put in the derived class information 105 for (TypeElement te : clazzes) { 106 for (Element field : te.getEnclosedElements()) { 107 if (field.getKind() != ElementKind.FIELD) continue; 108 processField(field); 109 } 110 } 111 112 // output the field data 113 System.out.println("Opening " + outFilename + " for output..."); 114 PrintWriter outf; 115 try { 116 outf = new PrintWriter(FilesPlume.newBufferedFileWriter(outFilename)); 117 } catch (Exception e) { 118 throw new Error("Unable to open file: " + outFilename, e); 119 } 120 121 if (formatTexinfo) { 122 writeTexInfo(outf); 123 } else { 124 writeText(outf); 125 } 126 outf.close(); 127 128 return OK; 129 } 130 131 // ============================== NON-STATIC METHODS ============================== 132 133 /** 134 * A document category, or a subsection of the "List of configuration options" section in the 135 * manual. 136 */ 137 static class DocCategory { 138 139 /** 140 * If non-null, then include only variables whose fully-qualified name starts with this prefix. 141 */ 142 public @Nullable String prefix; 143 144 /** 145 * If non-null, then include only variables with this simple name. Note that this is a field 146 * name that starts with "dkconfig_", not a configuration option name. 147 */ 148 public @Nullable String fieldName; 149 150 /** Include all configuration options whose fully-qualified name is in the list. */ 151 public List<String> fqNames; 152 153 /** The subsection name. */ 154 public String description; 155 156 /** Text that appears in the subsection before the list of configuration options. */ 157 public String blurb; 158 159 /** A map from a field name to its description. */ 160 public Map<String, String> fields; 161 162 /** 163 * Create a new DocCategory. 164 * 165 * @param prefix if non-null, include only variables whose fully-qualified name starts with this 166 * prefix 167 * @param simpleName if non-null, include only configuration options with this simple name 168 * @param fqConfigNames if non-null, include only configuration options whose fully-qualified 169 * name is in this list 170 * @param description the subsection name 171 * @param blurbLines text that appears in the subsection before the list of configuration 172 * options 173 */ 174 public DocCategory( 175 @Nullable String prefix, 176 @Nullable String simpleName, 177 @Nullable List<String> fqConfigNames, 178 String description, 179 String[] blurbLines) { 180 this( 181 prefix, 182 simpleName, 183 fqConfigNames, 184 description, 185 String.join(System.lineSeparator(), blurbLines)); 186 } 187 188 /** 189 * Create a new DocCategory. 190 * 191 * @param prefix if non-null, include only variables whose fully-qualified name starts with this 192 * prefix 193 * @param simpleName if non-null, include only configuration options with this simple name 194 * @param fqConfigNames if non-null, include only configuration options whose fully-qualified 195 * name is in this list 196 * @param description the subsection name 197 * @param blurb text that appears in the subsection before the list of configuration options 198 */ 199 public DocCategory( 200 @Nullable String prefix, 201 @Nullable String simpleName, 202 @Nullable List<String> fqConfigNames, 203 String description, 204 String blurb) { 205 this.prefix = prefix; 206 if (simpleName == null) { 207 fieldName = null; 208 } else { 209 fieldName = Configuration.PREFIX + simpleName; 210 } 211 if (fqConfigNames == null) { 212 this.fqNames = Collections.emptyList(); 213 } else { 214 this.fqNames = fqConfigNames; 215 } 216 this.description = description; 217 this.blurb = blurb; 218 fields = new HashMap<>(); 219 } 220 221 /** 222 * Return true if the given variable (that represents a configuration option) should be included 223 * in this section. 224 * 225 * @param fullConfigName the fully-qualified name of a Daikon configuration variable (no 226 * "dkconfig_") 227 * @param simpleFieldName the simple name of the variable (starts with "dkconfig_") 228 * @return true if the given field should be included in this section of the manual 229 */ 230 public boolean matches(String fullConfigName, String simpleFieldName) { 231 return ((prefix == null || fullConfigName.startsWith(prefix)) 232 && (fieldName == null || fieldName.equals(simpleFieldName))) 233 || fqNames.contains(fullConfigName); 234 } 235 } 236 237 /** Initialize the categories data structure. */ 238 public void initDocCategories() { 239 categories = 240 new DocCategory[] { 241 // Do not re-order these options! The pattern-matching is sensitive to the order 242 // and the parent document knows the filter option comes first (for node linking). 243 new DocCategory( 244 "daikon.inv.filter.", 245 "enabled", 246 null, 247 "Options to enable/disable filters", 248 new String[] { 249 "@cindex filters, enabling/disabling", 250 "These configuration options enable or disable filters that suppress printing", 251 "of certain invariants. Invariants are filtered if they are redundant.", 252 "See @ref{Invariant filters}, for more information.", 253 "Also see configuration option @code{daikon.PrintInvariants.print_all}." 254 }), 255 new DocCategory( 256 "daikon.inv.", 257 "enabled", 258 null, 259 "Options to enable/disable specific invariants", 260 new String[] { 261 "@cindex invariants, enabling/disabling", 262 "These options control whether Daikon looks for specific kinds of invariants.", 263 "See @ref{Invariant list}, for more information about the corresponding invariants." 264 }), 265 new DocCategory( 266 "daikon.inv.", 267 null, 268 null, 269 "Other invariant configuration parameters", 270 new String[] { 271 "@cindex invariants, configuring", 272 "The configuration options listed in this section parameterize the behavior of" 273 + " certain invariants.", 274 "See @ref{Invariant list}, for more information about the invariants." 275 }), 276 new DocCategory( 277 "daikon.derive.", 278 null, 279 null, 280 "Options to enable/disable derived variables", 281 new String[] { 282 "@cindex derived variables, enabling/disabling", 283 "These options control whether Daikon looks for invariants involving certain forms" 284 + " of derived variables.", 285 "Also see @ref{Variable names}." 286 }), 287 new DocCategory( 288 "daikon.simplify.", 289 null, 290 null, 291 "Simplify interface configuration options", 292 new String[] { 293 "@cindex Simplify theorem prover, configuring", 294 "The configuration options in this section are used to customize the interface to" 295 + " the Simplify theorem prover.", 296 "See the description of the @option{--suppress_redundant} command-line option in" 297 + " @ref{Options to control invariant detection}." 298 }), 299 new DocCategory( 300 "daikon.split.", 301 null, 302 null, 303 "Splitter options", 304 new String[] { 305 "@cindex Splitters, configuring", 306 "The configuration options in this section are used to customize the behavior" 307 + " of splitters,", 308 "which yield conditional invariants and implications" 309 + " (@pxref{Conditional invariants})." 310 }), 311 new DocCategory( 312 "daikon.Debug.", 313 null, 314 null, 315 "Debugging options", 316 new String[] { 317 "@cindex Splitters, configuring", 318 "The configuration options in this section are used to cause extra output that is" 319 + " useful for debugging.", 320 "Also see section \"Daikon debugging options\" (@pxref{Daikon debugging options})." 321 }), 322 new DocCategory( 323 "dummy prefix that won't match anything", 324 "dummy simple name that won't match anything", 325 Arrays.asList( 326 "daikon.Daikon.quiet", 327 "daikon.PrintInvariants.print_all", 328 // Progress output 329 "daikon.Daikon.progress_delay", 330 "daikon.Daikon.progress_display_width", 331 "daikon.FileIO.count_lines", 332 "daikon.FileIO.dtrace_line_count", 333 // Statistics 334 "daikon.PrintInvariants.true_inv_cnt", 335 "daikon.Daikon.print_sample_totals", 336 // Other 337 "daikon.PrintInvariants.print_inv_class", 338 "daikon.Daikon.output_conditionals", 339 "daikon.Daikon.guardNulls", 340 "daikon.FileIO.unmatched_procedure_entries_quiet", 341 "daikon.FileIO.verbose_unmatched_procedure_entries"), 342 "Quantity of output", 343 new String[] { 344 "@cindex Output, quantity of", 345 "The configuration options in this section make Daikon print more or less output.", 346 "They do not affect which invariants Daikon computes, only how it ouputs them.", 347 "Also see the following section." 348 }), 349 new DocCategory( 350 null, 351 null, 352 null, 353 "General configuration options", 354 new String[] {"This section lists miscellaneous configuration options for Daikon."}) 355 }; 356 } 357 358 /** 359 * Call Process(String, String, String) for each configuration field found. Intended to be 360 * overridden. 361 * 362 * @param field the javadoc element for a member field. 363 */ 364 public void processField(Element field) { 365 String name = field.getSimpleName().toString(); 366 if (name.startsWith(Configuration.PREFIX)) { 367 String fullname = field.getEnclosingElement().toString() + "." + name; 368 int snip = fullname.indexOf(Configuration.PREFIX); 369 fullname = 370 fullname.substring(0, snip) + fullname.substring(snip + Configuration.PREFIX.length()); 371 // setup the comment for info 372 String desc = getDocComment(docTrees.getDocCommentTree(field)); 373 process(fullname, name, desc); 374 } 375 } 376 377 /** A value that indicates no description was found. */ 378 public static String NO_DESCRIPTION = "(no description provided)"; 379 380 /** A value that indicates no default value was found. */ 381 public static String UNKNOWN_DEFAULT = "The default value is not known."; 382 383 /** A Pattern used to check for the end of a sentence. */ 384 public static Pattern endOfSentence; 385 386 static { 387 endOfSentence = Pattern.compile("[.?!>](\\))?$"); 388 } 389 390 /** 391 * Add (name, desc) pair to the map field 'fields' for the appropriate category. 392 * 393 * @param fullname the fully-qualified name of a Daikon configuration variable (no "dkconfig_") 394 * @param name the simple name of the variable (starts with "dkconfig_") 395 * @param desc the javadoc comment for this variable 396 */ 397 public void process(String fullname, String name, String desc) { 398 // System.out.printf("%s - %s%n", fullname, name); 399 400 if ("".equals(desc.trim())) { 401 desc = NO_DESCRIPTION; 402 } else if (!endOfSentence.matcher(desc).find()) { 403 // Add period if there is no end-of-sentence delimiter 404 desc = desc + "."; 405 } 406 407 for (int i = 0; i < categories.length; i++) { 408 if (categories[i].matches(fullname, name)) { 409 categories[i].fields.put(fullname, desc); 410 break; 411 } 412 } 413 } 414 415 /** 416 * Get the default value of a field as a string. 417 * 418 * @param field the field to inspect 419 * @return the default value 420 */ 421 private String getDefaultString(String field) { 422 try { 423 int i = field.lastIndexOf('.'); 424 @SuppressWarnings("signature") // application invariant 425 @ClassGetName String classname = field.substring(0, i); 426 String fieldname = field.substring(i + 1); 427 Class<?> c = ReflectionPlume.classForName(classname); 428 Field f = c.getField(Configuration.PREFIX + fieldname); 429 if (!Modifier.isStatic(f.getModifiers())) { 430 throw new Error("Field " + Configuration.PREFIX + fieldname + " should be static"); 431 } 432 @SuppressWarnings("nullness") // the field is static 433 Object value = f.get(null); 434 return "The default value is `" + value + "'."; 435 } catch (Exception e) { 436 System.err.println(e); 437 return UNKNOWN_DEFAULT; 438 } 439 } 440 441 /** 442 * Output the parameter info in textinfo format. 443 * 444 * @param out where to write the data 445 */ 446 public void writeTexInfo(PrintWriter out) { 447 out.println("@c BEGIN AUTO-GENERATED CONFIG OPTIONS LISTING"); 448 out.println(); 449 450 out.println("@menu"); 451 for (int c = 0; c < categories.length; c++) { 452 out.println("* " + categories[c].description + "::"); 453 } 454 out.println("@end menu"); 455 out.println(); 456 457 String up = "List of configuration options"; 458 for (int c = 0; c < categories.length; c++) { 459 String node = categories[c].description; 460 String next = (c + 1 < categories.length) ? categories[c + 1].description : ""; 461 String prev = (c > 0) ? categories[c - 1].description : up; 462 out.println("@node " + node + ", " + next + ", " + prev + ", " + up); 463 out.println("@subsubsection " + node); 464 out.println(); 465 out.println(categories[c].blurb); 466 out.println(); 467 out.println("@table @option"); 468 out.println(); 469 470 for ( 471 @KeyFor("categories[c].fields") String field : CollectionsPlume.sortedKeySet(categories[c].fields)) { 472 String desc = categories[c].fields.get(field); 473 String defaultString = getDefaultString(field); 474 475 // Simpler format for debugging 476 if (false) { 477 String value = defaultString.replaceFirst(".*`", ""); 478 value = value.replaceFirst("'.*", ""); 479 out.printf("@item %s %s%n%n", value, field); 480 continue; 481 } 482 483 // @item [field] 484 // [desc] 485 out.println("@item " + field); 486 desc = HtmlToTexinfo.javadocHtmlToTexinfo(desc); 487 out.println(desc); 488 if (!desc.contains("The default value is")) { 489 out.println(defaultString); 490 } 491 out.println(); 492 } 493 out.println("@end table"); 494 out.println(); 495 } 496 497 out.println("@c END AUTO-GENERATED CONFIG OPTIONS LISTING"); 498 out.println(); 499 } 500 501 /** 502 * Output the parameter info in text format. 503 * 504 * @param out where to write the data 505 */ 506 public void writeText(PrintWriter out) { 507 for (int c = 0; c < categories.length; c++) { 508 out.println(categories[c].description); 509 out.println(); 510 511 for ( 512 @KeyFor("categories[c].fields") String field : CollectionsPlume.sortedKeySet(categories[c].fields)) { 513 String desc = categories[c].fields.get(field); 514 String defaultString = getDefaultString(field); 515 516 // [field] 517 // [desc] 518 out.println(" " + field); 519 out.println(" " + desc); 520 if (!desc.contains("The default value is")) { 521 out.println(" " + defaultString); 522 } 523 out.println(); 524 } 525 } 526 } 527 528 /////////////////////////////////////////////////////////////////////////// 529 /// Helper methods 530 /// 531 532 /** 533 * Fetch the comment string from a DocCommentTree node. 534 * 535 * @param node the DocCommentTree to process 536 * @return the entire body of the documentation comment as a string. If no comments are found, an 537 * empty string is returned (not null). 538 */ 539 public String getDocComment(DocCommentTree node) { 540 if (node == null) return ""; 541 StringBuilder sb = new StringBuilder(); 542 for (DocTree t : node.getFullBody()) { 543 sb.append(t.toString()); 544 } 545 return sb.toString(); 546 } 547 548 /** 549 * Returns true if the given element kind is a type, i.e., a class, enum, interface, or annotation 550 * type. 551 * 552 * @param element the element to test 553 * @return true, iff the given kind is a type kind 554 */ 555 public static boolean isTypeElement(Element element) { 556 ElementKind elementKind = element.getKind(); 557 return elementKind.isClass() || elementKind.isInterface(); 558 } 559 560 /////////////////////////////////////////////////////////////////////////// 561 /// Javadoc command-line options 562 /// 563 564 // The doclet cannot use the Options class itself because Javadoc specifies its own way of 565 // handling command-line arguments. 566 567 /** 568 * A command-line option to the Javadoc doclet; implements the {@link Doclet.Option} interface. 569 * 570 * <p>Is abstract because it does not provide an implementation of the {@code process} method. 571 */ 572 abstract static class DocletOption implements Doclet.Option { 573 /** The number of arguments this option will consume. */ 574 private int argumentCount; 575 576 /** The user-friendly description of the option. */ 577 private String description; 578 579 /** 580 * The list of names and aliases that may be used to identify the option. Each starts with "-" 581 * or "--". 582 */ 583 private List<String> names; 584 585 /** 586 * A user-friendly string description of the option's parameters, or the empty string if this 587 * option has no parameters. 588 */ 589 private String parameters; 590 591 /** 592 * Creates a new DocletOption. 593 * 594 * @param name the option's name, starting with "-" or "--" 595 * @param parameters a user-friendly string description of the option's parameters, or the empty 596 * string if this option has no parameters 597 * @param argumentCount the number of arguments this option will consume 598 * @param description the user-friendly description of the option 599 */ 600 DocletOption(String name, String parameters, int argumentCount, String description) { 601 this.argumentCount = argumentCount; 602 this.description = description; 603 this.names = List.of(name); 604 this.parameters = parameters; 605 } 606 607 /** 608 * Creates a new DocletOption with an aliased name 609 * 610 * @param name the option's name, starting with "-" or "--" 611 * @param alias the option's alias, starting with "-" or "--" 612 * @param parameters a user-friendly string description of the option's parameters, or the empty 613 * string if this option has no parameters 614 * @param argumentCount the number of arguments this option will consume 615 * @param description the user-friendly description of the option 616 */ 617 DocletOption( 618 String name, String alias, String parameters, int argumentCount, String description) { 619 this.argumentCount = argumentCount; 620 this.description = description; 621 this.names = List.of(name, alias); 622 this.parameters = parameters; 623 } 624 625 @Override 626 public int getArgumentCount() { 627 return argumentCount; 628 } 629 630 @Override 631 public String getDescription() { 632 return description; 633 } 634 635 @Override 636 public Doclet.Option.Kind getKind() { 637 return Doclet.Option.Kind.STANDARD; 638 } 639 640 @Override 641 public List<String> getNames() { 642 return names; 643 } 644 645 @Override 646 public String getParameters() { 647 return parameters; 648 } 649 } 650 651 /** The command-line options for OptionsDoclet. */ 652 @SuppressWarnings( 653 "nullness:method.invocation" // when methods such as printError() are called, the receiver 654 // (an OptionsDoclet) is initialized 655 ) 656 private final Set<DocletOption> docletOptions = 657 Set.of( 658 new DocletOption( 659 "--texinfo", "-texinfo", "file", 1, "write texinfo format output to this file") { 660 @Override 661 public boolean process(String option, List<String> arguments) { 662 if (outFilename != null) { 663 printError("must only specify one output option"); 664 return FAILED; 665 } 666 outFilename = arguments.get(0); 667 formatTexinfo = true; 668 return OK; 669 } 670 }, 671 new DocletOption("--text", "-text", "file", 1, "write text format output to this file") { 672 @Override 673 public boolean process(String option, List<String> arguments) { 674 if (outFilename != null) { 675 printError("must only specify one output option"); 676 return FAILED; 677 } 678 outFilename = arguments.get(0); 679 formatTexinfo = false; 680 return OK; 681 } 682 }); 683 684 /** 685 * Sets variables that can only be set after all command-line options have been processed. Isuses 686 * errors and halts if any command-line options are incompatible with one another. 687 */ 688 private void postprocessOptions() { 689 boolean hasError = false; 690 if (outFilename == null) { 691 printError("either --texinfo or --text must be specified"); 692 hasError = true; 693 } 694 695 if (hasError) { 696 System.exit(1); 697 } 698 } 699 700 /** 701 * Print error message via delegation to {@link #reporter}. 702 * 703 * @param msg message to print 704 */ 705 private void printError(String msg) { 706 reporter.print(Diagnostic.Kind.ERROR, msg); 707 } 708}