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

反向思考借用检查的新方法
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` 使用前使其失效。编译器检测到这种不匹配并报告编译错误，从而防止释放后使用。

Verdagon 在 verdagon.dev 上分享了一篇 Hacker News 帖子，标题为“一种逆向思考借用检查的新方式”。作者描述通过大量手动探索发展这一想法，从编译期代际引用出发，最终得到逆向方法。在评论中，另一位用户称赞作者的手写写作风格；作者回应说，有思想的人类写作有助于让互联网保持人类连接的场所，而非机器中介的噪声。该帖子在捕获时有 15 分和 3 条评论，同时包含标准 HN 导航和 YC 申请通知。

原文

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)