Skip to content

Complete physical analysischeck/verify module migration in rapx#247

Merged
hxuhack merged 3 commits into
copilot/refactor-analysis-check-verifyfrom
copilot/copilotmigrate-physical-modules
May 12, 2026
Merged

Complete physical analysischeck/verify module migration in rapx#247
hxuhack merged 3 commits into
copilot/refactor-analysis-check-verifyfrom
copilot/copilotmigrate-physical-modules

Conversation

Copy link
Copy Markdown
Contributor

Copilot AI commented May 12, 2026

This continues the namespace split by completing the physical relocation of check/verify code out of analysis, and wiring the crate to compile against the new module tree. The prior refactor introduced top-level check/verify modules but still depended on files under analysis/*.

  • Physical module migration

    • Moved check-focused implementations:
      • analysis/opt/**check/opt/**
      • analysis/rcanary/**check/rcanary/**
      • analysis/safedrop/**check/safedrop/**
      • analysis/senryx/**check/senryx/**
    • Moved verify implementation:
      • analysis/verify/{attr_parser.rs, contract.rs, helpers.rs, target.rs, assets/**}verify/**
    • Removed stale analysis/verify/mod.rs.
  • Module tree completion

    • Replaced src/verify/mod.rs with the full local tree:
      • mod attr_parser;
      • mod contract;
      • mod helpers;
      • pub mod target;
    • Updated verify/target.rs to import sibling modules via super::... (instead of path attributes tied to old layout).
  • Path/import rewiring

    • Updated all migrated code references from crate::analysis::{opt|senryx|...} to crate::check::{opt|senryx|...} where appropriate.
    • Updated crate::analysis::verify usage to crate::verify.
    • Kept legitimate crate::analysis::{core,graphs,scan,upg,utils} references unchanged.
    • Fixed move-induced local import assumptions (e.g. check::opt and check::safedrop imports).
  • Asset/include path correctness after move

    • Adjusted verify helper include path to load shared analysis data from the new location context:
      serde_json::from_str(include_str!("../analysis/utils/data/std_sig.json"))
  • Minor review follow-up

    • Corrected a user-facing typo in an opt diagnostic message (isteadinstead).
Original prompt

Continue the refactor of repo safer-rust/RAPx on branch copilot/refactor-analysis-check-verify by performing the actual physical module migration for the Rust crate under rapx/.

Context:

  • A first-stage namespace split is already committed on the branch.
  • The crate now has top-level modules analysis, check, and verify declared in rapx/src/lib.rs.
  • rapx/src/analysis/mod.rs was reduced to analysis-only modules.
  • rapx/src/check/mod.rs and rapx/src/verify/mod.rs were added.
  • rapx/src/cli/check.rs was added and Commands::Check(CheckArgs) introduced.
  • However, the implementation files still physically live under rapx/src/analysis/..., so the module tree is incomplete and paths need to be fixed.

Your task:

  1. Physically move files/directories from rapx/src/analysis into the new namespaces:

    • Move rapx/src/analysis/opt/** to rapx/src/check/opt/**
    • Move rapx/src/analysis/rcanary/** to rapx/src/check/rcanary/**
    • Move rapx/src/analysis/safedrop/** to rapx/src/check/safedrop/**
    • Move rapx/src/analysis/senryx/** to rapx/src/check/senryx/**
    • Move rapx/src/analysis/verify/{attr_parser.rs,contract.rs,helpers.rs,target.rs,assets/**} into rapx/src/verify/
    • Replace rapx/src/verify/mod.rs with a complete module tree equivalent to the old analysis/verify/mod.rs and able to compile from the new location.
  2. Fix module declarations and imports across the crate so the new layout is consistent:

    • Update any crate::analysis::opt references to crate::check::opt
    • Update any crate::analysis::rcanary references to crate::check::rcanary
    • Update any crate::analysis::safedrop references to crate::check::safedrop
    • Update any crate::analysis::senryx references to crate::check::senryx
    • Update any crate::analysis::verify references to crate::verify
    • Keep legitimate crate::analysis::core, crate::analysis::graphs, crate::analysis::scan, crate::analysis::upg, and crate::analysis::utils references unchanged.
  3. Preserve public API names and behavior as much as possible:

    • Opt, rCanary, SafeDrop, CheckLevel, SenryxCheck, and VerifyTargetAnalysis should still be reachable from the paths already updated in rapx/src/lib.rs.
    • Do not rename CLI commands; only ensure the module/file structure matches the new namespaces.
  4. Clean up transitional leftovers:

    • Remove stale module declarations from rapx/src/analysis/mod.rs if any remain.
    • Ensure there is no dependence on rapx/src/analysis/verify/* after the migration.
    • Ensure rapx/src/verify/target.rs and helpers load assets from the new path correctly.
  5. Validation:

    • Run/build whatever validation is available to the coding agent for the crate.
    • If compile errors appear, fix straightforward import/module-path issues caused by the move.

Important constraints:

  • Work only in repository safer-rust/RAPx.
  • Continue from branch copilot/refactor-analysis-check-verify.
  • Create a pull request with the completed refactor.
  • Keep the PR focused on this module migration and path-fixing task.

The following is the prior conversation context from the user's chat exploration (may be truncated):

User: 创建agent,按照命令行analysis, check, verify refactor一下这个项目仓库,不要都放在analysis文件夹下面,src下分别创建check和verify文件夹

Assistant: 我正在等待你对刚才的操作确认/授权,一旦你回应,我就继续为这个仓库完成重构调整。

User: @copilot Accepted Confirmation: Are you sure?

Assistant: 可以,我已经理解你的目标:

  • 按命令行职责把项目重构为 analysis / check / verify
  • 不要把所有内容都放在 analysis 下面
  • src/ 下分别创建:
    • src/check/
    • src/verify/

不过我这条回复里不能继续直接执行仓库修改。
如果你愿意,我下一步可以继续帮你做成一个明确的重构方案,建议按下面方式整理:

建议目录结构

src/
  analysis/
  check/
  verify/

建议拆分原则

  • analysis/:放静态分析、信息收集、IR/中间表示分析、数据流/控制流分析等
  • check/:放规则检查、lint 类检查、模式匹配检查、违规检测等
  • verify/:放性质验证、约束证明、形式化验证、soundness/安全性验证等

推荐重构步骤

  1. 先梳理当前 src/analysis 下各模块职责
  2. 把“检查类”代码迁移到 src/check
  3. 把“验证类”代码迁移到 src/verify
  4. 修正 mod 声明和 use 路径
  5. 更新命令行子命令映射,使其对应:
    • analysis
    • check
    • verify
  6. 跑构建和测试,确保行为不变

如果你要我继续,我建议我下一步直接输出:

  1. 具体文件迁移清单
  2. 新的模块树设计
  3. CLI 子命令如何对应到三个目录
  4. 需要改的 mod.rs / main.rs / lib.rs 示例

如果你愿意,我下一条就直接给你一份 面向 RAPx 仓库的具体重构方案

User: 好的

Assistant: 已按你的要求完成第一步重构,并提交到新分支:

  • 分支:copilot/refactor-analysis-check-verify

这次调整做了这些事:

  • 保留 src/analysis/ 只放“分析类”模块
  • 新建 src/check/
  • 新建 src/verify/
  • 把顶层模块声明从原来的“都挂在 analysis 下”改成三层分离

已完成的结构调整

现在核心结构变成了:

rapx/src/
  analysis/
    mod.rs
    ...
  check/
    mod.rs
  verify/
    mod.rs

具体改动

  1. rapx/src/analysis/mod.rs

    • 只保留更偏 analysis 的模块:
    • core
    • graphs
    • scan
    • upg
    • utils
  2. 新增 rapx/src/check/mod.rs

    • 挂载:
    • opt
    • rcanary
    • safedrop
    • senryx
  3. 新增 rapx/src/verify/mod.rs

    • 挂载:
    • target
  4. rapx/src/lib.rs

    • 新增:
      • pub mod check;
      • pub mod verify;
    • 调整 use 路径:
      • `SafeDrop / rCanary / Opt / S...

This pull request was created from Copilot chat.

Copilot AI and others added 2 commits May 12, 2026 07:06
Copilot AI changed the title [WIP] Move physical module files for analysis, check, and verify Complete physical analysischeck/verify module migration in rapx May 12, 2026
Copilot AI requested a review from hxuhack May 12, 2026 07:11
@hxuhack hxuhack marked this pull request as ready for review May 12, 2026 07:15
@hxuhack hxuhack merged commit 616f457 into copilot/refactor-analysis-check-verify May 12, 2026
2 checks passed
hxuhack added a commit that referenced this pull request May 12, 2026
* Add a new cli option for verification. (#237)

* add verify test

* feat: add verify command with --scan option

* fix compilation errors

* fix bugs

* refactor verification module to make pipeline clearer (#238)

* Add unsafe callee detection for verification targets. (#239)

* Extend verify scan to collect unsafe callees

* add unsafe callees

* * rename scan to collect
* add std contracts
* add 2 test cases for alignment verification (#240)
* extract callee contracts.

---------

* Update verify target collector (#242)

* add local verify contract module

* add local verify helper module

* fix verify local module paths and type inference

* add English documentation to verify collect module

* update

* refactor verify (#243)

* add struct invariants (#244)

* add a struct example

* Refactor verify targets into function and struct targets

* Support struct field and generic resolution in verify helpers

* Simplify verify target collector structure

* Fix struct invariant collection for local struct targets

* Read struct invariants from local struct HIR items

* fix compilation bug

* fix bug

* Add RAPx attribute parser under verify

* Use shared RAPx attribute parser in verify target analysis

* Fix RAPx attribute parsing with syn outer attributes

* Use method context when parsing struct invariants

* update rapx attribute parsing (#245)

* merge two get fn proterty functions

* delete walk_fn

* refactor: simplify RAPx attribute parser flow

* refactor: deduplicate RAPx verify attribute collection

* refactor: remove requires kind filtering

* Associate RAPx kind with preceding property

* update attribute parser (#246)

* docs: add doc comments and inline comments to attr_parser.rs

* docs: clarify requires attribute parser comments and naming

* Refactor RAPx requires attribute parsing for semicolon metadata

* Simplify RAPx requires attribute parser for single property syntax

* Refactor src modules into analysis, check, and verify namespaces with dedicated CLI check args

* Complete physical `analysis` → `check`/`verify` module migration in `rapx` (#247)

---------

Co-authored-by: ClearLove <98693523+DiuDiu777@users.noreply.github.com>
@hxuhack hxuhack deleted the copilot/copilotmigrate-physical-modules branch May 12, 2026 07:31
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants