借债分析——位置无关规则（Location Insensitive）

写于2022年2月19日。

位置无关规则在原始规则的基础上，忽略推导过程中的位置信息及具体的借用源信息，可快速检测函数中是否有潜在错误。仅当有潜在错误时，再详细地作位置相关分析得出具体的错误信息。在源程序本身正确的情况下，牺牲位置精度以提升借用检查速度，将有益于改善编译时间。

推导

输入借用源（Origin）的包含关系

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

相比原始规则，去掉了位置信息，因此也无需在CFG上传播。

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

计算借债的存活情况

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

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

3. 和原始规则一样，外部借用源视为存活

placeholder_loan(Origin, Loan) :-
    placeholder(Origin, Loan).

origin_contains_loan_on_entry(Origin, Loan) :-
    placeholder_loan(Origin, Loan).

4. 类似于原始规则，将借债关联借用源的信息，按借用源的包含关系传播

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

由于忽略了位置关系，因此无需再在CFG中传播。但相应地，由于缺乏借用清除（loan_killed_at）信息，因此借债的存活范围将被扩大。

计算潜在错误

5. 近似的借债存活情况

对于某个借债而言，若其关联到任何一个在此处存活的借用源，那么该借债视为存活。与原始规则不同，借债与借用源的关联是位置无关的，因此可能放大关联关系。

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

与原始规则一样，当借债在某处既存活又失效时，视为错误。由于放大了借债与借用源的关联关系，所以只能是「潜在错误」，须经过详细的位置相关分析才能得出准确的错误信息。

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

6. 计算潜在的借用源包含错误

与原始规则不同，由于借用源包含关系是位置无关的，因此不能用其精确判定包含关系是否有误。于是反其道而行之，首先推断借债关联了哪些外部借用源，这个关联关系是精确的（因为外部借用源是位置无关的）。

known_contains(Origin, Loan) :-
    placeholder(Origin, Loan).
known_contains(Origin, Loan) :-
    known_contains(SubOrigin, Loan),
    known_placeholder_subset(SubOrigin, Origin).

相应地，若从外部推导出的借债关联借用源的信息，与事先推得的信息比较，矛盾者视为错误。同样，由于推导出的内部借债关联借用源的信息是不精确的，所以也只能是「潜在错误」，须经过详细的位置相关分析才能得出准确的错误信息。

potential_subset_errors(SubOrigin, Origin) :-
    placeholder(SubOrigin, Loan),
    placeholder_origin(Origin),
    origin_contains_loan_on_entry(Origin, Loan),
    !known_contains(Origin, Loan).

思考

1. 为什么无需按`subset`的传递性传递其包含关系？

此处的subset是位置无关的，若按其传递性传递（即相当于无条件按CFG传播），将可能出现完全错误的包含关系（联系原始规则中subset按CFG传播的前提是借用源在该位置处存活）。

另一方面，在规则4中，借债关联借用源的信息也已按subset传播，实际上对origin_contains_loan_on_entry而言，也相当于按subset的传递性传递的效果。

况且，此处按subset的传递性传播，是与具体借债相关的（只有关联到同一借债的借用源，才会被按subset的传递性传递）。所以同样是放大了潜在错误，相比无条件按CFG传播，按借债相关的传播的放大范围无疑更小一些。

Rust中文博客