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>

target: &'target FunctionTarget<'tcx>

path_info: Vec<CallGroup<'tcx>>

engine: VerifyEngine<'tcx>

allow_repeat: usize

Implementations

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

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

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

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.

fn check_or_property( &self, report: &mut VerificationReport<'tcx>, view: &CheckpointCheckView<'_, '_, 'tcx>, property_index: usize, or_property: &Property<'tcx>, )

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>