docs/manual/must-call-checker.tex

\htmlhr
\chapterAndLabel{Must Call Checker}{must-call-checker}

The Must Call Checker conservatively over-approximates
the set of methods that an object should call before it is de-allocated.
The checker does not enforce that the methods are called before objects are de-allocated,
nor are its annotations refined after a method is called; rather,
it is intended to be run as a subchecker of another checker. On its own, it does not
enforce any rules other than subtyping. Instead, the types that the Must Call Checker
computes can be used by later checkers that require an over-approximation
of the methods that each object in the program should call.

For example, consider a \<java.io.OutputStream>.  This \<OutputStream>
might have an obligation to call the \<close()> method, to release an
underlying file resource. The type of this \<OutputStream> is
\<@MustCall(\{"close"\})>.  Or, the \<OutputStream> might not have such an
obligation, if the underlying resource is a byte array (or if \<close()>
has already been called). The type of this \<OutputStream> is
\<@MustCall(\{\})>.  For an arbitrary \<OutputStream>, the Must Call
Checker over-approximates the methods that it should call by assigning it
the type \<@MustCall(\{"close"\}) OutputStream>, which can be read as ``an
OutputStream that might need to call \<close()> (but no other methods)
before it is de-allocated''.

\sectionAndLabel{Must Call annotations}{must-call-annotations}

The Must Call Checker supports these type qualifiers:

\begin{description}

\item[\refqualclasswithparams{checker/mustcall/qual}{MustCall}{String[] value}]
  gives a superset of the methods that
  must be called before the expression's value is de-allocated.
  The default type qualifier for an unannotated type is \<@MustCall(\{\})>.

\item[\refqualclass{checker/mustcall/qual}{MustCallUnknown}]
  represents a value with an unknown or infinite set of must-call obligations.
  It is used internally by the type system but should never be written by a
  programmer.

\item[\refqualclass{checker/mustcall/qual}{PolyMustCall}]
  is the polymorphic annotation for the Must Call type system.
  For a description of polymorphic qualifiers, see
  Section~\ref{method-qualifier-polymorphism}.

\item[\refqualclasswithparams{checker/mustcall/qual}{InheritableMustCall}{String[] value}]
  is an alias of \<@MustCall> that can only be written on a class declaration.
  It applies both to the class declaration on which it is written and also to all subclasses.
  This frees the user of the need to write the \<@MustCall> annotation on every subclass.
  See Section~\ref{must-call-on-class} for details.

\end{description}

\begin{figure}
\includeimage{mustcall}{5cm}
\caption{Part of the Must Call Checker's type
qualifier hierarchy.  The full hierarchy contains one \<@MustCall> annotation
for every combination of methods.
Qualifiers in gray are used internally by the type system but should
never be written by a programmer.}
\label{fig-must-call-hierarchy}
\end{figure}

Here are some facts about the type qualifier hierarchy, which is shown in
Figure~\ref{fig-must-call-hierarchy}.
Any expression of type \<@MustCall(\{\}) Object> also has type
\<@MustCall(\{"foo"\}) Object>.
The type \<@MustCall(\{"foo"\}) Object>
contains objects that need to call \<foo> and objects that need to call
nothing, but the type does not contain an
object that needs to call \<bar> (or both \<foo> and \<bar>).
\<@MustCall(\{"foo", "bar"\}) Object> represents all objects that need to
call \<foo>, \<bar>, both, or neither; it cannot not represent an object that needs
to call some other method.


\sectionAndLabel{Writing \<@MustCall>/\<@InheritableMustCall> on a class}{must-call-on-class}

As explained in Section~\ref{upper-bound-for-use}, a type
annotation on a type declaration means that every use of the type has that
annotation by default. \<@MustCall> annotations on a class declaration should
usually also be shared by subclasses. To do so, a programmer can either write
a \<@MustCall> annotation on every subclass, or can write \<@InheritableMustCall>
on only the class, which will cause the checker to treat every subclass as if
it has an identical \<@MustCall> annotation.  The latter is the preferred style.

For example, given the following class annotation:
\begin{Verbatim}
    package java.net;

    import org.checkerframework.checker.mustcall.qual.InheritableMustCall;

    @InheritableMustCall({"close"}) class Socket { }
\end{Verbatim}
any use of \<Socket> or a subclass of \<Socket> defaults to \<@MustCall(\{"close"\}) Socket>.

The \<@InheritableMustCall> annotation is necessary because type
annotations cannot be made inheritable.  \<@InheritableMustCall> is
a declaration annotation.


%% \sectionAndLabel{Lightweight ownership annotations}{must-call-ownership-annos}

