反向思考借用检查的新方法

反向思考借用检查的新方法
A new way to think about borrow checking (in reverse)

原始链接: https://verdagon.dev/blog/reverse-borrow-checking

第四阶段通过反向扫描检查释放后使用，跟踪三个事件：USE、MUTATE 和 DECLARE。扫描从函数末尾向上移动时，它维护一个待处理变量列表，这些变量稍后会被使用且必须保持有效。USE 将变量加入待处理列表；MUTATE 检查没有待处理变量被失效；DECLARE 将变量从待处理列表中移除。在示例中，`buff` 指向 `e.buffs[0]`，然后 `e.add_buff()` 修改了 `e`，这在 `buff` 使用前使其失效。编译器检测到这种不匹配并报告编译错误，从而防止释放后使用。

一篇 Hacker News 帖子链接到一篇文章，提出一种新的反向借用检查方法，该方法是在探索编译期代际引用之后开发的。作者 verdagon 描述了一个艰难的过程，并希望这个想法能站住脚。评论称赞工程实现，并推测 Rust 为何使用生命周期。讨论涉及语言设计权衡、人体工程学约束与语法导向算法、分组借用和失效标注。一位评论者将反向推理与 Hoare 风格验证进行比较，但警告编译器性能和回溯问题。其他人提到优化可能性、Vine 的逆运算符，以及对手写内容的赞赏。总体而言，该帖子讨论了一种实验性的借用检查替代方案及其对语言设计的潜在影响。

原文

Phase 4: Safety Checking

This post is half for fun, but also to ask for feedback on the algorithm. I don't think anyone's done it this way before, and there might be a good reason for that. If you see any problems with this approach, please help me out by leaving a comment, so I can fix (or scrap!) the approach. 8

Now we can use everything Phase 3 calculated!

This is the phase that checks for use-after-free.

It does it with a backwards scan, as was foretold.

Let's see it happen in a slightly bigger example:

struct Entity { hp int; buffs []int; }
func add_buff(self &Entity mut) {  }

func foo(e &Entity mut) {
  let buff = &e.buffs[0];
  e.add_buff();
  print_int(buff);
}

This program is doing a use after free, and we want the compiler to complain.

First, I'll desugar it into a more explicit syntax:

struct Entity { hp int; buffs []int; }
func add_buff<g'>(self &Entity in g) mut(g) {  }

func foo<g'>(e &Entity in g) mut(g) {
  let buff = &e.buffs[0];
  e.add_buff();
  print_int(buff);
}

Now I'm going to add in some comments, all determined by the backwards scan as it goes.

Further below, I'll explain what "DECLARE", "USE", and "MUTATE" mean.

struct Entity { hp int; buffs []int; }
func add_buff<g'>(self &Entity in g) mut(g) {  }

func foo<g'>(
  e &Entity in g          
) mut(g) {
  let buff = &e.buffs[0]; 
  e.add_buff();           
                          
  print_int(buff);        
}

The algorithm walks in reverse, from the end of the function to the start.

As it scans upward, it looks for these events:

When we USE a variable, add it to the pending list.
When we MUTATE anything, ensure no variables in pending are invalidated.
When we DECLARE a variable, remove it from the pending list.

pending contains all of the things USEd below, that we hope to see DECLAREd above.

We hope to never see a MUTATE to anything pending.

I think the best way to think of this is that pending contains all variables that will be used at some point below/later in the function, and therefore should be valid until then.

To really understand it, let's see it in action.

First, we look at the last line:

This is a USE, so we add it to the pending list. pending now has:

Now, still going backwards, we encounter the line above it:

We see the MUTATE so we ensure no variables in pending are invalidated.

Specifically, we'll ensure that nothing in pending is pointing at anything under e.

buff (group g.buffs[]) ... This matches! Show a compile error.

Here's what just happened: buff was pointing at g.buffs[], which starts with the g we just mutated with add_buff. That means that buff is invalidated above the line where it's used, which is a use-after-free.

So the compiler shows an error here. Huzzah!

反向思考借用检查的新方法 A new way to think about borrow checking (in reverse)

Phase 4: Safety Checking

反向思考借用检查的新方法
A new way to think about borrow checking (in reverse)