fw-immunant
commented
1 year ago While this project has significant overlap in direction with our own work on building a tool that transforms the unsafe output of C2Rust into safer Rust code, it does not have the same scope or rely on very similar techniques.
From the CROWN paper:
As mentioned in section 2.2, we do not attempt to translate array pointers to safe pointers. In the rest of the section, we focus on mutable, non-array pointers.
The translation requires a global view of pointers’ ownership, whereas infor- mation inferred by the ownership analysis refers to individual program locations. For the purpose of translation, given that we refactor owning pointers into box pointers, a pointer is considered (globally) owning if it owns a memory object at any program location within its scope. Otherwise, it is (globally) non-owning. When retyping pointer fields of structs, we must consider the scope of the struct declaration, which generally transcends the whole program. Within this scope, each field is usually accessed from several base variables, which must all be taken into consideration. For instance, given the List declaration in figure 1b and two variables l1 and l2 of type *mut List. Then, in order to determine the own- ership status of field next, we have to consider all the access paths to next originating from both base variables l1 and l2.
...
The non-owning pointers that are kept as raw pointers *mut T correspond to mutable local borrows. For Crown to soundly translate to mutable local borrows, it would have to reason about lifetime information. Given that in Rust there can’t be two mutable references to a value, Crown would have to check that there is no overlap between the lifetimes of different mutable references to the same object. In this work, we chose not to do this and instead leave it as a future work (as also mentioned under limitations in section 7). Notably, this restriction does not apply to output parameters, for which we translate to mutable references. This already covers the majority of mutable references – Das observed that, in C code, most references arise because the address of a variable is passed as a parameter [11]. Notably, the lack of a lifetime analysis means that we also can’t handle immutable local borrows, hence our translation’s focus on mutable pointers
In contrast, our ongoing work on safening the output of C2Rust does rely on the borrow checker and attempts to reason about lifetimes and immutable references, in addition to ownership. It uses the Polonius borrow checker implementation to explore the space of possible lifetime assignments and reasons about ownership by way of dataflow analysis and constraint propagation. A more detailed explanation of our approach will probably be written up after we finish prototyping, but for now it doesn't make sense to write down more than is useful for internal collaboration and development, as much is still in flux.
Thanks for asking! We're always glad to see people working atop C2Rust and building tools in this space.
This paper explain the CROWN translator for C > safe Rust translation.
Do you know this translator? it fills the current gap for safe Rust on c2rust? you will use it as a model?