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

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 通过一个例子介绍了 liveness，这是你的情况的一个更复杂的版本：

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将再次使用该变量也是如此，因为不会使用in 中的值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