cs.SEApr 2, 2026

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

Authors: Kaiwen Zhang, Guanjun Liu

Organizations: Tongji University, Shanghai, China

Read PDF
Ask AI
Cite

Copy citation

DOINot available for this paper

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.

Figures & tables

 Σ⊢g=˙⟨g,λ⟩⇒(⟨∅,∅⟩,∅)\textscU−GTyΣ⊢α=˙⟨τ^,λ⟩⇒(⟨[α↦τ^],∅⟩,∅)\textscU−TVarΣ⊢τ=˙⟨τ^,λ⟩⇒(σ,O)Σ⊢[τ]=˙⟨[τ^],λ⟩⇒(σ,O)\textscU−Slice\parΣ⊢Field(τ,f)=˙⟨τ^,λ⟩⇒(⟨∅,∅⟩,{Field(τ,f)=τ^})\textscU−FieldΣ⊢Assoc(τ,Tr,A)=˙⟨τ^,λ⟩⇒(⟨∅,∅⟩,{Assoc(τ,Tr,A)=τ^})\textscU−Assoc\parΣ⊢τ=˙⟨τ^,λ⟩⇒(σ0,O0)λ(ℓ′)=LΣ⊢Refℓq(τ)=˙⟨Refℓ′q(τ^),λ⟩⇒(σ0⊔⟨∅,[ℓ↦L]⟩,O0)\textscU−Ref\par∀i. Σ⊢τi=˙⟨τ^i,λ⟩⇒(σi,Oi)(σ,O)=⨆i(σi,Oi)Σ⊢(τ1,…,τn)=˙⟨(τ^1,…,τ^n),λ⟩⇒(σ,O)\textscU−TupleΣ⊢τ0=˙⟨τ^0,λ⟩⇒(σ0,O0)∀i. Σ⊢τi=˙⟨τ^i,λ⟩⇒(σi,Oi)(σ,O)=⨆i=0n(σi,Oi)Σ⊢τ0⟨τ1,…,τn⟩=˙⟨τ^0⟨τ^1,…,τ^n⟩,λ⟩⇒(σ,O)\textscU−App\frac{}{\Sigma\vdash g\mathrel{\dot{=}}\langle g,\lambda\rangle\Rightarrow(\langle\emptyset,\emptyset\rangle,\emptyset)}\hskip 9.24994pt\textsc{{U-GTy}}\frac{}{\Sigma\vdash\alpha\mathrel{\dot{=}}\langle\hat{\tau},\lambda\rangle\Rightarrow(\langle[\alpha\mapsto\hat{\tau}],\emptyset\rangle,\emptyset)}\hskip 9.24994pt\textsc{{U-TVar}}\frac{\Sigma\vdash\tau\mathrel{\dot{=}}\langle\hat{\tau},\lambda\rangle\Rightarrow(\sigma,\mathcal{O})}{\Sigma\vdash[\tau]\mathrel{\dot{=}}\langle[\hat{\tau}],\lambda\rangle\Rightarrow(\sigma,\mathcal{O})}\hskip 9.24994pt\textsc{{U-Slice}}\par\frac{}{\Sigma\vdash\mathsf{Field}(\tau,f)\mathrel{\dot{=}}\langle\hat{\tau},\lambda\rangle\Rightarrow(\langle\emptyset,\emptyset\rangle,\{\mathsf{Field}(\tau,f)=\hat{\tau}\})}\hskip 9.24994pt\textsc{{U-Field}}\frac{}{\Sigma\vdash\mathsf{Assoc}(\tau,\mathsf{Tr},A)\mathrel{\dot{=}}\langle\hat{\tau},\lambda\rangle\Rightarrow(\langle\emptyset,\emptyset\rangle,\{\mathsf{Assoc}(\tau,\mathsf{Tr},A)=\hat{\tau}\})}\hskip 9.24994pt\textsc{{U-Assoc}}\par\frac{\Sigma\vdash\tau\mathrel{\dot{=}}\langle\hat{\tau},\lambda\rangle\Rightarrow(\sigma_{0},\mathcal{O}_{0})\hskip 9.24994pt\lambda(\ell^{\prime})=L}{\Sigma\vdash\mathsf{Ref}^{q}_{\ell}(\tau)\mathrel{\dot{=}}\langle\mathsf{Ref}^{q}_{\ell^{\prime}}(\hat{\tau}),\lambda\rangle\Rightarrow(\sigma_{0}\sqcup\langle\emptyset,[\ell\mapsto L]\rangle,\mathcal{O}_{0})}\hskip 9.24994pt\textsc{{U-Ref}}\par\frac{\forall i.\ \Sigma\vdash\tau_{i}\mathrel{\dot{=}}\langle\hat{\tau}_{i},\lambda\rangle\Rightarrow(\sigma_{i},\mathcal{O}_{i})\hskip 9.24994pt(\sigma,\mathcal{O})=\bigsqcup_{i}(\sigma_{i},\mathcal{O}_{i})}{\Sigma\vdash(\tau_{1},\dots,\tau_{n})\mathrel{\dot{=}}\langle(\hat{\tau}_{1},\dots,\hat{\tau}_{n}),\lambda\rangle\Rightarrow(\sigma,\mathcal{O})}\hskip 9.24994pt\textsc{{U-Tuple}}\frac{\Sigma\vdash\tau_{0}\mathrel{\dot{=}}\langle\hat{\tau}_{0},\lambda\rangle\Rightarrow(\sigma_{0},\mathcal{O}_{0})\hskip 9.24994pt\forall i.\ \Sigma\vdash\tau_{i}\mathrel{\dot{=}}\langle\hat{\tau}_{i},\lambda\rangle\Rightarrow(\sigma_{i},\mathcal{O}_{i})\hskip 9.24994pt(\sigma,\mathcal{O})=\bigsqcup_{i=0}^{n}(\sigma_{i},\mathcal{O}_{i})}{\Sigma\vdash\tau_{0}\langle\tau_{1},\dots,\tau_{n}\rangle\mathrel{\dot{=}}\langle\hat{\tau}_{0}\langle\hat{\tau}_{1},\dots,\hat{\tau}_{n}\rangle,\lambda\rangle\Rightarrow(\sigma,\mathcal{O})}\hskip 9.24994pt\textsc{{U-App}} 
