Chapter 1. Introduction

RAPx is a static analysis and verification platform for Rust programs. It has two objectives:

• To serve as a companion to the Rust compiler in detecting semantic bugs related to unsafe code.
• To provide ready-to-use program analysis features for tool developers.

Although Rust has made significant progress in ensuring memory safety and protecting software from undefined behavior, the Rust compiler's capability is inherently limited due to Rice's theorem. In general, it refrains from detecting undefined behaviors related to unsafe code, as achieving both precise and efficient analysis is extremely challenging. This limitation arises because the Rust compiler prioritizes usability, as developers cannot tolerate false positives. RAPx is not bound by this constraint. It may produce false positives, as long as they remain within an acceptable range.

Writing program analysis tools is challenging. In this project, we also aim to provide a user-friendly framework for developing new static program analysis features for Rust. In particular, our project integrates dozens of classic program analysis algorithms, including those for pointer analysis, value-flow analysis, control-flow analysis, and more. Developers can choose and combine them like Lego blocks to achieve new bug detection or verification capabilities. The project repository is at github.com/safer-rust/RAPx.

Architecture

RAPx is organized into four top-level modules:

Vision

The verification module (rapx::verify) is positioned to become the harness for Rust Agentic Coding — an automated safety gate for AI-generated Rust code. As LLM-based coding agents increasingly produce unsafe blocks, a fast, contract-driven verifier that can independently confirm or reject the soundness of generated unsafe code is essential. RAPx's verification pipeline — from target collection through path-sensitive state tracking to SMT-backed property checking — provides the foundation for this role. Future directions include tighter integration with IDE and CI workflows, richer contract expression, and inter-procedural summary propagation to scale verification to whole crates.

Chapter 2. Installation and Usage Guide

Platform Support

RAPx supports the following three platforms:

• Linux (x86_64)
• macOS (x86_64)
• macOS (aarch64/Apple Silicon)

Preparation

RAPx requires a nightly Rust toolchain with three components: rustc-dev, rust-src, llvm-tools-preview.

Three toolchain versions are supported:

Install the recommended (latest) toolchain:

rustup toolchain install nightly --profile minimal --component rustc-dev,rust-src,llvm-tools-preview

The main branch pins nightly in its rust-toolchain.toml, so RAPx tracks the latest nightly. If you need a specific pinned version instead (e.g. to match the asterinas or verify-std CI jobs), install it explicitly:

rustup toolchain install nightly-2026-07-21 --profile minimal --component rustc-dev,rust-src,llvm-tools-preview

If you have multiple Rust versions, please ensure the correct version is set as default:

rustup show

Install

Download the project

git clone https://github.com/safer-rust/RAPx.git

Build and install RAPx

./install.sh

You can combine the previous two steps into a single command:

cargo +nightly install rapx --git https://github.com/safer-rust/RAPx.git

For macOS users, you may encounter compilation errors related to Z3 headers and libraries. There are two solutions:

The first one is to manually export the headers and libraries as follows:

export C_INCLUDE_PATH=/opt/homebrew/Cellar/z3/VERSION/include:$C_INCLUDE_PATH
ln -s /opt/homebrew/Cellar/z3/VERSION/lib/libz3.dylib /usr/local/lib/libz3.dylib

Alternatively, you can modify the Cargo.toml file to change the dependency of Z3 to use static linkage. However, this may significantly slow down the installation process, so we do not recommend enabling this option by default.

[dependencies]
z3 = {version="0.13.3", features = ["static-link-z3"]}

After this step, you should be able to see the RAPx plugin for cargo.

cargo --list

Execute the following command to run RAPx and print the help message:

cargo rapx --help
Usage: cargo rapx [OPTIONS] <COMMAND> [-- [CARGO_FLAGS]]

Commands:
  analyze  perform various analyses on the crate, e.g., alias analysis, callgraph generation
  check    check potential vulnerabilities in the crate, e.g., use-after-free, memory leak
  opt      detect code optimization opportunities
  verify   verify annotated functions in the crate, e.g., identify #[rapx::verify] targets
  help     Print this message or the help of the given subcommand(s)

Options:
      --timeout <TIMEOUT>        specify the timeout seconds in running rapx
      --test-crate <TEST_CRATE>  specify the tested package in the workspace
  -h, --help                     Print help
  -V, --version                  Print version

NOTE: multiple detections can be processed in single run by 
appending the options to the arguments. Like `cargo rapx check -f -m`
will perform two kinds of detection in a row.

Examples:

  1. detect use-after-free and memory leak:
     cargo rapx check -f -m
  2. detect optimization opportunities:
     cargo rapx opt
  3. perform alias analysis:
     cargo rapx analyze alias
  4. verify annotated functions:
     cargo rapx verify --prepare-targets

analyze command

Usage: cargo rapx analyze <COMMAND>

Commands:
  alias         alias analysis (meet-over-paths by default)
  adg           API dependency graphs
  safetyflow    unsafety propagation graph (safety flow analysis)
  safetyflowstd unsafety propagation graph on the standard library
  callgraph     callgraph generation
  dataflow      dataflow graphs
  heapowner     analyze heap-owning types
  paths         path-sensitive CFG paths
  pathcond      path constraint extraction
  range         range analysis
  scan          basic crate info
  ssa           print the SSA form of the crate
  mir           print MIR
  dot-mir       print MIR as DOT
  help          Print this message or the help of the given subcommand(s)

Options:
  -h, --help  Print help

Notable subcommand options:

• alias -s <STRATEGY> / --strategy <STRATEGY> — choose alias analysis strategy: mop (meet-over-paths, default) or mfp (maximum-fixed-point)
• dataflow -d / --debug — print debug information during dataflow analysis
• dataflow --draw — render dataflow graphs as PNG images (requires Graphviz)
• safetyflow --draw — render safety flow graphs as PNG images (requires Graphviz)
• safetyflowstd --draw — render safety flow graphs on stdlib as PNG images
• paths --postfix-repeat <N> — allow repeated SCC postfix segments (default 0)
• range -d / --debug — print debug information during range analysis
• adg --include-private — include private APIs in the API graph
• adg --include-unsafe — include unsafe APIs in the API graph
• adg --include-drop — include Drop impls in the API graph
• adg --max-iteration <N> — maximum generic iteration count (default 10)
• adg --dump [PATH] — dump API graph to file (default ./api_graph.dot)

check command

Usage: cargo rapx check [OPTIONS]

Options:
  -f, --uaf [<UAF>]    detect use-after-free/double-free (optional level, default 1)
  -m, --mleak          detect memory leakage
  -h, --help           Print help

opt command

Usage: cargo rapx opt

verify command

The verify command provides a contract-based verification pipeline for functions annotated with #[rapx::verify]. It uses path-sensitive backward/forward analysis and Z3-based SMT solving to prove safety properties. RAPx supports two verification modes (see Chapter 8 for details).

Usage: cargo rapx verify [OPTIONS]

Options:
      --prepare-targets            identify #[rapx::verify] functions and list their safety contracts
      --debug-contracts            print contract resolutions per target and exit (no verification)
      --skip-invariant             skip struct invariant checks, derive safety via
                              constructor-mutator-method chains (works with both modes)
      --postfix-repeat <N|auto>
                              extra SCC postfix repetitions during path enumeration;
                              `auto` is the default planner, a number fixes the repeat count
      --mode <MODE>               verification mode: scan, targeted (default scan)
      --crate <CRATE>             filter verification targets to the named crate
      --module <PATH>             filter verification targets to the named module path
  -h, --help                      Print help

Verification modes:

• scan — auto-detect: verify all functions with unsafe callees or struct invariants
• targeted — only verify functions annotated with #[rapx::verify]

The --skip-invariant flag works with both modes to skip struct invariant checks and instead derive safety through constructor-mutator-method chains.

The --postfix-repeat option controls loop unrolling depth:

• auto (default) — automatic loop-depth detection for InBound and Align contracts
• A fixed number N ≥ 0 — repeat loop body up to N+1 times

Filtering targets: --crate and --module work in any mode and can be combined:

cargo rapx verify --module my_mod::sub
cargo rapx verify --crate core --module ptr::NonNull

Environment Variables

For RAPX_RECURSIVE:

• none: check for current folder
• shallow: check for current workspace members
• deep: check for all workspaces from current folder

Uninstall

cargo uninstall rapx

Chapter 3. Framework of RAPx

Traditionally, performing code analysis requires modifying the compiler source code to add new passes. Developers then need to recompile the compiler to activate these new passes, which can be cumbersome. The Rust compiler offers a more portable way to conduct code analysis using the rustc_driver. We refer to this approach as the frontend method because it allows developers to directly access internal compiler data and perform analysis as callbacks.

Custom Cargo Commands

To support project-level program analysis, we want the analysis tool to be integrated into cargo as subcommands. To this end, we can name the tool as cargo-toolname and place it in $CARGO_HOME/bin or $PATH. Then we can execute the tool via the following command.

cargo toolname -more_arguments

Cargo will automatically search the binaries named cargo-toolname from the paths. The following figure demonstrates the whole process before reaching our analysis program. Note that we cannot directly invoke rapx in the first round but through cargo check because we need cargo to manage the project-level compilation and append detailed compilation options for launching rustc. However, we want to hook rustc execution and execute rapx instead for analysis. Therefore, we set RUSTC_WRAPPER with the value of cargo-rapx. In this way, cargo check will actually run cargo-rapx rustc appended_options. We then dispatch the execution to rapx with appended options.

Register Analysis Callbacks

Supposing the purpose is to execute a function named my_analysis, developers should design a new struct and implement the Callbacks Trait for the struct.

#![allow(unused)]
fn main() {
pub struct MyCallback {...}
impl Callbacks for MyCallback {
    fn after_analysis<'tcx>(&mut self, _compiler: &Compiler, tcx: TyCtxt<'tcx>) -> Compilation {
        my_analysis(tcx, *self) // the analysis function to execute after compilation.
        Compilation::Continue
    }
}
}

To execute the compiler and callback function, developers can employ the APIs rustc_driver::RunCompiler provided by Rust.

#![allow(unused)]

fn main() {
let mut callback = MyCallback::default();
let run_compiler = rustc_driver::RunCompiler::new(&args, callback);
let exit_code = rustc_driver::catch_with_exit_code(move || run_compiler.run());
}

Chapter 4. Preliminary: Compiler Internals

This chapter introduces the Rust compiler internals that RAPx builds upon. Understanding these concepts is essential for reading the analysis and verification chapters that follow.

Intermediate Representations

RAPx primarily operates on two levels of Rust's intermediate representation:

HIR (High-Level IR)

HIR is a type-checked, desugared AST. Macro expansion, name resolution, and type checking have completed by this stage. HIR is used in RAPx for:

• Fast pre-filtering: hir_contains_unsafe() in the Safety-Flow and Verification modules checks whether a function body contains unsafe fn declarations or unsafe { } blocks without descending into MIR.
• Attribute scanning: #[rapx::verify], #[rapx::requires(...)], and #[rapx::invariant(...)] are read from HIR attributes via tcx.hir_attrs().
• Struct definition inspection: Checking whether a struct has PhantomData fields or specific type invariants.

cargo rustc -- -Z unpretty=hir-tree

MIR (Mid-Level IR)

MIR is a control-flow-graph-based IR where each function is decomposed into basic blocks connected by terminators. MIR is not in SSA form by default. RAPx uses MIR for all path-sensitive and dataflow analyses because:

• MIR has a finite, well-defined set of statement and terminator kinds, making exhaustive pattern matching feasible.
• Every loop in MIR is a natural loop (has a single dominator), enabling SCC-based path enumeration.
• MIR preserves type information and place projections, enabling field-sensitive analysis.

cargo rustc -- -Zunpretty=mir

To obtain the optimized MIR for a function:

#![allow(unused)]
fn main() {
let body: &Body<'tcx> = tcx.optimized_mir(def_id);
}

RAPx compiles with -Zmir-opt-level=0 to preserve the original MIR structure (no inlining, no optimization passes that could obscure unsafe operations).

Key Data Structures

TyCtxt

TyCtxt<'tcx> is the central context object of the Rust compiler. It provides access to virtually all compiler state: type information, MIR bodies, HIR bodies, crate metadata, and trait resolution. Every RAPx analysis module receives a TyCtxt<'tcx> and uses it as the entry point for all queries.

#![allow(unused)]
fn main() {
// Get the MIR body for a function
let body = tcx.optimized_mir(def_id);

// Get the type of a MIR local
let ty = body.local_decls[local].ty;

// Iterate over all local crate definitions
for local_def_id in tcx.iter_local_def_id() {
    let def_kind = tcx.def_kind(local_def_id);
    // ...
}
}

DefId

DefId is a globally unique identifier for any item (function, struct, trait, impl, etc.) across all crates. It pairs a crate number (CrateNum) with a definition index.

#![allow(unused)]
fn main() {
let def_path = tcx.def_path_str(def_id);  // e.g. "std::vec::Vec::new"
let crate_name = tcx.crate_name(def_id.krate);  // "std", "core", etc.
}

LocalDefId is a crate-local variant that does not carry a crate identifier:

#![allow(unused)]
fn main() {
let def_id: DefId = local_def_id.to_def_id();
}

MIR Body Structure

A Body<'tcx> represents the MIR of a single function. Its key fields:

#![allow(unused)]
fn main() {
pub struct Body<'tcx> {
    pub basic_blocks: IndexVec<BasicBlock, BasicBlockData<'tcx>>,
    pub local_decls: IndexVec<Local, LocalDecl<'tcx>>,
    pub arg_count: usize,          // number of arguments
    pub spread_arg: Option<Local>, // variadic spread argument
    pub var_debug_info: Vec<VarDebugInfo<'tcx>>,
    pub span: Span,
    // ...
}
}

• arg_count: Arguments occupy Local(1) through Local(arg_count). Local(0) is the return value.
• local_decls: Maps each Local to its type, mutability, and source span.

BasicBlock and BasicBlockData

A BasicBlock is an index into the basic_blocks vector. BasicBlockData contains:

#![allow(unused)]
fn main() {
pub struct BasicBlockData<'tcx> {
    pub statements: Vec<Statement<'tcx>>,  // zero or more statements
    pub terminator: Option<Terminator<'tcx>>, // exactly one, except for unreachable blocks
    pub is_cleanup: bool,
}
}

Statements execute sequentially within a block. The terminator determines which block(s) execute next.

Statements

Statement kinds most relevant to RAPx:

Terminators

Terminator kinds most relevant to RAPx:

Place and Local

Place<'tcx> represents a memory location: a base Local plus a sequence of projections.

Local is an index into body.local_decls. Local(0) is the return value; Local(1..=arg_count) are function arguments; higher indices are temporaries and user variables.

#![allow(unused)]
fn main() {
let place = Place { local: Local::from_usize(3), projection: vec![] };
let place_with_field = place.project_field(1);  // _3.1
}

Projections applied in sequence:

Operand and Rvalue

Operand<'tcx> is the right-hand side source in assignments and call arguments:

