docs/manual/subtyping-checker.tex

\htmlhr
\chapterAndLabel{Subtyping Checker}{subtyping-checker}

The Subtyping Checker enforces only subtyping rules.  It operates over
annotations specified by a user on the command line.  Thus, users can
create a simple type-checker without writing any code beyond definitions of
the type qualifier annotations.

The Subtyping Checker can accommodate all of the type system enhancements that
can be declaratively specified (see Chapter~\ref{creating-a-checker}).
This includes type introduction rules via the
\refqualclass{framework/qual}{QualifierForLiterals} meta-annotation, and other features such as
type refinement (Section~\ref{type-refinement}) and
qualifier polymorphism (Section~\ref{method-qualifier-polymorphism}).

The Subtyping Checker is also useful to type system designers who wish to
experiment with a checker before writing code; the Subtyping Checker
demonstrates the functionality that a checker inherits from the Checker
Framework.

If you need typestate analysis, then you can extend a typestate checker.
For more details (including a definition of ``typestate''), see
Chapter~\ref{typestate-checker}.
See Section~\ref{faq-typestate} for a simpler alternative.

For type systems that require special checks (e.g., warning about
dereferences of possibly-null values), you will need to write code and
extend the framework as discussed in Chapter~\ref{creating-a-checker}.


\sectionAndLabel{Using the Subtyping Checker}{subtyping-using}

\begin{sloppypar}
The Subtyping Checker is used in the same way as other checkers (using the
\code{-processor org.checkerframework.common.subtyping.SubtypingChecker} option; see Chapter~\ref{using-a-checker}), except that it
requires an additional annotation processor argument via the standard
``\code{-A}'' switch. You must provide one or both of the two following
command-line arguments:
\end{sloppypar}

\begin{itemize}

\item
Provide the fully-qualified class name(s) of the annotation(s) in the custom
type system through the \code{-Aquals} option, using a comma-no-space-separated
notation:

\begin{alltt}
  javac -classpath \textit{/full/path/to/myProject/bin}:\textit{/full/path/to/myLibrary/bin} \ttbs
        -processor org.checkerframework.common.subtyping.SubtypingChecker \ttbs
        -Aquals=\textit{myPackage.qual.MyQual},\textit{myPackage.qual.OtherQual} MyFile.java ...
\end{alltt}

\item
Provide the fully-qualified paths to a set of directories that contain the
annotations in the custom type system through the \code{-AqualDirs} option,
using a colon-no-space-separated notation. For example,
if the Checker Framework is on the classpath rather than the processorpath:

\begin{alltt}
  javac -classpath \textit{/full/path/to/myProject/bin}:\textit{/full/path/to/myLibrary/bin} \ttbs
        -processor org.checkerframework.common.subtyping.SubtypingChecker \ttbs
        -AqualDirs=\textit{/full/path/to/myProject/bin}:\textit{/full/path/to/myLibrary/bin} MyFile.java
\end{alltt}

\end{itemize}

If the Checker Framework is on the processorpath, place the annotations on
the processorpath instead of on the classpath.


\subsectionAndLabel{Compiling your qualifiers and your project}{subtyping-compiling}

The annotations listed in \code{-Aquals} or \code{-AqualDirs} must be accessible to
the compiler during compilation.  Before you run the Subtyping Checker with
\code{javac}, they must be compiled and on the same path (the classpath or
processorpath) as the Checker Framework.  It
is not sufficient to supply their source files on the command line.


\subsectionAndLabel{Suppressing warnings from the Subtyping Checker}{subtyping-suppressing}

When suppressing a warning issued by the Subtyping Checker, as the
``checker name'' you may use the unqualified, uncapitalized name of any of
the annotations passed to \code{-Aquals}.  (See
Section~\ref{suppresswarnings-annotation-syntax} for details about the
\<@SuppressWarnings> syntax.)  As a matter of style, you should
choose one of the annotations as the ``checker name'' part of the
\code{@SuppressWarnings} string and use it consistently; this avoids
confusion and makes it easier to search for uses.


\sectionAndLabel{Subtyping Checker example\label{encrypted-example}}{subtyping-example}

Consider a hypothetical \code{Encrypted} type qualifier, which denotes that the
representation of an object (such as a \code{String}, \code{CharSequence}, or
\code{byte[]}) is encrypted. To use the Subtyping Checker for the \code{Encrypted}
type system, follow three steps.

\begin{enumerate}
\item
Define two annotations for the \code{Encrypted} and \code{PossiblyUnencrypted} qualifiers:

% alltt because it uses \textit
\begin{alltt}
package \textit{myPackage}.qual;

import org.checkerframework.framework.qual.DefaultFor;
import org.checkerframework.framework.qual.SubtypeOf;
import java.lang.annotation.ElementType;
import java.lang.annotation.Target;