Table 1
RuleSchema NameOutput Multiset ( π\pi )Guard Condition
1Moveτ^\mathsf{Move}_{\hat{\tau}}∅\varnothing¬IsCopy(τ^)\neg\mathsf{IsCopy}(\hat{\tau})
2CopyUseτ^\mathsf{CopyUse}_{\hat{\tau}}pτ^own⟨c⟩p^{\mathsf{own}}_{\hat{\tau}}\langle c\rangleIsCopy(τ^)\mathsf{IsCopy}(\hat{\tau})
2 ⋆DupCopyτ^\mathsf{DupCopy}_{\hat{\tau}}pτ^own⟨c⟩⊕pτ^own⟨c′⟩p^{\mathsf{own}}_{\hat{\tau}}\langle c\rangle\oplus p^{\mathsf{own}}_{\hat{\tau}}\langle c^{\prime}\rangleIsCopy(τ^)∧c′=NewVal(c,ν)\mathsf{IsCopy}(\hat{\tau})\wedge c^{\prime}=\mathsf{NewVal}(c,\nu)
2 ′DupCloneτ^\mathsf{DupClone}_{\hat{\tau}}pτ^own⟨c⟩⊕pτ^own⟨c′⟩p^{\mathsf{own}}_{\hat{\tau}}\langle c\rangle\oplus p^{\mathsf{own}}_{\hat{\tau}}\langle c^{\prime}\rangleτ^:Clone∧c′=NewVal(c,ν)\hat{\tau}:\mathsf{Clone}\wedge c^{\prime}=\mathsf{NewVal}(c,\nu)
3 ′DropOwnτ^\mathsf{DropOwn}_{\hat{\tau}}∅\varnothing⊤\top
Table 1: Ownership and Duplication Schemas.
No.Transition FlowStack Action ( Act\mathsf{Act} )Output Token Construction
4pτ^own→pτ^frz⊕pτ^refp^{\mathsf{own}}_{\hat{\tau}}\to p^{\mathsf{frz}}_{\hat{\tau}}\oplus p^{\mathsf{ref}}_{\hat{\tau}}push Shr(vo,vr,L)⋅Freeze(vo)\mathsf{push}\ \mathsf{Shr}(v_{o},v_{r},L)\cdot\mathsf{Freeze}(v_{o})cr=NewRef(c,ν,μ)c_{r}=\mathsf{NewRef}(c,\nu,\mu)
5pτ^frz→pτ^frz⊕pτ^refp^{\mathsf{frz}}_{\hat{\tau}}\to p^{\mathsf{frz}}_{\hat{\tau}}\oplus p^{\mathsf{ref}}_{\hat{\tau}}push Shr(vo,vr,L)\mathsf{push}\ \mathsf{Shr}(v_{o},v_{r},L)cr=NewRef(c,ν,μ)c_{r}=\mathsf{NewRef}(c,\nu,\mu)
6pτ^own→pτ^blk⊕pτ^mutp^{\mathsf{own}}_{\hat{\tau}}\to p^{\mathsf{blk}}_{\hat{\tau}}\oplus p^{\mathsf{mut}}_{\hat{\tau}}push Mut(vo,vr,L)\mathsf{push}\ \mathsf{Mut}(v_{o},v_{r},L)cr=NewRef(c,ν,μ)c_{r}=\mathsf{NewRef}(c,\nu,\mu)
7pτ^blk⊕pτ^mut→pτ^ownp^{\mathsf{blk}}_{\hat{\tau}}\oplus p^{\mathsf{mut}}_{\hat{\tau}}\to p^{\mathsf{own}}_{\hat{\tau}}pop Mut(vo,vr,L)\mathsf{pop}\ \mathsf{Mut}(v_{o},v_{r},L)–
8pτ^frz⊕pτ^ref→pτ^frzp^{\mathsf{frz}}_{\hat{\tau}}\oplus p^{\mathsf{ref}}_{\hat{\tau}}\to p^{\mathsf{frz}}_{\hat{\tau}}pop Shr(vo,vr,L)\mathsf{pop}\ \mathsf{Shr}(v_{o},v_{r},L)–
9pτ^frz⊕pτ^ref→pτ^ownp^{\mathsf{frz}}_{\hat{\tau}}\oplus p^{\mathsf{ref}}_{\hat{\tau}}\to p^{\mathsf{own}}_{\hat{\tau}}pop Shr(vo,vr,L)⋅Freeze(vo)\mathsf{pop}\ \mathsf{Shr}(v_{o},v_{r},L)\cdot\mathsf{Freeze}(v_{o})–
Table 2: Borrow Creation and Discharge Schemas
No.Transition FlowStack ActionToken/Guard
10pτown→pτfownp^{\mathsf{own}}_{\tau}\to p^{\mathsf{own}}_{\tau_{f}}ϵ\epsiloncf=NewVal(c,ν)c_{f}=\mathsf{NewVal}(c,\nu)
11pτref→pτref⊕pτfrefp^{\mathsf{ref}}_{\tau}\to p^{\mathsf{ref}}_{\tau}\oplus p^{\mathsf{ref}}_{\tau_{f}}ϵ\epsiloncc=NewVal(c,ν)c_{c}=\mathsf{NewVal}(c,\nu)
12pτmut→pRefmut(τ)blk⊕pτfmutp^{\mathsf{mut}}_{\tau}\to p^{\mathsf{blk}}_{\mathsf{Ref}^{\mathsf{mut}}(\tau)}\oplus p^{\mathsf{mut}}_{\tau_{f}}push Mut(… )\mathsf{push}\ \mathsf{Mut}(\dots)cc=NewRef(c,ν,μ)c_{c}=\mathsf{NewRef}(c,\nu,\mu)
13pRefmut(τ)blk⊕pτfmut→pτmutp^{\mathsf{blk}}_{\mathsf{Ref}^{\mathsf{mut}}(\tau)}\oplus p^{\mathsf{mut}}_{\tau_{f}}\to p^{\mathsf{mut}}_{\tau}pop Mut(… )\mathsf{pop}\ \mathsf{Mut}(\dots)(Stack match)
Table 3: Field Projection Schemas (for field ff of type τ\tau )
No.Transition FlowStack ActionToken/Guard
14pτref→pτref⊕pτownp^{\mathsf{ref}}_{\tau}\to p^{\mathsf{ref}}_{\tau}\oplus p^{\mathsf{own}}_{\tau}ϵ\epsilonIsCopy(τ)∧c′=NewVal(c,ν)\mathsf{IsCopy}(\tau)\wedge c^{\prime}=\mathsf{NewVal}(c,\nu)
15pτmut→pRefmut(τ)blk⊕pτmutp^{\mathsf{mut}}_{\tau}\to p^{\mathsf{blk}}_{\mathsf{Ref}^{\mathsf{mut}}(\tau)}\oplus p^{\mathsf{mut}}_{\tau}push Mut(… )\mathsf{push}\ \mathsf{Mut}(\dots)c′=NewRef(c,ν,μ)c^{\prime}=\mathsf{NewRef}(c,\nu,\mu)
15’pRefmut(τ)blk⊕pτmut→pτmutp^{\mathsf{blk}}_{\mathsf{Ref}^{\mathsf{mut}}(\tau)}\oplus p^{\mathsf{mut}}_{\tau}\to p^{\mathsf{mut}}_{\tau}pop Mut(… )\mathsf{pop}\ \mathsf{Mut}(\dots)(Stack match)
16pτmut→pRefmut(τ)blk⊕pτrefp^{\mathsf{mut}}_{\tau}\to p^{\mathsf{blk}}_{\mathsf{Ref}^{\mathsf{mut}}(\tau)}\oplus p^{\mathsf{ref}}_{\tau}push Mut(… )\mathsf{push}\ \mathsf{Mut}(\dots)c′=NewRef(c,ν,μ)c^{\prime}=\mathsf{NewRef}(c,\nu,\mu)
16’pRefmut(τ)blk⊕pτref→pτmutp^{\mathsf{blk}}_{\mathsf{Ref}^{\mathsf{mut}}(\tau)}\oplus p^{\mathsf{ref}}_{\tau}\to p^{\mathsf{mut}}_{\tau}pop Mut(… )\mathsf{pop}\ \mathsf{Mut}(\dots)(Stack match)
Table 4: Dereference and Reborrowing Schemas
More in this topic

Program Synthesis

Program synthesis automatically constructs executable programs from examples, specifications, demonstrations, or natural-language descriptions.

See all 179 papers

Explore similar work

CardsList
Jul 23, 2026

From Resource Flow to Executable Tests: Petri-Net-Guided LLM Test Generation for Concurrent Stateful Rust APIs

Concurrent stateful library APIs expose behavior through evolving resource ownership, lifecycle states, and competing interleavings. Large language models can synthesize executable Rust tests, but their outputs often violate API preconditions, remain shallow, or reduce concurrency to accidental sequential traces. Conversely, model-based and systematic testing techniques provide semantic control but commonly require substantial handwritten code to turn abstract scenarios into executable tests. This paper addresses the gap between formal scenario design and low-cost test concretization. We present a Petri-net-guided methodology for test generation over concurrent stateful Rust APIs. The method represents API resources, lifecycle conditions, and causal dependencies as colored tokens and transitions; derives legal deep-state, near-legal, and partial-order concurrent scenarios; and uses these scenarios as a constrained intermediate representation for LLM-based code synthesis. A local-faithfulness contract and structural repair loop preserve the modeled intent during concretization, while Petri-guided schedule shaping prioritizes high-conflict concurrency skeletons for systematic exploration. A layered semantic oracle then distinguishes synthesis failures from violations of the target API's expected behavior.

