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
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
//! 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 {
/// Proved by a *sound structural rule* (a fast-path that needs no solver
/// query): ZST guards, zero-element access, tracked invariants/flags,
/// type-level transparency, provenance-origin classification. These are
/// the rules that must be audited for soundness.
ProvedByRule,
/// Proved by an *SMT query*: the solver showed the negation is unsatisfiable
/// (numeric bounds, byte-range coverage, alignment modulo/linear checks).
ProvedBySmt,
/// 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 {
/// Whether this result counts as "proved" (by rule or by SMT).
pub(crate) fn is_proved(&self) -> bool {
matches!(self, CheckResult::ProvedByRule | CheckResult::ProvedBySmt)
}
/// The user-facing label for this result. `ProvedByRule` and `ProvedBySmt`
/// both report as `"Proved"` — the rule/SMT distinction is an internal
/// audit signal, not part of the report.
pub(crate) fn label(&self) -> &'static str {
match self {
CheckResult::ProvedByRule | CheckResult::ProvedBySmt => "Proved",
CheckResult::Failed => "Failed",
CheckResult::Unknown => "Unknown",
}
}
/// AND-combine two results: any `Failed` → `Failed`; any `Unknown` →
/// `Unknown`; only all-proved → proved (`Rule` when every conjunct was a
/// rule, otherwise `Smt`).
pub(crate) fn and(self, other: CheckResult) -> CheckResult {
match (self, other) {
(CheckResult::Failed, _) | (_, CheckResult::Failed) => CheckResult::Failed,
(CheckResult::Unknown, _) | (_, CheckResult::Unknown) => CheckResult::Unknown,
(CheckResult::ProvedByRule, CheckResult::ProvedByRule) => CheckResult::ProvedByRule,
_ => CheckResult::ProvedBySmt,
}
}
/// OR-combine two results: any proved → proved (a `Rule` proof dominates);
/// all `Failed` → `Failed`; otherwise `Unknown`.
pub(crate) fn or(self, other: CheckResult) -> CheckResult {
match (self, other) {
(CheckResult::ProvedByRule, _) | (_, CheckResult::ProvedByRule) => {
CheckResult::ProvedByRule
}
(CheckResult::ProvedBySmt, _) | (_, CheckResult::ProvedBySmt) => {
CheckResult::ProvedBySmt
}
(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.label()
));
if let Some(diagnostics) = &result.diagnostics {
out.push_str(diagnostics);
if !diagnostics.ends_with('\n') {
out.push('\n');
}
}
}
out
}
}