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

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 足够聪明，可以在那个粒度上工作，这就是为什么如果你删除最后的 x;它会警告说

value assigned to r is never read

在第 7 行(例如，使用 Go 不会收到该警告，但编译器无法在那么低的粒度下工作)。
因此，Rustc 可以推断出 'b 的最小必要长度。在第 5 行的结尾和第 7 行的开头之间的某个位置停止。
自 x不需要在第8行之前更新，没有冲突。
但是，如果您删除分配，'b现在必须扩展到封闭函数的最后一行，从而引发冲突。
您的推理似乎是词法生命周期的推理，而不是 NLL。您可能想通过 RFC 2094 ，讲的很详细。但本质上，它适用于值(value)的活力约束，并解决这些约束。事实上，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.

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

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