Kaiwen Zhang, Guanjun Liu

Tongji University Shanghai,China

Automated Software TestingLLM-Based Program SynthesisAutomated Test Generation
AskPDF
Jul 15, 2026

Generative Compilation: On-the-Fly Compiler Feedback as AI Generates Code

Languages with rich static semantics, such as Rust, provide stronger guarantees for AI-generated code, but their strictness makes generation more difficult. Off-the-shelf compilers can provide useful feedback post-generation, but does not guide intermediate generation steps, such as those during autoregressive LLM decoding. Constrained decoding intervenes earlier by rejecting invalid tokens during sampling, but requires white-box model access and costly reimplementation for semantic constraints.We introduce generative compilation, the first approach to obtaining compiler feedback on partial programs during generation. The core technical device is a sealor: a lightweight, mostly syntax-guided transformation that converts partial programs into complete ones that standard compilers can diagnose. It is designed such that possible-to-complete partial programs are never rejected, while preserving enough code context to catch genuine dead ends early. We construct such a sealor on a core Rust-like calculus and prove that it satisfies these properties, all mechanized in Lean. We extend it to the first partial-program checker for real Rust. We evaluate our method on challenging repository-level Rust coding tasks, across both frontier black-box and open-weight models. We show that generative compilation reduces non-compiling outputs and improves functional correctness, relative to standard post-generation feedback. It does so by detecting a broad range of errors close to their source and early during generation, thereby reducing errors cascades and enabling focused diagnostics. More broadly, generative compilation is a step toward making compilers a first-class citizen of AI-assisted programming active during generation, rather than a separate post-generation check.