#![allow(unused)]
fn main() {
pub enum Operand<'tcx> {
    Copy(Place<'tcx>),    // copy the value at place
    Move(Place<'tcx>),    // move the value at place
    Constant(Box<ConstOperand<'tcx>>),  // compile-time constant
}
}

Rvalue<'tcx> is the right-hand side of an assignment, describing how the value is produced:

How RAPx Hooks into rustc

RAPx runs as a custom rustc driver via the RUSTC_WRAPPER mechanism, similar to Miri. The entry point is cargo-rapx which:

1. Phase 1 (cargo rapx ...): Sets RUSTC_WRAPPER=cargo-rapx and invokes cargo check.
2. Phase 2 (rustc wrapper): Cargo invokes cargo-rapx path/to/rustc .... RAPx intercepts this, runs the requested analysis, then calls the real rustc to complete compilation.

The RapCallback struct in lib.rs implements rustc_driver::Callbacks with two hooks:

• config: Injects -Zalways-encode-mir, -Zmir-opt-level=0 and other flags to ensure MIR is available and unoptimized.
• after_analysis: After type checking and MIR construction, RAPx dispatches to the requested command (Analyze, Check, or Verify), each of which runs within rustc_public::rustc_internal::run(tcx, ...) to access the TyCtxt.

The Analysis Trait

Every RAPx analysis module implements the [Analysis] trait defined in rapx/src/analysis/mod.rs:

#![allow(unused)]
fn main() {
pub trait Analysis {
    fn run(&mut self);
}
}

Each analysis module provides a concrete struct that implements Analysis and executes the analysis when run() is called. Specialized subtraits (e.g., AliasAnalysis, DataflowAnalysis, RangeAnalysis) extend Analysis with query methods for their specific results.

Navigating the Compiler API

Common patterns used throughout RAPx:

#![allow(unused)]
fn main() {
// Iterate all function definitions in the local crate
for local_def_id in tcx.iter_local_def_id() {
    if matches!(tcx.def_kind(local_def_id), DefKind::Fn | DefKind::AssocFn) {
        let def_id = local_def_id.to_def_id();
        // ...
    }
}

// Get a function's MIR body
let body: &Body<'_> = tcx.optimized_mir(def_id);

// Walk all basic blocks
for (block_idx, bb) in body.basic_blocks.iter().enumerate() {
    for stmt in &bb.statements {
        if let StatementKind::Assign(box (place, rvalue)) = &stmt.kind {
            // handle assignment
        }
    }
    if let Some(terminator) = &bb.terminator {
        match &terminator.kind {
            TerminatorKind::Call { func, args, destination, .. } => { /* ... */ }
            TerminatorKind::SwitchInt { discr, targets } => { /* ... */ }
            TerminatorKind::Return => { /* ... */ }
            _ => {}
        }
    }
}

// Check if a function is unsafe or contains unsafe blocks (HIR-level)
let body_id = tcx.hir_body_id_if_owned(local_def_id);
let is_unsafe = hir_contains_unsafe(tcx, body_id);

// Get function argument count
let argc = body.arg_count;
// _0 = return value, _1.._argc = parameters

// Resolve a callee DefId from a Call terminator
if let Operand::Constant(c) = func {
    if let TyKind::FnDef(callee_def_id, _) = c.const_.ty().kind() {
        let callee_name = tcx.def_path_str(*callee_def_id);
    }
}
}

Stable MIR and Compatibility

The Nightly Dependency

RAPx depends on #![feature(rustc_private)] — it links against the Rust compiler's internal crates (rustc_middle, rustc_hir, rustc_driver, etc.). These APIs are unstable and change with every nightly compiler release. There is no stable compiler plugin API in Rust.

This has practical consequences:

• Pinned toolchain: RAPx ships a rust-toolchain.toml specifying an exact nightly version (e.g., nightly-2026-04-03). Users must install this version.
• Breakage on upgrade: Bumping the nightly version typically requires updating dozens of API calls across the codebase, as MIR statement/terminator variants, field names, and module paths shift.
• Conditional compilation: The compat.rs module (rapx/src/compat.rs) centralizes version-gated re-exports. build.rs detects the rustc version at build time and sets cfg flags like rapx_rustc_ge_193, rapx_rustc_ge_196, rapx_rustc_ge_198, rustc_spanned_at_root, etc. Source files use these flags to adapt to API changes without duplicating version checks.

Example from compat.rs:

#![allow(unused)]
fn main() {
// Spanned moved from rustc_span::source_map to rustc_span root in rustc 1.97
#[cfg(rustc_spanned_at_root)]
pub use rustc_span::Spanned;
#[cfg(not(rustc_spanned_at_root))]
pub use rustc_span::source_map::Spanned;
}

And a typical usage pattern in analysis code:

#![allow(unused)]
fn main() {
#[cfg(rapx_rustc_ge_198)]
let field_ty = field.ty(self.tcx, substs).skip_norm_wip();
#[cfg(not(rapx_rustc_ge_198))]
let field_ty = field.ty(self.tcx, substs);
}

The CI (rapx/.github/workflows/test.yml) tests against multiple nightly versions to catch regressions early.

Stable MIR (SMI)

The Rust compiler team is developing Stable MIR, an alternative API that provides a versioned, stable interface to compiler internals. It exposes MIR bodies, types, and associated metadata through a crate (rustc_smir) that abstracts over the internal representation. The goal is to allow external tools to query MIR without tracking nightly churn.

However, Stable MIR has limitations that make it unsuitable for RAPx's current needs:

• Read-only access: SMI provides MIR introspection but does not expose the full compiler callback infrastructure (rustc_driver::Callbacks, after_analysis, RUSTC_WRAPPER hook). RAPx needs to intercept compilation and run analyses between type checking and codegen.
• Limited HIR access: RAPx uses HIR for attribute scanning (#[rapx::verify], #[rapx::requires]) and fast pre-filtering (hir_contains_unsafe). SMI focuses on MIR and does not expose HIR.
• Evolving coverage: SMI does not yet expose all MIR constructs that RAPx depends on (e.g., TerminatorKind::InlineAsm, StatementKind::Intrinsic, certain AggregateKind variants).
• No standard library integration: RAPx links against core/alloc/std to build contract databases and call effect summaries. SMI targets external tooling that operates on already-compiled crates.

RAPx tracks the Stable MIR effort and may adopt it for MIR querying in the future, while retaining nightly-only hooks for compilation interception and HIR access. The compat.rs abstraction layer is designed to make such a migration feasible: most analysis code already imports compiler types through centralized re-exports rather than directly from rustc_middle.

Chapter 5. Analysis

This chapter introduces the analysis modules of RAPx, which implement commonly used program analysis features including path analysis, alias analysis, dataflow analysis, control-flow analysis, safety-flow analysis, and more. Please refer to the corresponding sub-chapters for more information.

Layered Design

Since many static analysis tasks are inherently undecidable due to Rice's Theorem, the analysis modules adopt a layered design that enables users to customize their own analysis routines:

• Analysis trait (top layer): Defines run() — the minimum interface every analysis must implement.
• Feature subtrait (middle layer): Each analysis category (e.g., AliasAnalysis, DataflowAnalysis) extends Analysis with domain-specific query methods.
• Default implementation (bottom layer): A struct (e.g., AliasAnalyzer, DataflowAnalyzer) provides a concrete algorithm implementing the subtrait.

Users can utilize a feature by creating an instance of the struct and invoking run(), or implement their own subtrait to plug in an alternative algorithm:

#![allow(unused)]
fn main() {
pub trait Analysis {
    fn run(&mut self);
}

pub trait AliasAnalysis: Analysis {
    fn get_fn_alias(&self, def_id: DefId) -> Option<FnAliasPairs>;
    fn get_all_fn_alias(&self) -> FnAliasMap;
    fn get_local_fn_alias(&self) -> FnAliasMap;
}

pub struct AliasAnalyzer<'tcx> { /* ... */ }

impl Analysis for AliasAnalyzer<'tcx> { /* ... */ }
impl AliasAnalysis for AliasAnalyzer<'tcx> { /* ... */ }
}

Chapter 5.1. Path Analysis

Path analysis extracts finite, acyclic execution paths from a function's control-flow graph (CFG). It is a foundational module — the alias analysis, SafeDrop dangling pointer detection, range analysis, and the verification pipeline all depend on the path enumeration and reachability checking infrastructure provided by this module. The implementation lives at rapx/src/analysis/path/.

5.1.1 Motivation: Meet-Over-Paths Analysis

Traditional dataflow analysis frameworks typically use chaotic iteration — a MOP (Merge Over Paths) approach that iteratively propagates abstract states across all CFG edges until convergence. For languages with simple branch conditions (e.g., integer comparisons), this works well because the state space is compact and every edge is reachable under some input.

Rust presents a fundamentally different challenge: enum types produce correlated branch conditions that make many structurally possible paths mutually exclusive. Consider a function that pattern-matches the same Option<T> or Result<T,E> twice:

#![allow(unused)]
fn main() {
fn example(x: Option<i32>) -> i32 {
    let a = match x {
        Some(_) => 1,
        None => -1,
    };
    match x {
        Some(_) => a + 1,
        None => a - 1,
    }
}
}

Structurally, the CFG has 2 × 2 = 4 paths through the two match statements. But only 2 are actually reachable: if x was Some at the first match, it must also be Some at the second. The possible return values are 1 + 1 = 2 and -1 - 1 = -2. A chaotic-iteration analysis treats all edges as independent and would merge abstract states from all four routes at every join point, losing the correlation that both match statements depend on the same x. This over-approximation produces spurious state combinations — for instance, the crossed paths would suggest return values of 1 - 1 = 0 and -1 + 1 = 0, making 0 a false positive that compounds with each additional match or if let in the function.

Path analysis addresses this by explicitly enumerating CFG paths and then filtering them with discriminant-constraint checking. Each surviving path carries a consistent set of branch decisions, and downstream analyses process each path independently without merging incompatible states. This is the essence of the meet-over-paths approach: the meet (merge) operation is applied over a set of validated paths rather than over all structurally possible edges.

5.1.2 Path Extraction

Given a MIR function body, the path extraction module answers: what are all the structurally possible CFG paths from function entry to each exit point? The key challenge is loops: each strongly connected component (SCC) in the CFG introduces cyclic back-edges that make a naive enumeration unbounded. RAPx solves this by decomposing SCCs into a hierarchical tree (Section 5.1.2.1) and applying controlled unrolling (Section 5.1.2.2). Structurally valid but semantically impossible paths are then filtered out through discriminant tracking, constant propagation, and SCC context deduplication (Section 5.1.2.3).

5.1.2.1 Natural Loops and SCC Trees

The key insight enabling finite path enumeration is that every loop in Rust MIR is a natural loop. A natural loop has a single dominator (entry block) through which all paths into the loop must pass. This property enables constructing a hierarchical SCC tree:

1. SCC Detection: The CFG is decomposed into strongly connected components (SCCs). Each SCC corresponds to a loop region.
2. Dominator Identification: For each SCC, the block that dominates all SCC members is the loop's entry.
3. SCC Tree Construction: Nested SCCs form a tree — the outermost SCC is the root, children are nested sub-SCCs, and further nesting continues recursively.

         ┌──────────────────────────────────┐
         │  Outer SCC (root)                │
         │  dominator: bb1                  │
         │  ┌──────────────────────────┐    │
         │  │ Inner SCC A (child)      │    │
         │  │ dominator: bb7           │    │
         │  └──────────────────────────┘    │
         │  ┌──────────────────────────┐    │
         │  │ Inner SCC B (child)      │    │
         │  │ dominator: bb12          │    │
         │  └──────────────────────────┘    │
         └──────────────────────────────────┘

The SCC tree enables top-down recursive unfolding: starting from the outermost SCC, the analysis descends into child SCCs and splices their enumerated internal paths as atomic segments into parent paths. This top-down approach also propagates accumulated path constraints from outer contexts into inner SCCs, so inner path enumeration only explores paths consistent with the outer context.

5.1.2.2 Controlled Loop Unrolling

To keep enumeration finite, the check_postfix_segment mechanism tracks path segments between successive visits to the same SCC dominator:

• A postfix segment is the block sequence from one visit to the SCC dominator until the next visit to that same dominator.
• Each distinct postfix segment is counted. The first occurrence is always allowed; subsequent occurrences are limited to postfix_repeat times. Beyond that, the branch is pruned.
• postfix_repeat = 0 (default): each distinct segment appears at most once (the initial occurrence), producing the minimum set of structurally distinct paths.
• postfix_repeat = N: allows N extra repetitions of the same segment, useful for analyses that need multi-iteration loop coverage.

A segment is only worth further exploration if its most recent traversal introduces at least one previously unvisited node. Traversals that merely repeat an already-seen sequence without new blocks are pruned immediately.

5.1.2.3 Pruning Infeasible Paths

Structural enumeration produces many paths that are semantically impossible — for example, taking the Some branch after having already taken the None branch on the same Option. RAPx employs three complementary pruning layers to filter out infeasible paths:

1. Discriminant-based filtering (check_transition): As the DFS traverses CFG edges, each transition through a SwitchInt terminator records the discriminant's concrete value in a constraint map. When the same discriminant is tested again later in the path, the existing constraint is checked — any transition that contradicts the known value is immediately pruned. This handles correlated match/if let branches on enum types and immutable booleans without requiring full SMT solving.

2. Constant propagation: Each block's BlockConstantInfo records which locals received constant assignments (from const rvalues or ADT constructors). As constraints flow through check_transition, copy chains are forwarded and unknown assignments invalidate relevant entries. This extends discriminant tracking to cases where the value propagates through temporary locals and copy operations.

3. SCC context deduplication (visited_sccs): When a nested SCC is reached via multiple parent paths, re-enumerating its internal sub-paths is redundant if the accumulated constraint state is identical. constraint_context hashes all (local → constant_value) bindings accumulated along the path prefix into a ConstraintHash. Before expanding a child SCC, dfs_scc_tree checks whether this hash has been seen before — if so, the expansion is skipped, avoiding combinatorial blowup. The hash naturally distinguishes genuinely different contexts (e.g., inner loop executed vs. skipped) while collapsing identical ones.

Together, these three layers dramatically reduce the number of paths that survive into the PathTree. The first two layers eliminate provably infeasible transitions; the third trades soundness for scalability by assuming that identical constraint fingerprints imply identical sub-path behavior. Example 2 (Section 5.1.3.2) demonstrates discriminant + constant filtering, while Example 3 (Section 5.1.3.3) illustrates the trade-off introduced by SCC context deduplication.

5.1.3 Examples

5.1.3.1 Example 1: Correlated Enum Branches (path_1)

Recall the example(x: Option<i32>) function from Section 5.1.1. Its MIR (cargo rapx analyze mir) contains two SwitchInt terminators on the same discriminant _1:

bb0:  _3 = discriminant(_1); switchInt(_3) -> [0: bb2, 1: bb3, otherwise: bb1]
bb1:  unreachable
bb2:  _2 = const -1_i32; goto bb4          // a = -1 (None)
bb3:  _2 = const 1_i32;  goto bb4          // a = 1  (Some)
bb4:  _4 = discriminant(_1); switchInt(_4) -> [0: bb5, 1: bb6, otherwise: bb1]
bb5:  _0 = Sub(_2, 1); goto bb9            // return a - 1
bb6:  _0 = Add(_2, 1); goto bb9            // return a + 1
bb9:  return

No loops — the CFG is a DAG. Path analysis (cargo rapx analyze paths) produces 2 paths:

Function: "example":
  Path [0, 3, 4, 6, 7, 9]    // Some → Some, returns 2
  Path [0, 2, 4, 5, 8, 9]    // None → None, returns -2

Structurally the two SwitchInt terminators create 2 × 2 = 4 combinations. Incremental constraint filtering via check_transition (see Section 5.1.2.3) prunes the crossed branches (None → Some and Some → None), leaving only the 2 consistent paths.

5.1.3.2 Example 2: Nested SCCs with Constraint Filtering (path_5)

The test at rapx/tests/analyze/path_5/src/lib.rs has two nested loops with boolean guards that the constraint system can track:

#![allow(unused)]
fn main() {
fn read2(x: bool) -> Option<u32> {
    let mut outer_retry = true;
    loop {
        let mut inner_retry = true;
        loop {
            if x { return Some(42); }          // bb2 → bb3 (exit via return)
            else if inner_retry { inner_retry = false; continue; }  // bb4 → bb5 → bb2
            else { break; }                    // bb4 → bb6 (break inner loop)
        }
        if outer_retry { outer_retry = false; continue; }  // bb6 → bb7 → bb1
        return None;                           // bb6 → bb8 → bb9 (exit via return)
    }
}
}

The MIR has 10 basic blocks:

bb0: _2 = const true;       goto bb1   // outer_retry = true
bb1: _3 = const true;       goto bb2   // inner_retry = true
bb2: switchInt(_1) → [0: bb4, otherwise: bb3]   // test x
bb3: return Some(42);       goto bb9   // → exit
bb4: switchInt(copy _3) → [0: bb6, otherwise: bb5]  // test inner_retry
bb5: _3 = const false;      goto bb2   // inner_retry = false; continue inner
bb6: switchInt(copy _2) → [0: bb8, otherwise: bb7]  // test outer_retry
bb7: _2 = const false;      goto bb1   // outer_retry = false; continue outer
bb8: return None;           goto bb9   // → exit
bb9: return

SCC structure:

• Inner SCC: {bb2, bb4, bb5}, dominator bb2, back edge bb5 → bb2. Exit: bb2 → bb3 (x = true), bb4 → bb6 (inner break).
• Outer SCC: {bb1, bb2, bb4, bb5, bb6, bb7}, dominator bb1, back edge bb7 → bb1. bb2 is a child SCC of the outer SCC.

Inner SCC Structural Paths

At postfix_repeat = 0, the inner SCC DFS from bb2 enumerates four structurally distinct paths:

The postfix segment [4, 5] appears once in C and D. A second occurrence would repeat the segment and is pruned by check_postfix_segment, so no paths with two inner retries (e.g., 2 → 4 → 5 → 2 → 4 → 5 → 2) are generated.

Combining Across Outer Iterations

The outer SCC DFS splices inner SCC paths as atomic building blocks at each visit to bb2. Each outer iteration picks one inner path (A, B, C, or D), then proceeds through bb6:

• If the inner path exits to bb3 (A or C), the path goes to bb9 via a return — this ends the function.
• If the inner path exits to bb6 (B or D), the path reaches bb6. At bb6, outer_retry is tested: switchInt(copy _2) → [0: bb8, otherwise: bb7].
  • If outer_retry = true (otherwise branch): → bb7 (set outer_retry = false) → bb1 (continue outer loop). The outer postfix segment from bb1 back to bb1 is either [2, 4, 6, 7] (B path) or [2, 4, 5, 2, 4, 6, 7] (D path).
  • If outer_retry = false (0 branch): → bb8 → bb9 (return None). The outer loop ends.

At postfix_repeat = 0, each distinct outer postfix segment appears at most once, so at most three outer iterations are possible (initial entry + two distinct returns to bb1). Structurally, the full CFG paths are all ordered selections of inner SCC paths, terminated by a path whose exit reaches bb9 (A or C for Some, B or D for None). Representative combinations:

Reachability Filtering

Discriminant-based filtering combined with constant propagation (see Section 5.1.2.3) eliminates all but two of the 20 structural paths. The filtering exploits that x is an immutable boolean (SwitchInt discriminant), and inner_retry/outer_retry are assigned constants at well-defined points:

Path [0, 1, 2, 3, 9]                              // x = true
Path [0, 1, 2, 4, 5, 2, 4, 6, 7, 1, 2, 4, 5, 2, 4, 6, 8, 9]  // x = false

5.1.3.3 Example 3: Nested SCCs with Structural Pruning (path_7)

For contrast, this example has two nested loops where the constraint system cannot prune structurally possible but semantically impossible paths. The test lives at rapx/tests/analyze/path_7/src/lib.rs:

#![allow(unused)]
fn main() {
fn walk(rows: i32, cols: i32) -> i32 {
    let mut total = 0;
    let mut r = 0;
    loop {
        if r >= rows { break; }
        let mut c = 0;
        loop {
            if c >= cols { break; }
            total += 1;
            c += 1;
        }
        r += 1;
    }
    total
}
}

The CFG has two back edges, bb8 → bb4 and bb9 → bb1, creating two nested SCCs:

Each SCC can produce two configurations at repeat = 0:

• Inner SCC: skip 4 → 5 (postfix: none), or one body iteration 4 → 6 → 7 → 8 → 4 (postfix: [6, 7, 8]), then exits via 5. A second iteration would repeat [6, 7, 8], which is pruned.
• Outer SCC: the postfix segment between successive visits to 1 is either [3, 4, 5, 9] (inner skip) or [3, 4, 6, 7, 8, 4, 5, 9] (inner body).

Structurally, combining these gives 5 possible paths:

Paths 1–4 all appear in the output; Path 5 never does. The divergence is driven by the visited_sccs cache (see Section 5.1.2.3). Here is what happens during DFS enumeration:

• Path 4 (body then skip): The DFS first reaches bb4 from bb3, enters the inner SCC, and explores the body child (bb4 → bb6 → bb7 → bb8 → bb4 → bb5). Along this path, c and total are mutated — their constant-tracking state is invalidated. The outer SCC loops back to bb1 → bb3 → bb4. At this second visit, the constraint hash differs from the first entry because the body path altered local state. visited_sccs misses, the inner SCC is re-expanded, and this time the skip child (bb4 → bb5) is spliced in, producing body-then-skip.

• Path 5 (skip then body): If the DFS first takes the skip child (bb4 → bb5), no locals are mutated — c remains the constant 0 assigned at bb3. The outer SCC loops back to bb4 with an identical constraint hash. visited_sccs hits and blocks re-expansion, so the body child is never spliced in — skip-then-body is suppressed.

5.1.4 Usage

CLI:

# Default: postfix_repeat = 0
cargo rapx analyze paths

# With controlled SCC segment repetition
cargo rapx analyze paths --postfix-repeat 1

In code:

#![allow(unused)]
fn main() {
use analysis::path::default::PathAnalyzer;

let mut analyzer = PathAnalyzer::new(tcx, false);  // false = no debug output
analyzer.analyze_all();                        // postfix_repeat = 0
// or: analyzer.analyze_all_repeat(1);         // postfix_repeat = 1
let all_paths = analyzer.get_all_paths();      // FxHashMap<DefId, PathTree>
let fn_paths = analyzer.analyze(def_id);       // single function
}

Paths are stored in a PathTree (prefix-tree), keyed by DefId. See the source for the full API — PathGraph for CFG+SCC+constraint checking, PathEnumerator for DFS enumeration with SCC caching.

5.1.5 Relationship to Other Modules

• Alias Analysis: The MOP-based AliasGraph wraps a PathGraph for path-sensitive alias checking. SCC decomposition, top-down traversal, and incremental constraint filtering are all shared.
• SafeDrop: Reuses PathGraph for path-sensitive dangling pointer detection with per-block alias facts tracked along enumerated paths.
• Verification: PathExtractor wraps PathGraph and uses PathEnumerator to find paths reaching specific unsafe callsites. The postfix_repeat parameter controls SCC postfix repetition.
• Range Analysis: PathAnalyzer::analyze(def_id) is used to obtain per-function PathTrees for path-constraint extraction in RangeAnalyzer.

Chapter 5.2. Alias Analysis

Alias analysis determines whether two program places (variable references, raw pointers, or their fields) point to the same memory allocation at a given program point. The task is challenging, with various options that balance precision and cost, including flow sensitivity, field sensitivity, and path sensitivity. RAPx provides two complementary approaches:

• MOP (Meet-Over-all-Paths): Path-sensitive enumeration with path reachability filtering, field-sensitive, context-insensitive.
• MFP (Maximum Fixed Point): A lattice-based dataflow analysis using the rustc_mir_dataflow framework, path-insensitive but efficient for complex control flow.

Both approaches implement the AliasAnalysis trait, which defines a uniform query interface.

5.2.1 AliasAnalysis Trait

RAPx provides the AliasAnalysis trait for alias analysis. The trait enables users to query the aliases among the arguments and return value of a function based on the function DefId, or the aliases of all functions as an FxHashMap. Developers can implement the trait based on their needs.

#![allow(unused)]
fn main() {
pub trait AliasAnalysis: Analysis {
    fn get_fn_alias(&self, def_id: DefId) -> Option<FnAliasPairs>;
    fn get_all_fn_alias(&self) -> FnAliasMap;
    fn get_local_fn_alias(&self) -> FnAliasMap;
}
}

The alias analysis result for each function is stored as FnAliasPairs, containing a HashSet of AliasPair instances:

#![allow(unused)]
fn main() {
pub struct FnAliasPairs {
    arg_size: usize,
    alias_set: HashSet<AliasPair>,
}

pub struct AliasPair {
    pub left_local: usize,       // parameter id; return value is `0`
    pub lhs_fields: Vec<usize>,  // field-sensitive: sequence of field numbers
    pub right_local: usize,
    pub rhs_fields: Vec<usize>,
}
}

Each AliasPair records an alias relationship between two program places, expressed as (parameter_id.field_seq, parameter_id.field_seq). The return value is assigned index 0, and function parameters use indices 1, 2, ..., arg_count. For example, (0, 1.1) means the return value aliases with the second field of the first parameter.

5.2.2 MOP-Based Alias Analysis

The MOP-based alias analysis achieves path sensitivity by enumerating distinct CFG paths and performing alias checks independently on each path, then merging results. The implementation lives at rapx/src/analysis/alias/default/.

5.2.2.1 Architecture: AliasGraph

The central data structure is AliasGraph, which wraps a PathGraph and layers alias-specific state on top:

#![allow(unused)]
fn main() {
pub struct AliasGraph<'tcx> {
    pub path_graph: PathGraph<'tcx>,
    pub constants: FxHashMap<usize, usize>,
    pub visit_times: usize,
    pub values: Vec<Value>,
    pub block_facts: Vec<AliasBlockFacts<'tcx>>,
    pub alias_sets: Vec<FxHashSet<usize>>,
    pub ret_alias: MopFnAliasPairs,
    pub arg_size: usize,
    pub span: Span,
}
}

Key fields:

• path_graph: The PathGraph providing CFG topology, SCC decomposition, and path reachability filtering.
• values: Heap-allocated nodes representing program places (locals and their field projections). Each Value records the originating MIR local, drop properties (may_drop, need_drop), a kind (RawPtr, Ref, etc.), and optional father information for field projections.
• block_facts: Per-block assignments and constant values extracted from MIR. Each AliasBlockFacts contains Assignment records (Copy, Move, InitBox, Variant) and ConstValue records.
• alias_sets: A flat vector of alias equivalence classes, each represented as an FxHashSet<usize>. Membership lookup uses linear scan over sets (distinct from the union-find structure used in MFP).
• ret_alias: The accumulated alias results for the function (MOP version with drop metadata).

5.2.2.2 Path-Sensitive Analysis via PathGraph Integration

The MOP analysis integrates with PathGraph for path-sensitive traversal. The overall flow in AliasGraph is:

1. AliasGraph::new() creates a PathGraph for the function and initializes values from MIR locals with drop and type information.
2. For each MIR basic block, AliasGraph extracts AliasBlockFacts — assignments (_1 = copy _2, _1 = move _2, _1 = &_2, _1 = &raw _2), aggregate initializations (tuples, structs decomposed field-by-field for field sensitivity), and constant values.
3. find_scc() delegates to PathGraph::find_scc(), reusing the same SCC tree decomposition and top-down traversal strategy.
4. process_function_paths() walks each enumerated path block-by-block. For each block, it calls:
   • alias_bb(): Processes intra-block assignments — copies values from right-hand to left-hand sides, syncs field aliases, and propagates father aliases.
   • alias_bbcall(): Handles call terminators — looks up the callee's alias summary, maps formal parameters to actual arguments, and merges the callee's alias relationships into the caller's alias sets.
5. After processing all paths, merge_results() collects alias pairs among function parameters and the return value, performs alias compression (field truncation and containment merging), and stores the result in ret_alias.

The path sensitivity is achieved by processing each PathGraph-enumerated path independently: process_function_paths() maintains path-local alias_sets and values state, resetting between paths. The reachability filtering from PathGraph prunes infeasible paths early via check_segment_reachability_with().

5.2.2.3 Feature: Path Reachability Filtering

The MOP-based alias analysis enumerates structurally distinct CFG paths. However, correlated branch conditions on the same discriminant can make certain combinations unreachable — for example, taking the First branch of a match after having already taken the Second branch on the same Selector. PathGraph provides check_segment_reachability_with() to prune such infeasible paths during enumeration, using the discriminant constraint tracking described in Section 5.1.2.3.

For example:

#![allow(unused)]
fn main() {
enum Selector { First, Second }

fn foo<'a>(x: &'a i32, y: &'a i32, choice: Selector) -> &'a i32 {
    let a = match choice {
        Selector::First => x,
        Selector::Second => y,
    };
    match choice {
        Selector::First => a,
        Selector::Second => x,
    }
}
}

• Without path filtering: 4 paths, merged result {(0,1), (0,2)} — incorrectly suggests the return value may alias y.
• With path filtering: 2 reachable paths, result {(0,1)} — correctly excludes the impossible y alias.

5.2.2.4 SCC Handling via PathGraph

A major challenge for path-sensitive analysis lies in the presence of strongly connected components (SCCs), since loops may induce an unbounded number of execution paths. The alias analysis addresses this by leveraging the SCC tree decomposition and path enumeration infrastructure provided by the Path Analysis module. Key observations specific to alias analysis:

• Traversing the same loop path once or multiple times does not change the resulting alias relationships — aliases are determined by value flow, not by iteration count.
• The top-down recursive SCC traversal enables propagating outer context constraints (e.g., discriminant values established before loop entry) into inner SCCs, pruning unreachable paths early.

The MOP analysis uses postfix_repeat = 0 (each distinct SCC segment appears once) by default, which is sufficient for alias relationships that are idempotent under loop iteration.

In the following, we use a concrete example to demonstrate how path-sensitive SCC handling enables precise alias discovery.

#![allow(unused)]
fn main() {
enum Selector { First, Second }

// Expected alias analysis result: (0, 1) (0, 2)
fn foo(x: *mut i32, y: *mut i32, choice: Selector) -> *mut i32 {
    let mut r = x;
    let mut q = x;

    unsafe {
        while *r > 0 {
            let mut p = match choice {
                Selector::First => y,
                Selector::Second => x,
            };

            loop {
                r = q;
                q = match choice {
                    Selector::First => x,
                    Selector::Second => p,
                };
                *q -= 1;
                if *r <= 1 { break; }
                q = y;
            }

            if *r == 0 { break; }
        }
    }

    r
}
}

The annotated MIR for this function contains approximately 27 basic blocks. The SCC tree has two levels: the outer SCC is dominated by the block checking *r > 0, and a nested inner SCC dominated by the block entering the loop { ... }.

We enumerate paths through the SCC tree in a recursive, top-down manner. A path segment between two occurrences of the same dominator is worth exploring only if it introduces at least one previously unvisited node. For instance, the segment 7 → 8 → 10 → ... → 7 followed by 7 → 9 → 10 → ... → 7 is valuable because the second repetition introduces block 9, which may lead to new alias relationships.

Using postfix_repeat = 0 (each distinct segment appears once), the inner SCC produces 10 structurally distinct paths. The path 7-9-10-21-24-11-20-25-19-13-7-9-10-21-24-11-20-25-19-26 effectively detects the alias relationship between r and y. In contrast, a straightforward DFS-based traversal fails to detect this alias relationship.

The alias analysis adopts a recursive, top-down strategy that propagates accumulated path constraints from outer SCCs inward. When reaching an inner SCC, constraints from the outer context determine which of the enumerated paths are reachable. For each reachable path, the inner SCC subsequence is concatenated with the outer SCC path, and alias analysis continues along the resulting trace.

5.2.2.5 Inter-Procedural Alias Resolution

When encountering a function call in the MIR, alias_bbcall() resolves aliases across function boundaries:

1. Checks fn_map for an existing callee summary. If found, uses it directly.
2. If not found, recursively creates a new AliasGraph for the callee, runs find_scc() and process_function_paths(), caches the result, and uses it.
3. A recursion_set tracks functions currently being analyzed to prevent infinite recursion in the case of mutually recursive functions. If the callee is already in the recursion_set, it is conservatively skipped.
4. handle_fn_alias() maps callee-formal positions to caller-actual value indices, constructing field projections on-the-fly if the callee's alias references fields not yet materialized in the caller's value graph.

5.2.2.6 Feature: Field Sensitivity

The MOP analysis is field-sensitive — it tracks aliases at the level of struct/tuple fields. This is achieved through:

• Value projection: Each struct field access creates a Value node with father pointing to the parent value and the field index. The projection() method recursively descends through ProjectionElem::Field, creating field nodes on demand. ProjectionElem::Deref is skipped without materialising a new node, so multi-level pointer aliases are not tracked.
• sync_field_alias(): When two values are aliased, their corresponding fields are also aliased recursively (up to MAX_FIELD_DEPTH = 10). The total number of value nodes per path is also bounded by MAX_VALUES_PER_PATH = 1000.
• sync_father_alias(): When a value is aliased, all aliases of its parent receive corresponding field projections, enabling transitive field-level aliasing.
• Alias compression: After path traversal, compress_aliases() performs field truncation (collapsing multi-level field projections to the first level) and containment merging (removing redundant sub-field aliases when a coarser alias already captures the relationship).

For example:

#![allow(unused)]
fn main() {
struct Point { x: i32, y: i32 }

fn foo(p1: &Point) -> &i32 {
    &p1.y
}
}

The result is (0, 1.1) — the return value aliases with field 1 (y) of the first parameter.

5.2.2.7 Key Steps of the MOP Algorithm

#![allow(unused)]
fn main() {
let mut alias_graph = AliasGraph::new(tcx, def_id);
alias_graph.find_scc();
alias_graph.process_function_paths(&mut fn_map, &mut recursion_set);
let result = alias_graph.ret_alias; // MopFnAliasPairs
}

1. Create AliasGraph wrapping a PathGraph, extract MIR locals into values, and extract per-block AliasBlockFacts from MIR statements and terminators.
2. Delegate to PathGraph::find_scc() for hierarchical SCC tree construction.
3. process_function_paths() walks each path, calling alias_bb() and alias_bbcall() per block, building alias_sets along the way, then merge_results() extracts and compresses the final alias pairs.

Reference

The MOP alias analysis is based on our SafeDrop paper, published in TOSEM:

@article{cui2023safedrop,
  title={SafeDrop: Detecting memory deallocation bugs of rust programs via static data-flow analysis},
  author={Mohan Cui, Chengjun Chen, Hui Xu, and Yangfan Zhou},
  journal={ACM Transactions on Software Engineering and Methodology},
  volume={32}, number={4}, pages={1--21}, year={2023},
  publisher={ACM New York, NY, USA}
}

5.2.3 MFP-Based Alias Analysis

In addition to the MOP approach, RAPx provides an alternative alias analysis implementation based on the MFP (Maximum Fixed Point) framework. The MFP analysis is built on Rust compiler's rustc_mir_dataflow infrastructure, which provides a general-purpose monotone dataflow analysis framework. The implementation lives at rapx/src/analysis/alias/mfp/.

5.2.3.1 Overview

The MFP approach differs fundamentally from MOP in its analysis strategy:

• Path insensitivity: Unlike MOP, which explicitly enumerates and analyzes individual execution paths, MFP merges information from all paths at control-flow join points. This means MFP does not track path-specific constraints (e.g., the value of a discriminant variable across branches).

• Flow sensitivity: Both approaches are flow-sensitive, tracking how alias relationships evolve along the control flow. However, MFP uses a worklist-based fixed-point iteration over the CFG, while MOP performs explicit path enumeration via PathGraph.

• Precision trade-offs: MFP may produce more conservative (over-approximate) results compared to MOP due to path insensitivity, but it can be more efficient for functions with complex control flow where path enumeration becomes expensive.

Example: Path Insensitivity in MFP

#![allow(unused)]
fn main() {
enum Selector { First, Second }

fn foo<'a>(x: &'a i32, y: &'a i32, choice: Selector) -> &'a i32 {
    let a = match choice {
        Selector::First => x,
        Selector::Second => y,
    };
    match choice {
        Selector::First => a,
        Selector::Second => x,
    }
}
}

MOP Analysis (Path-Sensitive):

• Path 1: choice = First → a = x → returns a (i.e., x) → alias (0, 1)
• Path 2: choice = Second → a = y → returns x → alias (0, 1)
• Result: {(0, 1)} (return value aliases only with parameter x)

MFP Analysis (Path-Insensitive):

• After the first match: a may alias with either x or y
• At the second match, both branches are considered reachable:
  • Branch First: returns a, which may be x or y → aliases (0, 1) and (0, 2)
  • Branch Second: returns x → alias (0, 1)
• Join at the merge point: {(0, 1), (0, 2)} (return value may alias with both x and y)
• Result: {(0, 1), (0, 2)} (includes spurious alias with parameter y)

The key difference is that MFP loses the correlation between the two match statements, leading to a spurious alias (0, 2) that MOP correctly excludes.

The MFP alias analyzer is implemented in the MfpAliasAnalyzer struct, which also implements the AliasAnalysis trait. Like the MOP approach, MFP analysis is field-sensitive and context-insensitive, supporting inter-procedural analysis through function summaries.

5.2.3.2 Lattice Design

The MFP approach models alias relationships using a lattice-based abstract domain built on the Union-Find (disjoint-set) data structure.

Abstract Domain

The abstract domain AliasDomain represents alias relationships among program places:

#![allow(unused)]
fn main() {
pub struct AliasDomain {
    parent: Vec<usize>,   // Parent array for Union-Find
    rank: Vec<usize>,     // Rank for union-by-rank optimization
}
}

Each place in the program is assigned a unique index, and the Union-Find structure tracks equivalence classes of aliased places. Two places are considered aliased if they belong to the same equivalence class (i.e., they have the same root).

Lattice Structure

The AliasDomain forms a join semi-lattice:

• Bottom (⊥): The initial state where no aliases exist. Each place is in its own equivalence class: parent[i] = i.
• Partial Order (⊑): Domain D₁ ⊑ D₂ if every alias pair in D₁ is also present in D₂.
• Join Operation (⊔): D₁ ⊔ D₂ produces a domain containing all alias relationships from both, implemented by extracting all alias pairs from one domain and unioning them in the other.

Monotonicity and Convergence

The lattice design ensures monotonicity: transfer functions always produce domains that are higher in the lattice. Combined with the finite height of the lattice (bounded by the number of possible alias pairs), the fixed-point iteration is guaranteed to converge.

Union-Find operations: find (O(α(n)) amortized), union (O(α(n)) amortized), where α(n) is the inverse Ackermann function.

5.2.3.3 Transfer Functions

The MFP analysis defines transfer functions for each type of MIR statement and terminator using a Kill-Gen pattern.

Kill-Gen Pattern

For an assignment lv = ...:

1. Kill: Remove all existing aliases involving lv and its field projections. Implemented via remove_aliases_with_prefix().
2. Gen: Establish new alias relationships based on the right-hand side.

Assignment: lv = rv

For Copy or Move assignments:

• Kill lv and all field projections.
• If rv is a place: union lv with rv, then sync_fields recursively.

Reference Creation: lv = &rv or lv = &raw rv

Creates an alias between the reference lv and the referent rv:

• Kill old aliases of lv.
• Union lv with rv, sync fields.

Aggregate Construction: lv = (op₁, op₂, ...)

For tuples and structs, each field is handled individually for field sensitivity:

• Kill lv and all its fields.
• For each field i: union lv.i with operand[i], sync fields.

Field Synchronization

When two places are aliased, their corresponding fields are also aliased recursively (up to MAX_SYNC_DEPTH = 3). The sync_fields function iterates over common field indices (0..16) and unions matching fields.

Function Calls: ret = f(args)

1. Kill: Remove aliases for the return place ret.
2. Gen: Apply the callee's function summary: map formal parameter indices to actual argument place indices, union the return place with the corresponding argument.

5.2.3.4 Intraprocedural Analysis

The intraprocedural analysis is implemented by FnAliasAnalyzer, which implements rustc_mir_dataflow::Analysis.

PlaceInfo: Field-Sensitive Place Management

PlaceInfo tracks all program places and their properties:

#![allow(unused)]
fn main() {
pub struct PlaceInfo<'tcx> {
    place_to_index: FxHashMap<PlaceId, usize>,
    index_to_place: Vec<PlaceId>,
    may_drop: Vec<bool>,
    need_drop: Vec<bool>,
    num_places: usize,
}
}

Places are represented by the recursive PlaceId:

#![allow(unused)]
fn main() {
pub enum PlaceId {
    Local(usize),                        // A local variable
    Field { base: Box<PlaceId>, field_idx: usize },  // A field projection
}
}

This enables precise tracking of aliases at the field level. During initialization, PlaceInfo::build recursively creates field projections for struct and tuple types, bounded by MAX_FIELD_DEPTH = 5 and MAX_DEREF_DEPTH = 3.

Fixed-Point Iteration

The dataflow analysis uses the standard worklist algorithm:

• OUT[B] = F_B(IN[B]): Output state = transfer function applied to input.
• IN[B] = ⊔_{P ∈ pred(B)} OUT[P]: Input state = join of all predecessor outputs.

Iteration continues until a fixed point is reached (no block's output changes).

5.2.3.5 Interprocedural Analysis

The MFP approach achieves inter-procedural precision through function summaries and global fixed-point iteration.

Function Summaries

A function summary captures alias relationships between parameters and the return value as a set of AliasPair instances. Since aliases may be connected through temporary variables, summary extraction performs a transitive closure to identify all parameter-return alias relationships.

The extracted candidates are normalized and filtered:

• Self-aliases (0, 0) are removed.
• Prefix-subsumed aliases are removed (e.g., (0, 1) subsumes (0.0, 1.0)).

Global Fixed-Point Iteration

The interprocedural analysis operates in three phases:

1. Starting from local crate functions, recursively traverse call sites to collect all reachable function DefIds.

2. All reachable functions start with empty summaries (⊥ or FnAliasPairs::new(arg_count)).

3. Iterate to fixed point (up to MAX_ITERATIONS = 10):

   • Sync current summaries to shared storage.
   • Re-analyze each function with the latest callee summaries.
   • If no summary changes, convergence is reached.

This outer iteration ensures that when analyzing a function f that calls g, the analysis uses the most up-to-date summary of g.

5.2.4 Quick Usage Guide

# MOP-based alias analysis (default)
cargo rapx analyze alias

# MFP-based alias analysis
cargo rapx analyze alias -s mfp

Example output for MOP:

Checking alias_mop_field...
21:50:18|RAP|INFO|: Alias found in Some("::foo"): {(0,1.1),(0,1.0)}
21:50:18|RAP|INFO|: Alias found in Some("::boxed::{impl#0}::new"): {(0.0,1)}

To use analysis results in code:

#![allow(unused)]
fn main() {
// MOP-based approach
let mut alias_analysis = AliasAnalyzer::new(tcx);
alias_analysis.run();
let result = alias_analysis.get_local_fn_alias();
rap_info!("{}", FnAliasMapWrapper(result));
}

#![allow(unused)]
fn main() {
// MFP-based approach
let mut analyzer = MfpAliasAnalyzer::new(tcx);
analyzer.run();
let alias = analyzer.get_local_fn_alias();
rap_info!("{}", FnAliasMapWrapper(alias));
}

Chapter 5.3. API-Dependency Graph

Overview

The API Dependency Graph is a directed graph structure that models dependencies among APIs, types, and generic parameters by traversing the APIs within a Rust library or crate. It contains three types of nodes: API, type and generic parameter. And it contains four types of edges : Arg(usize, recording the location in API parameter), Ret, Generic and Transform(TransformKind, recording the relation between types, such as T and &T, &mut T). Now this module is still under development and generic is not supported.

Use the following example to demonstrate this graph structure.

#![allow(unused)]
fn main() {
pub struct S1 {
    pub a: i32,
    pub b: f32,
}

pub struct S2 {
    pub a: i32,
    pub b: f32,
}

pub struct S3 {
    pub a: i32,
    pub b: f32,
}

pub fn api1(arg1: i32, arg2: &f32) -> S1 {
    S1 { a: arg1, b: *arg2 }
}
pub fn api2(arg1: &mut i32, arg2: f32) -> S2{
    S2 { a: *arg1, b: arg2 }    
}

pub fn api3(arg1: &S1, arg2: &S2) -> S3{
    S3 { a: arg1.a, b: arg2.b }
}
}

By scanning the code above, we generate an API Dependency Graph like this:

Quick Usage Guide

If your project doesn't have a rust-toolchain.toml, you need to create such a file contains the following content:

[toolchain]
# The default version of the rustc compiler
channel = "nightly-2026-04-03"
components = ["rustc-dev", "rust-src", "llvm-tools-preview"]

We use this feature for generating fuzz targets about library APIs. You can use this feature with the following command(Make sure you are in a cargo project):

cargo rapx analyze adg

This command will analyse your project and gengerate a .dot file in the current directory, which contains the API dependency graph information, and also generate a new project in the parent directory. The new project is a fuzz target that contains APIs in your project.You can visualize this graph by using one of the following commands.

dot -Tsvg your_crate_name.dot -o api_graph.svg
dot -Tpng your_crate_name.dot -o api_graph.png

To utilize the analysis results, you can use the module as follows:

#![allow(unused)]
fn main() {
use analysis::api_dependency::{ApiDependencyAnalyzer, Config}; // Import the module
let config = Config::default();
let mut api_graph = ApiDependencyAnalyzer::new(tcx, config);
api_graph.run();
}

The above codes can generate an API dependency graph based on your crate.

Graph APIs

The ApiDepGraph struct provides several APIs for interacting with the dependency graph. Below are the key methods. Before using these APIs, you need to import relevent module:

#![allow(unused)]
fn main() {
use analysis::api_dependency::graph; // Import the module
}

statistics

Returns statistics about the graph, including counts of API nodes, type nodes, generic parameter nodes, and edges.

#![allow(unused)]
fn main() {
// Here is the definition of Statistics
pub struct Statistics {
    pub num_api: usize,
    pub num_generic_api: usize,
    pub type_count: usize,
    pub edge_cnt: usize,
}
pub fn statistics(&self) -> Statistics
}

inner_graph

Returns reference of the graph data.

#![allow(unused)]
fn main() {
pub fn inner_graph(&self) -> &InnerGraph<'tcx> // InnerGraph is Graph<DepNode<'tcx>, DepEdge>
}

get_or_create_index

Retrieves or creates a node index for a given DepNode. If the node doesn't exist in the graph, it will be added.

#![allow(unused)]
fn main() {
pub fn get_or_create_index(&mut self, node: DepNode<'tcx>) -> NodeIndex
}

get_index

Given a DepNode, returns Option<NodeIndex>, since it may not exist in the graph.

#![allow(unused)]
fn main() {
pub fn get_index(&self, node: DepNode<'tcx>) -> Option<NodeIndex>
}

The feature is based on our RuMono paper, which was published in TOSEM.

@article{zhangrumono,
  title={RuMono: Fuzz Driver Synthesis for Rust Generic APIs},
  author={Zhang, Yehong and Wu, Jun and Xu, Hui},
  journal={ACM Transactions on Software Engineering and Methodology},
  publisher={ACM New York, NY}
}

Chapter 5.4. Call Graph Analysis

Overview

A call graph represents calling relationships between subroutines in a computer program. Each node represents a procedure and each edge (f,g) indicates the caller and callee relationship between f and g.

In our program, we provide the feature to generate static call graphs and store the result in a graph data structure implemented with adjacent list.

Quick Start

You can use the feature with the following command:

cargo rapx analyze callgraph

Graph APIs

To utilize the analysis results as you want, you can use our module as follows:

#![allow(unused)]
fn main() {
use analysis::callgraph::default::CallGraphAnalyzer;  // import module
let mut callgraph = CallGraphAnalyzer::new(tcx);    // create a callgraph object
callgraph.run();  // do the analysis
let fn_calls = callgraph.get_fn_calls();  // get all callees for each caller
}

get_fn_calls

#![allow(unused)]
fn main() {
pub fn get_fn_calls(&self) -> FnCallMap
}

Returns a map from each caller DefId to all its callee DefIds.

get_post_order

#![allow(unused)]
fn main() {
pub fn get_post_order(&self) -> Vec<DefId>
}

Returns the functions in post-order traversal of the call graph.

get_reverse_post_order

#![allow(unused)]
fn main() {
pub fn get_reverse_post_order(&self) -> Vec<DefId>
}

Returns the reverse post-order, suitable for bottom-up analyses.

Generating Call Graphs

Working with MIR (Mid-level Intermediate Representation)

MIR is Rust's intermediate representation used during compilation. It simplifies control flow by breaking down functions into a series of basic blocks, making it easier to analyze.

Our program make good use of this handy tool to help generate call graphs. We analyze what specific kind the current basic block belongs to, which represents ways of existing from a basic block.

#![allow(unused)]
fn main() {
pub struct Body<'tcx> {
    pub basic_blocks: BasicBlocks<'tcx>,
    ..
}

}

As basic_blocks exist in the struct Body, we should get Body first. There are some functions to help us with this:

1. optimized_mir
2. mir_for_ctfe ("stfe" stands for "Compile Time Function Evaluation")

In the case of DefKind::Const and DefKind::static, mir_for_ctfe is necessary, since rust prevents us from applying optimization to const or static ones.

Inside the BasicBlockData we can get Terminator.

#![allow(unused)]
fn main() {
pub enum TerminatorKind<'tcx> {
    Call {
        func: Operand<'tcx>,
        ..
    },
    ..
}
}

Our target is to get the Call in the enum TerminatorKind. Therefore we can use the resolve function to get define id of callee functions.

With define id (i.e. def_id), it is easy to apply it to def_path_str method to get define path and construct our call graphs.

Case Study: Dynamic Trait Analysis

It is nontrivial to analyze a program applying dynamic trait. Since we have to do our analysis statically, we guarantee the analysis sound and safe. In the case of dynamic trait analysis, we give out the "maybe" answer, e.g.:

|RAP|INFO|: 8:main -> 7:(dyn trait) <* as Animal>::make_sound

Chapter 5.5. Data-flow Analysis

Data-flow analysis tracks value flow through MIR locals — copy, move, borrow, field projection, dereference, and function calls. It builds a directed graph per function where nodes are MIR Local variables and edges record how values propagate between them. The module lives at rapx/src/analysis/dataflow/ and the core graph types (DataflowGraph, DataflowEdge, etc.) are in rapx/src/analysis/dataflow/types.rs.

Overview

For each function, the analyzer builds a DataflowGraph by visiting every MIR statement and terminator. Each edge in the graph records:

• Source / destination locals
• Edge operation: Copy, Move, Mut (mutable borrow), Immut (shared borrow), Deref, Field(i), Downcast(variant), Index, ConstIndex, Const, SubSlice
• Source location: basic block index and statement index

Each node records the MIR operations that produced its value (NodeOp): Use, Ref, Call(def_id), Cast, BinaryOp, Aggregate(kind), RawPtr, Discriminant, etc.

DataFlowAnalysis Trait

#![allow(unused)]
fn main() {
pub trait DataflowAnalysis: Analysis {
    fn get_fn_dataflow(&self, def_id: DefId) -> Option<DataFlowGraph>;
    fn get_all_dataflow(&self) -> DataFlowGraphMap;
    fn has_flow_between(&self, def_id: DefId, local1: Local, local2: Local) -> bool;
    fn collect_equivalent_locals(&self, def_id: DefId, local: Local) -> HashSet<Local>;
    fn get_fn_arg2ret(&self, def_id: DefId) -> Arg2Ret;
    fn get_all_arg2ret(&self) -> Arg2RetMap;
}
}

• get_fn_dataflow: Returns the full DataFlowGraph for a function.
• has_flow_between: Checks whether a value-flow path exists between two locals, traversing both upside (in-edges) and downside (out-edges) directions.
• collect_equivalent_locals: Finds all locals that are value-equivalent to the given local — traverses upside through Copy/Move/Mut/Immut/Deref edges to find the root, then traverses downside to collect equivalents.
• get_fn_arg2ret / get_all_arg2ret: Returns an IndexVec<Local, bool> mapping each argument to whether a value-flow path connects it to the return value (_0). This is the most commonly used query for downstream analyses.

Quick Usage

cargo rapx analyze dataflow

To enable debug logging and render DOT graphs:

cargo rapx analyze dataflow --debug --draw

In code:

#![allow(unused)]
fn main() {
let mut analyzer = DataflowAnalyzer::new(tcx, false);
analyzer.run();
let arg2ret = analyzer.get_all_arg2ret(); // Arg2RetMap
rap_info!("{}", Arg2RetMapWrapper(arg2ret));
}

Value Flow Graph Construction

DataflowAnalyzer::build_graphs() iterates over all local function definitions (iter_local_def_id) and calls build_graph for each Fn or AssocFn. The graph is built in DataflowGraph::add_statm_to_graph and add_terminator_to_graph by matching on each MIR statement kind:

Assignments (StatementKind::Assign)

For lv = rv:

Place Projections

When the left-hand side contains projections (e.g., (*ptr).field), intermediate nodes are created for each projection step:

• Deref — a new node with a Deref edge from the base pointer
• Field(i) — a new node with a Field(i) edge from the base struct/tuple
• Downcast(variant) — a new node with a Downcast edge from the enum
• Index — a new node with Index and Nop edges from the index operand

Call Terminators (TerminatorKind::Call)

For dst = f(args):

• If f is a known FnDef, each argument is connected to dst with the corresponding edge operation. The node is marked with NodeOp::Call(def_id).
• If f is a dynamic operand (trait object / function pointer), the function operand and arguments are connected to dst, marked NodeOp::CallOperand.

Constants

Constant operands create a synthetic marker node with NodeOp::Const(desc, ty) connected to the destination via a Const edge. This distinguishes constant-origin values from value-flow between program variables.

Graph Queries

DFS Traversal

The dfs method provides directional graph traversal:

#![allow(unused)]
fn main() {
pub fn dfs<F, G>(
    &self,
    now: Local,
    direction: Direction,    // Upside | Downside | Both
    node_operator: &mut F,   // FnMut(&DataflowGraph, Local) -> DFSStatus
    edge_validator: &mut G,  // FnMut(&DataflowGraph, EdgeIdx) -> DFSStatus
    traverse_all: bool,      // continue after finding target?
    seen: &mut HashSet<Local>,
) -> (DFSStatus, bool)
}

The traverse_all flag controls behavior: false stops immediately upon finding a target; true exhaustively visits all reachable nodes allowed by the validators. This is the foundation for is_connected, collect_equivalent_locals, collect_ancestor_locals, and collect_descending_locals.

Param-to-Return Dependencies

param_return_deps() is built on is_connected: for each argument _1.._n, it checks whether a value-flow path exists to _0. The result is IndexVec<Local, bool>.

Equivalent Locals

collect_equivalent_locals() finds all locals that hold the same value as the given local. It works in two phases:

1. Traverse upside through value-preserving edges (Copy, Move, Mut, Immut, Deref) to find the root.
2. Traverse downside from the root through the same edge types, collecting all reachable locals.

Field Sequence

get_field_sequence() traces upside through Field(i) edges to reconstruct the field access path (e.g., _1.0.2), returning the base local and the ordered sequence of field indices.

Example: create_vec

Consider the following function:

#![allow(unused)]
fn main() {
fn create_vec() -> *mut Vec<i32> {
    let mut v = Vec::new();
    v.push(1);
    &mut v as *mut Vec<i32>
}
}

The dataflow graph would show the following value flow:

• Vec::new() returns value into local v (Call edge).
• v.push(1) mutates v in place — &mut v is passed to push, creating a Mut edge from v to the borrow temporary, then to push's return.
• &mut v as *mut Vec<i32> creates a raw pointer — a Mut edge from v to the borrow temporary, a Cast to the raw pointer type, and the result flows to the return value _0.

The param_return_deps query would confirm that no function argument flows to the return value (since there are no parameters), indicating the return value is locally created.

Output Format

The DataFlowGraphWrapper display renders each function's graph as a compact adjacency list:

Function: "my_crate::create_vec"
Node _1 -> Node [_2]
Node _2 -> Node [_3, _4]
Node _3 -> Node [_0]

And Arg2RetWrapper shows argument-to-return dependencies:

Argument _1 ---> Return value _0
Argument _2 ---> Return value _0

Relationship to Other Modules

• Alias Analysis: Dataflow graphs provide value-equivalence information that complements alias relationships.
• SafeDrop: Uses dataflow analysis to determine whether a value flows to a deallocation site.
• Verification: The forward visitor uses def-use chains similar to dataflow's ancestor/descendant queries.

Test Example

The alias analysis test at rapx/tests/alias/alias_01/src/lib.rs demonstrates a simple value-flow scenario:

#![allow(unused)]
fn main() {
fn foo(p: *mut u8) -> Vec<u8, Global> {
    unsafe { Vec::from_raw_parts_in(p, 1, 1, Global) }
}
}

The dataflow graph for foo shows:

• p (argument _1) flows into Vec::from_raw_parts_in via a Move edge.
• The return value of from_raw_parts_in (_0) receives a Call edge from its arguments.
• The param_return_deps query confirms that _1 flows to _0.

This small function exercises all key graph features: argument tracking, call site modeling, and param-to-return dependency detection.

Chapter 5.6. Heap Ownership Analysis

Heap ownership analysis determines whether a Rust type owns heap-allocated memory. This information is essential for memory leak detection and other analyses that must distinguish stack-only types from those requiring deallocation. The module lives at rapx/src/analysis/heap_ownership/.

Overview

A type is classified as a heap owner if it directly or transitively contains a heap unit — a struct that combines a raw pointer to T with a PhantomData<T> marker, following Rust's ownership convention. For example, Vec<T> is a heap owner because its internal RawVec<T> contains both NonNull<T> (the pointer) and PhantomData<T> (the marker).

The analysis traverses all ADTs reachable from local crate function bodies, applies four phases top-down, and produces a HeapOwnershipResultMap keyed by DefId.

HeapOwnershipAnalysis Trait

#![allow(unused)]
fn main() {
pub trait HeapOwnershipAnalysis: Analysis {
    fn get_all_items(&self) -> HeapOwnershipResultMap;

    fn is_heapowner<'tcx>(hares: HeapOwnershipResultMap, ty: Ty<'tcx>) -> Result<bool, &'static str> { ... }
    fn maybe_heapowner<'tcx>(hares: HeapOwnershipResultMap, ty: Ty<'tcx>) -> Result<bool, &'static str> { ... }
}
}

