Verified Program Synthesis for Refactoring Rust Programs

PIs: Meng Wang and Cristina David, University of Bristol

The aim of the project is to mechanically produce semantic-preserving Rust programs that are verified safe by the Rust type system.

A significant amount of trustworthiness of software may be derived from the programming languages that it is written in, hence the development of automatic migration tools which allows for transpilation (a.k.a, source-to source compilation) from C to Rust.

Transpilation tools can reliably produce syntactically correct Rust code that is extensively tested to be semantically equivalent to the original C code, but despite being correct, the raw output of C2Rust does not automatically benefit from Rust’s safety features. This means that the output of C2Rust needs to be gradually rewritten and at the moment, this is achieved either by hand or by manually defining refactoring rules. This refactoring requirement has become a bottleneck that limits the benefit of transpilers, and holds back language migration in general. 

The goal of this project if to design a general synthesis-based refactoring framework. We can then integrate this framework with C2Rust to create an automated system that transpiles C code to quality Rust code, and significantly reduce the amount of manual refactoring.