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
//! 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, helpers::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,
}
/// 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 diagnostics generated by the staged visitors.
pub diagnostics: Option<VisitDiagnostics>,
/// Human-readable path description.
pub path_description: String,
/// Callee name for this checkpoint.
pub callee_name: String,
}
/// Human-readable diagnostics emitted for one path/property check.
#[derive(Clone, Debug)]
pub struct VisitDiagnostics {
/// Backward visit summary for relevant MIR items.
pub backward: String,
/// Forward visit summary for abstract facts collected from those items.
pub forward: String,
}
impl VisitDiagnostics {
/// Create diagnostics from backward and forward visitor summaries.
pub fn new(backward: String, forward: String) -> Self {
Self { backward, forward }
}
}
/// 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.backward);
if !diagnostics.backward.ends_with('\n') {
out.push('\n');
}
out.push_str(&diagnostics.forward);
if !diagnostics.forward.ends_with('\n') {
out.push('\n');
}
}
}
out
}
}