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