如何正式推理使用非词法生命周期的程序

Question

考虑以下 rust 程序：

fn main()
{
    let mut x = 1;
    let mut r = &x;
    r;
    let y = 1;
    r = &y;
    x = 2;
    r;
}

它编译没有任何错误，我同意这种行为。

问题是我在尝试正式推理时无法得出相同的结论：

变量 r 的类型是 &'a i32 一段时间 'a。
&x 的类型是 &'b i32 一段时间 'b。
生命周期 'a 包括 x = 2;。
从 let mut r = &x; 我们知道 'b: 'a.
因为3和4我们知道生命周期'b包括x = 2;.
因为2和5我们在做x = 2;的同时借用了x，所以程序应该是无效的。

上面的形式推理有什么问题，正确的推理是怎样的？

Answer 1

The lifetime 'a includes x = 2;.

Because of 3 and 4 we know that the lifetime 'b includes x = 2;.

他们没有。 r 被重新分配给第 7 行，这结束了整个事情，因为 r 此后是一个独立于旧值的全新值——是的 rustc is足够聪明，可以在那个粒度上工作，这就是为什么如果你删除最后的 x; 它会警告

value assigned to r is never read

在第 7 行（例如，使用 Go 时您不会收到该警告，编译器不会在那么低的粒度下工作）。

Rustc 因此可以推断 'b 的最小必要长度在第 5 行末尾和第 7 行开头之间的某处停止。

由于x第8行之前不需要更新，所以不存在冲突。

但是，如果删除分配，'b 现在必须扩展到封闭函数的最后一行，从而引发冲突。

您的推理似乎是词法生命周期的推理，而不是 NLL。您可能想要浏览 RFC 2094，它非常详细。但本质上，它根据值的 活性约束 并解决这些约束。事实上，RFC 通过一个示例介绍了活性，该示例是您的情况的更复杂版本：

let mut foo: T = ...;
let mut bar: T = ...;
let mut p: &'p T = &foo;
// `p` is live here: its value may be used on the next line.
if condition {
    // `p` is live here: its value will be used on the next line.
    print(*p);
    // `p` is DEAD here: its value will not be used.
    p = &bar;
    // `p` is live here: its value will be used later.
}
// `p` is live here: its value may be used on the next line.
print(*p);
// `p` is DEAD here: its value will not be used.

另请注意这句话，它非常适用于您的误解：

The key point is that p becomes dead (not live) in the span before it is reassigned. This is true even though the variable p will be used again, because the value that is in p will not be used.

所以你真的需要根据值而不是变量来推理。在头脑中使用 SSA 可能会有所帮助。

将此应用于您的版本：

let mut x = 1;
let mut r = &x;
// `r` is live here: its value will be used on the next line
r;
// `r` is DEAD here: its value will never be used
let y = 1;
r = &y;
// `r` is live here: its value will be used later
x = 2;
r;
// `r` is DEAD here: the scope ends

Answer 2

NLL 之前的生活

在讨论非词法生命周期（NLL）之前，让我们先讨论一下“普通”生命周期。在引入 NLL 之前的旧版 Rust 中，下面的代码将无法编译，因为 r 仍在范围内，而 x 在第 3 行中发生了变化。

let mut x = 1;
let mut r = &x;
x = 2; // Compile error

要解决此问题，我们需要在 x 发生突变之前明确地使 r 超出范围：

let mut x = 1;
{
    let mut r = &x;
}
x = 2;

此时你可能会想：如果在x = 2行之后，r行不再被使用，那么第一个片段应该是安全的。编译器是否可以更智能，以便我们不需要像在第二个代码段中那样显式地使 r 超出范围？

答案是肯定的，这就是 NLL 的用武之地。

NLL 后的生活

在 Rust 中引入 NLL 后，我们的生活变得更加轻松。下面的代码将编译：

let mut x = 1;
let mut r = &x;
x = 2; // Compiles under NLL

但是记住，只要r在x的mutation之后没有被使用，它就会编译。例如，即使在 NLL 下也不会编译：

let mut x = 1;
let mut r = &x;
x = 2; // Compile error: cannot assign to `x` because it is borrowed
r;     //                borrow later used here

虽然RFC 2094中描述的NLL的规则比较复杂，但是可以粗略地（在大多数情况下）概括为：

A program is valid as long as every owned value is not mutated between the assignment of a variable referring to it and the usage of that variable.

下面的代码是有效的，因为 x 在 before r 和 before r 的用法：

let mut x = 1;
x = 2;          // x is mutated
let mut r = &x; // r is assigned here
r;              // r is used here

下面的代码是有效的，因为 x 在 r 和的分配之后发生了变异r 的用法：

let mut x = 1;
let mut r = &x; // r is assigned here
r;              // r is used here
x = 2;          // x is mutated

下面的代码无效，因为 x 在 r 和之前的赋值之后发生了变异r:

的用法

let mut x = 1;
let mut r = &x; // r is assigned here
x = 2;          // x is mutated
r;              // r is used here      -> compile error

对于您的特定程序，它是有效的，因为当 x 发生变异时 (x = 2)，不再有引用 x 的变量——r 现在引用到 y 因为上一行 (r = &y)。因此，仍然遵守规则。

let mut x = 1;
let mut r = &x;
r;
let y = 1;

r = &y;

// This mutation of x is seemingly sandwiched between
// the assignment of r above and the usage of r below,
// but it's okay as r is now referring to y and not x
x = 2;

r;

如何正式推理使用非词法生命周期的程序

How to reason formally about programs using non lexical lifetimes

rust

borrow-checker

NLL 之前的生活

NLL 后的生活