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 the nightly channel. 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 and PtsGraph

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 visit_times: usize,
    pub values: Vec<Value>,
    pub pts_graph: PtsGraph,
    pub move_sources: FxHashMap<usize, 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: Per-local value nodes (locals and their field projections), kept for SafeDrop compatibility and indexed so each Value maps to a PtsGraph slot. Each Value records the originating MIR local, a father link and a fields map for field projections, and a slot_idx into the PtsGraph. Drop properties and type classification now live on the PtsGraph slots rather than on Value.
• pts_graph: The unified points-to / value-flow graph (see below), shared by the MoP alias analysis and SafeDrop.
• move_sources: Maps a Move-operand destination to its source value index, so SafeDrop can propagate drop information through move chains.
• ret_alias: The accumulated alias results for the function (MOP version with drop metadata).

The alias state lives in a PtsGraph (a unified points-to and value-flow graph), which replaced the earlier flat alias_sets/block_facts representation:

#![allow(unused)]
fn main() {
pub struct PtsGraph {
    points_to: Vec<FxHashSet<AbstractLoc>>, // slot holds a pointer into another slot
    value_flow: Vec<FxHashSet<usize>>,      // slot's value is a copy of another slot
    slots: Vec<Slot>,                       // registered slots (local + field path)
    may_drop: Vec<bool>,
    need_drop: Vec<bool>,
    slot_kind: Vec<ValueKind>,              // RawPtr, Ref, Adt, ...
    alias_parent: Vec<usize>,               // union-find alias partition
    may_hold: FxHashSet<(usize, usize)>,    // call return may hold any of several args
}
}

• points_to: directed edges recording that a slot holds a pointer/reference into another slot (created by &_x, &raw _x).
• value_flow: directed edges recording that a slot's value is a copy of another slot (created by _a = _b, casts).
• alias_parent: a union-find partition capturing value-equivalence through assignments. may_alias combines this partition with points-to intersection.
• may_hold: a call whose return value may be any one of several arguments keeps those arguments apart via may_hold edges instead of merging them into one partition.

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.
2. init_pts_graph() builds the PtsGraph from the body via points_to::builder::from_body, pre-registering every local and its type-determined field slots (up to depth limits) with may_drop / need_drop / slot_kind.
3. PathGraph::find_scc() computes the SCC tree decomposition, reusing the same top-down traversal strategy for loops.
4. process_function_paths() walks each enumerated path via dfs_mop. For each block it calls:
   • alias_bb(): Processes intra-block assignments (process_assignment), updating the PtsGraph — points-to edges (&_x), value-flow / alias-partition moves (_a = _b), and field-level propagation.
   • alias_bbcall(): Handles call terminators — resolves the callee's alias summary and applies it (apply_callee_summary), or falls back to a conservative merge for unknown calls.
5. At each path end, merge_results_pts() extracts field-sensitive alias pairs among parameters and the return value via PtsGraph::fn_alias_pairs (with field truncation/compression) and stores them in ret_alias.

The path sensitivity is achieved by processing each PathGraph-enumerated path independently: dfs_mop saves and restores the PtsGraph between sibling paths, so every path is analyzed with a fresh alias state. 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/Slot projection: Each struct field access creates a field node. Slot::project() produces a field slot (local.fields), and Value::projection() recursively descends through ProjectionElem::Field, creating field nodes on demand (father/fields maps). ProjectionElem::Deref is skipped without materialising a new node, so multi-level pointer aliases are not tracked.
• Field-level propagation in PtsGraph::assign_value: when a slot's value is copied, the copy is propagated to the corresponding sub-field slots (every slot that extends the destination is linked to the matching slot that extends the source).
• Upward propagation in PtsGraph::merge_equivalence: when two slots are merged, propagate_to_father also unifies their parent slots one level up, so field-level aliases are visible through a base local.
• Slot registration bounds: points_to::builder pre-registers field slots up to MAX_FIELD_DEPTH = 5 and MAX_DEREF_DEPTH = 3; the total number of slots per path is bounded by MAX_VALUES_PER_PATH = 1000.
• Alias compression: after path traversal, fn_alias_pairs performs field truncation (compress_fields, 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.path_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 build the PtsGraph from the body (init_pts_graph).
2. Delegate to PathGraph::find_scc() for hierarchical SCC tree construction.
3. process_function_paths() walks each path via dfs_mop, calling alias_bb() and alias_bbcall() per block to update the PtsGraph, then merge_results_pts() 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"
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, PtsGraph, 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, pts_graph, move_sources).
• Value: Represents a program place node (a local and its field projections via father/fields), indexed into the PtsGraph by slot_idx.
• PtsGraph: The unified points-to / value-flow graph. Drop metadata (may_drop / need_drop) and type classification (slot_kind) live on its slots; alias partitions are a union-find structure.
• 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 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:

Primitive properties

Alias(p1[, p2])

Alias accepts one or two target places: the two-argument form Alias(p1, p2) declares that p1 and p2 alias each other; the one-argument form Alias(p) declares an aliasing hazard on p alone, used inside the Ptr2Ref / Drop compound definitions where the other aliasing place (the return reference, or a still-live owner) is implicit. A hazard by default: unproved Alias is reported as a [hazard] entry and contributes to UNSOUND. It is also the mechanism for a no-aliasing precondition — Ptr2Ref(p, T) (and Drop(p, T)) include Alias(p), and a caller declares #[rapx::requires(Ptr2Ref(p, T))] to discharge the callee's hazard. 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))]
#[rapx::requires(Alias(ptr))]
}

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. Four argument forms are accepted:

• Allocated(ptr, Ty, count, allocator) — ptr points to Ty * count memory allocated by the allocator.
• Allocated(ptr, Ty, count) — allocator defaults to global.
• Allocated(ptr, Ty) — count defaults to 1, allocator global.
• Allocated(ptr) — element type inferred from ptr's pointee, count = 1, allocator global.

psp II.2.

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

InBound(slice, index) / InBound(ptr[, Ty[, count]])

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

• InBound(slice, index) — index into a slice/array; index implements std::slice::SliceIndex (usize or a range type such as Range/RangeInclusive/RangeFrom/RangeTo/RangeFull), expanding to the correct bounds check.
• InBound(ptr, Ty, count) — count elements of Ty at ptr.
• InBound(ptr, Ty) — count defaults to 1.
• InBound(ptr) — element type inferred from ptr's pointee, count = 1.

psp II.3.

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

Init(ptr[, Ty[, count]])

Memory is initialized for count elements of Ty. Stronger than Typed: Init implies Typed but not vice versa. Ty and count may be omitted: a missing Ty is inferred from ptr's pointee, a missing count defaults to 1. psp III.4.

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

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(indices) / NonOverlap(a, b[, T[, count]])

With one argument, indices is an array [I; N]. NonOverlap(indices) requires every pair of its elements to be non-overlapping under I's indexing rules: usize indices must be distinct, while ranges must not overlap. The array length N comes from its type; this form has no T or count argument. It does not assert that the indices are in bounds. The current verifier parses this form but cannot yet prove it, so checks return UNKNOWN.

With two to four arguments, a and b are pointers to the starts of two memory ranges, each of length sizeof(T) * count bytes. These ranges must be disjoint. If T is omitted, RAPx infers it from the pointers' common pointee type and reports an error if their pointee types differ. If count is omitted, it defaults to 1. psp II.4.

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

NonVolatile(p[, T[, len]])

Memory is not volatile — no other thread writes to the region (p, sizeof(T) * len). T and len may be omitted: a missing T is inferred from p's pointee, a missing len defaults to 1. Assumed satisfied — the VM does not model volatile access. psp V.2.

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

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. Declared but not yet verified — the checker returns Unknown.

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

Owning(ptr[, T[, count]])

ownership(*p) == none — the pointer is the sole carrier of ownership; no live owner aliases the pointee. T and count may be omitted: a missing T is inferred from ptr's pointee, a missing count defaults to 1. psp IV.1.

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

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. Declared but not yet verified — the checker returns Unknown.

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

Size(T, c)

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

• 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).

#![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[, count]])

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. Ty and count may be omitted: a missing Ty is inferred from ptr's pointee (a MaybeUninit<T> pointee is trivially "typed"), a missing count defaults to 1. psp III.6.

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

Unreachable

The code path is unreachable. psp V.5. Declared but not yet verified — the checker returns Unknown.

#![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. Declared but not yet verified — the checker returns Unknown.

#![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.

• ValidNum(predicate) — a comparison expression with operators <, <=, >, >=, ==, !=.
• ValidNum(value, interval) — a value constrained to a range. The interval is an array literal [lo, hi] (inclusive both ends), a string "[lo, hi]" where [/] is inclusive and (/) is exclusive (either side may be left empty for an unbounded bound), or a bare integer n (shorthand for value == n).

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

ValidString(ptr, u8, len) / ValidString(iter)

The byte data is valid UTF-8. Two forms: psp III.2.

• ValidString(ptr, u8, len) — len bytes at ptr are valid UTF-8.
• ValidString(iter) — an Iterator<Item = u8>; the length is derived from the backing byte buffer.

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

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]))]
}

Compound properties

Deref(ptr[, Ty[, count]])

Allocated ∧ InBound — the pointer can be safely dereferenced. Ty and count may be omitted: a missing Ty is inferred from ptr's pointee, a missing count defaults to 1. primitive-sp §2.2.

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

Drop(ptr[, T])

ValidPtr(p, T) ∧ Alias(p) — dropping *ptr (e.g. ManuallyDrop::drop(&mut slot)): the pointee is a valid value, and the freed memory must not be used again. T may be omitted and is then inferred from ptr's pointee.

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

Layout(ptr, layout)

ValidNum(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))]
}

Ptr2Ref(ptr, T)

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

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

Ptr2RefUninit(ptr, T)

Typed(p, T) ∧ ValidPtr(p, T, 1) ∧ Align(p, T) ∧ Alias(p) — a raw pointer meets all requirements for sound &MaybeUninit<T> / &mut MaybeUninit<T> conversion (the content need not be initialized — Init is deliberately absent).

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

ValidPtr(ptr, Ty, count)

NonNull(ptr) ∧ (Size(Ty, 0) ∨ Deref(ptr, Ty, count)) — the pointer is non-null and dereferenceable (in-bounds within a live allocation). For a ZST the dereference requirement is vacuous, so non-nullness alone suffices; a null pointer is never valid. primitive-sp §2.2.

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

ValidTraitObj(ptr)

NonNull(ptr) — a pointer to an unsized value whose metadata is read (size_of_val, align_of_val, for_value_raw, min_align_of_val). Enforces non-null; the pointee's alignment/validity is not checked because the single-argument form carries no element type.

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

