\section{Introduction}

Static analysis is useful \cite{ayewah2010google}, but underused in practice because of false positives \cite{Johnson2013}. A commonly-used way to reduce false positives is through programmer-provided annotations~\cite{barnett2007annotations} that make programmers intent manifest. For example, Facebook's Infer Eradicate~\cite{FacebookInfer}, Uber's \textsc{NullAway}~\cite{banerjee2019nullaway}, and the Java Nullness Checker from the Checker Framework~\cite{papi2008practical} all rely on \texttt{@NonNull} and \texttt{@Nullable} annotations to statically find and report potential null-pointer exceptions in Java code. However, in practice, annotating code completely can be very costly~\cite{chalin2007non}---or even impossible, for instance, when relying on third-party libraries and APIs.
As a result, since non-null reference variables are used extensively in software~\cite{chalin2007non}, many tools assume missing annotations are \texttt{@NonNull}. But, the huge number of false positives produced by such an approach in practice is a serious burden. To address this pitfall, \textsc{NullAway} assumes that sinks (i.e. targets of assignments and bindings) are \texttt{@Nullable} and sources are \texttt{@NonNull}. Unfortunately, both strategies are unsound, and therefore programs deemed valid may still raise null pointer exceptions at run time.

This paper explores a novel approach to these issues by drawing on research in gradual typing~\cite{siek2006gradual,siek2015refined,garcia2016abstracting} and its recent adaptation to gradual verification~\cite{bader2018gradual, wise2020gradual}.
We propose gradual program analysis as a principled, sound, and practical way to handle missing annotations. As a first step in the research agenda of gradual program analysis, this article studies the case of a simple null-pointer analysis. We present a general formal framework to derive gradual program analyses by transforming static analyses based on abstract interpretation~\cite{cousot:popl1977}. Specifically, we study analyses that operate over first-order procedural imperative languages and support user-provided annotations. This setting matches the core language used by many tools, such as Infer.
In essence, a \textit{gradual analysis} treats missing annotations optimistically, but injects run-time checks to preserve soundness. Crucially, the static portion of a gradual analysis uses the same algorithmic architecture as the underlying static analysis.\footnote{Note that an alternative is phrasing nullness as a type system, which can also be gradualized~\cite{brotherston2017granullar,blameForNull}.  We focus on approaches based on static analysis, which have very different technical foundations and user experience.  We compare to type-based approaches in Section~\ref{sec:related}.}

Additionally, we ensure that any gradual analysis produced from our framework satisfies the \textit{gradual guarantees}, adapted from Siek \emph{et al.}~\cite{siek2015refined} formulation for gradual typing. Any gradual analysis is also a \textit{conservative extension} of the base static analysis: when all annotations are provided, the gradual analysis is equivalent to the base static analysis, and no run-time checks are inserted.
Therefore, the gradual analysis smoothly trades off between static and dynamic checking, driven by the annotation effort developers are willing to invest.

To provide initial evidence of the applicability of gradual null-pointer analysis, we implement a gradual null-pointer analysis (GNPA) using Facebook's Infer analysis framework and report on preliminary experiments using the prototype.\footnote{\url{https://github.com/orgs/gradual-verification/packages/container/package/ecoop21}} The experiments show that a gradual null-pointer analysis can be effectively implemented, and used at scale to produce a small number of false positives in practice---fewer than Infer \textsc{Eradicate} as well as a more recent Infer checker, \textsc{NullSafe}. They also show that GNPA eliminates on average more than half of the null-pointer checks Java automatically inserts at run time. As a result, unlike other null-pointer analyses, GNPA can both prove the redundancy of run-time checks and reduce reported false positives.

The rest of the paper is organized as follows. In Section~\ref{sec:action}, we motivate gradual program analysis in the setting of null pointers by looking at how \textsc{Eradicate}, \textsc{NullSafe}, \textsc{NullAway}, and the Java Nullness Checker operate on example code with missing annotations, showcasing the concrete advantages of GNPA.
Section \ref{sec:language} formalizes PICL, a core imperative language similar to that of Infer. Section \ref{sec:static} then presents the static null-pointer analysis (NPA) for PICL, which is then used as the starting point for the derivation of the gradual analysis. We describe our approach to gradualizing a static program analysis in Section \ref{sec:gradual}, using GNPA as the running case study. Additionally, Section~\ref{sec:gradual} includes a discussion of important gradual properties our analysis adheres to: \textit{soundness}, \textit{conservative extension}, and the \textit{gradual guarantee}. All proofs can be found in the appendix of the full version of this paper.
We report on the preliminary empirical evaluation of an Infer GNPA checker called \emph{Graduator} in Section \ref{sec:empirical}.
Section~\ref{sec:related} discusses
related work and Section~\ref{sec:conclusion} concludes. In the conclusion, we sketch ways in which the approach presented here could be applied to other analysis domains, highlight open venues for future work in the area of gradual program analysis.

\section{Gradual Null-Pointer Analysis in Action}\label{sec:action}

This section informally introduces gradual null-pointer analysis and its potential compared to existing approaches through a simple example. We first briefly recall the basics of null-pointer analyses, and then discuss how current tools deal with missing annotations in problematic ways.

\subsection{Null-Pointer Analysis in a Nutshell}
\label{sec:npa-intro}

With programming languages that allow any type to be inhabited by a null value, programmers end up facing runtime errors (or worse if the language is unsafe) related to dereferencing null pointers. A null-pointer analysis is a static analysis that detects \emph{potential} null pointer dereferences and reports them as warnings, so that programmers can understand where explicit nullness checks should be added in order to avoid runtime errors.
Examples of null-pointer analyses are Infer Eradicate \cite{FacebookInferEradicate} and the Java Null Checker \cite{papi2008practical}.
Typically, a null-pointer analysis allows programmers to add annotations in the code to denote which variables (as well as fields, return values, etc.) are, or should be, non-null--e.g. \texttt{@NonNull}--and which are potentially null--e.g. \texttt{@Nullable}. A simple flow analysis is then able to detect and report conflicts, such as when a nullable variable is assigned to a non-null variable.

While a static null pointer analysis brings guarantees of robustness to a codebase, its adoption is not necessarily seamless. If a static analysis aims to be sound, it
must not suffer from false negatives, i.e. miss any actual null pointer dereference that can happen at runtime. While desirable, this means the analysis necessarily has to be conservative and therefore reports false positives---locations that are thought to potentially trigger null pointer dereferences, but actually do not.

This standard static analysis conundrum is exacerbated when considering programs where not all variables are annotated. Of course, in practice, a codebase is rarely fully annotated. Existing null-pointer analyses assign missing annotations a concrete annotation, such as $\ann{Nullable}$ or $\ann{NonNull}$. In doing so, they either report additional false positives, suffer from false negatives (and hence are unsound), or both. The rest of this section illustrates these issues with a simple example, and discusses how a gradual null-pointer analysis (GNPA) alleviates them. GNPA treats missing annotations in a special manner, following the gradual typing motto of being optimistic statically and relying on runtime checks for soundness~\cite{siek2006gradual}. Doing so allows the analysis to leverage both static and dynamic information to reduce false positives while maintaining soundness.

\subsection{Avoiding False Positives} \label{sec:action-falsepos}
GNPA can reduce the number of false positives reported by static tools by leveraging provided annotations and run-time checks. We demonstrate this with the unannotated program in Figure~\ref{fig:java-safereverse}. The program appends the reverse of a non-null string to the reverse of a null string and prints the result. The \texttt{reverse} method (lines \ref{line:safereverse-start}--\ref{line:safereverse-end}) returns the reverse of an input string when it is non-null and an empty string when the input is \texttt{null}. Additionally, \texttt{reverse} is unannotated, as highlighted for reference.

\begin{figure}
  \begin{center}
    \begin{minipage}{0.8\linewidth}
      \begin{lstlisting}[language=Java,numbers=left,escapechar=|]
class Main {

  static |\colorbox{lightblue}{\phantom{@?}}| String reverse(|\colorbox{lightblue}{\phantom{@?}}| String str) {|\label{line:safereverse-start}|
    if (str == null) return new String();|\label{line:return-nonnull}|
    StringBuilder builder = new StringBuilder(str);
    builder.reverse();
    return builder.toString();
  }|\label{line:safereverse-end}|

  public static void main(String[] args) {
    String reversed = reverse(null);|\label{line:safereverse-null}|
    String frown = reverse(":)");|\label{line:safereverse-smile}|
    String both = reversed.concat(frown);|\label{line:safereverse-concat}|
    System.out.println(both);
  }
}
\end{lstlisting}
    \end{minipage}
  \end{center}
  \caption{Unannotated Java code safely reversing nullable strings.}
  \label{fig:java-safereverse}
\end{figure}

The most straightforward approach to handling the missing annotations is to replace them with a fixed annotation.  Infer Eradicate and the Java Nullness Checker both choose \texttt{@NonNull} as the default, since that is the most frequent annotation used in practice~\cite{chalin2007non}.  Thus, in this example, they would treat \texttt{reverse}'s argument and return value as annotated with \texttt{@NonNull}. This correctly assigns \texttt{reversed} and \texttt{frown} as non-null on lines \ref{line:safereverse-null} and \ref{line:safereverse-smile}; and consequently, no false positive is reported when \texttt{reversed} is dereferenced on line \ref{line:safereverse-concat}. However, both tools will report a false positive each time \texttt{reverse} is called with \texttt{null}, as in line \ref{line:safereverse-null}.

Other uniform defaults are possible, but likewise lead to false positive warnings.  For example, choosing \texttt{@Nullable} by default would result in a false positive when \texttt{reversed} is dereferenced.  A more sophisticated choice would be the Java Nullness Checker's \texttt{@PolyNull} annotation, which supports type qualifier polymorphism for methods annotated with \texttt{@PolyNull}.  If \texttt{reverse}'s method signature is annotated with \texttt{@PolyNull}, then \texttt{reverse} would have two conceptual versions:
\begin{center}
\texttt{static @Nullable String reverse(@Nullable String str)}
\\
\texttt{static @NonNull String reverse(@NonNull String str)}
\end{center}
At a call site, the most precise applicable signature would be chosen; so, calling \texttt{reverse} with \texttt{null} (line \ref{line:safereverse-null}) would result in the \texttt{@Nullable} signature, and calling \texttt{reverse} with \texttt{":)"} (line \ref{line:safereverse-smile}) would result in the \texttt{@NonNull} signature. Unfortunately, this strategy marks \texttt{reversed} on line \ref{line:safereverse-null} as \texttt{@Nullable} even though it is \texttt{@NonNull}, and a false positive is reported when \texttt{reversed} is dereferenced on line \ref{line:safereverse-concat}.  So while \texttt{@PolyNull} increases the expressiveness of the annotation system, it does not solve the problem of avoiding false positives from uniform annotation defaults.

In contrast, GNPA optimistically assumes both calls to \texttt{reverse} in \texttt{main} (lines \ref{line:safereverse-null}--\ref{line:safereverse-smile}) are valid without assigning fixed annotations to \texttt{reverse}'s argument or return value. Then, the analysis can continue relying on \textit{contextual optimism} when reasoning about the rest of \texttt{main}: \texttt{reversed} is assumed \texttt{@NonNull} to satisfy its dereference on line \ref{line:safereverse-concat}.
Of course this is generally an unsound assumption, so a run-time check is inserted to ascertain the non-nullness of \texttt{reversed} and preserve soundness.
Alternatively, a developer could annotate the return value of \texttt{reverse} with \texttt{@NonNull}. GNPA will operate as before except it will leverage this new information during static reasoning. Therefore, \texttt{reversed} will be marked \texttt{@NonNull} on line \ref{line:safereverse-null} and the dereference of \texttt{reversed} on line \ref{line:safereverse-concat} will be statically proven safe without any run-time check.

It turns out that a non-uniform choice of defaults can be optimistic in the same sense as GNPA.  For example, \textsc{NullAway} assumes sinks are \texttt{@Nullable} and sources are \texttt{@NonNull} when annotations are missing. In fact, this strategy correctly annotates \texttt{reverse}, and so no false positives are reported by the tool for the program in Figure \ref{fig:java-safereverse}.
However, in contrast to the gradual approach, the \textsc{NullAway} approach is in fact unsound, as illustrated next.

