A new way to think about borrow checking (in reverse)

Phase 4: Safety Checking

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          // DECLARE e (group g)
) mut(g) {
  let buff = &e.buffs[0]; // DECLARE buff (group g.buffs[])
  e.add_buff();           // USE e (group g)
                          // MUTATE group g
  print_int(buff);        // USE buff (group g.buffs[])
}

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.

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

First, we look at the last line:

  print_int(buff);        // USE buff (group g.buffs[])

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

• buff (group g.buffs[])

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

  e.add_buff();           // USE e (group g)
                          // MUTATE group g

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!