rapx/verify/slicer/
display.rs

1//! Diagnostic formatting for path-refinement types.
2
3use std::fmt::Write;
4
5use rustc_middle::ty::TyCtxt;
6
7use crate::verify::{helpers::CheckpointLocation, path_extractor::PathStep};
8
9use super::types::{BackwardItem, ForgetReason, KeepReason, RelevantMirItems};
10
11impl<'tcx> RelevantMirItems<'tcx> {
12    /// Render a detailed, path-ordered diagnostic for a checkpoint visit.
13    pub fn describe(
14        &self,
15        tcx: TyCtxt<'tcx>,
16        checkpoint: &crate::verify::helpers::Checkpoint<'tcx>,
17        path_index: usize,
18    ) -> String {
19        let header = format!(
20            "      checkpoint: {} at bb{}",
21            checkpoint.callee_name(tcx),
22            checkpoint.block.as_usize()
23        );
24        self.describe_common(tcx, path_index, &header)
25    }
26
27    /// Render diagnostics for a struct invariant checkpoint (no callee name).
28    pub fn describe_for_checkpoint(
29        &self,
30        tcx: TyCtxt<'tcx>,
31        checkpoint: CheckpointLocation,
32        path_index: usize,
33    ) -> String {
34        let header = format!("      checkpoint: bb{}", checkpoint.block.as_usize());
35        self.describe_common(tcx, path_index, &header)
36    }
37
38    fn describe_common(&self, tcx: TyCtxt<'tcx>, path_index: usize, header: &str) -> String {
39        let mut out = String::new();
40        let caller = self.checkpoint.caller;
41        let body = tcx.optimized_mir(caller);
42
43        let _ = writeln!(out, "{header}");
44        let _ = writeln!(
45            out,
46            "      property: kind={:?}, args={:?}",
47            self.property.kind, self.property.args
48        );
49        let _ = writeln!(out, "      path {path_index}:");
50        let _ = writeln!(out, "        |_ kind: entry",);
51        let _ = writeln!(out, "        |_ steps: {}", self.path.describe_body());
52        let _ = writeln!(
53            out,
54            "        |_ roots: {} place(s), {} local(s)",
55            self.roots.place_count(),
56            self.roots.local_count()
57        );
58        let _ = writeln!(out, "      relevant MIR items:");
59
60        let mut has_relevant_item = false;
61        for step in self.path.steps.iter() {
62            let step_items: Vec<_> = self
63                .items
64                .iter()
65                .filter(|item| item_belongs_to_step(item, step))
66                .collect();
67            if step_items.is_empty() {
68                continue;
69            }
70            has_relevant_item = true;
71
72            let _ = writeln!(out, "        |_ {}", describe_path_step(step));
73            for item in step_items {
74                let _ = writeln!(out, "        |  |_ {}", describe_backward_item(item, body));
75            }
76        }
77        if !has_relevant_item {
78            let _ = writeln!(out, "        |_ <none>");
79        }
80
81        let forgets: Vec<_> = self
82            .items
83            .iter()
84            .filter_map(|item| match item {
85                BackwardItem::Forget { reason } => Some(reason),
86                _ => None,
87            })
88            .collect();
89        if !forgets.is_empty() {
90            let _ = writeln!(out, "      precision loss:");
91            for reason in forgets {
92                let _ = writeln!(out, "        |_ {}", describe_forget_reason(reason));
93            }
94        }
95
96        out
97    }
98}
99
100// ── diagnostic helpers ──────────────────────────────────────────────────
101
102fn item_belongs_to_step(item: &BackwardItem<'_>, step: &PathStep) -> bool {
103    match (item, step) {
104        (BackwardItem::Statement { block, .. }, PathStep::Block(step_block)) => block == step_block,
105        (BackwardItem::Terminator { block, kind }, PathStep::Block(step_block)) => {
106            block == step_block && *kind != KeepReason::Checkpoint
107        }
108        (BackwardItem::Terminator { block, kind }, PathStep::Checkpoint(location)) => {
109            *kind == KeepReason::Checkpoint && *block == location.block
110        }
111
112        (
113            BackwardItem::PathStep {
114                step: item_step, ..
115            },
116            step,
117        ) => same_path_step(item_step, step),
118        _ => false,
119    }
120}
121
122fn same_path_step(lhs: &PathStep, rhs: &PathStep) -> bool {
123    match (lhs, rhs) {
124        (PathStep::Block(lhs), PathStep::Block(rhs)) => lhs == rhs,
125        (PathStep::Checkpoint(lhs), PathStep::Checkpoint(rhs)) => lhs == rhs,
126        _ => false,
127    }
128}
129
130fn describe_path_step(step: &PathStep) -> String {
131    match step {
132        PathStep::Block(block) => format!("bb{}", block.as_usize()),
133        PathStep::Checkpoint(location) => format!("checkpoint(bb{})", location.block.as_usize()),
134    }
135}
136
137fn describe_backward_item(item: &BackwardItem<'_>, body: &rustc_middle::mir::Body<'_>) -> String {
138    match item {
139        BackwardItem::Statement {
140            block,
141            statement_index,
142            kind,
143            ..
144        } => {
145            let statement = &body.basic_blocks[*block].statements[*statement_index];
146            format!("stmt#{} [{:?}] {:?}", statement_index, kind, statement.kind)
147        }
148        BackwardItem::Terminator { block, kind } => {
149            let terminator = body.basic_blocks[*block].terminator();
150            format!("terminator [{:?}] {:?}", kind, terminator.kind)
151        }
152        BackwardItem::PathStep { kind, .. } => format!("path-step {:?}", kind),
153        BackwardItem::ContractFact { property } => {
154            format!(
155                "contract kind={:?}, args={:?}",
156                property.kind, property.args
157            )
158        }
159        BackwardItem::Forget { reason } => format!("forget {:?}", reason),
160    }
161}
162
163fn describe_forget_reason(reason: &ForgetReason) -> &'static str {
164    match reason {
165        ForgetReason::UnknownCall => {
166            "UnknownCall: a retained call may affect relevant state and has no summary yet"
167        }
168        ForgetReason::SccWithoutSummary => {
169            "SccWithoutSummary: a relevant SCC exit has no verified SCC summary yet"
170        }
171        ForgetReason::MayAliasWrite => {
172            "MayAliasWrite: a write may alias relevant state and is not modeled precisely yet"
173        }
174        ForgetReason::UnsupportedEffect => {
175            "UnsupportedEffect: a relevant MIR effect is not modeled precisely yet"
176        }
177    }
178}
rapx/verify/slicer/display.rs

rapx/verify/slicer/
display.rs