Niels Mündler-Sasahara, Hristo Venev, Dawn Song +2

ETH Zurich, Switzerland · INSAIT and Sofia University “St. Kliment Ohridski”, Bulgaria · University of California, Berkeley, USA

Code GenerationStatic Code Analysis
AskPDF
Apr 6, 2026

ENCRUST: Encapsulated Substitution and Agentic Refinement on a Live Scaffold for Safe C-to-Rust Translation

We present Encapsulated Substitution and Agentic Refinement on a Live Scaffold for Safe C-to-Rust Translation, a two-phase pipeline for translating real-world C projects to safe Rust. Existing approaches either produce unsafe output without memory-safety guarantees or translate functions in isolation, failing to detect cross-unit type mismatches or handle unsafe constructs requiring whole-program reasoning. Furthermore, function-level LLM pipelines require coordinated caller updates when type signatures change, while project-scale systems often fail to produce compilable output under real-world dependency complexity. Encrust addresses these limitations by decoupling boundary adaptation from function logic via an Application Binary Interface (ABI)-preserving wrapper pattern and validating each intermediate state against the integrated codebase. Phase 1 (Encapsulated Substitution) translates each function using an ABI-preserving wrapper that splits it into two components: a caller-transparent shim retaining the original raw-pointer signature, and a safe inner function targeted by the LLM with a clean, scope-limited prompt. This enables independent per-function type changes with automatic rollback on failure, without coordinated caller updates. A deterministic, type-directed wrapper elimination pass then removes wrappers after successful translation. Phase 2 (Agentic Refinement) resolves unsafe constructs beyond per-function scope, including static mut globals, skipped wrapper pairs, and failed translations, using an LLM agent operating on the whole codebase under a baseline-aware verification gate. We evaluate Encrust on 7 GNU Coreutils programs and 8 libraries from the Laertes benchmark, showing substantial unsafe-construct reduction across all 15 programs while maintaining full test-vector correctness.

Hohyun Sim, Hyeonjoong Cho, Ali Shokri +2

Korea University, South Korea · University of Houston, United States · State University of New York Korea, South Korea +1

Code TranslationLLM-Based Program Synthesis
AskPDF