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
122
123
124
125
126
127
128
129
130
131
//! 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 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 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 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 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 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 fn new(function: DefId) -> Self {
Self {
function,
results: Vec::new(),
}
}
/// Add one path/property check result to this report.
pub fn push(&mut self, result: PropertyCheckResult<'tcx>) {
self.results.push(result);
}
/// Return the number of check results in this report.
pub fn len(&self) -> usize {
self.results.len()
}
/// Return true when this report contains no check results.
pub fn is_empty(&self) -> bool {
self.results.is_empty()
}
/// Render the whole report as a readable multi-line diagnostic.
pub 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
}
}