借债分析——原始规则(Naive)

写于2022年2月8日。最后更新于2022年2月10日。

推导

输入、传递、传播借用源(Origin)的包含关系

1. 从MIR输入借用源的包含关系

subset(SubOrigin, Origin, Point) :-
    subset_base(SubOrigin, Origin, Point).

2. 按其传递性传递包含关系

subset(SubOrigin, SuperOrigin, Point) :-
    subset(SubOrigin, Origin, Point),
    subset(Origin, SuperOrigin, Point).

3. 在借用源存活的情况下,沿CFG传播其包含关系。

subset(SubOrigin, Origin, TargetPoint) :-
    subset(SubOrigin, Origin, SourcePoint),
    cfg_edge(SourcePoint, TargetPoint),
    origin_live_on_entry(SubOrigin, TargetPoint),
    origin_live_on_entry(Origin, TargetPoint).

计算借债(Loan)的存活情况

对每一个借债,先找出其关联的借用源(即包含该借债的借用源)。

  • 从借债发生处开始,先关联借债发生处的借用源,对应规则4;
  • 然后凡借债关联了某借用源,也必将关联其父借用源(即更「短命」的借用源),对应规则5;
  • 再沿CFG边,传播该借债关联的所有借用源,直到借债清除时,不应关联清除的借用源,对应规则6;

最后,只要借债在某处关联了任意一个存活的借用源,则视为借债在该处存活。

4. 从MIR中输入借债发生的信息,作为借债关联借用源存活信息的输入

origin_contains_loan_on_entry(Origin, Loan, Point) :-
    loan_issued_at(Origin, Loan, Point).

5. 将借债关联借用源的信息,按借用源的包含关系传播

注意:当借债关联了子借用源(SubOrigin,即更「长命」的借用源)时,子借用源的所有父借用源(Origin,即更「短命」的借用源)也都被关联;反之不成立。

origin_contains_loan_on_entry(Origin, Loan, Point) :-
    origin_contains_loan_on_entry(SubOrigin, Loan, Point),
    subset(SubOrigin, Origin, Point).

6. 将借债关联借用源的信息按CFG传播

传播条件为:借债关联的借用源不能在当前点被清除,且须在下一位置处存活(外部声明的生命周期始终视为存活)。

placeholder_origin(Origin) :-
    placeholder(Origin, _Loan).
origin_contains_loan_on_entry(Origin, Loan, TargetPoint) :-
    origin_contains_loan_on_entry(Origin, Loan, SourcePoint),
    !loan_killed_at(Loan, SourcePoint),
    cfg_edge(SourcePoint, TargetPoint),
    (origin_live_on_entry(Origin, TargetPoint); placeholder_origin(Origin)).

7. 借债关联的任一借用源存活时,都视为借债存活

loan_live_at(Loan, Point) :-
    origin_contains_loan_on_entry(Origin, Loan, Point),
    (origin_live_on_entry(Origin, Point); placeholder_origin(Origin)).

找出借债、借用源包含关系中存在的矛盾,用以报告语法错误

8. 当借债在某处既存活又失效时,视为错误

errors(Loan, Point) :-
    loan_invalidated_at(Loan, Point),
    loan_live_at(Loan, Point).

9. 当借用源在任意位置处存在与外部生命周期约束不一致的包含关系时,视为错误

subset_error(SubOrigin, Origin, Point) :-
    subset(SubOrigin, Origin, Point),
    placeholder_origin(SubOrigin),
    placeholder_origin(Origin),
    !known_placeholder_subset(SubOrigin, Origin).

思考

1. 为什么借债关联了某借用源,也必将关联其父借用源(更「短命」),而不是子借用源(更「长命」)?

fn main() {
let mut a: u32 = 1;
let b: &u32 = &a; // loan_issued_at(L0, 'a, P0)
//     ^      ^--- 'a
//     |--- subset_base('a, 'b),即'a: 'b
}

如上述代码所示,由load_issued_at(L0, 'a, P0)可得origin_contains_loan_on_entry(L0, 'a, P0)。联系借用源Origin的定义——所有引用到该Origin的Loan集合,可得'a为集合{L0}。那么根据规则5,应当推导出'b也包含集合{L0}。而'b包含L0也即意味着只要'b存活,L0就存活。

反过来,若'b不包含集合{L0},将意味着当L0不存活时,'b仍然有可能存活。回到代码中,要使L0不存活,只须修改a的值即可;而此时,由于'b仍然可能存活,即不可变引用的引用对象在其存活期间被修改,这必然不符合Rust的借用规则。

因此,'b必须包含L0,其他任意短命于'a的借用源亦如此。所以有规则5的:当借债关联了某借用源时,也必将关联更短命的父借用源。