如何使用非词法生命周期在程序中进行形式化推理

Question

考虑以下 Rust 程序：

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

它能够编译通过，我同意这种行为。

问题是当我试图正式地推理时，我无法得出相同的结论:

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

上述形式化推理有什么问题，正确推理应该如何进行?

- Supremum

Answer 1

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

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

它们不会。在第7行重新分配了 r，这就结束了整个过程，因为此后的 r 是一个完全独立于旧值的全新值 - 是的，rustc 足够聪明以处理那种粒度，这就是为什么如果你移除最后的 x; 它会警告：

未读取赋给 r 的值

在第7行（而如果你使用 Go，则不会收到该警告，编译器不会以那么低的粒度工作）。

Rustc 因此可以推断出 'b 的最小必要长度停止于第5行结束和第7行开始之间的某个位置。

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

如果您删除赋值操作，'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在span中变为死亡状态（而不是活动状态）。即使变量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

- Masklinn

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

但请记住，在 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

以下代码是无效的，因为在r被赋值之后，在使用r之前，x已经被改变了：

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;

- Daniel