@@ -92,7 +92,7 @@ A \emph{region}\footnote{Polonius calls regions \emph{origins}, which is a more
...
@@ -92,7 +92,7 @@ A \emph{region}\footnote{Polonius calls regions \emph{origins}, which is a more
Now, a loan $L$ is live at some node $N$, if there is some variable which is live at $N$ and contains $L$ in its region. This difference means that different paths through the \ac{CFG} are independent from each other, because a node in one path can’t see a node in the other one by walking back the \ac{CFG}.
Now, a loan $L$ is live at some node $N$, if there is some variable which is live at $N$ and contains $L$ in its region. This difference means that different paths through the \ac{CFG} are independent from each other, because a node in one path can’t see a node in the other one by walking back the \ac{CFG}.
Let’s look at the example from \autoref{lst:nll-reject-correct} with all regions made explicit. \lstinline~x'{L1, L2}~ denotes that expression \inline{x} has a region consisting of the two loans \inline{L1} and \inline{L2}.
Let’s look at the example from \autoref{lst:nll-reject-correct} with all regions made explicit. \inline{x'{L1, L2}} denotes that expression \inline{x} has a region consisting of the two loans \inline{L1} and \inline{L2}.
\begin{listing}[H]
\begin{listing}[H]
\begin{minted}{rust}
\begin{minted}{rust}
...
@@ -110,9 +110,9 @@ Let’s look at the example from \autoref{lst:nll-reject-correct} with all regio
...
@@ -110,9 +110,9 @@ Let’s look at the example from \autoref{lst:nll-reject-correct} with all regio
\label{lst:regions}
\label{lst:regions}
\end{listing}
\end{listing}
In \autoref{lst:regions} we can see that there are four relevant loans: \inline{L0} is the loan of the reference we got passed in. All references depend on it. \inline{first} creates a reference with loan \inline{L1} that is returned in the \inline{Some} branch, \inline{push} implicitly reborrows to push a value onto \inline{*v}. The final reference is created by the index operation and it may also be returned. Therefore, the return value has a region \lstinline~'{L0, L1, L2}~, because those three loans are what it may depend on.
In \autoref{lst:regions} we can see that there are four relevant loans: \inline{L0} is the loan of the reference we got passed in. All references depend on it. \inline{first} creates a reference with loan \inline{L1} that is returned in the \inline{Some} branch, \inline{push} implicitly reborrows to push a value onto \inline{*v}. The final reference is created by the index operation and it may also be returned. Therefore, the return value has a region \inline{'{L0, L1, L2}}, because those three loans are what it may depend on.
Under \ac{NLL}, the \inline{push} was not possible because \inline{x} being live and depending on \inline{fst} meant that \inline{fst} was live. With Polonius, we must check if there is any live variable that has a nonempty intersection with \lstinline~'{L0, L2}~. \inline{fst} and \inline{x} are not live, so they don’t pose a problem, even if the regions overlap. \inline{v} is live and there is a region overlap, but since the compiler inserts a reborrow, it is not a problem. There could still be an error if the borrow stack were invalidated at a later point, but since Polonius is only looking backwards, this is not something we have to consider here. There are no more live variables, so the node passes the borrow check.
Under \ac{NLL}, the \inline{push} was not possible because \inline{x} being live and depending on \inline{fst} meant that \inline{fst} was live. With Polonius, we must check if there is any live variable that has a nonempty intersection with \inline~{'{L0, L2}}. \inline{fst} and \inline{x} are not live, so they don’t pose a problem, even if the regions overlap. \inline{v} is live and there is a region overlap, but since the compiler inserts a reborrow, it is not a problem. There could still be an error if the borrow stack were invalidated at a later point, but since Polonius is only looking backwards, this is not something we have to consider here. There are no more live variables, so the node passes the borrow check.