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

//! SMT lowering for the `NonNull` safety property.
//!
//! This module reduces:
//!
//! ```text
//! NonNull(p)
//! ```
//!
//! to the common SMT obligation:
//!
//! ```text
//! NonZero { place: p }
//! ```
//!
//! The common model asserts path-local facts such as reference-derived pointers
//! and `as_ptr` results as non-zero assumptions, then asks whether the target can
//! still be zero.

use rustc_middle::ty::{TyCtxt, TyKind};

use super::common::{SmtCheckResult, SmtChecker, SmtObligation};
use crate::verify::{
    contract::{ContractPlace, PlaceBase, Property, PropertyArg},
    helpers::Checkpoint,
    verifier::ForwardVisitResult,
};

fn is_nonnull_param_ty(tcx: TyCtxt<'_>, ty: rustc_middle::ty::Ty<'_>) -> bool {
    let peeled = ty.peel_refs();
    if let TyKind::Adt(def, _) = peeled.kind() {
        let path = tcx.def_path_str(def.did());
        if path.contains("ptr::non_null::NonNull") {
            return true;
        }
    }
    false
}

/// Check `NonNull` by lowering it to `SmtObligation::NonZero`.
pub(crate) fn check<'tcx>(
    checker: &SmtChecker<'tcx>,
    checkpoint: &Checkpoint<'tcx>,
    property: &Property<'tcx>,
    forward: &ForwardVisitResult<'tcx>,
) -> SmtCheckResult {
    if checkpoint.is_ref {
        return SmtCheckResult::proved("NonNull trivially holds for ref-derived pointer");
    }

    // If the target maps to a callee parameter whose type is NonNull<T>,
    // the pointer is guaranteed non-null by construction.
    if let Some(callee) = checkpoint.callee {
        if let Some(PropertyArg::Place(ContractPlace {
            base: PlaceBase::Arg(arg_index),
            ..
        })) = property.args.first()
        {
            let tcx = checker.tcx;
            let fn_sig = tcx.fn_sig(callee).skip_binder();
            let input_tys = fn_sig.inputs().skip_binder();
            if let Some(param_ty) = input_tys.get(*arg_index) {
                if is_nonnull_param_ty(tcx, *param_ty) {
                    return SmtCheckResult::proved(
                        "NonNull trivially holds: callee parameter type is NonNull<T>",
                    );
                }
            }
        }
    }

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

    let obligation = SmtObligation::NonZero { place: target };
    let result = checker.prove_obligation(
        checkpoint,
        forward,
        obligation,
        property.null_guard.as_ref(),
    );
    if result.result == crate::verify::report::CheckResult::Unknown {
        if let Some(reason) =
            super::provenance::pedigree_proof(checker, checkpoint, property, forward, false)
        {
            return SmtCheckResult::proved(format!("NonNull proved: {reason}"));
        }
    }
    result
}

/// Check `NonNull` at a return checkpoint for struct invariant verification.
pub(crate) fn check_for_checkpoint<'tcx>(
    checker: &SmtChecker<'tcx>,
    caller: rustc_hir::def_id::DefId,
    property: &Property<'tcx>,
    forward: &ForwardVisitResult<'tcx>,
) -> SmtCheckResult {
    let Some(target) = checker.property_target(None, property) else {
        return SmtCheckResult::unknown("SMT NonNull target could not be resolved");
    };
    let obligation = SmtObligation::NonZero { place: target };
    checker.prove_obligation_for_checkpoint(caller, forward, obligation)
}