rapx/cli/
verify.rs

1use clap::Args;
2
3#[derive(Debug, Clone, Copy, clap::ValueEnum)]
4pub enum VerifyMode {
5    #[value(help = "Auto-detect: verify all functions with unsafe callees or struct invariants")]
6    Scan,
7    #[value(help = "Only verify functions annotated with #[rapx::verify]")]
8    Targeted,
9}
10
11/// Postfix repeat count: `auto` (default) enables automatic loop-depth
12/// detection; a number N ≥ 0 sets a fixed repeat count.
13#[derive(Debug, Clone)]
14pub enum PostfixRepeat {
15    Auto,
16    Fixed(usize),
17}
18
19impl std::fmt::Display for PostfixRepeat {
20    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
21        match self {
22            PostfixRepeat::Auto => write!(f, "auto"),
23            PostfixRepeat::Fixed(n) => write!(f, "{n}"),
24        }
25    }
26}
27
28impl std::str::FromStr for PostfixRepeat {
29    type Err = String;
30    fn from_str(s: &str) -> Result<Self, Self::Err> {
31        if s.eq_ignore_ascii_case("auto") {
32            Ok(PostfixRepeat::Auto)
33        } else {
34            s.parse::<usize>()
35                .map(PostfixRepeat::Fixed)
36                .map_err(|_| format!("expected 'auto' or a non-negative integer, got '{s}'"))
37        }
38    }
39}
40
41/// Arguments for the `verify` command.
42#[derive(Debug, Clone, Args)]
43pub struct VerifyArgs {
44    /// Identify all functions annotated with #[rapx::verify] and print each target, its unsafe callees, and their safety contracts.
45    #[arg(long)]
46    pub prepare_targets: bool,
47    /// Number of extra SCC postfix repetitions allowed during path enumeration.
48    /// `auto` (default): automatic loop-depth detection for InBound and Align.
49    /// A number ≥ 0 sets a fixed repeat count.
50    #[arg(long, default_value = "auto", value_parser = clap::value_parser!(PostfixRepeat))]
51    pub postfix_repeat: PostfixRepeat,
52    /// Verification mode: `scan` auto-detects unannotated unsafe targets (default), `targeted` verifies #[rapx::verify] functions.
53    #[arg(long, default_value = "scan")]
54    pub mode: VerifyMode,
55    /// Skip struct invariant checks and derive safety via constructor-mutator-method chains.
56    /// Works with both `scan` and `targeted` modes.
57    #[arg(long)]
58    pub skip_invariant: bool,
59    /// Filter verification targets to only those within the specified crate
60    /// (Rust crate name or Cargo package name, e.g. `std`, `core`, `my-crate`).
61    /// Useful for standard-library workspaces and sub-workspaces.
62    #[arg(long = "crate")]
63    pub crate_name: Option<String>,
64    /// Filter verification targets to only those within the specified module path
65    /// (e.g. `my_module::inner`). When combined with `--crate`, the path is
66    /// interpreted relative to that crate. Applies to all verification modes.
67    #[arg(long)]
68    pub module: Option<String>,
69    /// Print all contract resolutions for every verification target: each
70    /// unsafe callee with its resolved contracts, and the caller's own
71    /// contracts (expanded form).  Useful for debugging missing or unexpected
72    /// contract resolutions.
73    #[arg(long)]
74    pub debug_contracts: bool,
75}
rapx/cli/verify.rs

rapx/cli/
verify.rs
