本文阐述了到 Rust 2024 版本将 Polonius 稳定化的路线图。它确定了一些高级里程碑,总结了关键目标以及最近的进展。
Polonius 背景
Polonius 指代几样东西。它是借用检查器的一种新表述。它也是一个特定项目,实现了基于 Datalog 的分析。我们目前的计划不使用基于 Datalog 的实现,而是利用在实现中学到的东西,专注于在 rustc 内部重新实现 Polonius。
Polonius 的动机示例是所谓的“问题案例 #3:跨函数的条件控制流”:这里是指从函数内部的条件分支返回一个引用。
// v
在 Some
分支中返回可变引用 value
要求对 map
的可变借用一直存活到函数结束。这会阻止在 None
分支中的修改,尽管在 None
分支中本来就不会存在对 map
的可变借用。
解决这个借用检查器问题需要对流敏感性有更高的精度。它也暗示了我们在生命周期建模方面的局限性,这在控制流稍复杂一些的情况下表现得更明显,例如issue #47680
;
当前的借用检查器拒绝此代码。这是因为它看到存在对 temp
的借用来调用 temp.maybe_next()
。它还看到这个借用可以在循环中流动 —— 特别是,借用被 v
引用,然后 v
被存储到 temp
中。因此,当我们在循环顶部试图可变借用 temp
时,它会报告错误,因为可能存在来自先前迭代的借用。
然而,仔细阅读发现,虽然借用可能在循环中流动,但这仅发生在 Some
分支上,并且在该分支上 temp
被覆盖了。这意味着我们在下一次迭代中借用的 temp
实际上与我们在上一次迭代中借用的位置不同。同时,在 None
分支上,借用结束了。
这种“逐案”区分——看到流只发生在一个分支上,并且在该分支上存在重新赋值——需要比当前借用检查器更高的精度。
因此,“NLL 问题案例 #3”、issue #47680 等问题被从 NLL 推迟,留作未来的工作,即 Polonius。
关键思想在于
- 从将 生命周期 建模为 CFG 中的点集(具有 outlives 关系)转变为将 来源 建模为借用集(具有 subset 关系)。
- 在控制流图 (Control Flow Graph) 的每个点计算并跟踪子集关系(而现有借用检查器计算的是单一子类型关系)。
里程碑
这是一个粗略的路线图,我们在最初的步骤上拥有最高的可见度
- 每个步骤都有未知因素,将决定后续步骤需要完成哪些工作
- 因此,我们更多地讨论长期路线图的里程碑,以及短期内的具体任务。
以下是路线图的里程碑
1. 从主路径中剥离高阶问题
如今,trait 求解器生成高阶 outlives 约束,由借用检查器来求解。未来,我们希望由下一代 trait 求解器自行负责求解这些高阶约束,以便它只生成 Polonius 中使用的更简单的 subset
约束。这将使我们能够求解诸如 for<T> { if (T: 'a, 'a: 'b) { T: 'b } }
之类的蕴含谓词,而无需再次有效地复制相同的 trait 求解逻辑。这篇博文更详细地描述了该问题和可能的解决方案。
短期内,我们正在探索重构借用检查器,将高阶处理与普通处理分离。目标是在一种 Polonius “泄漏检查”中预处理 outlives 约束,我们可以在其中计算高阶错误。一旦 trait 求解器能够求解这些约束,这部分就可以移除。
当前状态:⏳ 类型团队成员将在未来几天开始这项任务。
2. 范围内的位置不敏感借用
在 Polonius 和现有借用检查器的两个关键区别(将区域视为“借用集”,以及在 CFG 的每个点计算子类型关系)中,这一步旨在解决*第一个*区别,而非第二个,因此我们称之为“范围内的位置*不*敏感借用”(因为子类型检查只进行一次,而不是针对每个位置):这个想法可以描述为“基于 Polonius 模型的 NLL”。
请注意,现有借用检查器的其他方面仍然是流敏感的。
在这一步中,我们将仅通过 outlives 约束来计算存活借用的集合,而不是计算区域在 CFG 中存活的点(后者用于计算借用何时超出范围)。我们认为这在报告错误方面与现有借用检查器是等效的。
重要的是,这一改变为增加位置敏感性铺平了道路(借用集也是未来改进借用检查器(如安全的内部引用)的更好基础)。
当前状态:✅ 我们已完成原型,并有一个开放的 PR 将此功能置于 -Z
标志下合并,这将在近期发生。
3. 验证整个测试套件在使用位置不敏感 Polonius 时通过
该 PR 确实通过了我们套件中的全部 15000 多个测试,但我们尚未通过 crater 运行检查 crates.io 上发布的 crate。
与我们的内部测试套件相比,绝大多数已发布的 crate 预计会构建成功而没有错误。在这方面,不太可能在那里发现问题,但无论如何都会进行检查。
当前状态:⏳ 进行中,crater 运行将在 PR 合并前完成。
4. 使用位置不敏感 Polonius 替换借用检查器的部分功能
该原型只执行附加工作,不修改现有的分析。
在这一步中,我们将重构借用检查器,使其数据结构存储借用集,并进行更多性能工作:例如,移除冗余计算,研究最坏情况下的可伸缩性和常数因子。
预计性能将相似,然后我们可以考虑在不使用功能标志的情况下启用位置不敏感的通道,并移除一些旧代码。
为了保留多年来众多贡献者努力带来的高质量诊断信息,可能会在新分析运行并检测到错误时,才使用现有的分析和诊断。
当前状态:我们已经对所需的数据结构更改、可以移除的一些冗余部分等进行了早期调查。
5. 在 nightly 版本上进行位置敏感通道
然后,整合位置敏感性(这更难高效实现)的工作就可以开始了。这一步将实现分析的第一个版本。
此时它可能仍然效率不高,并且需要使用功能标志,但这正是借用检查器应该接受比当前 NLL 更具表达力的代码的时候。
当前状态:我们正处于设计阶段,将我们的 Datalog 原型和算法适配到 rustc 中,构想沿 CFG 计算和传播子集约束的替代方法。
6. 在 a-mir-formality 中建模借用检查和 Polonius
类型团队正在构建 Rust MIR 和 trait 系统的模型,称为 a-mir-formality
。一旦它达到足够完整的状态,目标是在新语言特性稳定化之前,总是扩展该模型来覆盖它们。因此,我们正在努力将 Polonius 添加到模型中。这将是第二次进行此类建模,因为我们已经将 Polonius 添加到 a-mir-formality 的先前版本中。事实上,正是这项建模工作为我们提供了洞察力,从而实现了目前正在 nightly 版本中合并的位置不敏感 Polonius 表述。
有趣的是,这项工作完全独立于 rustc,理论上可以很快启动,并与其他工作并行进行。
7. 位置敏感通道稳定化
在此里程碑中,我们预计会有大量的优化和产品化工作。
如果预计会再次遇到与 2018 版本中 NLL 类似的体验,那么还需要大量工作和完善来处理诊断差异和问题,确保错误和附注足够清晰,以及完善文档。
此时,希望位置敏感通道已经足够高效,经过实践测试,一定程度上经过形式化验证,并可以在 2024 版本中启用。
大约在这个时候,也可以重启库化工作,将树内 Polonius 变成一个库,可能使用Stable MIR。这样它就可以在其他地方被重用,例如在rust-analyzer或gccrs中,或者被研究验证工具(如kani、prusti和creusot)的研究人员使用。
结论
我们非常高兴看到 Polonius 的计划日益清晰。目前,由于我们仍在进行基础性工作,暂不寻求志愿者或贡献者,除非他们非常熟悉编译器。我们确实期望随着项目的进展,对新贡献的需求会越来越多。敬请关注更新!