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

Question

考虑以下 rust 程序：

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

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

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

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

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

Answer 1

生命周期'a 包括x = 2;。

由于 3 和 4，我们知道生命周期 'b 包括 x = 2;。

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

分配给r 的值永远不会被读取

在第 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.

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

关键是p 在重新分配之前在跨度中变为死亡（不活跃）。即使变量p 将被再次使用也是如此，因为p 中的值 将不会被使用。

所以你真的需要推理出价值，而不是变量。在您的脑海中使用 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不再使用，那么第一个sn-p应该是安全的。编译器能否更智能，这样我们就不需要像在第二个 sn-p 中那样显式地使 r 超出范围？

答案是肯定的，那就是 NLL 出现的时候。

NLL 之后的生活

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

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

但请记住，只要x 突变后不使用r，它就会编译。例如，即使在 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规则相当复杂，但可以粗略地（在大多数情况下）概括为：

只要每个拥有的值在引用它的变量的赋值和该变量的使用之间没有发生突变，程序就是有效的。

下面的代码是有效的，因为x在r的赋值之前在和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;