Stream: t-compiler/rust-analyzer

Topic: Program slicing in RA


Will Crichton (Feb 27 2021 at 00:42, on Zulip):

Hi everyone. I'm Will, a CS PhD student at Stanford. My research is about using psychological principles to improve programming tools.

I'm interested in building a program slicer for Rust integrated into rust-analyzer. The core concept is that you could click a variable and query for the set of operations that are needed to compute the variable. A simple conservative analysis would be to include any code that mutably borrows that variable.

In order to implement this strategy, I need access to borrow information. But from my understanding, RA doesn't implement borrow checking, only type checking. Would I need to fully reimplement the Rust borrow checker to get borrow information? Or put another way, is my only choice to build a separate plugin against rustc_private that could somehow be invoked by RA?

Laurențiu (Feb 27 2021 at 05:47, on Zulip):

I'm probably missing something, but do you actually need borrow checking? Mutable borrows are already expressed in the type system and for a correct program you don't need the borrow checker to evaluate it

matklad (Feb 27 2021 at 09:19, on Zulip):

Yeah, I don't think you need full borrow checker here

matklad (Feb 27 2021 at 09:19, on Zulip):

though, you might need control flow analysis, which we don't have either

matklad (Feb 27 2021 at 09:20, on Zulip):

You might want to take a look at how we decide if we should underline the variable during highlighting: https://github.com/rust-analyzer/rust-analyzer/blob/master/crates/ide/src/syntax_highlighting/highlight.rs#L333-L335

matklad (Feb 27 2021 at 09:20, on Zulip):

The first approximation of a program slice would be the set of all expressions, where the variable is underined

matklad (Feb 27 2021 at 09:22, on Zulip):

image.png

matklad (Feb 27 2021 at 09:23, on Zulip):

(we actually need to improme that to not underline the varible when it is used immutably)

Will Crichton (Feb 27 2021 at 14:53, on Zulip):

@Laurențiu Nicola I think you need some kind of borrow information. Here's a simple example:

let mut x = 1;
let w = &mut x;
*w = 2;
println!("{}", x);

A program slicer needs to know that line 3 affects the value of x. Or at least, that w has a mutable borrow on x, and so mutations to w could affect x.

Right now, it's possible in RA to find all references to a variable. So I can identify that x is used on line 2. But the fact that w mutably borrows x is not computed.

@matklad can you explain when the highlighting you linked is activated? Can't seem to get underlining to appear in my own IDE. Nevermind, it's because I was using a different theme :-) the underlining doesn't seem to show up on Solarized Light.

matklad (Feb 27 2021 at 15:10, on Zulip):

@Will Crichton the IDE needs support for "semantic tokens" LSP feature, and the color scheme needs to have support for mutable token kind

matklad (Feb 27 2021 at 15:11, on Zulip):

ah, I see now, that's a good example! Yeah, at the moment rust-analyzer can only say: "hey, in line let w = &mut x, you are going to mutate x". It won't be able to infer that *w = 2 is a specific mutation to x

matklad (Feb 27 2021 at 15:12, on Zulip):

So yeah, if you need that level of precision, you either need to add borrow checker to rust-analyzer, or to build on top of rustc

Laurențiu (Feb 27 2021 at 15:13, on Zulip):

What about mutating values through Rc?

Will Crichton (Feb 27 2021 at 15:13, on Zulip):

@matklad Are there any features in RA that do round-trips to rustc? It's ok for now if the slicing takes a few seconds to run. I'm thinking that adding borrow checks to RA is probably too much for me right now.

@Laurențiu Nicola this analysis would definitely not be complete, ie won't work with interior mutability.

matklad (Feb 27 2021 at 15:14, on Zulip):

No, not really, we are by design avoid calling into rustc

Will Crichton (Feb 27 2021 at 15:15, on Zulip):

: ' ( alright, well I'll shelve this idea for now and just implement a standalone analysis.

Laurențiu (Feb 27 2021 at 15:16, on Zulip):

Would polonius help with this?

Will Crichton (Feb 27 2021 at 15:18, on Zulip):

