1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784
|
\htmlhr
\chapterAndLabel{Annotating libraries}{annotating-libraries}
When your code uses a library that is not currently being compiled,
the Checker Framework looks up the library's annotations in its class files.
Section~\ref{annotated-libraries-using} tells you how to find and use a
version of a library that contains type annotations.
If your code uses a library that does \emph{not} contain type annotations,
then the type-checker has no way to know the library's behavior.
The type-checker
makes conservative assumptions about unannotated bytecode.
% : it assumes that every method parameter has the bottom type annotation
% and that every method return type has the top type annotation
(See
Section~\ref{defaults-classfile} for details, an example, and how to
override this conservative behavior.)
These conservative library
annotations invariably lead to checker warnings.
This chapter describes how to eliminate
the warnings by adding annotations to the library.
(Alternately, you can instead
suppress all warnings related to an unannotated library, or to part of your
codebase, by use of the
\code{-AskipUses} or \code{-AonlyUses} command-line option; see
Sections~\ref{askipuses}--\ref{askipdefs}.)
You can write annotations for a library, and make them known to a checker, in two ways.
\begin{enumerate}
\item
Write annotations in a copy of the library's source code (for instance,
in a fork of the library's GitHub project). In addition to writing
annotations, adjust the build system to run pluggable-type-checking when
compiling (see \chapterpageref{external-tools}).
Then, when doing pluggable type-checking,
put the annotated library's \<.jar> file on the classpath, as explained in
Section~\ref{annotated-libraries-using}.
%% You only need to do this if for some reason you don't trust the
%% artifacts on Maven Central; but don't cater to that level of paranoia
%% by mentioning it.
% When \emph{running} your code, you can use either version of the library: the
% one you created or the original distributed version.
%% There is no point to advertising this deprecated workflow.
% You can insert annotations in the compiled \code{.class} files of the
% library. You would express the annotations textually, typically as an
% annotation index file, and
% then insert them in the library by using the Annotation File Utilities
% (\myurl{https://checkerframework.org/annotation-file-utilities/}).
% See the Annotation File Utilities documentation for full details.
With this compilation approach, the syntax of the library annotations is
validated ahead of time. Thus, this compilation approach is less
error-prone, and the type-checker runs faster. You get
correctness guarantees about the library in addition to your code.
For instructions, see Section~\ref{annotating-libraries-create}.
\item
Write annotations in a ``stub file'', if you do not have access to the
source code.
%% Leave out this complication.
% This approach is possible with annotated source code.
Then, when doing pluggable type-checking,
supply the ``stub file'' textually to the Checker Framework.
This approach does not require you to compile the library source
code.
A stub file is applicable to multiple versions of a library, so
the stub file does not need to be updated when a new version of the
library is released, unless the API has changed (such as defining a new
method).
For instructions, see Section~\ref{stub}.
\end{enumerate}
If you annotate a new library (either in its source code or in a stub
file), please inform the Checker Framework
developers so that your annotated library can be distributed with the
Checker Framework.
Sharing your annotations is useful even if the library is only partially
annotated.
However, as noted in Sections~\ref{get-started-with-legacy-code} and~\ref{library-tips-fully-annotate}, you
should annotate an entire class at a time.
You may find type inference tools (\chapterpageref{type-inference-to-annotate}) helpful
when getting started, but you should always examine their results.
%% This text does not feel so relevant.
% You can determine the correct annotations for a library either
% automatically by running an inference tool, or manually by reading the
% documentation. Presently, automated type inference tools are available for the
% Nullness (Section~\ref{nullness-inference}) type system.
\sectionAndLabel{Tips for annotating a library}{library-tips}
Section~\ref{tips-about-writing-annotations} gives general tips for writing
annotations. This section gives tips that are specific to annotating a
third-party library.
\subsectionAndLabel{Don't change the code}{library-tips-dont-change-the-code}
If you annotate a library that you maintain, you can refactor it to improve
its design.
When you annotate a library that you do not maintain, you should only add
annotations and, when necessary, documentation of those annotations. You
can place the documentation in a Java comment (\<//> or \</*...*/>) or in a
\refqualclass{framework/qual}{CFComment} annotation.
Do not change the library's code, which will change its behavior and make
the annotated version inconsistent with the unannotated version.
(Sometimes it is acceptable to make a refactoring, such as extracting an
expression into a new local variable in order to annotate its type or
suppress a warning. Perform refactoring only when you cannot use
\<@AssumeAssertion>.)
% (The only time it is acceptable to comment out existing code in the library
% is if the regular Java compiler cannot compile the code; but this should be
% extremely rare.)
Do not change publicly-visible documentation, such as Javadoc comments.
That also makes the annotated version inconsistent with the unannotated
version.
Do not change formatting and whitespace.
All of these changes increase the difference between upstream (the original
version) and your annotated version. This makes it harder for others to
understand what you have done, and they make it harder to pull changes from
upstream into the annotated library.
\subsectionAndLabel{Library annotations should reflect the specification, not the implementation}{library-tips-specification}
Publicly-visible annotations (including those on public method formal
parameters and return types) should be based on the
documentation, typically the method's Javadoc.
In other words, your annotations should re-state facts that are in the Javadoc
documentation.
Do not add requirements or guarantees beyond what the library author has
already committed to. If a project's Javadoc says nothing about nullness,
then you should not assume that the specification forbids null, nor that it
permits it.
(If the project's Javadoc explicitly mentions null everywhere it is permitted,
then you can assume it is forbidden elsewhere, where the author omitted those
statements.)
If a fact is not mentioned in the documentation, then it is usually an
implementation detail. Clients should not depend on implementation
details, which are prone to change without notice.
(In some cases, you can infer some facts from the
implementation, such as that null is permitted for a method's parameter or
return type if the implementation explicitly passes null to the method or
the method implementation returns null.)
If there is a fact that you think should be in the library's documentation
but was unintentionally omitted by its authors, then please submit a bug
report asking them to update the documentation to reflect this fact. After
they do, you can also express the fact as an annotation.
% If you wish to depend on your assumption that the behavior will never
% change, then you can create a local stub file as a workaround while you
% wait for the library documentation to be updated.
\subsectionAndLabel{Report bugs upstream}{library-tips-report-bugs}
While annotating the library, you may discover bugs or missing/wrong
documentation. If you have a documentation improvement or a bug fix, then
open a pull request against the upstream version of the library. This will
benefit all users of the library. And, once the documentation is updated,
you will be able to add annotations that are consistent with the
documentation.
\subsectionAndLabel{Fully annotate the library, or indicate which parts you did not}{library-tips-fully-annotate}
If you do not annotate all the files in the library, then use
\refqualclass{framework/qual}{AnnotatedFor} to indicate what files you have
annotated.
Whenever you annotate any part of a file, fully annotate the file! That
is, write annotations for all the methods and fields, based on their
documentation. If you don't annotate the whole file, then users may be
surprised that calls to some methods type-check as expected whereas other
methods do not (because they have not been annotated).
\subsectionAndLabel{Verify your annotations}{library-tips-verify}
Ideally, after you annotate a file, you should type-check the file to verify
the correctness and completeness of your annotations.
An alternative is to
only annotate method signatures. The alternative is quicker but more
error-prone, and there is no difference from the point of view of clients,
who can only see annotations on public methods and fields. When you
compile the library, the type-checker will probably issue warnings, but if
you supply \<-Awarns>, you don't have to suppress those warnings and the
compiler will still produce \<.class> files.
\sectionAndLabel{Creating an annotated library}{annotating-libraries-create}
This section describes how to create an annotated library.
\begin{enumerate}
\item See the
\ahref{https://search.maven.org/search?q=org.checkerframework.annotatedlib}{the
\<org.checkerframework.annotatedlib> group in the Central Repository}
to find out whether an annotated version of the library already exists.
%% This adds clutter to the source code, so omit the step from these instructions.
% \item Optionally, run a script that adds
% \<\refqualclass{framework/qual}{AnnotatedFor}(\ttlcb\ttrcb)>
% to each class. [[TODO: say where to find this script.]]
% This step has no semantic effect. It only saves you the trouble of
% typing those 17 characters later.
\begin{itemize}
\item
If it exists, but you want to add annotations for a different checker:
Clone its repository from \url{https://github.com/typetools/}, tweak
its buildfile to run an additional checker.
\item
If it does not already exist:
Fork the project. (First, verify that its license permits forking.)
Add a line in its main README to indicate that this is an annotated
version of the library. That line should also indicate how to obtain
the corresponding upstream version (typically a git tag
\ahref{https://rawgit.com/typetools/checker-framework/master/docs/developer/developer-manual.html#annotated-library-version-numbers}{corresponding
to a release}), so that others can see exactly what edits you have
made.
Adjust the library's
build process, such as an Ant, Gradle, or Maven buildfile.
Every time the build system runs the compiler, it should:
\begin{itemize}
\item
pass the \<-AuseDefaultsForUncheckedCode=source,bytecode>
command-line option and
\item
run every pluggable type-checker for which any
annotations exist, using \<-processor
\emph{TypeSystem1},\emph{TypeSystem2},\emph{TypeSystem3}>
\end{itemize}
You are not adding new build targets, but modifying existing targets.
The reason to run every type-checker is to verify
the annotations you wrote, and to use appropriate defaults for all
unannotated type uses.
\end{itemize}
\item Annotate some files.
% You can determine which files need to be annotated by using the
% \<-AprintUnannotatedMethods> command-line argument while type-checking a
% client of the library.
% This is a strong recomendation, but not a requirement. @AnnotatedFor
% can be written on a method as well.
When you annotate a file, annotate the whole thing, not just a few of its
methods. Once the file is fully annotated, add an
\<\refqualclass{framework/qual}{AnnotatedFor}(\ttlcb"\emph{checkername}"\ttrcb)>
annotation to its class(es), or augment an existing \<@AnnotatedFor>
annotation.
\item
Build the library.
Because of the changes that you made in step 1, this will run pluggable
type-checkers. If there are any compiler warnings, fix them and re-compile.
Now you have a \<.jar> file that you can use while type-checking and at
run time.
\item
Tell other people about your work so that they can benefit from it.
\begin{itemize}
\item
Please inform the Checker Framework developers
about your new annotated library by opening a pull request or an issue.
This will let us add your annotations to a repository in
\url{https://github.com/typetools/} and upload a compiled artifact to
the Maven Central Repository.
\item
Encourage the library's maintainers to accept your annotations into its
main version control repository. This will make the annotations easier
to maintain, the library will obtain the correctness guarantees of
pluggable type-checking, and there will be no need for the Checker
Framework to include an annotated version of the library.
If the library maintainers do not accept the annotations, then
periodically, such as when a new version of the library is released,
pull changes from upstream (the library's main version control system)
into your fork, add annotations to any newly-added methods in classes
that are annotated with \<@AnnotatedFor>, rebuild to create an updated
\<.jar> file, and inform the Checker Framework developers by opening an
issue or issuing a pull request.
\end{itemize}
\end{enumerate}
\sectionAndLabel{Creating an annotated JDK}{annotating-jdk}
This section tells how to create an annotated JDK for a new type system.
Section~\ref{reporting-bugs-annotated-libraries} tells how to improve
annotations for the JDK for an existing type system.
When you create a new checker, you need to also supply annotations for
parts of the JDK, either as stub files or as source code that will be
compiled and its annotations inserted into the JDK\@. This
section describes the latter approach.
It assumes that you have already followed the instructions for building the
Checker Framework from source (Section~\ref{build-source}).
Because there are two versions of the annotated JDK, you need to write your
annotations in two places.
For \textbf{JDK 11}, edit files in repository \url{https://github.com/typetools/jdk}.
That is all you need to do.
The rest of this section gives instructions for \textbf{JDK 8}.
If you are adding annotations to an existing annotated JDK, then you only
need to follow the last two steps.
\begin{enumerate}
\item
Get Java 8 source code (must be version 8)
\begin{enumerate}
\item Download JDK8 from Oracle
\item Open the downloaded tar (\<tar -xvzf>)
\item Unzip the contained \<src.zip> (resulting in folders: \<com/>, \<java/>, \<javax/>, \<launcher/>, \<org/>)
\end{enumerate}
\item
Set up the Checker Framework (replace \textit{mychecker} with the name of your checker)
\begin{enumerate}
\item \<mkdir \$CHECKERFRAMEWORK/checker/jdk/\textit{mychecker}/> \\
\<cd \$CHECKERFRAMEWORK/checker/jdk/\textit{mychecker}/> \\
\code{echo "include ../Makefile.jdk" > Makefile}
\item Add \textit{mychecker} to
\<\$CHECKERFRAMEWORK/checker/jdk/MakeFile> in the definition of
\<CHECKER\_DIRS> and in the definition of \<ANNOTATED\_CLASSES> (don't forget
to add a closing parenthesis at the end of the definition of \<ANNOTATED\_CLASSES>!).
\end{enumerate}
\item
For each file you want to annotate, copy the JDK version into the
directory
\<\$CHECKERFRAMEWORK/checker/jdk/\textit{mychecker}/src/>, using
the same directory structure as the JDK\@.
Whenever you add a file, fully annotate it, as described in
Section~\ref{library-tips}.
If you are only annotating fields and method signatures (but not
ensuring that method bodies type-check), then you don't need to suppress
warnings, because the JDK is built using the \<-Awarns> command-line
option.
\item
Build the annotated JDK\@. There are two ways:
\begin{itemize}
\item
Pass a flag.
Run \<./gradlew buildJdk -PuseLocalJdk>
% Is any more advice needed here, such as supplying -PuseLocalJdk to
% other commands?
\item
Make a setting in the buildfile.
Set \<jdkShaHash> to \<`local'> in \<checker/build.gradle>, then
run \<./gradlew buildJdk>
\end{itemize}
(First, be sure you have followed the instructions for building the Checker
Framework from source (Section~\ref{build-source})
including running \<./gradlew cloneAndBuildDependencies>.)
You may receive a compilation error because your files use a part of the
JDK that is not in the annotated JDK\@. If the missing part is relatively
small, please add it. If the missing part is large, then you can make
small changes to the JDK source code, such as commenting out a method body.
(Use \</*> and \<*/> on their own lines, so that the diffs are minimal.)
To upload a compiled version of the annotated JDK, for use by other people,
see \url{https://github.com/typetools/annotated-libraries}.
\end{enumerate}
\sectionAndLabel{Compiling partially-annotated libraries}{compiling-libraries}
If you completely annotate a library, then you can compile it using a
pluggable type-checker, and include the resulting \<.jar> file on your
classpath. You get a guarantee that the library contains no errors.
The rest of this section tells you how to compile a library if you
\emph{partially} annotate it: that is, you write annotations for some of its
classes but not others.
(There is another type of partial annotation, which is when you annotate
method signatures but do not type-check the bodies.
See Section~\ref{library-tips}.)
There are two concerns:
\begin{itemize}
\item
Ignoring type-checking errors in unannotated parts of the library.
Use the \<-AskipDefs> or \<-AonlyDefs> command-line arguments; see
Section~\ref{askipdefs}.
\item
Putting conservative annotations in unannotated parts of the library.
The checker needs to use normal defaulting rules
(Section~\ref{climb-to-top}) for code you have annotated and conservative
defaulting rules (Section~\ref{defaults-classfile}) for code you have not
yet annotated. This section describes how to do this. You use
\<@AnnotatedFor> to indicate which classes you have annotated.
\end{itemize}
\subsectionAndLabel{The \<-AuseDefaultsForUncheckedCode=source,bytecode> command-line argument}{AuseDefaultsForUncheckedCodesource}
\begin{sloppypar}
When compiling a library that is not fully annotated, use command-line
argument \<-AuseDefaultsForUncheckedCode=source,bytecode>. This causes
the checker to behave normally for classes with a relevant \<@AnnotatedFor>
annotation. For classes without \<@AnnotatedFor>, the checker uses
unchecked code defaults
(see Section~\ref{defaults-classfile}) for any type use with no explicit
user-written annotation, and the checker issues no warnings.
\end{sloppypar}
The \refqualclass{framework/qual}{AnnotatedFor} annotation, written on a
class, indicates that the class has been annotated for certain type
systems. For example, \<@AnnotatedFor(\ttlcb"nullness", "regex"\ttrcb)> means that
the programmer has written annotations for the Nullness and Regular
Expression type systems. If one of those two type-checkers is run,
the \<-AuseDefaultsForUncheckedCode=source,bytecode> command-line argument
has no effect and this class is treated normally:
unannotated types are defaulted using normal source-code
defaults and type-checking warnings are issued.
\refqualclass{framework/qual}{AnnotatedFor}'s arguments are any string that
may be passed to the \<-processor> command-line argument: the
fully-qualified class name for the checker, or a shorthand for built-in
checkers (see Section~\ref{shorthand-for-checkers}).
Writing \<@AnnotatedFor> on a class doesn't necessarily mean that you wrote
any annotations, but that the user examined the source code and verified
that all appropriate annotations are present.
\begin{sloppypar}
Whenever you compile a class using the Checker Framework, including when
using the \<-AuseDefaultsForUncheckedCode=source,bytecode> command-line
argument, the resulting \<.class> files are fully-annotated; each type use
in the \<.class> file has an explicit type qualifier for any checker that
is run.
\end{sloppypar}
\sectionAndLabel{Using stub classes}{stub}
A stub file contains ``stub classes'' that contain annotated signatures,
but no method bodies. A
checker uses the annotated signatures at compile time, instead of or in
addition to annotations that appear in the library.
Section~\ref{annotating-jdk} explains how you should choose between
creating stub classes or creating an annotated library.
Section~\ref{stub-creating} describes how to create stub classes.
Section~\ref{stub-using} describes how to use stub classes.
These sections illustrate stub classes via the example of creating a \refqualclass{checker/interning/qual}{Interned}-annotated
version of \code{java.lang.String}. You don't need to repeat these steps
to handle \code{java.lang.String} for the Interning Checker,
but you might do something similar for a different class and/or checker.
\subsectionAndLabel{Using a stub file}{stub-using}
The \code{-Astubs} argument causes the Checker Framework to read
annotations from annotated stub classes in preference to the unannotated
original library classes. For example:
\begin{myxsmall}
\begin{Verbatim}
javac -processor org.checkerframework.checker.interning.InterningChecker -Astubs=String.astub:stubs MyFile.java MyOtherFile.java ...
\end{Verbatim}
\end{myxsmall}
Each stub path entry is a stub file (ending with \<.astub>), directory, or
\<.jar> file; specifying a directory or \<.jar> file is
equivalent to specifying every file in it whose name ends with
\code{.astub}. The stub path entries are delimited by
\<File.pathSeparator> (`\<:>' for Linux and Mac, `\<;>' for Windows).
A checker automatically reads some of its own stub files, even without a
\<-Astubs> command-line argument; see
Section~\ref{creating-a-checker-annotated-jdk}.
\subsectionAndLabel{Multiple specifications for a method}{stub-multiple-specifications}
A file being compiled takes precedence over a stub file. If file \<A.java>
is being compiled, then any stub for class \<A> is ignored.
A stub file takes precedence over bytecode, for elements in the stub file.
If a stub file does not mention a method or field, its annotations are
taken from bytecode.
An un-annotated type variable in a stub file is used instead of
annotations on a type variable in bytecode.
This feature allows stub files to change the effective annotations in
all possible situations.
%% Uncomment when https://tinyurl.com/cfissue/2759 is fixed.
% Use the \<-AstubWarnIfOverwritesBytecode> command-line option to get a
% warning whenever a stub file overwrites bytecode annotations.
Use the \<-AstubWarnIfRedundantWithBytecode> command-line option to get
a warning whenever a stub file specification is redundant with
bytecode annotations.
If a method appears in more than one stub file (or twice in the same
stub file), then the annotations are merged. If any of the
methods have different annotations from the same hierarchy on the same type,
then the annotation from the last declaration is used.
% True for JDK 11 now; will soon be true for all JDK versions.
The annotated JDK is read as a stub file.
\subsectionAndLabel{Stub file format}{stub-format}
Every Java file is a valid stub file. However, you can omit information
that is not relevant to pluggable type-checking; this makes the stub file
smaller and easier for people to read and write.
Also note that the stub file's extension must be \<.astub>, not \<.java>.
As an illustration, a stub file for the Interning type system
(Chapter~\ref{interning-checker}) could be:
\begin{Verbatim}
import org.checkerframework.checker.interning.qual.Interned;
package java.lang;
@Interned class Class<T> {}
class String {
@Interned String intern();
}
\end{Verbatim}
The stub file format is allowed to differ from Java source code in the
following ways:
\begin{description}
\item{\textbf{Method bodies:}}
The stub class does not require method bodies for classes; any method
body may be replaced by a semicolon (\code{;}), as in an interface or
abstract method declaration.
\item{\textbf{Method declarations:}}
You only have to specify the methods that you need to annotate.
Any method declaration may be omitted, in which case the checker reads
its annotations from library's \<.class> files. (If you are using a stub class, then
typically the library is unannotated.)
\item{\textbf{Declaration specifiers:}}
Declaration specifiers (e.g., \<public>, \<final>, \<volatile>)
may be omitted.
\item{\textbf{Return types:}}
The return type of a method does not need to match the real method.
In particular, it is valid to use \<java.lang.Object> for every method.
This simplifies the creation of stub files.
\item{\textbf{Import statements:}}
Imports may appear at the beginning of the file or after any package declaration.
The only required import statements are the ones to import type
annotations. Import statements for types are optional.
\item{\textbf{Multiple classes and packages:}}
The stub file format permits having multiple classes and packages.
The packages are separated by a package statement:
\<package my.package;>. Each package declaration may occur only once; in
other words, all classes from a package must appear together.
\end{description}
\subsectionAndLabel{Creating a stub file}{stub-creating}
Stub files are generally stored together with the checker implementation,
in the same directory as the checker's \<.java> source code.
\subsubsectionAndLabel{If you have access to the Java source code}{stub-creating-with-source}
Every Java file is a stub file. If you have access to the Java file,
rename file \<A.java> to \<A.astub>. You can add
annotations to the signatures, leaving the method bodies unchanged.
The stub file parser silently ignores any annotations that it cannot
resolve to a type, so don't forget the \<import> statement.
Optionally (but highly recommended!), run the type-checker to verify that
your annotations are correct. When you run the type-checker on your
annotations, there should not be any stub file that also contains
annotations for the class. In particular, if you are type-checking the JDK
itself, then you should use the \<-Aignorejdkastub> command-line option.
This approach retains the original
documentation and source code, making it easier for a programmer to
double-check the annotations. It also enables creation of diffs, easing
the process of upgrading when a library adds new methods. And, the
annotations are in a format that the library maintainers can even
incorporate.
The downside of this approach is that the stub files are larger. This can
slow down the Checker Framework, because it parses the stub files each time
it runs.
% Furthermore, a programmer must search the stub file
% for a given method rather than just skimming a few pages of method signatures.
\subsubsectionAndLabel{If you do not have access to the Java source code}{stub-creating-without-source}
If you do not have access to the library source code, then you can create a
stub file from the class file (Section~\ref{stub-creating}),
and then annotate it. The rest of this section describes this approach.
\begin{enumerate}
\item
Create a stub file by running the stub class generator. (\<checker.jar> must be on your classpath.)
\begin{Verbatim}
cd nullness-stub
java -cp $CHECKERFRAMEWORK/checker/dist/checker.jar org.checkerframework.framework.stub.StubGenerator java.lang.String > String.astub
\end{Verbatim}
Supply it with the fully-qualified name of the class for which you wish to
generate a stub class. The stub class generator prints the
stub class to standard out, so you may wish to redirect its output to a
file.
\item
Add import statements for the annotations. So you would need to
add the following import statement at the beginning of the file:
\begin{Verbatim}
import org.checkerframework.checker.interning.qual.*;
\end{Verbatim}
\noindent
The stub file parser silently ignores any annotations that it cannot
resolve to a type, so don't forget the import statement.
Use the \<-AstubWarnIfNotFound> command-line option to see warnings
if an entry could not be found.
\item
Add annotations to the stub class. For example, you might annotate
the \sunjavadoc{java.base/java/lang/String.html\#intern()}{String.intern()} method as follows:
\begin{Verbatim}
@Interned String intern();
\end{Verbatim}
You may also remove irrelevant parts of the stub file; see
Section~\ref{stub-format}.
\end{enumerate}
\subsectionAndLabel{Troubleshooting stub libraries}{stub-troubleshooting}
\subsubsectionAndLabel{Type-checking does not yield the expected results}{stub-troubleshooting-type-checking-results}
By default, the stub parser silently ignores
annotations on unknown classes and methods.
The stub parser also silently ignores unknown annotations, so don't forget to
\<import> any annotations.
Some command-line options make the stub parser issue more warnings:
\begin{description}
\item[\<-AstubWarnIfNotFound>]
Warn whenever some element of a stub file cannot be found.
The \<@NoStubParserWarning> annotation on a package or type in a stub file
overrides the \<-AstubWarnIfNotFound> command-line option, and no warning
will be issued.
\item[\<-AstubWarnIfNotFoundIgnoresClasses>]
Modifies the behavior of \<-AstubWarnIfNotFound>
to report only missing methods/fields, but ignore missing classes, even if
other classes from the same package are present.
Useful if a package spans more than one jar.
%% Uncomment when https://tinyurl.com/cfissue/2759 is fixed.
% \item[\<-AstubWarnIfOverwritesBytecode>]
% Warn whenever some element of a
% stub file overwrites annotations contained in bytecode.
\end{description}
Finally,
use command-line option {\bf\<-AstubDebug>} to output debugging messages while
parsing stub files, including about unknown classes, methods, and
annotations. This overrides the \<@NoStubParserWarning> annotation.
\subsubsectionAndLabel{Problems parsing stub libraries}{stub-troubleshooting-parsing}
When using command-line option \<-AstubWarnIfNotFound>,
an error is issued if a stub file has a typo or the API method does not
exist.
Fix an error of the form
\begin{Verbatim}
StubParser: Method isLLowerCase(char) not found in type java.lang.Character
\end{Verbatim}
\noindent
by removing the extra ``L'' in the method name.
Fix an error of the form
\begin{Verbatim}
StubParser: Method enableForegroundNdefPush(Activity,NdefPushCallback)
not found in type android.nfc.NfcAdapter
\end{Verbatim}
\noindent
by removing the method \<enableForgroundNdefPush(...)> from
the stub file, because it is not defined in class \<android.nfc.NfcAdapter>
in the version of the library you are using.
\sectionAndLabel{Troubleshooting/debugging annotated libraries}{libraries-troubleshooting}
Sometimes, it may seem that a checker is treating a library as unannotated
even though the library has annotations. The compiler has two flags that
may help you in determining whether library files are read, and if they are
read whether the library's annotations are parsed.
\begin{description}
\item \<-verbose>
Outputs info about compile phases --- when the compiler
reads/parses/attributes/writes any file. Also outputs the classpath and
sourcepath paths.
\item \<-XDTA:parser> (which is equivalent to \<-XDTA:reader> plus \<-XDTA:writer>)
Sets the internal \<debugJSR308> flag, which outputs information about
reading and writing.
\end{description}
% LocalWords: plugin utils util dist RuntimeException NonNull TODO AFU enum
% LocalWords: sourcepath Nullness javac classpath src quals pathSeparator JDKs
% LocalWords: jdk Astubs skipUses astub AskipUses toArray JDK6 xvzf javax
% LocalWords: CollectionToArrayHeuristics BaseTypeVisitor Xbootclasspath
% LocalWords: Interning's UsesObjectEquals ApermitMissingJdk AonlyUses java pre
% LocalWords: Aignorejdkastub AstubWarnIfNotFound AstubDebug dont local'
% LocalWords: enableForgroundNdefPush XDTA debugJSR308 BCEL getopt jdk8
%% LocalWords: NoStubParserWarning CHECKERFRAMEWORK AnnotatedFor regex
%% LocalWords: AuseConservativeDefaultsForUnannotatedCode buildfile qual
%% LocalWords: AprintUnannotatedMethods checkername AskipDefs bcel mkdir
%% LocalWords: AuseSafeDefaultsForUnannotatedSourceCode TypeSystem1 cd
%% LocalWords: TypeSystem2 TypeSystem3 AuseDefaultsForUncheckedCode ln
% LocalWords: mychecker DIRS README TypeSystem un debugJSR org boolean
% LocalWords: AstubWarnIfOverwritesBytecode Awarns AssumeAssertion
%% LocalWords: Makefile buildJdk PuseLocalJdk jdkShaHash AonlyDefs
%% LocalWords: AuseDefaultsForUncheckedCodesource
%% LocalWords: AstubWarnIfNotFoundIgnoresClasses
|