\subsection{Avoiding False Negatives} \label{sec:action-falseneg}
When Eradicate, \textsc{NullAway}, and the Java Nullness Checker handle missing annotations, they all give up soundness in an attempt to limit the number of false positives produced.

To illustrate, consider the same program from Figure~\ref{fig:java-safereverse}, with one single change: the \texttt{reverse} method now returns \texttt{null} instead of an empty string (line \ref{line:return-nonnull}).
\begin{lstlisting}[language=Java,numbers=none,escapechar=|]
   if (str == null) return null;
\end{lstlisting}
All of the tools mentioned earlier, including \textsc{NullAway}, erroneously assume that the return value of \texttt{reverse} is \texttt{@NonNull}. On line \ref{line:safereverse-null}, \texttt{reversed} is assigned \texttt{reverse(null)}'s return value of \texttt{null}; so, it is an error to dereference \texttt{reversed} on line \ref{line:safereverse-concat}. Unfortunately, all of the tools assume \texttt{reversed} is assigned a non-null value and do not report an error on line \ref{line:safereverse-concat}. This is a \textit{false negative}, which means that at runtime the program will fail with a null-pointer exception.

GNPA is similarly optimistic about \texttt{reversed} being non-null on line \ref{line:safereverse-concat}. However, GNPA safeguards its optimistic static assumptions with run-time checks. Therefore, the analysis will correctly report an error on line \ref{line:safereverse-concat}.
Alternatively, a developer could annotate the return value of \texttt{reverse} with \texttt{@Nullable}. By doing so, the gradual analysis will be able to exploit this information statically to report a static error, instead of a dynamic error.

\mbox{}

To sum up, a gradual null-pointer analysis can reduce false positives by optimistically treating missing annotations, and preserve soundness by detecting errors at runtime. Of course, one may wonder why it is better to fail at runtime when passing a null value as a non-null annotated argument, instead of just relying on the upcoming null-pointer exception. There are two answers to this question. First, in unsafe languages like C, a null-pointer dereference results in a crash. Second, in a safe language like Java where a null-pointer dereference is anyway detected and reported, it can be preferable to fail as soon as possible, in order to avoid performing computation (and side effects) under an incorrect assumption. This is similar to how the eager reporting of gradual typing can be seen as an improvement over simply relying on the underlying safety checks of a dynamically-typed language.

\mbox{}

Next, we formally develop GNPA, prove that it is sound, and prove that it smoothly trades-off between static and dynamic checking following the gradual guarantee criterion from gradual typing~\cite{siek2015refined}. We finally report on an actual implementation of GNPA and compare its effectiveness with existing tools.

\section{PICL: A Procedural Imperative Core Language} \label{sec:language}

Following the Abstract Gradual Typing methodology introduced by Garcia \emph{et al.}~\cite{garcia2016abstracting}, we build GNPA on top of a static null-pointer analysis, NPA. Thus, we first formally present a procedural imperative core language (PICL), used for both analyses to operate on; we present NPA in Section \ref{sec:static}, and GNPA in Section \ref{sec:gradual}.
PICL is akin to the intermediate language of the Infer framework, and therefore the formal development around PICL drove the implementation of the Infer GNPA checker we evaluate in Section~\ref{sec:empirical}.

\begin{figure}[]
  \centering
 \begin{minipage}[t]{0.47\linewidth}
  \begin{plstx}
    *: x, y [\in] \sett{Var} \\
    *: e [\in] \sett{Expr} \\
    *: a [\in] \sett{Ann} = \{\texttt{Nullable},~\texttt{NonNull},~\qm\}\\
    : P ::= \overline{procedure} ~\overline{field} ~s \\
    : field ::= T ~f; \\
    : procedure ::= T\texttt{@}a~ m ~(~\overline{T\texttt{@}a ~x}~)~ \{ ~s~ \} \\
    : T ::= \texttt{ref} \\
    : \oplus ::= \land | \lor \\
  \end{plstx}
\end{minipage}\hfill
 \begin{minipage}[t]{0.47\linewidth}
  \begin{plstx}
    *: m [\in] \sett{Proc} \\
    *: f [\in] \sett{Field} \\
    *: s [\in] \sett{Stmt} \\
    : e ::= \code{null} | x | e \oplus e | e.f | \exprNew{\overline{f}} | \exprCall{m}{x} \\
    : c ::= e = \code{null} | e \neq \code{null} \\
    : s ::= \code{skip}
    | \stmtSeq{s}{s}
    | \stmtDecl{T}{x}
    | \stmtAssign{x}{e}
    | \stmtFieldAssign{x}{f}{y}
    | \stmtIfElse{c}{s}{s}
    | \stmtWhile{c}{s}
    | \stmtReturn{y} \\
  \end{plstx}
\end{minipage}
  \caption{Abstract syntax of PICL.}
  \label{fig:syntax}
\end{figure}

\subsection{Syntax \& Static Semantics}

The syntax of PICL can be found in Figure \ref{fig:syntax}. Programs consist of procedures\footnote{Procedures accept only one parameter to simplify later formalisms.}, fields, and statements. Statements include the empty statement, sequences, variable declarations, variable and field assignments, conditionals, while loops, and returns. Expressions consist of \texttt{null} literals, variables, comparisons, conjunctions, disjunctions, field accesses, object allocations, and procedure calls. Finally, procedures may have \texttt{Nullable} or \texttt{NonNull} annotations on their arguments and return values. Missing annotations are represented by \qm.

As the focus of this work is not on typing, we only consider well-formed and well-typed programs, which is standard and not formalized here. In particular, variables are declared and initialized before use, and field and procedure names are unique.

\subsection{Control Flow Graph Representation}
Well-formed programs written in the abstract syntax given in Fig. \ref{fig:syntax} are translated into \emph{control flow graphs}---one graph for each procedure body and one for the main $s$. A finite control flow graph (CFG) for program $p$ has vertices $\sett{Vert}_p$ and edges $\sett{Edge}_p \subseteq \sett{Vert}_p \times \sett{Vert}_p$. For $v_1, v_2 \in \sett{Vert}_p$, we write $\arcsto{p}{v_1}{v_2}$ to denote $(v_1, v_2) \in \sett{Edge}_p$. Each vertex holds a single instruction, which we can access using the function $\func{inst}_p : \sett{Vert}_p \to \sett{Inst}$. We write $\inst[v]{\iota}$ to denote a vertex $v \in \sett{Vert}_p$ such that $\func{inst}_p(v) = \iota$, or just $\inst{\iota}$ (omitting the $v$) when the vertex itself is not important. By construction, these translated CFGs satisfy certain well-formedness properties, listed in the appendix of the full version of this paper.

\begin{figure}[]
  \centering
  \begin{minipage}[t]{0.47\linewidth}
  \begin{plstx}
    *: x, y, z [\in] \sett{Var} \\
    *: a, b [\in] \sett{Ann} = \{\texttt{Nullable},~\texttt{NonNull},~\qm\} \\
  \end{plstx}
  \end{minipage}\hfill
  %
  \begin{minipage}[t]{0.47\linewidth}
  \begin{plstx}
    *: m [\in] \sett{Proc} \\
    *: f [\in] \sett{Field} \\
  \end{plstx}
  \end{minipage}
  %
  \begin{plstx}
    : I ::= \stmtAssign{x}{y}
    | \stmtAssign{x}{\code{null}}
    | \stmtCall{x}{m\texttt{@}a}{y\texttt{@}b}
    | \stmtAssign{x}{\exprNew{\overline{f}}}
    | \stmtAssign{x}{y \land z}
    | \stmtAssign{x}{y \lor z}
    | \stmtAssign{x}{y.f}
    | \stmtFieldAssign{x}{f}{y}
    | \stmtBranch{x}
    | \stmtIf{x}
    | \stmtElse{x}
    | \stmtReturn{y\texttt{@}a}
    | \code{main}
    | \stmtProc{m\texttt{@}a}{y\texttt{@}b}\\
  \end{plstx}
  \caption{Abstract syntax of a CFG instruction.}
  \label{fig:instr-syntax}
\end{figure}

The set of possible instructions is defined in Figure~\ref{fig:instr-syntax}. In general, the CFG instructions are atomic variants of program statements designed to simplify the analysis presentations. Figure \ref{fig:ex-cfg} gives the CFG of a simple procedure \texttt{foo}, which calls \texttt{bar} repeatedly until \texttt{x} becomes non-null and then returns \texttt{x}. The CFG starts with \texttt{foo}'s entry node $\stmtProc{foo@NonNull}{x@Nullable}$ (similarly, $\code{main}$ is always the entry node of the main program's CFG). Then, the while loop on lines \ref{ex:cfg-while-start}--\ref{ex:cfg-while-end} results in the $\stmtBranch{x}$ sub-graph, which leads to $\stmtIf{x}$ when $x$ is non-null and $\stmtElse{x}$ when $x$ is null. The call to \texttt{bar} follows from $\stmtElse{x}$ and loops back to $\stmtBranch{x}$ as expected. Finally, $\stmtReturn{x@NonNull}$ follows from $\stmtIf{x}$ ending the CFG. Precise semantics for instructions is given in Section \ref{sec:dyn-lang-semantics}.

\begin{figure}[]
  \begin{minipage}[t]{0.5\textwidth}
  \centering
  \small
  \begin{lstlisting}[language=Java,numbers=left,escapechar=|]
  ref@NonNull foo(ref@Nullable x)
  {
    |\label{ex:cfg-while-start}|while (x == null)
    {
      x := bar(x);
    |\label{ex:cfg-while-end}|}
    return x;
  }
  \end{lstlisting}
  \end{minipage}\hfill
  \begin{minipage}[t]{0.5\textwidth}
  \strut\vspace*{-\baselineskip}\newline
  \centering
  \begin{tikzpicture}[->]
    \node (v1) {\stmtProc{\texttt{foo@NonNull}}{\texttt{x@Nullable}}};
    \node (v2) [below = 0.5cm of v1] {\stmtBranch{\texttt{x}}};
    \node (v3) [below right = 0.5cm and 0.3cm of v2] {\stmtIf{\texttt{x}}};
    \node (v4) [below left = 0.5cm and 0.2cm of v2] {\stmtElse{\texttt{x}}};
    \node (v5) [below right = 0.5cm and -1.5cm of v4] {\stmtCall{\texttt{x}}{\texttt{bar@?}}{\texttt{x@?}}};
    \node (v6) [below right = 0.5cm and -1cm of v3] {\stmtReturn{\texttt{x@NonNull}}};

    \draw (v1) -> (v2);
    \draw (v2) -> (v3);
    \draw (v2) -> (v4);
    \draw (v4) -> (v5);
    \draw (v5) -> (v2);
    \draw (v3) -> (v6);
  \end{tikzpicture}
  \end{minipage}
  \caption{Example CFG.}
  \label{fig:ex-cfg}
\end{figure}

\subsection{Dynamic Semantics} \label{sec:dyn-lang-semantics}
We define the set of possible object locations as the set of natural numbers and 0, $\sett{Val} = \mathbb{N} \cup \{0\}$. The \texttt{null} pointer is location 0.

Now, a program state ($\sett{State}_p \subseteq \sett{Stack}_p \times \sett{Mem}_p$) consists of a stack and a heap. A heap $\mu \in \sett{Mem}_p = (\sett{Val} \setminus \{0\}) \rightharpoonup (\sett{Field} \rightharpoonup \sett{Val})$ maps object locations and field names to program values---other (possibly null) pointers. A stack is made of stack frames each containing a local variable environment and CFG node:
\begin{align*}
  S \in \sett{Stack}_p ::= E \cdot S \mid \mathsf{nil}
  \qq{where} & E \in \sett{Frame}_p = \sett{Env} \times \sett{Vert}_p \\
  \qand      & \sett{Env} = \sett{Var} \rightharpoonup \sett{Val}.
\end{align*}

