A Synthesis Method of Safe Rust Code Based on Pushdown Colored Petri Nets

TL;DR

This paper introduces a novel synthesis method for safe Rust code using Pushdown Colored Petri Nets (PCPN), modeling ownership, borrowing, and lifetime constraints to generate correct code automatically.

Contribution

The paper proposes a new PCPN-based approach to synthesize safe Rust code directly from API signatures, ensuring compile-time safety constraints are met.

Findings

Synthesized Rust code is verified to be correct.

The PCPN model accurately captures ownership, borrowing, and lifetime constraints.

The approach automates safe code generation from API specifications.

Abstract

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.