rapx/verify/smt_check/
init.rs

1//! SMT lowering for the `Init` safety property.
2//!
3//! This first version proves only a local one-element write pattern:
4//!
5//! ```text
6//! ptr.write(value)
7//! require Init(ptr, T, 1)
8//! ```
9//!
10//! Forward visit records `ptr.write` as a `KnownInit` fact.  The common SMT
11//! backend then checks whether the Init target has the same address as a known
12//! initialized pointer.  Range initialization across loops still needs a loop
13//! summary and is intentionally left as `Unknown`.
14
15use super::common::{SmtCheckResult, SmtChecker, SmtObligation, SmtTerm};
16
17use crate::verify::{contract::Property, helpers::Checkpoint, verifier::ForwardVisitResult};
18use rustc_middle::ty::{Ty, TyKind};
19
20/// Check `Init` by lowering it to a common initialized-memory obligation.
21pub(crate) fn check<'tcx>(
22    checker: &SmtChecker<'tcx>,
23    checkpoint: &Checkpoint<'tcx>,
24    property: &Property<'tcx>,
25    forward: &ForwardVisitResult<'tcx>,
26) -> SmtCheckResult {
27    let Some(target) = checker.property_target(checkpoint, property) else {
28        return SmtCheckResult::unknown("Init target could not be resolved");
29    };
30    let Some(required_ty) = checker.property_required_ty(checkpoint, property) else {
31        return SmtCheckResult::unknown("Init type could not be resolved");
32    };
33    let Some(elements_expr) = checker.property_len_expr(checkpoint, property) else {
34        return SmtCheckResult::unknown("Init element-count argument could not be resolved");
35    };
36    let Some(elements_term) = checker.contract_expr_to_smt_term(checkpoint.caller, &elements_expr)
37    else {
38        return SmtCheckResult::unknown("Init element-count argument could not be lowered to SMT");
39    };
40
41    let elem_size = compute_elem_size(checker, checkpoint.caller, required_ty);
42
43    checker.prove_obligation(
44        checkpoint,
45        forward,
46        SmtObligation::Initialized {
47            place: target,
48            ty_name: format!("{required_ty:?}"),
49            elements: elements_term,
50            elem_size,
51            array_elem_size: array_elem_size(checker, checkpoint.caller, required_ty),
52            array_len_term: array_len_term(checker, required_ty),
53        },
54    )
55}
56
57fn compute_elem_size<'tcx>(
58    checker: &SmtChecker<'tcx>,
59    caller: rustc_hir::def_id::DefId,
60    ty: Ty<'tcx>,
61) -> Option<u64> {
62    if let Some((_, size)) = checker.type_layout(caller, ty) {
63        return Some(size);
64    }
65    None
66}
67
68fn array_elem_size<'tcx>(
69    checker: &SmtChecker<'tcx>,
70    caller: rustc_hir::def_id::DefId,
71    ty: Ty<'tcx>,
72) -> Option<u64> {
73    if let TyKind::Array(elem, _) = ty.kind() {
74        checker.type_layout(caller, *elem).map(|(_, s)| s)
75    } else {
76        None
77    }
78}
79
80fn array_len_term<'tcx>(
81    checker: &SmtChecker<'tcx>,
82    ty: Ty<'tcx>,
83) -> Option<SmtTerm> {
84    use rustc_middle::ty::ConstKind;
85    if let TyKind::Array(_, len) = ty.kind() {
86        if let Some(val) = len.try_to_target_usize(checker.tcx) {
87            return Some(SmtTerm::Const(val));
88        }
89        if let ConstKind::Param(param) = len.kind() {
90            return Some(SmtTerm::ConstParam(param.name.to_string()));
91        }
92        Some(SmtTerm::ConstParam(format!("Ty(usize, {len})")))
93    } else {
94        None
95    }
96}
97
98/// Check `Init` at a return checkpoint for struct invariant verification.
99pub(crate) fn check_for_checkpoint<'tcx>(
100    checker: &SmtChecker<'tcx>,
101    caller: rustc_hir::def_id::DefId,
102    property: &Property<'tcx>,
103    forward: &ForwardVisitResult<'tcx>,
104) -> SmtCheckResult {
105    let Some(target) = checker.property_target_direct(property) else {
106        return SmtCheckResult::unknown("Init target could not be resolved");
107    };
108    let Some(required_ty) = checker.property_required_ty_direct(property) else {
109        return SmtCheckResult::unknown("Init type could not be resolved");
110    };
111    let Some(elements_expr) = checker.property_len_expr_direct(property) else {
112        return SmtCheckResult::unknown("Init element-count argument could not be resolved");
113    };
114    let Some(elements) = checker.contract_expr_to_smt_term(caller, &elements_expr) else {
115        return SmtCheckResult::unknown("Init element-count argument could not be lowered to SMT");
116    };
117
118    checker.prove_obligation_for_checkpoint(
119        caller,
120        forward,
121        SmtObligation::Initialized {
122            place: target,
123            ty_name: format!("{required_ty:?}"),
124            elements,
125            elem_size: compute_elem_size(checker, caller, required_ty),
126            array_elem_size: array_elem_size(checker, caller, required_ty),
127            array_len_term: array_len_term(checker, required_ty),
128        },
129    )
130}
rapx/verify/smt_check/init.rs

rapx/verify/smt_check/
init.rs
