\htmlhr
\chapterAndLabel{Fake Enum Checker for fake enumerations}{fenum-checker}

The Fake Enum Checker, or Fenum Checker, enables you to define a type alias
or typedef, in which two different sets of values have the same
representation (the same Java type) but are not allowed to be used
interchangeably.  It is also possible to create a typedef using the
Subtyping Checker (\chapterpageref{subtyping-checker}), and that approach
is sometimes more appropriate.

One common use for the Fake Enum Checker is the
\emph{fake enumeration pattern} (Section~\ref{fenum-pattern}).  For
example, consider this code adapted from Android's
\href{https://developer.android.com/reference/android/support/annotation/IntDef}{\code{IntDef}}
documentation:

\begin{Verbatim}
@NavigationMode int NAVIGATION_MODE_STANDARD = 0;
@NavigationMode int NAVIGATION_MODE_LIST = 1;
@NavigationMode int NAVIGATION_MODE_TABS = 2;

@NavigationMode int getNavigationMode();

void setNavigationMode(@NavigationMode int mode);
\end{Verbatim}

The Fake Enum Checker can issue a compile-time warning if the programmer
ever tries to call \<setNavigationMode> with an \<int> that is not a
\<@NavigationMode int>.

The Fake Enum Checker gives the same safety guarantees as a true enumeration
type or typedef, but retaining backward-compatibility with interfaces that
use existing Java types.  You can apply fenum annotations to any Java type,
including all primitive types and also reference types.  Thus, you could
use it (for example) to represent floating-point values between 0 and 1, or
\<String>s with some particular characteristic.
(Note that the Fake Enum Checker does not let you create a shorter alias
for a long type name, as a real typedef would if Java supported it.)

As explained in Section~\ref{fenum-annotations}, you can either define your
own fenum annotations, such as \<@NavigationMode> above, or you can use the
\refqualclass{checker/fenum/qual}{Fenum} type qualifier with a string argument.
Figure~\ref{fig-fenum-hierarchy} shows part of the type hierarchy for the
Fenum type system.

\begin{figure}
\includeimage{fenum}{3.2cm}
\caption{Partial type hierarchy for the Fenum type system.
There are two forms of fake enumeration annotations --- above, illustrated
by \code{@Fenum("A")} and \code{@FenumC}.
See Section~\ref{fenum-annotations} for descriptions of how to
introduce both types of fenums. The type qualifiers in gray
(\code{@FenumTop}, \code{@FenumUnqualified}, and \code{@FenumBottom})
should never be written in
source code; they are used internally by the type system.
\<@FenumUnqualified> is the default qualifier for unannotated types, except
for upper bounds which default to \<@FenumTop>.
}
\label{fig-fenum-hierarchy}
\end{figure}

\sectionAndLabel{Fake enum annotations}{fenum-annotations}

The Fake Enum Checker supports two ways to introduce a new fake enum (fenum):

\begin{enumerate}
\item Introduce your own specialized fenum annotation with code like this in
file \code{\emph{MyFenum}.java}:

\begin{alltt}
package \textit{myPackage}.qual;

import java.lang.annotation.Documented;
import java.lang.annotation.ElementType;
import java.lang.annotation.Retention;
import java.lang.annotation.RetentionPolicy;
import java.lang.annotation.Target;
import org.checkerframework.checker.fenum.qual.FenumTop;
import org.checkerframework.framework.qual.SubtypeOf;

@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target(\ttlcb{}ElementType.TYPE_USE, ElementType.TYPE_PARAMETER\ttrcb)
@SubtypeOf(FenumTop.class)
public @interface \textit{MyFenum} \ttlcb\ttrcb
\end{alltt}

You only need to adapt the italicized package, annotation, and file names in the example.

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

\item Use the provided \refqualclass{checker/fenum/qual}{Fenum} annotation, which takes a
\code{String} argument to distinguish different fenums or type aliases.
For example, \code{@Fenum("A")} and \code{@Fenum("B")} are two distinct
type qualifiers.
\end{enumerate}


The first approach allows you to define a short, meaningful name suitable for
your project, whereas the second approach allows quick prototyping.


\sectionAndLabel{What the Fenum Checker checks}{fenum-checks}

The Fenum Checker ensures that unrelated types are not mixed.
All types with a particular fenum annotation, or \code{@Fenum(...)} with a
particular \code{String} argument, are
disjoint from all unannotated types and from all types with a different fenum
annotation or \code{String} argument.

The checker ensures that
only compatible fenum types are used in comparisons and arithmetic operations
(if applicable to the annotated type).

It is the programmer's responsibility to ensure that fields with a fenum type
are properly initialized before use.  Otherwise, one might observe a \code{null}
reference or zero value in the field of a fenum type.  (The Nullness Checker
(\chapterpageref{nullness-checker}) can prevent failure to initialize a
reference variable.)


\sectionAndLabel{Running the Fenum Checker}{fenum-running}

The Fenum Checker can be invoked by running the following commands.

\begin{itemize}
  \item
If you define your own annotation(s), provide the name(s) of the annotation(s)
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.checker.fenum.FenumChecker \ttbs
        -Aquals=\textit{myPackage.qual.MyFenum} MyFile.java ...
\end{alltt}

The annotations listed in \code{-Aquals} must be accessible to
the compiler during compilation.  Before you run the Fenum 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.

You can also provide the fully-qualified paths to a set of directories
that contain the annotations 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.checker.fenum.FenumChecker \ttbs
        -AqualDirs=\textit{/full/path/to/myProject/bin}:\textit{/full/path/to/myLibrary/bin} MyFile.java ...
\end{alltt}

Note that in these two examples, the compiled class file of the
\<myPackage.qual.MyFenum> annotation must exist in either the \<myProject/bin>
directory or the \<myLibrary/bin> directory. The following placement of
the class file will work with the above commands:

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

The two options can be used at the same time to provide groups of annotations
from directories, and individually named annotations.

\item
If your code uses the \refqualclass{checker/fenum/qual}{Fenum} annotation, you do
not need the \code{-Aquals} or \code{-AqualDirs} option:

\begin{Verbatim}
  javac -processor org.checkerframework.checker.fenum.FenumChecker MyFile.java ...
\end{Verbatim}

\end{itemize}

For an example of running the Fake Enum Checker on Android code, see
\url{https://github.com/karlicoss/checker-fenum-android-demo}.


\sectionAndLabel{Suppressing warnings}{fenum-suppressing}

One example of when you need to suppress warnings is when you initialize the
fenum constants to literal values.
To remove this warning message, add a \code{@SuppressWarnings} annotation to either
the field or class declaration, for example:

\begin{Verbatim}
@SuppressWarnings("fenum:assignment") // initialization of fake enums
class MyConsts {
  public static final @Fenum("A") int ACONST1 = 1;
  public static final @Fenum("A") int ACONST2 = 2;
}
\end{Verbatim}


\sectionAndLabel{Example}{fenum-example}

The following example introduces two fenums in class \code{TestStatic}
and then performs a few typical operations.

\begin{Verbatim}
@SuppressWarnings("fenum:assignment")   // initialization of fake enums
public class TestStatic {
  public static final @Fenum("A") int ACONST1 = 1;
  public static final @Fenum("A") int ACONST2 = 2;

  public static final @Fenum("B") int BCONST1 = 4;
  public static final @Fenum("B") int BCONST2 = 5;
}

class FenumUser {
  @Fenum("A") int state1 = TestStatic.ACONST1;     // ok
  @Fenum("B") int state2 = TestStatic.ACONST1;     // Incompatible fenums forbidden!

  void fenumArg(@Fenum("A") int p) {}

  void fenumTest() {
    state1 = 4;                     // Direct use of value forbidden!
    state1 = TestStatic.BCONST1;    // Incompatible fenums forbidden!
    state1 = TestStatic.ACONST2;    // ok

    fenumArg(5);                    // Direct use of value forbidden!
    fenumArg(TestStatic.BCONST1);   // Incompatible fenums forbidden!
    fenumArg(TestStatic.ACONST1);   // ok
  }
 }
\end{Verbatim}

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


\sectionAndLabel{The fake enumeration pattern}{fenum-pattern}

Java's
\href{https://docs.oracle.com/javase/specs/jls/se11/html/jls-8.html#jls-8.9}{\code{enum}}
keyword lets you define an enumeration type: a finite set of distinct values
that are related to one another but are disjoint from all other
types, including other enumerations.
Before enums were added to Java, there were two ways to encode an
enumeration, both of which are error-prone:

\begin{description}
\item[the fake enum pattern]  a set of \code{int} or \code{String}
  constants (as often found in older C code).

\item[the typesafe enum pattern]  a class with private constructor.
% This requires
% \href{http://www.javaworld.com/javaworld/javatips/jw-javatip122.html}{careful development}.
\end{description}

Sometimes you need to use the fake enum pattern,
rather than a real enum or the typesafe enum pattern.
%
One reason is backward-compatibility.  A public API that predates Java's
enum keyword may use \code{int} constants; it cannot be changed, because
doing so would break existing clients.  For example, Java's JDK still uses
\code{int} constants in the AWT and Swing frameworks, and Android also uses
\code{int} constants rather than Java enums.
%
Another reason is performance, especially in environments with limited
resources.  Use of an int instead of an object can
reduce code size, memory requirements, and run time.
% Android no longer recommends use of ints instead of enums:  see
% http://stackoverflow.com/questions/5143256/why-was-avoid-enums-where-you-only-need-ints-removed-from-androids-performanc

In cases when code has to use the fake enum pattern, the Fake Enum Checker,
or Fenum Checker, gives the same safety guarantees as a true enumeration type.
The developer can introduce new types that are distinct from all values of the
base type and from all other fake enums. Fenums can be introduced for
primitive types as well as for reference types.


\sectionAndLabel{References}{fenum-references}

\begin{itemize}
\item Case studies of the Fake Enum Checker:\\
  ``Building and using pluggable type-checkers''~\cite{DietlDEMS2011}
  (ICSE 2011, \url{https://homes.cs.washington.edu/~mernst/pubs/pluggable-checkers-icse2011.pdf#page=3})

\item Java Language Specification on enums:\\
  \url{https://docs.oracle.com/javase/specs/jls/se11/html/jls-8.html#jls-8.9}

\item Tutorial trail on enums:\\
  \url{https://docs.oracle.com/javase/tutorial/java/javaOO/enum.html}

\item Java Tip 122: Beware of Java typesafe enumerations:\\
  \url{https://www.infoworld.com/article/2077487/java-tip-122--beware-of-java-typesafe-enumerations.html}

\end{itemize}

% LocalWords:  enums typesafe Fenum Fenums fenum MyFenum quals fenums Aquals
% LocalWords:  TestStatic FenumC FenumD myPackage RetentionPolicy IntDef
% LocalWords:  SubtypeOf FenumTop MyFile Enum enum AWT java jls qual
%  LocalWords:  FenumUnqualified FenumBottom ElementType classpath typedef
%%  LocalWords:  bootclasspath AqualDirs myProject myLibrary RUNTIME
%  LocalWords:  setNavigationMode NavigationMode checkers'' processorpath