Struct VerifyDriver 

pub(crate) 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>

target: &'target FunctionTarget<'tcx>

path_info: Vec<CallGroup<'tcx>>

engine: VerifyEngine<'tcx>

allow_repeat: usize

Implementations

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

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

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

Run unsafe-checkpoint verification for the managed function target.

fn check_property_paths( &self, view: &CheckpointCheckView<'_, '_, 'tcx>, property: &Property<'tcx>, ) -> Vec<(CheckResult, String)>

Check one property (atom / And / Or) across all paths, returning per-path (result, path_desc) pairs. And/Or are folded per path, preserving per-leaf slicing for precision.

fn combine_check_paths( &self, view: &CheckpointCheckView<'_, '_, 'tcx>, children: &[Box<Property<'tcx>>], fold: fn(CheckResult, CheckResult) -> CheckResult, replace_desc_on: fn(&CheckResult) -> bool, ) -> Vec<(CheckResult, String)>

Fold And/Or children per path: fold combines results, and the description is replaced when replace_desc_on matches the child result.

pub(crate) 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(crate) fn iter_callsite_checks( &self, ) -> impl Iterator<Item = CheckpointCheckView<'_, 'target, 'tcx>> + '_

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

pub(crate) 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.

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

Verify built-in type invariants (e.g. the synthesized slice invariant) at every path endpoint. Assumes them at entry (as ContractFacts) and re-proves them at the end of each path, so a mutation that breaks the invariant is caught even without a user-written invariant annotation.

fn run_invariant_checks( &self, invariants: &[Property<'tcx>], entry_facts: &[RelevantItem<'tcx>], is_constructor: bool, check_unwind: bool, label: &str, ) -> Vec<PropertyCheckResult<'tcx>>

Shared core for verify_struct_invariants / verify_type_invariants: enumerate the paths to each invariant checkpoint (build_invariant_trees) and check every invariant against every path, producing one PropertyCheckResult per (checkpoint, invariant, path) triple.

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