Brief overview of where things are in Polonius related to the Borrow Checker

[lancejpollard]

Hi there,

I am excited to find the blog post and this repo which seems to have an implementation of the borrow-checker which I'm eager to learn about. I would like to see exactly how the borrow checker works.

But looking through all of the files in this repo (there's only a few), I didn't see anything which seemed like it would do actual CFG generation from the source code, or typechecking, or borrowchecking. I'm not sure if I missed it or what, but was wondering if you might be able to explain where things are and where to start tracing the code to find where the borrow checker is implemented in the nitty gritty details.

I'm looking for code sort of like this in the repo, but not finding anything.

Thank you so much, looking forward to your response!

Lance

[amandasystems]

Hi Lance!

I'm afraid it's a bit more complicated than that. While Polonius implements a borrow check, it does not currently implement the full one, and it doesn't really analyse Rust code (or MIR). Rather, it operates on a set of inputs (we call them facts) derived from the MIR ("variable x defined here", "variable x used here", etc). Those we have a small pseudo-language to express, but for real Rust programs, fact generation happens in the Rust compiler, and is currently spread out across a number of modules, making it hard to follow. I've been meaning to clean that up but haven't been able to yet. In other words, if you were looking in this repository, you didn't miss it.

That said, we do have some sketches for formal, Prolog/Datalog-style rules defining the borrow check (or rather, the Polonius version of it), though I wouldn't call them gritty and they aren't the current implementation. If you like, I can also send you my master's thesis, which covers some details, though not all of the grit.

The others may be able to get you better answers! I've been out of the loop for a while now.

[lqd]

As Albin mentioned, polonius (specifically the polonius-engine crate) is made to be integrated within rustc, and therefore all of the work not directly related to the analyses is done there instead: polonius computes its analyses on data structures given by rustc (or this repo's tests), the datalog facts Albin mentioned.

All the work to parse rust code into HIR/THIR, do the typechecking, MIR generation, and so on until these facts are generated will be in the rust repository, and I believe you would find a lot of interesting information about what happens before polonius in the rustc dev guide.

Those facts are the inputs to polonius, their definition is here, are mostly documented in the link Albin gave, with a lot of additions in this unmerged PR, and are used in polonius' main entry point here.

The entry point from where rustc calls into polonius is specifically here in the NLL module, and everything upstream from that will be interesting to trace to understand the code. It will be a bit bottom up but should at least give you all the landmarks from which to start your investigation.

Something which is also interesting is that fact generation in rustc is using the session profiler, so it's another landmark to see the code immediately preceding polonius: it will be contained in the profiled scopes named polonius_fact_generation (like this search query shows). Just as an example on how to work your way back into rustc to find the information you're looking for: you mentioned the CFG, it is currently modeled as the cfg_edge relation and will be filled by rustc's polonius fact generation here from the MIR's Locations. Everything upstream from that will lead you to MIR generation and ultimately to parsing.

[lancejpollard]

@albins yes I would love to see your masters thesis!

Thank you all for the info, it helps a lot. I will dig into some of these links you have shared. Thank you.