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