rapx/verify/
def_use.rs

1//! Def-use computation for the backward path visitor.
2//!
3//! These types and helpers track which MIR places are relevant to a safety
4//! property and compute definitions/uses from MIR terminators.
5//! This is the data layer that `slicing` drives block-by-block along a
6//! finite verification path; keeping it separate lets the core visit logic stay
7//! focused on path-level decisions (calls, SCC exits, path conditions).
8
9use crate::compat::FxHashSet;
10use crate::compat::Spanned;
11use rustc_middle::mir::{
12    Local, Operand, Place, ProjectionElem, Rvalue, Terminator, TerminatorKind,
13};
14use rustc_middle::ty::TyCtxt;
15
16use super::{
17    contract::{
18        ContractExpr, ContractPlace, ContractProjection, NumericPredicate, PlaceBase, Property,
19        PropertyArg, PropertyKind,
20    },
21    helpers::{Checkpoint, callee_param_index_for_local},
22};
23
24/// Definitions and uses collected from one MIR item.
25#[derive(Clone, Debug, Default)]
26pub struct DefUse {
27    /// Places defined or invalidated by the MIR item.
28    pub defs: RelevantPlaces,
29    /// Places read by the MIR item.
30    pub uses: RelevantPlaces,
31}
32
33impl DefUse {
34    /// Create an empty use-def summary.
35    pub fn new() -> Self {
36        Self::default()
37    }
38}
39
40/// Base of a contract/MIR place tracked by relevance.
41#[derive(Clone, Debug, Eq, PartialEq, Hash)]
42pub enum PlaceBaseKey {
43    /// MIR return local `_0`.
44    Return,
45    /// MIR local by numeric index.
46    Local(usize),
47    /// Callee argument by index before checkpoint binding.
48    Arg(usize),
49}
50
51/// Projection-insensitive enough place key for relevance tracking.
52#[derive(Clone, Debug, Eq, PartialEq, Hash)]
53pub struct PlaceKey {
54    /// Base local/argument of the place.
55    pub base: PlaceBaseKey,
56    /// Field projections kept from the contract place.
57    pub fields: Vec<usize>,
58}
59
60impl PlaceKey {
61    /// Build a relevance place key from a parsed contract place.
62    pub fn from_contract_place(place: &ContractPlace<'_>) -> Self {
63        Self {
64            base: match place.base {
65                PlaceBase::Return => PlaceBaseKey::Return,
66                PlaceBase::Arg(index) => PlaceBaseKey::Arg(index),
67                PlaceBase::Local(local) => PlaceBaseKey::Local(local),
68            },
69            fields: place
70                .projections
71                .iter()
72                .map(|projection| match projection {
73                    ContractProjection::Field { index, .. } => *index,
74                })
75                .collect(),
76        }
77    }
78
79    /// Build a relevance place key from a MIR place.
80    pub fn from_mir_place(place: &Place<'_>) -> Self {
81        Self {
82            base: if place.local.as_usize() == 0 {
83                PlaceBaseKey::Return
84            } else {
85                PlaceBaseKey::Local(place.local.as_usize())
86            },
87            fields: place
88                .projection
89                .iter()
90                .filter_map(|projection| match projection {
91                    ProjectionElem::Field(index, _) => Some(index.as_usize()),
92                    _ => None,
93                })
94                .collect(),
95        }
96    }
97
98    /// Return the MIR local represented by this key when it is already known.
99    pub fn local(&self) -> Option<Local> {
100        match self.base {
101            PlaceBaseKey::Return => Some(Local::from_usize(0)),
102            PlaceBaseKey::Local(local) => Some(Local::from_usize(local)),
103            PlaceBaseKey::Arg(_) => None,
104        }
105    }
106
107    /// Return true when this place shares a base-and-projection prefix with
108    /// `other`.  Two places overlap when one of them is a shorter projection
109    /// of the other (e.g. `[]` overlaps `[0]`, but `[0]` does not overlap
110    /// `[1]`).
111    pub fn overlaps(&self, other: &PlaceKey) -> bool {
112        self.base == other.base && {
113            let min_len = self.fields.len().min(other.fields.len());
114            self.fields[..min_len] == other.fields[..min_len]
115        }
116    }
117}
118
119/// Set of places that make MIR items relevant to a property.
120#[derive(Clone, Debug, Default)]
121pub struct RelevantPlaces {
122    /// Contract-level places, including callee arguments before binding.
123    pub places: FxHashSet<PlaceKey>,
124    /// MIR locals that are already known from local contract places.
125    pub locals: FxHashSet<Local>,
126}
127
128impl RelevantPlaces {
129    /// Create an empty relevance set.
130    pub fn new() -> Self {
131        Self::default()
132    }
133
134    /// Extract initial relevance roots from a required property.
135    pub fn from_property(property: &Property<'_>) -> Self {
136        let mut set = Self::new();
137        set.collect_property(property);
138        set
139    }
140
141    /// Return true when no roots have been collected.
142    pub fn is_empty(&self) -> bool {
143        self.places.is_empty() && self.locals.is_empty()
144    }
145
146    /// Return the number of contract-level places in this set.
147    pub fn place_count(&self) -> usize {
148        self.places.len()
149    }
150
151    /// Return the number of MIR locals in this set.
152    pub fn local_count(&self) -> usize {
153        self.locals.len()
154    }
155
156    /// Insert a MIR local as a relevance root.
157    pub fn insert_local(&mut self, local: Local) {
158        self.locals.insert(local);
159        self.places.insert(PlaceKey {
160            base: if local.as_usize() == 0 {
161                PlaceBaseKey::Return
162            } else {
163                PlaceBaseKey::Local(local.as_usize())
164            },
165            fields: Vec::new(),
166        });
167    }
168
169    /// Insert a MIR place as a relevance root.
170    pub fn insert_mir_place(&mut self, place: &Place<'_>) {
171        self.insert_place_key(PlaceKey::from_mir_place(place));
172    }
173
174    /// Insert a contract place as a relevance root.
175    pub fn insert_contract_place(&mut self, place: &ContractPlace<'_>) {
176        self.insert_place_key(PlaceKey::from_contract_place(place));
177    }
178
179    /// Insert a prebuilt place key as a relevance root.
180    pub fn insert_place_key(&mut self, place: PlaceKey) {
181        if let Some(local) = place.local() {
182            self.locals.insert(local);
183        }
184        self.places.insert(place);
185    }
186
187    /// Merge another relevance set into this one.
188    pub fn extend(&mut self, other: RelevantPlaces) {
189        self.places.extend(other.places);
190        self.locals.extend(other.locals);
191    }
192
193    /// Remove a list of place keys and rebuild the derived local set.
194    pub fn remove_place_keys(&mut self, places: &[PlaceKey]) {
195        for place in places {
196            self.places.remove(place);
197        }
198        self.rebuild_locals();
199    }
200
201    /// Return true if this set shares any known root with `other`.
202    pub fn intersects(&self, other: &RelevantPlaces) -> bool {
203        self.places
204            .iter()
205            .any(|sp| other.places.iter().any(|op| sp.overlaps(op)))
206    }
207
208    /// Remove all roots contained in `other` from this set.
209    pub fn remove_all(&mut self, other: &RelevantPlaces) {
210        for local in &other.locals {
211            self.locals.remove(local);
212            self.places.retain(|place| place.local() != Some(*local));
213        }
214        for place in &other.places {
215            self.places.remove(place);
216            if let Some(local) = place.local() {
217                self.locals.remove(&local);
218            }
219        }
220    }
221
222    fn rebuild_locals(&mut self) {
223        self.locals = self.places.iter().filter_map(PlaceKey::local).collect();
224    }
225
226    /// Collect all roots mentioned by a property.
227    fn collect_property(&mut self, property: &Property<'_>) {
228        for (arg_index, arg) in property.args.iter().enumerate() {
229            if self.collect_target_argument_root(&property.kind, arg_index, arg) {
230                continue;
231            }
232            self.collect_property_arg(arg);
233        }
234    }
235
236    /// Collect a numeric std-contract target argument as a callee argument root.
237    fn collect_target_argument_root(
238        &mut self,
239        kind: &PropertyKind,
240        arg_index: usize,
241        arg: &PropertyArg<'_>,
242    ) -> bool {
243        if !is_target_argument_index(kind, arg_index) {
244            return false;
245        }
246        let PropertyArg::Expr(ContractExpr::Const(value)) = arg else {
247            return false;
248        };
249        let Ok(index) = usize::try_from(*value) else {
250            return false;
251        };
252        self.insert_place_key(PlaceKey {
253            base: PlaceBaseKey::Arg(index),
254            fields: Vec::new(),
255        });
256        true
257    }
258
259    /// Collect all roots mentioned by a property argument.
260    fn collect_property_arg(&mut self, arg: &PropertyArg<'_>) {
261        match arg {
262            PropertyArg::Place(place) => self.insert_contract_place(place),
263            PropertyArg::Expr(expr) => self.collect_contract_expr(expr),
264            PropertyArg::Predicates(predicates) => {
265                for predicate in predicates {
266                    self.collect_numeric_predicate(predicate);
267                }
268            }
269            PropertyArg::Ty(_) | PropertyArg::Ident(_) => {}
270        }
271    }
272
273    /// Collect all roots mentioned by a numeric predicate.
274    fn collect_numeric_predicate(&mut self, predicate: &NumericPredicate<'_>) {
275        self.collect_contract_expr(&predicate.lhs);
276        self.collect_contract_expr(&predicate.rhs);
277    }
278
279    /// Collect all roots mentioned by a contract expression.
280    fn collect_contract_expr(&mut self, expr: &ContractExpr<'_>) {
281        match expr {
282            ContractExpr::Place(place) => self.insert_contract_place(place),
283            ContractExpr::Binary { lhs, rhs, .. } => {
284                self.collect_contract_expr(lhs);
285                self.collect_contract_expr(rhs);
286            }
287            ContractExpr::Unary { expr, .. } => self.collect_contract_expr(expr),
288            ContractExpr::Len(expr) => self.collect_contract_expr(expr),
289            ContractExpr::IndexAccess { slice, index } => {
290                self.collect_contract_expr(slice);
291                self.collect_contract_expr(index);
292            }
293            ContractExpr::Const(_)
294            | ContractExpr::ConstParam { .. }
295            | ContractExpr::SizeOf(_)
296            | ContractExpr::AlignOf(_)
297            | ContractExpr::Unknown => {}
298        }
299    }
300}
301
302/// Return whether an argument index is a target-place position for a property.
303fn is_target_argument_index(kind: &PropertyKind, arg_index: usize) -> bool {
304    match kind {
305        PropertyKind::NonOverlap | PropertyKind::Alias => arg_index <= 1,
306        PropertyKind::ValidNum | PropertyKind::Unknown => false,
307        _ => arg_index == 0,
308    }
309}
310
311/// Bind callee parameter roots to concrete MIR call operands.
312pub fn bind_callsite_roots(
313    tcx: TyCtxt<'_>,
314    relevance: &mut RelevantPlaces,
315    checkpoint: &Checkpoint<'_>,
316) {
317    let argument_roots: Vec<(PlaceKey, usize)> = relevance
318        .places
319        .iter()
320        .filter_map(|place| match place.base {
321            PlaceBaseKey::Arg(index) => Some((place.clone(), index)),
322            PlaceBaseKey::Local(local) => checkpoint
323                .callee
324                .and_then(|callee| callee_param_index_for_local(tcx, callee, local))
325                .map(|index| (place.clone(), index)),
326            _ => None,
327        })
328        .collect();
329
330    let mut bound_roots = RelevantPlaces::new();
331    let mut rebound_roots = Vec::new();
332    for (root, index) in argument_roots {
333        if let Some(operand) = checkpoint.args.get(index) {
334            if let Some(place) = bind_operand_place(operand, &root.fields) {
335                bound_roots.insert_place_key(place);
336            } else {
337                bound_roots.extend(operand_uses(operand));
338            }
339            rebound_roots.push(root);
340        }
341    }
342
343    relevance.remove_place_keys(&rebound_roots);
344    relevance.extend(bound_roots);
345}
346
347fn bind_operand_place(operand: &Operand<'_>, fields: &[usize]) -> Option<PlaceKey> {
348    let mut place = match operand {
349        Operand::Copy(place) | Operand::Move(place) => PlaceKey::from_mir_place(place),
350        Operand::Constant(_) => return None,
351        #[cfg(rapx_rustc_ge_196)]
352        Operand::RuntimeChecks(_) => return None,
353    };
354    place.fields.extend(fields.iter().copied());
355    Some(place)
356}
357
358// ── def-use extraction from MIR ────────────────────────────────────────
359
360/// Collect definitions and uses for one MIR terminator.
361pub fn terminator_use_def<'tcx>(terminator: &Terminator<'tcx>) -> DefUse {
362    let mut use_def = DefUse::new();
363    match &terminator.kind {
364        TerminatorKind::Call {
365            func,
366            args,
367            destination,
368            ..
369        } => {
370            use_def.defs.insert_mir_place(destination);
371            use_def.uses.extend(operand_uses(func));
372            for arg in args {
373                use_def.uses.extend(operand_uses(&arg.node));
374            }
375        }
376        TerminatorKind::SwitchInt { discr, .. } => {
377            use_def.uses.extend(operand_uses(discr));
378        }
379        TerminatorKind::Assert { cond, .. } => {
380            use_def.uses.extend(operand_uses(cond));
381        }
382        TerminatorKind::Drop { place, .. } => {
383            use_def.uses.extend(place_uses(place));
384        }
385        _ => {}
386    }
387    use_def
388}
389
390/// Collect MIR roots used by selected call argument indices.
391pub fn call_args_uses_at<'tcx>(
392    args: &[Spanned<Operand<'tcx>>],
393    indices: &[usize],
394) -> RelevantPlaces {
395    let mut uses = RelevantPlaces::new();
396    for index in indices {
397        if let Some(arg) = args.get(*index) {
398            uses.extend(operand_uses(&arg.node));
399        }
400    }
401    uses
402}
403
404/// Collect all MIR roots used by an operand.
405pub fn operand_uses<'tcx>(operand: &Operand<'tcx>) -> RelevantPlaces {
406    let mut uses = RelevantPlaces::new();
407    match operand {
408        Operand::Copy(place) | Operand::Move(place) => {
409            uses.extend(place_uses(place));
410        }
411        Operand::Constant(_) => {}
412        #[cfg(rapx_rustc_ge_196)]
413        Operand::RuntimeChecks(_) => {}
414    }
415    uses
416}
417
418/// Collect the base and projection-index roots used by a MIR place.
419pub fn place_uses(place: &Place<'_>) -> RelevantPlaces {
420    let mut uses = RelevantPlaces::new();
421    uses.insert_mir_place(place);
422    uses.extend(place_projection_uses(place));
423    uses
424}
425
426/// Collect only the index roots used by a place projection.
427pub fn place_projection_uses(place: &Place<'_>) -> RelevantPlaces {
428    let mut uses = RelevantPlaces::new();
429    for projection in place.projection {
430        if let ProjectionElem::Index(local) = projection {
431            uses.insert_local(local);
432        }
433    }
434    uses
435}
436
437/// Collect all MIR operands referenced by an rvalue.
438pub fn rvalue_operands<'tcx>(rvalue: &'tcx Rvalue<'tcx>) -> Vec<&'tcx Operand<'tcx>> {
439    let mut operands = Vec::new();
440    match rvalue {
441        Rvalue::Use(op, ..)
442        | Rvalue::Repeat(op, _)
443        | Rvalue::Cast(_, op, _)
444        | Rvalue::UnaryOp(_, op) => {
445            operands.push(op);
446        }
447        Rvalue::BinaryOp(_, pair) => {
448            let (lhs, rhs) = &**pair;
449            operands.push(lhs);
450            operands.push(rhs);
451        }
452        Rvalue::Ref(_, _, _) | Rvalue::RawPtr(_, _) => {}
453        #[cfg(not(rapx_rustc_ge_196))]
454        Rvalue::ShallowInitBox(_, _) => {}
455        Rvalue::Aggregate(_, aggregate_operands) => {
456            operands.extend(aggregate_operands.iter());
457        }
458        Rvalue::Discriminant(_) | Rvalue::CopyForDeref(_) | Rvalue::ThreadLocalRef(_) | _ => {}
459    }
460    operands
461}
rapx/verify/def_use.rs

rapx/verify/
def_use.rs
