rapx/verify/smt_check/
valid_ptr.rs

1//! SMT lowering for the composite `ValidPtr` safety property.
2//!
3//! `ValidPtr(p, T, n)` is not a primitive SMT obligation.  The verifier reduces
4//! it to the pointer-validity formula used by the staged SMT checker:
5//!
6//! ```text
7//! ValidPtr(p, T, n) =
8//!   Size(T, 0) || (!Size(T, 0) && Deref(p, T, n))
9//!
10//! Deref(p, T, n) =
11//!   Allocated(p, T, n, *) && InBound(p, T, n)
12//! ```
13//!
14//! Zero-sized types do not require an allocated dereferenceable range.  For
15//! non-ZSTs, `ValidPtr` delegates to the `Deref` composite checker.
16
17use super::{
18    common::{SmtCheckResult, SmtChecker, TypeSizeClass},
19    deref,
20};
21use crate::verify::{
22    contract::{Property, PropertyKind},
23    helpers::Checkpoint,
24    report::CheckResult,
25    verifier::ForwardVisitResult,
26};
27
28/// Check `ValidPtr` using `Size(T,0) || (!Size(T,0) && Deref(p,T,n))`.
29pub(crate) fn check<'tcx>(
30    checker: &SmtChecker<'tcx>,
31    checkpoint: &Checkpoint<'tcx>,
32    property: &Property<'tcx>,
33    forward: &ForwardVisitResult<'tcx>,
34) -> SmtCheckResult {
35    let Some(required_ty) = checker.property_required_ty(checkpoint, property) else {
36        return SmtCheckResult::unknown("ValidPtr type could not be resolved");
37    };
38
39    match checker.type_size_class(checkpoint.caller, required_ty) {
40        TypeSizeClass::Zero => {
41            SmtCheckResult::proved(format!("ValidPtr proved by Size({required_ty:?}, 0)"))
42        }
43        TypeSizeClass::NonZero => {
44            let deref_property = primitive_property(property, PropertyKind::Deref);
45            let deref = deref::check(checker, checkpoint, &deref_property, forward);
46            match &deref.result {
47                CheckResult::Proved => {
48                    SmtCheckResult::proved("ValidPtr proved: non-ZST target satisfies Deref")
49                }
50                CheckResult::Failed => SmtCheckResult {
51                    result: CheckResult::Failed,
52                    query: None,
53                    notes: vec![String::from(
54                        "ValidPtr failed: non-ZST target does not satisfy Deref",
55                    )],
56                },
57                CheckResult::Unknown => {
58                    SmtCheckResult::unknown("ValidPtr unknown: non-ZST Deref is not proved")
59                }
60            }
61            .with_note(format!("primitive Deref via SMT: {:?}", deref.result))
62        }
63        TypeSizeClass::Unknown => {
64            let deref_property = primitive_property(property, PropertyKind::Deref);
65            let deref = deref::check(checker, checkpoint, &deref_property, forward);
66            match &deref.result {
67                CheckResult::Proved => SmtCheckResult::proved(
68                    "ValidPtr proved: Deref holds, so the formula holds for zero and non-zero sizes",
69                ),
70                CheckResult::Failed | CheckResult::Unknown => SmtCheckResult::unknown(
71                    "ValidPtr unknown: type size is unresolved and Deref is not proved",
72                ),
73            }
74            .with_note("type size: Unknown")
75            .with_note(format!("primitive Deref via SMT: {:?}", deref.result))
76        }
77    }
78}
79
80/// Reuse the original arguments while checking one primitive component.
81fn primitive_property<'tcx>(property: &Property<'tcx>, kind: PropertyKind) -> Property<'tcx> {
82    Property {
83        kind,
84        args: property.args.clone(),
85    }
86}
rapx/verify/smt_check/valid_ptr.rs

rapx/verify/smt_check/
valid_ptr.rs
