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-04-03 --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
  ownedheap     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 three 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)
      --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, invless (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]
• invless — like scan or targeted but skip struct invariant checks

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 dispath 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, queries: &'tcx Queries<'tcx>) -> Compilation {
        compiler.session().abort_if_errors();
        queries.global_ctxt().unwrap().enter(
            |tcx| my_analysis(tcx, *self) // the analysis function to execute after compilation.
        );
        compiler.session().abort_if_errors();
        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 name(&self) -> &'static str;
    fn run(&mut self);
    fn reset(&mut self);
}
}

• name(): Returns a human-readable name for logging.
• run(): Executes the analysis. This is the main entry point called by the dispatcher.
• reset(): Clears internal state for re-execution.

Each analysis module defines a subtrait (e.g., AliasAnalysis, DataflowAnalysis, RangeAnalysis) that extends Analysis with query methods. A default implementation struct (e.g., AliasAnalyzer, DataflowAnalyzer) provides concrete algorithms.

Navigating the Compiler API

Common patterns used throughout RAPx:

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

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

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

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

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

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

Stable MIR and Compatibility

The Nightly Dependency

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

This has practical consequences:

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

Example from compat.rs:

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

And a typical usage pattern in analysis code:

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

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

Stable MIR (SMI)

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

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

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

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

Chapter 5. Analysis

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

Layered Design

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

• Analysis trait (top layer): Defines name(), run(), and reset() — 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 name(&self) -> &'static str;
    fn run(&mut self);
    fn reset(&mut self);
}

pub trait AliasAnalysis: Analysis {
    fn get_fn_alias(&self, def_id: DefId) -> Option<FnAliasPairs>;
    fn get_all_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_analysis/.

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_analysis::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_analysis/default/.

5.2.2.1 Architecture: AliasGraph

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

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

Key fields:

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

5.2.2.2 Path-Sensitive Analysis via PathGraph Integration

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

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

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

5.2.2.3 Feature: Path Reachability Filtering

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

For example:

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

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

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

5.2.2.4 SCC Handling via PathGraph

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

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

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

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

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

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

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

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

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

    r
}
}

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

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

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

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

5.2.2.5 Inter-Procedural Alias Resolution

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

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

5.2.2.6 Feature: Field Sensitivity

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

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

For example:

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

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

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

5.2.2.7 Key Steps of the MOP Algorithm

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

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

Reference

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

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

5.2.3 MFP-Based Alias Analysis

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

Example output for MOP:

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

To use analysis results in code:

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

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

Chapter 5.3. API-Dependency Graph

Overview

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

Use the following example to demonstrate this graph structure.

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

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

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

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

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

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

Quick Usage Guide

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

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

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

cargo rapx analyze adg

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

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

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

#![allow(unused)]
fn main() {
use analysis::api_dependency::{ApiDependencyAnalyzer, Config}; // Import the module
let config = Config::default(); // pub_only=true by 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 api_count: usize,
    pub type_count: usize,
    pub generic_param_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>
}

provider_tys

Returns a list of types that can be transformed into the ty type.

