docs/manual/aliasing-checker.tex - typetools/checker-framework - Git at Google

 \htmlhr
 \chapterAndLabel{Aliasing Checker}{aliasing-checker}

 The Aliasing Checker identifies expressions that definitely have no
 aliases.

 Two expressions are aliased when they have the same non-primitive value;
 that is, they are references to the identical Java object
 in the heap. Another way of saying this is that two expressions,
 $\mathit{exprA}$ and $\mathit{exprB}$, are aliases of each other when
 $\mathit{exprA} \<==> \mathit{exprB}$ at the same program point.

 Assigning to a variable or field typically creates an alias.  For example,
 after the statement \<a = b;>, the variables \<a> and \<b> are aliased.

 Knowing that an expression is not aliased permits more accurate reasoning
 about how side effects modify the expression's value.

 To run the Aliasing Checker, supply the
 \code{-processor org.checkerframework.common.aliasing.AliasingChecker}
 command-line option to javac.
 However, a user rarely runs the Aliasing Checker directly.
 This type system is mainly intended to be used together with other type systems.
 For example, the SPARTA information flow type-checker
 (Section~\ref{sparta-checker}) uses the Aliasing Checker to improve its
 type refinement --- if an expression has no aliases, a more refined type
 can often be inferred, otherwise the type-checker makes conservative
 assumptions.

 \sectionAndLabel{Aliasing annotations}{aliasing-annotations}

 \begin{figure}
 \includeimage{aliasing}{2cm}
 \caption{Type hierarchy for the Aliasing type system.
   These qualifiers are applicable to any reference (non-primitive) type.}
 \label{fig-aliasing-hierarchy}
 \end{figure}

 There are two possible types for an expression:

 \begin{description}

 \item[\refqualclass{common/aliasing/qual}{MaybeAliased}]
 is the type of an expression that might have an alias.
 This is the default, so every unannotated type is
 \code{@MaybeAliased}. (This includes the type of \code{null}.)

 \item[\refqualclass{common/aliasing/qual}{Unique}]
 is the type of an expression that has no aliases.

 The \code{@Unique} annotation is only allowed at local variables, method
 parameters, constructor results, and method returns.
 A constructor's result should be annotated with \code{@Unique} only if the
 constructor's body does not creates an alias to the constructed object.

 \end{description}

 There are also two annotations, which are currently trusted instead of verified,
 that can be used on formal parameters (including
 the receiver parameter, \<this>):

 \begin{description}

 \item[\refqualclass{common/aliasing/qual}{NonLeaked}]
 identifies a formal parameter that is not leaked nor
 returned by the method body.
 For example, the formal parameter of the String copy constructor,
 \code{String(String s)}, is \code{@NonLeaked} because the body of the method
 only makes a copy of the parameter.

 \item[\refqualclass{common/aliasing/qual}{LeakedToResult}]
 is used when the parameter may be returned, but it is not
 otherwise leaked.
 For example, the receiver parameter of \code{StringBuffer.append(StringBuffer
 this, String s)} is
 \code{@LeakedToResult}, because the method returns the updated receiver.

 \end{description}

 \sectionAndLabel{Leaking contexts}{aliasing-leaking-contexts}
 This section lists the expressions that create aliases.  These are also
 called ``leaking contexts''.

 \begin{description}
 \item[Assignments]
 After an assignment, the left-hand side and the right-hand side are
 typically aliased.  (The only counterexample is when the right-hand side is
 a fresh expression; see Section~\ref{aliasing-refinement}.)

 \begin{Verbatim}
   @Unique Object u = ...;
   Object o = u;                    // (not.unique) type-checking error!
 \end{Verbatim}

 If this example type-checked, then \<u> and \<o> would be aliased.
 For this example to type-check, either the \<@Unique> annotation on the
 type of \<u>, or the \<o = u;> assignment, must be removed.

 \item[Method calls and returns (pseudo-assignments)]
 Passing an argument to a method is a ``pseudo-assignment'' because it effectively
 assigns the argument to the formal parameter.  Return statements are also
 pseudo-assignments.
 As with assignments, the left-hand side and right-hand side of
 pseudo-assignments are typically aliased.

 Here is an example for argument-passing:

 \begin{Verbatim}
   void mightDoAnything(Object o) { ... }

   @Unique Object u = ...;
   mightDoAnything(u);  // type-checking error, because the callee may create an alias of the passed argument
 \end{Verbatim}

 Passing a non-aliased
 reference to a method does not necessarily create an alias.
 However, the body of the method might create an alias or leak the
 reference.  Thus, the Aliasing Checker always treats a method call as
 creating aliases for each argument unless the corresponding formal
 parameter is marked as
 @\refqualclass{common/aliasing/qual}{NonLeaked} or
 @\refqualclass{common/aliasing/qual}{LeakedToResult}.

 Here is an example for a return statement:

 \begin{Verbatim}
 Object id(@Unique Object p) {
     return p;     // (not.unique) type-checking error!
 }
 \end{Verbatim}

 If this code type-checked, then it would be possible for clients to write
 code like this:

 \begin{Verbatim}
 @Unique Object u = ...;
 Object o = id(u);
 \end{Verbatim}

 \noindent
 after which there is an alias to \<u> even though it is declared as \<@Unique>.

 However, it is permitted to write

 \begin{Verbatim}
 Object id(@LeakedToResult Object p) {
     return p;
 }
 \end{Verbatim}

 \noindent
 after which the following code type-checks:

 \begin{Verbatim}
 @Unique Object u = ...;
 id(u);                   // method call result is not used
 Object o1 = ...;
 Object o2 = id(o1);      // argument is not @Unique
 \end{Verbatim}


 \item[Throws]
 A thrown exception can be captured by a catch block, which creates an
 alias of the thrown exception.

 \begin{Verbatim}
 void aliasInCatchBlock() {
     @Unique Exception uex = new Exception();
     try {
         throw uex;    // (not.unique) type-checking error!
     } catch (Exception ex) {
         // uex and ex refer to the same object here.
     }
 }
 \end{Verbatim}

 \item[Array initializers]

 Array initializers assign the elements in the initializers to corresponding
 indexes in the array, therefore expressions in an array initializer are leaked.

 \begin{Verbatim}
 void aliasInArrayInitializer() {
     @Unique Object o = new Object();
     Object[] ar = new Object[] { o };  // (not.unique) type-checking error!
     // The expressions o and ar[0] are now aliased.
 }
 \end{Verbatim}

 %Remember to add enhanced for statement if support to type variables is added.

 \end{description}


 \sectionAndLabel{Restrictions on where \<@Unique> may be written}{aliasing-unique-restrictions}

 The \<@Unique> qualifier may not be written on locations such as fields,
 array elements, and type parameters.

 As an example of why \<@Unique> may not be written on a field's type,
 consider the following code:

 \begin{Verbatim}
 class MyClass {
     @Unique Object field;
     void makesAlias() {
         MyClass myClass2 = this;
         // this.field is now an alias of myClass2.field
     }
 }
 \end{Verbatim}

 That code must not type-check, because \<field> is declared as \<@Unique>
 but has an alias.  The Aliasing Checker solves the problem by forbidding
 the \<@Unique> qualifier on subcomponents of a structure, such as fields.
 Other solutions might be possible; they would be more complicated but would
 permit more code to type-check.

 \<@Unique> may not be written on a type parameter for similar reasons.
 The assignment

 \begin{Verbatim}
 List<@Unique Object> l1 = ...;
 List<@Unique Object> l2 = l1;
 \end{Verbatim}

 \noindent
 must be forbidden because it would alias \<l1.get(0)> with \<l2.get(0)>
 even though both have type \<@Unique>.  The Aliasing Checker forbids this
 code by rejecting the type \code{List<@Unique Object>}.


 \sectionAndLabel{Aliasing type refinement}{aliasing-refinement}

 Type refinement enables a type checker to treat an expression as a subtype
 of its declared type.  For example, even if you declare a local variable as
 \<@MaybeAliased> (or don't write anything, since \<@MaybeAliased> is the
 default), sometimes the Aliasing Checker can determine that it is actually
 \<@Unique>.
 % This prevents the type checker from issuing false positive warnings.
 For more details, see Section~\ref{type-refinement}.

 The Aliasing Checker treats type refinement in the usual way,
 except that at (pseudo-)assignments
 the right-hand-side (RHS) may lose its type refinement, before the
 left-hand-side (LHS) is type-refined.
 The RHS always loses its type refinement (it is widened to
 \code{@MaybeAliased}, and its declared type must have been
 \code{@MaybeAliased}) except in the following cases:

 \begin{itemize}
 \item
 The RHS is a fresh expression --- an expression that returns a different value
 each time it is evaluated. In practice, this is only method/constructor calls
 with \code{@Unique} return type. A variable/field is not fresh because it can
 return the same value when evaluated twice.
 \item
 The LHS is a \code{@NonLeaked} formal parameter and the RHS is an argument in a
 method call or constructor invocation.
 \item
 The LHS is a \code{@LeakedToResult} formal parameter, the RHS is an argument in
 a method call or constructor invocation, and the method's return value is
 discarded --- that is, the method call or constructor invocation is written
 syntactically as a statement rather than as a part of a larger expression or
 statement.
 \end{itemize}
 %(Notice that the last two rules above are restricted to pseudo-assignments.)

 A consequence of the above rules is that most method calls are treated conservatively.
 If a variable with declared type \code{@MaybeAliased} has been refined
 to \code{@Unique} and is used as an argument of a method call, it usually loses its
 \code{@Unique} refined type.


 Figure~\ref{fig-aliasing-refinement-example} gives an example of the Aliasing Checker's
 type refinement rules.

 \begin{figure}
 %BEGIN LATEX
 \begin{smaller}
 %END LATEX
 \begin{Verbatim}
 // Annotations on the StringBuffer class, used in the examples below.
 // class StringBuffer {
 //  @Unique StringBuffer();
 //  StringBuffer append(@LeakedToResult StringBuffer this, @NonLeaked String s);
 // }

 void foo() {
     StringBuffer sb = new StringBuffer();    // sb is refined to @Unique.

     StringBuffer sb2 = sb;                   // sb loses its refinement.
     // Both sb and sb2 have aliases and because of that have type @MaybeAliased.
 }

 void bar() {
     StringBuffer sb = new StringBuffer();     // sb is refined to @Unique.

     sb.append("someString");
     // sb stays @Unique, as no aliases are created.

     StringBuffer sb2 = sb.append("someString");
     // sb is leaked and becomes @MaybeAliased.

     // Both sb and sb2 have aliases and because of that have type @MaybeAliased.
 }

 \end{Verbatim}
 %BEGIN LATEX
 \end{smaller}
 %END LATEX
 \caption{Example of the Aliasing Checker's type refinement rules.}
 \label{fig-aliasing-refinement-example}
 \end{figure}

 %%  LocalWords:  MaybeAliased NonLeaked LeakedToResult l1 l2 RHS LHS
 %%  LocalWords:  subcomponents
	\htmlhr
	\chapterAndLabel{Aliasing Checker}{aliasing-checker}

	The Aliasing Checker identifies expressions that definitely have no
	aliases.

	Two expressions are aliased when they have the same non-primitive value;
	that is, they are references to the identical Java object
	in the heap. Another way of saying this is that two expressions,
	$\mathit{exprA}$ and $\mathit{exprB}$, are aliases of each other when
	$\mathit{exprA} \<==> \mathit{exprB}$ at the same program point.

	Assigning to a variable or field typically creates an alias. For example,
	after the statement \<a = b;>, the variables \<a> and \<b> are aliased.

	Knowing that an expression is not aliased permits more accurate reasoning
	about how side effects modify the expression's value.

	To run the Aliasing Checker, supply the
	\code{-processor org.checkerframework.common.aliasing.AliasingChecker}
	command-line option to javac.
	However, a user rarely runs the Aliasing Checker directly.
	This type system is mainly intended to be used together with other type systems.
	For example, the SPARTA information flow type-checker
	(Section~\ref{sparta-checker}) uses the Aliasing Checker to improve its
	type refinement --- if an expression has no aliases, a more refined type
	can often be inferred, otherwise the type-checker makes conservative
	assumptions.

	\sectionAndLabel{Aliasing annotations}{aliasing-annotations}

	\begin{figure}
	\includeimage{aliasing}{2cm}
	\caption{Type hierarchy for the Aliasing type system.
	These qualifiers are applicable to any reference (non-primitive) type.}
	\label{fig-aliasing-hierarchy}
	\end{figure}

	There are two possible types for an expression:

	\begin{description}

	\item[\refqualclass{common/aliasing/qual}{MaybeAliased}]
	is the type of an expression that might have an alias.
	This is the default, so every unannotated type is
	\code{@MaybeAliased}. (This includes the type of \code{null}.)

	\item[\refqualclass{common/aliasing/qual}{Unique}]
	is the type of an expression that has no aliases.

	The \code{@Unique} annotation is only allowed at local variables, method
	parameters, constructor results, and method returns.
	A constructor's result should be annotated with \code{@Unique} only if the
	constructor's body does not creates an alias to the constructed object.

	\end{description}

	There are also two annotations, which are currently trusted instead of verified,
	that can be used on formal parameters (including
	the receiver parameter, \<this>):

	\begin{description}

	\item[\refqualclass{common/aliasing/qual}{NonLeaked}]
	identifies a formal parameter that is not leaked nor
	returned by the method body.
	For example, the formal parameter of the String copy constructor,
	\code{String(String s)}, is \code{@NonLeaked} because the body of the method
	only makes a copy of the parameter.

	\item[\refqualclass{common/aliasing/qual}{LeakedToResult}]
	is used when the parameter may be returned, but it is not
	otherwise leaked.
	For example, the receiver parameter of \code{StringBuffer.append(StringBuffer
	this, String s)} is
	\code{@LeakedToResult}, because the method returns the updated receiver.

	\end{description}

	\sectionAndLabel{Leaking contexts}{aliasing-leaking-contexts}
	This section lists the expressions that create aliases. These are also
	called ``leaking contexts''.

	\begin{description}
	\item[Assignments]
	After an assignment, the left-hand side and the right-hand side are
	typically aliased. (The only counterexample is when the right-hand side is
	a fresh expression; see Section~\ref{aliasing-refinement}.)

	\begin{Verbatim}
	@Unique Object u = ...;
	Object o = u; // (not.unique) type-checking error!
	\end{Verbatim}

	If this example type-checked, then \<u> and \<o> would be aliased.
	For this example to type-check, either the \<@Unique> annotation on the
	type of \<u>, or the \<o = u;> assignment, must be removed.

	\item[Method calls and returns (pseudo-assignments)]
	Passing an argument to a method is a ``pseudo-assignment'' because it effectively
	assigns the argument to the formal parameter. Return statements are also
	pseudo-assignments.
	As with assignments, the left-hand side and right-hand side of
	pseudo-assignments are typically aliased.

	Here is an example for argument-passing:

	\begin{Verbatim}
	void mightDoAnything(Object o) { ... }

	@Unique Object u = ...;
	mightDoAnything(u); // type-checking error, because the callee may create an alias of the passed argument
	\end{Verbatim}

	Passing a non-aliased
	reference to a method does not necessarily create an alias.
	However, the body of the method might create an alias or leak the
	reference. Thus, the Aliasing Checker always treats a method call as
	creating aliases for each argument unless the corresponding formal
	parameter is marked as
	@\refqualclass{common/aliasing/qual}{NonLeaked} or
	@\refqualclass{common/aliasing/qual}{LeakedToResult}.

	Here is an example for a return statement:

	\begin{Verbatim}
	Object id(@Unique Object p) {
	return p; // (not.unique) type-checking error!
	}
	\end{Verbatim}

	If this code type-checked, then it would be possible for clients to write
	code like this:

	\begin{Verbatim}
	@Unique Object u = ...;
	Object o = id(u);
	\end{Verbatim}

	\noindent
	after which there is an alias to \<u> even though it is declared as \<@Unique>.

	However, it is permitted to write

	\begin{Verbatim}
	Object id(@LeakedToResult Object p) {
	return p;
	}
	\end{Verbatim}

	\noindent
	after which the following code type-checks:

	\begin{Verbatim}
	@Unique Object u = ...;
	id(u); // method call result is not used
	Object o1 = ...;
	Object o2 = id(o1); // argument is not @Unique
	\end{Verbatim}



	\item[Throws]
	A thrown exception can be captured by a catch block, which creates an
	alias of the thrown exception.

	\begin{Verbatim}
	void aliasInCatchBlock() {
	@Unique Exception uex = new Exception();
	try {
	throw uex; // (not.unique) type-checking error!
	} catch (Exception ex) {
	// uex and ex refer to the same object here.
	}
	}
	\end{Verbatim}

	\item[Array initializers]

	Array initializers assign the elements in the initializers to corresponding
	indexes in the array, therefore expressions in an array initializer are leaked.

	\begin{Verbatim}
	void aliasInArrayInitializer() {
	@Unique Object o = new Object();
	Object[] ar = new Object[] { o }; // (not.unique) type-checking error!
	// The expressions o and ar[0] are now aliased.
	}
	\end{Verbatim}

	%Remember to add enhanced for statement if support to type variables is added.

	\end{description}


	\sectionAndLabel{Restrictions on where \<@Unique> may be written}{aliasing-unique-restrictions}

	The \<@Unique> qualifier may not be written on locations such as fields,
	array elements, and type parameters.

	As an example of why \<@Unique> may not be written on a field's type,
	consider the following code:

	\begin{Verbatim}
	class MyClass {
	@Unique Object field;
	void makesAlias() {
	MyClass myClass2 = this;
	// this.field is now an alias of myClass2.field
	}
	}
	\end{Verbatim}

	That code must not type-check, because \<field> is declared as \<@Unique>
	but has an alias. The Aliasing Checker solves the problem by forbidding
	the \<@Unique> qualifier on subcomponents of a structure, such as fields.
	Other solutions might be possible; they would be more complicated but would
	permit more code to type-check.

	\<@Unique> may not be written on a type parameter for similar reasons.
	The assignment

	\begin{Verbatim}
	List<@Unique Object> l1 = ...;
	List<@Unique Object> l2 = l1;
	\end{Verbatim}

	\noindent
	must be forbidden because it would alias \<l1.get(0)> with \<l2.get(0)>
	even though both have type \<@Unique>. The Aliasing Checker forbids this
	code by rejecting the type \code{List<@Unique Object>}.


	\sectionAndLabel{Aliasing type refinement}{aliasing-refinement}

	Type refinement enables a type checker to treat an expression as a subtype
	of its declared type. For example, even if you declare a local variable as
	\<@MaybeAliased> (or don't write anything, since \<@MaybeAliased> is the
	default), sometimes the Aliasing Checker can determine that it is actually
	\<@Unique>.
	% This prevents the type checker from issuing false positive warnings.
	For more details, see Section~\ref{type-refinement}.

	The Aliasing Checker treats type refinement in the usual way,
	except that at (pseudo-)assignments
	the right-hand-side (RHS) may lose its type refinement, before the
	left-hand-side (LHS) is type-refined.
	The RHS always loses its type refinement (it is widened to
	\code{@MaybeAliased}, and its declared type must have been
	\code{@MaybeAliased}) except in the following cases:

	\begin{itemize}
	\item
	The RHS is a fresh expression --- an expression that returns a different value
	each time it is evaluated. In practice, this is only method/constructor calls
	with \code{@Unique} return type. A variable/field is not fresh because it can
	return the same value when evaluated twice.
	\item
	The LHS is a \code{@NonLeaked} formal parameter and the RHS is an argument in a
	method call or constructor invocation.
	\item
	The LHS is a \code{@LeakedToResult} formal parameter, the RHS is an argument in
	a method call or constructor invocation, and the method's return value is
	discarded --- that is, the method call or constructor invocation is written
	syntactically as a statement rather than as a part of a larger expression or
	statement.
	\end{itemize}
	%(Notice that the last two rules above are restricted to pseudo-assignments.)

	A consequence of the above rules is that most method calls are treated conservatively.
	If a variable with declared type \code{@MaybeAliased} has been refined
	to \code{@Unique} and is used as an argument of a method call, it usually loses its
	\code{@Unique} refined type.


	Figure~\ref{fig-aliasing-refinement-example} gives an example of the Aliasing Checker's
	type refinement rules.

	\begin{figure}
	%BEGIN LATEX
	\begin{smaller}
	%END LATEX
	\begin{Verbatim}
	// Annotations on the StringBuffer class, used in the examples below.
	// class StringBuffer {
	// @Unique StringBuffer();
	// StringBuffer append(@LeakedToResult StringBuffer this, @NonLeaked String s);
	// }

	void foo() {
	StringBuffer sb = new StringBuffer(); // sb is refined to @Unique.

	StringBuffer sb2 = sb; // sb loses its refinement.
	// Both sb and sb2 have aliases and because of that have type @MaybeAliased.
	}

	void bar() {
	StringBuffer sb = new StringBuffer(); // sb is refined to @Unique.

	sb.append("someString");
	// sb stays @Unique, as no aliases are created.

	StringBuffer sb2 = sb.append("someString");
	// sb is leaked and becomes @MaybeAliased.

	// Both sb and sb2 have aliases and because of that have type @MaybeAliased.
	}

	\end{Verbatim}
	%BEGIN LATEX
	\end{smaller}
	%END LATEX
	\caption{Example of the Aliasing Checker's type refinement rules.}
	\label{fig-aliasing-refinement-example}
	\end{figure}

	%% LocalWords: MaybeAliased NonLeaked LeakedToResult l1 l2 RHS LHS
	%% LocalWords: subcomponents