Struct LoopSensitivityAnalyzer 

pub(crate) struct LoopSensitivityAnalyzer<'tcx> {
    tcx: TyCtxt<'tcx>,
}

Computes the repeat plan for one verification target.

The analyzer is intentionally target-local. It does not cache across functions because MIR bodies, SCCs, and property roots are small enough for the current auto pass, and keeping the state local prevents stale repeat choices when the same function is checked under a virtual target.

Fields

tcx: TyCtxt<'tcx>

Implementations

impl<'tcx> LoopSensitivityAnalyzer<'tcx>

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

Create an analyzer over the current compiler type context.

pub(crate) fn analyze(&self, target: &FunctionTarget<'tcx>) -> RepeatPlan

Build a loop-sensitivity repeat plan for target.

The algorithm is:

1. Collect all safety sinks and bind their roots to caller locals.
2. Build an SCC-aware PathGraph for the target function.
3. Build a whole-function local dependency index.
4. Produce dataflow-distance hints from loop-carried local transfers.
5. Produce numeric-range hints from simple induction-sensitive sinks.
6. Calibrate both hint streams into one repeat budget.

This is a conservative planner: it may choose a deeper repeat for loops that turn out to be safe, but it avoids adding tag-specific verifier reruns or new user-visible output.

fn dataflow_distance_hints<'target>( &self, sinks: &[SafetySink<'target, 'tcx>], graph: &PathGraph<'_>, dependencies: &LocalDependencyIndex, component_summaries: &[(LoopComponent, LoopLocalSummary, LoopNumericSummary)], ) -> Vec<DataflowDistanceHint>

Compute loop-carried dataflow hints for every safety sink.

This detector is tag-agnostic: it only asks whether the sink’s caller locals depend on state locals that are redefined across an SCC. The concrete safety checker remains responsible for deciding whether the propagated value is actually invalid once the deeper path is enumerated.

fn numeric_range_hints<'target>( &self, sinks: &[SafetySink<'target, 'tcx>], graph: &PathGraph<'_>, dependencies: &LocalDependencyIndex, component_summaries: &[(LoopComponent, LoopLocalSummary, LoopNumericSummary)], ) -> Vec<NumericRangeHint>

Compute numeric/index range hints for induction-sensitive sinks.

This is intentionally small but already separates numeric planning from generic dataflow. ValidNum tries to recover a concrete violating iteration for positive affine increments; InBound currently marks the first iteration missed by shallow unrolling when the pointer/index root depends on an induction variable.

fn collect_sinks<'target>( &self, target: &'target FunctionTarget<'tcx>, ) -> Vec<SafetySink<'target, 'tcx>>

Collect caller-side sinks from all checkpoint kinds in a target.

This mirrors VerifyDriver::properties_for_callsite so the planner and verifier operate on the same obligations. Keeping it here avoids constructing a VerifyDriver only to learn whether a deeper repeat is needed before path extraction.