Refactoring tools are central to modern development, with extract-function refactorings used heavily in day-to-day work. For Rust, however, ownership, borrowing, and advanced type features make automated extract-function refactoring challenging. Existing tools either rely on slow compiler-based analysis, support only restricted language fragments, or provide little assurance beyond "it still compiles." This paper presents REM2.0, a new extract-function and verification toolchain for Rust. REM2.0 works atop rust-analyzer as a persistent daemon, providing low-latency refactorings with a VSCode front-end. It adds a repairer that automatically adjusts lifetimes and signatures when extraction exposes borrow-checker issues, and an optional verification pipeline connecting to CHARON and AENEAS to generate Coq equivalence proofs for a supported Rust subset. The architecture is evaluated on three benchmark suites. On the original REM artefact, REM2.0 achieves 100% compatibility while reducing latency from ~1000ms to single-digit milliseconds in the daemon. On 40 feature-focused extractions from 20 highly starred GitHub repositories, REM2.0 handles most examples involving async/await, const fn, non-local control flow, generics, and higher-ranked trait bounds. On twenty verification benchmarks, the CHARON/AENEAS pipeline constructs end-to-end equivalence proofs for cases within its current subset. Overall, results show that a rust-analyzer-based design can provide fast, feature-rich extract-function refactoring for real Rust programs, while opt-in verification delivers machine-checked behaviour preservation.

翻译：重构工具是现代软件开发的核心，其中提取函数重构在日常工作中被广泛使用。然而对于 Rust 语言而言，所有权机制、借用规则及高级类型特性使得自动化提取函数重构变得尤为困难。现有工具要么依赖缓慢的基于编译器的分析，要么仅支持受限的语言子集，或只能提供“代码仍可编译”这种程度的有限保证。本文提出 REM2.0，一个面向 Rust 的新型提取函数与验证工具链。REM2.0 基于 rust-analyzer 作为常驻守护进程运行，通过 VSCode 前端提供低延迟重构操作。该工具链新增了修复模块，可在提取操作引发借用检查器问题时自动调整生命周期与函数签名，并提供了可选的验证流程——通过连接 CHARON 与 AENEAS 工具，为支持的 Rust 子集生成 Coq 等价性证明。该架构在三个基准测试集上进行了评估：在原始 REM 测试集上，REM2.0 实现了 100% 的兼容性，同时将守护进程的延迟从约 1000 毫秒降低至个位数毫秒；在从 20 个高星标 GitHub 仓库提取的 40 个特性导向案例中，REM2.0 成功处理了涉及 async/await、const fn、非局部控制流、泛型及高阶 trait 约束的大多数示例；在二十项验证基准测试中，CHARON/AENEAS 流程为其当前支持的子集案例构建了端到端的等价性证明。总体而言，研究结果表明：基于 rust-analyzer 的设计能够为实际 Rust 程序提供快速且功能丰富的提取函数重构，而可选的验证机制则能提供机器可检验的行为保持性保证。