Skip to main content

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(crate) 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_scan::Checkpoint;
16use crate::helpers::mir_utils::callee_param_index_for_local;
17
18impl PlaceKey {
19    /// Build a relevance place key from a parsed contract place.
20    pub(crate) 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::ForEach => None,
34                })
35                .collect(),
36        }
37    }
38}
39
40impl RelevantPlaces {
41    /// Extract initial relevance roots from a required property.
42    pub(crate) 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(crate) 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        if let Property::And(and) = property {
56            for conjunct in &and.conjuncts {
57                self.collect_property(conjunct);
58            }
59            return;
60        }
61        if let Property::Or(or) = property {
62            for disjunct in &or.disjuncts {
63                self.collect_property(disjunct);
64            }
65            return;
66        }
67        let kind = property.kind();
68        for (arg_index, arg) in property.args().iter().enumerate() {
69            if let Some(k) = kind
70                && self.collect_target_argument_root(&k, arg_index, arg)
71            {
72                continue;
73            }
74            self.collect_property_arg(arg);
75        }
76    }
77
78    /// Collect a numeric std-contract target argument as a callee argument root.
79    fn collect_target_argument_root(
80        &mut self,
81        kind: &PropertyKind,
82        arg_index: usize,
83        arg: &PropertyArg<'_>,
84    ) -> bool {
85        if !is_target_argument_index(kind, arg_index) {
86            return false;
87        }
88        let PropertyArg::Expr(ContractExpr::Const(value)) = arg else {
89            return false;
90        };
91        let Ok(index) = usize::try_from(*value) else {
92            return false;
93        };
94        self.insert_place_key(PlaceKey {
95            base: PlaceBaseKey::Arg(index),
96            fields: Vec::new(),
97        });
98        true
99    }
100
101    /// Collect all roots mentioned by a property argument.
102    fn collect_property_arg(&mut self, arg: &PropertyArg<'_>) {
103        match arg {
104            PropertyArg::Expr(expr) => self.collect_contract_expr(expr),
105            PropertyArg::Predicates(predicates) => {
106                for predicate in predicates {
107                    self.collect_numeric_predicate(predicate);
108                }
109            }
110            PropertyArg::Ty(_) | PropertyArg::Ident(_) | PropertyArg::Region(_) => {}
111        }
112    }
113
114    /// Collect all roots mentioned by a numeric predicate.
115    fn collect_numeric_predicate(&mut self, predicate: &NumericPredicate<'_>) {
116        self.collect_contract_expr(&predicate.lhs);
117        self.collect_contract_expr(&predicate.rhs);
118    }
119
120    /// Collect all roots mentioned by a contract expression.
121    fn collect_contract_expr(&mut self, expr: &ContractExpr<'_>) {
122        match expr {
123            ContractExpr::Place(place) => self.insert_contract_place(place),
124            ContractExpr::Binary { lhs, rhs, .. } => {
125                self.collect_contract_expr(lhs);
126                self.collect_contract_expr(rhs);
127            }
128            ContractExpr::Unary { expr, .. } => self.collect_contract_expr(expr),
129            ContractExpr::Len(expr) => {
130                self.collect_contract_expr(expr);
131                if let ContractExpr::Place(place) = expr.as_ref() {
132                    self.need_len.insert(PlaceKey::from_contract_place(place));
133                }
134            }
135            ContractExpr::IndexAccess { slice, index } => {
136                self.collect_contract_expr(slice);
137                self.collect_contract_expr(index);
138            }
139            ContractExpr::If {
140                cond,
141                then_expr,
142                else_expr,
143            } => {
144                self.collect_numeric_predicate(cond);
145                self.collect_contract_expr(then_expr);
146                self.collect_contract_expr(else_expr);
147            }
148            ContractExpr::Const(_)
149            | ContractExpr::ConstParam { .. }
150            | ContractExpr::SizeOf(_)
151            | ContractExpr::AlignOf(_)
152            | ContractExpr::Unknown => {}
153        }
154    }
155}
156
157/// Return whether an argument index is a target-place position for a property.
158fn is_target_argument_index(kind: &PropertyKind, arg_index: usize) -> bool {
159    match kind {
160        PropertyKind::NonOverlap | PropertyKind::Alias => arg_index <= 1,
161        PropertyKind::ValidNum | PropertyKind::Unknown => false,
162        _ => arg_index == 0,
163    }
164}
165
166/// Bind callee parameter roots to concrete MIR call operands.
167pub(crate) fn bind_callsite_roots(
168    tcx: TyCtxt<'_>,
169    relevance: &mut RelevantPlaces,
170    checkpoint: &Checkpoint<'_>,
171) {
172    let argument_roots: Vec<(PlaceKey, usize)> = relevance
173        .places
174        .iter()
175        .filter_map(|place| argument_index_of_place(tcx, checkpoint, place))
176        .collect();
177
178    let mut bound_roots = RelevantPlaces::new();
179    let mut rebound_roots = Vec::new();
180    for (root, index) in argument_roots {
181        if let Some(operand) = checkpoint.args.get(index) {
182            if let Some(place) = bind_operand_place(operand, &root.fields) {
183                bound_roots.insert_place_key(place);
184            } else {
185                bound_roots.extend(operand_uses(operand));
186            }
187            rebound_roots.push(root);
188        }
189    }
190
191    relevance.remove_place_keys(&rebound_roots);
192    relevance.extend(bound_roots);
193
194    // Bind need_len places: contract `Len(place)` expressions where the
195    // inner place is a callee argument.  The bound callsite place is
196    // registered in relevance.need_len so the backward slicer can match
197    // `slice::len()` calls that operate on the same pointer/slice.
198    {
199        let need_len_roots: Vec<(PlaceKey, usize)> = relevance
200            .need_len
201            .iter()
202            .filter_map(|place| argument_index_of_place(tcx, checkpoint, place))
203            .collect();
204        for (root, index) in need_len_roots {
205            if let Some(operand) = checkpoint.args.get(index) {
206                if let Some(place) = bind_operand_place(operand, &root.fields) {
207                    relevance.need_len.insert(place);
208                }
209            }
210        }
211    }
212}
213
214/// Map a root place to its callee argument index, if it is an `Arg` or a
215/// `Local` that traces to a callee parameter.
216fn argument_index_of_place(
217    tcx: TyCtxt<'_>,
218    checkpoint: &Checkpoint<'_>,
219    place: &PlaceKey,
220) -> Option<(PlaceKey, usize)> {
221    match place.base {
222        PlaceBaseKey::Arg(index) => Some((place.clone(), index)),
223        PlaceBaseKey::Local(local) => checkpoint
224            .callee
225            .and_then(|callee| callee_param_index_for_local(tcx, callee, local))
226            .map(|index| (place.clone(), index)),
227        _ => None,
228    }
229}
230
231fn bind_operand_place(operand: &Operand<'_>, fields: &[usize]) -> Option<PlaceKey> {
232    let mut place = match operand {
233        Operand::Copy(place) | Operand::Move(place) => PlaceKey::from_mir_place(place),
234        Operand::Constant(_) => return None,
235        #[cfg(rapx_ge_95)]
236        Operand::RuntimeChecks(_) => return None,
237    };
238    place.fields.extend(fields.iter().copied());
239    Some(place)
240}