rapx/verify/smt_check/
non_null.rs

1//! SMT lowering for the `NonNull` safety property.
2//!
3//! This module reduces:
4//!
5//! ```text
6//! NonNull(p)
7//! ```
8//!
9//! to the common SMT obligation:
10//!
11//! ```text
12//! NonZero { place: p }
13//! ```
14//!
15//! The common model asserts path-local facts such as reference-derived pointers
16//! and `as_ptr` results as non-zero assumptions, then asks whether the target can
17//! still be zero.
18
19use super::common::{SmtCheckResult, SmtChecker, SmtObligation};
20use crate::verify::{contract::Property, helpers::Checkpoint, verifier::ForwardVisitResult};
21
22/// Check `NonNull` by lowering it to `SmtObligation::NonZero`.
23pub(crate) fn check<'tcx>(
24    checker: &SmtChecker<'tcx>,
25    checkpoint: &Checkpoint<'tcx>,
26    property: &Property<'tcx>,
27    forward: &ForwardVisitResult<'tcx>,
28) -> SmtCheckResult {
29    if checkpoint.is_ref {
30        return SmtCheckResult::proved("NonNull trivially holds for ref-derived pointer");
31    }
32    let Some(target) = checker.property_target(checkpoint, property) else {
33        return SmtCheckResult::unknown("NonNull target could not be resolved");
34    };
35
36    let obligation = SmtObligation::NonZero { place: target };
37    checker.prove_obligation(checkpoint, forward, obligation)
38}
rapx/verify/smt_check/non_null.rs

rapx/verify/smt_check/
non_null.rs