• get_all_items: Returns the full analysis result.
• is_heapowner: Checks whether a concrete (monomorphized) type owns heap memory — returns true if any variant has HeapOwnership::True.
• maybe_heapowner: Checks whether a non-heap-owning type could become a heap owner after monomorphization — returns true if any variant has HeapOwnership::False with at least one type parameter flagged as owning.

Result Format

#![allow(unused)]
fn main() {
pub type HeapOwnershipResultMap = HashMap<DefId, Vec<(HeapOwnership, Vec<bool>)>>;

pub enum HeapOwnership {
    False = 0,   // never owns heap memory
    True = 1,    // owns heap memory
    Unknown = 2, // not yet analyzed
}
}

Each DefId maps to a Vec of variants (one for structs, one per variant for enums). Each variant is (HeapOwnership, Vec<bool>):

• HeapOwnership: whether this variant directly owns heap memory.
• Vec<bool>: per-type-parameter flags — true means the corresponding generic parameter may contribute to heap ownership when monomorphized (used for maybe_heapowner queries).

For example, Vec<T, A> returns (True, [false, true]): the Vec itself is a heap owner; T does not affect ownership; A (allocator) may.

Quick Usage

cargo rapx analyze heapowner

In code:

#![allow(unused)]
fn main() {
let mut analyzer = HeapOwnershipAnalyzer::new(tcx);
analyzer.run();
let result = analyzer.get_all_items();
rap_info!("{}", HeapOwnershipResultMapWrapper(result));
}

The Four-Phase Pipeline

HeapOwnershipAnalyzer::start() in default.rs proceeds through four phases. First, it visits all MIR bodies reachable from the local crate, collects all ADT types, and records their DefIds. Then:

Phase 1: Raw Generic Extraction (extract_raw_generic)

For each ADT, determines which type parameters appear as raw generics — directly embedded in a field without being wrapped in *mut, &, or a heap-owning container. Raw generics may contribute to heap ownership after monomorphization; non-raw generics (behind pointers) do not.

The IsolatedParam type visitor walks each field type and sets record[i] = true when type parameter i appears directly (nested inside tuples, arrays, or other ADT wrappers are recursively explored). The result is a Vec<bool> per variant.

Given struct Example<A, B, T, S> {
    a: A,                  // A appears raw → record[0] = true
    b: (i32, (f64, B)),    // B appears raw → record[1] = true
    c: [[(S) ; 1] ; 2],    // S appears raw → record[3] = true
    d: Vec<T>,             // T is inside Vec, not raw → record[2] = false
}
Result: (False, [true, true, false, true])

Phase 2: Generic Propagation (extract_raw_generic_prop)

Propagates raw-generic flags upward through nested ADTs. When a field is itself a generic ADT (e.g., X<A> inside Example<A, ...>), the raw-generic flags of the inner ADT are transferred to the outer ADT's type parameters. This handles cases like:

struct X<A> { a: A }
// X<A>: (False, [true]) — A is raw

struct Y<B> { a: (i32, (f64, B)), b: X<i32> }
// Y<B>: (False, [true]) — B is raw; X<i32> contributes nothing (i32 is not a param)

struct Example<A, B, T, S> { a: X<A>, b: (i32, (f64, B)), c: [[(S);1];2], d: Vec<T> }
// After propagation: (False, [true, true, false, true])
// X<A> propagates: A is raw → outer's A flag = true

The IsolatedParamPropagation visitor handles this: when it encounters Adt(field_adt, substs), it looks up the field ADT's raw-generic flags and propagates them through the substitution mapping (which inner param maps to which outer param) into the outer record.

Phase 3: Phantom Unit Detection (extract_phantom_unit)

Identifies heap units — structs that are the fundamental building blocks of heap ownership. A struct is a heap unit if and only if:

1. It contains PhantomData<T> where T is a raw generic type parameter (not buried behind *mut, &, etc.). This establishes ownership intent — PhantomData indicates the struct logically owns T.
2. It also contains a pointer field (raw pointer or reference to any type). Without a pointer, PhantomData alone is not sufficient — there must be actual memory that the PhantomData "owns" on behalf of T.

The FindPtr visitor recursively scans all fields looking for TyKind::RawPtr or TyKind::Ref. If both conditions are satisfied, the variant is promoted to HeapOwnership::True.

struct Foo<T> {            // Vec's internal RawVec equivalent
    ptr: NonNull<T>,       // pointer field ✓
    _marker: PhantomData<T>, // PhantomData with raw T ✓
}
// → (True, [false]) — heap unit, T does not affect ownership

struct Proxy3<'a, T> {
    _p: *mut T,
    _marker: PhantomData<&'a T>,  // PhantomData holds &T, not raw T
}
// → (False, [false, false]) — NOT a heap unit

Phase 4: Heap Propagation (extract_heap_prop)

Propagates HeapOwnership::True flags upward through the type tree. Starting from leaf heap units discovered in Phase 3, the HeapPropagation visitor marks an ADT as a heap owner if any of its fields is a known heap owner.

struct Proxy2<T> { _p: *mut T, _marker: PhantomData<T> }
// Phase 3: (True, [false]) — heap unit

struct Proxy5<T> { _x: Proxy2<T> }
// Phase 4: Proxy2 is True → Proxy5 becomes (True, [false]) — heap owner via Proxy2

struct Proxy4<T> { _x: T }
// Phase 4: no heap unit in fields → stays (False, [true]) — only a heap owner when T is one

The visitor short-circuits: once any field returns True, the entire ADT is marked True and traversal stops. Enum variants are handled independently — only structs participate in propagation (enum ownership depends on the active variant at runtime, handled separately in rCanary).

Ownership Layout Encoding

Beyond the boolean heap-owner classification, the Encoder struct in default.rs produces an OwnershipLayoutResult for each field of a type. This is used by the memory leak detector (rCanary) to determine, at runtime, which fields of a drop-in-progress struct need deallocation.

Encoder::encode() matches on the type kind:

The result is a Vec<HeapOwnership> per field plus flags for whether the type requires runtime deallocation checking.

Examples

Basic Proxy Types

The test at rapx/tests/analyze/heapowner_proxy/src/main.rs defines five proxy structs:

#![allow(unused)]
fn main() {
struct Proxy1<T> { _p: *mut T }
// No PhantomData → (False, [false])
// Has a pointer but no ownership intent

struct Proxy2<T> { _p: *mut T, _marker: PhantomData<T> }
// PhantomData + pointer → (True, [false])
// Heap unit: owns memory of type T

struct Proxy3<'a, T> { _p: *mut T, _marker: PhantomData<&'a T> }
// PhantomData holds reference, not raw T → (False, [false, false])

struct Proxy4<T> { _x: T }
// No heap unit, but T is raw generic → (False, [true])
// Becomes heap owner when T is one (e.g., Proxy4<Vec<i32>>)

struct Proxy5<T> { _x: Proxy2<T> }
// Proxy2 is heap unit → (True, [false])
// Inherits heap ownership from Proxy2
}

Standard Library Types

cargo rapx analyze heapowner

Type: std::string::String: (1, [])
Type: std::vec::Vec<T/#0, A/#1>: (1, [0,1])
Type: std::ptr::Unique<T/#0>: (1, [0])
Type: std::alloc::Global: (0, [])
Type: std::ptr::NonNull<T/#0>: (0, [0])
Type: std::marker::PhantomData<T/#0>: (0, [0])

• String owns heap memory (via its internal Vec<u8>).
• Vec<T, A> owns heap memory; T does not affect ownership; A may (different allocators could own heap).
• Unique<T> (the internal pointer wrapper) is a heap unit per PhantomData convention, but does not propagate ownership to T.
• NonNull<T> is just a pointer — no PhantomData → not a heap unit.
• PhantomData<T> itself is not a heap owner.

Relationship to Other Modules

• Memory Leak Detection: rCanary uses HeapOwnershipAnalyzer to identify which types need deallocation tracking, and uses Encoder::encode() to determine field-level ownership layouts for runtime drop analysis.
• SafeDrop: Uses heap ownership information to reason about whether a pointer aliases memory subject to deallocation.

Chapter 5.7. Range Analysis in Rust

Range analysis is a type of static analysis used to track the range (interval) of possible values that a variable can take during the execution of a program. By maintaining an upper and lower bound for each variable, the analysis helps optimize code by narrowing the values that a program may handle. In Rust, range analysis is particularly important in verifying safety properties, such as ensuring that an array access is always within bounds or that certain calculations do not result in overflows.

Range Analysis Trait

#![allow(unused)]
fn main() {
pub trait RangeAnalysis<'tcx, T: IntervalArithmetic + ConstConvert + Debug>: Analysis {
    fn get_fn_range(&self, def_id: DefId) -> Option<RAResult<'tcx, T>>;
    fn get_fn_ranges_percall(
        &self,
        def_id: DefId,
    ) -> Option<Vec<RAResult<'tcx, T>>>;
    fn get_all_fn_ranges(&self) -> RAResultMap<'tcx, T>;
    fn get_all_fn_ranges_percall(&self) -> RAVecResultMap<'tcx, T>;
    fn get_fn_local_range(
        &self,
        def_id: DefId,
        local: Place<'tcx>,
    ) -> Option<Range<T>>;
    fn get_fn_path_constraints(
        &self,
        def_id: DefId,
    ) -> Option<PathConstraint<'tcx>>;
    fn get_all_path_constraints(&self) -> PathConstraintMap<'tcx>;
}
}

Quick Usage Guide

To test the feature via terminal command:

cargo rapx analyze range

or show the entire analysis process via terminal command:

RAPX_LOG=trace cargo rapx analyze range

To use the feature in Rust code:

#![allow(unused)]
fn main() {
let mut range_analysis = RangeAnalyzer::<i128>::new(tcx, false);
range_analysis.run();
let path_constraint = range_analysis.get_all_path_constraints();
rap_info!("{}", PathConstraintMapWrapper(path_constraint));
let result = range_analysis.get_all_fn_ranges();
}

Supported Integer Types For Ranges:

• i32, i64, i128
• u32, u64, u128
• usize

Default Implementation

RAPx provides a default implementation of RangeAnalysis trait in range/mod.rs. The implementation is inspired by the following CGO paper.

• Raphael Ernani Rodrigues, Victor Hugo Sperle Campos, and Fernando Magno Quintao Pereira. "A fast and low-overhead technique to secure programs against integer overflows." In Proceedings of the 2013 IEEE/ACM international symposium on code generation and optimization (CGO), pp. 1-11. IEEE, 2013.

#![allow(unused)]
fn main() {
pub struct RangeAnalyzer<'tcx, T: IntervalArithmetic + ConstConvert + Debug> {
    pub tcx: TyCtxt<'tcx>,
    pub debug: bool,
    pub ssa_def_id: Option<DefId>,
    pub essa_def_id: Option<DefId>,
    pub final_vars: RAResultMap<'tcx, T>,
    pub ssa_places_mapping: FxHashMap<DefId, HashMap<Place<'tcx>, HashSet<Place<'tcx>>>>,
    pub fn_constraintgraph_mapping: FxHashMap<DefId, ConstraintGraph<'tcx, T>>,
    pub callgraph: CallGraph<'tcx>,
    pub body_map: FxHashMap<DefId, Body<'tcx>>,
    pub cg_map: FxHashMap<DefId, Rc<RefCell<ConstraintGraph<'tcx, T>>>>,
    pub vars_map: FxHashMap<DefId, Vec<RefCell<VarNodes<'tcx, T>>>>,
    pub final_vars_vec: RAVecResultMap<'tcx, T>,
    pub path_constraints: PathConstraintMap<'tcx>,
}
}

Why SSA Form?

Before performing range analysis, the MIR (Mid-level Intermediate Representation) is first transformed into Static Single Assignment (SSA) form. SSA guarantees that each variable is assigned exactly once, and every use of a variable refers to a unique definition. This transformation simplifies the analysis in several ways:

• It makes data flow explicit, allowing the analysis to accurately track how values propagate through the program.

• It allows precise modeling of control flow joins using phi-like constructs.

• It improves precision by allowing the interval of each version of a variable to be analyzed separately after each assignment.

Don’t worry about losing track of variables after SSA transformation: The RangeAnalyzer maintains a mapping ssa_places_mapping, which is a HashMap from the original MIR Place to their corresponding SSA Places. This ensures that even after SSA conversion, you can still query the intervals for the variables you care about using their original MIR identity. The SSA transformation is essential for sound and precise interval analysis and is a foundational preprocessing step in this system.

Range Analysis Features

Flow Sensitivity

Interval analysis in Rust can be flow-sensitive, meaning that it accounts for the different execution paths a program might take. This allows the analysis to track how intervals change as variables are assigned or modified during the execution flow, improving the precision of analysis.

Lattice-based Approach

In this approach, values of variables are represented in a lattice, where each element represents an interval. A lattice ensures that each combination of intervals has a defined result, and merging different paths of a program is done by taking the least upper bound (LUB) of intervals from each path.

For example, if a variable x can have an interval [0, 10] on one path and [5, 15] on another path, the merged interval would be [0, 15] because that represents the union of both possible value ranges.

Meet-over-all-paths (MOP) Approach

In the meet-over-all-paths (MOP) approach, the analysis is performed by considering every possible path through a program and merging the results into a final interval. This approach is path-sensitive but may be less scalable on large programs because it needs to account for all paths explicitly.

Precise Interprocedural Analysis

Although each callee function is analyzed once globally for performance,Every call site (i.e., function invocation) triggers a separate numeric evaluation using the actual arguments passed in.

This hybrid approach preserves analysis precision without sacrificing performance.

Range Analysis Test Examples

RAP provides several small test programs under rapx/tests/analyze/range_1 to demonstrate different aspects of the range analysis. This section shows the source code of three representative tests (range_1, range_2, and range_symbolic) and explains what each of them is checking.

Example 1: range_1 — Intra-procedural loop ranges

Source: rapx/tests/analyze/range_1/src/main.rs

fn main() {
    let mut k = 0;
    while k < 100 {
        let mut i = 0;
        let mut j = k;
        while i < j {
            i += 1;
            j -= 1;
        }
        k += 1;
    }
}

This example is an intra-procedural test that exercises nested loops and variable updates inside them.

• k starts from 0 and is increased until it reaches 100, so the analysis should infer:
  • k (and the corresponding SSA locals) have ranges within [0, 100] at the appropriate program points.
• Inside the inner loop, i and j move towards each other:
  • i is incremented, j is decremented.
  • The condition while i < j ensures that the loop stops when the two meet or cross.
• The range analysis needs to:
  • Track how k grows across the outer loop.
  • Track how i and j evolve in the inner loop.
  • Derive precise intervals for these locals at the end of each loop.

The corresponding unit test (test_range_analysis in rapx/tests/tests.rs) checks that the printed ranges for several locals (e.g., _1, _4, _6, _11, _12, _34) match the expected intervals such as [0, 100], [0, 99], [1, 100], etc.

Example 2: range_2 — Inter-procedural range propagation

Source: rapx/tests/analyze/range_2/src/main.rs

fn main() {
    let para1 = 42;
    foo1(para1);

    let para2 = 52;
    let _x = foo2(55, para2);

}

// This function tests passing ranges of parameters between functions.
fn foo1(mut k: usize) {
    while k < 100 {
        k += 1;
    }
}

// This function tests whether the range of returned value is processed as expected.
fn foo2(mut k: usize, _c: usize) -> usize {
    while k < 100 {
        k += 1;
    }
    k
}

This example focuses on inter-procedural range analysis:

• In main, para1 is initialized to 42 and passed to foo1 as the argument k.
  • Inside foo1, k is incremented in a loop while k < 100, so at the end of the function the range of k should be [100, 100].
• For foo2, k is initialized with the literal 55 and incremented until it reaches 100, then returned.
  • The analysis should infer that the return value of foo2 is always 100, i.e. range [100, 100].

The test (test_interprocedual_range_analysis) checks that:

• The parameter and local values in foo1 and foo2 have precise ranges like [42, 42], [52, 52], and [100, 100].
• These ranges are correctly propagated across function calls (from caller to callee and back via return values).

This demonstrates that the range analysis is not limited to a single function, but can reason about how ranges flow across call edges.

Example 3: range_symbolic — Symbolic bound expressions

Source: rapx/tests/analyze/range_symbolic/src/main.rs

fn foo1(x: i32) -> i32 {
    let a = x + 1;
    let y = x;
    let mut result ;
    let _b = a - y; // _11/_8. [1,1] can be inferred before range analysis
    if a >= y {    // always true
        result =  a;
    } else {
        result =  y;
    }
    return result;  // result is always a, but its upper/lower bound 
                    // symbexpr is hard to be inferred without range analysis
}

fn main(){
    let y = 2;
    let x = y;
    foo1(2);
}

This test is designed to show symbolic range expressions:

• Inside foo1, we have:
  • a = x + 1
  • y = x
  • _b = a - y
• Even before full range analysis, _b can be known to be 1:
  • _b = (x + 1) - x = 1, so its range is [1, 1].
• The conditional if a >= y is always true because a = x + 1 and y = x.
  • Therefore, result will always be a.
• However, to express the bounds of result precisely, the analysis needs to:
  • Track that a is x + 1 symbolically.
  • Use symbolic expressions (such as Binary(AddWithOverflow, Place(_1), Constant(1))) to represent lower and upper bounds of intervals.

The unit test (test_symbolic_interval) asserts the existence of specific symbolic interval strings in the analysis output, for example:

• A symbolic lower and upper bound based on x + 1.
• A symbolic interval that refers to another place (e.g. Place(_1)).
• A symbolic interval for a constant (e.g. [1, 1] as a constant expression).

This demonstrates that the range analysis in RAP does not only compute numeric intervals, but also keeps track of symbolic expressions for lower and upper bounds. This is important when the exact numeric values cannot be known statically, but their relationship to program variables can still be expressed and exploited for further analyses.

Chapter 5.8. Safety-Flow Analysis

Safety-Flow Analysis tracks how unsafety propagates through a Rust crate. It builds a graph that connects safe callers to the unsafe operations they transitively depend on, revealing the full unsafety boundary of the crate. This module lives at rapx/src/analysis/safety_flow/.

Overview

Rust's safety model is compartmentalized: unsafe blocks and unsafe fn declarations isolate the surface area where UB can originate. However, safe functions that internally call unsafe functions still carry a verification burden — the safety of the safe caller depends on whether it correctly upholds the unsafe callee's preconditions.

Safety-Flow Analysis answers two questions:

1. Which functions in my crate touch unsafe code? — including safe wrappers, methods on types with invariants, and functions that dereference raw pointers or access static mut.
2. What is the unsafety dependency graph? — for each module, how do constructors, mutators, callers, and unsafe callees relate to each other?

Quick Usage

cargo rapx analyze safetyflow

To also render the unsafety propagation graph as PNG images (requires Graphviz):

cargo rapx analyze safetyflow --draw

For the Rust standard library:

cargo rapx analyze safetyflowstd

Unsafety Sources

The analysis classifies three kinds of unsafe operations in a function body (root.rs:UnsafeOpKind):

A function is considered an unsafe root if it contains at least one of the above. Detection uses a two-stage filter:

1. HIR pre-check (root.rs:hir_contains_unsafe): A fast check for unsafe fn or unsafe { } blocks. Functions that pass neither are skipped entirely.
2. MIR scan (root.rs:scan_mir): For functions passing the HIR check, the MIR body is scanned for specific unsafe operations. Functions with zero unsafe callees, no raw pointer dereferences, and no static mut accesses are excluded.

Pipeline

FnCollector::collect(tcx)
  └─ Collects all function BodyIds from the crate
       │
       ├─ hir_contains_unsafe()   ← HIR pre-filter
       ├─ scan_mir()              ← MIR-level unsafe operation detection
       │
       └─ SafetyFlowUnit          ← Per-function unsafety summary
              │
              ├─ caller → callees (unsafe fn edges)
              ├─ constructors → caller
              ├─ mutable methods → caller
              └─ raw_ptr / static_mut → caller

Function Collection

FnCollector (fn_collector.rs) uses tcx.hir_visit_all_item_likes_in_crate to collect all function bodies, grouped by module.

Root Detection

scan_mir (root.rs:82) performs a MIR-level scan for each function:

• get_unsafe_callees traverses all TerminatorKind::Call terminators, checking whether each callee's FnDef has Safety::Unsafe.
• get_rawptr_deref finds locals whose type is *const T or *mut T and that appear in assignment statements — indicating a raw pointer dereference.
• collect_global_local_pairs maps static mut DefIds to the MIR locals that reference them.

If all three sets are empty, the function is excluded from the safety flow graph.

SafetyFlowUnit

Each unsafe root produces a SafetyFlowUnit (safetyflow_unit.rs):

#![allow(unused)]
fn main() {
pub struct SafetyFlowUnit {
    pub caller: FnInfo,              // The function under analysis
    pub callees: HashSet<FnInfo>,    // Unsafe callees it calls
    pub raw_ptrs: HashSet<Local>,    // Raw pointer dereference locals
    pub static_muts: HashSet<DefId>, // static mut accesses
    pub caller_cons: HashSet<FnInfo>,// Constructors of the caller's struct
    pub mut_methods: HashSet<DefId>, // Mutable methods on the caller's struct
}
}

Constructors are resolved via get_cons by checking which functions in the same impl block return Self. Mutable methods are resolved via get_muts by checking &mut self parameters.

A BasicUnitCounts structure in the same file classifies each unit into 13 categories (e.g., "safe function calling unsafe method", "unsafe method with unsafe constructor calling unsafe function") for statistical reporting.

Module-Level Graphs

SafetyFlowGraph (safetyflow_graph.rs) aggregates units per module and generates DOT-format graphs with three edge types:

Nodes are colored: red for unsafe functions, black for safe functions. Constructors are drawn as septagons, methods as ellipses, and free functions as boxes. Each struct's methods and constructors are grouped in a dashed subgraph cluster.

Standard Library Audit

When run in TargetCrate::Std mode (mod.rs:48), the analysis follows a different pipeline (std_analysis.rs) optimized for the standard library's structure. It produces unsafe call chains rather than per-module graphs (see chain.rs for the DFS-based chain extraction).

Output Format

The console output groups functions by module and shows:

SafetyFlow: my_module (3 function(s))
  my_module::safe_wrapper [Safe]
    -> core::ptr::read
    -> core::ptr::write
    *raw* ptr deref: _3, _7
    + constructor: my_module::MyStruct::new
    ~ mut_self: my_module::MyStruct::set_field

A final summary reports total counts:

SafetyFlow summary: 42 function(s), 87 call edge(s), 15 raw ptr deref(s), 2 static mut access(es)

Relationship to Verification

Safety-Flow Analysis is the upstream stage of the verification pipeline. The VerifyTargetCollector reuses hir_contains_unsafe and scan_mir from root.rs to identify verification targets. While Safety-Flow produces a module-level overview of unsafety propagation, the verification module drills into each function with path-sensitive SMT-based property checking.

Test Examples

The test suite at rapx/tests/analyze/safetyflow_raw_ptr contains tests for each unsafety source:

Safe Caller Calling Unsafe Callee (safe_caller)

// rapx/tests/analyze/safetyflow_safe_caller/src/main.rs
fn main() {
    let mut s = String::from("a tmp string");
    let ptr = s.as_mut_ptr();
    let _v = unsafe { Vec::from_raw_parts(ptr, s.len(), s.len()) };
}

main is a safe function that calls Vec::from_raw_parts inside an unsafe block. The safety flow graph captures this as a CallerToCallee edge from a safe caller to an unsafe callee. This is the most common pattern in Rust codebases — safe wrappers around unsafe primitives.

Raw Pointer Dereference (raw_ptr)

// rapx/tests/analyze/safetyflow_raw_ptr/src/main.rs
fn main() {
    let mut value = 0i32;
    let ptr: *mut i32 = &mut value as *mut i32;
    unsafe {
        *ptr = 1;
    }
}

main contains a raw pointer dereference (*ptr = 1). The analysis records _ptr as a RawPtr local and connects it to a synthetic "raw ptr deref" node in the output graph. This pattern is typical in FFI code and low-level memory manipulation.

Struct Methods with Unsafe Operations (struct)

#![allow(unused)]
fn main() {
// rapx/tests/analyze/safetyflow_raw_ptr/src/main.rs (struct test)
struct St1 { pub ptr: *mut u8, len: usize }
struct St2 { pub ptr: *mut u8, pub len: usize }

impl St1 {
    pub fn from(p: *mut u8, l: usize) -> St1 {
        St1 { ptr: p, len: l }
    }
    pub unsafe fn get(&self) -> &[u8] {
        slice::from_raw_parts(self.ptr, self.len)
    }
    pub unsafe fn set_len(&mut self, len: usize) {
        self.len = 1;
    }
}
// St2 has identical impls...
}

Two structs (St1, St2) with unsafe methods. St1 has private fields, St2 has public fields. The safety flow graph distinguishes: for St2 (public fields), mutable field access is treated as an implicit mutator; for St1 (private fields), only explicit &mut self methods contribute. The output shows constructor → method edges and mutator → caller edges for each struct in its own subgraph cluster.

Expected Output

For the struct test, running cargo rapx analyze safetyflow produces output like:

SafetyFlow: struct (4 function(s))
  St1::from [Safe]
    + constructor: St1::from
  St1::get [Unsafe]
    -> core::slice::raw::from_raw_parts
    + constructor: St1::from
  St1::set_len [Unsafe]
    + constructor: St1::from
  St2::get [Unsafe]
    -> core::slice::raw::from_raw_parts
    + constructor: St2::from
    ~ mut_self: St2::len (public field)

This reveals the full unsafety surface: both St1 and St2 have unsafe methods calling slice::from_raw_parts, and St2 additionally has public-field mutation paths that could affect the safety of get.

Chapter 6. Check

This chapter introduces the bug detection modules of RAPx, covering security-focused use cases. RAPx supports detection of dangling pointers and memory leaks. Performance optimization is covered as a standalone module in Chapter 7, and unsafe code verification in Chapter 8.

Module Overview

The check module at rapx/src/check/ contains two main sub-modules:

All check modules are invoked through the cargo rapx check sub-command with appropriate flags. Multiple flags can be combined to run several detectors simultaneously.

Architecture

Each check module follows a common architecture:

1. Alias Preparation: The MOP-based alias analysis is run first to compute function-level alias summaries.
2. Path-Sensitive Traversal: Using PathGraph, each function's execution paths are enumerated and analyzed independently.
3. Bug Pattern Matching: Each module applies domain-specific rules along each path to identify bug patterns (dangling pointer usage, leaked allocations).
4. Warning Emission: Detected bugs are reported with file locations, function names, and diagnostic messages.

Default Options for Rust Project Compilation

To analyze system software without std (e.g., Asterinas), try:

cargo rapx check -f -- --target x86_64-unknown-none

To analyze the Rust standard library:

cargo rapx check -f -- -Z build-std --target x86_64-unknown-linux-gnu

To run all check modules at once:

cargo rapx check -f -m

Chapter 6.1. Dangling Pointer Detection

Rust uses ownership-based resource management (OBRM) and automatically deallocates unused resources without a garbage collector. This approach can potentially lead to premature memory deallocation, resulting in use-after-free or double-free errors. A significant portion of these bugs is related to the unwinding path, making them difficult to detect through testing or dynamic analysis. For more details, please refer to the SafeDrop paper published in TOSEM.

The implementation lives at rapx/src/check/safedrop/.

PoC

Below is a toy example demonstrating a Rust program with a use-after-free bug. The Data object is automatically dropped once the program exits the inner block scope of main. Accessing ptr after this point triggers a use-after-free error.

struct Data {
    value: Box<i32>,
}

impl Data {
    fn new(value: i32) -> Data {
        Data { value: Box::new(value) }
    }

    fn print_value(&self) {
        println!("Value: {}", self.value);
    }
}

fn main() {
    let ptr: *const Data;

    {
        let data = Data::new(42);
        ptr = &data as *const Data;
    } // data is automatically dropped here, leaving ptr dangling.

    unsafe {
        (*ptr).print_value(); // use-after-free.
    }
}

Usage

To detect such bugs, navigate to the project directory and execute:

cargo rapx check -f

RAPx outputs a warning message in yellow if bugs are detected:

21:49|RAP-FRONT|WARN|: Use after free detected in function "main"
21:49|RAP-FRONT|WARN|: Location: src/main.rs:27:9: 27:20 (#0)
21:49|RAP-FRONT|WARN|: Location: src/main.rs:27:9: 27:34 (#0)

Mechanism

SafeDrop performs two essential steps for dangling pointer detection:

1. Alias Preparation

The MOP-based alias analysis is run first to compute alias summaries for all functions. SafeDropGraph wraps the alias analysis's AliasGraph and reuses its Value, AliasBlockFacts, and MopFnAliasPairs types, along with the path-sensitive alias_bb and alias_bbcall traversal methods. The precomputed alias summaries identify which function parameters and return values may alias, enabling inter-procedural drop tracking without re-analyzing callees.

Key data structures from the alias analysis reused by SafeDrop:

• AliasGraph: Wraps PathGraph for CFG topology and path enumeration, plus alias-specific state (values, alias_sets, block_facts).
• Value: Represents program places (locals and field projections) with drop metadata (may_drop, need_drop).
• AliasBlockFacts: Per-block assignment records and constant values.
• MopAliasPair / MopFnAliasPairs: Alias results annotated with drop information.

2. Path-Sensitive Bug Detection

SafeDrop traverses each enumerated execution path of a target function, performing drop analysis at each program point:

1. Drop Event Tracking: At each basic block, the analysis identifies which values are dropped at that point. Drop points are determined from MIR's explicit TerminatorKind::Drop terminators and known drop function calls (e.g., drop_in_place). StorageDead statements and implicit drop scopes are not currently tracked.

2. Alias Propagation: Using the alias sets built during path traversal, the analysis propagates drop information through alias relationships. If a aliases b and a is dropped, then b is considered dangling.

3. Dangling Use Detection: At each program point where a value is used (read, written, or passed to a function), the analysis checks whether any alias of that value has already been dropped along the current path.

4. Inter-procedural Drop Propagation: When a function call drops one of its arguments (e.g., drop_in_place, or a consuming call), SafeDrop consults the callee's alias summary and the caller's argument-to-alias mapping to determine which caller-side values become dangling after the call.

5. Return Value Checking: Return values that alias with dropped locals are also flagged, catching cases where a function returns a dangling pointer to a deallocated local.

The path sensitivity is critical: by analyzing each CFG path independently, SafeDrop avoids the over-approximation that would occur if all paths were merged at join points. For example, if a value is dropped on one branch but not another, path-sensitive analysis correctly reports the bug only on the path where the drop occurs, while a path-insensitive analysis might produce false positives on the other branch or false negatives by ignoring the drop.

Source Structure

The safedrop/ module is organized as follows:

Reference

The feature is based on our SafeDrop paper, published in TOSEM:

@article{cui2023safedrop,
  title={SafeDrop: Detecting memory deallocation bugs of rust programs via static data-flow analysis},
  author={Mohan Cui, Chengjun Chen, Hui Xu, and Yangfan Zhou},
  journal={ACM Transactions on Software Engineering and Methodology},
  volume={32}, number={4}, pages={1--21}, year={2023},
  publisher={ACM New York, NY, USA}
}

Chapter 6.2. Memory Leakage Detection

Rust employs a novel ownership-based resource management model to facilitate automated deallocation during compile time. However, developers may intentionally bypass this mechanism into manual drop mode (e.g., via ManuallyDrop, Box::into_raw, or raw pointer manipulation), which is prone to memory leaks.

rCanary is a static model checker that detects memory leaks across the semi-automated memory management boundary. It uses SMT-based constraint solving to reason about heap ownership transfer and detect leaked allocations. The implementation lives at rapx/src/check/rcanary/.

Bug Types

rCanary detects two categories of memory leaks:

1. Orphan Object

An orphan object is a heap-allocated item that has been detached from Rust's ownership system (e.g., converted to a raw pointer via Box::into_raw) but never properly freed.

fn main() {
    let mut buf = Box::new("buffer");
    // heap item 'buf' becomes an orphan object
    let ptr = Box::into_raw(buf);
    // leak by missing free operation on 'ptr'
    // unsafe { drop_in_place(ptr); }
}

2. Proxy Type

A proxy type is a compound type (struct) containing at least one field that stores an orphan object (raw pointer to heap data). If the type's Drop implementation fails to manually free that field, the heap allocation leaks.

struct Proxy<T> {
    ptr: *mut T,
}

impl<T> Drop for Proxy<T> {
    fn drop(&mut self) {
        // user should manually free the field 'ptr'
        // unsafe { drop_in_place(self.ptr); }
    }
}

fn main() {
    let mut buf = Box::new("buffer");
    // heap item 'buf' becomes an orphan object
    let ptr = &mut *ManuallyDrop::new(buf) as *mut _;
    let proxy = Proxy { ptr };
    // leak by missing free 'proxy.ptr' in drop
}

Architecture

rCanary's overall architecture consists of three main stages:

Stage 1: Type Analysis (ADT-DEF Analysis)

The type analysis examines type definitions (ADTs) to classify each field as Owned or Unowned with respect to heap management. A field is Owned if the type's Drop implementation is expected to free the heap allocation pointed to by that field. The analysis extracts per-type drop obligations: for each variant of each ADT, which fields must be manually freed.

Key output: A mapping from each ADT type to its field ownership classification tuples, e.g.:

std::boxed::Box<T/#0, A/#1> [(Owned, [false, true])]
std::mem::ManuallyDrop<T/#0> [(Unowned, [true])]

Stage 2: Flow Analysis (Constraint Construction)

The flow analysis (FlowAnalysis in ranalyzer.rs) performs path-sensitive traversal of the MIR, constructing boolean constraints in SMT-LIB2 format:

1. Intra-procedural Visitor (ranalyzer/intra_visitor.rs): Walks each function's MIR, tracking ownership transitions at each statement and terminator. For each program point, it maintains:

   • Taint sets: Which locals currently hold orphan objects.
   • Drop obligations: Which locals must be freed before the function returns.
   • Ownership state: Whether each local is Declared, Init (with constraint variables), or uninitialized.

2. Constraint Encoding: Each ownership transition (e.g., Box::into_raw, ManuallyDrop::new, assignments, drops) generates SMT formulas. Boolean variables encode:

   • Constructor initialization status.
   • Drop-all obligations at return points.
   • Field-level drop propagation through struct assignments.

3. Inter-procedural Summaries (ranalyzer/inter_visitor.rs): Function summaries capture the relationship between a function's arguments and return value with respect to drop obligations. When a callee is encountered, its summary is applied to the caller's constraint state.

Stage 3: Constraint Solving (SMT)

The generated SMT formulas are fed to the Z3 solver. The solver checks whether there exists a satisfying assignment where:

• A heap allocation was created and ownership was transferred to a raw pointer (becoming orphaned).
• The orphan allocation is not freed before the program point where it goes out of scope.

If Z3 finds a satisfying assignment, a memory leak is reported at the corresponding source location. The constraint model also identifies which specific allocation site leaked and which path through the function reaches the leak.

Source Structure

Usage

Prerequisites

Before using rCanary, install the Z3 solver (minimum version 4.10):

# macOS
brew install z3

# Ubuntu/Debian
apt-get install z3

Running rCanary

Navigate to the root directory of a Cargo program and run:

cargo rapx check -m

Note: Analysis requires the nightly-2026-04-03 toolchain with rustc-dev, rust-src, and llvm-tools-preview components installed.

Output

When a leak is detected:

22:10:39|RAP|WARN|: Memory Leak detected in function main
warning: Memory Leak detected.
 --> src/main.rs:3:16
  |
1 | fn main() {
2 |     let buf = Box::new("buffer");
3 |     let _ptr = Box::into_raw(buf);
  |                ------------------ Memory Leak Candidates.
4 | }

Additional Configure Arguments

rCanary provides optional environment variables for diagnostic output:

• ADTRES: Print type analysis results, including type definitions and analysis tuples.
• Z3GOAL: Emit the Z3 formula for the given function in SMT-LIB2 format.
• ICXSLICE: Enable verbose output with intermediate rCanary debug metadata (per-block taint sets, ownership states, constraint variables).

Note: These parameters may change due to version migration.

Example: Z3GOAL Output

(goal
  |CONSTRAINTS: T 0|
  (= |0_0_1_ctor_fn| #b01)
  |CONSTRAINTS: S 1 2|
  (= |1_2_1| #b00)
  (= |1_2_3_ctor_asgn| |0_0_1_ctor_fn|)
  |CONSTRAINTS: T 1|
  (= |1_0_3_drop_all| (bvand |1_2_3_ctor_asgn| #b10))
  ...
  |CONSTRAINTS: T 2|
  (= |2_0_3_return| #b00))

Reference

The feature is based on our rCanary work, published in TSE:

@article{cui2024rcanary,
  title={rCanary: Detecting memory leaks across semi-automated memory management boundary in Rust},
  author={Mohan Cui, Hongliang Tian, Hui Xu, and Yangfan Zhou},
  journal={IEEE Transactions on Software Engineering},
  year={2024},
}

Chapter 7. Optimization

This module identifies performance bottlenecks and inefficiencies using static analysis methods. The implementation lives at rapx/src/check/opt/.

Usage

To detect performance bugs:

cargo rapx opt

RAPx outputs a summary of detected inefficiencies by category, along with detailed source locations and suggested improvements.

Architecture

The opt module operates in three steps:

1. Dataflow Graph Construction: Builds function-level dataflow graphs via DataflowAnalyzer.
2. Pattern Matching: Each checker walks the dataflow graph to find known inefficiency patterns.
3. Reporting: Detected issues are reported via rap_warn! with annotated source snippets, and a summary is logged via rap_info! with per-category counts.

All checkers run together; there is currently no way to select individual checks.

Categories

The module covers six categories of performance checks:

Test Cases

The tests/opt/ directory contains three end-to-end test cases:

bounds_len — Bounds Checking

#![allow(unused)]
fn main() {
fn foo(mut a: Vec<i32>) {
    for i in 0..a.len() {
        a[i] = a[i] + 1;
    }
}

fn foo1(input: &[u8]) {
    let mut index = 0;
    let len = input.len();
    while index < len {
        let b = input[index];
        index += 1;
    }
}
}

RAPx detects that the index i is provably within [0, a.len()) and the while loop's index < len guard ensures index is always in bounds. The bounds checks on a[i] and input[index] are redundant.

Expected output: Bounds Checking: 2.

encoding_check — Encoding Checking

#![allow(unused)]
fn main() {
use std::str;

fn foo_1(mut n: u128, base: usize, output: &mut String) {
    const BASE_64: &[u8; 64] = b"0123456789abcdef...ABCDEFGHIJKLMNOPQRSTUVWXYZ@$";
    let mut s = [0u8; 128];
    let mut index = s.len();
    let base = base as u128;
    loop {
        index -= 1;
        s[index] = BASE_64[(n % base) as usize];
        n /= base;
        if n == 0 {
            break;
        }
    }
    output.push_str(str::from_utf8(&s[index..]).unwrap());
}

static CHARS: &[u8; 5] = b"12345";

fn foo_2() -> String {
    let mut v = Vec::with_capacity(12);
    v.push(CHARS[2 as usize]);
    v.push(CHARS[3 as usize]);
    v.push(b' ');
    String::from_utf8_lossy(&v).to_string()
}
}

RAPx detects two encoding inefficiencies: manual base-64 encoding with String::push_str that could use a more efficient approach, and character-by-character Vec::push before UTF-8 conversion.

Expected output: Encoding Checking: 2.

hash_key_cloning — Memory Cloning

#![allow(unused)]
fn main() {
use std::collections::HashSet;

fn foo(a: &Vec<String>) {
    let mut b = HashSet::new();
    for i in a {
        let c = i.clone();
        b.insert(c);
    }
}
}

RAPx detects that i.clone() produces a value that is only used as a HashSet key. The original borrowed value could be used instead, avoiding an unnecessary allocation.

Expected output: Cloning: 1.

Detailed Module Reference

Bounds Checking (checking/bounds_checking/)

Rust performs automatic bounds checking on indexed accesses for safety. In performance-critical loops, these checks can be eliminated when the index is provably within bounds.

Sub-modules:

• bounds_len.rs: Analyzes index-vs-length relationships to prove bounds checks are redundant.
• bounds_extend.rs: Detects cases where Vec::extend or Vec::extend_from_slice would be more efficient than element-by-element push.
• bounds_loop_push.rs: Detects patterns where for loop iteration combined with push can be replaced with bulk operations.

Encoding Checks (checking/encoding_checking/)

Detects inefficient encoding patterns in string and byte manipulation.

Sub-modules:

• array_encoding.rs: Detects inefficient array-to-slice encoding patterns.
• string_lowercase.rs: Detects manual case conversion patterns that should use to_lowercase() or to_ascii_lowercase().
• string_push.rs: Detects repeated String::push in loops that could use push_str, write!, or extend.
• vec_encoding.rs: Detects inefficient vector encoding patterns like repeated push when bulk operations are available.

Memory Cloning (memory_cloning/)

Detects unnecessary clone operations where a cloned value is only used immutably.

Sub-modules:

• used_as_immutable.rs: Detects cloned values that are only used in immutable contexts (e.g., clones used as keys in hash-based collections where the original borrowed value could be used instead).

Note: Developers need to manually verify whether removing the clone is semantically safe, as clone removal may change ownership semantics.

Data Collection (data_collection/)

Detects suboptimal collection choices and suggests alternatives with better algorithmic complexity.

Initialization (initialization/)

• local_set.rs: Suggests HashSet initialization patterns.
• vec_init.rs: Detects Vec initialization that can be optimized with vec![] or with_capacity.

Reallocation (reallocation/)

• flatten_collect.rs: Suggests flatten().collect() instead of nested iteration.
• unreserved_hash.rs: Detects HashMap/HashSet usage without reserve.
• unreserved_vec.rs: Detects Vec usage without reserve before known-size population.

Suboptimal (suboptimal/)

• participant.rs: Detects repeated collection traversal patterns.
• slice_contains.rs: Detects Vec::contains on large vectors where HashSet would be faster.
• vec_remove.rs: Detects Vec::remove in loops (O(n²) when swap_remove would be O(n)).

Chapter 8. Verification

Unsafe code enables low-level operations while circumventing Rust's safety guarantees, and may introduce undefined behavior (UB) if misused. The verification module (rapx::verify) provides a staged pipeline for checking that unsafe call sites satisfy their callee's safety preconditions. It combines path-sensitive MIR traversal, abstract interpretation, and Z3-based SMT solving to produce verdicts of Proved or Unproved for each safety property at each unsafe call site.

Chapter Outline

• 8.1 Design Principles and Verification Modes — the three assumptions, contract-based verification, and the scan / targeted modes
• 8.2 Verification Target Collection — how targets are gathered and how contracts are resolved (annotation → JSON → call-chain)
• 8.3 Safety Property Contracts — built-in property reference, user-defined contracts (the def DSL), contract annotation (direct + JSON), and inspecting with --debug-contracts
• 8.4 The Verification Pipeline — a complete walkthrough of the verification pipeline using a linked-list case study: loop-repeat planning, path extraction, backward slicing, symbolic VM execution, and SMT check

Chapter 8.1. Design Principles and Verification Modes

8.1.1 Design Principles

The verification is grounded on three assumptions:

• Origin of Unsafe Code: All instances of undefined behavior arise from unsafe code — safe Rust's type system already rules out data races, use-after-free, null-pointer dereferences, and buffer overflows. Verification focuses exclusively on the unsafe boundary where the compiler's guarantees end.
• Explicit Safety Properties: Safety properties of unsafe code are documented through attributes:
  • #[rapx::requires(...)] on unsafe functions — preconditions callers must satisfy before invoking the function.
  • #[rapx::invariant(...)] on structs — structural invariants that must hold for every instance.
  • #[rapx::ensures(...)] on unsafe trait methods — postconditions that every implementor of the trait must guarantee. Only unsafe trait implementations involve #[rapx::ensures]; regular functions use #[rapx::requires] instead. See the Rust Safety Standard for the underlying methodology. Each annotation declares a contract, making safety obligations machine-checkable rather than implicit in documentation comments. The full contract syntax is described in Chapter 8.3.
• Soundness of Unsafe Code Usage: Unsafe code is considered safe if every possible execution path satisfies the safety properties of every unsafe callee it invokes. If a path exists that would violate even one property, the call site is flagged as unproved.

8.1.2 Verification Modes

RAPx supports two verification modes, selectable via cargo rapx verify --mode <MODE>. Each mode targets a different use case in the development workflow.

scan Mode (Default)

Fully automatic. The VerifyTargetCollector (target.rs) walks all function bodies in the crate using a HIR visitor. It selects functions for verification if:

• the function body contains an unsafe { } block, or
• the function is a method on a struct with #[rapx::invariant] annotations.

For each selected function, build_function_target collects all unsafe call sites from the MIR body and resolves each callee's safety contracts from #[rapx::requires] annotations or a bundled JSON database for standard library functions (see Chapter 8.3).

cargo rapx verify --mode scan

targeted Mode

Only verifies functions explicitly annotated with #[rapx::verify]. No pre-filter is applied; the collector simply checks for the attribute presence.

cargo rapx verify --mode targeted

The annotation pattern:

#![allow(unused)]
#![feature(register_tool)]
#![register_tool(rapx)]

fn main() {
#[rapx::verify]
#[rapx::requires(ValidPtr(ptr, u32, 1))]
unsafe fn my_function(ptr: *mut u32, len: usize) {
    unsafe { ptr::write(ptr.add(len - 1), 0); }
}
}

Verifying the standard library. When the crate under analysis relies on the #[cfg_attr(rapx, ...)] pattern (as the annotated rust-std fork does), the rapx cfg and the tool registration must be injected through RUSTFLAGS:

export RUSTFLAGS="--cfg=rapx -Zcrate-attr=feature(register_tool) -Zcrate-attr=register_tool(rapx)"
cargo rapx verify --module slice --mode targeted

Without --cfg=rapx the cfg_attr-gated markers never expand, and the verifier reports that the module matched no functions.

8.1.3 Common Options

--prepare-targets lists all verification targets and their resolved contracts without running verification (see Chapter 8.2 for detailed examples).

The --skip-invariant flag skips struct invariant checks and instead derives safety through constructor-mutator-method chains. For structs that lack #[rapx::invariant] annotations, the verifier enumerates all paths from each constructor through zero or more &mut self mutators to a final reader method. For each chain, it collects the constructor's #[rapx::requires] contracts (if any), filters out properties invalidated by subsequent field mutations, merges in the reader method's own #[rapx::requires], and verifies that the accumulated contracts entail the callee's safety requirements at every unsafe call site. Works with both scan and targeted modes:

cargo rapx verify --skip-invariant

The --crate <CRATE> and --module <PATH> flags restrict verification to a specific crate and module. When combined, only functions in the intersection are verified. This is commonly used for verifying standard library modules:

cargo rapx verify --crate core --module slice

The crate prefix is matched flexibly, so --module slice matches core::slice::*.

The --postfix-repeat flag provides manual control over loop unrolling depth. By default (auto), the verifier chooses the repeat count automatically. When auto-detection produces inaccurate results, --postfix-repeat=N disables auto-expansion and fixes the repeat count to N. The full mechanism is described in Chapter 8.4.1 Path Extraction.

The --debug-contracts flag prints the full contract resolution for every verification target: each unsafe callee with its resolved contracts, and the caller's own contracts in expanded form. Useful for diagnosing missing or unexpected contract resolutions:

cargo rapx verify --debug-contracts

Chapter 8.2. Verification Target Collection

When verification starts, RAPx scans the crate to identify verification targets — functions whose safety contracts need to be checked — and resolves the contracts for each target.

8.2.1 What Gets Verified

In scan mode (the default), a function is selected as a verification target if:

• its body contains an unsafe { } block, or
• it is a method on a struct with #[rapx::invariant] annotations.

For each target, the collector gathers:

• Every call to an unsafe fn in the function body, along with the callee's resolved contracts.
• Every raw pointer dereference (*ptr, *ptr = val) in unsafe blocks — these implicitly require ValidPtr + Align + Typed, as if those contracts were declared on a pseudo-callee.
• Every static mut access — treated similarly.
• Entry assumptions — the facts the verifier can assume when the function is entered:
  • The function's own #[rapx::requires] annotations.
  • If the function is a method on a struct with #[rapx::invariant], those invariants are included as entry facts.
  • Type-level invariants for function parameters (e.g. a &[T] parameter automatically supplies ValidPtr + NonNull + Allocated + InBound + Typed for the slice's data pointer).

8.2.2 How Contracts Are Resolved

For each unsafe callee, the verifier needs to know what safety properties it requires. Contracts are resolved in four tiers, tried in order:

1. Direct annotation: #[rapx::requires(...)] on the callee itself. See Chapter 8.3.2.

2. Trait method inheritance: If the callee is a trait method impl and has no direct annotation, its contracts are inherited from #[rapx::requires] on the trait's method declaration.

3. JSON database: For standard library functions that can't be annotated upstream, contracts are loaded from a bundled database. See Chapter 8.3.2.

4. Call-chain inheritance: If the unsafe callee still has no contracts, the verifier looks inside its MIR body for the unsafe functions it calls (its own unsafe callees). If any of those have resolved contracts, they are used as the verification target — the caller only needs to satisfy the contracts of the deepest callee in the chain. This follows a bounded depth. For example, if A calls B, B calls C, and C has #[rapx::requires], verifying the call to B checks A's state against C's contracts.

If all four tiers produce nothing, the callee's contracts are left as Unknown — the callsite cannot be verified.

8.2.3 Inspecting Targets with --prepare-targets

The --prepare-targets flag prints every verification target collected by the scanner — a function or method whose unsafe operations need to be checked — along with its resolved contracts:

cargo rapx verify --prepare-targets

For the linked_list_nonnull case study, the collector finds 13 targets. Output excerpt (annotations explained below):

23:35:35|RAPx|INFO|: Start analysis with RAPx.
23:35:35|RAPx|INFO|: ============================================================
23:35:35|RAPx|INFO|: [rapx::verify] prepare targets for struct: LinkedList
23:35:35|RAPx|INFO|: ============================================================
23:35:35|RAPx|INFO|:   struct invariants:                              ①
23:35:35|RAPx|INFO|:     - Align(head.unwrap_some(), Node<T>)
23:35:35|RAPx|INFO|:     - Allocated(head.unwrap_some(), Node<T>, 1)
23:35:35|RAPx|INFO|:     - Typed(head.unwrap_some(), Node<T>)
23:35:35|RAPx|INFO|:     - Owning(head.unwrap_some())
23:35:35|RAPx|INFO|:     - Align(tail.unwrap_some(), Node<T>)
23:35:35|RAPx|INFO|:     - Allocated(tail.unwrap_some(), Node<T>, 1)
23:35:35|RAPx|INFO|:     - Typed(tail.unwrap_some(), Node<T>)
23:35:35|RAPx|INFO|:     - Owning(tail.unwrap_some())
23:35:35|RAPx|INFO|:   --- method: new ------------------------------------------------- ②
23:35:35|RAPx|INFO|:       return checkpoints: 1 block(s) [0]             ③
23:35:35|RAPx|INFO|:       unsafe checkpoints: <none>
...
23:35:35|RAPx|INFO|:   --- method: drop ------------------------------------------------
23:35:35|RAPx|INFO|:       return checkpoints: 1 block(s) [7]
23:35:35|RAPx|INFO|:       unsafe callee: std::boxed::Box::<T>::from_raw(*mut T) -> std::boxed::Box<T>
23:35:35|RAPx|INFO|:         safety contracts:                           ④
23:35:35|RAPx|INFO|:           - Align(raw, T)
23:35:35|RAPx|INFO|:           - Allocated(raw, T, 1, global)
23:35:35|RAPx|INFO|:           - Typed(raw, T)
23:35:35|RAPx|INFO|:           - Owning(raw)
23:35:35|RAPx|INFO|:           - Alias(raw, ret)
23:35:35|RAPx|INFO|:         path: shortest path: 0 -> 1 -> 2 -> 3 -> 4  ⑤
23:35:35|RAPx|INFO|:       unsafe callee: std::ptr::NonNull::<T>::as_ref(&std::ptr::NonNull<T>) -> &'a T
23:35:35|RAPx|INFO|:         safety contracts:
23:35:35|RAPx|INFO|:           - Ptr2Ref(self.0, T)
23:35:35|RAPx|INFO|:         path: shortest path: 0 -> 1 -> 2
23:35:35|RAPx|INFO|: ============================================================
23:35:35|RAPx|INFO|: [rapx::verify] total: 0 free function(s), 13 method(s), 1 struct(s), 0 trait(s)  ⑥

Chapter 8.3. Safety Property Contracts

RAPx verifies safety through explicit contracts declared in source code. A contract is a logical statement about pointer validity, numeric bounds, ownership, and other safety properties that RAPx checks against a function's MIR. This chapter covers the two kinds of contract (§8.3.1), how to attach them to code (§8.3.2), and how to inspect the resolved assertions (§8.3.3).

8.3.1 Contracts

A contract is either a built-in property shipped with RAPx, or a user-defined contract composed from the built-ins.

8.3.1.1 Built-in Properties

The semantics of each property kind are defined in primitive-sp.md. The annotated reference with examples:

Alias(p1, p2)

p1 == p2 — the two places refer to the same memory. Always a hazard: unproved Alias is reported as a [hazard] entry and contributes to UNSOUND. Alias itself is not a safety violation, provided it does not also violate Owning or Alive. psp IV.2.

#![allow(unused)]
fn main() {
#[rapx::requires(Alias(ptr, ret))]
}

Align(ptr, Ty)

ptr % alignment(Ty) == 0 — the pointer satisfies the alignment requirement of Ty. psp I.1.

#![allow(unused)]
fn main() {
#[rapx::requires(Align(ptr, u32))]
}

Alive(ptr, 'a)

lifetime(*p) >= l — the allocation is still live and not freed across the lifetime 'a. psp IV.3.

#![allow(unused)]
fn main() {
#[rapx::requires(Alive(ptr, 'a))]
}

Allocated(ptr, Ty, count, [allocator])

Memory belongs to a live allocation. The fourth argument (allocator) defaults to global when omitted. psp II.2.

#![allow(unused)]
fn main() {
#[rapx::requires(Allocated(ptr, u8, layout.size()))]
#[rapx::requires(Allocated(ptr, u8, layout.size(), Global))]
}

Deref(ptr, Ty, count)

Allocated ∧ InBound — the pointer can be safely dereferenced. primitive-sp §2.2.

#![allow(unused)]
fn main() {
#[rapx::requires(Deref(ptr, u32, count))]
}

InBound

The accessed memory lies within the bounds of a single allocated object. Two forms:

The slice form supports all SliceIndex types and expands to the correct bounds check. psp II.3.

Init(ptr, Ty, count)

Memory is initialized for count elements of Ty. Stronger than Typed: Init implies Typed but not vice versa. psp III.4.

#![allow(unused)]
fn main() {
#[rapx::requires(Init(ptr, T, len))]
}

Layout(ptr, layout)

ValidNum(rem(ptr, layout.align), 0) ∧ Allocated(ptr, u8, layout.size, Global) — the pointer matches the layout's size and alignment from a prior allocation. primitive-sp §2.2.

#![allow(unused)]
fn main() {
#[rapx::requires(Layout(ptr, layout))]
}

NonNull(ptr) / Null(ptr)

ptr != 0 — the pointer is not null. psp II.1. Null(ptr) is the inverse — the pointer may be null, used inside any(...) for null-guarded contracts.

#![allow(unused)]
fn main() {
#[rapx::requires(NonNull(ptr))]
#[rapx::requires(any(Null(self), (ValidPtr(self, T, 1), Align(self, T))))]
}

NonOverlap(a, b, T, count)

The memory ranges (a, sizeof(T) * count) and (b, sizeof(T) * count) are pairwise disjoint. psp II.4.

#![allow(unused)]
fn main() {
#[rapx::requires(NonOverlap(src, dst, u32, count))]
}

NonVolatile(p, T, len)

Memory is not volatile — no other thread writes to the region (p, sizeof(T) * len). psp V.2.

#![allow(unused)]
fn main() {
#[rapx::requires(NonVolatile(ptr, T, count))]
}

NoPadding(T)

The type T has no padding bytes — padding(T) == 0. psp I.3.

#![allow(unused)]
fn main() {
#[rapx::requires(NoPadding(T))]
}

Opened(fd)

An OS resource (e.g. file descriptor) is valid and open. psp V.3.

#![allow(unused)]
fn main() {
#[rapx::requires(Opened(fd))]
}

Owning(ptr)

ownership(*p) == none — the pointer is the sole carrier of ownership; no live owner aliases the pointee. psp IV.1.

#![allow(unused)]
fn main() {
#[rapx::invariant(Owning(ptr))]
}

Pinned(p, l)

∀t ∈ 0..l, &(*p)_0 = p_t — the target is pinned for lifetime l (its address will not change). psp V.1.

#![allow(unused)]
fn main() {
#[rapx::requires(Pinned(ptr, 'a))]
}

Ptr2Ref(ptr, T)

Init(p, T, 1) ∧ Align(p, T) ∧ Alias(p, ret) — a raw pointer meets all requirements for sound reference conversion. primitive-sp §2.2.

#![allow(unused)]
fn main() {
#[rapx::requires(Ptr2Ref(ptr, T))]
}

Size(T, c) / NonSize(T, c)

sizeof(T) = c — the type T has the specified byte size. Three forms for c:

• Constant: Size(T, 1) — exact byte size (implies T: Sized). Size(T, 0) for ZST.
• sized: Size(T, sized) — T: Sized, non-ZST (default for generics).
• unsized: Size(T, unsized) — !Sized (for ?Sized bounds).

NonSize is an alias for Size. psp I.2.

#![allow(unused)]
fn main() {
#[rapx::requires(Size(T, 1))]
#[rapx::requires(Size(T, sized))]
}

SplitTransmute([Src], [Dst])

A Typed variant for slice-level transmutation: every size_of(Dst)-byte window within [Src] is a valid Dst value, without requiring alignment. Both [Src] and [Dst] are slice types.

#![allow(unused)]
fn main() {
#[rapx::requires(SplitTransmute([T], [U]))]
}

Trait(T, trait)

The type T implements the specified trait — trait ∈ traitimpl(T). psp V.4.

#![allow(unused)]
fn main() {
#[rapx::requires(Trait(T, Copy))]
}

Typed(ptr, Ty)

The memory at ptr satisfies TypeInvariant(T) — it was created as type T and has not been type-punned. Weaker than Init: does not require initialized content. psp III.6.

#![allow(unused)]
fn main() {
#[rapx::requires(Typed(ptr, T))]
}

Unreachable

The code path is unreachable. psp V.5.

#![allow(unused)]
fn main() {
#[rapx::requires(Unreachable)]
}

Unwrap(x, variant)

unwrap(x) = variant — the Option/Result is in the expected variant (Some, Ok, Err). psp III.5.

#![allow(unused)]
fn main() {
#[rapx::requires(Unwrap(self, Some))]
#[rapx::requires(Unwrap(self, Ok))]
}

ValidCStr(ptr, len)

The C string at ptr is null-terminated at byte position len with no interior null bytes. psp III.3.

#![allow(unused)]
fn main() {
#[rapx::requires(ValidCStr(ptr, 1))]
}

ValidNum(predicate) / ValidNum(value, interval)

Numeric constraints. Two forms: psp III.1.

1-arg predicate form — a comparison expression. Supported operators: <, <=, >, >=, ==, !=. A bare identifier is treated as != 0.

#![allow(unused)]
fn main() {
#[rapx::requires(ValidNum(index < len))]
#[rapx::requires(ValidNum(size_of::<T>() * len <= isize::MAX))]
}

2-arg interval form — a value constrained to a range. The interval can be an array literal [lo, hi] (inclusive both ends) or a string using bracket notation "[lo, hi]" where [/] means inclusive and (/) means exclusive:

#![allow(unused)]
fn main() {
#[rapx::requires(ValidNum(mid, [0, len]))]           // 0 <= mid <= len
#[rapx::requires(ValidNum(mid, "[0, self.len]"))]    // 0 <= mid <= self.len
#[rapx::requires(ValidNum(x, "[0, 10)"))]            // 0 <= x < 10
}

ValidPtr(ptr, Ty, count)

For ZSTs vacuously true; for non-ZSTs equivalent to Allocated(ptr, Ty, count) ∧ InBound(ptr, Ty, count) — the pointer points to a live allocation and the access range is within bounds. primitive-sp §2.2.

#![allow(unused)]
fn main() {
#[rapx::requires(ValidPtr(ptr, u32, len))]
}

ValidString(ptr, u8, len)

The byte data at ptr for len bytes is valid UTF-8. psp III.2.

#![allow(unused)]
fn main() {
#[rapx::requires(ValidString(v, u8, 1))]
}

ValidTransmute(Src, Dst)

A Typed variant for transmutation: memory of type Src satisfies TypeInvariant(Dst) when Dst is structurally composed of Src (exact type equality, array/tuple/simd/transparent decomposition). Both args are types.

#![allow(unused)]
fn main() {
#[rapx::requires(ValidTransmute(u32, [u8; 4]))]
}

8.3.1.2 User-Defined Contracts

In addition to the built-in tags, you can define new named contracts inside your crate with the pred! macro (from rapx_macros). A user-defined contract is a boolean combination of the primitive properties: it adds no new semantics — it is a pure front-end that expands to ordinary Property objects, so no rapx rebuild is required.

To use pred!, add rapx-macros as a dependency and enable the rapx tool attribute — the same nightly register_tool setup used for every #[rapx::...] attribute (see §8.3.2.1):

[dependencies]
rapx-macros = "0.7.34"

#![allow(unused)]
#![feature(register_tool)]
#![register_tool(rapx)]
fn main() {
}

A def is written as a pred! block of the form Name(params) { body }. Its parameters are typed Ptr (a target place), Ty (a type), Expr (a numeric expression), or Ident (an identifier such as a trait name, enum variant, allocator, or lifetime). By convention the contract name is CamelCase, matching the built-in compounds (ValidPtr, Deref, Ptr2Ref, …):

#![allow(unused)]
fn main() {
use rapx_macros::pred;

pred!(MySafeRead(p: Ptr, T: Ty, n: Expr) { NonNull(p) && Align(p, T) && Allocated(p, T, n) });
}

The block is not compiled as Rust: the macro serializes its source text into a #[rapx::def_contract("...")] tool attribute that the verifier parses at analysis time. Once defined, the name becomes a first-class tag usable wherever a property is expected:

#![allow(unused)]
fn main() {
#[rapx::requires(MySafeRead(ptr, u8, len))]
pub unsafe fn read_byte(ptr: *const u8, len: usize) -> u8 {
    unsafe { *ptr }
}
}

DSL grammar

A def body is parsed by a small pest grammar (the single source of truth, in grammar.pest). The surface:

Boolean composition — the body is a DNF expression: || separates disjuncts, && joins conjuncts, and parentheses group a conjunction into a single disjunct.

def_body = or_expr
or_expr = and_expr ("||" and_expr)*
and_expr = def_leaf ("&&" def_leaf)*
def_leaf = tag_call | "(" or_expr ")"

#![allow(unused)]
fn main() {
pred!(DerefOrNull(p: Ptr, T: Ty, n: Expr) { Null(p) || (Allocated(p, T, n) && InBound(p, T, n)) });
}

Argument expressions — a tag's arguments are numeric/place expressions with the usual operators:

Built-in functions — size_of(T), align_of(T), len(x), min(a, b), max(a, b). Turbofish size_of::<T>() is not supported — write size_of(T).

Places and projections — a place is self, return, Arg_N, or an identifier, optionally followed by projections:

• .0 / .name — field access (self.0, self.ptr).
• .unwrap_some() — unwrap an Option payload (head.unwrap_some()).
• .iter() — iterate the elements of a container (buckets.iter()).

Type-level constants — T::MAX, T::MIN (e.g. isize::MAX).

Conditionals — if cond { e1 } else { e2 } is an expression usable in argument (Expr) position, e.g. to special-case ZSTs (as in the std-challenge-18 case study):

#![allow(unused)]
fn main() {
pred!(ZstAwareInBound(ptr: Ptr, T: Ty, end_or_len: Expr) {
    InBound(ptr, T, if size_of(T) == 0 { 0 } else { (end_or_len - ptr) / size_of(T) })
});
}

!x.is_empty() is sugar for len(x) != 0, usable as a condition or ValidNum predicate when x is a slice/container place such as self (e.g. ValidNum(!self.is_empty())) — not for a raw pointer.

A def body may reference other defs as well as primitives. The same mechanism defines RAPx's built-in compound properties (ValidPtr, Deref, Ptr2Ref, …) in std-contracts.rs — using the same Name(params) { body } syntax, so a user can read the bundled compounds and write their own the same way. See tests/verify_units/dsl_custom_def for a complete SOUND example.

8.3.2 Contract Annotation

8.3.2.1 Direct Annotation

Contracts written in source use register_tool tool attributes; the crate (or module) must enable the tool:

#![allow(unused)]
#![feature(register_tool)]
#![register_tool(rapx)]
fn main() {
}

Three attributes carry contracts:

• #[rapx::requires(...)] — a precondition on an (usually unsafe) function. Multiple properties can be comma-grouped or the attribute repeated.
• #[rapx::invariant(...)] — a struct-level invariant that must hold for every instance at all observable points (see Chapter 8.4).
• #[rapx::verify] — marks a function as a verification entry point for --mode targeted (Chapter 8.1.2).

#![allow(unused)]
fn main() {
#[rapx::requires(ValidPtr(ptr, u32, len))]
#[rapx::requires(Align(ptr, u32))]
#[rapx::requires(ValidNum(index < len))]
pub unsafe fn write_slice(ptr: *mut u32, len: usize, index: usize) {
    // ...
}
}

The any(D1, D2) combinator expresses a null guard: any(Null(p), (P1(p, ...), P2(p, ...))) — the conjunct properties hold when p is non-null, and the whole contract is vacuously satisfied when p is null.

A property may carry kind = "precond" | "hazard" | "option" metadata (e.g. #[rapx::requires(..., kind = "hazard")]); Alias is always classified hazard.

Places accepted in annotations: parameter names (self, ptr, index, len), field names in invariant (ptr, cap, head — no self. prefix), field projections (self.0, self.ptr), length sugar (self.len → len(self)), and const generics (N).

8.3.2.2 JSON Contracts

Standard-library functions that cannot be annotated upstream use JSON contracts in std-public-contracts.json. Each entry maps a function path to a list of { "tag": ..., "args": [...] } objects:

{
  "core::ptr::const_ptr::add": [
    { "tag": "NonNull", "args": ["self"] },
    { "tag": "Align",   "args": ["self", "T"] },
    { "tag": "InBound", "args": ["self", "T", "count"] }
  ]
}

Argument strings use the same expression grammar as direct annotations. Path lookup first tries an exact match on the cleaned def-path, then falls back to wildcard segment replacement (e.g. core::slice::<impl [T]>::* → core::slice::*).

8.3.3 Inspecting Contracts with --debug-contracts

Pass --debug-contracts to see every contract assertion expanded with its semantic meaning. While --prepare-targets (§8.2.3) shows which contracts attach to each verification target, --debug-contracts shows what each contract means — the concrete SMT obligation. Note that --prepare-targets and --debug-contracts are mutually exclusive; run them in separate invocations for both views.

Example output from the linked_list_nonnull case study (continued from §8.2.3):

13:10:58|RAPx|INFO|: ============================================================================
13:10:58|RAPx|INFO|: [rapx::debug-contracts] struct: LinkedList
13:10:58|RAPx|INFO|: ============================================================================
13:10:58|RAPx|INFO|:   [Struct Invariants]:
13:10:58|RAPx|INFO|:   |- Align(head.unwrap_some(), Node<T>)
13:10:58|RAPx|INFO|:   |  (head.unwrap_some() as usize) % align_of::<Node<T>>() == 0
13:10:58|RAPx|INFO|:   |- Allocated(head.unwrap_some(), Node<T>, 1)
13:10:58|RAPx|INFO|:   |  head.unwrap_some() points to a live allocation of size: size_of(Node<T>) * 1
13:10:58|RAPx|INFO|:   |- Typed(head.unwrap_some(), Node<T>)
13:10:58|RAPx|INFO|:   |  *head.unwrap_some() holds TypeInvariant(Node<T>)
13:10:58|RAPx|INFO|:   `- Owning(head.unwrap_some())
13:10:58|RAPx|INFO|:      ownership(*head.unwrap_some()) = none: no live owner aliases the pointee
13:10:58|RAPx|INFO|: 
13:10:58|RAPx|INFO|: |- --- method: pop_front ---------------------------------------------------
13:10:58|RAPx|INFO|: |   fn LinkedList::<T>::pop_front(&mut self: &mut LinkedList<T>) -> std::option::Option<T>
13:10:58|RAPx|INFO|: |   [Unsafe Callees]:
13:10:58|RAPx|INFO|: |   |- fn std::boxed::Box::<T>::from_raw(raw: *mut T) -> std::boxed::Box<T>
13:10:58|RAPx|INFO|: |   | |- Align(raw, T)
13:10:58|RAPx|INFO|: |   | |  (raw as usize) % align_of::<T>() == 0
13:10:58|RAPx|INFO|: |   | |- Allocated(raw, T, 1, global)
13:10:58|RAPx|INFO|: |   | |  raw points to a live allocation of size: size_of(T) * 1
13:10:58|RAPx|INFO|: |   | |- Typed(raw, T)
13:10:58|RAPx|INFO|: |   | |  *raw holds TypeInvariant(T)
13:10:58|RAPx|INFO|: |   | |- Owning(raw)
13:10:58|RAPx|INFO|: |   | |  ownership(*raw) = none: no live owner aliases the pointee
13:10:58|RAPx|INFO|: |   | `- [hazard] Alias(raw, ret)
13:10:58|RAPx|INFO|: |   |    raw and ret alias each other (hazard)
13:10:58|RAPx|INFO|: |   `- fn std::ptr::NonNull::<T>::as_mut::<'a>(&mut self: &mut std::ptr::NonNull<T>) -> &'a mut T
13:10:58|RAPx|INFO|: |     `- Ptr2Ref(self.0, T)
13:10:58|RAPx|INFO|: |        A raw pointer meets all requirements for sound &/&mut conversion: initialized, aligned, no aliasing conflict.
13:10:58|RAPx|INFO|: 
13:10:58|RAPx|INFO|: ... (8 more methods)

Chapter 8.4. The Verification Pipeline

This chapter walks through the verification pipeline using the linked_list_nonnull case study — a doubly-linked list built with NonNull<Node> pointers:

#![allow(unused)]
fn main() {
#[rapx::invariant(Align(head.unwrap_some(), Node))]
#[rapx::invariant(Allocated(head.unwrap_some(), Node, 1))]
#[rapx::invariant(Typed(head.unwrap_some(), Node))]
#[rapx::invariant(Owning(head.unwrap_some()))]
#[rapx::invariant(Align(tail.unwrap_some(), Node))]
#[rapx::invariant(Allocated(tail.unwrap_some(), Node, 1))]
#[rapx::invariant(Typed(tail.unwrap_some(), Node))]
#[rapx::invariant(Owning(tail.unwrap_some()))]
struct LinkedList { head: Option<NonNull<Node>>, tail: Option<NonNull<Node>> }
}

Running cargo rapx verify on the case study produces:

02:43:07|RAPx|INFO|: Start analysis with RAPx.
02:43:07|RAPx|INFO|: ============================================================
02:43:07|RAPx|INFO|: [rapx::verify] function: LinkedList::<T>::new
02:43:07|RAPx|INFO|: ============================================================
02:43:07|RAPx|INFO|:   --- struct invariants ---
02:43:07|RAPx|INFO|:       checkpoint bb0:
02:43:07|RAPx|INFO|:         path 0:
02:43:07|RAPx|INFO|:           ├── Align | Proved (x2)
02:43:07|RAPx|INFO|:           ├── Allocated | Proved (x2)
02:43:07|RAPx|INFO|:           ├── Typed | Proved (x2)
02:43:07|RAPx|INFO|:           └── Owning | Proved (x2)
02:43:07|RAPx|INFO|:   result: SOUND
02:43:07|RAPx|INFO|:
...
02:43:07|RAPx|INFO|: ============================================================
02:43:07|RAPx|INFO|: [rapx::verify] function: <LinkedList<T> as std::ops::Drop>::drop
02:43:07|RAPx|INFO|: ============================================================
02:43:07|RAPx|INFO|:   --- unsafe checkpoints ---
02:43:07|RAPx|INFO|:       unsafe checkpoint: bb2 -> core::ptr::non_null::as_ref
02:43:07|RAPx|INFO|:         path [0, 1, 2]:
02:43:07|RAPx|INFO|:           Ptr2Ref | Proved
02:43:07|RAPx|INFO|:         path [0, 1, 2, 3, 4, 5, 6, 1, 2]:
02:43:07|RAPx|INFO|:           Ptr2Ref | Proved
02:43:07|RAPx|INFO|:         ... (2 deeper paths, all Proved)
02:43:07|RAPx|INFO|:       unsafe checkpoint: bb4 -> alloc::boxed::from_raw
02:43:07|RAPx|INFO|:         path [0, 1, 2, 3, 4]:
02:43:07|RAPx|INFO|:           ├── Align | Proved (x3)
02:43:07|RAPx|INFO|:           ├── Allocated | Proved (x3)
02:43:07|RAPx|INFO|:           ├── Typed | Proved (x3)
02:43:07|RAPx|INFO|:           ├── Owning | Proved (x3)
02:43:07|RAPx|INFO|:           └── [hazard] Alias | Proved (x3)
02:43:07|RAPx|INFO|:         path [0, 1, 2, 3, 4, 5, 6, 1, 2, 3, 4]:
02:43:07|RAPx|INFO|:           ├── Align | Proved (x3)
02:43:07|RAPx|INFO|:           ├── Allocated | Proved (x3)
02:43:07|RAPx|INFO|:           ├── Typed | Proved (x3)
02:43:07|RAPx|INFO|:           ├── Owning | Proved (x3)
02:43:07|RAPx|INFO|:           └── [hazard] Alias | Proved (x3)
02:43:07|RAPx|INFO|:         ... (2 deeper paths, all Proved)
02:43:07|RAPx|INFO|:   result: SOUND
02:43:07|RAPx|INFO|:

The report covers 13 targets:

For each target the pipeline runs: path extraction → backward slicing → symbolic VM execution → SMT check. The sections below use <LinkedList as Drop>::drop as the running example — it has two unsafe callsites (as_ref for Ptr2Ref, Box::from_raw for Allocated/Owning/Alias) inside a while let loop, making it a compact but representative walkthrough.

8.4.1 Path Extraction

The first stage enumerates acyclic paths from function entry to each unsafe callsite using PathGraph's SCC decomposition (see §5.1 Path Analysis for the full algorithm). Each path is a sequence of basic block IDs.

The drop function contains a while let loop over the linked list nodes:

#![allow(unused)]
fn main() {
fn drop(&mut self) {
    let mut current = self.head;
    unsafe {
        while let Some(node) = current {
            current = node.as_ref().next;        // ← Ptr2Ref at as_ref
            drop(Box::from_raw(node.as_ptr())); // ← Allocated/Owning/Alias at from_raw
        }
    }
}
}

The while let body forms an SCC (bb2 → bb3 → bb4 → bb5 → bb6 → bb1 → bb2). Depending on the repeat budget, the path extractor unrolls this SCC, producing one path per loop iteration depth:

Checkpoint bb2 -> as_ref (Ptr2Ref):

path [0, 1, 2]                                  → 1 element, 1st iteration
path [0, 1, 2, 3, 4, 5, 6, 1, 2]               → 2 elements, 2nd iteration
path [0, 1, 2, 3, 4, 5, 6, 1, 2, 3, 4, 5, 6, 1, 2]  → 3 elements, 3rd iteration

Checkpoint bb4 -> from_raw (Allocated/Owning/Alias):

path [0, 1, 2, 3, 4]                            → 1 element
path [0, 1, 2, 3, 4, 5, 6, 1, 2, 3, 4]         → 2 elements
path [0, 1, 2, 3, 4, 5, 6, 1, 2, 3, 4, 5, 6, 1, 2, 3, 4]  → 3 elements

Each path records exactly one visit to the target callsite after the prescribed number of loop iterations. The sections below use the shortest from_raw path as the running example:

path [0, 1, 2, 3, 4]   →   Allocated/Typed/Owning | Proved, Alias | Proved

Paths are stored in a PathTree per callsite and capped at 1024. By default, auto mode chooses the repeat budget before path extraction. With --postfix-repeat=N, verification uses the fixed repeat count N.

8.4.2 Backward Slicing

Take the path [0, 1, 2, 3, 4] — a single-element list: self.head is Some, the while let enters once, as_ref at bb2 exposes the node, and Box::from_raw at bb4 frees it. The relevant MIR blocks:

bb0:  {
    _2 = move (_1.0: Option<NonNull<Node<T>>>)   // current = self.head
}
bb1:  {
    _3 = discriminant(_2)
    switchInt(move _3) → [0: bb7, 1: bb2]         // None → exit, Some → loop
}
bb2:  {
    _4 = copy ((_2 as Some).0)                    // extract NonNull from Option
    _6 = &mut _4
    _5 = NonNull::<Node<T>>::as_ref(move _6)      // ← CHECKPOINT: Ptr2Ref
}
bb3:  {
    _7 = &(*_5).next
    _2 = move _7                                  // current = node.next
}
bb4:  {
    _8 = NonNull::<Node<T>>::as_ptr(copy _4)
    _9 = Box::<Node<T>>::from_raw(move _8)        // ← CHECKPOINT
}
bb5:  {
    drop(_9)                                      // free the Box
}
bb6:  {
    goto → bb1                                    // loop back
}
bb7:  {
    return
}

The BackwardSlicer extracts only the MIR statements that contribute to the target place's value — everything else is dropped.

Walk backward from _9 = Box::from_raw(move _8):

The collected chain is _9 → _8 → _4 → _2 → _1.0 (where _1.0 is the head field of LinkedList). The slicer recognises standard-library calls by their effects: NonNull::as_ptr → returns a raw pointer to the same allocation; ((_2 as Some).0) → projection from Option to inner NonNull.

No ContractFact items are injected — drop has no #[rapx::requires] of its own.

8.4.3 Symbolic VM Execution

The SymbolicVm (vm/mod.rs) is a semantic MIR executor that replaces the earlier pattern-matching forward verifier. Instead of deriving ad-hoc facts from MIR patterns, it executes the retained MIR items from the backward slicer and directly builds symbolic state (VmState) with Z3 terms for every value.

8.4.3.1 Building symbolic state before the checkpoint

The VM executes retained MIR items in forward path order. Each MIR statement and terminator is translated into a transfer function that updates VmState:

At execution time, the VM tracks:

• local_addresses: The numeric address bound to each MIR local
• allocations: All known memory allocations with their size, element count, type, and provenance
• init_allocations: Allocations that have been written to (initialized)
• path_conditions: Accumulated branch constraints from SwitchInt and Assert terminators

At the from_raw checkpoint, the verifier resolves the value chain _9 → _8 → _4 → _2 → _1.0 through the VM's provenance tracking. The origin _1.0 (self.head) is a NonNull<Node<T>> pointer stored in the struct — its provenance was tracked from the struct invariant that guarantees Allocated(head.unwrap_some(), Node, 1).

8.4.3.2 Hazard tracking (Alias)

Box::from_raw declares the Alias(p, ret) hazard: _9 takes ownership of the allocation at _8, and the verifier must prove that no other live pointer aliases the same memory at this point. The PropertyChecker checks that the origin pointer's allocation is not referenced by any other live local or field.

In drop, after _2 is updated to node.next in bb3, the original _4 pointer is the only remaining handle to the old node's allocation. The verifier confirms no conflicting alias exists → Alias | Proved.

8.4.4 SMT Check

The PropertyChecker (property_checker) translates the VM state into Z3 assertions and checks each safety property:

• Value-definition chain. MIR assignments create symbolic Z3 terms for each local. _8 is defined as the raw pointer from _4, which projects from _2, which originates from self.head. The Z3 model follows this value chain — no separate equality assertion needed.
• Allocation model. Each allocation records its base address, element size (from sizeof(T)), and element count. The VM asserts that the address range is within the allocation bounds.
• Initialization tracking. The struct invariant Allocated(head.unwrap_some(), Node, 1) tells the verifier that self.head's allocation holds one initialized Node<T>. The VM propagates this to _4 → _8.
• Path conditions. The switchInt at bb1 constrains the solver: _2 is Some.

The check uses negation-as-failure: assert all constraints from VmState, assert the negated goal, solve — Unsat → Proved, Sat → Failed.

For Box::from_raw on _8, five obligations are checked:

Align

constraints ∧ ¬(_8 % align_of::<Node<T>>() = 0)

The struct invariant Align(head.unwrap_some(), Node) guarantees self.head is aligned. The VM propagates alignment through the value chain _1.0 → _2 → _4 → _8. The negated goal contradicts the invariant → Unsat → Align | Proved.

Allocated

Allocated means _8 points to a live heap allocation of size sizeof(Node<T>).

• Is it heap-allocated? The struct invariant Allocated(head.unwrap_some(), Node, 1) guarantees self.head owns a heap allocation.
• Fits within bounds? The allocation has element_count = 1, and Box::from_raw consumes exactly 1 element.

The negated goal contradicts the invariant → Unsat → Allocated | Proved.

Typed

Typed(p, T) means the allocation at p holds valid data of type T. The struct invariant Typed(head.unwrap_some(), Node) is propagated through the value chain. Negating it contradicts the invariant → Typed | Proved.

Owning

Owning(p) means the current function holds unique ownership of allocation p — no other code can access it. When drop takes &mut self, it has exclusive access to the struct's fields, including head. The invariant Owning(head.unwrap_some()) confirms the struct owns the allocation, and the &mut self receiver transfers that ownership to drop. Negating → Unsat → Owning | Proved.

Alias

constraints ∧ (another live pointer aliases _8)

After _2 is updated to node.next in bb3, the VM confirms _4 is the only handle to the old node's allocation. No other local or field points to the same memory → Unsat → Alias | Proved.

8.4.5 Auto-Repeat Planner

For the bb4 -> from_raw checkpoint, Box::from_raw requires Allocated, Owning, and Alias (plus Align/Typed propagated from the struct invariants). The SCC in drop (the while let loop) means the pointer's origin — self.head — remains valid across iterations: after freeing the first node, current advances to node.next, which is also covered by the head invariant.

The planner recognises that deeper unrolling still satisfies the same invariants and produces increasing path depths. The shortest path (depth 0) contains a single loop iteration:

depth 0:  path [0, 1, 2, 3, 4]               — 1  body iteration
depth 1:  path [0, 1, 2, 3, 4, 5, 6, 1, 2, 3, 4]    — 2  body iterations
depth 2:  path [0, 1, 2, 3, 4, 5, 6, 1, 2, 3, 4, 5, 6, 1, 2, 3, 4]  — 3  body iterations

All five properties (Align, Allocated, Typed, Owning, Alias) are proved at each depth, with the shortest path covered by multiple rounds (producing Proved (x3) in the output). The Proved set is identical across all three depths — deeper paths do not reveal a violating state, and the final verdict remains SOUND.

The repeat planner only decides how many loop repetitions should be explored. The backward slicer, symbolic VM, and SMT checker then run on the extracted paths as usual.

Chapter 9. Utilities

This chapter introduces some utilities and gatgets of RAPx, which help printing user-friendly debug messages or implement other functionality.

Chapter 9.1 Logging and Diagnostics

RAPx provides two complementary systems for output: a leveled logging framework for development and debugging, and a diagnostic rendering utility for user-facing error reports with annotated source code.

Logging Macros

The logging system is implemented in rapx/src/utils/log.rs, built on the fern and log crates. It provides five macros at increasing severity:

All macros use the target "RAPx", are defined as #[macro_export], and format output with timestamps and colored level prefixes:

HH:MM:SS|RAPx|LEVEL|: message

Example output:

21:50:18|RAPx|INFO|: Start analysis with RAP.
21:50:18|RAPx|INFO|: Alias found in Some("::foo"): {(0,1)}
21:50:20|RAPx|WARN|: no safety contracts found for std callee "core::ptr::read"
21:50:21|RAPx|INFO|: SafetyFlow summary: 42 function(s), 87 call edge(s)

Environment Variable

The log level is controlled by RAPX_LOG:

RAPX_LOG=info   cargo rapx analyze alias      # default — summary output
RAPX_LOG=debug  cargo rapx verify              # + path/fact detail
RAPX_LOG=trace  cargo rapx analyze dataflow    # + full internal state
RAPX_LOG=warn   cargo rapx check -f             # warnings only, use-after-free detection
RAPX_LOG=error  cargo rapx verify              # errors only

The default level (when RAPX_LOG is unset) is INFO.

Log Format

init_log() configures fern with:

• Timestamps via chrono::Local
• Colored output via fern::colors::ColoredLevelConfig: Trace=Cyan, Debug=Blue, Info=White+Green, Warn=Yellow, Error=Red
• stderr output only (stdout is avoided due to compatibility issues)

Diagnostic Rendering

For user-facing error reports (e.g., "cloning detected here"), RAPx uses the annotate_snippets crate to render annotated source code with underlines and messages. The span utility functions in rapx/src/utils/span.rs bridge rustc's Span objects to annotate_snippets's offset-based API.

Span Utilities

The key pattern: use relative_pos_range(background_span, target_span) to convert a rustc Span into a byte offset range that annotate_snippets can underline.

Rendering Example

A typical diagnostic report (from the memory-cloning checker in rapx/src/check/opt/memory_cloning/):

#![allow(unused)]
fn main() {
fn report_used_as_immutable(graph: &Graph, clone_span: Span, use_span: Span) {
    let code_source = span_to_source_code(graph.span);
    let filename = span_to_filename(clone_span);

    let snippet = Snippet::source(&code_source)
        .line_start(span_to_line_number(graph.span))
        .origin(&filename)
        .fold(true)
        .annotation(
            Level::Error
                .span(relative_pos_range(graph.span, clone_span))
                .label("Cloning happens here."),
        )
        .annotation(
            Level::Error
                .span(relative_pos_range(graph.span, use_span))
                .label("Used here"),
        );

    let message = Level::Warning
        .title("Unnecessary memory cloning detected")
        .snippet(snippet)
        .footer(Level::Help.title("Use borrowings instead."));

    let renderer = Renderer::styled();
    println!("{}", renderer.render(message));
}
}

When clone_span and use_span reference separate lines within a function, the renderer produces text like:

warning: Unnecessary memory cloning detected
  --> src/main.rs:15:9
   |
15 |       let cloned = value.clone();
   |                    ^^^^^^^^^^^^^ Cloning happens here.
...
25 |       process(&cloned);
   |               ^^^^^^^ Used here
   |
   = help: Use borrowings instead.

Building Messages

annotate_snippets messages are assembled from:

• .title(): A one-line summary (Warning, Error, or Info level).
• .snippet(): A Snippet pointing to source code with .line_start(), .origin() (file path), and one or more .annotation() calls.
• .annotation(): A Level + .span(byte_range) + .label("explanation") triple.
• .footer(): Optional footer with Level::Help for fix suggestions.
• Renderer::styled(): Renders with ANSI colors for terminal output.

Chapter 10. Case Study

This chapter presents case studies applying RAPx to real-world Rust projects.

Chapter Outline

• 10.1 Verifying core::slice Safety (Challenge 17) — verifying safety contracts in the Rust standard library's slice module
• 10.2 Asterinas — applying RAPx to the Asterinas OS kernel

Chapter 10.1. Verifying core::slice Safety (Challenge 17)

This case study demonstrates how RAPx verifies safety contracts in the Rust standard library's slice module, targeting Challenge 17: Verify the safety of slice functions from the Verify Rust Std Lib project.

10.1.1 Goal

Prove that all 37 challenge-listed functions in library/core/src/slice/mod.rs are free of undefined behavior by:

• Writing #[rapx::requires(...)] safety preconditions on unsafe callees
• Adding #[rapx::verify] annotations to trigger verification
• Running RAPx in targeted mode against the annotated functions

The verification must be unbounded (valid for slices of arbitrary length) and must hold for generic type T without monomorphization.

10.1.2 Tool Integration

Following the same conditional pattern as Kani (#[cfg_attr(kani, ...)]) and Flux (#[cfg(flux)]), the project uses cfg_attr to avoid hard-coding register_tool in source code:

• core/src/lib.rs: No #![register_tool(rapx)] — tool registration is injected via RUSTFLAGS
• core/Cargo.toml: ['cfg(rapx)'] declared in [lints.rust.unexpected_cfgs] to suppress unknown cfg warnings
• Source files: #[cfg_attr(rapx, rapx::verify)] and #[cfg_attr(rapx, rapx::requires(...))] conditionally activate only when RAPx runs

#![allow(unused)]
fn main() {
// Example from core/src/slice/mod.rs
#[cfg_attr(rapx, rapx::verify)]
#[cfg_attr(rapx, rapx::requires(ValidNum(a, "[0,self.len())")))]
#[cfg_attr(rapx, rapx::requires(ValidNum(b, "[0,self.len())")))]
pub const unsafe fn swap_unchecked(&mut self, a: usize, b: usize) { /* ... */ }
}

Run verification:

cd library/core
RUSTFLAGS="--cfg=rapx -Zcrate-attr=feature(register_tool) -Zcrate-attr=register_tool(rapx)" \
  cargo rapx verify --module slice --mode targeted

Note: Commands must be run from library/core, not the library workspace root. In the library workspace, core is only a dependency (the members are std, sysroot, coretests, alloctests), and RAPx analyzes a crate only when it is compiled as the primary package. Running from library/core makes core local, so its #[rapx::verify] annotations are visible without needing the --crate core filter.

The RUSTFLAGS environment variable provides three things:

A GitHub Actions workflow (.github/workflows/rapx.yml) runs verification on every push and pull request, using the same RUSTFLAGS setup. It pins a specific RAPx commit via RAPX_VERSION, cds into library/core, and invokes cargo rapx verify --module slice --mode targeted.

10.1.3 Function-by-Function Verification

Slice type invariant. Every target is a method on the primitive [T] (no #[rapx::invariant] struct), so RAPx relies on the slice type invariant declared in std-type-invariants.json under the [T] key. This runs in two independent places:

1. Entry (init_parameters) — for a &[T] / &mut [T] parameter self, the VM establishes the slice's validity as symbolic state:

   • the slice type invariant (re-proved at return): NonNull (flag non_null), Align (flag aligned), the length bound len * size_of(T) <= isize::MAX, and any(len(self) == 0, (Allocated, Init)) — the data allocation itself plus element initialization, required only for non-empty slices;
   • entry fact: the non-negativity bound 0 <= len (the usize length is never negative);
   • the data allocation itself carries align = align_of(T), size = len · sizeof_T, element_ty = T, where sizeof_T is the shared symbolic element size (≥ 1 for a generic T; the invariant's size_of(T) bound is instead the concrete impl-layout size).

2. Return (type-invariant re-proof) — the properties re-proved at the function's Return block are exactly the ones declared by the JSON entry:

"[T]": {
  "invariants": [
    { "tag": "NonNull", "args": ["$self"] },
    { "tag": "Align", "args": ["$self", "$elem"] },
    { "tag": "ValidNum", "args": ["size_of($elem) * len($self) <= isize::MAX"] },
    {
      "any": [
        { "tag": "ValidNum", "args": ["len($self) == 0"] },
        [
          { "tag": "Allocated", "args": ["$self", "$elem", "len($self)"] },
          { "tag": "Init", "args": ["$self", "$elem", "len($self)"] }
        ]
      ]
    }
  ]
}

NonNull and Align hold for every slice — even an empty one, whose dangling data pointer (NonNull::dangling) is still non-null and properly aligned (Rust requires alignment for size-0 access). Allocated and Init hold only for non-empty slices, so they are wrapped in any(len == 0, …). The length bound len * size_of(T) <= isize::MAX is part of the re-proved invariant — for the parameter it is fixed at entry (the reference's address and length are immutable), and for a returned slice it is re-proved at return (and re-enforced at from_raw_parts, whose own contract carries the same ValidNum). The 0 <= len bound is just the usize non-negativity. Align is likewise re-checked at &*ptr (Ptr2Ref = Init + ValidPtr + Align + Alias, where ValidPtr = NonNull + Deref).

10.1.3.1 get_unchecked

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
#[cfg_attr(rapx, rapx::requires(InBound(self, index)))]
pub const unsafe fn get_unchecked<I>(&self, index: I) -> &I::Output
where
    I: [const] SliceIndex<Self>,
{
    unsafe { &*index.get_unchecked(self) }
}
}

Verification Targets. The body &*index.get_unchecked(self) desugars into two unsafe operations:

(1) index.get_unchecked(self) — the SliceIndex::get_unchecked trait call, returning a raw pointer *const Output.

(2) &*ptr — the raw-pointer dereference that turns that pointer back into a reference. RAPx models this as a Ptr2Ref(p, T) checkpoint, decomposed into four obligations: Init(p, T, 1) + ValidPtr(p, T, 1) + Align(p, T) + Alias(p), where ValidPtr = NonNull + Deref.

On top of these, the &[T] receiver self carries a slice type invariant (NonNull + Align + ValidNum(size_of(T)·len <= isize::MAX) + any(len == 0, (Allocated, Init))) that init_parameters establishes at entry and that is re-proved at the function's return block.

Path. The two unsafe operations sit on the normal path bb0 → bb1 (get_unchecked in bb0, the &* deref in bb1). The &[T] invariant is re-proved only at the return block bb1 — RAPx re-proves type invariants at Return blocks, not at the cleanup resume in bb2 (the panic-unwind path, never taken here).

MIR (compiled with nightly-2025-11-25; locals _1 = self, _2 = index):

bb0: _5 = move _2;
     _6 = &raw const (*_1);
     _4 = <I as SliceIndex<[T]>>::get_unchecked(move _5, move _6) -> [return: bb1, unwind: bb2];
bb1: _3 = &(*_4);   // &* — raw-pointer deref (Ptr2Ref checkpoint)
     _0 = &(*_3);   // safe reborrow, no checkpoint
     return;
bb2 (cleanup): resume;

Verification. The VM steps the path statement by statement. For every local it records a symbolic value (VmValue) with three parts:

• term — a Z3 integer: the pointer's address (for references/pointers) or the scalar's value;
• prov — provenance (alloc, offset): which allocation the pointer derives from, at what byte offset;
• flags — known invariants non_null / aligned / init.

alloc(x) is the memory object (Allocation) that local x points into — its prov carries an AllocId into the VM's allocation table, where each entry holds base / size / align and the marks initialized / alive_assumed / dead.

The #[rapx::requires] fact (InBound) is recorded at entry as the numeric bound index < len (a path condition), while the slice type invariant (NonNull/Align/ValidNum(size_of(T)·len <= isize::MAX)/any(len == 0, (Allocated, Init))) is established by init_parameters itself and re-proved at return. Each InBound checkpoint is discharged by SMT over that recorded bound and the allocation's base/size. For a generic T the element size is a shared symbolic constant sizeof_T (≥ 1) rather than a monomorphized byte count: the data allocation's byte size is len·sizeof_T, and the SMT cancels that factor (len·sizeof_T / sizeof_T = len) to recover the element count for InBound. The path, step by step:

entry   _1 = self (&[T]), _2 = index (I)

          init_parameters:
            data alloc: align = align_of(T), size = len · sizeof_T, element_ty = T, initialized = true
            _1: term = data base, prov = (data alloc, 0), flags { non_null, aligned, init }
               slice type invariant (JSON `[T]` entry; entry facts synthesized by `init_parameters`; re-proved at return):
                 NonNull(_1)
                 Align(_1, T)
                 len(_1)·size_of(T) ≤ isize::MAX   (size_of(T) = the concrete impl-layout bound, = 1 for a fully generic T)
                 any(len(_1) == 0, (Allocated(_1, T, len(_1)), Init(_1, T, len(_1))))
               entry fact: 0 ≤ len(_1)  (usize non-negativity)
            _2: term = param_2 (fresh symbolic)

          caller contracts (asserted as facts):
            InBound(_1, _2)      →  _2 < len(_1)

_5 = move _2
          VM  _5: term = _2.term

_6 = &raw const (*_1)
          VM  _6: term = _1.term, prov = _1.prov, flags { non_null }

_4 = get_unchecked(move _5, move _6)                    [checkpoint (1)]
          check  InBound(_6, _5)   ←  _5 < len(_6)         Proved
                              (SMT: _5 = _2 (move _2); _6 aliases _1, so len(_6) = len(_1)
                               = size/sizeof_T = len (cancels sizeof_T);
                               thus _5 < len(_6) ⟺ _2 < len(_1) — the `InBound(_1, _2)` entry fact)
          VM  _4: term = _6.term + _5·sizeof_T, prov = (_6.alloc, _6.offset + _5·sizeof_T)

_3 = &(*_4)                                             [checkpoint (2)]
          check  Init(_4, T, 1)     ←  alloc(_4).initialized         Proved
          check  ValidPtr(_4, T, 1) ←  non-null + in-bounds (within _1's data alloc)   Proved
          check  Align(_4, T)       ←  _6 aligned to T (from _1's data alloc), _5·sizeof_T keeps alignment   Proved
          check  Alias(_4)          ←  (hazard) _4 traces to &self, a shared borrow → aliasing safe   Proved
          VM  _3: term = _4.term, prov = _4.prov, flags { non_null, aligned, init }

_0 = &(*_3)
          VM  _0: term = _3.term, prov = _3.prov, flags { non_null, aligned, init }

return                                                   [type-invariant]
          check  NonNull(_1), Align(_1, T), len(_1)·size_of(T) ≤ isize::MAX,
                 any(len(_1) == 0, (Allocated(_1, T, len), Init(_1, T, len)))  ←  _1 unchanged   Proved

result: SOUND

10.1.3.2 get_unchecked_mut

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
#[cfg_attr(rapx, rapx::requires(InBound(self, index)))]
pub const unsafe fn get_unchecked_mut<I>(&mut self, index: I) -> &mut I::Output
where
    I: [const] SliceIndex<Self>,
{
    unsafe { &mut *index.get_unchecked_mut(self) }
}
}

Verification Targets. &mut *index.get_unchecked_mut(self) desugars into the same two unsafe callsites, on the mutable receiver:

(1) index.get_unchecked_mut(self) — the SliceIndex::get_unchecked_mut trait call, returning *mut Output.

(2) &mut *ptr — the reference creation from that raw pointer (a Ptr2Ref operation: Init + ValidPtr + Align + Alias, exclusive).

Path. Both callsites sit on the single normal path bb0 → bb1 (get_unchecked_mut in bb0, the &mut * deref in bb1); the cleanup blocks bb3…bb5 are dead on the normal path.

MIR. The statements on that path:

bb0: _8 = &raw mut (*_1);
     _6 = <I as SliceIndex<[T]>>::get_unchecked_mut(move _7, move _8) -> [return: bb1, unwind: bb3];
bb1: _5 = &mut (*_6);   // &mut * — raw-pointer deref (Ptr2Ref checkpoint)
     _4 = &mut (*_5);   // safe reborrows, no checkpoint
     _3 = &mut (*_4);
     _0 = &mut (*_3);
bb2: return

Verification. Same as get_unchecked, on the mutable receiver:

10.1.3.3 swap_unchecked

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
#[cfg_attr(rapx, rapx::requires(ValidNum(a, "[0,self.len())")))]
#[cfg_attr(rapx, rapx::requires(ValidNum(b, "[0,self.len())")))]
pub const unsafe fn swap_unchecked(&mut self, a: usize, b: usize) {
    assert_unsafe_precondition!(
        check_library_ub,
        "slice::swap_unchecked requires that the indices are within the slice",
        (len: usize = self.len(), a: usize = a, b: usize = b,) => a < len && b < len,
    );
    let ptr = self.as_mut_ptr();
    unsafe {
        ptr::swap(ptr.add(a), ptr.add(b));
    }
}
}

Verification Targets. The single unsafe callsite ptr::swap(ptr.add(a), ptr.add(b)):

#![allow(unused)]
fn main() {
// core::ptr::swap
#[rapx::requires(ValidPtr(x, T, 1))]
#[rapx::requires(Align(x, T))]
#[rapx::requires(ValidPtr(y, T, 1))]
#[rapx::requires(Align(y, T))]
}

Path. assert_unsafe_precondition! lowers to a precondition_check panic guard (guarded by UbChecks), which is not an unsafe checkpoint; the single unsafe callsite is reached on the normal path bb0 → bb1 → bb2 → bb3 → bb5 → bb6 → bb7 → bb8.

MIR. The statements on that path:

bb5: _11 = as_mut_ptr(&mut (*_1));
bb6: _14 = ptr.add(copy _11, _2);   // ptr.add(a)
bb7: _17 = ptr.add(copy _11, _3);   // ptr.add(b)
bb8: _13 = ptr::swap(move _14, move _17);   // ← checkpoint

Verification. The pipeline runs Entry → VM execution → property check over the extracted path.

Entry. The preconditions ValidNum(a, "[0,self.len())") and ValidNum(b, "[0,self.len())") (i.e. a < len && b < len), plus the &mut [T] slice invariant.

VM execution.

Property check. ptr.add(a) and ptr.add(b) stay within the slice because a < len and b < len, so both element pointers satisfy ValidPtr + Align (inherited from the slice's data pointer). ptr::swap is defined for a == b, so no overlap obligation arises.

10.1.3.4 as_chunks_unchecked

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
#[cfg_attr(rapx, rapx::requires(ValidNum(N, "[1,)")))]
#[cfg_attr(rapx, rapx::requires(ValidNum(len(self) % N == 0)))]
pub const unsafe fn as_chunks_unchecked<const N: usize>(&self) -> &[[T; N]] {
    assert_unsafe_precondition!(
        check_language_ub,
        "slice::as_chunks_unchecked requires `N != 0` and the slice to split exactly into `N`-element chunks",
        (n: usize = N, len: usize = self.len()) => n != 0 && len.is_multiple_of(n),
    );
    // SAFETY: Caller must guarantee that `N` is nonzero and exactly divides the slice length
    let new_len = unsafe { exact_div(self.len(), N) };
    // SAFETY: We cast a slice of `new_len * N` elements into
    // a slice of `new_len` many `N` elements chunks.
    unsafe { from_raw_parts(self.as_ptr().cast(), new_len) }
}
}

Verification Targets. Two unsafe callsites:

(1) exact_div(self.len(), N) — requires a non-zero divisor;

(2) from_raw_parts(self.as_ptr().cast(), new_len):

#![allow(unused)]
fn main() {
// core::slice::raw::from_raw_parts
#[rapx::requires(NonNull(data))]
#[rapx::requires(ValidPtr(data, T, len))]
#[rapx::requires(Init(data, T, len))]
#[rapx::requires(Alive(data, 'a))]
#[rapx::requires(Alias(data))]
#[rapx::requires(Align(data, T))]
#[rapx::requires(ValidNum(size_of(T) * len <= isize::MAX))]
}

Path. After the precondition_check guard, the two callsites are reached in order on the normal path … → bb7 → bb8 → bb9 → bb10 (exact_div in bb7, from_raw_parts in bb10).

MIR. The statements on that path:

bb6:  _8 = len(&(*_1));
bb7:  _7 = exact_div(move _8, const N);                  // ← checkpoint (1)
bb8:  _12 = as_ptr(&(*_1));
bb9:  _11 = ptr.cast::<[T; N]>(move _12);
bb10: _10 = raw::from_raw_parts(move _11, copy _7);      // ← checkpoint (2)
bb11: _0 = &(*_10);

Verification.

Entry. The preconditions ValidNum(N, "[1,)") (N != 0) and ValidNum(len(self) % N == 0), plus the &[T] slice invariant.

VM execution.

Property check.

• (1) exact_div's non-zero divisor: discharged by N != 0.
• (2) from_raw_parts's ValidPtr/InBound/ValidNum: len % N == 0 gives len = new_len * N, so the byte size size_of([T; N]) * new_len equals the slice's own size. NonNull/Align/Init/Allocated are inherited from the slice invariant, while ValidPtr/ValidNum/Alive/Alias follow from the slice's full validity established at entry. The cast re-interprets T as [T; N], layout-identical by construction.

10.1.3.5 as_chunks_unchecked_mut

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
#[cfg_attr(rapx, rapx::requires(ValidNum(N, "[1,)")))]
#[cfg_attr(rapx, rapx::requires(ValidNum(len(self) % N == 0)))]
pub const unsafe fn as_chunks_unchecked_mut<const N: usize>(&mut self) -> &mut [[T; N]] {
    assert_unsafe_precondition!(
        check_language_ub,
        "slice::as_chunks_unchecked requires `N != 0` and the slice to split exactly into `N`-element chunks",
        (n: usize = N, len: usize = self.len()) => n != 0 && len.is_multiple_of(n)
    );
    let new_len = unsafe { exact_div(self.len(), N) };
    unsafe { from_raw_parts_mut(self.as_mut_ptr().cast(), new_len) }
}
}

Verification Targets. Same two callsites as as_chunks_unchecked — exact_div(self.len(), N) and from_raw_parts_mut(self.as_mut_ptr().cast(), new_len) (the _mut variant of the from_raw_parts contract, adding Alias).

Path. … → bb7 → bb8 → bb9 → bb10 (exact_div in bb7, from_raw_parts_mut in bb10).

MIR. The statements on that path:

bb6:  _9 = len(&(*_1));
bb7:  _8 = exact_div(move _9, const N);                  // ← checkpoint (1)
bb8:  _14 = as_mut_ptr(&mut (*_1));
bb9:  _13 = ptr.cast::<[T; N]>(move _14);
bb10: _12 = raw::from_raw_parts_mut(move _13, copy _8);  // ← checkpoint (2)
bb11: _0 = &mut (*_12);

Verification. Identical to as_chunks_unchecked: (1) exact_div's divisor discharged by N != 0; (2) from_raw_parts_mut's ValidPtr/InBound/ValidNum discharged by len % N == 0, and its Alias obligation discharged by the exclusive &mut self receiver.

10.1.3.6 split_at_unchecked

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
#[cfg_attr(rapx, rapx::requires(ValidNum(mid, [0,self.len()])))]
pub const unsafe fn split_at_unchecked(&self, mid: usize) -> (&[T], &[T]) {
    let len = self.len();
    let ptr = self.as_ptr();
    assert_unsafe_precondition!(
        check_library_ub,
        "slice::split_at_unchecked requires the index to be within the slice",
        (mid: usize = mid, len: usize = len) => mid <= len,
    );
    // SAFETY: Caller has to check that `0 <= mid <= self.len()`
    unsafe { (from_raw_parts(ptr, mid), from_raw_parts(ptr.add(mid), unchecked_sub(len, mid))) }
}
}

Verification Targets. Two from_raw_parts callsites, each carrying the full slice contract:

#![allow(unused)]
fn main() {
// core::slice::raw::from_raw_parts — required by both calls
#[rapx::requires(NonNull(data))]
#[rapx::requires(ValidPtr(data, T, len))]
#[rapx::requires(Init(data, T, len))]
#[rapx::requires(Alive(data, 'a))]
#[rapx::requires(Alias(data))]
#[rapx::requires(Align(data, T))]
#[rapx::requires(ValidNum(size_of(T) * len <= isize::MAX))]
}

Path. After the precondition_check guard, both callsites are reached on the normal path … → bb6 → bb7 → bb8 (left from_raw_parts in bb6, right one in bb8).

MIR. The statements on that path:

bb0: _3 = len(&(*_1));
bb1: _5 = as_ptr(&(*_1));
bb6: _13 = raw::from_raw_parts(copy _5, copy _2);        // ← checkpoint (1), left [0, mid)
bb7: _18 = ptr.add(copy _5, copy _2);                   // ptr.add(mid)
bb8: _21 = SubUnchecked(copy _3, copy _2);              // len - mid
     _17 = raw::from_raw_parts(move _18, move _21);     // ← checkpoint (2), right [mid, len)

Verification.

Entry. The precondition ValidNum(mid, [0,self.len()]) (0 <= mid <= len), plus the &[T] slice invariant.

VM execution. _5 = as_ptr(_1) carries the slice's provenance; _18 = ptr.add(_5, _2) is the mid pointer; _21 = len - mid the right length.

Property check.

• (1) from_raw_parts(ptr, mid): in bounds by mid <= len → Proved.
• (2) from_raw_parts(ptr.add(mid), len - mid): covers [mid, len), in bounds; SubUnchecked(len, mid) is safe by mid <= len → Proved.

mid == len yields an empty right slice with a one-past-the-end pointer, which is valid.

10.1.3.7 split_at_mut_unchecked

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
#[cfg_attr(rapx, rapx::requires(ValidNum(mid, [0,self.len()])))]
pub const unsafe fn split_at_mut_unchecked(&mut self, mid: usize) -> (&mut [T], &mut [T]) {
    let len = self.len();
    let ptr = self.as_mut_ptr();
    assert_unsafe_precondition!(
        check_library_ub,
        "slice::split_at_mut_unchecked requires the index to be within the slice",
        (mid: usize = mid, len: usize = len) => mid <= len,
    );
    unsafe {
        (
            from_raw_parts_mut(ptr, mid),
            from_raw_parts_mut(ptr.add(mid), unchecked_sub(len, mid)),
        )
    }
}
}

Verification Targets. Two from_raw_parts_mut callsites, each requiring the _mut variant of the from_raw_parts contract (adding Alias for exclusive access).

Path. … → bb6 → bb7 → bb8 (left from_raw_parts_mut in bb6, right one in bb8).

MIR. The statements on that path:

bb0: _3 = len(&(*_1));
bb1: _5 = as_mut_ptr(&mut (*_1));
bb6: _13 = raw::from_raw_parts_mut(copy _5, copy _2);      // ← checkpoint (1), left [0, mid)
bb7: _18 = ptr.add(copy _5, copy _2);                      // ptr.add(mid)
bb8: _21 = SubUnchecked(copy _3, copy _2);                 // len - mid
     _17 = raw::from_raw_parts_mut(move _18, move _21);    // ← checkpoint (2), right [mid, len)

Verification. Same as split_at_unchecked: the bounds are discharged by 0 <= mid <= len; the two halves [0, mid) and [mid, len) are disjoint, so their Alias obligations are discharged by that disjointness plus the exclusive receiver.

10.1.3.8 align_to

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::requires(ValidTransmute(T, U)))]
#[cfg_attr(rapx, rapx::verify)]
pub unsafe fn align_to<U>(&self) -> (&[T], &[U], &[T]) {
    if U::IS_ZST || T::IS_ZST {
        return (self, &[], &[]);
    }
    let ptr = self.as_ptr();
    let offset = unsafe { crate::ptr::align_offset(ptr, align_of::<U>()) };
    if offset > self.len() {
        (self, &[], &[])
    } else {
        let (left, rest) = self.split_at(offset);
        let (us_len, ts_len) = rest.align_to_offsets::<U>();
        unsafe {
            (
                left,
                from_raw_parts(rest.as_ptr() as *const U, us_len),
                from_raw_parts(rest.as_ptr().add(rest.len() - ts_len), ts_len),
            )
        }
    }
}
}

Verification Targets. On the non-ZST, non-empty path: align_offset (effect-modelled) and the two from_raw_parts(rest.as_ptr() as *const U, …) calls. The transmute obligation is expressed by the type-level precondition:

#![allow(unused)]
fn main() {
#[rapx::requires(ValidTransmute(T, U))]
}

Path. The ZST (bb2) and offset > len (bb8) branches return early with no unsafe checkpoint. The unsafe path is … → bb5 → bb9 → bb12 → bb13 → bb17.

MIR. The statements on the unsafe path:

bb5:  _17 = ptr.align_offset(copy _15, mem::align_of::<U>());   // offset
bb9:  _35 = split_at(&(*_1), copy _17);                          // (left, rest)
bb10: _40 = rest.align_to_offsets::<U>();                        // (us_len, ts_len)
bb12: _45 = move _46 as *const U;                                // rest.as_ptr() as *const U
      _44 = raw::from_raw_parts(move _45, copy _38);             // ← checkpoint (1), middle [U]
bb16: _51 = ptr.add(copy _52, copy _54);                         // rest.as_ptr().add(len - ts_len)
bb17: _50 = raw::from_raw_parts(move _51, copy _39);             // ← checkpoint (2), tail [T]

Verification.

Entry. ValidTransmute(T, U) plus the &[T] slice invariant.

Property check. align_offset yields a valid aligned split point; split_at(offset) and the two from_raw_parts keep the three slices contiguous and in bounds — discharged by the range analysis. The essential risk — that the middle bytes form a valid [U] — is delegated to the ValidTransmute(T, U) axiom; RAPx verifies everything around the transmute.

10.1.3.9 align_to_mut

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::requires(ValidTransmute(T, U)))]
#[cfg_attr(rapx, rapx::verify)]
pub unsafe fn align_to_mut<U>(&mut self) -> (&mut [T], &mut [U], &mut [T]) {
    if U::IS_ZST || T::IS_ZST {
        return (self, &mut [], &mut []);
    }
    let ptr = self.as_ptr();
    let offset = unsafe { crate::ptr::align_offset(ptr, align_of::<U>()) };
    if offset > self.len() {
        (self, &mut [], &mut [])
    } else {
        let (left, rest) = self.split_at_mut(offset);
        let (us_len, ts_len) = rest.align_to_offsets::<U>();
        let rest_len = rest.len();
        let mut_ptr = rest.as_mut_ptr();
        unsafe {
            (
                left,
                from_raw_parts_mut(mut_ptr as *mut U, us_len),
                from_raw_parts_mut(mut_ptr.add(rest_len - ts_len), ts_len),
            )
        }
    }
}
}

Verification Targets. Same transmute-based pattern as align_to: align_offset, and two from_raw_parts_mut(mut_ptr as *mut U, …) calls, with:

#![allow(unused)]
fn main() {
#[rapx::requires(ValidTransmute(T, U))]
}

Path. The unsafe path is … → bb5 → bb9 → bb13 → bb16 (mirroring align_to with _mut slices).

MIR. The statements on the unsafe path:

bb5:  _17 = ptr.align_offset(copy _15, mem::align_of::<U>());
bb9:  _35 = split_at_mut(&mut (*_1), copy _17);
bb10: _40 = rest.align_to_offsets::<U>();
bb12: _44 = rest.as_mut_ptr();
bb13: _49 = move _50 as *mut U;
      _48 = raw::from_raw_parts_mut(move _49, copy _38);   // ← checkpoint (1), middle [U]
bb15: _54 = ptr.add(copy _44, copy _56);                   // mut_ptr.add(rest_len - ts_len)
bb16: _53 = raw::from_raw_parts_mut(move _54, copy _39);   // ← checkpoint (2), tail [T]

Verification. The three returned &mut slices are mutually disjoint (proved by the pointer arithmetic) and their Alias obligations are discharged by that disjointness plus the exclusive receiver. The transmute itself is covered by ValidTransmute(T, U).

10.1.3.10 get_disjoint_unchecked_mut

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
#[cfg_attr(rapx, rapx::requires(InBound(self, indices)))]
#[cfg_attr(rapx, rapx::requires(NonOverlap(indices)))]
pub unsafe fn get_disjoint_unchecked_mut<I, const N: usize>(
    &mut self,
    indices: [I; N],
) -> [&mut I::Output; N]
where
    I: GetDisjointMutIndex + SliceIndex<Self>,
{
    let slice: *mut [T] = self;
    let mut arr: MaybeUninit<[&mut I::Output; N]> = MaybeUninit::uninit();
    let arr_ptr = arr.as_mut_ptr();
    unsafe {
        for i in 0..N {
            let idx = indices.get_unchecked(i).clone();
            arr_ptr.cast::<&mut I::Output>().add(i).write(&mut *slice.get_unchecked_mut(idx));
        }
        arr.assume_init()
    }
}
}

Verification Targets. Inside the for i in 0..N loop, three unsafe callsites per iteration:

(1) indices.get_unchecked(i) — the slice get_unchecked on [I; N], requiring InBound(indices, i);

(2) slice.get_unchecked_mut(idx) — SliceIndex::get_unchecked_mut:

#![allow(unused)]
fn main() {
#[rapx::requires(InBound(slice, self))]
}

(3) the raw-pointer dereference &mut * — a normal Ptr2Ref on the *mut I::Output returned by get_unchecked_mut (the value to be written into the MaybeUninit slot):

#![allow(unused)]
fn main() {
#[rapx::requires(Init(ptr, T, 1))]
#[rapx::requires(ValidPtr(ptr, T, 1))]
#[rapx::requires(Align(ptr, T))]
#[rapx::requires(Alias(ptr))]
}

Path. The loop body bb4 → … → bb14 → bb4 is an SCC, unrolled per iteration; the three callsites sit at bb7 (get_unchecked), bb12 (get_unchecked_mut), and bb13 (&mut * + write).

MIR. The loop-body statements on one iteration:

bb7:  _21 = get_unchecked(&_2 as &[I], copy _24);   // indices.get_unchecked(i)  ← checkpoint (1)
bb10: _27 = ptr.cast::<&mut I::Output>(copy _5);
      _26 = ptr.add(move _27, copy _29);           // arr_ptr.cast().add(i)
bb12: _32 = ptr.get_unchecked_mut::<I>(_33, _34);  // slice.get_unchecked_mut(idx)  ← checkpoint (2)
bb13: _31 = &mut (*_32);                           // &mut *  ← checkpoint (3)
      _25 = ptr.write(move _26, move _30);         // MaybeUninit::write
bb8:  _0 = MaybeUninit::assume_init(...);          // after all N iterations

Verification.

Entry. The preconditions InBound(self, indices) and NonOverlap(indices), plus the &mut [T] slice invariant.

Property check.

• (1) indices.get_unchecked(i): the loop index i is < N by construction → InBound discharged.
• (2) slice.get_unchecked_mut(idx): discharged by InBound(self, indices).
• (3) &mut *: Init/ValidPtr/Align inherited from the slice invariant; the Alias obligation is discharged by NonOverlap(indices) (no two returned references alias).

The MaybeUninit array is fully written before assume_init, so the initialization obligation is discharged by the loop covering all N slots.

10.1.3.11 first_chunk / first_chunk_mut

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
pub const fn first_chunk<const N: usize>(&self) -> Option<&[T; N]> {
    if self.len() < N {
        None
    } else {
        Some(unsafe { &*(self.as_ptr().cast_array()) })
    }
}

#[cfg_attr(rapx, rapx::verify)]
pub const fn first_chunk_mut<const N: usize>(&mut self) -> Option<&mut [T; N]> {
    if self.len() < N {
        None
    } else {
        Some(unsafe { &mut *(self.as_mut_ptr().cast_array()) })
    }
}
}

Verification Targets. The single callsite is the raw-pointer dereference &*(self.as_ptr().cast_array()) (and &mut * for _mut) — a Ptr2Ref on a [T; N] pointer:

#![allow(unused)]
fn main() {
// Ptr2Ref
#[rapx::requires(Init(ptr, [T; N], 1))]
#[rapx::requires(ValidPtr(ptr, [T; N], 1))]
#[rapx::requires(Align(ptr, [T; N]))]
#[rapx::requires(Alias(ptr))]
}

Path. The else branch bb0 → bb1 → bb3 → bb4 → bb5 (the len < N branch bb2 returns None with no checkpoint).

MIR. The statements on the else path:

bb3: _8 = as_ptr(&(*_1));                       // self.as_ptr()
bb4: _7 = ptr.cast_array::<N>(move _8);         // *const T -> *const [T; N]
bb5: _6 = &(*_7);   // &* — raw-pointer deref (Ptr2Ref checkpoint)
     _5 = &(*_6);   // safe reborrow
     _0 = Option::<&[T; N]>::Some(move _5);

Verification.

Entry. The &[T] / &mut [T] slice invariant.

VM execution. cast_array re-interprets the slice data pointer as *const [T; N]; the &* creates the reference.

Property check. The else branch carries the path condition len >= N, so the N-element array fits inside the slice — discharging Init/InBound. Align follows from the slice invariant ([T; N] has the same alignment as T). Alias is discharged by the shared/exclusive receiver. For N == 0 the empty array is returned, and dereferencing a dangling pointer to a zero-sized array is legal.

10.1.3.12 split_first_chunk / split_first_chunk_mut

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
pub const fn split_first_chunk<const N: usize>(&self) -> Option<(&[T; N], &[T])> {
    let Some((first, tail)) = self.split_at_checked(N) else { return None };
    Some((unsafe { &*(first.as_ptr().cast_array()) }, tail))
}

#[cfg_attr(rapx, rapx::verify)]
pub const fn split_first_chunk_mut<const N: usize>(
    &mut self,
) -> Option<(&mut [T; N], &mut [T])> {
    let Some((first, tail)) = self.split_at_mut_checked(N) else { return None };
    Some((unsafe { &mut *(first.as_mut_ptr().cast_array()) }, tail))
}
}

Verification Targets. The single callsite is the raw-pointer dereference &*(first.as_ptr().cast_array()) (and &mut * for _mut) — a Ptr2Ref on [T; N], same contract as first_chunk.

Path. The Some branch bb0 → bb1 → bb2 → bb4 → bb5 (the None branch bb3 returns with no checkpoint).

MIR. The statements on the Some path:

bb0: _5 = split_at_checked(&(*_1), const N);
bb1: switchInt(discriminant(_5)) -> [1: bb2, otherwise: bb3];
bb2: _3 = copy (((_5 as Some).0).0);   // first
     _4 = copy (((_5 as Some).0).1);   // tail
     _12 = as_ptr(&(*_3));             // first.as_ptr()
bb4: _11 = ptr.cast_array::<N>(move _12);
bb5: _10 = &(*_11);   // &* — raw-pointer deref (Ptr2Ref checkpoint)
     _9 = &(*_10);    // safe reborrow
     _8 = (move _9, move &(*_4));

Verification.

Entry. The slice invariant.

Property check. split_at_checked(N) returns Some only when N <= len, so first has exactly N elements and the deref is in bounds — Init/Align/Alias discharged as in first_chunk. The tail slice is returned as-is.

10.1.3.13 split_last_chunk / split_last_chunk_mut

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
pub const fn split_last_chunk<const N: usize>(&self) -> Option<(&[T], &[T; N])> {
    let Some(index) = self.len().checked_sub(N) else { return None };
    let (init, last) = self.split_at(index);
    Some((init, unsafe { &*(last.as_ptr().cast_array()) }))
}

#[cfg_attr(rapx, rapx::verify)]
pub const fn split_last_chunk_mut<const N: usize>(
    &mut self,
) -> Option<(&mut [T], &mut [T; N])> {
    let Some(index) = self.len().checked_sub(N) else { return None };
    let (init, last) = self.split_at_mut(index);
    Some((init, unsafe { &mut *(last.as_mut_ptr().cast_array()) }))
}
}

Verification Targets. The single callsite is the raw-pointer dereference &*(last.as_ptr().cast_array()) (and &mut * for _mut) — a Ptr2Ref on [T; N].

Path. The Some branch bb0 → bb1 → bb2 → bb3 → bb5 → bb6 → bb7 (the None branch bb4 returns with no checkpoint).

MIR. The statements on the Some path:

bb0: _5 = len(&(*_1));
bb1: _4 = checked_sub(move _5, const N);
bb2: switchInt(discriminant(_4)) -> [1: bb3, otherwise: bb4];
bb3: _3 = copy ((_4 as Some).0);       // index = len - N
     _10 = split_at(&(*_1), copy _3);  // (init, last)
bb5: _8 = copy (_10.0);  _9 = copy (_10.1);
     _18 = as_ptr(&(*_9));             // last.as_ptr()
bb6: _17 = ptr.cast_array::<N>(move _18);
bb7: _16 = &(*_17);   // &* — raw-pointer deref (Ptr2Ref checkpoint)
     _15 = &(*_16);   // safe reborrow
     _0 = Some((move &(*_8), move _15));

Verification.

Entry. The slice invariant.

Property check. checked_sub(N) returning Some(index) establishes len >= N; split_at(index) (with index = len - N) then yields a trailing slice of exactly N elements, so the deref is in bounds — Init/Align/Alias discharged as in first_chunk.

10.1.3.14 last_chunk / last_chunk_mut

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
pub const fn last_chunk<const N: usize>(&self) -> Option<&[T; N]> {
    let Some(index) = self.len().checked_sub(N) else { return None };
    let (_, last) = self.split_at(index);
    Some(unsafe { &*(last.as_ptr().cast_array()) })
}

#[cfg_attr(rapx, rapx::verify)]
pub const fn last_chunk_mut<const N: usize>(&mut self) -> Option<&mut [T; N]> {
    let Some(index) = self.len().checked_sub(N) else { return None };
    let (_, last) = self.split_at_mut(index);
    Some(unsafe { &mut *(last.as_mut_ptr().cast_array()) })
}
}

