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    def_use::RelevantPlaces,
11    helpers::CheckpointLocation,
12    path_extractor::{Path, PathStep},
13};
14use rustc_middle::mir::BasicBlock;
15
16/// MIR items relevant to one `(checkpoint, path, property)` item.
17#[derive(Clone, Debug)]
18pub struct RelevantMirItems<'tcx> {
19    /// Unsafe checkpoint whose obligation is being checked.
20    pub checkpoint: CheckpointLocation,
21    /// Required property that determines the relevance roots.
22    pub property: contract::Property<'tcx>,
23    /// Path being visited.
24    pub path: Path,
25    /// Items kept from the path.
26    pub items: Vec<BackwardItem<'tcx>>,
27    /// Initial roots extracted from the property.
28    pub roots: RelevantPlaces,
29}
30
31impl<'tcx> RelevantMirItems<'tcx> {
32    /// Append one kept item to the visited path.
33    pub fn push(&mut self, item: BackwardItem<'tcx>) {
34        self.items.push(item);
35    }
36
37    /// Return true when no MIR/path item has been kept yet.
38    pub fn is_empty(&self) -> bool {
39        self.items.is_empty()
40    }
41}
42
43/// One item kept while walking a path backward.
44#[derive(Clone, Debug)]
45pub enum BackwardItem<'tcx> {
46    /// A MIR statement retained from a basic block.
47    Statement {
48        block: BasicBlock,
49        statement_index: usize,
50        kind: KeepReason,
51    },
52    /// A MIR terminator retained from a basic block.
53    Terminator { block: BasicBlock, kind: KeepReason },
54    /// A path-level step retained as structural context.
55    PathStep { step: PathStep, kind: KeepReason },
56    /// A contract fact injected by the engine before the forward visit.
57    /// Never produced by the backward visitor itself.
58    ContractFact { property: contract::Property<'tcx> },
59    /// A conservative loss of precision for relevant state.
60    Forget { reason: ForgetReason },
61}
62
63/// Why a retained item is relevant.
64#[derive(Clone, Copy, Debug, Eq, PartialEq)]
65pub enum KeepReason {
66    /// The item defines a relevant place.
67    Definition,
68    /// The item contributes a branch/path condition.
69    PathCondition,
70    /// The item contributes pointer provenance or pointer arithmetic.
71    PointerFlow,
72    /// The item refines state through a runtime check.
73    RuntimeCheck,
74    /// The item is the unsafe checkpoint being checked.
75    Checkpoint,
76    /// The item represents a loop summary or loop exit.
77    LoopExit,
78    /// The item may invalidate a relevant fact.
79    Invalidation,
80    /// The item may affect relevant state but is not modeled precisely yet.
81    UnknownEffect,
82}
83
84/// Reason for conservatively forgetting relevant state.
85#[derive(Clone, Debug, Eq, PartialEq)]
86pub enum ForgetReason {
87    /// A call may modify relevant state but has no summary yet.
88    UnknownCall,
89    /// An SCC region may modify relevant state but has no summary yet.
90    SccWithoutSummary,
91    /// A write may alias relevant state.
92    MayAliasWrite,
93    /// A relevant statement or terminator is not supported yet.
94    UnsupportedEffect,
95}
rapx/verify/slicer/types.rs

rapx/verify/slicer/
types.rs