Hmm possibly. If I could drop-in a borrow checker and just implement the initial fact generation, that seems like less works. Great point, I will check it out.

Laurențiu (Feb 27 2021 at 15:19, on Zulip):

But I don't think it's seen much work lately

detrumi (Feb 27 2021 at 15:19, on Zulip):

I don't think Polonius is complete enough to be useful here

Will Crichton (Feb 27 2021 at 15:21, on Zulip):

I will add -- as a research project, my initial goal is not to build the most robust program slicer possible. Rather, I want to find situations in everyday Rust development that would benefit from slicing. So long as the tool works for a few key cases, that's a good start.

After this phase, if slicing seems to be really useful, then we could figure out a longer-term integration strategy.

Laurențiu (Feb 27 2021 at 15:28, on Zulip):

If that doesn't pan out, can I interest you in a test case minimization tool? :joy_cat:

Vytautas Astrauskas [he/him] (Feb 27 2021 at 16:15, on Zulip):

A quick question: does RA have precise information about lifetime constraints? For example, in the following snippet:

let mut x = vec![...];
r = &mut x;
r.push(&mut y);

The last statement would add a constraint that the anonymous lifetime associated with y should outlive the anonymous lifetime associated with r. As far as I know, Polonius is missing this information and it is critical.

Vytautas Astrauskas [he/him] (Feb 27 2021 at 16:17, on Zulip):

By “missing” I mean that this information is computed by Rustc and given to Polonius as input.

Jonas Schievink [he/him] (Feb 27 2021 at 16:17, on Zulip):

r-a does not compute that at the moment

Florian Diebold (Feb 27 2021 at 16:17, on Zulip):

no, rust-analyzer doesn't deal with lifetimes at all yet, basically. There's a large amount of plumbing that would need to be implemented before we can even start thinking about polonius integration

Florian Diebold (Feb 27 2021 at 16:18, on Zulip):

and a prerequisite to that is switching to Chalk's type representation fully

Vytautas Astrauskas [he/him] (Feb 27 2021 at 16:18, on Zulip):

I see. Thanks!

Laurențiu (Feb 27 2021 at 16:22, on Zulip):

Florian Diebold said:

and a prerequisite to that is switching to Chalk's type representation fully

Is there an incremental path to that? A part that somebody other than you could implement?

Vytautas Astrauskas [he/him] (Feb 27 2021 at 16:22, on Zulip):

@Will Crichton So, it seems that you will have to build on top of Rustc. If you are aiming for a research prototype, one option would be to hack something on top of Prusti, which should have most of the information you need or at least some ideas how to get it.

Will Crichton (Feb 27 2021 at 16:37, on Zulip):

Vytautas Astrauskas What's the advantage of using Prusti vs. rustc_private? Are there more slicing-relevant analyses than in rustc? Or is the analysis information more conveniently accessed/ documented?

Vytautas Astrauskas [he/him] (Feb 27 2021 at 16:47, on Zulip):

Will Crichton said:

Vytautas Astrauskas What's the advantage of using Prusti vs. rustc_private? Are there more slicing-relevant analyses than in rustc? Or is the analysis information more conveniently accessed/ documented?

The borrow checker information is buried deep inside the Rustc and Prusti uses extremely ugly hacks to get that information out. If you build on top of Prusti, you will not need to reimplement them. Of course, if you know a better way of getting out the borrow information, then I would be super happy to hear that because maintaining this code is a pain.

Vytautas Astrauskas [he/him] (Feb 27 2021 at 17:00, on Zulip):

@Will Crichton If you would like to have a call to discuss what Prusti does and whether/how that could be useful for you, let me know.

Florian Diebold (Feb 27 2021 at 20:29, on Zulip):

Laurențiu Nicola said:

Florian Diebold said:

and a prerequisite to that is switching to Chalk's type representation fully

Is there an incremental path to that? A part that somebody other than you could implement?

Hmm actually I think the best approach is to gradually move the API of things like Ty to be the same as the Chalk version, to reduce the size of the final step of actually switching

Lukas Wirth (Feb 28 2021 at 00:57, on Zulip):

I'll try to work on that a bit

Last update: Jul 27 2021 at 21:15UTC