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
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

//! SMT lowering for the `NonOverlap` safety property.
//!
//! `NonOverlap(a, b)` is mostly used by copy/swap-style unsafe APIs.  The
//! contract tells us which pointer arguments must be disjoint; the element count
//! usually comes from the call itself, e.g. `copy_nonoverlapping(src, dst,
//! count)`.

use super::common::{SmtCheckResult, SmtChecker, SmtObligation, SmtTerm};
use crate::verify::{
    contract::Property, def_use::PlaceKey, helpers::Checkpoint, verifier::ForwardVisitResult,
};
use rustc_middle::mir::{Operand, Rvalue, StatementKind};

/// Check `NonOverlap` by lowering two pointer ranges to a common SMT obligation.
pub(crate) fn check<'tcx>(
    checker: &SmtChecker<'tcx>,
    checkpoint: &Checkpoint<'tcx>,
    property: &Property<'tcx>,
    forward: &ForwardVisitResult<'tcx>,
) -> SmtCheckResult {
    let Some(left) = checker.property_place_arg(checkpoint, property, 0) else {
        return SmtCheckResult::unknown("NonOverlap left pointer could not be resolved");
    };
    let Some(right) = checker.property_place_arg(checkpoint, property, 1) else {
        return SmtCheckResult::unknown("NonOverlap right pointer could not be resolved");
    };
    let left = resolve_callsite_copy(checker, checkpoint, left);
    let right = resolve_callsite_copy(checker, checkpoint, right);

    let count = property
        .args
        .get(2)
        .and_then(|_| checker.property_len_expr(checkpoint, property))
        .and_then(|expr| checker.contract_expr_to_smt_term(checkpoint.caller, &expr))
        .or_else(|| checker.callsite_arg_smt_term(checkpoint, 2))
        .unwrap_or(SmtTerm::Const(1));

    let elem_size = checker
        .place_pointee_size(checkpoint.caller, &left)
        .or_else(|| checker.place_pointee_size(checkpoint.caller, &right))
        .unwrap_or(1);

    checker.prove_obligation(
        checkpoint,
        forward,
        SmtObligation::NonOverlapping {
            left,
            right,
            left_count: count.clone(),
            right_count: count,
            elem_size,
        },
    )
}

fn resolve_callsite_copy<'tcx>(
    checker: &SmtChecker<'tcx>,
    checkpoint: &Checkpoint<'tcx>,
    mut place: PlaceKey,
) -> PlaceKey {
    for _ in 0..8 {
        if !place.fields.is_empty() {
            return place;
        }
        let Some(local) = place.local() else {
            return place;
        };
        let body = checker.tcx.optimized_mir(checkpoint.caller);
        let block = &body.basic_blocks[checkpoint.block];
        let source = block
            .statements
            .iter()
            .rev()
            .find_map(|statement| assignment_source_for_local(statement, local))
            .or_else(|| {
                body.basic_blocks.iter().rev().find_map(|block| {
                    block
                        .statements
                        .iter()
                        .rev()
                        .find_map(|statement| assignment_source_for_local(statement, local))
                })
            });
        let Some(source) = source else {
            return place;
        };
        let next = PlaceKey::from_mir_place(source);
        if next == place {
            return place;
        }
        place = next;
    }
    place
}

fn assignment_source_for_local<'a, 'tcx>(
    statement: &'a rustc_middle::mir::Statement<'tcx>,
    local: rustc_middle::mir::Local,
) -> Option<&'a rustc_middle::mir::Place<'tcx>> {
    let StatementKind::Assign(assign) = &statement.kind else {
        return None;
    };
    let (target, rvalue) = assign.as_ref();
    if target.local != local {
        return None;
    }
    rvalue_source_place(rvalue)
}

fn rvalue_source_place<'a, 'tcx>(
    rvalue: &'a Rvalue<'tcx>,
) -> Option<&'a rustc_middle::mir::Place<'tcx>> {
    match rvalue {
        Rvalue::Use(Operand::Copy(place), ..)
        | Rvalue::Use(Operand::Move(place), ..)
        | Rvalue::Cast(_, Operand::Copy(place), _)
        | Rvalue::Cast(_, Operand::Move(place), _)
        | Rvalue::CopyForDeref(place) => Some(place),
        _ => None,
    }
}