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

//! SMT lowering for the `Allocated` safety property.
//!
//! `Allocated(p, T, n)` means the whole `n`-element range starting at `p`
//! belongs to a single live allocation object.  The lowering is intentionally
//! object-sensitive: adjacent stack locals do not form one larger allocation
//! even when their addresses happen to be close.

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

/// Check `Allocated` by lowering it to a common allocation obligation.
pub(crate) fn check<'tcx>(
    checker: &SmtChecker<'tcx>,
    checkpoint: &Checkpoint<'tcx>,
    property: &Property<'tcx>,
    forward: &ForwardVisitResult<'tcx>,
) -> SmtCheckResult {
    if let Some(reason) = super::field_invariant::discharge_from_contract_fact_with_checkpoint(property, forward, checkpoint) {
        return SmtCheckResult::proved(format!("Allocated proved: {reason}"));
    }

    let Some(target) = checker.property_target(Some(checkpoint), property) else {
        return SmtCheckResult::unknown("Allocated target could not be resolved");
    };
    if checker.property_required_ty(Some(checkpoint), property).is_none()
        && checker.property_len_expr(Some(checkpoint), property).is_none()
    {
        if checker.is_len_carrying_place_for_caller(checkpoint.caller, &target) {
            return SmtCheckResult::proved(
                "allocation proved: safe slice/reference target carries one live allocation object",
            );
        }
        return SmtCheckResult::unknown(
            "Allocated target has no type/count arguments and is not a supported slice/reference",
        );
    }
    let Some(required_ty) = checker.property_required_ty(Some(checkpoint), property) else {
        return SmtCheckResult::unknown("Allocated type could not be resolved");
    };
    let Some(elements_expr) = checker.property_len_expr(Some(checkpoint), property) else {
        return SmtCheckResult::unknown("Allocated element-count argument could not be resolved");
    };
    let Some(elements) = checker.contract_expr_to_smt_term(checkpoint.caller, &elements_expr, None)
    else {
        return SmtCheckResult::unknown(
            "Allocated element-count argument could not be lowered to SMT",
        );
    };

    if let Some(reason) = super::provenance::vec_from_raw_parts_roundtrip(checker, checkpoint) {
        return SmtCheckResult::proved(format!("Allocated proved: {reason}"));
    }

    let result = checker.prove_obligation(
        checkpoint,
        forward,
        SmtObligation::Allocated {
            place: target.clone(),
            ty_name: format!("{required_ty:?}"),
            elements: elements.clone(),
        },
        property.null_guard.as_ref(),
    );
    if matches!(result.result, crate::verify::report::CheckResult::Proved) {
        return result;
    }

    let required_elements = match elements {
        super::common::SmtTerm::Const(value) => Some(value),
        _ => None,
    };
    if let Some(reason) = super::field_invariant::discharge_from_field_invariant(
        checker.tcx,
        checkpoint.caller,
        &target,
        forward,
        crate::verify::contract::PropertyKind::Allocated,
        Some(required_ty),
        required_elements,
    ) {
        return SmtCheckResult::proved(format!("Allocated proved: {reason}"));
    }

    result
}

/// Check `Allocated` 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("Allocated target could not be resolved");
    };
    let Some(required_ty) = checker.property_required_ty(None, property) else {
        return SmtCheckResult::unknown("Allocated type could not be resolved");
    };
    let Some(elements_expr) = checker.property_len_expr(None, property) else {
        return SmtCheckResult::unknown("Allocated element-count argument could not be resolved");
    };
    let Some(elements) = checker.contract_expr_to_smt_term(caller, &elements_expr, None) else {
        return SmtCheckResult::unknown(
            "Allocated element-count argument could not be lowered to SMT",
        );
    };
    let result = checker.prove_obligation_for_checkpoint(
        caller,
        forward,
        SmtObligation::Allocated {
            place: target,
            ty_name: format!("{required_ty:?}"),
            elements,
        },
    );
    if matches!(result.result, crate::verify::report::CheckResult::Proved) {
        return result;
    }
    if let Some(reason) = super::field_invariant::discharge_from_contract_fact(property, forward) {
        return SmtCheckResult::proved(format!("Allocated proved: {reason}"));
    }
    result
}