#![allow(unused)]
fn main() {
pub fn provider_tys(&self, ty: Ty<'tcx>) -> Vec<Ty<'tcx>>
}

all_transform_for

Returns all transformation kinds applicable to the specified type.

#![allow(unused)]
fn main() {
pub fn all_transform_for(&self, ty: Ty<'tcx>) -> Vec<TransformKind>
}

get_node

Retrieves or creates a node index for a given DepNode. If node doesn't exist in graph, it will add this node into the graph and return it's NodeIndex.

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

get_index_by_node

Given a DepNode, returns Option<Nodeindex>, cause it may not exist in the graph

#![allow(unused)]
fn main() {
pub fn get_index_by_node(&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 callgraph = CallGraphAnalyzer::new(tcx);    // create a callgraph object
callgraph.start();  // do the analysis
}

get_callee_def_path

#![allow(unused)]
fn main() {
pub fun get_callee_def_path(&self, def_path: String) -> Option<HashSet<String>>{
    ...
}
}

You can get all callees define path returned in a hash set with the caller define path.

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 structures are in rapx/src/graphs/dataflow.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. Owned Heap Analysis

Owned heap 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/ownedheap_analysis/.

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 an OHAResultMap keyed by DefId.

OwnedHeapAnalysis Trait

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

    fn is_heapowner<'tcx>(hares: OHAResultMap, ty: Ty<'tcx>) -> Result<bool, &'static str> { ... }
    fn maybe_heapowner<'tcx>(hares: OHAResultMap, 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 OwnedHeap::True.
• maybe_heapowner: Checks whether a non-heap-owning type could become a heap owner after monomorphization — returns true if any variant has OwnedHeap::False with at least one type parameter flagged as owning.

Result Format

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

pub enum OwnedHeap {
    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 (OwnedHeap, Vec<bool>):

• OwnedHeap: 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 owned-heap

In code:

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

The Four-Phase Pipeline

OwnedHeapAnalyzer::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 OwnedHeap::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 OwnedHeap::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<OwnedHeap> per field plus flags for whether the type requires runtime deallocation checking.

Examples

Basic Proxy Types

The test at rapx/tests/analyze/ownedheap_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 owned-heap

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 OwnedHeapAnalyzer 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:

RAP_LOG=trace cargo rapx analyze range

To use the feature in Rust code:

#![allow(unused)]
fn main() {
let mut range_analysis = RangeAnalyzer::<i128>::new(self.tcx, false);
range_analysis.run();
let path_constraint = range_analysis.get_all_path_constraints();
rap_info!("{}", PathConstraintMapWrapper(path_constraint));
let result = analyzer.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_analysis/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/range/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/range/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/range/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/safetyflow_analysis/.

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 as a member and reuses its Value, AliasBlockFacts, and MopFnAliasPairs types. However, SafeDropGraph implements its own path-sensitive alias_bb and alias_bbcall methods that layer drop-aware logic (drop record synchronisation, use-after-free checks, and drop-info clearing) on top of AliasGraph's core assign_alias and merge_alias operations. The precomputed alias summaries identify which function parameters and return values may alias, enabling inter-procedural drop tracking without re-analyzing callees.

Key data structures from the alias analysis reused by SafeDrop:

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

2. Path-Sensitive Bug Detection

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

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

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

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

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

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

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

Source Structure

The safedrop/ module is organized as follows:

Reference

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

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

Chapter 6.2. Memory Leakage Detection

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

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

Bug Types

rCanary detects two categories of memory leaks:

1. Orphan Object

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

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

2. Proxy Type

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

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

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

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

Architecture

rCanary's overall architecture consists of three main stages:

Stage 1: Type Analysis (ADT-DEF Analysis)

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

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

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

Stage 2: Flow Analysis (Constraint Construction)

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

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

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

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

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

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

Stage 3: Constraint Solving (SMT)

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

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

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

Source Structure

Usage

Prerequisites

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

# macOS
brew install z3

# Ubuntu/Debian
apt-get install z3

Running rCanary

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

cargo rapx check -m

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

Output

When a leak is detected:

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

Additional Configure Arguments

rCanary provides optional environment variables for diagnostic output:

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

Note: These parameters may change due to version migration.

Example: Z3GOAL Output

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

Reference

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

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

Chapter 7. Optimization

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

Usage

To detect performance bugs:

cargo rapx opt

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

Architecture

The opt module operates in three steps:

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

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

Categories

The module covers six categories of performance checks:

Test Cases

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

bounds_len — Bounds Checking

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

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

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

Expected output: Bounds Checking: 2.

encoding_check — Encoding Checking

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

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

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

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

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

Expected output: Encoding Checking: 2.

hash_key_cloning — Memory Cloning

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

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

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

Expected output: Cloning: 1.

Detailed Module Reference

Bounds Checking (checking/bounds_checking/)

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

Sub-modules:

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

Encoding Checks (checking/encoding_checking/)

Detects inefficient encoding patterns in string and byte manipulation.

Sub-modules:

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

Memory Cloning (memory_cloning/)

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

Sub-modules:

• used_as_immutable.rs: Detects cloned values that are only used in immutable contexts.
• hash_key_cloning.rs: Specifically targets 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)).

Iterator (iterator/)

The iterator check (next_iterator.rs) detects manual for loops that can be expressed as iterator chains, enabling the compiler to apply loop fusion and other optimizations.

#![allow(unused)]
fn main() {
fn foo(data: &[i32]) -> Vec<i32> {
    let mut result = Vec::new();
    for &item in data {
        result.push(item * 2);
    }
    result
}
}

RAPx suggests using iterator combinators (map, collect):

#![allow(unused)]
fn main() {
fn foo(data: &[i32]) -> Vec<i32> {
    data.iter().map(|&item| item * 2).collect()
}
}

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 / invless modes
• 8.2 Verification Target Collection — how targets are gathered and how contracts are resolved (annotation → JSON → call-chain)
• 8.3 Safety Property Contracts — complete syntax reference: property kinds, argument grammar, ValidNum predicates, direct annotation syntax, and the JSON contract database format
• 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, forward verification, 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 three 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(self.0, T, 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.

invless Mode

For structs that lack #[rapx::invariant] annotations, their safety contracts are still verifiable through constructor-to-caller method chains. invless mode 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 along the path. If every constructor → mutator* → method chain passes for a given struct, the struct's usage is considered sound.

cargo rapx verify --mode invless

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 --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 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.4.

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 two targets:

Full output (annotations explained below):

14:49:41|RAPx|INFO|: Start analysis with RAPx.
14:49:41|RAPx|INFO|: ============================================================
14:49:41|RAPx|INFO|: [rapx::verify] prepare targets for struct: LinkedList
14:49:41|RAPx|INFO|: ============================================================
14:49:41|RAPx|INFO|:   struct invariants:                              ①
14:49:41|RAPx|INFO|:     - Align(head.unwrap_some(), Node)
14:49:41|RAPx|INFO|:     - Align(tail.unwrap_some(), Node)
14:49:41|RAPx|INFO|:     - Allocated(head.unwrap_some(), Node, 1)
14:49:41|RAPx|INFO|:     - Owning(head.unwrap_some())
14:49:41|RAPx|INFO|:   --- method: from_vec ---------------------------- ②
14:49:41|RAPx|INFO|:       return checkpoints: 1 block(s) [15]           ③
14:49:41|RAPx|INFO|:       unsafe callee: std::ptr::NonNull::<T>::as_mut(…)
14:49:41|RAPx|INFO|:         safety contracts:                           ④
14:49:41|RAPx|INFO|:           - Ptr2Ref(self.head, T)
14:49:41|RAPx|INFO|:       checkpoint paths:                             ⑤
14:49:41|RAPx|INFO|:         #0 core::ptr::non_null::as_mut at bb10
14:49:41|RAPx|INFO|:           path 0: 0 -> 1 -> 2 -> 3 -> 5 -> 7 -> 8 -> 9 -> 11 -> 14 -> 2 -> 3 -> 5 -> 7 -> 8 -> 9 -> 10
14:49:41|RAPx|INFO|:         #1 core::ptr::non_null::as_mut at bb12
14:49:41|RAPx|INFO|:           path 0: 0 -> 1 -> 2 -> 3 -> 5 -> 7 -> 8 -> 9 -> 11 -> 14 -> 2 -> 3 -> 5 -> 7 -> 8 -> 9 -> 10 -> 12
14:49:41|RAPx|INFO|:   --- method: drop -------------------------------- ②
14:49:41|RAPx|INFO|:       return checkpoints: 1 block(s) [7]            ③
14:49:41|RAPx|INFO|:       + constructor: LinkedList::from_vec           ⑥
14:49:41|RAPx|INFO|:       unsafe callee: std::boxed::Box::<T>::from_raw(…)
14:49:41|RAPx|INFO|:         safety contracts:                           ④
14:49:41|RAPx|INFO|:           - Allocated(raw, T, 1)
14:49:41|RAPx|INFO|:           - Owning(raw)
14:49:41|RAPx|INFO|:           - Alias(raw, ret)
14:49:41|RAPx|INFO|:       unsafe callee: std::ptr::NonNull::<T>::as_ref(…)
14:49:41|RAPx|INFO|:         safety contracts:
14:49:41|RAPx|INFO|:           - Ptr2Ref(self.head, T)
14:49:41|RAPx|INFO|:       checkpoint paths:                             ⑤
14:49:41|RAPx|INFO|:         #0 core::ptr::non_null::as_ref at bb2
14:49:41|RAPx|INFO|:           path 0: 0 -> 1 -> 2
14:49:41|RAPx|INFO|:         #1 alloc::boxed::from_raw at bb4
14:49:41|RAPx|INFO|:           path 0: 0 -> 1 -> 2 -> 3 -> 4
14:49:41|RAPx|INFO|: ============================================================
14:49:41|RAPx|INFO|: [rapx::verify] total: 0 free function(s), 2 method(s), …  ⑦

Chapter 8.3. Safety Property Contracts

RAPx verifies safety through explicit contracts declared in source code. This chapter covers how to write contracts using the available property kinds, and how to inspect resolved contracts with --debug-contracts.

Contracts are declared in two ways:

1. Direct annotation — #[rapx::requires(...)], #[rapx::invariant(...)] attributes in Rust source (§8.3.2).
2. JSON database — pre-written contracts for standard-library functions that cannot be annotated upstream (§8.3.4).

8.3.1 Property Kinds

The semantics of each property kind are defined in primitive-sp.md. An annotated reference with examples for each kind is in §8.3.3.

8.3.2 Direct Annotation Syntax

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

#[rapx::requires(...)]

Declares a precondition on an (usually unsafe) function. Each attribute holds one property; group with commas or repeat the attribute:

#![allow(unused)]
fn main() {
// Repeated attributes …
#[rapx::requires(ValidPtr(ptr, u32, 1))]
#[rapx::requires(Align(ptr, u32))]

// … are equivalent to a single grouped attribute
#[rapx::requires(ValidPtr(ptr, u32, 1), Align(ptr, u32))]
}

A complete example:

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

#[rapx::verify]

Marks a function as a verification entry point for --mode targeted (Chapter 8.1.2). It takes no arguments and is orthogonal to #[rapx::requires].

#[rapx::invariant(...)]

Declares a struct-level invariant that must hold for every instance at all observable points (see Chapter 8.4):

#![allow(unused)]
fn main() {
#[rapx::invariant(ValidPtr(ptr, T, cap))]
#[rapx::invariant(Align(ptr, T))]
pub struct MyBuf<T> {
    ptr: *mut T,
    len: usize,
    cap: usize,
}
}

any(...) Combinator

The any(...) combinator represents logical OR between disjuncts, where commas inside each parenthesized disjunct mean logical AND:

any((Null(p)), (P1(p, ...), P2(p, ...), ...))

The currently supported shape is a null guard: exactly two disjuncts, one being Null(p) alone, the other a conjunction of properties over the same place p. The semantics: the conjunct properties hold whenever p is non-null, and the whole contract is satisfied when p is null. This works in both #[rapx::requires] and #[rapx::invariant] positions:

• In requires: The SMT solver encodes (p == 0) ∨ (P1 ∧ P2). If the caller's state satisfies either branch, the contract is proved. This is useful for functions like ptr::as_ref() that accept null pointers — the contract declares the pointer may be null, but must be valid and aligned when non-null:

#![allow(unused)]
fn main() {
#[rapx::requires(any(Null(self), (ValidPtr(self, T, 1), Align(self, T))))]
pub unsafe fn as_ref<'a, T>(self: *const T) -> Option<&'a T> { /* ... */ }
}

• In invariant: Used for struct fields that may be null (e.g., linked list tail pointers). Combined with dominance information from null checks in user code (if ptr.is_null() { return; }), the verifier determines which branch to prove:

#![allow(unused)]
fn main() {
#[rapx::invariant(any((Null(next)), (ValidPtr(next, Node, 1), Align(next, Node))))]
pub struct Node {
    value: u32,
    next: *mut Node,
}
}

In both cases, any(Null(p), (P1, P2)) expands to individual Property objects for P1 and P2, each tagged with the null-guard place. The SMT checker then asserts p != 0 before proving each conjunct, which is equivalent to proving (p == 0) ∨ P_i_holds.

Contract Kind Metadata

A property may carry a trailing kind = "<string>" tag inside the same attribute. Two ContractKind values are recognized:

• kind = "precond" (default): A normal safety precondition. An Unproved verdict for this kind contributes to the UNSOUND result.
• kind = "hazard": An advisory warning about a known unsafety pattern. An Unproved verdict for this kind does not contribute to the UNSOUND count — it is printed as an informational [hazard] entry. Set via kind = "hazard" inside #[rapx::requires]:

#![allow(unused)]
fn main() {
#[rapx::requires(ValidNum(size_of::<T>() * len <= isize::MAX), kind = "hazard")]
pub unsafe fn from_raw_parts<T>(ptr: *const T, len: usize) -> *const [T] {
    // ...
}
}

The Alias property is always classified as hazard automatically. Hazard contracts are also used in std-public-contracts.json to flag known but currently unprovable constraints.

Places accepted in annotations

• Parameter names in requires: self, ptr, index, len.
• Field names in invariant: ptr, cap, head — no self. prefix.
• Field projections in requires (via self): self.0, self.ptr.
• Length sugar: self.len is read as len(self).
• Const generics: N resolves to the enclosing item's const parameter.

8.3.3 Property Reference

Alias(p1, p2)

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

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

Align(ptr, Ty)

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

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

Alive(ptr, 'a)

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

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

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

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

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

Deref(ptr, Ty, count)

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

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

InBound / InBounded

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

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

Init(ptr, Ty, count)

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

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

Layout(ptr, layout)

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

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

NonNull(ptr) / Null(ptr)

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

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

NonOverlap(a, b, T, count)

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

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

NonVolatile(p, T, len)

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

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

NoPadding(T)

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

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

Opened(fd)

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

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

Owning(ptr)

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

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

Pinned(p, l)

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

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

Ptr2Ref(ptr, T)

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

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

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

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

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

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

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

SplitTransmute([Src], [Dst])

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

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

Trait(T, trait)

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

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

Typed(ptr, Ty)

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

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

Unreachable

The code path is unreachable. psp V.5.

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

Unwrap(x, variant)

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

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

ValidCStr(ptr, len)

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

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

ValidNum(predicate) / ValidNum(value, interval)

Numeric constraints. Two forms: psp III.1.

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

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

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

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

ValidPtr(ptr, Ty, count)

(ptr as usize) % align_of::<Ty>() != 0 — the pointer is valid for reading and writing count elements of Ty. Defined in primitive-sp §2.2: for ZSTs vacuously true; for non-ZSTs equivalent to Allocated ∧ InBound.

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

ValidString(ptr, u8, len)

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

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

ValidTransmute(Src, Dst)

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

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

8.3.4 JSON Contracts

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

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

The 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.5 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. Run them together for both views.

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

14:43:38|RAPx|INFO|: [rapx::debug-contracts] Expanded Contract Assertions
14:43:38|RAPx|INFO|: ============================================================
14:43:38|RAPx|INFO|: 
14:43:38|RAPx|INFO|: fn LinkedList::from_vec(values: std::vec::Vec<i32>) -> LinkedList
14:43:38|RAPx|INFO|: -------------------------------------------------------------------
14:43:38|RAPx|INFO|:   Safety Tag: Align(head.unwrap_some(), Node)
14:43:38|RAPx|INFO|:     Meaning:   (head.unwrap_some() as usize) % align_of::<Node>() == 0
14:43:38|RAPx|INFO|:   Safety Tag: Allocated(head.unwrap_some(), Node, 1)
14:43:38|RAPx|INFO|:     Meaning:   head.unwrap_some() points to live heap/stack allocation, Node, 1
14:43:38|RAPx|INFO|:   Safety Tag: Owning(head.unwrap_some())
14:43:38|RAPx|INFO|:     Meaning:   ownership(*head.unwrap_some()) = none
14:43:38|RAPx|INFO|: 
14:43:38|RAPx|INFO|: fn std::ptr::NonNull::<T>::as_mut::<'a>(&mut self: &mut std::ptr::NonNull<T>) -> &'a mut T
14:43:38|RAPx|INFO|: -------------------------------------------------------------------
14:43:38|RAPx|INFO|:   Safety Tag: Ptr2Ref(self.0, T)
14:43:38|RAPx|INFO|:     Meaning:   can soundly convert self.0 to &/&mut reference
14:43:38|RAPx|INFO|: 
14:43:38|RAPx|INFO|: fn std::boxed::Box::<T>::from_raw(raw: *mut T) -> std::boxed::Box<T>
14:43:38|RAPx|INFO|: -------------------------------------------------------------------
14:43:38|RAPx|INFO|:   Safety Tag: [hazard] Alias(raw, ret)
14:43:38|RAPx|INFO|:     Meaning:   raw and ret alias each other (hazard)

Use --debug-contracts together with --prepare-targets to see both contract resolution and their semantics in one pass.

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(Owning(head.unwrap_some()))]
struct LinkedList { head: Option<NonNull<Node>>, tail: Option<NonNull<Node>> }
}

Running cargo rapx verify on the case study produces:

12:00:18|RAPx|INFO|: Start analysis with RAPx.
12:00:19|RAPx|INFO|: ============================================================
12:00:19|RAPx|INFO|: [rapx::verify] function: LinkedList::from_vec
12:00:19|RAPx|INFO|: ============================================================
12:00:19|RAPx|INFO|:   --- unsafe checkpoints ---
12:00:19|RAPx|INFO|:       unsafe checkpoint: bb10 -> core::ptr::non_null::as_mut
12:00:19|RAPx|INFO|:         path [0, 1, 2, 3, 5, 7, 8, 9, 11, 14, 2, 3, 5, 7, 8, 9, 10, 12, 13, 14, 2, 3, 5, 7, 8, 9, 10, 12, 13, 14, 2, 3, 5, 7, 8, 9, 10]:
12:00:19|RAPx|INFO|:           Ptr2Ref | Proved
12:00:19|RAPx|INFO|:         path [0, 1, 2, 3, 5, 7, 8, 9, 11, 14, 2, 3, 5, 7, 8, 9, 10, 12, 13, 14, 2, 3, 5, 7, 8, 9, 10]:
12:00:19|RAPx|INFO|:           Ptr2Ref | Proved
12:00:19|RAPx|INFO|:       unsafe checkpoint: bb12 -> core::ptr::non_null::as_mut
12:00:19|RAPx|INFO|:         path [0, 1, 2, 3, 5, 7, 8, 9, 11, 14, 2, 3, 5, 7, 8, 9, 10, 12, 13, 14, 2, 3, 5, 7, 8, 9, 10, 12]:
12:00:19|RAPx|INFO|:           Ptr2Ref | Proved
12:00:19|RAPx|INFO|:         path [0, 1, 2, 3, 5, 7, 8, 9, 11, 14, 2, 3, 5, 7, 8, 9, 10, 12, 13, 14, 2, 3, 5, 7, 8, 9, 10, 12, 13, 14, 2, 3, 5, 7, 8, 9, 10, 12]:
12:00:19|RAPx|INFO|:           Ptr2Ref | Proved
12:00:19|RAPx|INFO|:   --- struct invariants ---
12:00:19|RAPx|INFO|:       checkpoint bb15:
12:00:19|RAPx|INFO|:         path 0, 1, 2, 3, 5, 7, 8, 9, 11, 14, 2, 3, 6, 15:
12:00:19|RAPx|INFO|:           Align | Proved (x2)
12:00:19|RAPx|INFO|:           Allocated | Proved
12:00:19|RAPx|INFO|:           Owning | Proved
12:00:19|RAPx|INFO|:         path 0, 1, 2, 3, 6, 15:
12:00:19|RAPx|INFO|:           Align | Proved (x2)
12:00:19|RAPx|INFO|:           Allocated | Proved
12:00:19|RAPx|INFO|:           Owning | Proved
12:00:19|RAPx|INFO|:   result: SOUND
12:00:19|RAPx|INFO|:
12:00:19|RAPx|INFO|: ============================================================
12:00:19|RAPx|INFO|: [rapx::verify] function: <LinkedList as std::ops::Drop>::drop
12:00:19|RAPx|INFO|: ============================================================
12:00:19|RAPx|INFO|:   --- unsafe checkpoints ---
12:00:19|RAPx|INFO|:       unsafe checkpoint: bb2 -> core::ptr::non_null::as_ref
12:00:19|RAPx|INFO|:         path [0, 1, 2, 3, 4, 5, 6, 1, 2, 3, 4, 5, 6, 1, 2]:
12:00:19|RAPx|INFO|:           Ptr2Ref | Proved
12:00:19|RAPx|INFO|:         path [0, 1, 2, 3, 4, 5, 6, 1, 2, 3, 4, 5, 6, 1, 2, 3, 4, 5, 6, 1, 2]:
12:00:19|RAPx|INFO|:           Ptr2Ref | Proved
12:00:19|RAPx|INFO|:         path [0, 1, 2, 3, 4, 5, 6, 1, 2]:
12:00:19|RAPx|INFO|:           Ptr2Ref | Proved
12:00:19|RAPx|INFO|:       unsafe checkpoint: bb4 -> alloc::boxed::from_raw
12:00:19|RAPx|INFO|:         path [0, 1, 2, 3, 4, 5, 6, 1, 2, 3, 4]:
12:00:19|RAPx|INFO|:           Allocated | Proved
12:00:19|RAPx|INFO|:           Owning | Proved
12:00:19|RAPx|INFO|:           [hazard] Alias | Proved
12:00:19|RAPx|INFO|:         path [0, 1, 2, 3, 4, 5, 6, 1, 2, 3, 4, 5, 6, 1, 2, 3, 4]:
12:00:19|RAPx|INFO|:           Allocated | Proved
12:00:19|RAPx|INFO|:           Owning | Proved
12:00:19|RAPx|INFO|:           [hazard] Alias | Proved
12:00:19|RAPx|INFO|:         path [0, 1, 2, 3, 4, 5, 6, 1, 2, 3, 4, 5, 6, 1, 2, 3, 4, 5, 6, 1, 2, 3, 4]:
12:00:19|RAPx|INFO|:           Allocated | Proved
12:00:19|RAPx|INFO|:           Owning | Proved
12:00:19|RAPx|INFO|:           [hazard] Alias | Proved
12:00:19|RAPx|INFO|:   result: SOUND
12:00:19|RAPx|INFO|:

The report shows two targets:

For each target the pipeline runs: path extraction → backward slicing → forward verification → SMT check. The sections below use from_vec as the example.

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 for value in values { … } loop contains an SCC with two branches (tail is None or Some). The path extractor unrolls this SCC according to the repeat budget, producing paths for the first iteration (both branches) and subsequent iterations (each branch repeated). The sections below use the first Ptr2Ref path as the single running example:

path [0, 1, 2, 3, 5, 7, 8, 9, 11, 14, 2, 3, 5, 7, 8, 9, 10]   →   Ptr2Ref | Proved

This path represents a two-element input: the first iteration (empty list, bb11 initialises head and tail), then the second iteration where _2.1 is Some and as_mut() is called at bb10.

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, 5, 7, 8, 9, 11, 14, 2, 3, 5, 7, 8, 9, 10] — two-element input, first iteration initialises the empty list, second iteration calls tail.as_mut() at bb10. The relevant MIR blocks:

bb0:  {
    _2 = LinkedList { head: None, tail: None }   // empty list
}
bb1:  {
    _8 = <Vec<i32> as IntoIterator>::into_iter(move _1) → bb2
}
bb2:  {
    _11 = <IntoIter<i32> as Iterator>::next(&mut _8) → bb3   // for loop body
}
bb3:  {
    switchInt(discriminant(_11)) → [0: bb6, 1: bb5]   // None → exit, Some → process
}
bb5:  {
    _17 = Box::<Node>::new(move _18) → bb7             // heap allocate
}
bb7:  {
    _24 = move _17
    _23 = Box::<Node>::leak(move _24) → bb8            // transfer ownership
}
bb8:  {
    _22 = NonNull::<Node>::from(move _23) → bb9        // wrap in NonNull
}
bb9:  {
    _25 = discriminant((_2.1: Option<NonNull<Node>>))
    switchInt(move _25) → [0: bb11, 1: bb10]           // tail is None? Some?
}
bb10: {
    _30 = copy ((_2.1 as Some).0: NonNull<Node>)       // extract stored NonNull
    _34 = &mut _30
    _33 = NonNull::<Node>::as_mut(move _34) → bb12     // ← CHECKPOINT
}
bb11: {
    (_2.0) = Some(_27)                                  // set head
    (_2.1) = Some(_29)  // _29 = copy _22              // set tail
}
bb14: {
    goto → bb2                                          // loop back
}

The example path reaches bb10 on the second iteration: the first iteration went through bb11 (tail was None, initialised), then bb14 loops back, bb2-5-7-8 allocates a second node, bb9 dispatches again — this time tail is Some, so control flows to bb10.

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

Walk backward from _33 = as_mut(move _34):

The collected chain is _34 → _30 → _2.1 → _22 → _23 → _17(where _2.1 is the tail field of LinkedList). The slicer recognises standard-library calls by their effects: Box::new → BoxAllocation, NonNull::from → ReturnPointerFromArg.

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

8.4.3 Forward Verification

The ForwardVerifier performs two distinct analyses:

• Fact accumulation (8.4.3.1): abstract interpretation along a single extracted path from function entry to the checkpoint, gathering facts that feed into SMT checks.
• Hazard tracking (8.4.3.2): a full-CFG flow-sensitive scan from the checkpoint through all reachable branches, checking for alias/ownership conflicts.

Per primitive-sp, Ptr2Ref is Init(p, T, 1) && Align(p, T) && Alias(p, ret). Init and Align are checked together by the SMT solver against accumulated path facts; Alias is handled by the full-CFG hazard tracking phase below.

8.4.3.1 Fact accumulation before the checkpoint

At the checkpoint, the verifier resolves the value chain _34 → _30 → _2.1 → _22 → _23 → _17. At the origin (Box::new), two facts are available for Ptr2Ref:

8.4.3.2 Hazard tracking after the checkpoint

Unlike fact accumulation which follows a single path, the hazard scan operates on the full function CFG, traversing all branches reachable from the checkpoint.

as_mut declares the Alias(p, ret) hazard: _33 aliases _17, violating Rust's exclusive mutability. The verifier must check that this alias causes no UB in the remainder of the function.

The scan checks two things on the full CFG:

1. Exclusive mutability — any raw read/write through the origin(_17, _30, _34)while _33 is live? No conflicts found.
2. Hazard cross function boundary — does _33 escape the function(returned or stored in a surviving field)or remain live at any exit? No: used only locally to set prev/next in bb12-13, dies at scope end. If it did escape(e.g. fn get_tail_mut(&mut self) -> &mut Node { unsafe { self.tail.as_mut() } }), the caller would inherit the obligation.

8.4.4 SMT Check

Each accumulated fact lowers to an SMT constraint:

• Value-definition chain. MIR assignments like _34 = &mut _30 create a definition: _34 is a reference to _30. The SMT model follows this chain, so _34 and _30(and ultimately _17)map to the same Z3 address variable — no separate equality assertion needed.
• PointsTo declares two pointers share provenance, and asserts each is aligned: addr % align_of::<pointee_ty>() = 0.
• KnownAllocated records the allocation's element count(1 for Box<Node>). Used to recover allocation bounds (base, len) during SMT checks.
• KnownInit marks the origin as holding initialized(non-MaybeUninit)memory, enabling the Init range check.

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

For Ptr2Ref on _17, two obligations are checked:

Align

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

The negated goal contradicts the alignment constraint from PointsTo → Unsat → Align | Proved.

Init

Init means _17 points to initialized(non-MaybeUninit)memory whose access fits within the allocation bounds.

• Initialized? Yes: KnownInit from Box::new marks _17's origin as initialized.
• Fits within allocation? Box::new allocates one Node at _17. The allocation has len = 1(element), the access is 1 element starting at offset = 0:

offset + access ≤ len  →  0 + 1 ≤ 1

Trying to assert 0 + 1 > 1 contradicts the known allocation bounds → Unsat → Init | Proved.

8.4.5 Auto-Repeat Planner

For the checkpoint bb10 -> as_mut, Ptr2Ref requires two preconditions: Init and Align. In default auto mode, the planner notices that this checkpoint depends on loop-carried state and chooses a deeper repeat budget. The path extractor therefore produces two paths reaching bb10:

repeat 1:
  path [0, 1, 2, 3, 5, 7, 8, 9, 11, 14, 2, 3, 5, 7, 8, 9, 10, 12, 13, 14, 2, 3, 5, 7, 8, 9, 10]:
    Init  | Proved
    Align | Proved

repeat 2:
  path [0, 1, 2, 3, 5, 7, 8, 9, 11, 14, 2, 3, 5, 7, 8, 9, 10, 12, 13, 14, 2, 3, 5, 7, 8, 9, 10, 12, 13, 14, 2, 3, 5, 7, 8, 9, 10]:
    Init  | Proved
    Align | Proved

The Proved set (Init and Align) is identical across these repeat depths. In this case, 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, forward verifier, and SMT checker then run on the extracted paths as usual.

Chapter 9. Utilities

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

Chapter 9.1 Logging and Diagnostics

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

Logging Macros

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

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

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

Example output:

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

Environment Variable

The log level is controlled by RAPX_LOG:

RAPX_LOG=info   cargo rapx analyze alias      # default — summary output
RAPX_LOG=debug  cargo rapx verify              # + path/fact detail
RAPX_LOG=trace  cargo rapx analyze dataflow    # + full internal state
RAPX_LOG=warn   cargo rapx check -uaf          # warnings only
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

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.

Goal

Prove that all 37 #[rapx::verify]-annotated functions in library/core/src/slice/mod.rs are free of undefined behavior by:

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

Tool Integration

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

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

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

#![allow(unused)]
fn main() {
// Example from core/src/ptr/mod.rs
#[cfg_attr(rapx, rapx::requires(Align(src, T)))]
#[cfg_attr(rapx, rapx::requires(Align(dst, T)))]
#[cfg_attr(rapx, rapx::requires(ValidPtr(src, T, count)))]
#[cfg_attr(rapx, rapx::requires(ValidPtr(dst, T, count)))]
#[cfg_attr(rapx, rapx::requires(NonOverlap(dst, src, T, count)))]
#[cfg_attr(rapx, rapx::requires(ValidNum(size_of(T) * count <= isize::MAX)))]
pub unsafe fn copy_nonoverlapping<T>(src: *const T, dst: *mut T, count: usize) { /* ... */ }
}

Commands

Run verification:

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

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

The RUSTFLAGS environment variable provides three things:

CI Integration

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

Verification Results

All 37 functions pass with result: SOUND. Below is the complete output for one representative target:

============================================================
[rapx::verify] function: slice::<impl [T]>::get_unchecked_mut
============================================================
  --- unsafe checkpoints ---
      unsafe checkpoint: bb1 -> raw-ptr-deref
        path [0, 1]:
          NonNull | Proved
          Align | Proved
      unsafe checkpoint: bb0 -> core::slice::index::SliceIndex::get_unchecked_mut
        path [0]:
          InBound | Proved
  result: SOUND

Code Reference

• Source: safer-rust/rapx-verify-rust-std
• Challenge: #281 / 0017-slice

10.2 Asterinas

Asterinas uses an older toolchain (2025-02-01). 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