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

//! SMT lowering for the composite `ValidPtr` safety property.
//!
//! `ValidPtr(p, T, n)` is not a primitive SMT obligation.  The verifier reduces
//! it to the pointer-validity formula used by the staged SMT checker:
//!
//! ```text
//! ValidPtr(p, T, n) =
//!   Size(T, 0) || (!Size(T, 0) && Deref(p, T, n))
//!
//! Deref(p, T, n) =
//!   Allocated(p, T, n, *) && InBound(p, T, n)
//! ```
//!
//! Zero-sized types do not require an allocated dereferenceable range.  For
//! non-ZSTs, `ValidPtr` delegates to the `Deref` composite checker.

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

/// Check `ValidPtr` using `Size(T,0) || (!Size(T,0) && Deref(p,T,n))`.
pub(crate) fn check<'tcx>(
    checker: &SmtChecker<'tcx>,
    checkpoint: &Checkpoint<'tcx>,
    property: &Property<'tcx>,
    forward: &ForwardVisitResult<'tcx>,
) -> SmtCheckResult {
    let Some(required_ty) = checker.property_required_ty(Some(checkpoint), property) else {
        return SmtCheckResult::unknown("ValidPtr type could not be resolved");
    };

    match checker.type_size_class(checkpoint.caller, required_ty) {
        TypeSizeClass::Zero => {
            SmtCheckResult::proved(format!("ValidPtr proved by Size({required_ty:?}, 0)"))
        }
        TypeSizeClass::NonZero => {
            let deref_property = contract::decomp::with_kind(property, PropertyKind::Deref);
            let deref = checker.check(checkpoint, &deref_property, forward);
            match &deref.result {
                CheckResult::Proved => {
                    SmtCheckResult::proved("ValidPtr proved: non-ZST target satisfies Deref")
                }
                CheckResult::Failed => SmtCheckResult {
                    result: CheckResult::Failed,
                    query: None,
                    notes: vec![String::from(
                        "ValidPtr failed: non-ZST target does not satisfy Deref",
                    )],
                },
                CheckResult::Unknown => {
                    if let Some(reason) = super::provenance::pedigree_proof(
                        checker, checkpoint, property, forward, true,
                    ) {
                        SmtCheckResult::proved(format!("ValidPtr proved: {reason}"))
                    } else if let Some(reason) = super::field_invariant::discharge_from_contract_fact_with_checkpoint(property, forward, checkpoint) {
                        SmtCheckResult::proved(format!("ValidPtr proved: {reason}"))
                    } else if let Some(reason) =
                        field_invariant_reason(checker, checkpoint, property, forward, required_ty)
                    {
                        SmtCheckResult::proved(format!("ValidPtr proved: {reason}"))
                    } else {
                        SmtCheckResult::unknown("ValidPtr unknown: non-ZST Deref is not proved")
                    }
                }
            }
            .with_note(format!("primitive Deref via SMT: {:?}", deref.result))
        }
        TypeSizeClass::Unknown => {
            let deref_property = contract::decomp::with_kind(property, PropertyKind::Deref);
            let deref = checker.check(checkpoint, &deref_property, forward);
            match &deref.result {
                CheckResult::Proved => SmtCheckResult::proved(
                    "ValidPtr proved: Deref holds, so the formula holds for zero and non-zero sizes",
                ),
                CheckResult::Failed | CheckResult::Unknown => SmtCheckResult::unknown(
                    "ValidPtr unknown: type size is unresolved and Deref is not proved",
                ),
            }
            .with_note("type size: Unknown")
            .with_note(format!("primitive Deref via SMT: {:?}", deref.result))
        }
    }
}

/// Try to discharge `ValidPtr` from a struct field invariant covering the
/// dereferenced pointer (same field path, type, and element count).
fn field_invariant_reason<'tcx>(
    checker: &SmtChecker<'tcx>,
    checkpoint: &Checkpoint<'tcx>,
    property: &Property<'tcx>,
    forward: &ForwardVisitResult<'tcx>,
    required_ty: rustc_middle::ty::Ty<'tcx>,
) -> Option<String> {
    let target = checker.property_target(Some(checkpoint), property)?;
    let required_elements = checker
        .property_len_expr(Some(checkpoint), property)
        .and_then(|expr| match expr {
            crate::verify::contract::ContractExpr::Const(value) => u64::try_from(value).ok(),
            _ => None,
        });
    super::field_invariant::discharge_from_field_invariant(
        checker.tcx,
        checkpoint.caller,
        &target,
        forward,
        PropertyKind::ValidPtr,
        Some(required_ty),
        required_elements,
    )
}