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
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
//! 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::verify::checkpoint::CheckpointLocation;
/// Why a [`CheckResult::Unknown`] could not be discharged.
///
/// Carried by the `Unknown` variant so the report can distinguish a solver
/// timeout (the common case under the fixed per-query budget) from a structural
/// "no rule for this shape" gap.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub(crate) enum UnknownReason {
/// The SMT solver returned `unknown` — with the fixed per-query timeout
/// this is effectively a timeout on a query it could not decide in time.
SmtTimeout,
/// The inline recursion limit was reached, so the callee's body was not
/// executed and the memory state is incomplete.
InlineDepthExceeded,
/// The checker has no rule for this shape (unsupported property, unannotated
/// callee, unresolvable operand, undecidable generic, …).
Unimplemented,
}
impl UnknownReason {
/// Merge two reasons, keeping the more diagnostic one.
fn merge(self, other: UnknownReason) -> UnknownReason {
match (self, other) {
(UnknownReason::SmtTimeout, _) | (_, UnknownReason::SmtTimeout) => {
UnknownReason::SmtTimeout
}
(UnknownReason::InlineDepthExceeded, _) | (_, UnknownReason::InlineDepthExceeded) => {
UnknownReason::InlineDepthExceeded
}
_ => UnknownReason::Unimplemented,
}
}
}
/// 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;
/// the reason is carried in the payload.
Unknown(UnknownReason),
}
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. An `Unknown` result is suffixed
/// with its reason when it is not the generic unimplemented case.
pub(crate) fn label(&self) -> &'static str {
match self {
CheckResult::ProvedByRule | CheckResult::ProvedBySmt => "Proved",
CheckResult::Failed => "Failed",
CheckResult::Unknown(UnknownReason::SmtTimeout) => "Unknown (timeout)",
CheckResult::Unknown(UnknownReason::InlineDepthExceeded) => {
"Unknown (inline depth)"
}
CheckResult::Unknown(UnknownReason::Unimplemented) => "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(a), CheckResult::Unknown(b)) => {
CheckResult::Unknown(a.merge(b))
}
(CheckResult::Unknown(a), _) | (_, CheckResult::Unknown(a)) => CheckResult::Unknown(a),
(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(a), CheckResult::Unknown(b)) => {
CheckResult::Unknown(a.merge(b))
}
(CheckResult::Unknown(a), _) | (_, CheckResult::Unknown(a)) => CheckResult::Unknown(a),
}
}
}
/// 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
}
}