File: annotating-libraries.tex

package info (click to toggle)
checker-framework-java 3.2.0%2Bds-3
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid, trixie
  • size: 23,104 kB
  • sloc: java: 145,916; xml: 839; sh: 518; makefile: 404; perl: 26
file content (784 lines) | stat: -rw-r--r-- 33,402 bytes parent folder | download | duplicates (2)
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