Struct VerifyDriver 

pub struct VerifyDriver<'target, 'tcx> {
    tcx: TyCtxt<'tcx>,
    target: &'target FunctionTarget<'tcx>,
    path_info: Vec<CallGroup<'tcx>>,
    engine: VerifyEngine<'tcx>,
    allow_repeat: usize,
}

Orchestrates the three-stage verification pipeline (backward data-dependency analysis → forward state simulation → SMT checking) for a single function under analysis.

Each VerifyDriver instance bundles together:

1. The problem statement (target) — which unsafe checkpoints and raw-pointer dereferences exist, what safety contracts they demand, and what entry assumptions (from #[rapx::requires]) and struct invariants apply.

2. The reachability model (path_info) — SCC-aware acyclic paths from function entry to each checkpoint, produced by flattening the MIR control-flow graph with bounded loop unrolling.

3. The verification engine (engine) — a stateless pipeline shared across all (checkpoint, path, property) triples.

4. The loop-unrolling budget (allow_repeat) — caps how many extra iterations a loop body may appear beyond its first occurrence, trading completeness against path enumeration cost.

Verification proceeds in two phases per driver instance:

• verify_function: checks safety properties at each unsafe checkpoint (callee #[rapx::requires] contracts).
• verify_struct_invariants: checks struct invariants at return-block checkpoints (constructors) or at all path endpoints (non-constructor methods).

Fields

tcx: TyCtxt<'tcx>

Compiler type-context handle — gateway to MIR bodies, type definitions, HIR attributes, and def-path strings used throughout the pipeline.

target: &'target FunctionTarget<'tcx>

The function being verified: its identity (def_id), the unsafe operations inside it (checkpoints, raw_ptr_deref_checks), the contracts those operations demand (callee_requires), the contracts the function itself requires as entry assumptions (caller_requires), and any struct invariants to be enforced (struct_invariants).

path_info: Vec<CallGroup<'tcx>>

SCC-aware path metadata for this function.

Per-callee call groups with shared path trees.

engine: VerifyEngine<'tcx>

Stateless three-stage verification pipeline: backward data-dependency analysis → forward state simulation → SMT constraint checking. Shared across all (checkpoint, path, property) triples for this target.

allow_repeat: usize

Loop-unrolling depth for SCC-aware path enumeration.

Controls how many extra times a repeated SCC postfix segment (loop-body) is allowed to appear beyond its first occurrence.

• 0 = each distinct postfix segment at most once (no loop repeats).
• 1 = allow one repeat (loop body appears up to twice).
• n = allow n repeats (loop body appears up to n+1 times).

Higher values increase path coverage but risk exponential blow-up in path count. The CLI driver iterates repeat from 0 to the configured maximum, accumulating results incrementally.

Implementations

impl<'target, 'tcx> VerifyDriver<'target, 'tcx>

pub fn new(tcx: TyCtxt<'tcx>, target: &'target FunctionTarget<'tcx>) -> Self

Build a driver for one collected function target.

pub fn new_with_repeat( tcx: TyCtxt<'tcx>, target: &'target FunctionTarget<'tcx>, allow_repeat: usize, ) -> Self

Build a driver with control over SCC postfix repeat count.

pub fn tcx(&self) -> TyCtxt<'tcx>

Return the compiler type context owned by this driver.

pub fn target(&self) -> &'target FunctionTarget<'tcx>

Return the function target managed by this driver.

pub fn path_info(&self) -> &[CallGroup<'tcx>]

Return the per-callee call groups managed by this driver.

pub fn verify_function(&self) -> VerificationReport<'tcx>

Run unsafe-checkpoint verification for the managed function target.

pub fn properties_for_callsite( &self, checkpoint: &Checkpoint<'tcx>, ) -> &'target [Property<'tcx>]

Return the required properties for a concrete unsafe checkpoint.

Dispatches on CheckpointKind: synthetic checkpoints (raw pointer dereference, static mut access) carry their properties in target.raw_ptr_deref_checks / target.static_mut_checks; real unsafe calls look up target.callee_requires by callee DefId.

pub fn iter_callsite_checks( &self, ) -> impl Iterator<Item = CheckpointCheckView<'_, 'target, 'tcx>> + '_

Iterate over checkpoints together with their shared path tree and properties.

pub fn verify_struct_invariants(&self) -> VerificationReport<'tcx>

Run struct invariant verification for the managed function target.

For constructors (functions returning Self), paths are filtered to return blocks to avoid unwinding paths where the struct may not be fully initialised. For methods, all whole-CFG paths from PathGraph::enumerate_paths_repeat are used directly.

fn build_invariant_trees( &self, is_constructor: bool, ) -> FxHashMap<CheckpointLocation, PathTree>