ZstAwareInBound(ptr, T, end_or_len) / ZstAwareInit(ptr, T, end_or_len)

InBound / Init with ZST-aware element counting: 0 elements when T is zero-sized, otherwise (end_or_len - ptr) / size_of(T) elements.

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

Send / Sync predicates

The following type-level predicates discharge Send/Sync marker-trait obligations. Send requires ContainNoType(Self, Rc, Ref, …) ∧ (NoRawPtr(Self) || TamedRawPtr(Self)); Sync requires RefSend(Self) ∧ ContainNoType(Self, Rc, Cell, UnsafeCell, …) (the composition is declared in std-trait-ensures.json).

ContainNoType(T, bad1, ...)

T does not structurally contain any of the listed types (one or more negative type names). Used to discharge Send/Sync obligations.

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

NoRawPtr(T)

The type T structurally contains no raw pointers — recursively through its fields, generic arguments, and nested types. Used to discharge Send obligations.

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

NoInternalMut(T)

The type T has no interior mutation through raw pointers.

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

UniInternalMut(T)

The type T has unique interior mutation (an exclusive owner, with no aliasing Clone).

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

AtomicUpdate(T)

The type T updates its raw pointers under synchronization or atomically.

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

RefSend(T)

&T: Send — the type can be shared across threads: every interior-mutability / raw-pointer field of T is guarded by a synchronization primitive (mutex/rwlock/atomic).

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

TamedRawPtr(T, ptr)

Allocated(ptr, T, 1) ∧ Owning(ptr) ∧ (NoInternalMut(T) || UniInternalMut(T) || AtomicUpdate(T)) — a raw-pointer field that is allocated and owning, and whose updates are read-only, exclusive, or atomic.

Note the argument order: TamedRawPtr is a type-level predicate, so the type T comes first (like NoRawPtr/RefSend); ptr names the struct's raw-pointer field and is normally not written by hand — inside a Send/Sync obligation it is auto-bound from the struct's #[rapx::invariant(Allocated(ptr))] / Owning(ptr), so the usual spelling is TamedRawPtr(Self).

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

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.53"

#![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). A trailing ? marks a parameter optional — omitted trailing optional parameters are dropped from the expanded inner calls, letting the target primitive apply its own default (e.g. an inferred element type, or count = 1), as in the bundled Deref(p: Ptr, T: Ty?, n: Expr?). 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_property("...")] 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 boolean combination of Tag(args) calls: || separates disjuncts, && joins conjuncts, and parentheses allow arbitrary nesting.

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). The turbofish forms size_of::<T>() / align_of::<T>() (optionally with a std::mem:: / core::mem:: path prefix) are also accepted; size_of(T) remains the preferred shorthand.

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()).
• .len() — query the receiver length (self.len()).

Only these projections and the equivalent length forms len(x) and x.len() are resolved. Both refer to the receiver’s len() method; for a local method whose result RAPx cannot derive, the predicate remains UNKNOWN. Getter-style method calls are not — write the field access instead: layout.size, not layout.size() (the field is size, so the .size form resolves and the .size() form does not).

Type-level constants — T::MAX, T::MIN, T::BITS (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) })
});
}

