AeneasVerif
Feature request: Retag statements
Hello, Would it be possible to emit Retag statements (possibly on demand)? We want to run an analysis that makes use of tree borrows, and would need those in. The person in charge of this project would probably be happy to implement this feature if you give us a few pointers :)
Cheers!
That would be great to have! This is currently blocked on us supporting a later MIR than we do. Today we use mir_built but retags are only added in mir_drops_elaborated_and_const_checked; this is tracked here.
This is already something we plan to do; I haven't estimated how hard this would be yet. I would very much welcome help here! I wrote up some instructions here. Pop on the Zulip if you want to have a go or have questions.
Our student is starting this Monday and will probably start on something slightly different, but I'll give her the various links for when she starts this project, thank you very much for the pointers!
That's an easy issue: just add StatementKind::Retag to ullbc and llbc, as well as a test that uses --mir elaborated and showcases a Retag statement (probably something with a reborrow?).
@N1ark correct me if I'm wrong but it looks like retag statements are not necessary for Tree Borrows? This might be something we have to confirm with Ralf or Johannes 🤔 If that is true, I'd just close this issue really since it means Retag are only useful for Stacked Borrows and don't need to be supported by ULLBC
it's not that we don't need them it's really just that they appear at very specific places (function calls and reborrows) so one can just apply retags in these specific places rather than using an explicit statement -- im happy to close this issue because of this; if anyone wants to do retag they just do it in these two spots without ""polluting"" the AST for everyone
That's the code that adds retags in rustc: https://github.com/rust-lang/rust/blob/master/compiler/rustc_mir_transform/src/add_retag.rs . It's not huge but it doesn't look trivial either. One interesting point is that if we had retags then we could do more UB-preserving transformations in charon like inlining or inserting reborrows.