Verification Targets. The single callsite is the raw-pointer dereference &*(last.as_ptr().cast_array()) (and &mut * for _mut) — a Ptr2Ref on [T; N].

Path. The Some branch bb0 → bb1 → bb2 → bb3 → bb5 → bb6 → bb7.

MIR. The statements on the Some path:

bb3: _3 = copy ((_4 as Some).0);       // index = len - N
     _9 = split_at(&(*_1), copy _3);
bb5: _8 = copy (_9.1);                  // last
     _15 = as_ptr(&(*_8));
bb6: _14 = ptr.cast_array::<N>(move _15);
bb7: _13 = &(*_14);   // &* — raw-pointer deref (Ptr2Ref checkpoint)
     _12 = &(*_13);   // safe reborrow

Verification. Same as split_last_chunk, but only the trailing chunk is returned. checked_sub(N) establishes len >= N, so the N-element deref is in bounds.

10.1.3.15 reverse

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
pub const fn reverse(&mut self) {
    let half_len = self.len() / 2;
    let Range { start, end } = self.as_mut_ptr_range();

    let (front_half, back_half) =
        unsafe {
            (
                slice::from_raw_parts_mut(start, half_len),
                slice::from_raw_parts_mut(end.sub(half_len), half_len),
            )
        };

    revswap(front_half, back_half, half_len);

    #[inline]
    const fn revswap<T>(a: &mut [T], b: &mut [T], n: usize) {
        let (a, _) = a.split_at_mut(n);
        let (b, _) = b.split_at_mut(n);
        let mut i = 0;
        #[safety::loop_invariant(i <= n)]
        while i < n {
            mem::swap(&mut a[i], &mut b[n - 1 - i]);
            i += 1;
        }
    }
}
}

