rapx/verify/
report.rs

1//! Diagnostics and summaries for the staged verifier pipeline.
2//!
3//! The driver and later checking stages report their per-path property results
4//! through the types in this module.  Keeping these types here leaves the driver
5//! focused on orchestration.
6
7use rustc_hir::def_id::DefId;
8
9use super::{contract::Property, helpers::CheckpointLocation};
10
11/// Verification status for one required property on one path.
12#[derive(Clone, Debug)]
13pub enum CheckResult {
14    /// The property has been proved for this path.
15    Proved,
16    /// The verifier found a possible violation for this path.
17    Failed,
18    /// The verifier has not implemented or completed the proof for this path.
19    Unknown,
20}
21
22/// Result for one required property along one path to a checkpoint.
23#[derive(Clone, Debug)]
24pub struct PropertyCheckResult<'tcx> {
25    /// Unsafe checkpoint being checked.
26    pub checkpoint: CheckpointLocation,
27    /// Index of the checkpoint in the function-level checkpoint list.
28    pub checkpoint_index: usize,
29    /// Index of the path in the checkpoint path set.
30    pub path_index: usize,
31    /// Index of the property in the checkpoint-level property list.
32    pub property_index: usize,
33    /// Required property checked on this path.
34    pub property: Property<'tcx>,
35    /// Current verification status.
36    pub result: CheckResult,
37    /// Optional path-local diagnostics generated by the staged visitors.
38    pub diagnostics: Option<VisitDiagnostics>,
39    /// Human-readable path description.
40    pub path_description: String,
41    /// Callee name for this checkpoint.
42    pub callee_name: String,
43}
44
45/// Human-readable diagnostics emitted for one path/property check.
46#[derive(Clone, Debug)]
47pub struct VisitDiagnostics {
48    /// Backward visit summary for relevant MIR items.
49    pub backward: String,
50    /// Forward visit summary for abstract facts collected from those items.
51    pub forward: String,
52}
53
54impl VisitDiagnostics {
55    /// Create diagnostics from backward and forward visitor summaries.
56    pub fn new(backward: String, forward: String) -> Self {
57        Self { backward, forward }
58    }
59}
60
61/// Verification report for one function target.
62#[derive(Clone, Debug)]
63pub struct VerificationReport<'tcx> {
64    /// Function that was verified.
65    pub function: DefId,
66    /// Per-path property results emitted by the verifier.
67    pub results: Vec<PropertyCheckResult<'tcx>>,
68}
69
70impl<'tcx> VerificationReport<'tcx> {
71    /// Create an empty report for a function target.
72    pub fn new(function: DefId) -> Self {
73        Self {
74            function,
75            results: Vec::new(),
76        }
77    }
78
79    /// Add one path/property check result to this report.
80    pub fn push(&mut self, result: PropertyCheckResult<'tcx>) {
81        self.results.push(result);
82    }
83
84    /// Return the number of check results in this report.
85    pub fn len(&self) -> usize {
86        self.results.len()
87    }
88
89    /// Return true when this report contains no check results.
90    pub fn is_empty(&self) -> bool {
91        self.results.is_empty()
92    }
93
94    /// Render the whole report as a readable multi-line diagnostic.
95    pub fn describe(&self) -> String {
96        let mut out = String::new();
97        out.push_str(&format!(
98            "[rapx::verify::diagnostics] function {:?}: {} check item(s)\n",
99            self.function,
100            self.results.len()
101        ));
102
103        for (index, result) in self.results.iter().enumerate() {
104            out.push_str(&format!(
105                "  check #{index}: checkpoint #{}, bb{}, path #{}, property #{} {:?}, result {:?}\n",
106                result.checkpoint_index,
107                result.checkpoint.block.as_usize(),
108                result.path_index,
109                result.property_index,
110                result.property.kind,
111                result.result
112            ));
113
114            if let Some(diagnostics) = &result.diagnostics {
115                out.push_str(&diagnostics.backward);
116                if !diagnostics.backward.ends_with('\n') {
117                    out.push('\n');
118                }
119                out.push_str(&diagnostics.forward);
120                if !diagnostics.forward.ends_with('\n') {
121                    out.push('\n');
122                }
123            }
124        }
125
126        out
127    }
128}
rapx/verify/report.rs

rapx/verify/
report.rs
