rapx/verify/
def_use.rs

1//! Verify-specific extensions for def-use computation.
2//!
3//! Re-exports core types from `helpers/def_use` and augments
4//! `PlaceKey` / `RelevantPlaces` with contract/property-aware methods.
5
6pub use crate::helpers::def_use::*;
7
8use rustc_middle::mir::Operand;
9use rustc_middle::ty::TyCtxt;
10
11use super::contract::{
12    ContractExpr, ContractPlace, ContractProjection, NumericPredicate, PlaceBase, Property,
13    PropertyArg, PropertyKind,
14};
15use crate::helpers::mir_utils::callee_param_index_for_local;
16use crate::helpers::mir_scan::Checkpoint;
17
18impl PlaceKey {
19    /// Build a relevance place key from a parsed contract place.
20    pub fn from_contract_place(place: &ContractPlace<'_>) -> Self {
21        Self {
22            base: match place.base {
23                PlaceBase::Return => PlaceBaseKey::Return,
24                PlaceBase::Arg(index) => PlaceBaseKey::Arg(index),
25                PlaceBase::Local(local) => PlaceBaseKey::Local(local),
26            },
27            fields: place
28                .projections
29                .iter()
30                .filter_map(|projection| match projection {
31                    ContractProjection::Field { index, .. } => Some(*index),
32                    ContractProjection::Downcast { .. } => Some(0),
33                    ContractProjection::IterElements => None,
34                })
35                .collect(),
36        }
37    }
38}
39
40impl RelevantPlaces {
41    /// Extract initial relevance roots from a required property.
42    pub fn from_property(property: &Property<'_>) -> Self {
43        let mut set = Self::new();
44        set.collect_property(property);
45        set
46    }
47
48    /// Insert a contract place as a relevance root.
49    pub fn insert_contract_place(&mut self, place: &ContractPlace<'_>) {
50        self.insert_place_key(PlaceKey::from_contract_place(place));
51    }
52
53    /// Collect all roots mentioned by a property.
54    fn collect_property(&mut self, property: &Property<'_>) {
55        let kind = property.kind();
56        for (arg_index, arg) in property.args().iter().enumerate() {
57            if let Some(k) = kind
58                && self.collect_target_argument_root(&k, arg_index, arg)
59            {
60                continue;
61            }
62            self.collect_property_arg(arg);
63        }
64    }
65
66    /// Collect a numeric std-contract target argument as a callee argument root.
67    fn collect_target_argument_root(
68        &mut self,
69        kind: &PropertyKind,
70        arg_index: usize,
71        arg: &PropertyArg<'_>,
72    ) -> bool {
73        if !is_target_argument_index(kind, arg_index) {
74            return false;
75        }
76        let PropertyArg::Expr(ContractExpr::Const(value)) = arg else {
77            return false;
78        };
79        let Ok(index) = usize::try_from(*value) else {
80            return false;
81        };
82        self.insert_place_key(PlaceKey {
83            base: PlaceBaseKey::Arg(index),
84            fields: Vec::new(),
85        });
86        true
87    }
88
89    /// Collect all roots mentioned by a property argument.
90    fn collect_property_arg(&mut self, arg: &PropertyArg<'_>) {
91        match arg {
92            PropertyArg::Expr(expr) => self.collect_contract_expr(expr),
93            PropertyArg::Predicates(predicates) => {
94                for predicate in predicates {
95                    self.collect_numeric_predicate(predicate);
96                }
97            }
98            PropertyArg::Ty(_) | PropertyArg::Ident(_) => {}
99        }
100    }
101
102    /// Collect all roots mentioned by a numeric predicate.
103    fn collect_numeric_predicate(&mut self, predicate: &NumericPredicate<'_>) {
104        self.collect_contract_expr(&predicate.lhs);
105        self.collect_contract_expr(&predicate.rhs);
106    }
107
108    /// Collect all roots mentioned by a contract expression.
109    fn collect_contract_expr(&mut self, expr: &ContractExpr<'_>) {
110        match expr {
111            ContractExpr::Place(place) => self.insert_contract_place(place),
112            ContractExpr::Binary { lhs, rhs, .. } => {
113                self.collect_contract_expr(lhs);
114                self.collect_contract_expr(rhs);
115            }
116            ContractExpr::Unary { expr, .. } => self.collect_contract_expr(expr),
117            ContractExpr::Len(expr) => {
118                self.collect_contract_expr(expr);
119                if let ContractExpr::Place(place) = expr.as_ref() {
120                    self.need_len.insert(PlaceKey::from_contract_place(place));
121                }
122            }
123            ContractExpr::IndexAccess { slice, index } => {
124                self.collect_contract_expr(slice);
125                self.collect_contract_expr(index);
126            }
127            ContractExpr::Min { a, b } | ContractExpr::Max { a, b } => {
128                self.collect_contract_expr(a);
129                self.collect_contract_expr(b);
130            }
131            ContractExpr::If {
132                cond,
133                then_expr,
134                else_expr,
135            } => {
136                self.collect_numeric_predicate(cond);
137                self.collect_contract_expr(then_expr);
138                self.collect_contract_expr(else_expr);
139            }
140            ContractExpr::Const(_)
141            | ContractExpr::ConstParam { .. }
142            | ContractExpr::SizeOf(_)
143            | ContractExpr::AlignOf(_)
144            | ContractExpr::Unknown => {}
145        }
146    }
147}
148
149/// Return whether an argument index is a target-place position for a property.
150fn is_target_argument_index(kind: &PropertyKind, arg_index: usize) -> bool {
151    match kind {
152        PropertyKind::NonOverlap | PropertyKind::Alias => arg_index <= 1,
153        PropertyKind::ValidNum | PropertyKind::Unknown => false,
154        _ => arg_index == 0,
155    }
156}
157
158/// Bind callee parameter roots to concrete MIR call operands.
159pub fn bind_callsite_roots(
160    tcx: TyCtxt<'_>,
161    relevance: &mut RelevantPlaces,
162    checkpoint: &Checkpoint<'_>,
163) {
164    let argument_roots: Vec<(PlaceKey, usize)> = relevance
165        .places
166        .iter()
167        .filter_map(|place| match place.base {
168            PlaceBaseKey::Arg(index) => Some((place.clone(), index)),
169            PlaceBaseKey::Local(local) => checkpoint
170                .callee
171                .and_then(|callee| callee_param_index_for_local(tcx, callee, local))
172                .map(|index| (place.clone(), index)),
173            _ => None,
174        })
175        .collect();
176
177    let mut bound_roots = RelevantPlaces::new();
178    let mut rebound_roots = Vec::new();
179    for (root, index) in argument_roots {
180        if let Some(operand) = checkpoint.args.get(index) {
181            if let Some(place) = bind_operand_place(operand, &root.fields) {
182                bound_roots.insert_place_key(place);
183            } else {
184                bound_roots.extend(operand_uses(operand));
185            }
186            rebound_roots.push(root);
187        }
188    }
189
190    relevance.remove_place_keys(&rebound_roots);
191    relevance.extend(bound_roots);
192
193    // Bind need_len places: contract `Len(place)` expressions where the
194    // inner place is a callee argument.  The bound callsite place is
195    // registered in relevance.need_len so the backward slicer can match
196    // `slice::len()` calls that operate on the same pointer/slice.
197    {
198        let need_len_roots: Vec<(PlaceKey, usize)> = relevance
199            .need_len
200            .iter()
201            .filter_map(|place| match place.base {
202                PlaceBaseKey::Arg(index) => Some((place.clone(), index)),
203                PlaceBaseKey::Local(local) => checkpoint
204                    .callee
205                    .and_then(|callee| callee_param_index_for_local(tcx, callee, local))
206                    .map(|index| (place.clone(), index)),
207                _ => None,
208            })
209            .collect();
210        for (root, index) in need_len_roots {
211            if let Some(operand) = checkpoint.args.get(index) {
212                if let Some(place) = bind_operand_place(operand, &root.fields) {
213                    relevance.need_len.insert(place);
214                }
215            }
216        }
217    }
218}
219
220fn bind_operand_place(operand: &Operand<'_>, fields: &[usize]) -> Option<PlaceKey> {
221    let mut place = match operand {
222        Operand::Copy(place) | Operand::Move(place) => PlaceKey::from_mir_place(place),
223        Operand::Constant(_) => return None,
224        #[cfg(rapx_ge_99)]
225        Operand::RuntimeChecks(_) => return None,
226    };
227    place.fields.extend(fields.iter().copied());
228    Some(place)
229}
rapx/verify/def_use.rs

rapx/verify/
def_use.rs
