Add CFG for NLL reject correct

thesis/1-introduction.tex

@@ -507,7 +507,7 @@ Different approaches to borrow checking only differ in determining when $L$ is l
 
 \subsubsection{Classic \ac{NLL}}
 
-Under \ac{NLL} the liveness of a loan is derived from the lifetime of a reference. As discussed in \autoref{subsec:non-lexical-lifetimes}, a reference is live in a node of the \ac{CFG} if it may be used later. The corresponding loan is live exactly when the reference is live. \todo{lifetime subtyping and inferred lifetimes/constraints} Crucially, if a function returns a reference, it is live for the whole body of the function. \autoref{lst:nll-reject-correct} shows an example. In the \inline{Some} branch, the reference returned by \inline{v.first()} is in turn returned from the function, meaning it must be live at least until the end of the function body. But in the \inline{None} branch, an exclusive reference is needed to push a value to the vector. This should not be a problem since the shared reference from \inline{v.first()} is not used in this branch, and a different reference is returned from the function instead. However, \ac{NLL} can’t accomodate this situation because it \emph{may} be used later, see \autoref{fig:cfg-nll-reject-correct}.
+Under \ac{NLL} the liveness of a loan is derived from the lifetime of a reference. As discussed in \autoref{subsec:non-lexical-lifetimes}, a reference is live in a node of the \ac{CFG} if it may be used later. The corresponding loan is live exactly when the reference is live. \todo{lifetime subtyping and inferred lifetimes/constraints} Crucially, if a function returns a reference, it is live for the whole body of the function. \autoref{lst:nll-reject-correct} shows an example. In the \inline{Some} branch, the reference returned by \inline{v.first()} is in turn returned from the function, meaning it must be live at least until the end of the function body. But in the \inline{None} branch, an exclusive reference is needed to push a value to the vector. This should not be a problem since the shared reference from \inline{v.first()} is not used in this branch, and a different reference is returned from the function instead. However, \ac{NLL} can’t accomodate this situation because it \emph{may} be used later, see \autoref{fig:cfg-nll-reject-correct}.\todo{Is this correct? I think maybe the problem lies with \inline{x}. But the borrow checker is not angry about it.}
 
 \begin{lstlisting}[language=Rust, caption={\ac{NLL} reject correct program}, label={lst:nll-reject-correct}]
 fn first_or_insert(v: &mut Vec<i32>) -> &i32 {
@@ -522,17 +522,19 @@ fn first_or_insert(v: &mut Vec<i32>) -> &i32 {
     \centering
     \begin{tikzpicture}
         \begin{scope}[every node/.style={draw, rectangle}]
-            \node {TODO};
-            % \node (A) at (0,4.5) {\inline{let mut x = 0;}};
-            % \node[ultra thick] (B) at (0,3) {\inline{let xref = &x;}};
-            % \node[ultra thick] (C) at (0,1.5) {\inline{println!("\{xref\}");}};
-            % \node (D) at (0,0) {\inline{x += 1;}};
+            \node[ultra thick] (A) at (0,5) {\inline{match v.first()}};
+            \node[ultra thick] (B) at (-1,2.75) {\inline{x}};
+            \node[ultra thick, draw=red] (C) at (1,3.5) {\inline{v.push(1);}};
+            \node[ultra thick] (D) at (1,2) {\inline{&v[0]}};
+            \node[ultra thick] (E) at (0,0.5) {\inline{return}};
         \end{scope}
-        % \path [->] (A) edge node[left] {} (B);
-        % \path [->, ultra thick] (B) edge node[left] {} (C);
-        % \path [->] (C) edge node[left] {} (D);
+        \path [->, ultra thick] (A) edge node[left] {} (B);
+        \path [->, ultra thick] (A) edge node[left] {} (C);
+        \path [->, ultra thick] (C) edge node[left] {} (D);
+        \path [->, ultra thick] (B) edge node[left] {} (E);
+        \path [->, ultra thick] (D) edge node[left] {} (E);
     \end{tikzpicture}
-    \caption{Control-flow diagram for \autoref{lst:nll-reject-correct}, nodes in which the reference returned by \inline{v.first()} is live are marked with a thick border.}
+    \caption{Control-flow diagram for \autoref{lst:nll-reject-correct}.}
     \label{fig:cfg-nll-reject-correct}
 \end{figure}
 
@@ -540,6 +542,8 @@ fn first_or_insert(v: &mut Vec<i32>) -> &i32 {
 
 When creating a reference, it gets an associated \emph{region} (\emph{origin} in Polonius), which is part of its type. (What is a region?) A loan is live if some live variable has it in its type.
 
+\todo[inline]{Write up nicely the stuff below}
+
 \begin{enumerate}
     \item Borrow checking in Polonius:
           \begin{enumerate}