rapx/verify/slicer/
types.rs

1//! Data types for the path-refinement layer.
2//!
3//! These structures are produced by the backward visitor and consumed by the
4//! forward visitor, engine, and diagnostic formatting.  `ContractFact` is the
5//! only variant never produced by the backward visitor itself — it is injected
6//! by the engine before the forward visit.
7
8use crate::verify::{contract, path_extractor::Path};
9use rustc_hir::def_id::DefId;
10use rustc_middle::mir::BasicBlock;
11
12/// A proof goal for one `(checkpoint, path)` item: the set of relevant items
13/// plus the path context needed to verify the target property.
14#[derive(Clone, Debug)]
15pub(crate) struct ProofGoal<'tcx> {
16    /// Path being visited; `path.target` identifies the checkpoint.
17    pub path: Path,
18    /// Items kept from the path.
19    pub items: Vec<RelevantItem<'tcx>>,
20    /// Per-global-block function ownership `(def_id, local_index)`, populated
21    /// for inlined multi-function paths. Empty for single-function goals.
22    pub block_fn: Vec<(DefId, usize)>,
23}
24
25/// One relevant item kept from the backward slice.
26#[derive(Clone, Debug)]
27pub(crate) enum RelevantItem<'tcx> {
28    /// A MIR statement retained from a basic block. `def_id` identifies the
29    /// function owning `block` (differs from the caller for inlined callees).
30    Statement {
31        def_id: DefId,
32        block: BasicBlock,
33        statement_index: usize,
34    },
35    /// A MIR terminator retained from a basic block.  For a `SwitchInt`, `block`
36    /// is the switch block and `switch_succ` is the successor taken along this
37    /// path (so the VM need not re-resolve it from the path); for any other
38    /// terminator — or when the path ends at the checkpoint — `switch_succ` is
39    /// `None`.
40    Terminator {
41        def_id: DefId,
42        block: BasicBlock,
43        switch_succ: Option<BasicBlock>,
44    },
45    /// Enter an inlined callee: bind the caller's argument locals to the callee
46    /// parameters. `args` holds the caller's argument local indices.
47    CalleeEntry { callee: DefId, args: Vec<usize> },
48    /// Return from an inlined callee: write the callee's `_0` to the caller's
49    /// destination local.
50    CalleeExit { dest: usize },
51    /// A contract fact injected by the engine before the forward visit.
52    /// Never produced by the backward visitor itself.
53    ContractFact { property: contract::Property<'tcx> },
54    /// An unknown call with no summary (`unsupported`): its effects cannot be
55    /// modeled, so the slicer keeps the terminator but conservatively drops
56    /// precision on the relevant state it touches. The forward VM is a no-op on
57    /// this marker.
58    UnknownCall,
59}
rapx/verify/slicer/types.rs

rapx/verify/slicer/
types.rs
