rapx 0.7.20

A static analysis platform for Rust program analysis and verification
Documentation 
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

//! 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},
    deref,
};
use crate::verify::{
    contract::{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(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 = primitive_property(property, PropertyKind::Deref);
            let deref = deref::check(checker, 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 => {
                    SmtCheckResult::unknown("ValidPtr unknown: non-ZST Deref is not proved")
                }
            }
            .with_note(format!("primitive Deref via SMT: {:?}", deref.result))
        }
        TypeSizeClass::Unknown => {
            let deref_property = primitive_property(property, PropertyKind::Deref);
            let deref = deref::check(checker, 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))
        }
    }
}

/// Reuse the original arguments while checking one primitive component.
fn primitive_property<'tcx>(property: &Property<'tcx>, kind: PropertyKind) -> Property<'tcx> {
    Property {
        kind,
        args: property.args.clone(),
    }
}