原子式与输入

写于2022年1月21日。

原子式(Atom)

原子式即分析过程中用到的输入信息的分类。

Variable

由用户定义的变量。如let x, y;中的xy

Path

结构体、元组、数组等变量的字段访问路径。如a.bx.y.z.0s[0]等(数组不区分不同下标)。

Point

控制流图(Control-flow Graph,CFG)中的某个语句。每条语句被拆成Start和Mid两个节点,

  • Start:执行该语句前;
  • Mid:执行该语句时。

Loan

借债,对应Rust中的借用(borrow)概念。如let y = &x;中的&x

Origin

借用源,对应Rust中的生存期(lifetime)概念。如let x: &'a i32;中的'a

Origin应理解为「所有引用到该OriginLoan集合」。

输入事实(AllFacts

输入来源于MIR。主要包含CFG的执行到达关系图;变量的赋值、移动、访问情况;借债的发生、清除、失效信息;因借用产生、或外部定义的笁存期及其约束条件等信息。

cfg_edge

cfg_edge(SourcePoint, TargetPoint),一条控制流图的边,表示SourcePoint的下一条执行点为TargetPoint

loan_issued_at

loan_issued_at(Origin, Loan, Point)表示在位置Point处发生了借债Loan,其生存期为Origin

placeholder(与universal_region

placeholder(Origin, Loan)表示外部定义的生存期(如fn max<'a>(a: &'a str, b: &'a str) -> &'a str中的'a,及期关联的Loan。这些生存期也是函数签名的一部份。另外,由于它的Loan对借债检查而言是未知的,不能作任何假设,因此称之为「占位符」(placeholder)。

universal_region(Origin)placeholder类似,单指由函数签名定义的生存期,不带具体的Loan

loan_killed_at

loan_killed_at(Loan, Point)指某个借债Loan在位置Point处被清除。表明该借债Loan对应的路径PathPoint处被赋值或覆写。

例如


#![allow(unused)]
fn main() {
let mut a = 1;
let mut b = 2;
let mut q = &mut a;
let r = &mut *q; // `Loan` L0,此处借用了`*q`
// `q` 不能再使用,只能通过`r`访问
q = &mut b; // L0被清除
// 此后,`q`与`r`可以继续使用
}

q再次赋值后,Loan L0 被清除。Rustc在进入借用检查之前会将这样的关系计算好,保存在loan_killed_at中。之后,在借债分析时,loan_killed_at中的Point将阻止相应的Loan在CFG中传播。

subset_base

subset_base(SubOrigin, Origin, Point)表示,在位置Point处,有一条SubOrigin: Origin的约束(即SubOrigin应当长存于(outlives)Origin

loan_invalidated_at

loan_invalidated_at(Point, Loan)表明在Point处失效。

借用有共享(shared)与可变(mutable)两种。共享借用只能用于读取,不能写入或修改;可变借用必须独占,保证不能有对同一Path的借用。否则,视为借用失效,失效的借债将保存在loan_invalidated_at关系中。

known_placeholder_subset

known_placeholder_subset(SubOrigin, Origin)用于表示函数签名处定义的生存期约束。