Verification Targets. Two callsites:

(1) the two from_raw_parts_mut(start, half_len) / from_raw_parts_mut(end.sub(half_len), half_len) calls (the _mut from_raw_parts contract with Alias);

(2) inside revswap, the mem::swap(&mut a[i], &mut b[n - 1 - i]) calls (the ptr::swap contract).

Path. bb0 → bb1 → bb2 → bb3 → bb4 → bb5 → bb6 (the two from_raw_parts_mut at bb3/bb5, then the revswap call at bb6); inside revswap the mem::swap loop is an SCC unrolled per iteration.

MIR. The statements on that path:

bb2: _2 = Div(len(&(*_1)), const 2);        // half_len
     _8 = as_mut_ptr_range(&mut (*_1));     // (start, end)
bb3: _6 = copy (_8.0);  _7 = copy (_8.1);   // start, end
     _13 = from_raw_parts_mut(copy _6, copy _2);   // front_half  ← checkpoint (1)
bb4: _17 = ptr.sub(copy _7, copy _2);       // end.sub(half_len)
bb5: _16 = from_raw_parts_mut(move _17, copy _2);  // back_half   ← checkpoint (1)
bb6: _21 = revswap(&mut (*_10), &mut (*_11), copy _2);   // revswap → mem::swap loop