%% TODO: this explanation feels...lacking to me. It doesn't make that much sense IMO
%% without explaining the must-call consistency checker's usage of Owning/NotOwning.
%% It's therefore been commented out here. Some version of this needs to appear, either
%% here or in the documentation of the consistency checker, when that is merged. For now,
%% this manual page doesn't list @Owning or @NotOwning at all, because they can't be explained
%% without context - so we've decided to treat them as if they don't exist, for now.

%% In many programs, aliasing creates two or more program elements that represent the same
%% underlying object on which some methods might need to be called (i.e. whose type has a non-empty
%% \<@MustCall> qualifier). For example, an \<OutputStream> might be stored in both
%% a local variable and a field. Typically, the Must Call Checker will over-approximate both
%% the local variable and the field (and any other pointers to the object) as \<@MustCall(\{"close"\})>:
%% that is, because all \<OutputStream> objects might need to be closed, each pointer to an
%% \<OutputStream> might need to be closed, too. In practice, however, some of these pointers can be
%% ignored: they are \emph{non-owning}. In the example of an \<OutputStream> that is stored in both
%% a local variable and a field, for instance, it may be the case that the field is non-owning (such
%% as a cache) and the local is owning; or, it might be the case that the field is owning (an open connection,
%% for example, that will be closed later), and the local is non-owning.

%% The Must Call Checker supplies two annotations to support this concept: \<@Owning> and \<@NotOwning>.
%% The Must Call Checker's support for these annotations is limited: method parameters annotated as
%% \<@NotOwning> are treated as bottom (i.e. \<@MustCall(\{\})>) within the method bodies in which they
%% appear. A client analysis of the Must Call Checker can use these annotations as a guide for which
%% pointer to a given object is intended by the programmer as the pointer through which the must-call obligations
%% of the object are satisfied, but these annotations are only hints.

%% This feature can be disabled by passing the \<-AnoLightweightOwnership> command-line parameter to the Must
%% Call Checker.

\sectionAndLabel{Assumptions about reflection}{must-call-reflection}

The Must Call Checker is unsound with respect to reflection: it assumes
that objects instantiated reflectively do not have must-call obligations (i.e., that their
type is \<@MustCall(\{\})>. If the checker is run with \<-AresolveReflection>, then
this assumption applies only to types that cannot be resolved.

\sectionAndLabel{Type parameter bounds often need to be annotated}{must-call-type-params}

In an unannotated program, there may be mismatches between defaulted type
qualifiers that lead to type-checking errors.  That is, the defaulted
annotations at two different locations may be different and in conflict.  A
specific example is in code that contains a mix of explicit upper bounds
with an \<extends> clause and implicit upper bounds without an \<extends>
clause.

For example, consider the following example (from
\href{https://github.com/plume-lib/plume-util}{plume-lib/plume-util}) of an
interface with explicit upper bounds and a client with implicit upper
bounds:
\begin{Verbatim}
  interface Partition<ELEMENT extends @Nullable Object, CLASS extends @Nullable Object> {}

  class MultiRandSelector<T> {
    private Partition<T, T> eq;
  }
\end{Verbatim}

The code contains no \<@MustCall> annotations.
Running the Must Call Checker on this code produces an error at each use
of \<T> in \<MultiRandSelector>:

\begin{smaller}
\begin{Verbatim}
error: [type.argument] incompatible type argument for type parameter ELEMENT of Partitioner.
        private Partitioner<T, T> eq;
                            ^
  found   : T extends @MustCallUnknown Object
  required: @MustCall Object
error: [type.argument] incompatible type argument for type parameter CLASS of Partitioner.
        private Partitioner<T, T> eq;
                               ^
  found   : T extends @MustCallUnknown Object
  required: @MustCall Object
\end{Verbatim}
\end{smaller}

The defaulted Must Call annotations differ.
\<Partitioner> has an explicit bound, which uses the usual default of \<@MustCall(\{\})>.
\<MultiRandSelector> has an implicit bound, which defaults to top (that is,
\<@MustCallUnknown>), as explained in Section~\ref{climb-to-top}.

In many cases, including this one, you can eliminate the false positive
warning without writing any \<@MustCall> annotations.
You can either:
\begin{itemize}
\item
  adding an explicit bound to \<MultiRandSelector>, changing its declaration to
  \code{class MultiRandSelector<T extends Object>}, or
\item removing the explicit bound from \<Partition>, changing its declaration to
  \code{interface Partition<ELEMENT, CLASS>}.
\end{itemize}

% LocalWords:  de subchecker OutputStream MustCall MustCallUnknown
% LocalWords:  PolyMustCall InheritableMustCall MultiRandSelector
% LocalWords:  Partitioner