Further, we restrict the set of states $\xi = \stat{\fram{\rho_1}{v_1} \cdot \fram{\rho_2}{v_2} \cdots \fram{\rho_n}{v_n} \cdot \mathsf{nil}}{\mu} \in \sett{State}_p$ to include only those satisfying the following conditions:
\begin{enumerate}
  \item \textit{Bottom stack frame is in \code{main}:} Let $\func{descend} : \sett{Vert}_p \to \mathcal{P}^{+}(\sett{Vert}_p)$ give the descendants of each node in the control flow graph. Then $v_i \in \func{descend}(v_0)$ if and only if $i = n$.
  \item \textit{Every variable defaults to \code{null}{} (except on \code{main}{} and \code{proc}{} nodes):} If $\func{inst}_p(v_i) \neq \code{main}$ and $\func{inst}_p(v_i) \neq \stmtProc{m@a}{y@b}$ then $\rho_i$ is a total function.
  \item \textit{Follow the ``true'' branch when non-null:} If $\func{inst}_p(v_i) = \stmtIf{y}$ then $\rho_i(y) \neq 0$.
  \item \textit{Follow the ``false'' branch when null:} If $\func{inst}_p(v_i) = \stmtElse{y}$ then $\rho_i(y) = 0$.
  \item\label{rule:call} \textit{Every frame except the top is a procedure call:}
    If $v_i \in \func{descend}(\stmtProc{m\texttt{@}a}{y\texttt{@}b})$ then $\func{inst}_p(v_{i +
    1}) = \stmtCall{x}{m\texttt{@}a}{y'\texttt{@}b}$, and either $b = \qm$ or $\rho_{i + 1}(y') \in \func{conc}(b)$ (see section~\ref{sec:static}.
\end{enumerate}

Now, the small-step semantics of PICL is given in
Figure~\ref{fig:semantics}, where $\rho_0 = \set{x \mapsto 0}{x \in \sett{Var}}$.
\begin{figure}[]
  \centering
  \begin{footnotesize}
    \begin{gather*}
      \stat{\fram{\rho}{\inst[u]{\stmtAssign{x}{y}}} \cdot S}{\mu} \longrightarrow_p \stat{\fram{\rho[x \mapsto \rho(y)]}{v} \cdot S}{\mu} \\
      \stat{\fram{\rho}{\inst[u]{\stmtBranch{y}}} \cdot S}{\mu} \longrightarrow_p \stat{\fram{\rho}{\inst[v]{\func{branch}(\rho(y), y)}} \cdot S}{\mu} \\
      \stat{\fram{\rho}{\inst[u]{\stmtIf{y}}} \cdot S}{\mu} \longrightarrow_p \stat{\fram{\rho}{v} \cdot S}{\mu} \\
      \stat{\fram{\rho}{\inst[u]{\stmtElse{y}}} \cdot S}{\mu} \longrightarrow_p \stat{\fram{\rho}{v} \cdot S}{\mu} \\
      \stat{\fram{\rho}{\inst[u]{\stmtCall{x}{m\texttt{@}a}{y\texttt{@}b}}} \cdot S}{\mu} \longrightarrow_p \stat{\fram{\varnothing}{\inst{\stmtProc{m\texttt{@}a}{y'\texttt{@}b}}} \cdot \fram{\rho}{u} \cdot S}{\mu} \\
      \stat{\fram{\rho_1}{\inst[u]{\stmtProc{m\texttt{@}a}{y\texttt{@}b}}} \cdot \fram{\rho_2}{\inst[w]{\stmtCall{x}{m\texttt{@}a}{y'\texttt{@}b}}} \cdot S}{\mu} \longrightarrow_p \stat{\fram{\rho_0[y \mapsto \rho_2(y')]}{v} \cdot \fram{\rho_2}{w} \cdot S}{\mu} \\
      \stat{\fram{\rho_1}{\inst{\stmtReturn{y\texttt{@}a}}} \cdot \fram{\rho_2}{\inst[u]{\stmtCall{x}{m\texttt{@}a}{y'\texttt{@}b}}} \cdot S}{\mu} \longrightarrow_p \stat{\fram{\rho_2[x \mapsto \rho_1(y)]}{v} \cdot S}{\mu}\;\dagger \\
      \stat{\fram{\rho}{\inst[u]{\stmtAssign{x}{\code{null}}}} \cdot S}{\mu} \longrightarrow_p \stat{\fram{\rho[x \mapsto 0]}{v} \cdot S}{\mu} \\
      \stat{\fram{\rho}{\inst[u]{\stmtAssign{x}{\exprNew{\overline{f}}}}} \cdot S}{\mu} \longrightarrow_p \stat{\fram{\rho[x \mapsto \func{new}(\mu)]}{v} \cdot S}{\mu[\func{new}(\mu) \mapsto \overline{[f_i \mapsto \code{null}]}]} \\
      \stat{\fram{\rho}{\inst[u]{\stmtAssign{x}{y \land z}}} \cdot S}{\mu} \longrightarrow_p \stat{\fram{\rho[x \mapsto \func{and}(\rho(y), \rho(z))]}{v} \cdot S}{\mu} \\
      \stat{\fram{\rho}{\inst[u]{\stmtAssign{x}{y \lor z}}} \cdot S}{\mu} \longrightarrow_p \stat{\fram{\rho[x \mapsto \func{or}(\rho(y), \rho(z))]}{v} \cdot S}{\mu} \\
      \stat{\fram{\rho}{\inst[u]{\stmtAssign{x}{y.f}}} \cdot S}{\mu} \longrightarrow_p \stat{\fram{\rho[x \mapsto \mu(\rho(y))(f)]}{v} \cdot S}{\mu} \\
      \stat{\fram{\rho}{\inst[u]{\stmtAssign{x.f}{y}}} \cdot S}{\mu} \longrightarrow_p \stat{\fram{\rho}{v} \cdot S}{\mu[\rho(x) \mapsto [f \mapsto \rho(y)]]} \\
      \stat{\fram{\rho}{\inst[u]{\code{main}}} \cdot S}{\mu} \longrightarrow_p \stat{\fram{\rho_0}{v} \cdot S}{\mu}
    \end{gather*}
  \end{footnotesize}
  \caption{Small-step semantics rules that hold when $\arcsto{p}{u}{v}$. \;
    $\dagger{}$ This particular rule only applies if either $a = \qm$ or
    $\rho_1(y) \in \func{conc}(a)$ (see Section~\ref{sec:static}).}
  \label{fig:semantics}
\end{figure}
The rules rely on the following helper functions:
\begin{align*}
  \func{new}        & : \sett{Mem}_p \to \sett{Val} \setminus \{0\} & \func{new}(\mu)           & = 1 + \max(\{0\} \cup \dom(\mu))                     \\
  \func{branch}     & : \sett{Val} \times \sett{Var} \to \sett{Inst}                  & \func{branch}(n, x)          & = \stmtIf{x}\text{ if }n > 0\text{; }\stmtElse{x}\text{ otherwise} \\
  \func{and}        & : \sett{Val} \times \sett{Val} \to \sett{Val}      & \func{and}(n_1, n_2)      & = n_2\text{ if }n_1 > 0\text{; }n_1\text{ otherwise}   \\
  \func{or}         & : \sett{Val} \times \sett{Val} \to \sett{Val}      & \func{or}(n_1, n_2)       & = n_1\text{ if }n_1 > 0\text{; }n_2\text{ otherwise}
\end{align*}

Notably, $\stmtBranch{y}$ steps to the $\stmtIf{y}$ node when $y$ is non-null and $\stmtElse{y}$ when $y$ is null. Additionally, if a procedure call's argument disagrees with its parameter annotation, then it will get stuck (rule~\ref{rule:call} for states); otherwise, the call statement will safely step to the procedure's body. In contrast, the semantics will get stuck if a return value does not agree with the procedure's return annotation.

\section{A Static Null-Pointer Analysis for PICL}\label{sec:static}
In this section, we formalize a static null-pointer analysis, called NPA, for PICL on which we will build GNPA. Here, we will only consider completely annotated programs, $\sett{Ann} = \{ \ann{Nullable} ,~ \ann{NonNull} \}$. Therefore, we use a ``prime'' symbol for sets like $\sett{Inst}' \subseteq \sett{Inst}$ to indicate that this is not the whole story. We present NPA's semilattice of abstract values, flow function, fixpoint algorithm, and how the analysis uses the results from the fixpoint algorithm to report warnings to the user.

\subsection{Semilattice of Abstract Values} \label{sec:static-semilattice}
The set of abstract values $\sett{Abst} = \{\ann{Nullable},~ \ann{Null},~ \ann{NonNull}\}$ make up the finite semilattice defined in Figure~\ref{fig:semilattice}.
The partial order $\sqsubseteq~ \subseteq \sett{Abst} \times \sett{Abst}$ given is
\begin{mathpar}
\ann{Null} \sqsubseteq \ann{Nullable}
\and
\ann{NonNull} \sqsubseteq \ann{Nullable}
\and
\forall.~ l \in \sett{Abst} ~.~ l \sqsubseteq l.
\end{mathpar}
The join function $\sqcup : \sett{Abst} \times \sett{Abst} \to \sett{Abst}$ induced by the partial order is:
\begin{mathpar}
\ann{Null} ~\sqcup~ \ann{NonNull} = \ann{Nullable}
\and
\forall.~ l \in \sett{Abst} ~.~ l ~\sqcup~ \ann{Nullable} = \ann{Nullable}
\and
\forall.~ l \in \sett{Abst} ~.~ l ~\sqcup~ l = l
\end{mathpar}
Clearly, $\ann{Nullable}$ is the top element $\top$.
\begin{figure}
  \centering
  \begin{tikzpicture}
    \node (t) {\ann{Nullable}};
    \node (a) [below left = 0.5cm and -0.5cm of t] {\ann{Null}};
    \node (b) [below right = 0.5cm and -0.5cm of t] {\ann{NonNull}};

    \draw (t) -- (a);
    \draw (t) -- (b);
  \end{tikzpicture}
  \caption{The \sett{Abst}{} semilattice.}
  \label{fig:semilattice}
\end{figure}
Next, we relate this semilattice to $\sett{Val}$ via a concretization function
$\func{conc} : \sett{Abst} \to \mathcal{P}^{+}(\sett{Val})$:
  \[
    \func{conc}(\ann{Nullable}) = \sett{Val} \qc
    \func{conc}(\ann{Null}) = \{0\} \qc
    \func{conc}(\ann{NonNull}) = \sett{Val} \setminus \{0\},
  \]
which satisfies the property $\forall.~ l_1, l_2 \in \sett{Abst} ~.~ l_1 \sqsubseteq~ l_2 ~\iff~ \func{conc}(l_1) \subseteq \func{conc}(l_2)$.

\subsection{Flow Function}
Similar to how we use $\sett{Env}$ to represent mappings from variables to concrete values, we will use $\sigma \in \sett{Map} = \sett{Var} \rightharpoonup \sett{Abst}$ to represent mappings from variables to abstract values---\emph{abstract states}. Then, we extend the semilattice's partial order relation to abstract states $\sigma_1,
  \sigma_2 \in \sett{Map}$:
\[
  \sigma_1 \sqsubseteq \sigma_2
  \quad\iff\quad
  \forall.~ x \in \sett{Var} ~.~ \sigma_1(x) \sqsubseteq \sigma_2(x)
\]

\noindent We also extend the join operation to abstract states $\sigma_1, \sigma_2 \in \sett{Map}$:
        \[
          (\sigma_1 \sqcup \sigma_2)(x) =
          \begin{cases}
            a \sqcup b        & \text{if $\sigma_1(x) = a$ and $\sigma_2(x) = b$}          \\
            a                & \text{if $\sigma_1(x) = a$ and $\sigma_2(x)$ is undefined} \\
            b                & \text{if $\sigma_1(x)$ is undefined and $\sigma_2(x) = b$} \\
            \text{undefined} & \text{otherwise}.
          \end{cases}
        \]

The NPA's flow function $\func{flow} : \sett{Inst}' \times \sett{Map} \to \sett{Map}$ is defined in Figure~\ref{fig:flow}. Note, $\sigma_0 = \set{x \mapsto \ann{Null}}{x \in \sett{Var}}$. Also, we omit the $\stmtReturn{y\texttt{@}a}$ case because it does not have CFG successors in a well-formed program.

\begin{figure}[]
  \centering
  \begin{align*}
    \func{flow}(\stmtAssign{x}{y}, \sigma)        & = \sigma[x \mapsto \sigma(y)]            \\
    \func{flow}(\stmtBranch{x}, \sigma)           & = \sigma                                 \\
    \func{flow}(\stmtIf{x}, \sigma)               & = \sigma[x \mapsto \ann{NonNull}]                 \\
    \func{flow}(\stmtElse{x}, \sigma)             & = \sigma[x \mapsto \ann{Null}]                 \\
    \func{flow}(\stmtCall{x}{m\texttt{@}a}{y\texttt{@}b}, \sigma) & = \sigma[x \mapsto a]                    \\
    \func{flow}(\stmtProc{m\texttt{@}a}{y\texttt{@}b}, \sigma)    & = \sigma_0[y \mapsto b]                  \\
    \func{flow}(\stmtAssign{x}{\code{null}}, \sigma)             & = \sigma[x \mapsto \ann{Null}]                 \\
    \func{flow}(\stmtAssign{x}{\exprNew{\overline{f}}}, \sigma)       & = \sigma[x \mapsto \ann{NonNull}]                 \\
    \func{flow}(\stmtAssign{x}{y \land z}, \sigma) & = \begin{cases}
      \sigma[x \mapsto \ann{Null}] & \text{if }\ann{Null} \in \{\sigma(y), \sigma(z)\} \\
      \sigma[x \mapsto \ann{Nullable}] & \text{if }\ann{Nullable} \in \{\sigma(y), \sigma(z)\} \\
      \sigma[x \mapsto \ann{NonNull}] & \text{otherwise}
    \end{cases} \\
    \func{flow}(\stmtAssign{x}{y \lor z}, \sigma) & = \begin{cases}
      \sigma[x \mapsto \ann{NonNull}] & \text{if }\ann{NonNull} \in \{\sigma(y), \sigma(z)\} \\
      \sigma[x \mapsto \ann{Nullable}] & \text{if }\ann{Nullable} \in \{\sigma(y), \sigma(z)\} \\
      \sigma[x \mapsto \ann{Null}] & \text{otherwise}
    \end{cases} \\
    \func{flow}(\stmtAssign{x}{y.f}, \sigma)           & = \sigma[x \mapsto \ann{Nullable}][y \mapsto \ann{NonNull}] \\
    \func{flow}(\stmtFieldAssign{x}{f}{y}, \sigma)        & = \sigma[x \mapsto \ann{NonNull}]                 \\
    \func{flow}(\code{main}, \sigma)          & = \sigma_0
  \end{align*}
  \caption{All consequential cases of the flow function used by NPA.}
  \label{fig:flow}
\end{figure}

\subsubsection{Properties}
It can be shown that this flow function is monotonic: for any $\iota \in \sett{Inst}'$ and abstract states $\sigma_1, \sigma_2 \in \sett{Map}$, if $\sigma_1 \sqsubseteq \sigma_2$ then $\func{flow}\bb{\iota}(\sigma_1) \sqsubseteq \func{flow}\bb{\iota}(\sigma_2)$. It can also be shown that the flow function is locally sound, \emph{i.e.}~ the flow function models the concrete semantics at each step. To express this property formally, we define the predicate $\predd{desc}(\rho, \sigma)$ on $\sett{Env} \times \sett{Map}$, which says that the abstract state $\sigma$ ``describes'' the concrete environment $\rho$:
\[
  \predd{desc}(\rho, \sigma)
  \quad\iff\quad
  \text{for all $x \in \sett{Var} ~.~ \rho(x) \in \func{conc}(\sigma(x))$.}
\]
Then, if
 $\stat{S' \cdot \fram{\rho}{\inst[v]{\iota}} \cdot S}{\mu}
  \longrightarrow_p
  \stat{\fram{\rho'}{v'} \cdot S}{\mu'}$,
it must be the case that
\[
  \predd{desc}(\rho, \sigma)
  \quad\implies\quad
  \predd{desc}(\rho', \func{flow}\bb{\iota}(\sigma))
  \qq{for all}
  \sigma \in \sett{Map}.
\]

\subsection{Fixpoint Algorithm}
This brings us to Algorithm~\ref{alg:kildall} \cite{kildall1973unified}, which is used to analyze a program and compute whether each program variable is $\ann{Nullable}$, $\ann{NonNull}$, or $\ann{Null}$ at each program point (the program results $\pi$). More specifically, the algorithm applies the flow function to each program instruction recording or updating the results until a fixpoint is reached---\emph{i.e.}~ until the results stop changing (becoming more approximate). The algorithm will always reach a fixpoint (terminate), because $\func{flow}$ is monotone and the height of the semilattice (Sec. \ref{sec:static-semilattice}) is finite. Note, the algorithm does not specify the order in which instructions are analyzed, because the order does not affect the results when $\func{flow}$ is monotonic. An implementation may choose to analyze instructions in CFG order---following the directed edges of the CFG.

\begin{algorithm}
  \caption{Kildall's worklist algorithm}
  \label{alg:kildall}
  \begin{algorithmic}[1]
    \Function{Kildall}{$\func{flow}, \sqcup, p$}
      \State $\pi \gets \set{v \mapsto \varnothing}{v \in \sett{Vert}_p}$
      \State $V \gets \sett{Vert}_p$ \Comment{$V \subseteq \sett{Vert}_p$}
      \While{$V \neq \varnothing$} \label{line:while}
        \State $\inst[v]{\iota} \gets \text{an element of $V$}$ \Comment{$v \in V$ and $\iota = \func{inst}_p(v)$}
        \State $V \gets V \setminus \{v\}$ \Comment{$v \notin V$}
        \State $\sigma \gets \pi(v)$ \label{line:sigma}
        \State $\sigma' \gets \func{flow}\bb{\iota}(\sigma)$ \label{line:flow}
        \For{$\arcsto{p}{v}{u}$} \label{line:for} \Comment{$u \in \sett{Vert}_p$}
          \If{$\sigma' \sqcup \pi(u) \neq \pi(u)$} \label{line:if} \Comment{think of as $\sigma' \not\sqsubseteq \pi(u)$}
            \State{$\pi(u) \gets \pi(u) \sqcup \sigma'$} \label{line:join}
            \State{$V \gets V \cup \{u\}$} \label{line:enqueue}
          \EndIf \label{line:if-end}
        \EndFor \label{line:for-end}
      \EndWhile \label{line:while-end}
      \State \textbf{return} $\pi$
    \EndFunction
  \end{algorithmic}
\end{algorithm}

\subsection{Safety Function \& Static Warnings}
Next, we present a way to use analysis results $\pi$ produced by the fixpoint algorithm to determine whether to accept or reject a given program. Our goal is to ensure that when we run the program, it will not get stuck; that is, for any state $\xi$ that the program
reaches, we want to ensure that either $\xi$ is a final state $\stat{E \cdot \mathsf{nil}}{\mu}$ or there is another state $\xi'$ such that $\xi \longrightarrow_p \xi'$. To do this, we define the safety function $\func{safe}\bb{\iota}(x) : \sett{Inst}' \times
\sett{Var} \to \sett{Abst}$, which returns the abstract value representing the set of ``safe'' values $x$ can take on before $\iota$ is executed. Figure~\ref{fig:safe} gives a few representative cases for $\func{safe}$, and in all the cases not shown $\func{safe}$ returns \ann{Nullable}. In particular, a procedure call's argument must adhere to the procedure's parameter annotation, a return value must adhere to its corresponding return annotation, and all field accesses must have non-null receivers. Therefore, the safety function guards against all undefined behavior.

\begin{figure}[]
  \centering
  \begin{align*}
    \func{safe}(\stmtCall{x}{m\texttt{@}a}{y\texttt{@}b}, y) & = b    \\
    \func{safe}(\stmtReturn{y\texttt{@}a}, y)        & = a    \\
    \func{safe}(\stmtAssign{x}{y.f}, y)           & = \ann{NonNull} \\
    \func{safe}(\stmtFieldAssign{x}{f}{y}, x)        & = \ann{NonNull}
  \end{align*}
  \caption{All nontrivial cases of the safety function.}
  \label{fig:safe}
\end{figure}

\subsubsection{Static Warnings}

\noindent Now, we can state the meaning of a valid program $p \in \sett{Prog}'$:
\[
  \text{for all}\quad
  \inst[v]{\iota} \in \sett{Vert}_p
  \qand
  x \in \sett{Var}
  ~.\quad
  \pi(v) = \sigma
  \quad\implies\quad
  \sigma(x) \sqsubseteq \func{safe}\bb{\iota}(x)
\]
\[
  \text{where} \quad \pi = \func{Kildall}(\func{flow}, \sqcup, p).
\]
That is, NPA emits static warnings when the fixpoint results disagree, according to the partial order $\sqsubseteq$, with the safety function. Also, we prove in Section \ref{sec:static-properties} that a valid program does not get stuck.

\subsection{Soundness of NPA} \label{sec:static-properties}
As discussed above, PICL's semantics are designed to get stuck when procedure annotations are violated or when null objects are dereferenced. Therefore, informally \emph{soundness} says that a valid program does not get stuck during execution. Formally, soundness is defined with progress and preservation statements. Before their statement we must first define the notion of valid states to complement our definition of valid programs:
\[
  \text{Let}~ p \in \sett{Prog}'. ~\text{A state}~ \xi =
  \stat{\fram{\rho_1}{v_1} \cdot \fram{\rho_2}{v_2} \cdots \fram{\rho_n}{v_n}
  \cdot \mathsf{nil}}{\mu} \in \sett{State}_p ~\text{is \emph{valid} if}
\]
\[
  \text{for all}\quad
  1 \leq i \leq n
  ~.\quad
  \predd{desc}(\rho_i, \pi(v_i))
  \quad\text{where}~ \pi = \func{Kildall}(\func{flow}, \sqcup, p).
\]
A state is \emph{valid} if it is described by the static analysis results $\pi$.

\begin{proposition}[static progress]\label{prop:static-progress}
  Let $p \in \sett{Prog}'$ be valid. If $\xi = \stat{E_1 \cdot E_2 \cdot S}{\mu} \in
    \sett{State}_p$ is valid then $\xi \longrightarrow_p \xi'$ for some $\xi' \in \sett{State}_p$.
\end{proposition}

\begin{proposition}[static preservation]\label{prop:static-preservation}
  Let $p \in \sett{Prog}'$ be valid. If $\xi \in \sett{State}_p$ is valid and $\xi
    \longrightarrow_p \xi'$ then $\xi'$ is valid.
\end{proposition}

\section{Gradual Null-Pointer Analysis}\label{sec:gradual}
In this section, we derive GNPA from NPA, presented previously (Sec. \ref{sec:static}). We proceed following the Abstracting Gradual Typing methodology introduced by Garcia \emph{et al.}~\cite{garcia2016abstracting} in the context of gradual type systems, adapting it to fit the concepts of static analysis.

We present the GNPA's lifted semilattice (Sec. \ref{sec:gradual-semilattice}), flow and safety functions (Sec. \ref{sec:gradual-flow-safety}), and fixpoint algorithm (Sec. \ref{sec:gradual-fixpoint}). We also discuss how static (Sec. \ref{sec:gradual-warnings}) and run-time warnings (Sec. \ref{sec:gradual-runtime}) are generated by the analysis. Finally, Section \ref{sec:gradual-properties} establishes the main properties of GNPA.

Note, here, annotations may be missing, so we extend our set of annotations with $\qm$: $\sett{Ann} = \{\ann{NonNull},~\ann{Nullable}\} \cup \{\qm\}$.

\subsection{Lifting the Semilattice} \label{sec:gradual-semilattice}

In this section, we lift the semilattice ($\sett{Abst}$, $\sqsubseteq$, $\sqcup$) (Sec. \ref{sec:static-semilattice}) by following the Abstracting Gradual Typing (AGT) framework \cite{garcia2016abstracting}. First, we extend the set of semilattice elements $\sett{Abst}$ to the new set $\Grad{\sett{Abst}} \supseteq \sett{Abst}$:
\[
 \Grad{\sett{Abst}} = \sett{Abst} \cup \{\qm\} \cup \set{\qm[a]}{a \in \sett{Abst}} =
\]
$$
 \{ \ann{Nullable},~ \ann{NonNull},~ \ann{Null},~ \qm,~ \qm[\ann{NonNull}],~ \qm[\ann{Null}] \}.
$$

Note that we equate the elements $\qm[\ann{Nullable}]$ and $\ann{Nullable}$ in $\Grad{\sett{Abst}}$. In Section \ref{sec:gradual-qmsemantics}, we give the semantics of the new lattice elements resulting in $\top = \qm[\ann{Nullable}] = \ann{Nullable}$. If $\sett{Abst}$ had a bottom element $\bot$, then $\bot = \qm[\bot]$ similarly.

The join $\sqcup$ and partial order $\sqsubseteq$ are also lifted to their respective counterparts $\mathbin{\Grad{\join}}$ (Sec. \ref{sec:gradual-join}) and $\mathrel{\Grad{\under}}$ (Sec. \ref{sec:gradual-under}). The resulting lifted semilattice $(\Grad{\sett{Abst}}, \mathbin{\Grad{\join}})$ with lifted relation $\mathrel{\Grad{\under}}$ underpins the optimism in GNPA.

\subsubsection{Giving Meaning to Missing Annotations} \label{sec:gradual-qmsemantics}
A straightforward way to handle $\qm$ would be to make it the top element $\qm = \top$ or the bottom element $\qm = \bot$ of NPA's semilattice. However, neither choice is sufficient for our goal:
\begin{itemize}
  \item If $\qm = \bot$, then $\qm \sqsubseteq a$ for all $a \in
    \sett{Abst}$ and $\func{conc}(\bot) = \varnothing$. As a result, if the return annotation of a procedure was $\qm$, then we could use the return value in any context without the analysis giving a warning. But, anytime an initialized variable is checked against the $\qm$ annotation, such as checking the non-null return value $y$ against the $\qm$ return annotation $\ann{NonNull} \sqsubseteq \qm$, the check will fail as $a \not \sqsubseteq \qm$ for all $a \in \sett{Abst} ~.~ a \neq \bot$.
  \item If we let $\qm = \top$ then we have $a \sqsubseteq \qm$ for all $a \in
    \sett{Abst}$. Therefore, we can pass any argument to a parameter annotated
    as $\qm$ without the static part of GNPA giving a warning. But, if the return
    annotation of that procedure is $\qm$, then the analysis will produce false positives in caller contexts wherever the return value is dereferenced. In other words, our analysis would operate exactly as \texttt{PolyNull} for the example in Fig. \ref{fig:java-safereverse}, which is not ideal.
\end{itemize}

Our goal is to construct an analysis system that does not produce false positive static warnings when a developer omits an annotation. To achieve this, we draw on work in gradual typing \cite{garcia2016abstracting}. We define the injective concretization function $\gamma
: \Grad{\sett{Abst}} \to \mathcal{P}^{+}(\sett{Abst})$ where $\Grad{\sett{Abst}} \supseteq \sett{Abst}$ is the lifted semilattice element set (Sec. \ref{sec:gradual-semilattice}):
\[
  \gamma(a) = \{a\}
  \qq{for}
  a \in \sett{Abst},
  \quad
  \gamma(\qm) = \sett{Abst},
  \qand  \gamma(\qm[a]) = \set{b \in \sett{Abst}}{a \sqsubseteq b}.
\]
An element in $\sett{Abst}$ is mapped to itself as it can only represent itself. In contrast, $\qm$ may represent any element in $\sett{Abst}$ at all times to support optimism in all possible contexts. Further, $\qm[a]$ means ``$a$ or anything more general than it,'' in contrast to a gradual formula $\phi \land \qm$ that means ``$\phi$ or anything more specific than it'' \cite{bader2018gradual}. As a result, $\qm[a]$ does not play the intuitive role of ``supplying missing information,'' as it would in gradual verification. Instead, $\qm[a]$ is simply an artifact of our construction, which is why the only element of $\sett{Ann} \setminus \sett{Abst}$ is $\qm$.

Then, if $\gamma(\Grad{a}) \subseteq \gamma(\Grad{b})$ for some $\Grad{a}, \Grad{b} \in \Grad{\sett{Abst}}$, we write $\Grad{a} \lesssim \Grad{b}$ and say that \emph{$\Grad{a}$ is more precise than $\Grad{b}$}. Further, $\iota_1 \lesssim \iota_2$ means that 1) the two instructions are equal except for their annotations, and 2) the annotations in $\iota_1$ are more precise than the corresponding annotations in $\iota_2$.

\subsubsection{Lifted Join $\mathbin{\Grad{\join}}$} \label{sec:gradual-join}

We begin by introducing a semilattice definition \cite{davey2002introduction}, which states that a semilattice is an algebraic structure $(S, \sqcup)$ where for all $x, y, z \in S$ the following hold:
\begin{itemize}
  \item $x \sqcup (y \sqcup z) = (x \sqcup y) \sqcup z$ (associativity)
  \item $x \sqcup y = y \sqcup x$ (commutativity)
  \item $x \sqcup x = x$ (idempotency)
\end{itemize}
Then, we write $x \sqsubseteq y$ when $x \sqcup y = y$ and it can be shown this $\sqsubseteq$ is a partial order. Recall that NPA uses $\sqcup$ in Algorithm~\ref{alg:kildall} to compute a fixpoint that describes the behavior of a program $p$. The fixpoint can only be reached when $\sqcup$ is idempotent. Similarly, $\sqcup$ must be commutative and associative so that program instructions can be analyzed in any order. Thus, our extended join operation $\mathbin{\Grad{\join}} : \Grad{\sett{Abst}} \times \Grad{\sett{Abst}} \to
\Grad{\sett{Abst}}$ must be associative, commutative, and idempotent making $(\Grad{\sett{Abst}}, \mathbin{\Grad{\join}})$ a join-semilattice.

To define such a function we turn to insights from gradual typing \cite{garcia2016abstracting}. We define an abstraction function $\alpha : \mathcal{P}^{+}(\sett{Abst}) \to
\Grad{\sett{Abst}}$, which forms a Galois connection with $\gamma$:
\[
  \alpha(\Coll{a})
  = \gamma^{-1}\qty(
        \bigcap_{\substack{
            \Grad{b} \in \Grad{\sett{Abst}} \\
            \gamma(\Grad{b}) \supseteq \Coll{a}
          }}
        \gamma(\Grad{b})
      )
\]
where, for $a \in \sett{Abst}$, $\gamma^{-1}$ is:
\begin{mathpar}
\gamma^{-1}(\{a\}) = a
\and
\gamma^{-1}(\sett{Abst}) = \qm
\and
\gamma^{-1}(\{b \in \sett{Abst} : a \sqsubseteq b \}) = \qm[a].
\end{mathpar}
Then we define the join of $\Grad{a}, \Grad{b} \in \Grad{\sett{Abst}}$ as follows:
\[
  \Grad{a} \mathbin{\Grad{\join}} \Grad{b}
  = \alpha(\set{a \sqcup b}{\text{
      $a \in \gamma(\Grad{a})$
      and $b \in \gamma(\Grad{b})$}
  })
\]
For example,
\begin{flalign}
\ann{NonNull} \mathbin{\Grad{\join}} \qm &= \alpha(\{ a \sqcup b : a \in \{\ann{NonNull}\} ~\text{and}~ b \in \sett{Abst} \}) \label{join-eq-alpha-start}\\
&= \alpha(\{ \ann{NonNull},~ \ann{Nullable} \}) \label{join-eq-alpha-set}\\
&= \gamma^{-1}\left( \gamma(\qm[\ann{NonNull}]) \cap \gamma(\qm) \right) \label{join-eq-intersect-gamma}\\
&= \gamma^{-1}\left( \{ \ann{NonNull},~ \ann{Nullable} \} \cap \sett{Abst} \right) \label{join-eq-intersect-sets}\\
&= \gamma^{-1}\left( \{ \ann{NonNull},~ \ann{Nullable} \} \right) \label{join-eq-intersect-result}\\
&= \qm[\ann{NonNull}] \label{join-eq-result}
\end{flalign}
That is, the join of all the $\sett{Abst}$ elements represented by $\ann{NonNull}$ and $\qm$ results in the set $\{\ann{NonNull},~ \ann{Nullable}\}$ (\ref{join-eq-alpha-start}, \ref{join-eq-alpha-set}). Applying $\alpha$ to this set is equivalent to applying $\gamma^{-1}$ to $\gamma(\qm[\ann{NonNull}]) \cap \gamma(\qm)$ (\ref{join-eq-intersect-gamma}); because, the only $\Grad{\sett{Abst}}$ elements that represent both $\ann{NonNull}$ and $\ann{Nullable}$ are $\qm[\ann{NonNull}]$ and $\qm$. The intersection of $\gamma(\qm[\ann{NonNull}])$ and $\gamma(\qm)$ is $\{\ann{NonNull},$ $\ann{Nullable}\}$ (\ref{join-eq-intersect-sets}, \ref{join-eq-intersect-result}), so we are really applying  $\gamma^{-1}$ to $\{\ann{NonNull},~ \ann{Nullable}\}$ (\ref{join-eq-intersect-result}). Therefore, $\ann{NonNull} \mathbin{\Grad{\join}} \qm = \qm[\ann{NonNull}]$ (\ref{join-eq-result}).
Notice, the intersection of the representative sets $\gamma(\qm[\ann{NonNull}])$ and $\gamma(\qm)$ of $\{\ann{NonNull},~\ann{Nullable}\} = \Coll{a}$ is used to find the most precise element in $\Grad{\sett{Abst}}$ that can represent $\Coll{a}$.

Now we return to the properties of $\mathbin{\Grad{\join}}$. Since $\sqcup$ is commutative, we have that $\mathbin{\Grad{\join}}$ is commutative. Idempotency is also not too onerous: it is equivalent to the condition that every element of $\Grad{\sett{Abst}}$ represents a subsemilattice of $\sett{Abst}$. That is, for every $\Grad{a} \in \Grad{\sett{Abst}}$ and $a_1, a_2 \in \gamma(\Grad{a})$, we must have $a_1 \sqcup a_2 \in \gamma(\Grad{a})$. This is true by construction. Associativity is tricky and motivates our complex definition of $\Grad{\sett{Abst}}$. Ideally, $\Grad{\sett{Abst}}$ would be defined simply as $\sett{Abst} \cup \{\qm\}$, however in this case $\mathbin{\Grad{\join}}$ is not associative:
  \begin{align*}
    \ann{Null} \mathbin{\Grad{\join}} (\ann{NonNull} \mathbin{\Grad{\join}} \qm)
     & = \ann{Null} \mathbin{\Grad{\join}} \qm \\
     & = \qm                                  \\
     & \neq \ann{Nullable}                              \\
     & = \ann{Nullable} \mathbin{\Grad{\join}} \qm \\
     & = (\ann{Null} \mathbin{\Grad{\join}} \ann{NonNull}) \mathbin{\Grad{\join}} \qm.
  \end{align*}
Fortunately, our definition of $\Grad{\sett{Abst}}$ which also includes the intermediate optimistic elements $\qm[\ann{NonNull}]$ and $\qm[\ann{Null}]$ results in an associative $\mathbin{\Grad{\join}}$ function and a finite-height semilattice $(\Grad{\sett{Abst}},~ \mathbin{\Grad{\join}})$. Figure~\ref{fig:semilattice-lifted} shows the semilattice structure induced by $\mathbin{\Grad{\join}}$.

\begin{figure}
  \centering
  \begin{tikzpicture}
    \node (t) {$\ann{Nullable}$};
    \node (aq) [below left = 0.5cm and -0.7cm of t] {$\qm[\ann{Null}]$};
    \node (bq) [below right = 0.5cm and -0.7cm of t] {$\qm[\ann{NonNull}]$};
    \node (q) [below right = 0.5cm and 0cm of aq] {$\qm$};
    \node (a) [below left = 0.5cm and -0.7cm of aq] {$\ann{Null}$};
    \node (b) [below right = 0.5cm and -1cm of bq] {$\ann{NonNull}$};

    \draw (t) -- (aq);
    \draw (t) -- (bq);
    \draw (aq) -- (a);
    \draw (aq) -- (q);
    \draw (bq) -- (q);
    \draw (bq) -- (b);
  \end{tikzpicture}
  \caption{The semilattice structure induced by the lifted join $\mathbin{\Grad{\join}}$. Specifically, this is the Hasse diagram of the partial order
    $\set{(\Grad{a}, \Grad{b})}{\Grad{a} \mathbin{\Grad{\join}} \Grad{b} = \Grad{b}}$.}
  \label{fig:semilattice-lifted}
\end{figure}

\subsubsection{Lifted Order $\mathrel{\Grad{\under}}$}\label{sec:gradual-under}

Now it is fairly straightforward to construct $\mathrel{\Grad{\under}}$. Recall, NPA emits static warnings when the fixpoint results disagree with the safety function, according to the partial order $\sqsubseteq$. The fixpoint results and the safety function now return elements in $\Grad{\sett{Abst}}$, so we lift $\sqsubseteq$ to $\mathrel{\Grad{\under}} ~\subseteq \Grad{\sett{Abst}} \times \Grad{\sett{Abst}}$ using the concretization function $\gamma$:
\[
  \Grad{a} \mathrel{\Grad{\under}} \Grad{b}
  \quad\iff\quad \exists ~.\quad
  a \in \gamma(\Grad{a})
  \qand
  b \in \gamma(\Grad{b})
  \qq{such that}
  a \sqsubseteq b
  \qq{for} \Grad{a}, \Grad{b} \in \Grad{\sett{Abst}}.
\]
Figure~\ref{fig:order} gives the lifted order relation $\mathrel{\Grad{\under}}$ in graphical form.

\begin{figure}[]
  \centering
  \begin{tikzpicture}[>=stealth]
    \graph[counterclockwise=6]{
      t/"$\top$";
      aq/"$\qm[A]$";
      a/"$A$";
      q/"$\qm$";
      b/"$B$";
      bq/"$\qm[B]$";

      aq -> t;
      a -> t;
      q -> t;
      b -> t;
      bq -> t;

      t -> aq;
      a -> aq;
      q -> aq;
      bq -> aq;

      aq -> a;
      q -> a;

      t -> q;
      aq -> q;
      a -> q;
      b -> q;
      bq -> q;

      q -> b;
      bq -> b;

      t -> bq;
      b -> bq;
      q -> bq;
      aq -> bq;

      a -> bq;
      b -> aq;
    };
  \end{tikzpicture}
  \caption{The lifted partial order, where each
    directed edge $\Grad{a} \to \Grad{b}$ means $\Grad{a} \mathrel{\Grad{\under}} \Grad{b}$.
    (Self-loops are omitted). Here, \ann{Nullable}{} is abbreviated $\top$, and \ann{Null}{} and
    \ann{NonNull}{} are abbreviated $A$ and $B$ respectively.}
  \label{fig:order}
\end{figure}

The $\Grad{\sqsubseteq}$ predicate is a maximally permissive version of the $\sqsubseteq$ predicate for $\qm[\ann{NonNull}]$, $\qm[\ann{Null}]$, and $\qm$. For example, $\qm \mathrel{\Grad{\under}} \ann{NonNull}$ since $\gamma(\qm) = \{\ann{NonNull},~ \ann{Null},~ \ann{Nullable}\}$, $\gamma(\ann{NonNull}) = \{\ann{NonNull}\}$, and $\ann{NonNull} \sqsubseteq \ann{NonNull}$. By similar reasoning, $\ann{NonNull} \mathrel{\Grad{\under}} \qm$. In fact, $\qm \mathrel{\Grad{\under}} a \mathrel{\Grad{\under}} \qm$, $\qm[\ann{NonNull}] \mathrel{\Grad{\under}} a \mathrel{\Grad{\under}} \qm[\ann{NonNull}]$, and $\qm[\ann{Null}] \mathrel{\Grad{\under}} a \mathrel{\Grad{\under}} \qm[\ann{Null}]$ for $a \in \sett{Abst}$. So, clearly $\mathrel{\Grad{\under}}$ is not a partial order. The $\mathrel{\Grad{\under}}$ predicate must be maximally permissive to support the optimism used in the \texttt{safeReverse} example from Figure \ref{fig:java-safereverse} (Sec. \ref{sec:action-falsepos}): calls to \texttt{safeReverse} with null and non-null arguments are valid and dereferences of its return values are also valid.
However, $\mathrel{\Grad{\under}}$ is the same as $\sqsubseteq$ when both of its arguments come from $\sett{Abst}$, \emph{e.g.}~ $\ann{NonNull} \mathrel{\Grad{\under}} \ann{Nullable}$ and $\ann{Nullable} \not \mathrel{\Grad{\under}} \ann{NonNull}$. This allows our gradual analysis to apply NPA where annotations are complete enough to support it.

\subsubsection{Properties}\label{subsec:semilattice-properties}
We previously mentioned some of the properties which ($\Grad{\sett{Abst}}$, $\mathbin{\Grad{\join}}$) satisfy. Here, we formally state them, and their proofs can be found in the appendix of the full version of this paper.

\begin{proposition}\label{prop:semilattice}
  $(\Grad{\sett{Abst}},~ \mathbin{\Grad{\join}})$ is a semilattice; in other words, $\mathbin{\Grad{\join}}$ is associative, idempotent, and commutative.
\end{proposition}

\begin{proposition}\label{prop:finite-height}
  If the height of $(\sett{Abst},~ \sqcup)$ is $n > 0$, then the height of
  $(\Grad{\sett{Abst}},~ \mathbin{\Grad{\join}})$ is $n + 1$ (in particular, $(\Grad{\sett{Abst}},~ \mathbin{\Grad{\join}})$ has finite height).
\end{proposition}

\subsection{Lifting the Flow \& Safety Functions} \label{sec:gradual-flow-safety}
Now both instructions and abstract states ($\Grad{\sigma} \in \Grad{\sett{Map}} = \sett{Var} \rightharpoonup \Grad{\sett{Abst}}$) may contain optimistic abstract values. Therefore, similar to lifting the join $\mathbin{\Grad{\join}}$, we follow the AGT \emph{consistent function lifting} approach \cite{garcia2016abstracting} when defining GNPA's
flow function $\Grad{\func{flow}} : \sett{Inst} \times \Grad{\sett{Map}} \to \Grad{\sett{Map}}$ for this new domain.

Specifically, for $\iota \in \sett{Inst}$ and
$\Grad{\sigma} = \set{x \mapsto \Grad{a}_x}{x \in \sett{Var}} \in \Grad{\sett{Map}}$, we
define
\begin{flalign*}
   & \Grad{\func{flow}}\bb{\stmtCall{z}{m\texttt{@}a}{y\texttt{@}b}}(\Grad{\sigma}) = \{x \mapsto \alpha(\{(\func{flow}\bb{\stmtCall{z}{m\texttt{@}a'}{y\texttt{@}b'}}(\sigma'))(x)
   \\
   & \hspace{135pt} : a' \in \gamma(a) \wedge b' \in \gamma(b) \wedge \sigma' \in \Sigma\}) :x \in \sett{Var}\} \\
   & \Grad{\func{flow}}\bb{\stmtProc{m\texttt{@}a}{y\texttt{@}b}}(\Grad{\sigma}) = \{x \mapsto \alpha(\{(\func{flow}\bb{\stmtProc{m\texttt{@}a'}{y\texttt{@}b'}}(\sigma'))(x)
   \\
   & \hspace{135pt} : a' \in \gamma(a) \wedge b' \in \gamma(b) \wedge \sigma' \in \Sigma\}) :x \in \sett{Var}\} \\
   & \Grad{\func{flow}}\bb{\iota}(\Grad{\sigma}) = \set{x \mapsto \alpha(\set{(\func{flow}\bb{\iota}(\sigma'))(x)}{\sigma' \in \Sigma})}{x \in \sett{Var}}
   \quad \text{otherwise}\\
   & \\
   & \text{where} \quad \Sigma = \set{\set{x \mapsto a_x}{x \in \sett{Var}}}{a_x \in \gamma(\Grad{a}_x)\text{ for all }x \in \sett{Var}}.
\end{flalign*}
Note that the procedure call and procedure entry instructions are the only instructions in $\func{flow}$'s domain that may contain $\qm$ annotations, so the corresponding $\func{flow}$ rules are lifted with respect to those annotations. Similarly, all rules are lifted with respect to their abstract states.

Recall that we defined the predicate $\predd{desc}$ on $\sett{Env} \times \sett{Map}$ to express the local soundness of $\func{flow}$. For $\Grad{\func{flow}}$, we lift $\predd{desc}$ to $\Grad{\predd{desc}}$ on $\sett{Env} \times \Grad{\sett{Map}}$ such that it is maximally permissive like the $\mathrel{\Grad{\under}}$ predicate:
\[
  \Grad{\predd{desc}}(\rho, \Grad{\sigma})
  \quad\iff\quad
  \predd{desc}(\rho, \sigma)\text{ for some }\sigma \in \Sigma
\]
\[
\text{where}~ \Sigma ~\text{is constructed in the same way as for}~ \Grad{\func{flow}}.
\]

\noindent Finally, we again follow the consistent function lifting methodology to construct $\Grad{\func{safe}} : \sett{Inst} \times \sett{Var} \to \Grad{\sett{Abst}}$ from $\func{safe} : \sett{Inst}' \times \sett{Var} \to \sett{Abst}$:
\begin{flalign*}
    & \Grad{\func{safe}}\bb{\stmtCall{z}{m\texttt{@}a}{y\texttt{@}b}}(x) = \alpha(\set{\func{safe}\bb{\stmtCall{z}{m\texttt{@}a'}{y\texttt{@}b'}}(x)}{a' \in \gamma(a) \wedge b' \in \gamma(b)})\\
    & \Grad{\func{safe}}\bb{\stmtProc{m\texttt{@}a}{y\texttt{@}b}}(x) = \alpha(\set{\func{safe}\bb{\stmtProc{m\texttt{@}a'}{y\texttt{@}b'}}(x)}{a' \in \gamma(a) \wedge b' \in \gamma(b)})\\
    & \Grad{\func{safe}}\bb{\stmtReturn{y\texttt{@}a}}(x) = \alpha(\set{\func{safe}\bb{\stmtReturn{y\texttt{@}a'}}(x)}{a' \in \gamma(a)})\\
    & \Grad{\func{safe}}\bb{\iota}(x) = \alpha(\func{safe}\bb{\iota}(x)) \quad \text{otherwise}
\end{flalign*}

Other than the casewise-defined $\func{flow}$ rules for $\land$ and $\lor$, the lifted $\Grad{\func{flow}}$ and $\Grad{\func{safe}}$ functions simplify down to the same computation rules as $\func{flow}$ and $\func{safe}$ as shown in Figure~\ref{fig:flow} and Figure~\ref{fig:safe} respectively, replacing $\func{flow}$ with $\Grad{\func{flow}}$ and $\func{safe}$ with $\Grad{\func{safe}}$.

\subsection{Lifting the Fixpoint Algorithm} \label{sec:gradual-fixpoint}
To lift the fixpoint algorithm, we simply plug $\Grad{\func{flow}}$ and
$\mathbin{\Grad{\join}}$ into Algorithm~\ref{alg:kildall} to compute $\Grad{\pi} =
\func{Kildall}(\Grad{\func{flow}}, \mathbin{\Grad{\join}}, p) : \sett{Vert}_p \to \Grad{\sett{Map}}$ for any $p \in \sett{Prog}$.

\subsection{Static Warnings} \label{sec:gradual-warnings}
Using the lifted safety function, we say that a partially-annotated program $p
\in \sett{Prog}$ is \emph{statically valid} if
\[
  \text{for all}\quad
  \inst[v]{\iota} \in \sett{Vert}_p
  \qand
  x \in \sett{Var}
  \qc
  \Grad{\pi}(v) = \Grad{\sigma}
  \quad\implies\quad
  \Grad{\sigma}(x) \mathrel{\Grad{\under}} \Grad{\func{safe}}\bb{\iota}(x)
\]
\[
  \text{where}~ \Grad{\pi} = \func{Kildall}(\Grad{\func{flow}}, \mathbin{\Grad{\join}}, p).
\]
Each piece of GNPA's static system ($(\Grad{\sett{Abst}}, \mathbin{\Grad{\join}})$, $\mathrel{\Grad{\under}}$, $\Grad{\func{flow}}$, $\Grad{\func{safe}}$, and the fixpoint algorithm) is designed to be maximally optimistic for missing annotations. Therefore, the resulting system will not produce false positive warnings due to missing annotations. The system is also designed to apply NPA where annotations are available to support it, so it will still warn about violations of procedure annotations or null object dereferences where possible. See Section \ref{sec:action-falsepos} for more information.

\subsection{Dynamic Checking} \label{sec:gradual-runtime}
GNPA's static system reduces false positive warnings at the cost of soundness. For example,  as in Section \ref{sec:action-falseneg}, the analysis may assume a variable with a $\qm$ annotation is non-null to satisfy an object dereference when the variable is actually null. In order to avoid false negatives and ensure that our gradual analysis is sound, we modify the semantics of PICL to insert run-time checks where the analysis may be unsound.
That is, if $p$ is \emph{statically valid} and there are program points $\inst[v]{\iota}$ such that
\[
  a \not\sqsubseteq \bigsqcup \gamma(\Grad{\func{safe}}\bb{\iota}(x))
  \qq{for some}
  x \in \sett{Var}
  \qand
  a \in \gamma((\Grad{\pi}(v))(x)),
\]
then a run-time check must be inserted at those points to ensure the value of $x$ is in $\func{conc}(\bigsqcup \gamma(\Grad{\func{safe}}\bb{\iota}(x)))$.

More precisely, we define a dedicated error state $\code{error}$ and expand the set
of run-time states to be $\Grad{\sett{State}}_p = \sett{State}_p \cup \{\code{error}\}$. Then
we define a restricted semantics $\mathrel{\Grad{\stepsto}}_p$ on $\Grad{\sett{State}}_p \times
\Grad{\sett{State}}_p$ as follows. Let $\xi \in \sett{State}_p$. If
\[
  \xi = \stat{\fram{\rho}{\inst{\iota}} \cdot S}{\mu}
  \qand
  \lnot\Grad{\predd{desc}}(\rho, \set{x \mapsto \Grad{\func{safe}}\bb{\iota}(x)}{x \in \sett{Var}})
\]
then $\xi \mathrel{\Grad{\stepsto}}_p \code{error}$. If there is some $\xi' \in \sett{State}_p$ such that $\xi \longrightarrow_p \xi'$, then $\xi \mathrel{\Grad{\stepsto}}_p \xi'$. Otherwise, there is no $\Grad{\xi}' \in \Grad{\sett{State}}_p$ such that $\xi \mathrel{\Grad{\stepsto}}_p \xi'$.

\subsection{Gradual Properties} \label{sec:gradual-properties}
GNPA is sound, \emph{conservative extension} of NPA---the static system is applied in full to programs with complete annotations, and adheres to the gradual guarantees inspired by Siek \emph{et al.}~\cite{siek2015refined}. The gradual guarantees ensure losing precision is harmless, \emph{i.e.}~ increasing the number of missing annotations in a program does not break its validity or reducibility.

To formally present each property, we first extend the notion of a valid state. Let $p \in \sett{Prog}$. A state $\xi = \stat{\fram{\rho_1}{v_1} \cdot \fram{\rho_2}{v_2} \cdots \fram{\rho_n}{v_n} \cdot \mathsf{nil}}{\mu} \in \sett{State}_p$ is valid if
\[
  \text{for all}\quad
  1 \leq i \leq n
  \qc
  \Grad{\predd{desc}}(\rho_i, \Grad{\pi}(v_i))
  \quad \text{where} \quad \Grad{\pi} = \func{Kildall}(\Grad{\func{flow}}, \mathbin{\Grad{\join}}, p).
\]
Then, for fully-annotated programs, GNPA and the modified semantics are conservative extensions of NPA and PICL's semantics, respectively.

\begin{proposition}[conservative static extension]\label{prop:conservative-static-extension}~\\
  If $p \in \sett{Prog}'$ then $\func{Kildall}(\func{flow}, \sqcup, p) =
    \func{Kildall}(\Grad{\func{flow}}, \mathbin{\Grad{\join}}, p)$.
\end{proposition}

\begin{proposition}[conservative dynamic extension]\label{prop:conservative-dynamic-extension}
  Let $p \in \sett{Prog}'$ be valid, and let $\xi_1, \xi_2 \in \sett{State}_p$. If $\xi_1$
  is valid then $\xi_1 \longrightarrow_p \xi_2$ if and only if $\xi_1 \mathrel{\Grad{\stepsto}}_p
    \xi_2$.
\end{proposition}

GNPA is sound, \emph{i.e.}~ valid programs will not get stuck during execution. However, programs may step to a dedicated \code{error}{} state when run-time checks fail. Soundness is stated with a progress and preservation argument.

\begin{proposition}[gradual progress]\label{prop:gradual-progress}
  Let $p \in \sett{Prog}$ be valid. If $\xi = \stat{E_1 \cdot E_2 \cdot S}{\mu} \in
  \sett{State}_p$ is valid then $\xi \mathrel{\Grad{\stepsto}}_p \Grad{\xi}'$ for some
  $\Grad{\xi}' \in \Grad{\sett{State}}_p$.
\end{proposition}

\begin{proposition}[gradual preservation]\label{prop:gradual-preservation}
  Let $p \in \sett{Prog}$ be valid. If $\xi \in \sett{State}_p$ is valid and $\xi
  \mathrel{\Grad{\stepsto}}_p \xi'$ for some $\xi' \in \sett{State}_p$, then $\xi'$ is valid.
\end{proposition}

Finally, GNPA satisfies both the static and dynamic gradual guarantees. Both of the guarantees rely on a definition of \emph{program precision}. Specifically, if programs $p_1$ and $p_2$ are identical except perhaps that some annotations in $p_2$ are $\qm$ where they are not $\qm$ in $p_1$, then we say that \emph{$p_1$ is more precise than $p_2$}, and write $p_1 \lesssim p_2$.

Then, the \emph{static gradual guarantee} states that increasing the number of missing annotations in a valid program does not introduce static warnings (\emph{i.e.}~ break program validity).

\begin{proposition}[static gradual guarantee]\label{prop:static-gradual-guarantee}
  Let $p_1, p_2 \in \sett{Prog}$ such that $p_1 \lesssim p_2$. If $p_1$ is
  statically valid then $p_2$ is statically valid.
\end{proposition}

The \emph{dynamic gradual guarantee} ensures that increasing the number of missing annotations in a program does not change the observable behavior of the program (\emph{i.e.}~ break program reducibility for valid programs).

\begin{proposition}[dynamic gradual guarantee]\label{prop:dynamic-gradual-guarantee}
  Let $p_1, p_2 \in \sett{Prog}$ be statically valid, where $p_1 \lesssim p_2$. Let
  $\xi_1, \xi_2 \in \sett{State}_{p_2}$. If $\xi_1 \mathrel{\Grad{\stepsto}}_{p_1} \xi_2$ then
  $\xi_1 \mathrel{\Grad{\stepsto}}_{p_2} \xi_2$.
\end{proposition}

Note, the small-step semantics $\mathrel{\Grad{\stepsto}}$ are designed to make the proofs of the aforementioned properties easier at the cost of easily implementable run-time checks. Therefore, we give the following proposition that connects a more implementable design to $\mathrel{\Grad{\stepsto}}$. That is, we can use the contrapositive of this proposition to implement more optimal run-time checks. Specifically, the na\"ive implementation would check each variable at each program point to make sure it satisfies the safety function for the instruction about to be executed. But Proposition~\ref{prop:static-progress} tells us that we only need to check variables at runtime when our analysis results don't already guarantee (statically) that they will satisfy the safety function.

\begin{proposition}[run-time checks]\label{prop:runtime-checks}
  Let $p \in \sett{Prog}$ be valid according to $\Grad{\pi} =
  \func{Kildall}(\Grad{\func{flow}}, \mathbin{\Grad{\join}}, p)$, and let $\xi =
  \stat{\fram{\rho}{\inst[v]{\iota}} \cdot S}{\mu} \in \sett{State}_p$ be valid. If
  $\xi \mathrel{\Grad{\stepsto}}_p \code{error}$ then there is some $x \in \sett{Var}$ and $a \in
  \gamma((\Grad{\pi}(v))(x))$ such that $a \not\sqsubseteq \bigsqcup
  \gamma(\Grad{\func{safe}}\bb{\iota}(x))$.
\end{proposition}

\section{Preliminary Empirical Evaluation}\label{sec:empirical}
In this section, we discuss the implementation of GNPA and two studies designed to evaluate its usefulness in practice. Preliminary evidence suggests that our analysis can be used at scale, produces fewer false positives than state-of-the-art tools, and eliminates on average more than half of the null-pointer checks Java automatically inserts at run time. These results illustrate an important practical difference between GNPA and other null-pointer analyses. While a sound static analysis can be used to prove the redundancy of run-time checks, and an unsound static analysis can be used to reduce the number of false positives, neither of those can do both at the same time. On the other hand, GNPA can both prove the redundancy of run-time checks and reduce reported false positives

\subsection{Research Questions}

We seek answers to the following questions:
\begin{enumerate}
  \item \label{q:prototype} Can a gradual null-pointer analysis be effectively implemented and used at scale?
  \item \label{q:false-positives} Does such a null-pointer analysis produce fewer false positives than industry-grade analyses?
  \item \label{q:eliminate-checks} Does the gradual null-pointer analysis perform significantly fewer null-pointer checks than the na\"ive approach of checking every dereference?
\end{enumerate}

\subsection{Prototype}

Facebook Infer provides a framework to construct static analyses that use abstract interpretation. We built a prototype of GNPA, called \emph{Graduator}, in this framework. Our prototype uses Infer's HIL intermediate language representation (IR). As a result, Graduator can be used to analyze code written in C, C++, Objective-C, and Java.

\begin{figure}
  \centering
  \begin{tikzpicture}
    \node (t) {$\ann{Nullable}$};
    \node (n) [below = of t] {$\ann{NonNull}$};

    \draw (t) -- (n);
  \end{tikzpicture}
  \qquad\qquad
  \begin{tikzpicture}[->,>=stealth']
    \node (t) {$\ann{Nullable}$};
    \node (q) [below right=0.5cm and 0.5cm of t] {$\qm$};
    \node (n) [below=1.35cm of t] {$\ann{NonNull}$};

    \draw (n) -> (q);
    \draw (n) -> (t);
    \draw (t) -> (q);
    \draw (q) -> (n);
    \draw (q) -> (t);
  \end{tikzpicture}
  \qquad\qquad
  \begin{tikzpicture}
    \graph[grid placement, wrap after=1]{
      t/"$\ann{Nullable}$" -- q/"$\qm$" -- n/"$\ann{NonNull}$";
    };
  \end{tikzpicture}
  \caption{\textit{Left:} The starting null-pointer semilattice for Graduator.
    \textit{Middle:} The lifted partial ordering, where each directed edge $\Grad{a} \to \Grad{b}$ means $\Grad{a} \mathrel{\Grad{\under}} \Grad{b}$. (Self-loops are omitted.) \textit{Right:} The semilattice structure induced by the lifted join $\mathbin{\Grad{\join}}$.}
  \label{fig:smaller-lattice}
\end{figure}

The preceding case study (Secs. \ref{sec:language}--\ref{sec:gradual}) uses a base semilattice with three elements, \ann{Null}, \ann{NonNull}, and \ann{Nullable}, in order to demonstrate that a semilattice lifting may contain additional intermediate optimistic elements, \qm[\ann{Null}] and \qm[\ann{NonNull}]. For simplicity, we implemented the semilattice from Figure \ref{fig:smaller-lattice}, along with its lifted variant, order relation and join function, in our prototype. This semilattice is the same as the base one in the case study except it does not contain \ann{Null}: the initial static semilattice has only \ann{NonNull}{} and \ann{Nullable}{}, and the gradual semilattice only adds one additional \qm{} element. There are a couple other differences between our formalism and our Graduator prototype, one of which is that Graduator allows field annotations while our formalism does not.

Infer does not support modifying Java source code, so Graduator simply reports the locations where it should insert run-time checks rather than inserting them directly. In fact, Graduator may output any of the following:
\begin{itemize}
  \item \texttt{GRADUAL\_STATIC}---a static warning.
  \item \texttt{GRADUAL\_CHECK}---a location to check a possibly-null
    dereference.
  \item \texttt{GRADUAL\_BOUNDARY}---another location to insert a check,
    such as passing an argument to a method, returning from a method, or assigning a value to a field.
\end{itemize}
Since Java checks for null-pointer dereferences automatically, soundness is preserved. A more complete implementation of GNPA would insert run-time checks as part of the build process. As a result, some bugs may be caught earlier when the gradual analysis inserts checks at method boundaries and field assignments.

By implementing Graduator with Infer's framework, Graduator is guaranteed to operate at scale. We also evaluate Graduator on a number of open source repositories as discussed in Sections \ref{sec:empirical-static} and \ref{sec:empirical-runtime}.
Thus, the answer to RQ\ref{q:prototype} is yes.

\subsection{Static Warnings} \label{sec:empirical-static}

\begin{figure}[]
  \centering
  \begin{tikzpicture}[scale=0.05]
    \draw (28.3598,-34.6431) circle (69 and 34.5);
    \draw (8.33837,-1.62742) circle (27 and 13.5);
    \draw (71.2821,-0.296814) circle (46 and 23.0);
    \draw (110,-50) circle (5 and 5);

    \node at (-60,-35.0) {Eradicate};
    \node at (-40,0.0) {Graduator};
    \node at (140,0.0) {NullSafe};
    \node at (135,-50) {\textsc{NullAway}};

    \node at (110,-50) {0};

    \node at (22,-40.0) {1229};
    \node at (3,3.5) {126};
    \node at (75,6.5) {474};

    \node at (29.5,3) {1};
    \node at (55,-12.5) {159};
    \node at (10,-7.5) {81};

    \node at (30.4,-3.5) {20};
  \end{tikzpicture}
  \caption{The total number of static warnings reported by the three Infer null
    checkers, for all 15 repositories.}
  \label{fig:venn}
\end{figure}

To evaluate Graduator, we ran it on 15 of the 18 open-source Java repositories used to evaluate \textsc{NullAway} \cite{banerjee2019nullaway} (we excluded 3 of the 18 repositories because we were unable to successfully run Infer on them). We also ran \textsc{NullAway}, and Infer's existing null-pointer checkers Eradicate and NullSafe, on the repositories. Figure~\ref{fig:venn} shows the number of \emph{static} warnings produced by each of these three checkers: 1489 for Eradicate, 654 for NullSafe, 228 for Graduator, and 0 for \textsc{NullAway}, for a total of 2371.

Based on the \textsc{NullAway} paper (in which Uber states that in practice they have found no instances of null-pointer dereferences caused by their tool's unsoundness), it seems reasonable to assume that these repositories do not have null-pointer bugs, since \textsc{NullAway} itself reports no static warnings for these repositories. After examining all 2371 warnings ourselves, we found that all but 57 (50 from Eradicate only, 2 from Graduator only, and 5 from Eradicate and Graduator but not NullSafe) were false positives due to systematic imprecision in the analysis tools. We were unable to determine whether the remaining 57 warnings represent actual bugs or not.

Under this assumption, Graduator reports significantly fewer false positives than Infer's existing null-pointer checkers (although in this respect, it is of course outperformed by \textsc{NullAway}) (RQ\ref{q:false-positives}).
An interesting aspect of Figure~\ref{fig:venn} is how many warnings are produced by only one of the checkers: 1229 for Eradicate, 474 for NullSafe, and 126 for Graduator. Many of these warnings arose from generated and test case code.

\subsubsection{Generated Code}

Several of the 15 repositories generate code as part of their build process, and in some cases, the analysis tools gave warnings about the generated code. This accounts for
\begin{itemize}
  \item 380 of the warnings given by NullSafe alone,
  \item 356 of the warnings given by Eradicate alone,
  \item 130 of the warnings given by both Eradicate and NullSafe but not
    Graduator, and
  \item 8 of the warnings given by Graduator alone.
\end{itemize}
Graduator reports significantly fewer static warnings for generated code, because such code is typically unannotated and Graduator is designed to be optimistic when annotations are missing.

\subsubsection{Test Code}

It is reasonable to assume that test code does not contain null dereference bugs, because if it did, then those bugs would show up when the tests are run. Static warnings about test code account for
\begin{itemize}
  \item 384 of the warnings given by Eradicate alone, and
  \item 73 of the warnings given by both Eradicate and Graduator, but not NullSafe.
\end{itemize}
That is, Graduator reports fewer warnings for test code than Eradicate, but more than NullSafe. The NullSafe checker does not appear to treat test code specially, so it is unclear why NullSafe is performing better than Graduator for such code.

\subsubsection{Remaining False Positives}

The reader may wonder why Graduator reports any false positives on this codebase, since it intuitively seems that the static portion of a gradual analysis ought to be optimistic.  Examining the warnings given by Graduator, we see that none of the warnings are due to treating missing annotations pessimistically; instead, they are due to places where the analysis has whatever annotations it needs, but the analysis is imprecise in other respects.  For example, one common source of false positives is when a field is checked for null, then is read again.  Our original static analysis is limited in that it does not treat fields flow-sensitively, causing false positives that are independent of the choice to be gradual or not with respect to annotations.

\textsc{NullAway} avoids giving false positives on this same codebase, due to a combination of some unsound assumptions and a more precise analysis approach.  While our approach for deriving gradual program analyses focuses on retaining soundness through a combination of static and dynamic checks, incorporating more precise analysis techniques (e.g. a flow-sensitive treatment of fields, perhaps in combination with a gradual alias analysis) could eliminate more of these false positives.  In the meantime, our comparison to Eradicate and NullSafe is appropriate as these are the static analysis tools taking the most similar approach.

\subsection{Run-time Checks} \label{sec:empirical-runtime}

\begin{table}
  \caption{Percentage of null-dereference checks which Graduator found to be
    redundant.}
  \begin{small}
    \begin{tabular}{lrrr}
      repository & dereference sites & eliminated checks & percent eliminated \\
      \hline
      keyvaluestore & 419 & 156 & 37\% \\
      uLeak & 620 & 241 & 39\% \\
      butterknife & 2773 & 1129 & 41\% \\
      jib & 5896 & 2499 & 42\% \\
      skaffold-tools-for-java & 366 & 185 & 51\% \\
      picasso & 2719 & 1458 & 54\% \\
      meal-planner & 858 & 475 & 55\% \\
      caffeine & 9455 & 5701 & 60\% \\
      AutoDispose & 3218 & 1993 & 62\% \\
      ColdSnap & 6360 & 4325 & 68\% \\
      ReactiveNetwork & 2097 & 1626 & 78\% \\
      okbuck & 19089 & 15130 & 79\% \\
      FloatingActionButtonSpeedDial & 3049 & 2581 & 85\% \\
      QRContact & 1272 & 1171 & 92\% \\
      OANDAFX & 2216 & 2056 & 93\% \\
      \hline
      overall & 60407 & 40726 & 67\%
    \end{tabular}
  \end{small}
  \label{tab:dereferences}
\end{table}

For the same set of 15 repositories analyzed by \textsc{NullAway}, we performed another experiment using our prototype. We configured Graduator to ignore \emph{all} annotations, so in effect, every field, argument, and return value was annotated as \qm. For each repository, we counted all the locations where Graduator gave a \texttt{GRADUAL\_STATIC}, \texttt{GRADUAL\_CHECK}, or \texttt{GRADUAL\_BOUNDARY} warning, and compared that number to the total number of pointer dereferences in the code. By ignoring annotations, we ensured that each of these warnings appeared on dereferences, rather than allowing early checks at, e.g., method boundaries. We also ran analogous experiments with annotations enabled, but the number of run-time check warnings found were very similar to the numbers found with annotations disabled.

Table~\ref{tab:dereferences} shows what percentage of these dereference sites received no static warnings or run-time checks. Recall that Java automatically checks all dereferences to ensure that they are not null. Because GNPA is sound, this figure shows the percentage of null checks that are provably redundant, and could be safely removed by an ahead-of-time compiler.

Since we were able to eliminate an average of $67\%$ of the null checks which Java automatically inserts, this experiment suggests the answer to RQ\ref{q:eliminate-checks} is yes. Note that these numbers only discuss the number of dereferences that appear in the code, and do not take into account which of these dereferences are executed more or less frequently at run-time.

This also illustrates an important practical difference between GNPA and other null-pointer analyses. While a sound static analysis can be used to prove the redundancy of run-time checks, and an unsound static analysis can be used to reduce the number of false positives, neither of those can do both at the same time. On the other hand, a gradual analysis can both prove the redundancy of run-time checks and reduce reported false positives.

\section{Related Work}\label{sec:related}

As discussed previously, our work builds on prior research in gradual typing: the criteria for gradual type systems~\cite{siek2015refined} and the Abstracting Gradual Typing methodology, which develops a gradual type system from a purely static one~\cite{garcia2016abstracting}. In contrast to prior work in gradual typing, we address the challenges of tracking transitive dataflow relationships, rather than the local checks of typical type systems. In doing so, we gradualize, for the first time, the abstract interpretation of a program~\cite{cousot:popl1977}, and the canonical dataflow analysis fix-point algorithm~\cite{kildall1973unified}.

The most closely related work in program analysis consists of \textit{hybrid analyses}, which combine static and dynamic analysis techniques to counteract the weaknesses inherent to each approach. For example, Choi \emph{et al.}~\cite{10.1145/512529.512560} used a static analysis to substantially lower the run-time overhead of a dynamic data race analysis. Prior work on hybrid program analyses combines static and dynamic techniques in ad-hoc ways. Instead, we propose a principled methodology for deriving a hybrid (gradual) analysis from a static one, and show that the resulting analysis adheres to desirable properties such as soundness and the gradual guarantee.

There is a large body of literature on static program analysis, including multiple specialized conferences. Our work opens the door to gradual versions of them. Previously, we discussed existing null-pointer analysis tools~\cite{FacebookInfer}, \cite{banerjee2019nullaway} and frameworks~\cite{papi2008practical}, and how GNPA is an improvement over them. Notably, our prototype is implemented in Infer's framework~\cite{FacebookInfer}.

The Granullar type system \cite{brotherston2017granullar} and the Blame for Null calculus\cite{blameForNull} are gradual type systems for nullness, and thus solve a related problem to GNPA.
The main difference in our work is that we use dataflow analysis instead of typing.
This results in a significantly different user experience, as a full static specification within a gradual type system typically requires many more types to be specified (e.g. on all local variables) compared to a dataflow analysis, where for example we do not require (or even allow) nullity annotations on local variables.
Basing our work on dataflow analysis also has a major impact on the technical development, requiring the novel lattice-based gradualization framework described in this paper rather than the well-known type-based gradualization approaches used in Granullar and Blame for Null.
Blame for Null also investigates the notion of blame, which we leave for future work in the program analysis setting.

Contract checking~\cite{eiffelBook, findlerFelleisen:icfp2002} can be used to check properties like nullness. Building on the idea of hybrid type checking~\cite{knowles2010hybrid}, Xu \emph{et al.}~\cite{xu2012hybrid} explored how to check contracts using a hybrid of static and dynamic analysis.  Their work was specialized to the context of logical assertions, whereas we are in the area of lattice-based program analyses.  It is also unclear whether their approach conforms to the gradual guarantee.

O'Hearn \emph{et al.}~\cite{o2019incorrectness} proposed Incorrectness Logic as a means of proving that a program has a bug, rather than proving it correct.  This is consistent with our goal of reducing false positives, but it stays in the realm of static reasoning, and therefore gives up soundness.  In contrast, we reduce false positives without giving up soundness by adding run-time checks.

\section{Conclusion}\label{sec:conclusion}
This paper is the first work on gradual program analysis. We introduced a framework which transforms abstract interpretation based static analyses relying on annotations into gradual ones. Gradual analyses handle missing annotations specially, allowing them to smoothly leverage both static and dynamic techniques. Static information is used where possible and dynamic information where necessary to reduce false positives while preserving soundness. Such analyses are also \emph{conservative extensions} of their underlying static analyses and adhere to \emph{gradual guarantees}, which state that losing precision is harmless. When presenting our framework, we developed a gradual null-pointer analysis, GNPA, with the previously mentioned properties that reduces false positives compared to some popular existing tools.

Importantly, the gradual framework can be applied as described to any abstract interpretation based static analysis under the following restrictions. The analysis should support annotations, have a finite-height semilattice, a monotonic, locally-sound flow function, a safety function, and operate on a first-order, procedural, imperative programming language. Additionally, checking membership in the semilattice should be decidable. Thus, initial followup work could include gradual taint analysis, to which our framework immediately applies. Finally, we do not support widening, but we do support context-sensitivity. In the future, we plan to explore extensions of our framework for infinite-height semilattices and widening; this would allow gradualization of other analyses, such as interval analysis. Still further work could include, for instance, pointer analyses, which do not have analogues in the field of gradual typing.

On the empirical side, there are further research questions to be answered: How often does a gradual analysis catch bugs statically versus how often does it catch them at run time? Is performance lost or gained when run time checks are inserted earlier via annotations rather than just-in-time? Finally, a gradual analysis will still report false positives anywhere its base static analysis is utilized and reports false positives. As a result, we plan to explore the aforementioned research questions, including the trade-off between gradual analyses reducing false positives and being conservative extensions of underlying static analyses.