/**
 * Denotes that the representation of an object is encrypted.
 */
@SubtypeOf(PossiblyUnencrypted.class)
@DefaultFor(\{TypeUseLocation.LOWER_BOUND\})
@Target(\{ElementType.TYPE_USE, ElementType.TYPE_PARAMETER\})
public @interface Encrypted \{\}
\end{alltt}

~

% alltt because it uses \textit
\begin{alltt}
package \textit{myPackage}.qual;

import org.checkerframework.framework.qual.DefaultQualifierInHierarchy;
import org.checkerframework.framework.qual.SubtypeOf;
import java.lang.annotation.ElementType;
import java.lang.annotation.Target;

/**
 * Denotes that the representation of an object might not be encrypted.
 */
@DefaultQualifierInHierarchy
@SubtypeOf(\{\})
@Target(\{ElementType.TYPE_USE, ElementType.TYPE_PARAMETER\})
public @interface PossiblyUnencrypted \{\}
\end{alltt}

Note that all custom annotations must have the
\<@Target(ElementType.TYPE\_USE)> meta-annotation.
See Section~\ref{creating-define-type-qualifiers}.

Don't forget to compile these classes:

\begin{Verbatim}
$ javac myPackage/qual/Encrypted.java myPackage/qual/PossiblyUnencrypted.java
\end{Verbatim}

The resulting \<.class> files should either be on the same path (the classpath or
processor path) as the Checker Framework.

\item
  Write \code{@Encrypted} annotations in your program (say, in file
  \code{YourProgram.java}):

\begin{alltt}
import \textit{myPackage}.qual.Encrypted;

...

public @Encrypted String encrypt(String text) \{
    // ...
\}

// Only send encrypted data!
public void sendOverInternet(@Encrypted String msg) \{
    // ...
\}

void sendText() \{
    // ...
    @Encrypted String ciphertext = encrypt(plaintext);
    sendOverInternet(ciphertext);
    // ...
\}

void sendPassword() \{
    String password = getUserPassword();
    sendOverInternet(password);
\}
\end{alltt}

You may also need to add \code{@SuppressWarnings} annotations to the
\code{encrypt} and \code{decrypt} methods.  Analyzing them is beyond the
capability of any realistic type system.

\item
  Invoke the compiler with the Subtyping Checker, specifying the
  \code{@Encrypted} annotation using the \code{-Aquals} option.
  You should add the \code{Encrypted} classfile to the processor classpath:

\begin{alltt}
  javac -processorpath \textit{myqualpath} -processor org.checkerframework.common.subtyping.SubtypingChecker \
        -Aquals=\textit{myPackage.qual.Encrypted},\textit{myPackage.qual.PossiblyUnencrypted} YourProgram.java

YourProgram.java:42: incompatible types.
found   : @myPackage.qual.PossiblyUnencrypted java.lang.String
required: @myPackage.qual.Encrypted java.lang.String
    sendOverInternet(password);
                     ^
\end{alltt}

\item
You can also provide the fully-qualified paths to a set of directories
that contain the qualifiers using the \code{-AqualDirs} option, and add
the directories to the boot classpath, for example:

\begin{alltt}
  javac -classpath \textit{/full/path/to/myProject/bin}:\textit{/full/path/to/myLibrary/bin} \ttbs
        -processor org.checkerframework.common.subtyping.SubtypingChecker \ttbs
        -AqualDirs=\textit{/full/path/to/myProject/bin}:\textit{/full/path/to/myLibrary/bin} YourProgram.java
\end{alltt}

\begin{sloppypar}
Note that in these two examples, the compiled class file of the
\<myPackage.qual.Encrypted> and \<myPackage.qual.PossiblyUnencrypted> annotations
must exist in either the \<myProject/bin> directory or the \<myLibrary/bin>
directory. The following placement of the class files will work with the above
commands:
\end{sloppypar}

\begin{alltt}
  .../myProject/bin/myPackage/qual/Encrypted.class
  .../myProject/bin/myPackage/qual/PossiblyUnencrypted.class
\end{alltt}

\end{enumerate}

Also, see the example project in the \<docs/examples/subtyping-extension> directory.


\sectionAndLabel{Type aliases and typedefs}{subtyping-type-alias}

A type alias or typedef is a type that shares the same representation as
another type but is conceptually distinct from it.  For example, some
strings in your program may be street addresses; others may be passwords;
and so on.  You wish to indicate, for each string, which one it is, and to
avoid mixing up the different types of strings.  Likewise, you could
distinguish integers that are offsets from those that are absolute values.

Creating a new type makes your code easier to understand by conveying the
intended use of each variable.  It also prevents errors that come from
using the wrong type or from mixing incompatible types in an operation.

If you want to create a type alias or typedef, you have multiple options:
a regular Java subtype,
the Units Checker (\chapterpageref{units-checker}),
the Fake Enum Checker (\chapterpageref{fenum-checker}), or
the Subtyping Checker.

