Struct BackwardSlicer 

pub struct BackwardSlicer<'tcx> {
    tcx: TyCtxt<'tcx>,
}

Entry point for backward path visiting.

Fields

tcx: TyCtxt<'tcx>

Implementations

impl<'tcx> BackwardSlicer<'tcx>

pub fn new(tcx: TyCtxt<'tcx>) -> Self

Create a backward visitor over the current compiler type context.

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

Return the compiler type context owned by this visitor.

pub fn visit_path_tree( &self, tree: &PathTree, target_block: usize, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, ) -> Vec<RelevantMirItems<'tcx>>

Visit a path tree in post-order, sharing backward analysis across common prefixes. Merges child-relevance sets at branch nodes (the union is a sound over-approximation). Returns per-leaf results.

Callee parameter roots are bound at checkpoint nodes.

pub fn visit_path_tree_for_checkpoint( &self, tree: &PathTree, target_block: usize, caller: DefId, checkpoint_loc: CheckpointLocation, property: &Property<'tcx>, ) -> Vec<RelevantMirItems<'tcx>>

Like [visit_path_tree] but without callee-root binding (used for struct-invariant checks where property places are already in the caller’s local namespace).

fn visit_path_tree_impl( &self, tree: &PathTree, target_block: usize, caller: DefId, checkpoint_block: BasicBlock, bind_checkpoint: Option<&Checkpoint<'tcx>>, property: &Property<'tcx>, ) -> Vec<RelevantMirItems<'tcx>>

Internal: post-order recursion returning per-leaf (block_path, backward_items).

fn build_leaf_items( visitor: &Self, node: &PathNode, target_block: usize, checkpoint_block: BasicBlock, bind_checkpoint: Option<&Checkpoint<'tcx>>, property: &Property<'tcx>, body: &'tcx Body<'tcx>, flow: &DataflowGraph, keep_alloc: bool, ) -> Vec<(Vec<usize>, Vec<BackwardItem<'tcx>>, RelevantPlaces)>

Post-order recursion: returns one (block_path, backward_items, relevant_before_block) per checkpoint leaf. Each leaf is independent — no merging, no HashMap collision.

fn visit_statement( &self, block: BasicBlock, statement_index: usize, statement: &'tcx Statement<'tcx>, flow: &DataflowGraph, relevant: &mut RelevantPlaces, items: &mut Vec<BackwardItem<'tcx>>, keep_allocation_invalidations: bool, )

Visit one MIR statement against the current relevance frontier.

fn visit_terminator( &self, block: BasicBlock, terminator: &Terminator<'tcx>, flow: &DataflowGraph, body: &Body<'tcx>, relevant: &mut RelevantPlaces, items: &mut Vec<BackwardItem<'tcx>>, keep_allocation_invalidations: bool, )

Visit one MIR terminator against the current relevance frontier.