rapx 0.7.28

A static analysis platform for Rust program analysis and verification
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129

//! SMT lowering for the `Ptr2Ref` safety property.
//!
//! Per `contract/decomp.rs`, the spec decomposition is:
//!
//! ```text
//! Ptr2Ref(p, T) = Init(p, T, 1) && Align(p, T) && Alias(p, ret)
//! ```
//!
//! Currently only `NonNull` and `Align` are checked via SMT.  `Init` and
//! `Alias` require richer provenance and element-count tracking and are
//! deferred to future implementation.

use super::common::{SmtCheckResult, SmtChecker, SmtObligation, place_label};
use crate::verify::{
    contract::Property, helpers::Checkpoint, report::CheckResult, verifier::ForwardVisitResult,
};

pub(crate) fn check<'tcx>(
    checker: &SmtChecker<'tcx>,
    checkpoint: &Checkpoint<'tcx>,
    property: &Property<'tcx>,
    forward: &ForwardVisitResult<'tcx>,
) -> SmtCheckResult {
    // For NonNull::as_mut / NonNull::as_ref, the callee's self parameter type
    // is NonNull<T> whose inner pointer is guaranteed non-null and properly
    // aligned (NonNull can only be constructed from a valid, aligned pointer).
    if let Some(callee) = checkpoint.callee {
        let callee_path = checker.tcx.def_path_str(callee);
        if callee_path.contains("NonNull::as_ref") || callee_path.contains("NonNull::as_mut") {
            return SmtCheckResult::proved(
                "Ptr2Ref proved: NonNull guarantees valid pointer-to-ref conversion",
            );
        }
    }

    let Some(target) = checker.property_target(Some(checkpoint), property) else {
        return SmtCheckResult::unknown("Ptr2Ref target could not be resolved");
    };

    let target_label = place_label(&target);

    let nonnull_result = checker.prove_obligation(
        checkpoint,
        forward,
        SmtObligation::NonZero {
            place: target.clone(),
        },
        property.null_guard.as_ref(),
    );

    let Some(pointee_ty) = checker.infer_pointee_ty(checkpoint.caller, &target) else {
        return match &nonnull_result.result {
            CheckResult::Proved => SmtCheckResult::proved(
                "Ptr2Ref: NonNull proved, alignment skipped (no pointee type)",
            ),
            CheckResult::Failed => SmtCheckResult {
                result: CheckResult::Failed,
                query: None,
                notes: vec![
                    "Ptr2Ref failed: pointer is null (no pointee type to check alignment)"
                        .to_string(),
                ],
            },
            CheckResult::Unknown => {
                SmtCheckResult::unknown("Ptr2Ref: could not infer pointee type for alignment check")
            }
        }
        .with_note("Ptr2Ref alignment check skipped: could not infer pointee type");
    };

    let Some(required_align) = checker.required_alignment(checkpoint.caller, pointee_ty) else {
        return match &nonnull_result.result {
            CheckResult::Proved => SmtCheckResult::proved(format!(
                "Ptr2Ref: NonNull proved, alignment skipped (layout unavailable for {pointee_ty:?})",
            )),
            CheckResult::Failed => SmtCheckResult {
                result: CheckResult::Failed,
                query: None,
                notes: vec![format!(
                    "Ptr2Ref failed: pointer is null (layout unavailable for {pointee_ty:?})"
                )],
            },
            CheckResult::Unknown => SmtCheckResult::unknown(format!(
                "Ptr2Ref: could not determine alignment for {pointee_ty:?}"
            )),
        };
    };

    let align_result = checker.prove_obligation(
        checkpoint,
        forward,
        SmtObligation::Aligned {
            place: target.clone(),
            align: required_align,
            ty_name: format!("{pointee_ty:?}"),
        },
        property.null_guard.as_ref(),
    );

    match (&nonnull_result.result, &align_result.result) {
        (CheckResult::Proved, CheckResult::Proved) => SmtCheckResult::proved(format!(
            "Ptr2Ref proved: {target_label} is non-null and {required_align}-byte aligned for {pointee_ty:?}",
        ))
        .with_note("Ptr2Ref: NonNull + Align both proved"),
        (CheckResult::Failed, _) => SmtCheckResult {
            result: CheckResult::Failed,
            query: None,
            notes: vec![format!(
                "Ptr2Ref failed: pointer {target_label} is not provably non-null"
            )],
        },
        (_, CheckResult::Failed) => SmtCheckResult {
            result: CheckResult::Failed,
            query: None,
            notes: vec![format!(
                "Ptr2Ref failed: pointer {target_label} is not {required_align}-byte aligned for {pointee_ty:?}",
            )],
        },
        (CheckResult::Proved, CheckResult::Unknown) => SmtCheckResult::unknown(format!(
            "Ptr2Ref: NonNull proved for {target_label}, but alignment ({required_align}-byte for {pointee_ty:?}) is unproven",
        )),
        (CheckResult::Unknown, CheckResult::Proved) => SmtCheckResult::unknown(format!(
            "Ptr2Ref: alignment proved for {target_label}, but non-null is unproven",
        )),
        _ => SmtCheckResult::unknown(format!(
            "Ptr2Ref: could not prove non-null nor alignment for {target_label}"
        )),
    }
}