!self.is_empty() requires the local is_empty() method to return false (e.g. ValidNum(!self.is_empty())). RAPx uses the method result when available and does not assume that is_empty() is equivalent to len() == 0. Other receiver forms remain UNKNOWN if their method cannot be resolved.

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-compound-properties.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. Each attribute holds one property (optionally with kind = ...); repeat the attribute for multiple properties.
• #[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, and its precondition role is expressed through Ptr2Ref/Drop, which include Alias(p).

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 calls (self.len() or 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-api-requires.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 8.5. Verification Approach

The verifier discharges each safety property by symbolic reasoning over the VM state. This chapter first describes the symbolic VM state (§8.5.1), then the deduction rules that read that state (§8.5.2), and finally the special treatment of Alias, which is a hazard by default but also expresses a no-aliasing precondition (§8.5.3).

8.5.1 The Symbolic VM

VM design

The SymbolicVm (vm/mod.rs) is a semantic MIR executor: it executes the MIR items the backward slicer retained (§8.4.2) and directly builds a symbolic state (VmState) with a Z3 term for every value.

Execution proceeds top-to-bottom through the diagram below. run allocates an empty VmState; execute_items binds the parameters to fresh symbolic values, then walks the retained items in forward path order — each MIR statement or terminator is a transfer function that updates the state. At a checkpoint, the state contains the path conditions and memory effects modeled for the retained items. Unsupported operations and truncated inlining can leave a property unproved.

   ProofGoal { path, items: Vec<RelevantItem> }
   (produced by the backward slicer, §8.4.2)
                    │
                    ▼
   SymbolicVm::run(z3_ctx, tcx, goal)        ← stateless, pure input → state
                    │
                    ▼
   VmState::new(...)                      ← empty state (structure below)
                    │
                    ▼
   execute_items(&items)                  ← forward path order
                    │
                    ├─ init_parameters():  _1.._N ← fresh Z3 constants
                    │
                    └─ for item in items:
                          Statement    → exec_statement
                          Terminator   → exec_terminator
                          CalleeEntry  → handle_callee_entry  (save_frame)
                           CalleeExit   → handle_callee_exit   (restore_frame)
                           ContractFact → assert_contract_fact
                      ▼
   VmState ──► PropertyChecker::check ──► Z3 (assert_all + negation-as-failure)

The SymbolicVm takes the MIR of each path as input and maintains the following state during execution (besides the borrowed z3_ctx/tcx handles):

• Frame-scoped (current_frame: FrameState) — saved/restored on inline entry/exit, so a callee reuses MIR locals freely:

  • current_def_id — the function whose body is being executed.
  • local_alloc — the stack allocation backing each local's place. This is the only name → object binding: a local's whole value lives at path == [] and its field values at path == [i, ..] in the path-scoped MemoryContent::values (keyed by the local's allocation and declared type), so there is no local-keyed value table here.

• Path-scoped (everything else) — accumulates across the whole path, including inlined frames:

  • units — the object space: one MemoryUnit per allocation, each holding its allocation shape and its content (the per-byte byte_array plus the concrete byte_written offset set, the typed-value layer values, and the facts); whole values live at path == [] and field values at path == [i, ..].
  • constraints — accumulated solver assertions and the term term_caches.
  • caller_frames — saved caller frames for path-replay inlining.
  • inline — recursive-inline scratch: inline_depth, inline_truncated_terms, arg_referents, deferred_field_writes.
  • alias_hazard_allocs — the root allocations named by every Alias the caller's contract declares (a hazard like Alias(self, ret) or a Ptr2Ref precondition like Alias(self.0)); the alias checker discharges only these, see §8.5.3.

When the recursive inliner hits MAX_INLINE_DEPTH it no longer proceeds on an unconstrained value: the destination gets a distinguishable placeholder term recorded in inline_truncated_terms, and a property whose target value (or a checkpoint argument it reads, or a pointer provenance offset) depends on that term is reported Unknown (InlineDepthExceeded) rather than a spurious proof or failure.

The deduction rules in §8.5.2 read three things out of this state — values, allocations, and provenance — described in the subsections below.

Values and facts

A MIR local's whole value (its rvalue) and each of its field values are both symbolic values (VmValue), stored in MemoryContent::values keyed by (view_ty, path) within the local's allocation (each MemoryUnit is one allocation, so the AllocId is the unit index, not part of the key) — path == [] is the whole value, path == [i, ..] is field i (viewed as view_ty, so a reinterpret cast resolves to the right field view):

VmValue { z3_term, ty, provenance, facts, source }

• z3_term — a Z3 term. For pointer/reference types (&T, *const T, Box<T>, …) it is the address; for scalar types it is the value; for aggregate types it is the base address of the stack slot backing the aggregate.
• ty — the Rust type, for layout queries.
• provenance — Option<Provenance> (see below); None for a scalar.
• facts — the derived value facts (ValueFacts) that serve as the "fast-path flags" of §8.5.2:
  • non_null: bool, init: bool, in_bounds: bool.
  • align_n: Option<Int> — the pointer's alignment lower bound. Here Int is z3::ast::Int, a Z3 term, not a Rust integer: Some(n) asserts z3_term % n == 0, i.e. the pointer is at least n-aligned (alignments are powers of two, so "at least n" ⇔ "a multiple of n"). For a concrete type n is a constant term (Some(8)); for a generic type n is the symbolic constant align_T — a fresh Z3 constant shared per type — so a generic T is carried as a symbol, not a number. None records no alignment fact (e.g. a raw pointer *mut T), independent of whether T is generic.
• source — a ValueSource carrying any extra semantics beyond z3_term/type/provenance:
  • None — a plain value.
  • FieldOffset — a compile-time offset_of! field offset, propagated to a pointer's provenance when used as an add/byte_add offset.
  • Discriminant(Int) — a symbolic enum variant index (e.g. Iterator::next returns Some(x) iff !is_empty), tying switchInt branches to the real condition instead of a fresh symbol.
  • Comparison { lhs, rhs, op, cond } — a comparison result (Le/Lt/Ge/Gt/Eq/Ne): the operands plus the direct boolean condition (offset <= len), so switchInt/Assert emit a precise path condition instead of ite(cond, 1, 0) != 0.
  • BinaryOp { lhs, rhs, op } — a non-comparison binary-op result (Add/Sub/…/Div/Rem), used for guard inference (tracing a switch/assert guard back to the pointer it null-checks/alignment-checks) and division-axiom injection.

Allocation table

Every allocation a the VM tracks is one MemoryUnit (vm::state::MemoryUnit, stored at VmState::units[a]), split into its shape (allocation) and its contents (content). Its fields, grouped as in the code:

• Shape (always present):
  • base: Int — base address (a fresh Z3 constant).
  • size: Int — byte size (may be symbolic; an external parameter is sized as "unbounded").
  • align: Int — alignment in bytes (may be symbolic for a generic element type).
  • element_ty: ElementTy — the contents' type: Typed(T) for a concrete Ty (or u8 for a raw byte buffer), or Generic for a symbolic T.
  • kind: AllocKind — Object (a single Box<T>/struct/scalar/untyped buffer), Slice { len } (a slice/array buffer, with size == len · size_of(element_ty)), or External (an external raw-pointer parameter or a Vec/CString parameter's heap buffer, of unbounded size i64::MAX or a symbolic unknown size — nullability is tracked on the pointer term, not here).
• Lifecycle facts (allocation.facts: AllocFacts) — cross-cutting per-allocation lifecycle facts, kept apart from the shape metadata above:
  • dead: bool — freed (StorageDead/Drop).
  • liveness: Option<Region> — the region an external allocation is assumed alive for (Alive(p, 'a) contract / 'static); only consulted for external allocations, whose memory is caller-owned (so dead carries no guarantee). None = no assumption.
  • for_each: ForEachFacts — uniform facts about the container's pointer elements (x.iter() for_each invariants), anchored to the allocation so a pointer loaded from it resolves the fact via its provenance: target_ty (Typed), aligned_ty (Align), allocated: (Ty, n) (Allocated, n may be symbolic), owning (Owning).
• Content facts (content.facts: ContentFacts) — per-allocation content facts, kept next to the stored bytes/values rather than on the lifecycle layer:
  • initialized: bool — contents hold a readable value (Box::new/Vec/reference referent/callee return/write/ValidCStr/const data); false for new_uninit/uninit.
  • cstr_trusted: bool — a null-terminated byte buffer (valid C string).
  • utf8_trusted: bool — a valid UTF-8 buffer (ValidString).
  • split_transmute_to: Option<Ty> — the destination element type this allocation is licensed to be re-interpreted into by a SplitTransmute([T], [U]) contract (the slice's data buffer, reached through the slice value's provenance); None = no license.
• Relationships (optional):
  • parent: Option<AllocId> — the source allocation of a sub-view (s[i..j]/get/split_at/align_to/as_chunks/from_raw_parts); root_alloc follows this edge to group aliasing views.

The data allocation of a two-part value (Vec/String/CString) is not stored as an edge: it is re-derived on demand from the header's owning pointer field — the field whose provenance names the heap buffer, located generically by container_ptr_field (Box.0.pointer → [0, 0], Vec.buf.ptr.pointer → [0, 0, 0]). data_alloc_of reads that field's provenance; for a slice view whose header AllocId no longer carries a type key it falls back to header_data_alloc (scan the header's materialized fields for the single owning-pointer provenance). A &[T] reference needs neither — its provenance already names the data.

The entry differs by how the allocation was created:

Provenance

Every pointer value carries the allocation it points into, the byte offset within it, and (when known) the structure of that offset:

provenance(p) = { alloc_id: a, offset: off, offset_kind: k }   ⇔   p points into allocation a at byte offset off

offset_kind classifies the offset so the checker can use a cheaper, more precise proof: Field carries the "field in-bounds" guarantee (offset + size_of(field) <= size_of(container), e.g. Option::as_slice); Element(i) tracks the element index so InBound checks i + count <= slice_len linearly instead of the non-linear byte form (i+count)·S <= len·S (undecidable in Z3 NIA for a generic S); Byte marks a byte-strided (byte_add) or unclassifiable offset. offset_kind is None at the base (offset == 0).

A cast (&mut → *mut, *mut → *const) preserves provenance; a plain copy q = p copies provenance (so p and q are aliases).

Provenance recording rules

The VM maintains provenance in execution order, one transfer per MIR statement/terminator. Below, prov(p) = (a, off) abbreviates the full provenance(p) = { alloc_id: a, offset: off, offset_kind }, and slice_len denotes AllocKind::Slice { len } (read via Allocation::slice_len()):

── Allocation creation (Box::new / Vec::new / …) ──
a := fresh
──────────────────────────────────────────
prov(p) = (a, 0)      a.parent = ⊥         (a.kind = Slice { len } for a Vec/slice)

── View of a pointer (&*p / &mut *p / as_ptr / as_mut_ptr / into_raw) ──
prov(p) = (a, off)
────────────────────────
prov(&*p) = prov(p) = (a, off)          (the view inherits p's provenance)

── Slice view (from_raw_parts(ptr, n)) ──
prov(ptr) = (a, off)
────────────────────────────────────────
b := fresh   prov(s) = (b, 0)   b.kind = Slice { len: n }   b.parent = a

── Split (split_at(s, mid)) ──
prov(s) = (a, 0)   a.kind = Slice { len }   0 ≤ mid ≤ len
──────────────────────────────────────────────────────────────
prov(s[..mid]) = (b₁, 0)   b₁.kind = Slice { len: mid }      b₁.parent = a
prov(s[mid..]) = (b₂, 0)   b₂.kind = Slice { len: len−mid }   b₂.parent = a

── Element arithmetic (p.add(k)) ──
prov(p) = (a, off)
──────────────────────────────
prov(p.add(k)) = (a, off + k·S)      S = sizeof(element)

── Byte arithmetic (p.byte_add(k)) ──
prov(p) = (a, off)
──────────────────────────────
prov(p.byte_add(k)) = (a, off + k)

── Cast reinterprets a buffer (byte ↔ field) ──
A `*mut u8` ↔ `*mut T` cast switches the *view* of an allocation without
changing its bytes.  A *scalar* field round-trips across the two views
(little-endian, concrete size); a *pointer* field does not — provenance is not a
byte, so a byte→field read of a pointer field mints a fresh symbol:

  byte → field:  field(i).z3_term = Σⱼ byte[off(i) + j] · 256ʲ
  field → byte:  byte[off(i) + j]  = (field(i).z3_term ÷ 256ʲ) mod 256

where `off(i)` is field `i`'s byte offset and `256ʲ` is its byte-weight.

Alias rule

Two live reference views p and q alias when they name the same allocation, or sub-allocations of it:

prov(p) = (a, _)    prov(q) = (b, _)
root(a) == root(b)  where root(a) follows parent(a) to the top (⊥)

A view is live when its MIR local is between its StorageLive and StorageDead (and not moved). The parent chain is what makes a slice view (from_raw_parts) or a split_at half count as aliasing its source, even though each has a distinct AllocId — this is why root, not alloc_id alone, is the grouping key.

8.5.2 Deduction Rules

The proof of a property combines two kinds of rule. State-construction axioms describe how the symbolic VM builds the state — model invariants, not obligations. Property discharge rules prove each primitive from that state, through a fast path (a derived flag or layout fact, no solver) or an SMT query (the accumulated constraints plus the negation of the goal). Compound properties are macros over the primitives, and the fast-path flags shortcut the same rules without a query. Notation used throughout:

Notation:  S = sizeof_T,  A = align_T,  s : &[T],  len = s.len()

State-construction axioms

These hold by construction of the symbolic VM — each transfer function records how it updates VmState; none is a property the checker proves.

── Slice type invariant ──
NonNull(s) ∧ Align(s, T) ∧ ValidNum(len·S ≤ isize::MAX) ∧ Allocated(s, T, len) ∧ Init(s, T, len)

── Layout ──
──────────        ──────────        ──────────────────         ────────
S ≥ 0             A ≥ 1             S % A == 0                 len ≥ 0

For a *generic* `T` (no concrete layout), `S` and `A` are the shared symbolic
constants `sizeof_T` / `align_T`.  `size_of::<T>()` / `align_of::<T>()` on such a
`T` bind to these same symbols (not `0`/`1`), so they agree with allocation
sizes and pointer strides; `align_of::<T>() ≥ 1` keeps a cast like
`align as *const T` in `NonNull::dangling` non-null.

── Allocation (s : &[T]) ──
prov(s) = (a, 0)   a.kind = Slice { len }   a.size = len·S   a.align = A   a.initialized = true

── Pointer identity ──
prov(p) = (a, off)
─────────────────────
p.z3_term = a.base + off

── Pointer arithmetic ──
prov(p) = (a, off)                      prov(p) = (a, off)
──────────────────────────────          ──────────────────────────────
prov(p.add(k)) = (a, off + k·S)         (p.add(k)).z3_term = p.z3_term + k·S

── Alignment offset ──
prov(p) = (a, off)    S = sizeof(pointee)    A' = align_of::<U>()
────────────────────────────────────────────────────────────────────────────
align_offset(p, A') = k     (p.z3_term + k·S) % A' == 0      0 ≤ k < A'

`align_offset` is modelled as returning the offset in *elements* of the pointee
type (not bytes), so the aligned address is `p.z3_term + k·S`; a downstream
`p.add(k) as *const U` can then discharge `Align(p, U)`.  The bound `k < A'`
covers successful offsets, but `A' / S` is not their general upper bound:
the stride and requested alignment determine which offsets are reachable.
Rust returns `usize::MAX` when alignment cannot be reached. The current VM
always asserts a successful offset and does not model that failure result;
this can make a feasible path inconsistent and lead to a vacuous proof.

── Byte-range case split (generic S) ──
S = 0                                          S ≥ 1
──────────────────────                        ──────────────────────
x·S = y·S = 0   (byte range vacuous)           x·S ≤ y·S ⟺ x ≤ y

── Integer arithmetic ──
i < len
─────────────
i + 1 ≤ len

Memory-shape properties

Each rule proves one memory-shape primitive from the state built above. Fast paths use the derived flags and layout facts of §8.5.1; otherwise an SMT query asserts the constraints plus the negation of the goal.

── Align(p, T) ──
p.z3_term % align_of(T) == 0
────────────────────────────
Align(p, T)

Fast paths (no query): `align_of(T) == 1`; `align_n(p) ≥ align_of(T)` — compared structurally when both terms
are concrete powers of two, and by a linear SMT query when `align_of(T)` is a
symbolic `align_T` (for a generic `T`, `align_n` and `align_of(T)` are the *same*
shared `align_T` constant, so `align_T ≥ align_T` is trivially discharged);
`align_n` is only a *lower bound* on `p`'s alignment, so it discharges
`Align(p, T)` only when it is at least `align_of(T)`, never below; a
`for_each.aligned_ty(a) = U` fact with `align_of(U) ≥ align_of(T)`; a stack
borrow of a local whose type alignment is `≥ align_of(T)`; an allocation base
with `align(a) ≥ align_of(T)` and `off % align_of(T) == 0`.  Otherwise an SMT
modulo query under `p.z3_term = a.base + off` and `a.base % align(a) == 0`.
The current checker also accepts a concrete zero-sized type without checking
the pointer address. This shortcut is unsound for an aligned ZST, such as
`#[repr(align(8))] struct Z;`: a pointer to `Z` must still be 8-byte aligned.

── NonNull(p) ──
non_null(p)   ∨   in_bounds(p)   ∨   (prov(p) = (a, _) ∧ ¬external(a))   ∨   p.z3_term ≠ 0 (SMT)
─────────────────────────────────────────────────────────────────────────────────────────────────────
NonNull(p)

A tracked stack/heap allocation's base is never zero, so `¬external` implies
non-null; an *external* raw-pointer allocation carries no implied non-nullness
and is discharged only by a `#[rapx::invariant(NonNull(..))]`-derived
`non_null` flag or by proving `p.z3_term ≠ 0` from the path conditions.

── Allocated(p, T, n) ──
prov(p) = (a, off)    ¬dead(a)    off + n·S ≤ size(a)
──────────────────────────────────────────────────────
Allocated(p, T, n)

Vacuous when `n == 0` (any pointer is valid for its 0-byte prefix).  A type
compatibility fast path (element type matches `T`, `MaybeUninit<T>` ≡ `T`,
array/slice element, or a smart-pointer peel) discharges without the byte-range
query; an external "unbounded" allocation (sized `i64::MAX`) auto-passes; a
field-offset pointer checks against the *field's* size.

── InBound(p, T, n) ──
prov(p) = (a, off)    off = k·S (element stride)    a.kind = Slice { len }
────────────────────────────────────────────────────────────────────────────
InBound(p, T, n)  ⟺  k + n ≤ len

The slice form `InBound(s, i)` is the base case (`k = 0, n = 1`): `i < len` (for
a range index, `end ≤ len`).  Without an element-strided offset the check falls
back to the byte form `off + n·S ≤ size(a)` (case-split on `S` for a generic
element size).  Vacuous when `n == 0`; a ZST auto-passes; a field-offset pointer
checks against the field's own size.

── Init(p, T, n) ──
prov(p) = (a, off)    ∀ b ∈ [off, off + n·S) : initialized(a, b)
────────────────────────────────────────────────────────────────────
Init(p, T, n)

Vacuous when `n == 0`.  `Init(p, MaybeUninit<T>, n)` reduces to `Typed` —
`MaybeUninit<T>` carries no validity invariant, so there is nothing to
initialize.  Byte-level coverage is decided by the allocation's `initialized`
flag / per-byte `byte_array` (`byte[i] = select(array, i)`, unwritten offsets read the `UNINIT` sentinel); a byte never written is a confirmed violation.

── Owning(p) ──
prov(p) = (a, _)    ¬∃ live o ≠ dest : needs_drop(o) ∧ prov(o) = (a, _)
──────────────────────────────────────────────────────────────────────
Owning(p)

The check scans the *live* locals for a `needs_drop` owner whose buffer aliases
`a` (excluding the call's own destination and the reconstructed owner), which
would mean a second owner drops the same allocation.  The `for_each.owning` flag
(an `Owning(container.iter())` invariant declaring every element the sole owner
of its pointee) discharges `Owning` directly.

── Alive(p) ──
prov(p) = (a, _)    ¬dead(a)    (a is a tracked allocation, or p is a live reference/owner)
────────────────────────────
Alive(p)

── Alive (assumed for a region) ──
prov(p) = (a, _)    liveness(a) = Some('a)    ¬dead(a)    'a: 'r
───────────────────────────────────────────────────────────────────────
Alive(p, 'r)

`liveness` is only consulted for external raw-pointer allocations (whose memory
is owned by the caller, so `dead` carries no guarantee). `Some('static)` is
set by a `ValidCStr(p, n)` fact, an `Allocated` raw-pointer parameter, or
`'static` const/static data; `Some('a)` by an `Alive(p, 'a)`
contract/invariant. The assumption's region must cover the demanded region
(`'a: 'r`), resolved via rustc's `FreeRegionMap` (declared `where 'a: 'b` bounds
and their transitive closure) or — for a reference parameter `&'r Self<'a>` — by
the implied outlives of the type itself (`'a: 'r`); a wider demand than the
assumption fails.

── Typed(p, T) ──
prov(p) = (a, _)    element_ty(a) = T   (or a field of `T` at `off`; MaybeUninit is vacuously typed)
─────────────────────────────────────────────────────────────────────────────────────────────────
Typed(p, T)

── Typed (pointer container) ──
prov(p) = (a, _)    for_each.target_ty(a) = T
──────────────────────────────────────────────
Typed(p, T)

── Null (guarded branch of any(Null(p), …)) ──
p.z3_term = 0   (or p carries no non-null provenance)
───────────────────────────────────────────────────
Null(p)   (else the other disjunct decides)

── NonOverlap(p, q, n) ──
prov(p) = (a, _)    prov(q) = (b, _)    a ≠ b
─────────────────────────────────────────────
NonOverlap(p, q, n)
(else the byte ranges [p.z3_term, p.z3_term+n·S) and [q.z3_term, q.z3_term+n·S) are disjoint — an SMT query)

Two pointers with the same `alloc_id` fall through to the byte-range query.
The distinct-ID fast path above is an implementation limitation, not a sound
deduction for sub-views: `from_raw_parts` and split operations can give
overlapping views of one allocation different IDs with the same `root`. Their
ranges must be checked before `NonOverlap` can be proved; the current fast path
can otherwise incorrectly accept overlap.

Layout and type-level properties

── Size ──
size_of(T) = n                T: Sized ∧ size_of(T) > 0
──────────────────            ───────────────────────────
Size(T, n)                    Size(T, sized)

── NoPadding ──
T has no padding bytes (scalars/pointers/refs, arrays, tuples, and non-union structs, recursively)
────────────────────────────────────────────────────────────────────────────────────────────────────
NoPadding(T)

── ValidTransmute ──
size_of(src) = size_of(dst)     (a generic size — `0` — trusts the type system, since the call compiled)
──────────────────────────────────────────────────────────────────────────────────────────────────────
ValidTransmute(src, dst)

── SplitTransmute ──
split_transmute_to(receiver_alloc) = dst_elem
  ∨   src_elem = dst_elem   ∨   dst_elem is SIMD with a src lane   ∨   all-bit-patterns-valid(dst_elem)
──────────────────────────────────────────────────────────────────────────────────────────────────────
SplitTransmute([Src], [Dst])

The first disjunct is the caller-declared license: a `requires(SplitTransmute([T],
[U]))` contract records `U` on the slice's data allocation (via the slice value's
provenance), and the check discharges exactly that transmute — not every
transmute — when the receiver slice resolves to the same allocation.

── Trait ──
T: Copy    (or T: Sized; or T: <trait> appears among the caller's where-clauses)
──────────────────────────────────────────────────────────────────────────────────
Trait(T, Copy)

Numeric and byte-string properties

── ValidNum ──
∀ pred :  assert_all ∧ ¬cond(pred) is UNSAT    (with Euclidean-division/NIA axioms)
─────────────────────────────────────────────────────────────────────────────
ValidNum(...)

Each predicate (`index < len`, or the interval form desugared to `lo ≤ v ∧ v ≤ hi`)
is evaluated to a Z3 comparison; the negation is shown unsatisfiable under the path
constraints, with division axioms (`X = (X/N)·N + X%N`) injected to decide non-linear
inequalities.  A `size_of::<T>() · count ≤ isize::MAX`-shaped predicate (the slice
size invariant) is discharged by rule without a query.

── ValidString (UTF-8) ──
n = 0   ∨   the tracked bytes of prov(p)'s allocation form valid UTF-8
─────────────────────────────────────────────────────────────────────
ValidString(p, T, n)

── ValidCStr (nul-terminated) ──
cstr_trusted(a)   ∨   the bytes contain no interior NUL and end with a terminal NUL
─────────────────────────────────────────────────────────────────────────────────────
ValidCStr(p, n)

Compound properties

The compound safety properties are macros over the primitives (Deref reads "in-bounds within a live allocation"; ValidPtr is vacuous for a ZST, where non-nullness alone suffices):

Deref(p, T, n)      = Allocated(p, T, n) ∧ InBound(p, T, n)
ValidPtr(p, T, n)   = NonNull(p) ∧ (Size(T, 0) ∨ Deref(p, T, n))
Ptr2Ref(p, T)       = Init(p, T, 1) ∧ ValidPtr(p, T, 1) ∧ Align(p, T) ∧ Alias(p)
Ptr2RefUninit(p, T) = Typed(p, T) ∧ ValidPtr(p, T, 1) ∧ Align(p, T) ∧ Alias(p)
Drop(p, T)          = ValidPtr(p, T, 1) ∧ Alias(p)

Fast-path flags

The VM's derived value facts shortcut three primitives without an SMT query:

non_null(p)          in_bounds(p)          align_n(p) ≥ align_of(T)      (both powers of two)
────────────        ─────────────────      ────────────────────────────
NonNull(p)          InBound(p, T, 1)       Align(p, T)

non_null proves NonNull; in_bounds proves InBound(p, T, 1) (a single-element bound, established by a prior deref or contract); align_n is a lower bound on p's alignment, so it proves Align(p, T) only when it is at least align_of(T). The value's init flag is not a shortcut for Init(p, T, 1): Init concerns the pointee memory's initialized bytes (the allocation's initialized flag / per-byte byte_array), whereas init marks a value whose content is known initialized — it feeds the Typed fast paths and the MaybeUninit write exceptions, not the Init check.

These flags are sourced, not invented. A raw-pointer field (*mut T / *const T / NonNull<T>) carries no implicit non_null/init/align fact: those must be declared on the struct via #[rapx::invariant(NonNull(..))] / #[rapx::invariant(Init(..))] / #[rapx::invariant(Align(..))] (or discharged at the deref by a null guard). A deref of an unannotated raw field therefore fails NonNull/Init rather than silently assuming it. A concrete Align invariant is additionally recorded as the path condition p.z3_term % A == 0, so it survives pointer arithmetic (p.add(k)) that drops the value-level flag.

8.5.3 The Alias Hazard

Alias is a hazard by default — unproved Alias is reported as a [hazard] entry and contributes to UNSOUND — but it is also the property used to express a no-aliasing precondition: Ptr2Ref(p, T) (and Drop(p, T)) include Alias(p), and a caller discharges the hazard by declaring #[rapx::requires(Ptr2Ref(p, T))]. In both roles it asserts that a reference produced by a deref does not unsafely alias other live references. It applies to any deref that produces a reference (&*p / &mut *p / from_raw_parts, ...); a bare *p read or *p = ... write is Deref/ReadMemory, not Alias.

A caller-declared Alias is anchored to an allocation, not a whole-path flag. assert_contract_fact resolves each Alias source place — a hazard's Alias(self, ret) or a Ptr2Ref's Alias(self.0), following field projections — to the root allocation of the named parameter, and records it in VmState::alias_hazard_allocs. A call-site or escape check then discharges the hazard only when the produced view's origin resolves to one of those allocations, so a contract licensing Alias(self, ret) no longer licenses every other alias on the path.

The check runs five passes over the produced view:

── Alias (hazard) ──
  applies to any deref that produces a reference (&*p / &mut *p / from_raw_parts, ...);
  a bare *p read / *p = ... write is Deref/ReadMemory, not Alias.

  The alias check runs five passes over the produced view:

  1. resolve provenance — resolve_origin(p) → the allocation p points to, and
     its origin kind: &mut → MutRef, & → SharedRef, *const/*mut → RawPtr,
     Box/Vec/NonNull → Owned.

  2. collect the live alias set (flow-sensitive) — walk the VM's *current*
     locals: a live reference view aliases p when it names the same allocation
     (provenance), or a sub-allocation of it (`from_raw_parts` / `split_at`
     keep a `parent` edge back to the allocation they were split from).

  3. callsite check — the caller's contract must discharge the raw-pointer
     provenance's aliasing:
       an `Alias` declaration naming p's allocation (root(p) ∈ alias_hazard_allocs)
         → ✓ (Alias(p) is caller-guaranteed; its Init/NonNull/Allocated/Align parts
         are separate checks)
       otherwise, shared-XOR-mutable over the live alias set (step 2):
         &*p    requires no live &mut to *p   → else ✗
         &mut *p requires no live &    to *p   → else ✗
       a raw-pointer origin without a precondition → alias set unknown, defer.

  4. forward check — while the view is live, the *origin* raw pointer must not
     be accessed again; this is also what rejects a second `&mut *p` while the
     first `&mut` is still live:
       SharedView:  a raw write through the origin → ✗
       UniqueView:  any raw access through the origin → ✗

  5. escape — is the view returned?
     not returned → the borrow ends (steps 3–4 decide).
     returned → the escape hazard must be discharged:
       an `Alias(ptr, ret)` declaration naming the origin's allocation → ✓
         (the caller handles the aliasing)
       a shared view from an encapsulated raw field → ✓ (a per-function
         derivation forest resolves the nested field path, e.g. `self.node.ptr`
         → `[node, ptr]`, to the innermost raw field; a private field not
         written/exposed by safe code upholds the returned `&T`)
       a shared view re-borrowed from a reference parameter → ✓ only when the
         returned region does not outlive the parameter's region (`src: ret`,
         via rustc's outlives relation); returning a `&'b str` as `&'a str`
         with `'a: 'b` is rejected.
       otherwise → ✗

  ✓ = safe   ✗ = violation   Unknown = cannot prove safe (hazard not eliminated)

8.5.3.1 Precision

The alias analysis over-approximates several kinds of overlap:

• Sensitive: allocation identity (provenance alloc_id + parent chain), flow (the VM's current locals and StorageLive/StorageDead liveness), and — for the escape pass — the field path.
• Insensitive: byte offset/range. Two disjoint views of the same allocation (e.g. hand-written &*p and &mut *p.add(1)) may be treated as aliasing. Split operations give their halves separate AllocIds but preserve a common parent, so root-based alias checks can still group them.
• Path/context-insensitive: the forward scan uses CFG-reachable blocks (no path conditions), and the analysis is intra-procedural (cross-function aliasing is discharged by Alias/Ptr2Ref preconditions).

This abstraction can produce false positives on disjoint ranges and reference-parameter provenance. It does not by itself establish a no-missed-aliasing guarantee for the verifier: the NonOverlap distinct-ID shortcut described above can miss overlapping sub-views.

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

Check the unsafe operations in the 37 challenge-listed functions in library/core/src/slice/mod.rs 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

RAPx represents slice length and generic type T symbolically, without monomorphization. Its path analysis still enumerates finitely many paths and loop repetitions, subject to a path limit. A SOUND result in this chapter means that the obligations on those enumerated paths were discharged; it does not establish an inductive proof for every iteration of an arbitrary-length loop. The loop invariants mentioned below explain the source-level safety argument and are not assumptions or induction results supplied by RAPx.

10.1.2 Tool Integration

Like Kani (#[cfg_attr(kani, ...)]), RAPx annotations use cfg_attr so they only activate when the tool runs — register_tool is injected via RUSTFLAGS, never hard-coded in source:

#![allow(unused)]
fn main() {
// 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 from library/core (not the workspace root — core must be the primary package, not a dependency, for its annotations to be visible):

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

• --cfg=rapx activates the cfg_attr(rapx, ...) expansion.
• -Zcrate-attr=feature(register_tool) -Zcrate-attr=register_tool(rapx) registers rapx as a tool namespace.

A GitHub Actions workflow (.github/workflows/rapx.yml) runs the command on pushes and PRs. It currently installs the published RAPx crate version 0.7.56 through RAPX_VERSION, rather than pinning a Git commit or following RAPx main. Its pass condition only rejects lines containing result: UNSOUND; UNKNOWN results are allowed. The command is piped through tee without pipefail, so the workflow also does not reliably propagate a nonzero RAPx exit status. The individual SOUND traces below describe verifier output, not a guarantee enforced by this CI job.

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 — established by init_parameters at entry and re-proved at return:

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

Symbolic resolution. $self instantiates to the slice reference and $elem to the element type T. For a generic T, its size and alignment are unknown, so RAPx represents them symbolically as sizeof_T and align_T (sizeof_T ≥ 0 — T may be a ZST — and align_T ≥ 1, linked by the layout constraint sizeof_T % align_T == 0); the slice length is likewise symbolic, written len. The atoms therefore resolve to:

• NonNull($self) → self.term ≠ 0
• Align($self, $elem) → self.term % align_T == 0
• ValidNum(size_of($elem) * $self.len() <= isize::MAX) → len * sizeof_T ≤ isize::MAX
• Allocated($self, $elem, $self.len()) → Allocated(self, T, len)
• Init($self, $elem, $self.len()) → Init(self, T, len)

The following traces cite these symbolic forms directly. 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 also hold unconditionally: an empty slice (len == 0) has zero elements, so both are vacuous.

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.

Besides these, the &[T] receiver's slice type invariant 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 call's unwind edge to bb2 (resume, the panic path) is also part of the CFG, so RAPx's path graph enumerates it — but bb2 holds no unsafe checkpoint, so it adds no obligation. The &[T] invariant is re-proved only at the return block bb1 — a type invariant is a normal-return postcondition, so the panic-unwind path carries none.

MIR (compiled with nightly-2026-02-05; 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. Each local is a symbolic VmValue (term = address/value, prov = (alloc, offset), plus flags non_null/aligned/init); alloc(x) is the Allocation a local points into, holding base/size/align.

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)/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 (≥ 0, so T may be a ZST) rather than a monomorphized byte count, so the data allocation's byte size is len*sizeof_T; the element alignment is likewise a shared symbolic align_T (≥ 1), tied to the size by the layout constraint sizeof_T % align_T == 0. The slice length is materialized on the allocation as slice_len (mirroring the fat pointer's metadata word), with size = slice_len * sizeof_T, so len() reads it directly. The path, step by step:

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

          init_parameters:
            data_alloc.align = align_T, data_alloc.slice_len = len, data_alloc.size = len * sizeof_T, data_alloc.element_ty = T
            _1.term = data_alloc.base, _1.prov = (data_alloc, 0), _1.flags = { non_null, aligned, init, in_bounds }
               slice type invariant (JSON `[T]` entry):
                 NonNull(_1)           : _1.term ≠ 0
                 Align(_1, T)          : _1.term % align_T == 0
                 ValidNum(..)          : len * sizeof_T ≤ isize::MAX
                 Allocated(_1, T, len) : len·sizeof_T ≤ data_alloc.size
                 Init(_1, T, len)      : data_alloc.initialized = true   (whole slice data initialized)
               entry fact: len ≥ 0              (usize non-negativity)
            _2.term = param_2 (fresh symbolic)

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

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

_6 = &raw const (*_1)
          VM  _6.term = _1.term, _6.prov = _1.prov, _6.flags = { non_null, in_bounds }, _6.align_n = data_alloc.align = align_T

_4 = get_unchecked(move _5, move _6)                    [checkpoint (1)]
          check  InBound(_6, _5)   ←  SMT: assert entry `_2.term < len`; assert ¬(`_5.term < len`); `_5.term` ≡ `_2.term` ⇒ UNSAT    Proved
          VM  _4.term = _6.term + _5.term*sizeof_T, _4.prov = (data_alloc, _6.offset + _5.term*sizeof_T), _4.flags = { non_null, in_bounds }

_3 = &(*_4)                                             [checkpoint (2)]
          check  Init(_4, T, 1)      ←  data_alloc.initialized = true                                     Proved
          check  NonNull(_4)         ←  non_null ∈ _4.flags                                             Proved
          check  Allocated(_4, T, 1) ←  SMT: assert ¬(`(_5.term+1)*sizeof_T ≤ len*sizeof_T`)
                                            — case split on `sizeof_T`: ZST (`= 0`, both sides 0) and
                                              non-ZST (`≥ 1`, unsat by `_5.term < len`) ⇒ UNSAT    Proved
          check  InBound(_4, T, 1)   ←  in_bounds ∈ _4.flags, count == 1 (single-element fast-path)    Proved
          check  Align(_4, T)        ←  required align = align_T; real align_n = align_T ⇒ proved    Proved
          check  Alias(_4)           ←  (hazard) resolve_origin(_4) → _1 (&self, shared) ⇒ shared view safe    Proved
          VM  _3.term = _4.term, _3.prov = _4.prov, _3.flags = { non_null, aligned, init, in_bounds }

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

return                                                   [type-invariant]
          check  NonNull + Align + ValidNum + Allocated + Init  ←  _1 unchanged    Proved

result: SOUND

Formal reasoning rules. The deduction rules for discharging each property (Layout, Allocation, pointer arithmetic, slice bounds, fast-path flags, Ptr2Ref) are given in §8.5.

Alias hazard. Alias is a hazard by default, but it also expresses a no-aliasing precondition through Ptr2Ref/Drop. Its five-pass check — provenance resolution, the flow-sensitive alias set, shared-XOR-mutable, the forward check, and escape — is described in §8.5.

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) }
}
}

MIR. On the mutable receiver the shape is the same as get_unchecked (§10.1.3.1) — one InBound checkpoint at get_unchecked_mut, then the &mut * deref (Ptr2Ref checkpoint) — except the mutable reference reborrows into a longer chain: each &mut * is a distinct borrow edge through the opaque I::Output projection, and only the first is a checkpoint.

bb0: _7 = move _2;
     _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. Identical to get_unchecked, with two differences: the &mut [T] receiver, and the Alias hazard resolving to &mut self (exclusive) instead of &self (shared). Both checkpoints discharge the same way; the trailing _4/_3/_0 = &mut (*…) are safe reborrows.

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. Three unsafe callsites — the two ptr.add pointer-arithmetic calls and ptr::swap:

#![allow(unused)]
fn main() {
// core::ptr::mut_ptr::add
#[rapx::requires(InBound(self, T, count))]

// 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 three unsafe callsites are reached on the normal path bb0 → bb1 → bb2 → bb3 → bb5 → bb6 (ptr.add(a)) → bb7 (ptr.add(b)) → bb8 (ptr::swap).

MIR. The statements on that path:

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

Verification.

entry   _1 = self (&mut [T]), _2 = a (usize), _3 = b (usize)

          init_parameters:
            data_alloc.align = align_T, data_alloc.slice_len = len, data_alloc.size = len * sizeof_T, data_alloc.element_ty = T
            _1.term = data_alloc.base, _1.prov = (data_alloc, 0), _1.flags = { non_null, aligned, init, in_bounds }
               slice type invariant (JSON `[T]` entry):
                 NonNull(_1)           : _1.term ≠ 0
                 Align(_1, T)          : _1.term % align_T == 0
                 ValidNum(..)          : len * sizeof_T ≤ isize::MAX
                 Allocated(_1, T, len) : len·sizeof_T ≤ data_alloc.size
                 Init(_1, T, len)      : data_alloc.initialized = true

          caller contracts (asserted as facts):
            ValidNum(a, [0, len))   →  _2.term < len
            ValidNum(b, [0, len))   →  _3.term < len

_11 = as_mut_ptr(&mut (*_1))
          VM  _11.term = _1.term, _11.prov = _1.prov, _11.align_n = align_T

_14 = ptr.add(copy _11, _2)                                [checkpoint (1)]
          check  InBound(_11, T, _2)  ←  _2.term < len (caller `ValidNum(a, [0, len))`)    Proved
          VM  _14.term = _11.term + _2.term*sizeof_T, _14.prov = (data_alloc, _2.term*sizeof_T), _14.align_n = align_T

_17 = ptr.add(copy _11, _3)                                [checkpoint (2)]
          check  InBound(_11, T, _3)  ←  _3.term < len (caller `ValidNum(b, [0, len))`)    Proved
          VM  _17.term = _11.term + _3.term*sizeof_T, _17.prov = (data_alloc, _3.term*sizeof_T), _17.align_n = align_T

_13 = ptr::swap(move _14, move _17)                        [checkpoint (3)]
          check  ValidPtr(_14, T, 1)  ←  NonNull (flag) + Allocated/InBound by `_2.term < len`    Proved
          check  Align(_14, T)        ←  required align = align_T; real align_n = align_T ⇒ proved    Proved
          check  ValidPtr(_17, T, 1)  ←  NonNull (flag) + Allocated/InBound by `_3.term < len`    Proved
          check  Align(_17, T)        ←  required align = align_T; real align_n = align_T ⇒ proved    Proved

return                                                      [type-invariant]
          check  NonNull + Align + ValidNum + Allocated + Init  ←  _1 unchanged    Proved

result: SOUND

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(self.len() % 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   _1 = self (&[T])

          init_parameters:
            data_alloc.align = align_T, data_alloc.slice_len = len, data_alloc.size = len * sizeof_T, data_alloc.element_ty = T
            _1.term = data_alloc.base, _1.prov = (data_alloc, 0), _1.flags = { non_null, aligned, init, in_bounds }
               slice type invariant (JSON `[T]` entry):
                 NonNull(_1)           : _1.term ≠ 0
                 Align(_1, T)          : _1.term % align_T == 0
                 ValidNum(..)          : len * sizeof_T ≤ isize::MAX
                 Allocated(_1, T, len) : len·sizeof_T ≤ data_alloc.size
                 Init(_1, T, len)      : data_alloc.initialized = true

          caller contracts (asserted as facts):
            ValidNum(N, [1, ∞))           →  N ≠ 0
            ValidNum(len % N == 0)        →  len % N == 0

_8 = len(&(*_1))
          VM  _8.term = len

_7 = exact_div(move _8, const N)                          [checkpoint (1)]
          check  non-zero divisor      ←  N ≠ 0                                                     Proved
          VM  _7.term = len / N  (= new_len)

_12 = as_ptr(&(*_1))
          VM  _12.term = _1.term, _12.prov = _1.prov

_11 = ptr.cast::<[T; N]>(move _12)
          VM  re-interpret *const T as *const [T; N] (layout-identical)

_10 = raw::from_raw_parts(move _11, copy _7)              [checkpoint (2)]
          check  NonNull + Align + Init + Allocated   ←  inherited from the slice invariant            Proved
          check  ValidPtr + ValidNum + Alive + Alias  ←  slice's full validity at entry                 Proved
          check  InBound + ValidNum                   ←  len % N == 0 ⇒ len = new_len*N, so
                                                            new_len * size_of([T; N]) = len * sizeof_T  Proved
          VM  _10 = (&[T; N]) of new_len elements over data_alloc

_0 = &(*_10)
          VM  safe reborrow → return slot

return                                                      [type-invariant]
          check  NonNull + Align + ValidNum + Allocated + Init  ←  _1 unchanged    Proved

result: SOUND

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(self.len() % 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, on the mutable receiver:

entry   _1 = self (&mut [T])                                        [slice invariant]
          fact: N ≠ 0,  len % N == 0

_8 = exact_div(len, N)                            [checkpoint (1)]
          check  non-zero divisor      ←  N ≠ 0                                        Proved

_12 = from_raw_parts_mut(cast::<[T; N]>(as_mut_ptr(_1)), _8)   [checkpoint (2)]
          check  ValidPtr/InBound/ValidNum  ←  len % N == 0                            Proved
          check  Alias                     ←  exclusive &mut self receiver              Proved

return                                             [type-invariant]
          check  NonNull + Align + ValidNum + Allocated + Init  ←  _1 unchanged    Proved

result: SOUND

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. The ptr.add(mid) pointer-arithmetic call, then two from_raw_parts callsites:

#![allow(unused)]
fn main() {
// core::ptr::const_ptr::add
#[rapx::requires(InBound(self, T, count))]

// 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, the three callsites are reached on the normal path … → bb6 (left from_raw_parts) → bb7 (ptr.add) → bb8 (right from_raw_parts).

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)  ← checkpoint (2)
bb8: _21 = SubUnchecked(copy _3, copy _2);              // len - mid
     _17 = raw::from_raw_parts(move _18, move _21);     // ← checkpoint (3), right [mid, len)

Verification.

entry   _1 = self (&[T]), _2 = mid (usize)

          init_parameters:
            data_alloc.align = align_T, data_alloc.slice_len = len, data_alloc.size = len * sizeof_T, data_alloc.element_ty = T
            _1.term = data_alloc.base, _1.prov = (data_alloc, 0), _1.flags = { non_null, aligned, init, in_bounds }
               slice type invariant (JSON `[T]` entry):
                 NonNull(_1)           : _1.term ≠ 0
                 Align(_1, T)          : _1.term % align_T == 0
                 ValidNum(..)          : len * sizeof_T ≤ isize::MAX
                 Allocated(_1, T, len) : len·sizeof_T ≤ data_alloc.size
                 Init(_1, T, len)      : data_alloc.initialized = true

          caller contracts (asserted as facts):
            ValidNum(mid, [0, len])   →  0 ≤ _2.term ≤ len

_3 = len(&(*_1))
          VM  _3.term = len

_5 = as_ptr(&(*_1))
          VM  _5.term = _1.term, _5.prov = _1.prov

_13 = raw::from_raw_parts(copy _5, copy _2)               [checkpoint (1), left [0, mid)]
          check  NonNull + ValidPtr + Init + Alive + Alias + Align + ValidNum  ←  mid ≤ len ⇒ [0, mid) ⊆ [0, len)    Proved
          VM  _13 = (&[T]) of mid elements over data_alloc

_18 = ptr.add(copy _5, copy _2)                           [checkpoint (2)]
          check  InBound(_5, T, _2)  ←  _2.term ≤ len (caller `ValidNum(mid, [0, len])`)    Proved
          VM  _18.term = _5.term + _2.term*sizeof_T, _18.prov = (data_alloc, _2.term*sizeof_T)

_21 = SubUnchecked(copy _3, copy _2)
          VM  _21.term = len − mid

_17 = raw::from_raw_parts(move _18, move _21)             [checkpoint (3), right [mid, len)]
          check  NonNull + ValidPtr + Init + Alive + Alias + Align + ValidNum  ←  mid ≤ len ⇒ [mid, len) ⊆ [0, len)    Proved
          VM  _17 = (&[T]) of len−mid elements at data_alloc + mid*sizeof_T

return                                                      [type-invariant]
          check  NonNull + Align + ValidNum + Allocated + Init  ←  _1 unchanged    Proved

result: SOUND

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. The ptr.add(mid) pointer-arithmetic call, then two from_raw_parts_mut callsites, each requiring the _mut variant of the from_raw_parts contract (adding Alias for exclusive access).

Path. … → bb6 (left from_raw_parts_mut) → bb7 (ptr.add) → bb8 (right from_raw_parts_mut).

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)  ← checkpoint (2)
bb8: _21 = SubUnchecked(copy _3, copy _2);                 // len - mid
     _17 = raw::from_raw_parts_mut(move _18, move _21);    // ← checkpoint (3), right [mid, len)

Verification. Same as split_at_unchecked, on the mutable receiver:

entry   _1 = self (&mut [T]), _2 = mid (usize)            [slice invariant]
          fact: 0 ≤ _2.term ≤ len

_13 = from_raw_parts_mut(as_mut_ptr(_1), _2)               [checkpoint (1), left [0, mid)]
          check  NonNull + ValidPtr + Init + Alive + Alias + Align + ValidNum  ←  mid ≤ len    Proved

_18 = ptr.add(as_mut_ptr(_1), _2)                          [checkpoint (2)]
          check  InBound(_5, T, _2)  ←  _2.term ≤ len (caller `ValidNum(mid, [0, len])`)    Proved

_21 = SubUnchecked(len, _2)
_17 = from_raw_parts_mut(ptr.add(as_mut_ptr(_1), _2), _21) [checkpoint (3), right [mid, len)]
          check  NonNull + ValidPtr + Init + Alive + Alias + Align + ValidNum  ←  mid ≤ len    Proved
          check  Alias  ←  [0, mid) and [mid, len) disjoint + exclusive receiver                Proved

return                                                      [type-invariant]
          check  NonNull + Align + ValidNum + Allocated + Init  ←  _1 unchanged    Proved

result: SOUND

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, no contract obligations), the ptr.add pointer-arithmetic call, 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)  ← checkpoint (2)
bb17: _50 = raw::from_raw_parts(move _51, copy _39);             // ← checkpoint (3), tail [T]

Verification.

entry   _1 = self (&[T])                                        [slice invariant]
          fact: ValidTransmute(T, U)

_17 = ptr.align_offset(as_ptr(_1), align_of::<U>())
          VM  _17.term = offset (aligned split point)

_35 = split_at(&(*_1), _17)
          VM  _35 = (left, rest);  left = [0, offset), rest = [offset, len)

_40 = rest.align_to_offsets::<U>()
          VM  _40 = (us_len, ts_len)

_45 = rest.as_ptr() as *const U
_44 = raw::from_raw_parts(_45, _38)                              [checkpoint (1), middle [U]]
          check  NonNull + ValidPtr + Init + Alive + Alias + Align + ValidNum  ←  range analysis: middle in bounds    Proved

_51 = ptr.add(rest.as_ptr(), len − ts_len)                      [checkpoint (2)]
          check  InBound(rest.as_ptr(), T, len − ts_len)  ←  range analysis    Proved

_50 = raw::from_raw_parts(_51, _39)                              [checkpoint (3), tail [T]]
          check  NonNull + ValidPtr + Init + Alive + Alias + Align + ValidNum  ←  range analysis: tail in bounds      Proved

return                                                           [type-invariant]
          check  NonNull + Align + ValidNum + Allocated + Init  ←  _1 unchanged    Proved

result: SOUND

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 (effect-modelled), the ptr.add pointer-arithmetic call, 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)  ← checkpoint (2)
bb16: _53 = raw::from_raw_parts_mut(move _54, copy _39);   // ← checkpoint (3), tail [T]

Verification. Same as align_to, on the mutable receiver:

entry   _1 = self (&mut [T])                                   [slice invariant]
          fact: ValidTransmute(T, U)

_48 = from_raw_parts_mut(rest.as_mut_ptr() as *mut U, us_len)   [checkpoint (1), middle [U]]
          check  NonNull + ValidPtr + Init + Alive + Alias + Align + ValidNum  ←  range analysis      Proved

_54 = ptr.add(rest.as_mut_ptr(), rest_len − ts_len)             [checkpoint (2)]
          check  InBound(rest.as_mut_ptr(), T, rest_len − ts_len)  ←  range analysis    Proved

_53 = from_raw_parts_mut(rest.as_mut_ptr().add(rest_len − ts_len), ts_len)   [checkpoint (3), tail [T]]
          check  NonNull + ValidPtr + Init + Alive + Alias + Align + ValidNum  ←  range analysis      Proved
          check  Alias  ←  three &mut slices mutually disjoint + exclusive receiver                      Proved

return                                                           [type-invariant]
          check  NonNull + Align + ValidNum + Allocated + Init  ←  _1 unchanged    Proved

result: SOUND

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, four unsafe callsites per iteration:

(1) indices.get_unchecked(i) — the slice get_unchecked on [I; N], requiring InBound(indices, i);

(2) arr_ptr.cast().add(i) — the element-strided add over the MaybeUninit<[&mut I::Output; N]> slot array, requiring InBound(arr_ptr, &mut I::Output, i);

(3) slice.get_unchecked_mut(idx) — SliceIndex::get_unchecked_mut:

#![allow(unused)]
fn main() {
#[rapx::requires(InBound(slice, self))]
}

(4) 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 four callsites sit at bb7 (get_unchecked), bb10 (ptr.add), 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)  ← checkpoint (2)
bb12: _32 = ptr.get_unchecked_mut::<I>(_33, _34);  // slice.get_unchecked_mut(idx)  ← checkpoint (3)
bb13: _31 = &mut (*_32);                           // &mut *  ← checkpoint (4)
      _25 = ptr.write(move _26, move _30);         // MaybeUninit::write
bb8:  _0 = MaybeUninit::assume_init(...);          // after all N iterations

Verification.

entry   _1 = self (&mut [T]), _2 = indices ([I; N])              [slice invariant]
          fact: InBound(self, indices),  NonOverlap(indices)

# one loop iteration (unrolled):
_21 = indices.get_unchecked(i)                                   [checkpoint (1)]
          check  InBound(indices, i)  ←  loop index i < N                          Proved

_26 = ptr.add(arr_ptr.cast(), i)                                 [checkpoint (2)]
          check  InBound(arr_ptr.cast(), &mut I::Output, i)  ←  i < N              Proved

_32 = slice.get_unchecked_mut(idx)                               [checkpoint (3)]
          check  InBound(slice, idx)  ←  InBound(self, indices)                     Proved
          VM  _32 = element pointer (data_alloc, idx*sizeof_T)

_31 = &mut (*_32)                                                [checkpoint (4)]
          check  Init + ValidPtr + Align  ←  inherited from the slice invariant      Proved
          check  Alias                   ←  NonOverlap(indices): no two refs alias    Proved

_25 = ptr.write(arr_ptr.cast().add(i), _31)                      // MaybeUninit slot write

return                                                            [type-invariant]
          check  NonNull + Align + ValidNum + Allocated + Init  ←  _1 unchanged      Proved

result: SOUND

The source-level argument is that the loop writes all N slots before assume_init. The trace above checks the enumerated loop iterations; it does not independently prove full initialization for arbitrary N by induction.

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   _1 = self (&[T]) / (&mut [T])                           [slice invariant]

# else branch path condition: len ≥ N

_8 = as_ptr(&(*_1))
          VM  _8.term = _1.term, _8.prov = _1.prov

_7 = ptr.cast_array::<N>(move _8)
          VM  re-interpret *const T as *const [T; N] (layout-identical)

_6 = &(*_7)                                                     [Ptr2Ref checkpoint]
          check  Init + InBound    ←  len ≥ N ⇒ N-element array fits in the slice    Proved
          check  Align             ←  slice invariant ([T; N] aligns as T)           Proved
          check  Alias             ←  shared / exclusive receiver                    Proved
          VM  _6 = &[T; N] over data_alloc

_5 = &(*_6)
          VM  safe reborrow
_0 = Option::<&[T; N]>::Some(_5)

return                                                           [type-invariant]
          check  NonNull + Align + ValidNum + Allocated + Init  ←  _1 unchanged    Proved

result: SOUND

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   _1 = self (&[T]) / (&mut [T])                           [slice invariant]

_5 = split_at_checked(_1, N)
          VM  _5 = Some((first, tail))  iff  N ≤ len          // path condition N ≤ len

_3 = first, _4 = tail
_12 = as_ptr(&(*_3)); _11 = ptr.cast_array::<N>(_12)

_10 = &(*_11)                                                   [Ptr2Ref checkpoint]
          check  Init + Align + Alias  ←  as in first_chunk (N ≤ len)    Proved
          VM  _10 = &[T; N] over data_alloc

_8 = (reborrow(_10), &(*_4))                                     // tail returned as-is

return                                                           [type-invariant]
          check  NonNull + Align + ValidNum + Allocated + Init  ←  _1 unchanged    Proved

result: SOUND

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   _1 = self (&[T]) / (&mut [T])                           [slice invariant]

_4 = checked_sub(len, N)                                        // path condition: len ≥ N

_3 = index = len − N
_10 = split_at(_1, _3)                                          // (init, last); last has exactly N elements

_18 = as_ptr(&last); _17 = ptr.cast_array::<N>(_18)

_16 = &(*_17)                                                   [Ptr2Ref checkpoint]
          check  Init + Align + Alias  ←  as in first_chunk (last has N elements)    Proved
          VM  _16 = &[T; N] over data_alloc + (len−N)*sizeof_T

_0 = Some((&init, reborrow(_16)))

return                                                           [type-invariant]
          check  NonNull + Align + ValidNum + Allocated + Init  ←  _1 unchanged    Proved

result: SOUND

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:

entry   _1 = self (&[T]) / (&mut [T])                           [slice invariant]
          path condition: len ≥ N   (from checked_sub)

_13 = &(*cast_array::<N>(as_ptr(&last)))                        [Ptr2Ref checkpoint]
          check  Init + Align + Alias  ←  last has exactly N elements    Proved

return                                                           [type-invariant]
          check  NonNull + Align + ValidNum + Allocated + Init  ←  _1 unchanged    Proved

result: SOUND

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. Three callsites:

(1) end.sub(half_len) — the mut_ptr::sub pointer arithmetic:

#![allow(unused)]
fn main() {
// core::ptr::mut_ptr::sub
#[rapx::requires(InBound(self, T, count))]
}

(2) 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);

(3) 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)  ← checkpoint (2)
bb5: _16 = from_raw_parts_mut(move _17, copy _2);  // back_half   ← checkpoint (3)
bb6: _21 = revswap(&mut (*_10), &mut (*_11), copy _2);   // revswap → mem::swap loop

Verification.

entry   _1 = self (&mut [T])                                   [slice invariant]

_2 = Div(len, 2)                                               // half_len
_8 = as_mut_ptr_range(&mut (*_1))                              // (start, end)

_13 = from_raw_parts_mut(start, _2)                             [checkpoint (1), front_half]
          check  ValidPtr + InBound + Alias  ←  front [0, half_len) in bounds, disjoint    Proved

_17 = ptr.sub(end, _2)                                          [checkpoint (2)]
          check  InBound(end, T, half_len)  ←  len − half_len ≥ 0 (half_len ≤ len)    Proved

_16 = from_raw_parts_mut(_17, _2)                               [checkpoint (3), back_half]
          check  ValidPtr + InBound + Alias  ←  back [len−half_len, len) in bounds; len−half_len ≥ half_len ⇒ disjoint    Proved

_21 = revswap(front_half, back_half, half_len)
          # source-level invariant i ≤ n; RAPx checks enumerated iterations
          check  mem::swap(&mut a[i], &mut b[n−1−i])  ←  disjoint halves ⇒ no alias    Proved

return                                                           [type-invariant]
          check  NonNull + Align + ValidNum + Allocated + Init  ←  _1 unchanged    Proved

result: SOUND

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   _1 = self (&[T]) / (&mut [T])                           [slice invariant]
          path condition: N ≠ 0   (from assert!)

_10 = (len / N) * N                                            // len_rounded_down

_18 = split_at_unchecked(_1, _10)                               [checkpoint (1)]
          check  ValidNum(mid, [0, len])  ←  len_rounded_down = len/N*N ≤ len    Proved

_21 = as_chunks_unchecked(_16)                                  [checkpoint (2)]
          check  ValidNum(N, [1, ∞)) + ValidNum(len % N == 0)  ←  N ≠ 0; len_rounded_down multiple of N    Proved

return                                                           [type-invariant]
          check  NonNull + Align + ValidNum + Allocated + Init  ←  _1 unchanged    Proved

result: SOUND

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   _1 = self (&[T])                                       [slice invariant]
          path condition: N ≠ 0   (from assert!)

_18 = len − (len / N) * N                                      // = len % N (remainder)

_16 = split_at(_1, _18)                                        // (remainder, multiple_of_n)

_25 = as_chunks_unchecked(&multiple_of_n)                      [checkpoint]
          check  ValidNum(N, [1, ∞)) + ValidNum(len % N == 0)  ←  N ≠ 0; multiple_of_n length is a multiple of N    Proved

return                                                           [type-invariant]
          check  NonNull + Align + ValidNum + Allocated + Init  ←  _1 unchanged    Proved

result: SOUND

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   _1 = self (&[T]) / (&mut [T]), _2 = mid (usize)         [slice invariant]

_3 = Le(_2, len)                                                // branch condition: mid ≤ len

_7 = split_at_unchecked(_1, _2)                                 [checkpoint, Some branch only]
          check  ValidNum(mid, [0, len])  ←  mid ≤ len ∧ mid: usize ≥ 0    Proved

return                                                           [type-invariant]
          check  NonNull + Align + ValidNum + Allocated + Init  ←  _1 unchanged    Proved

result: SOUND

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   _1 = self (&[T])                                       [slice invariant]
          source-level invariant: base + size == len (not assumed by RAPx)

# loop iteration (unrolled):
_25 = self.get_unchecked(mid)                                   [checkpoint]
          check  InBound(slice, mid)  ←  mid = base + size/2 < base + size == len    Proved

# epilogue:
_44 = self.get_unchecked(base)                                  [checkpoint]
          check  InBound(slice, base)  ←  size ≤ 1 ⇒ base < len                      Proved

_51 = assert_unchecked(base < len)                              ←  base < len          Proved
_65 = assert_unchecked(result ≤ len)                            ←  verified independently   Proved

return                                                           [type-invariant]
          check  NonNull + Align + ValidNum + Allocated + Init  ←  _1 unchanged    Proved

result: SOUND

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 three ptr.add pointer-arithmetic calls (each requiring InBound(self, T, count)), 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)  ← checkpoint
bb8:  _26 = ptr.add(copy _14, copy _28);      // prev_ptr_write = ptr.add(next_write - 1)  ← checkpoint
bb9:  _32 = call_mut(&mut _2, &mut *(_23), &mut *(_26));   // same_bucket(&mut *ptr_read, &mut *prev_ptr_write)
bb13: _43 = ptr.add(copy _14, copy _28);      // ptr_write = prev_ptr_write.add(1)  ← checkpoint
bb14: _45 = mem::swap(&mut *(_23), &mut *(_43));           // mem::swap(&mut *ptr_read, &mut *ptr_write)

Verification.

entry   _1 = self (&mut [T])                                   [slice invariant]
          source-level relation: 1 ≤ next_write ≤ next_read < len (not assumed by RAPx)

# loop iteration (unrolled):
_23 = ptr.add(as_mut_ptr(_1), next_read)                       [checkpoint]  // ptr_read
          check  InBound(ptr, T, next_read)  ←  next_read < len    Proved

_26 = ptr.add(as_mut_ptr(_1), next_write − 1)                  [checkpoint]  // prev_ptr_write
          check  InBound(ptr, T, next_write − 1)  ←  next_write − 1 < len    Proved

_32 = same_bucket(&mut *_23, &mut *_26)                        [Ptr2Ref checkpoint]
          check  Init + ValidPtr + Align + Alias  ←  next_read, next_write−1 in bounds; next_read > next_write−1 ⇒ no alias    Proved

_43 = ptr.add(as_mut_ptr(_1), next_write)                      [checkpoint]  // ptr_write = prev_ptr_write.add(1)
          check  InBound(ptr, T, next_write)  ←  next_write < len    Proved

_45 = mem::swap(&mut *_23, &mut *_43)                          [Ptr2Ref checkpoint]
          check  Init + ValidPtr + Align + Alias  ←  in bounds; next_read ≠ next_write ⇒ ptr_read, ptr_write distinct    Proved

return                                                           [type-invariant]
          check  NonNull + Align + ValidNum + Allocated + Init  ←  _1 unchanged    Proved

result: SOUND

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   _1 = self (&mut [T]), _2 = mid (usize)                  [slice invariant]
          path condition: 0 ≤ mid ≤ len   (from assert!)

_9 = SubWithOverflow(len, _2)                                  // k = len − mid ≥ 0
_14 = as_mut_ptr(&mut (*_1))                                   // p

_18 = ptr.add(_14, _2)                                          [checkpoint (1)]
          check  InBound(p, T, mid)   ←  left half [p, p+mid) in bounds; mid ≤ len    Proved
          VM  _18 = (data_alloc, mid*sizeof_T)

_16 = ptr_rotate(mid, _18, _9)                                  [checkpoint (2)]
          check  NonNull + Align + ValidPtr(mid, T, k)  ←  right half [p+mid, p+len) valid; k = len − mid    Proved

return                                                           [type-invariant]
          check  NonNull + Align + ValidNum + Allocated + Init  ←  _1 unchanged    Proved

result: SOUND

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   _1 = self (&mut [T]), _2 = src (&[T])                    [slice invariants]
          path condition: dest.len() == src.len()   (from the mismatch panic)

_16 = as_ptr(&(*_2)); _18 = as_mut_ptr(&mut (*_1)); _20 = len

_15 = ptr.copy_nonoverlapping(_16, _18, _20)                    [checkpoint]
          check  ValidPtr(src, T, n) + ValidPtr(dst, T, n)  ←  equal lengths    Proved
          check  Align(src) + Align(dst)                    ←  slice invariant    Proved
          check  NonOverlap(dst, src, T, n)                 ←  &mut self and &src are exclusive    Proved
          check  ValidNum(n * sizeof_T ≤ isize::MAX)        ←  slice validity    Proved

return                                                           [type-invariant]
          check  NonNull + Align + ValidNum + Allocated + Init  ←  _1 unchanged    Proved

result: SOUND

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. The two ptr.add pointer-arithmetic calls (src_ptr = ptr.add(src_start), dest_ptr = ptr.add(dest)), then 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)  ← checkpoint (1)
bb10: _34 = ptr.add(copy _29, copy _3);         // dest_ptr = ptr.add(dest)  ← checkpoint (2)
bb11: _38 = move _31 as *const T;
      _37 = ptr::copy(move _38, move _34, move _41);   // ← checkpoint (3)

Verification.

entry   _1 = self (&mut [T])                                   [slice invariant]
          path conditions: src_start ≤ src_end ≤ len;  dest + count ≤ len

_11 = src_end − src_start                                      // count
_29 = as_mut_ptr(&mut (*_1))                                   // ptr
_31 = ptr.add(_29, src_start)                                  [checkpoint (1)]  // src_ptr
          check  InBound(ptr, T, src_start)  ←  src_start ≤ src_end ≤ len    Proved

_34 = ptr.add(_29, dest)                                       [checkpoint (2)]  // dest_ptr
          check  InBound(ptr, T, dest)  ←  dest + count ≤ len ⇒ dest ≤ len    Proved

_37 = ptr::copy(_31, _34, count)                               [checkpoint (3)]
          check  ValidPtr(src, T, n) + ValidPtr(dst, T, n)  ←  both ranges ⊆ [0, len)    Proved
          check  Align(src) + Align(dst)                    ←  slice invariant    Proved

return                                                           [type-invariant]
          check  NonNull + Align + ValidNum + Allocated + Init  ←  _1 unchanged    Proved

result: SOUND

ptr::copy permits overlap (memmove), so no NonOverlap obligation arises.

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   _1 = self (&mut [T]), _2 = other (&mut [T])             [slice invariants]
          path condition: self.len() == other.len()   (from assert!)

_16 = as_mut_ptr(&mut (*_1)); _18 = as_mut_ptr(&mut (*_2)); _20 = len

_15 = ptr::swap_nonoverlapping(_16, _18, _20)                   [checkpoint]
          check  ValidPtr(x, T, n) + Align(x)      ←  equal lengths + slice invariant    Proved
          check  ValidPtr(y, T, n) + Align(y)      ←  equal lengths + slice invariant    Proved
          check  NonOverlap(x, y, T, n)            ←  &mut self and &mut other exclusive    Proved

return                                                           [type-invariant]
          check  NonNull + Align + ValidNum + Allocated + Init  ←  _1 unchanged    Proved

result: SOUND

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   _1 = self (&[T]) / (&mut [T])                           [slice invariant]
          path condition: size_of::<Simd<T, LANES>>() == size_of::<[T; LANES]>()   (from assert_eq!)

_0 = align_to::<Simd<T, LANES>>(&(*_1))                          [checkpoint (transmute)]
          check  ValidTransmute(T, Simd<T, LANES>)  ←  layout-identical by the size assertion    Proved
          # all alignment / contiguity / bounds properties inherited from align_to verification

return                                                           [type-invariant]
          check  NonNull + Align + ValidNum + Allocated + Init  ←  _1 unchanged    Proved

result: SOUND

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   _1 = self (&mut [T]), _2 = indices ([I; N])              [slice invariant]

_5 = get_disjoint_check_valid(indices, len)                     // inlined helper branches on the enumerated Ok paths

_15 = get_disjoint_unchecked_mut(_1, indices)                   [checkpoint]
          check  InBound(self, indices)   ←  inlined Ok-path conditions          Proved
          check  NonOverlap(indices)      ←  inlined Ok-path conditions          Proved

return                                                           [type-invariant]
          check  NonNull + Align + ValidNum + Allocated + Init  ←  _1 unchanged    Proved

result: SOUND

These results concern the enumerated paths through the helper and the unsafe call. They do not constitute a separately verified postcondition for get_disjoint_check_valid over every loop iteration.

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). Its #[rapx::verify] annotation yields a SOUND (no unsafe checkpoints) result. The annotation does not turn its Ok return into a trusted postcondition; RAPx analyzes the helper's inlined branches when checking 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.

entry   _1 = indices (&[I; N]), _2 = len (usize)

# outer loop: for (i, idx) in indices.iter().enumerate()
_20 = idx.is_in_bounds(len)

# inner loop: for idx2 in indices[..i]
_39 = idx.is_overlapping(idx2)

result: SOUND (no unsafe checkpoints; pure validation loop)

By inspection, the source returns Ok only after every index passes is_in_bounds and every compared pair passes is_overlapping. The helper's own SOUND result does not prove that postcondition. The caller check uses conditions from the helper paths it enumerates.

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   _1 = self (&[T]) / (&mut [T])                           [slice invariant]
          fact: ValidTransmute([T; N], T)

_2 = unchecked_mul(len, N)                                      // new length = len * N

_12 = ptr.cast::<T>(as_ptr(_1))                                 // re-interpret *const [T; N] as *const T

_11 = raw::from_raw_parts(_12, _2)                              [checkpoint]
          check  NonNull + ValidPtr + Init + Alive + Alias + Align  ←  inherited from the slice invariant    Proved
          check  ValidNum(new_len * sizeof_T ≤ isize::MAX)          ←  slice already in the address space     Proved
          # cast re-interpretation covered by ValidTransmute([T; N], T)

return                                                           [type-invariant]
          check  NonNull + Align + ValidNum + Allocated + Init  ←  _1 unchanged    Proved

result: SOUND

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