A Java subtype is easy to create and does not require a tool such as the
Checker Framework; for instance, you would declare \<class Address extends
String>.  There are a number of limitations to this ``pseudo-typedef'',
however~\cite{Goetz2006:typedef}.
Primitive types and final types (including \<String>) cannot be extended.
Equality and identity tests can return incorrect results when a wrapper
object is used.  Existing return types in code would need to be changed,
which is easy with an annotation but disruptive to change the Java type.
Therefore, it is best to avoid the pseudo-typedef antipattern.

The Units Checker (\chapterpageref{units-checker}) is useful for the
particular case of units of measurement, such as kilometers verses miles.

The Fake Enum Checker (\chapterpageref{fenum-checker})
builds in a set of assumptions.  If those fit your
use case, then it's easiest to use the Fake Enum Checker (though you can
achieve them using the Subtyping Checker).  The Fake Enum Checker forbids
mixing of fenums of different types, or fenums and unannotated types.  For
instance, binary operations other than string concatenations are forbidden,
such as \<NORTH+1>, \<NORTH+MONDAY>, and \<NORTH==MONDAY>.  However,
\<NORTH+SOUTH> is permitted.

By default, the Subtyping Checker does not forbid any operations.

If you choose to use the Subtyping Checker, then you have an additional
design choice to make about the type system.  In the general case, your
type system will look something like Figure~\ref{fig-typedef-hierarchy}.

\begin{figure}
\includeimage{typedef}{3.5cm}
\caption{Type system for a type alias or typedef type system.
  The type system designer may choose to omit some of these types, but
  this is the general case.
  The type system designer's choice of defaults affects the interpretation
  of unannotated code, which affects the guarantees given for unannotated code.
  \label{fig-typedef-hierarchy}}
\end{figure}

References whose type is \<@MyType> are known to store only values from
your new type.  There is no such guarantee for \<@MyTypeUnknown> and
\<@NotMyType>, but those types mean different things.  An expression of type
\<@NotMyType> is guaranteed never to evaluate to a value of your new type.
An expression of type \<@MyTypeUnknown> may evaluate to any value ---
including values of your new type and values not of your new type.
(\<@MyTypeBottom> is the type of \<null> and is also used for dead code and
erroneous situations; it can be ignored for this
discussion.)

A key choice for the type system designer is which type is the default.
That is, if a programmer does not write \<@MyType> on a given type use,
should that type use be interpreted as \<@MyTypeUnknown> or as
\<@NotMyType>?

\begin{itemize}
\item
If unannotated types are interpreted as \<@NotMyType>, then the type system
enforces very strong separation between your new type and all other types.
Values of your type will never mix with values of other types.  If you
don't see \<@MyType> written explicitly on a type, you will know that
it does not contain values of your type.

\item
If unannotated types are interpreted as \<@MyTypeUnknown>, then
a generic, unannotated type may contain a value of your new type.
In this case, \<@NotMyType> does not need to exist, and \<@MyTypeBottom>
may or may not exist in your type system.
\end{itemize}

A downside of the stronger guarantee that comes from using \<@NotMyType> as
the default is the need to write additional annotations.
For example, if \<@NotMyType> is the default, this code does not typecheck:

\begin{Verbatim}
void method(Object o) { ... }
<U> void use(List<U> list) {
  method(list.get(0));
}
\end{Verbatim}

Because (implicit) upper bounds are interpreted as the top type (see
Section~\ref{generics-defaults}), this is interpreted as

\begin{Verbatim}
void method(@NotMyType Object o) { ... }
<@U extends @MyTypeUnknown Object> void use(List<U> list) {
  // type error: list.get(0) has type @MyTypeUnknown, method expects @NotMyType
  method(list.get(0));
}
\end{Verbatim}

To make the code type-check, it is necessary to write an explicit
annotation, either to restrict \<use>'s argument or to expand \<method>'s
parameter type.




% LocalWords:  TODO ImplicitFor Aquals sourcepath java NonNull AqualDirs
% LocalWords:  CharSequence classpath nullness quals SuppressWarnings classfile
% LocalWords:  uncapitalized processorpath Warski MyFile YourProgram qual
%%  LocalWords:  bootclasspath PossiblyUnencrypted myProject myLibrary msg
%%  LocalWords:  ElementType myqualpath sendOverInternet myPackage typedefs
%%  LocalWords:  SubtypeOf LiteralKind DefaultFor TypeUseLocation fenum
%%  LocalWords:  DefaultQualifierInHierarchy sendText sendPassword MyType
%  LocalWords:  getUserPassword CompassDirection MyTypeUnknown NotMyType
%  LocalWords:  MyTypeBottom typecheck ciphertext plaintext decrypt fenums
%%  LocalWords:  typedef antipattern typestate''