Verification.

Entry. The &mut [T] slice invariant (including exclusive access).

Property check. With half_len = len / 2, the front half [0, half_len) and back half [len - half_len, len) are disjoint and in bounds (len - half_len >= half_len), discharging ValidPtr/InBound/Alias for both from_raw_parts_mut calls. In revswap, the loop invariant i <= n proves a[i] and b[n - 1 - i] stay in bounds, and the disjoint halves guarantee mem::swap never aliases.

10.1.3.16 as_chunks / as_chunks_mut

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
pub const fn as_chunks<const N: usize>(&self) -> (&[[T; N]], &[T]) {
    assert!(N != 0, "chunk size must be non-zero");
    let len_rounded_down = self.len() / N * N;
    let (multiple_of_n, remainder) = unsafe { self.split_at_unchecked(len_rounded_down) };
    let array_slice = unsafe { multiple_of_n.as_chunks_unchecked() };
    (array_slice, remainder)
}

#[cfg_attr(rapx, rapx::verify)]
pub const fn as_chunks_mut<const N: usize>(&mut self) -> (&mut [[T; N]], &mut [T]) {
    assert!(N != 0, "chunk size must be non-zero");
    let len_rounded_down = self.len() / N * N;
    let (multiple_of_n, remainder) = unsafe { self.split_at_mut_unchecked(len_rounded_down) };
    let array_slice = unsafe { multiple_of_n.as_chunks_unchecked_mut() };
    (array_slice, remainder)
}
}

Verification Targets. Two chained callsites: split_at_unchecked(len_rounded_down) (contract ValidNum(mid, [0, self.len()])) and as_chunks_unchecked() (contract ValidNum(N, "[1,)") + ValidNum(len % N == 0)).

Path. bb0 → bb3 → bb4 → bb5 → bb6 → bb7 (the assert! branch bb1/bb2 panics); split_at_unchecked at bb6, as_chunks_unchecked at bb7.

MIR. The statements on that path:

bb3: _12 = len(&(*_1));
bb4: _11 = Div(move _12, const N);        // len / N
bb5: _10 = MulWithOverflow(copy _11, const N);   // * N  (= len_rounded_down)
bb6: _18 = split_at_unchecked(&(*_1), copy _10); // ← checkpoint (1)
bb7: _21 = as_chunks_unchecked(&(*_16));         // ← checkpoint (2)

Verification.

Entry. The slice invariant.

Property check. assert!(N != 0) provides the path condition N != 0. len_rounded_down = len / N * N is <= len (discharging split_at_unchecked's mid <= len) and a multiple of N (discharging as_chunks_unchecked's len % N == 0). Both internal unsafe calls are thus covered by facts established in the body.

10.1.3.17 as_rchunks

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
pub const fn as_rchunks<const N: usize>(&self) -> (&[T], &[[T; N]]) {
    assert!(N != 0, "chunk size must be non-zero");
    let len = self.len() / N;
    let (remainder, multiple_of_n) = self.split_at(self.len() - len * N);
    let array_slice = unsafe { multiple_of_n.as_chunks_unchecked() };
    (remainder, array_slice)
}
}

Verification Targets. A single callsite as_chunks_unchecked() (contract ValidNum(N, "[1,)") + ValidNum(len % N == 0)), reached after a safe split_at.

Path. bb0 → bb3 → bb4 → bb5 → bb8 → bb9 (the assert! branch bb1/bb2 panics); split_at at bb8, as_chunks_unchecked at bb9.

MIR. The statements on that path:

bb3: _11 = len(&(*_1));
bb5: _10 = Div(move _11, const N);                 // len / N
bb8: _18 = SubWithOverflow(copy _11, copy _10 * N); // self.len() - len * N
     _16 = split_at(&(*_1), move _18);
bb9: _25 = as_chunks_unchecked(&(*_15));           // ← checkpoint

Verification.

Entry. The &[T] slice invariant.

Property check. assert!(N != 0) provides N != 0. self.len() - len * N is the remainder len % N, so the right slice multiple_of_n has a length that is a multiple of N, discharging as_chunks_unchecked's len % N == 0. The left remainder has length < N by construction.

10.1.3.18 split_at_checked / split_at_mut_checked

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
pub const fn split_at_checked(&self, mid: usize) -> Option<(&[T], &[T])> {
    if mid <= self.len() {
        Some(unsafe { self.split_at_unchecked(mid) })
    } else {
        None
    }
}

#[cfg_attr(rapx, rapx::verify)]
pub const fn split_at_mut_checked(&mut self, mid: usize) -> Option<(&mut [T], &mut [T])> {
    if mid <= self.len() {
        Some(unsafe { self.split_at_mut_unchecked(mid) })
    } else {
        None
    }
}
}

Verification Targets. A single callsite split_at_unchecked(mid) / split_at_mut_unchecked(mid) (contract ValidNum(mid, [0, self.len()])), reached only on the mid <= len branch.

Path. bb0 → bb1 → bb2 → bb3 (the Some branch); the else branch bb4 returns None.

MIR. The statements on the Some path:

bb0: _5 = len(&(*_1));
bb1: _3 = Le(copy _2, move _5);
     switchInt(move _3) -> [0: bb4, otherwise: bb2];
bb2: _7 = split_at_unchecked(&(*_1), copy _2);   // ← checkpoint
bb3: _0 = Some(move _7);

Verification.

Entry. The slice invariant.

Property check. The branch condition mid <= self.len() (plus mid: usize >= 0) is exactly the 0 <= mid <= len precondition, so the Some branch is discharged directly; the else branch returns None.

10.1.3.19 binary_search_by

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
pub fn binary_search_by<'a, F>(&'a self, mut f: F) -> Result<usize, usize>
where
    F: FnMut(&'a T) -> Ordering,
{
    let mut size = self.len();
    if size == 0 {
        return Err(0);
    }
    let mut base = 0usize;

    while size > 1 {
        let half = size / 2;
        let mid = base + half;
        let cmp = f(unsafe { self.get_unchecked(mid) });
        base = hint::select_unpredictable(cmp == Greater, base, mid);
        size -= half;
    }

    let cmp = f(unsafe { self.get_unchecked(base) });
    if cmp == Equal {
        unsafe { hint::assert_unchecked(base < self.len()) };
        Ok(base)
    } else {
        let result = base + (cmp == Less) as usize;
        unsafe { hint::assert_unchecked(result <= self.len()) };
        Err(result)
    }
}
}

Verification Targets. self.get_unchecked(mid) (inside the loop) and self.get_unchecked(base) (epilogue), each carrying #[rapx::requires(InBound(slice, self))]; plus two hint::assert_unchecked hints.

Path. The loop body bb4 → … → bb12 → bb4 is an SCC, unrolled per iteration; get_unchecked(mid) at bb7, the epilogue get_unchecked(base) at bb13, and the two assert_unchecked at bb18/bb23.

MIR. The loop-body and epilogue statements:

bb7:  _25 = get_unchecked(&(*_1), copy _17);   // self.get_unchecked(mid)  ← checkpoint
bb8:  _21 = call_mut(_22, move _23);           // f(&self[mid])
bb13: _44 = get_unchecked(&(*_1), copy _46);   // self.get_unchecked(base)  ← checkpoint
bb18: _51 = assert_unchecked(move _52);        // base < len
bb23: _65 = assert_unchecked(move _66);        // result <= len

Verification.

Entry. The &[T] slice invariant.

Property check. The loop invariant is base + size == len (initially base = 0, size = len). Each iteration computes mid = base + half with half = size / 2, so mid < base + size == len, discharging get_unchecked(mid)'s InBound. After size -= half the invariant is restored, so the unrolled loop is inductive. On exit size <= 1, hence base < len, discharging the final get_unchecked(base). The two assert_unchecked bounds facts are verified independently.

10.1.3.20 partition_dedup_by

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
pub fn partition_dedup_by<F>(&mut self, mut same_bucket: F) -> (&mut [T], &mut [T])
where
    F: FnMut(&mut T, &mut T) -> bool,
{
    let len = self.len();
    if len <= 1 {
        return (self, &mut []);
    }

    let ptr = self.as_mut_ptr();
    let mut next_read: usize = 1;
    let mut next_write: usize = 1;

    unsafe {
        while next_read < len {
            let ptr_read = ptr.add(next_read);
            let prev_ptr_write = ptr.add(next_write - 1);
            if !same_bucket(&mut *ptr_read, &mut *prev_ptr_write) {
                if next_read != next_write {
                    let ptr_write = prev_ptr_write.add(1);
                    mem::swap(&mut *ptr_read, &mut *ptr_write);
                }
                next_write += 1;
            }
            next_read += 1;
        }
    }

    self.split_at_mut(next_write)
}
}

Verification Targets. Inside the while next_read < len loop, the raw-pointer dereferences &mut *ptr_read, &mut *prev_ptr_write, &mut *ptr_write (each requiring Init + ValidPtr + Align + Alias), and mem::swap.

Path. The loop body bb5 → … → bb20 → bb5 is an SCC, unrolled per iteration; the derefs are at bb9 (same_bucket's &mut *) and bb14 (mem::swap's &mut *).

MIR. The loop-body statements on one iteration:

bb5:  _20 = Lt(copy _16, copy _3);            // next_read < len
bb6:  _23 = ptr.add(copy _14, copy _16);      // ptr_read = ptr.add(next_read)
bb8:  _26 = ptr.add(copy _14, copy _28);      // prev_ptr_write = ptr.add(next_write - 1)
bb9:  _32 = call_mut(&mut _2, &mut *(_23), &mut *(_26));   // same_bucket(&mut *ptr_read, &mut *prev_ptr_write)
bb14: _45 = mem::swap(&mut *(_23), &mut *(_43));           // mem::swap(&mut *ptr_read, &mut *ptr_write)

Verification.

Entry. The &mut [T] slice invariant.

Property check. The loop invariant is 1 <= next_write <= next_read < len. This keeps next_read and next_write - 1 in bounds and guarantees next_read > next_write - 1, so ptr_read and prev_ptr_write never point to the same element. When next_read != next_write, ptr_read and ptr_write are distinct, so mem::swap does not alias. RAPx proves these index facts via loop-invariant range analysis.

10.1.3.21 rotate_left / rotate_right

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
pub const fn rotate_left(&mut self, mid: usize) {
    assert!(mid <= self.len());
    let k = self.len() - mid;
    let p = self.as_mut_ptr();
    unsafe {
        rotate::ptr_rotate(mid, p.add(mid), k);
    }
}

#[cfg_attr(rapx, rapx::verify)]
pub const fn rotate_right(&mut self, k: usize) {
    assert!(k <= self.len());
    let mid = self.len() - k;
    let p = self.as_mut_ptr();
    unsafe {
        rotate::ptr_rotate(mid, p.add(mid), k);
    }
}
}

Verification Targets. Two unsafe callsites:

(1) ptr.add(mid) — the element-strided add:

#![allow(unused)]
fn main() {
// core::ptr::mut_ptr::add
#[rapx::requires(InBound(self, T, count))]
}

(2) rotate::ptr_rotate(mid, p.add(mid), k) — the rotate helper:

#![allow(unused)]
fn main() {
// core::slice::rotate::ptr_rotate
#[rapx::requires(NonNull(mid))]
#[rapx::requires(Align(mid, T))]
#[rapx::requires(ValidPtr(mid, T, right))]
}

Path. bb0 → bb1 → bb2 → bb4 → bb5 → bb6 → bb7 (the assert! branch bb3 panics); ptr.add at bb6, ptr_rotate at bb7.

MIR. The statements on that path:

bb2: _10 = len(&(*_1));
bb4: _9 = SubWithOverflow(copy _10, copy _2);   // k = len - mid
bb5: _14 = as_mut_ptr(&mut (*_1));              // p
bb6: _18 = ptr.add(copy _14, copy _2);          // p.add(mid)  ← checkpoint (1)
bb7: _16 = ptr_rotate(move _17, move _18, move _21);   // ← checkpoint (2)

Verification.

Entry. The &mut [T] slice invariant.

Property check. assert!(mid <= self.len()) gives 0 <= mid <= len (resp. 0 <= k <= len), so k = len - mid >= 0. The two callsites split the range into halves:

• (1) ptr.add(mid) requires the left half [p, p.add(mid)) to be in bounds — discharged by mid <= len.
• (2) ptr_rotate's ValidPtr(mid, T, right) requires the right half [p.add(mid), p.add(mid) + right) = [p.add(mid), p.add(len)) to be valid for right = k = len - mid elements — discharged by the slice invariant and k = len - mid.

Together they span the whole [p, p + len) range that ptr_rotate operates over.

10.1.3.22 copy_from_slice

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
pub const fn copy_from_slice(&mut self, src: &[T])
where
    T: Copy,
{
    // SAFETY: `T` implements `Copy`.
    unsafe { copy_from_slice_impl(self, src) }
}
}

Verification Targets. A single callsite at the internal helper copy_from_slice_impl, which itself calls copy_nonoverlapping:

#![allow(unused)]
fn main() {
// core::ptr::copy_nonoverlapping
#[rapx::requires(Align(src, T))]
#[rapx::requires(Align(dst, T))]
#[rapx::requires(ValidPtr(src, T, count))]
#[rapx::requires(ValidPtr(dst, T, count))]
#[rapx::requires(NonOverlap(dst, src, T, count))]
#[rapx::requires(ValidNum(size_of(T) * count <= isize::MAX))]
}

Path. bb0 → bb1 → bb2 → bb6 → bb7 → bb8 → bb9 (the length-mismatch branch bb3/bb4/bb5 panics); copy_nonoverlapping at bb9.

MIR. The statements on that path:

bb6: _16 = as_ptr(&(*_2));                  // src.as_ptr()
bb7: _18 = as_mut_ptr(&mut (*_1));          // self.as_mut_ptr()
bb8: _20 = len(&(*_1));
bb9: _15 = ptr.copy_nonoverlapping(move _16, move _18, move _20);   // ← checkpoint

Verification.

Entry. The &mut [T] and &[T] slice invariants, plus the T: Copy bound.

Property check. copy_from_slice_impl first checks dest.len() != src.len() and panics on mismatch, then calls copy_nonoverlapping. The equal-length assertion plus the mutual exclusivity of &mut self and &src discharge ValidPtr / NonOverlap / ValidNum. The T: Copy bound justifies the bitwise copy.

10.1.3.23 copy_within

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
pub fn copy_within<R: RangeBounds<usize>>(&mut self, src: R, dest: usize)
where
    T: Copy,
{
    let Range { start: src_start, end: src_end } = slice::range(src, ..self.len());
    let count = src_end - src_start;
    assert!(dest <= self.len() - count, "dest is out of bounds");
    unsafe {
        let ptr = self.as_mut_ptr();
        let src_ptr = ptr.add(src_start);
        let dest_ptr = ptr.add(dest);
        ptr::copy(src_ptr, dest_ptr, count);
    }
}
}

Verification Targets. A single callsite ptr::copy(src_ptr, dest_ptr, count):

#![allow(unused)]
fn main() {
// core::ptr::copy
#[rapx::requires(ValidPtr(src, T, count))]
#[rapx::requires(Align(src, T))]
#[rapx::requires(ValidPtr(dst, T, count))]
#[rapx::requires(Align(dst, T))]
}

Path. bb0 → bb1 → bb2 → bb3 → bb4 → bb5 → bb6 → bb9 → bb10 → bb11 (the dest > len - count branch bb7/bb8 panics); ptr::copy at bb11.

MIR. The statements on that path:

bb2: _11 = SubWithOverflow(copy _5, copy _4);   // count = src_end - src_start
bb6: _29 = as_mut_ptr(&mut (*_1));              // ptr
bb9: _31 = ptr.add(copy _29, copy _4);          // src_ptr = ptr.add(src_start)
bb10: _34 = ptr.add(copy _29, copy _3);         // dest_ptr = ptr.add(dest)
bb11: _38 = move _31 as *const T;
      _37 = ptr::copy(move _38, move _34, move _41);   // ← checkpoint

Verification.

Entry. The &mut [T] slice invariant.

Property check. slice::range(src, ..self.len()) normalizes the source range and enforces src_start <= src_end <= len; assert!(dest <= len - count) enforces dest + count <= len. Both ranges therefore lie within [0, len). ptr::copy permits overlap (memmove), so no NonOverlap obligation arises — only the in-bounds facts, which are discharged.

10.1.3.24 swap_with_slice

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
pub const fn swap_with_slice(&mut self, other: &mut [T]) {
    assert!(self.len() == other.len(), "destination and source slices have different lengths");
    unsafe {
        ptr::swap_nonoverlapping(self.as_mut_ptr(), other.as_mut_ptr(), self.len());
    }
}
}

Verification Targets. A single callsite ptr::swap_nonoverlapping(self.as_mut_ptr(), other.as_mut_ptr(), self.len()):

#![allow(unused)]
fn main() {
// core::ptr::swap_nonoverlapping
#[rapx::requires(ValidPtr(x, T, count))]
#[rapx::requires(Align(x, T))]
#[rapx::requires(NonOverlap(x, y, T, count))]
}

Path. bb0 → bb1 → bb2 → bb3 → bb6 → bb7 → bb8 (the length-mismatch branch bb4/bb5 panics); swap_nonoverlapping at bb8.

MIR. The statements on that path:

bb3: _16 = as_mut_ptr(&mut (*_1));          // self.as_mut_ptr()
bb6: _18 = as_mut_ptr(&mut (*_2));          // other.as_mut_ptr()
bb7: _20 = len(&(*_1));
bb8: _15 = swap_nonoverlapping(move _16, move _18, move _20);   // ← checkpoint

Verification.

Entry. The two &mut [T] slice invariants.

Property check. assert!(self.len() == other.len()) establishes equal lengths. The two &mut [T] references are mutually exclusive by Rust's borrow rules, discharging swap_nonoverlapping's NonOverlap obligation.

10.1.3.25 as_simd / as_simd_mut

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
pub fn as_simd<const LANES: usize>(&self) -> (&[T], &[Simd<T, LANES>], &[T])
where
    Simd<T, LANES>: AsRef<[T; LANES]>,
    T: simd::SimdElement,
    simd::LaneCount<LANES>: simd::SupportedLaneCount,
{
    assert_eq!(size_of::<Simd<T, LANES>>(), size_of::<[T; LANES]>());
    unsafe { self.align_to() }
}

#[cfg_attr(rapx, rapx::verify)]
pub fn as_simd_mut<const LANES: usize>(&mut self) -> (&mut [T], &mut [Simd<T, LANES>], &mut [T])
where
    Simd<T, LANES>: AsMut<[T; LANES]>,
    T: simd::SimdElement,
    simd::LaneCount<LANES>: simd::SupportedLaneCount,
{
    assert_eq!(size_of::<Simd<T, LANES>>(), size_of::<[T; LANES]>());
    unsafe { self.align_to_mut() }
}
}

Verification Targets. A single callsite align_to() / align_to_mut() (whose transmute obligation is ValidTransmute(T, Simd<T, LANES>)).

Path. bb0 → bb1 → bb3 (the size-mismatch branch bb2 panics); align_to at bb1.

MIR. The statements on that path:

bb0: _11 = copy (*_8);  _12 = copy (*_9);       // size_of::<Simd<T, LANES>>(), size_of::<[T; LANES]>()
     _10 = Eq(move _11, move _12);
     switchInt(move _10) -> [0: bb2, otherwise: bb1];
bb1: _0 = align_to::<Simd<T, LANES>>(&(*_1));   // ← checkpoint (transmute)

Verification.

Entry. The slice invariant, plus the assert_eq!-established fact size_of::<Simd<T, LANES>>() == size_of::<[T; LANES]>().

Property check. The size assertion proves the SIMD vector type is layout-identical to [T; LANES], making the align_to transmute sound. All alignment, contiguity, and bounds properties are inherited from the align_to / align_to_mut verification.

10.1.3.26 get_disjoint_mut

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
pub fn get_disjoint_mut<I, const N: usize>(
    &mut self,
    indices: [I; N],
) -> Result<[&mut I::Output; N], GetDisjointMutError>
where
    I: GetDisjointMutIndex + SliceIndex<Self>,
{
    get_disjoint_check_valid(&indices, self.len())?;
    // SAFETY: The `get_disjoint_check_valid()` call checked that all indices
    // are disjunct and in bounds.
    unsafe { Ok(self.get_disjoint_unchecked_mut(indices)) }
}
}

Verification Targets. A single callsite get_disjoint_unchecked_mut(indices), whose two preconditions are InBound(self, indices) and NonOverlap(indices).

Path. bb0 → bb1 → bb2 → bb3 → bb5 → bb8 (the Err branch bb6/bb7 returns early); get_disjoint_unchecked_mut at bb5.

MIR. The statements on the Ok path:

bb1: _5 = get_disjoint_check_valid(&(*_2), len(&(*_1)));   // returns Result
bb3: switchInt(discriminant(_4)) -> [1: bb6, 0: bb5];
bb5: _15 = get_disjoint_unchecked_mut(&mut (*_1), move _17);   // ← checkpoint
bb8: _0 = Ok(move _15);

Verification.

Entry. The &mut [T] slice invariant.

Property check. get_disjoint_check_valid(...)? returning Ok establishes that all indices are in bounds and pairwise non-overlapping, discharging the InBound and NonOverlap preconditions of get_disjoint_unchecked_mut. RAPx connects the Ok result of the checker to the preconditions at the call site.

10.1.3.27 get_disjoint_check_valid

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
fn get_disjoint_check_valid<I: GetDisjointMutIndex, const N: usize>(
    indices: &[I; N],
    len: usize,
) -> Result<(), GetDisjointMutError> {
    for (i, idx) in indices.iter().enumerate() {
        if !idx.is_in_bounds(len) {
            return Err(GetDisjointMutError::IndexOutOfBounds);
        }
        for idx2 in &indices[..i] {
            if idx.is_overlapping(idx2) {
                return Err(GetDisjointMutError::OverlappingIndices);
            }
        }
    }
    Ok(())
}
}

Verification Targets. No unsafe callsites — this is a pure O(n²) validation loop over the indices (is_in_bounds and is_overlapping). It is annotated with #[rapx::verify] so RAPx treats it as the trusted precondition generator for get_disjoint_mut.

MIR. The nested-loop shape (outer next at bb4, is_in_bounds at bb7, inner next at bb14, is_overlapping at bb16):

bb4:  _12 = <Enumerate<Iter<I>>>::next(...);        // (i, idx)
bb7:  _20 = <I as GetDisjointMutIndex>::is_in_bounds(&idx, len);   // idx.is_in_bounds(len)
bb14: _33 = <Iter<I>>::next(...);                   // idx2 in indices[..i]
bb16: _39 = <I as GetDisjointMutIndex>::is_overlapping(&idx, &idx2);

Verification. The nested loops prove that an Ok return implies every index passed is_in_bounds and no pair is_overlapping — the facts that get_disjoint_mut then relies on.

10.1.3.28 as_flattened / as_flattened_mut

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
#[cfg_attr(rapx, rapx::requires(ValidTransmute([T; N], T)))]
pub const fn as_flattened(&self) -> &[T] {
    let len = if T::IS_ZST {
        self.len().checked_mul(N).expect("slice len overflow")
    } else {
        unsafe { self.len().unchecked_mul(N) }
    };
    unsafe { from_raw_parts(self.as_ptr().cast(), len) }
}

#[cfg_attr(rapx, rapx::verify)]
#[cfg_attr(rapx, rapx::requires(ValidTransmute([T; N], T)))]
pub const fn as_flattened_mut(&mut self) -> &mut [T] {
    let len = if T::IS_ZST {
        self.len().checked_mul(N).expect("slice len overflow")
    } else {
        unsafe { self.len().unchecked_mul(N) }
    };
    unsafe { from_raw_parts_mut(self.as_mut_ptr().cast(), len) }
}
}

Verification Targets. A single callsite from_raw_parts(self.as_ptr().cast(), len) (and from_raw_parts_mut for _mut), with the layout-identity axiom:

#![allow(unused)]
fn main() {
#[rapx::requires(ValidTransmute([T; N], T))]
}

Path. bb0 → … → bb8 → bb9 → bb10 (the ZST branch bb1/bb2/bb3/bb4 uses checked_mul; the non-ZST branch bb5/bb6/bb7 uses unchecked_mul); from_raw_parts at bb10.

MIR. The statements on the non-ZST path:

bb5: _9 = len(&(*_1));
bb6: _2 = unchecked_mul(move _9, const N);     // len = self.len() * N
bb8: _13 = as_ptr(&(*_1));
bb9: _12 = ptr.cast::<T>(move _13);            // self.as_ptr().cast()
bb10: _11 = raw::from_raw_parts(move _12, copy _2);   // ← checkpoint

Verification.

Entry. The slice invariant plus ValidTransmute([T; N], T).

Property check. The new length is len * N: for ZSTs checked_mul guards overflow; for non-ZSTs the multiplication cannot overflow because the slice is already in the address space. from_raw_parts requires len * N elements of T (i.e. len * size_of::<[T; N]>() bytes) in bounds, which follows from the slice's own validity. The cast re-interpretation is covered by the ValidTransmute([T; N], T) axiom.

10.1.4 Code Reference

• Source: safer-rust/rapx-verify-rust-std
• Challenge: #281 / 0017-slice

Chapter 10.2. Asterinas

Asterinas uses a pinned nightly toolchain. To apply RAPx, a few minor modifications are required (see an example here). Then, RAPx can be applied using the following command.

cd ostd
cargo rapx check -f -- --target x86_64-unknown-none