A Synthesis Method of Safe Rust Code Based on Pushdown Colored Petri Nets
For developers and researchers working with Rust, this work provides a formal method to automatically generate safe code that adheres to Rust's strict compile-time constraints, though it is an incremental step building on Petri net theory.
The paper tackles the challenge of automatically synthesizing correct and safe Rust code that satisfies ownership, borrowing, and lifetime constraints. The proposed method based on Pushdown Colored Petri Nets (PCPN) successfully generates valid call sequences, with all synthesized codes verified as correct in experiments.
Safe Rust guarantees memory safety through strict compile-time constraints: ownership can be transferred, borrowing can temporarily guarantee either shared read-only or exclusive write access, and ownership and borrowing are scoped by lifetime. Automatically synthesizing correct and safe Rust code is challenging, as the generated code must not only satisfy ownership, borrowing, and lifetime constraints, but also meet type and interface requirements at compile time. This work proposes a synthesis method based on our newly defined Pushdown Colored Petri Net (PCPN) that models these compilation constraints directly from public API signatures to synthesize valid call sequences. Token colors encode dynamic resource states together with a scope level indicating the lifetime region in which a borrow is valid. The pushdown stack tracks the entering or leaving of lifetime parameter via pushing and popping tokens. A transition is enabled only when type matching and interface obligations both hold and the required resource states are available. Based on the bisimulation theory, we prove that the enabling and firing rules of PCPN are consistent with the compile-time check of these three constraints. We develop an automatic synthesis tool based on PCPN and the experimental results show that the synthesized codes are all correct.