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};
10use crate::helpers::mir_scan::CheckpointLocation;
11
12/// Verification status for one required property on one path.
13#[derive(Clone, Debug, PartialEq)]
14pub enum CheckResult {
15    /// The property has been proved for this path.
16    Proved,
17    /// The verifier found a possible violation for this path.
18    Failed,
19    /// The verifier has not implemented or completed the proof for this path.
20    Unknown,
21}
22
23impl CheckResult {
24    /// AND-combine two results: any `Failed` → `Failed`; any `Unknown` →
25    /// `Unknown`; only all-`Proved` → `Proved`.
26    pub fn and(self, other: CheckResult) -> CheckResult {
27        match (self, other) {
28            (CheckResult::Failed, _) | (_, CheckResult::Failed) => CheckResult::Failed,
29            (CheckResult::Unknown, _) | (_, CheckResult::Unknown) => CheckResult::Unknown,
30            _ => CheckResult::Proved,
31        }
32    }
33
34    /// OR-combine two results: any `Proved` → `Proved`; all `Failed` →
35    /// `Failed`; otherwise `Unknown`.
36    pub fn or(self, other: CheckResult) -> CheckResult {
37        match (self, other) {
38            (CheckResult::Proved, _) | (_, CheckResult::Proved) => CheckResult::Proved,
39            (CheckResult::Failed, CheckResult::Failed) => CheckResult::Failed,
40            _ => CheckResult::Unknown,
41        }
42    }
43}
44
45/// Result for one required property along one path to a checkpoint.
46#[derive(Clone, Debug)]
47pub struct PropertyCheckResult<'tcx> {
48    /// Unsafe checkpoint being checked.
49    pub checkpoint: CheckpointLocation,
50    /// Index of the checkpoint in the function-level checkpoint list.
51    pub checkpoint_index: usize,
52    /// Index of the path in the checkpoint path set.
53    pub path_index: usize,
54    /// Index of the property in the checkpoint-level property list.
55    pub property_index: usize,
56    /// Required property checked on this path.
57    pub property: Property<'tcx>,
58    /// Current verification status.
59    pub result: CheckResult,
60    /// Optional path-local diagnostic message generated by the verifier.
61    pub diagnostics: Option<String>,
62    /// Human-readable path description.
63    pub path_description: String,
64    /// Callee name for this checkpoint.
65    pub callee_name: String,
66}
67
68/// Verification report for one function target.
69#[derive(Clone, Debug)]
70pub struct VerificationReport<'tcx> {
71    /// Function that was verified.
72    pub function: DefId,
73    /// Per-path property results emitted by the verifier.
74    pub results: Vec<PropertyCheckResult<'tcx>>,
75}
76
77impl<'tcx> VerificationReport<'tcx> {
78    /// Create an empty report for a function target.
79    pub fn new(function: DefId) -> Self {
80        Self {
81            function,
82            results: Vec::new(),
83        }
84    }
85
86    /// Add one path/property check result to this report.
87    pub fn push(&mut self, result: PropertyCheckResult<'tcx>) {
88        self.results.push(result);
89    }
90
91    /// Return the number of check results in this report.
92    pub fn len(&self) -> usize {
93        self.results.len()
94    }
95
96    /// Return true when this report contains no check results.
97    pub fn is_empty(&self) -> bool {
98        self.results.is_empty()
99    }
100
101    /// Render the whole report as a readable multi-line diagnostic.
102    pub fn describe(&self) -> String {
103        let mut out = String::new();
104        out.push_str(&format!(
105            "[rapx::verify::diagnostics] function {:?}: {} check item(s)\n",
106            self.function,
107            self.results.len()
108        ));
109
110        for (index, result) in self.results.iter().enumerate() {
111            out.push_str(&format!(
112                "  check #{index}: checkpoint #{}, bb{}, path #{}, property #{} {:?}, result {:?}\n",
113                result.checkpoint_index,
114                result.checkpoint.block.as_usize(),
115                result.path_index,
116                result.property_index,
117                result.property.kind(),
118                result.result
119            ));
120
121            if let Some(diagnostics) = &result.diagnostics {
122                out.push_str(diagnostics);
123                if !diagnostics.ends_with('\n') {
124                    out.push('\n');
125                }
126            }
127        }
128
129        out
130    }
131}
rapx/verify/report.rs

rapx/verify/
report.rs
