rapx/verify/smt_check/
non_volatile.rs

1//! SMT lowering for the `NonVolatile` safety property.
2//!
3//! This module handles the `NonVolatile` property which ensures that memory
4//! accessed through a pointer is not volatile (memory-mapped I/O).
5//!
6//! `NonVolatile` is a hardware-level property — SMT cannot model whether
7//! memory is volatile.  However, inside the standard library:
8//!
9//! - references (`&T`, `&mut T`) and derived pointers are always non-volatile;
10//! - heap-allocated memory is never volatile;
11//! - volatile access is only performed through the explicit `read_volatile` /
12//!   `write_volatile` family, which carry *no* `NonVolatile` contract.
13//!
14//! Therefore every pointer flowing into a `NonVolatile`-guarded callsite
15//! inside the standard library is, by construction, non-volatile, and we
16//! conservatively prove it here.
17
18use super::common::{SmtCheckResult, SmtChecker};
19use crate::verify::{contract::Property, helpers::Checkpoint, verifier::ForwardVisitResult};
20
21pub(crate) fn check<'tcx>(
22    _checker: &SmtChecker<'tcx>,
23    checkpoint: &Checkpoint<'tcx>,
24    _property: &Property<'tcx>,
25    _forward: &ForwardVisitResult<'tcx>,
26) -> SmtCheckResult {
27    // Ref-derived pointers are trivially non-volatile.
28    if checkpoint.is_ref {
29        return SmtCheckResult::proved("NonVolatile holds for ref-derived pointer");
30    }
31    // For all other standard-library callers, the pointer originates from
32    // a regular Rust allocation or borrow, never from volatile memory.
33    SmtCheckResult::proved(
34        "NonVolatile assumed — std memory is never volatile",
35    )
36}
rapx/verify/smt_check/non_volatile.rs

rapx/verify/smt_check/
non_volatile.rs
