rapx/verify/smt_check/
non_overlap.rs

1//! SMT lowering for the `NonOverlap` safety property.
2//!
3//! `NonOverlap(a, b)` is mostly used by copy/swap-style unsafe APIs.  The
4//! contract tells us which pointer arguments must be disjoint; the element count
5//! usually comes from the call itself, e.g. `copy_nonoverlapping(src, dst,
6//! count)`.
7
8use super::common::{SmtCheckResult, SmtChecker, SmtObligation, SmtTerm};
9use crate::verify::{
10    contract::Property, def_use::PlaceKey, helpers::Checkpoint, verifier::ForwardVisitResult,
11};
12use rustc_middle::mir::{Operand, Rvalue, StatementKind};
13
14/// Check `NonOverlap` by lowering two pointer ranges to a common SMT obligation.
15pub(crate) fn check<'tcx>(
16    checker: &SmtChecker<'tcx>,
17    checkpoint: &Checkpoint<'tcx>,
18    property: &Property<'tcx>,
19    forward: &ForwardVisitResult<'tcx>,
20) -> SmtCheckResult {
21    let Some(left) = checker.property_place_arg(checkpoint, property, 0) else {
22        return SmtCheckResult::unknown("NonOverlap left pointer could not be resolved");
23    };
24    let Some(right) = checker.property_place_arg(checkpoint, property, 1) else {
25        return SmtCheckResult::unknown("NonOverlap right pointer could not be resolved");
26    };
27    let left = resolve_callsite_copy(checker, checkpoint, left);
28    let right = resolve_callsite_copy(checker, checkpoint, right);
29
30    let count = property
31        .args
32        .get(2)
33        .and_then(|_| checker.property_len_expr(checkpoint, property))
34        .and_then(|expr| checker.contract_expr_to_smt_term(checkpoint.caller, &expr))
35        .or_else(|| checker.callsite_arg_smt_term(checkpoint, 2))
36        .unwrap_or(SmtTerm::Const(1));
37
38    let elem_size = checker
39        .place_pointee_size(checkpoint.caller, &left)
40        .or_else(|| checker.place_pointee_size(checkpoint.caller, &right))
41        .unwrap_or(1);
42
43    checker.prove_obligation(
44        checkpoint,
45        forward,
46        SmtObligation::NonOverlapping {
47            left,
48            right,
49            left_count: count.clone(),
50            right_count: count,
51            elem_size,
52        },
53    )
54}
55
56fn resolve_callsite_copy<'tcx>(
57    checker: &SmtChecker<'tcx>,
58    checkpoint: &Checkpoint<'tcx>,
59    mut place: PlaceKey,
60) -> PlaceKey {
61    for _ in 0..8 {
62        if !place.fields.is_empty() {
63            return place;
64        }
65        let Some(local) = place.local() else {
66            return place;
67        };
68        let body = checker.tcx.optimized_mir(checkpoint.caller);
69        let block = &body.basic_blocks[checkpoint.block];
70        let source = block
71            .statements
72            .iter()
73            .rev()
74            .find_map(|statement| assignment_source_for_local(statement, local))
75            .or_else(|| {
76                body.basic_blocks.iter().rev().find_map(|block| {
77                    block
78                        .statements
79                        .iter()
80                        .rev()
81                        .find_map(|statement| assignment_source_for_local(statement, local))
82                })
83            });
84        let Some(source) = source else {
85            return place;
86        };
87        let next = PlaceKey::from_mir_place(source);
88        if next == place {
89            return place;
90        }
91        place = next;
92    }
93    place
94}
95
96fn assignment_source_for_local<'a, 'tcx>(
97    statement: &'a rustc_middle::mir::Statement<'tcx>,
98    local: rustc_middle::mir::Local,
99) -> Option<&'a rustc_middle::mir::Place<'tcx>> {
100    let StatementKind::Assign(assign) = &statement.kind else {
101        return None;
102    };
103    let (target, rvalue) = assign.as_ref();
104    if target.local != local {
105        return None;
106    }
107    rvalue_source_place(rvalue)
108}
109
110fn rvalue_source_place<'a, 'tcx>(
111    rvalue: &'a Rvalue<'tcx>,
112) -> Option<&'a rustc_middle::mir::Place<'tcx>> {
113    match rvalue {
114        Rvalue::Use(Operand::Copy(place), ..)
115        | Rvalue::Use(Operand::Move(place), ..)
116        | Rvalue::Cast(_, Operand::Copy(place), _)
117        | Rvalue::Cast(_, Operand::Move(place), _)
118        | Rvalue::CopyForDeref(place) => Some(place),
119        _ => None,
120    }
121}
rapx/verify/smt_check/non_overlap.rs

rapx/verify/smt_check/
non_overlap.rs
