rapx/verify/smt_check/
align.rs

1//! SMT lowering for the `Align` safety property.
2//!
3//! This module reduces:
4//!
5//! ```text
6//! Align(p, T)
7//! ```
8//!
9//! to the common SMT obligation:
10//!
11//! ```text
12//! Aligned { place: p, align: align_of(T) }
13//! ```
14//!
15//! The common model then proves the obligation by asking whether the path facts
16//! plus the negated alignment goal are satisfiable.
17
18use super::common::{SmtCheckResult, SmtChecker, SmtObligation};
19use crate::verify::{contract::Property, helpers::Checkpoint, verifier::ForwardVisitResult};
20
21/// Check `Align` by lowering it to `SmtObligation::Aligned`.
22pub(crate) fn check<'tcx>(
23    checker: &SmtChecker<'tcx>,
24    checkpoint: &Checkpoint<'tcx>,
25    property: &Property<'tcx>,
26    forward: &ForwardVisitResult<'tcx>,
27) -> SmtCheckResult {
28    if checkpoint.is_ref {
29        return SmtCheckResult::proved("Align trivially holds for ref-derived pointer");
30    }
31    let Some(target) = checker.property_target(checkpoint, property) else {
32        return SmtCheckResult::unknown("SMT Align target could not be resolved");
33    };
34    let Some(required_ty) = checker.property_required_ty(checkpoint, property) else {
35        return SmtCheckResult::unknown("SMT Align type could not be resolved");
36    };
37    let Some(required_align) = checker.required_alignment(checkpoint.caller, required_ty) else {
38        return SmtCheckResult::unknown(format!(
39            "SMT Align layout unavailable for {:?}",
40            required_ty
41        ));
42    };
43
44    let obligation = SmtObligation::Aligned {
45        place: target,
46        align: required_align,
47        ty_name: format!("{required_ty:?}"),
48    };
49    checker.prove_obligation(checkpoint, forward, obligation)
50}
51
52/// Check `Align` at a return checkpoint for struct invariant verification.
53pub(crate) fn check_for_checkpoint<'tcx>(
54    checker: &SmtChecker<'tcx>,
55    caller: rustc_hir::def_id::DefId,
56    property: &Property<'tcx>,
57    forward: &ForwardVisitResult<'tcx>,
58) -> SmtCheckResult {
59    let Some(target) = checker.property_target_direct(property) else {
60        return SmtCheckResult::unknown("SMT Align target could not be resolved");
61    };
62    let Some(required_ty) = checker.property_required_ty_direct(property) else {
63        return SmtCheckResult::unknown("SMT Align type could not be resolved");
64    };
65    let required_align = checker
66        .required_alignment(caller, required_ty)
67        .or_else(|| {
68            checker
69                .type_layout(caller, required_ty)
70                .map(|(align, _)| align)
71        })
72        .unwrap_or(0);
73
74    let obligation = SmtObligation::Aligned {
75        place: target,
76        align: required_align,
77        ty_name: format!("{required_ty:?}"),
78    };
79    checker.prove_obligation_for_checkpoint(caller, forward, obligation)
80}
rapx/verify/smt_check/align.rs

rapx/verify/smt_check/
align.rs
