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::{
9    contract,
10    path_extractor::Path,
11};
12use rustc_hir::def_id::DefId;
13use rustc_middle::mir::{BasicBlock, Local};
14
15/// A proof goal for one `(checkpoint, path)` item: the set of relevant items
16/// plus the path context needed to verify the target property.
17#[derive(Clone, Debug)]
18pub struct ProofGoal<'tcx> {
19    /// Path being visited; `path.target` identifies the checkpoint.
20    pub path: Path,
21    /// Items kept from the path.
22    pub items: Vec<RelevantItem<'tcx>>,
23}
24
25/// One relevant item kept from the backward slice.
26#[derive(Clone, Debug)]
27pub enum RelevantItem<'tcx> {
28    /// A MIR statement retained from a basic block.
29    Statement {
30        block: BasicBlock,
31        statement_index: usize,
32    },
33    /// A MIR terminator retained from a basic block.
34    Terminator { block: BasicBlock },
35    /// A contract fact injected by the engine before the forward visit.
36    /// Never produced by the backward visitor itself.
37    ContractFact { property: contract::Property<'tcx> },
38    /// A conservative loss of precision for relevant state (an unsupported
39    /// call whose effects are not modeled).
40    Forget,
41    /// Enter a callee's MIR body. Subsequent Statement/Terminator items
42    /// are interpreted in the callee's context until `CalleeExit`.
43    /// `args` holds the caller's Local indices for each callee parameter
44    /// (arg 0 → callee local_1, arg 1 → callee local_2, ...).
45    CalleeEntry {
46        callee: DefId,
47        args: Vec<Local>,
48    },
49    /// Return from a callee's MIR body. Writes `local_0` (callee return)
50    /// to the caller's `dest` local. Restores the caller's function context.
51    CalleeExit {
52        dest: Local,
53    },
54}
rapx/verify/slicer/types.rs

rapx/verify/slicer/
types.rs
