Skip to main content

rapx/helpers/
mir_scan.rs

1use rustc_hir::{Safety, def_id::DefId};
2use rustc_middle::{
3    mir::{
4        BasicBlock, Body, BorrowKind, Local, Operand, Place, ProjectionElem, Rvalue,
5        StatementKind, TerminatorKind,
6    },
7    ty::{self, Ty, TyCtxt, TyKind},
8};
9use rustc_span::Span;
10use std::collections::{HashMap, HashSet};
11
12use super::name::get_cleaned_def_path_name;
13
14/// Stable MIR location for a call terminator inside one function body.
15#[derive(Clone, Copy, Debug, Eq, PartialEq, Hash)]
16pub struct CheckpointLocation {
17    /// Function containing the call terminator.
18    pub caller: DefId,
19    /// Basic block whose terminator is the call.
20    pub block: BasicBlock,
21}
22
23/// Kind of an unsafe verification checkpoint inside a function body.
24#[derive(Clone, Copy, Debug, Eq, PartialEq, Hash)]
25pub enum CheckpointKind {
26    /// A real unsafe function call.
27    UnsafeCall,
28    /// A raw pointer dereference.
29    RawPtrDeref,
30    /// A mutable static variable access.
31    StaticMutAccess,
32}
33
34/// A verification checkpoint in one MIR body.
35///
36/// Unifies unsafe calls, raw-pointer dereferences, and mutable static
37/// accesses under a single type so they all flow through the same path
38/// extraction and SMT verification pipeline.
39#[derive(Clone, Debug)]
40pub struct Checkpoint<'tcx> {
41    pub caller: DefId,
42    pub callee: Option<DefId>,
43    pub block: BasicBlock,
44    pub span: Span,
45    pub args: Vec<Operand<'tcx>>,
46    pub kind: CheckpointKind,
47    pub is_ref: bool,
48    pub is_mut_ref: bool,
49    pub destination: Option<Local>,
50}
51
52impl<'tcx> Checkpoint<'tcx> {
53    /// Return the MIR location that identifies this checkpoint inside the verifier.
54    pub fn location(&self) -> CheckpointLocation {
55        CheckpointLocation {
56            caller: self.caller,
57            block: self.block,
58        }
59    }
60
61    /// Return a human-readable label for diagnostics.
62    pub fn callee_name(&self, tcx: TyCtxt<'tcx>) -> String {
63        match self.callee {
64            Some(def_id) => get_cleaned_def_path_name(tcx, def_id),
65            None => match self.kind {
66                CheckpointKind::RawPtrDeref => "raw-ptr-deref".to_string(),
67                CheckpointKind::StaticMutAccess => "static-mut-access".to_string(),
68                CheckpointKind::UnsafeCall => "unknown-callee".to_string(),
69            },
70        }
71    }
72}
73
74/// Checks the safety of a function signature.
75pub fn check_safety(tcx: TyCtxt<'_>, def_id: DefId) -> Safety {
76    let poly_fn_sig = tcx.fn_sig(def_id);
77    let fn_sig = poly_fn_sig.skip_binder();
78    fn_sig.safety()
79}
80
81/// Helper checking if a [`Place`] involves raw pointer dereference.
82pub fn place_has_raw_deref<'tcx>(
83    _tcx: TyCtxt<'tcx>,
84    body: &Body<'tcx>,
85    place: &Place<'tcx>,
86) -> bool {
87    let local = place.local;
88    for proj in place.projection.iter() {
89        if let ProjectionElem::Deref = proj.kind() {
90            let ty = body.local_decls[local].ty;
91            if let TyKind::RawPtr(_, _) = ty.kind() {
92                return true;
93            }
94        }
95    }
96    false
97}
98
99/// Analyzes the MIR of the given function to collect all local variables
100/// that are involved in dereferencing raw pointers (`*const T` or `*mut T`).
101pub fn get_rawptr_deref(tcx: TyCtxt<'_>, def_id: DefId) -> HashSet<Local> {
102    let mut raw_ptrs = HashSet::new();
103    if tcx.is_mir_available(def_id) {
104        let body = tcx.optimized_mir(def_id);
105        for bb in body.basic_blocks.iter() {
106            for stmt in &bb.statements {
107                if let StatementKind::Assign(assign) = &stmt.kind {
108                    let (lhs, rhs) = &**assign;
109                    if place_has_raw_deref(tcx, &body, lhs) {
110                        raw_ptrs.insert(lhs.local);
111                    }
112                    if let Rvalue::Use(op, ..) = rhs {
113                        match op {
114                            Operand::Copy(place) | Operand::Move(place) => {
115                                if place_has_raw_deref(tcx, &body, place) {
116                                    raw_ptrs.insert(place.local);
117                                }
118                            }
119                            _ => {}
120                        }
121                    }
122                    if let Rvalue::Ref(_, _, place) = rhs {
123                        if place_has_raw_deref(tcx, &body, place) {
124                            raw_ptrs.insert(place.local);
125                        }
126                    }
127                }
128            }
129            if let Some(terminator) = &bb.terminator {
130                match &terminator.kind {
131                    rustc_middle::mir::TerminatorKind::Call { args, .. } => {
132                        for arg in args {
133                            match arg.node {
134                                Operand::Copy(place) | Operand::Move(place) => {
135                                    if place_has_raw_deref(tcx, &body, &place) {
136                                        raw_ptrs.insert(place.local);
137                                    }
138                                }
139                                _ => {}
140                            }
141                        }
142                    }
143                    _ => {}
144                }
145            }
146        }
147    }
148    raw_ptrs
149}
150
151/// Collects pairs of global static variables and their corresponding local variables
152/// within a function's MIR that are assigned from statics.
153pub fn collect_global_local_pairs(tcx: TyCtxt<'_>, def_id: DefId) -> HashMap<DefId, Vec<Local>> {
154    let mut globals: HashMap<DefId, Vec<Local>> = HashMap::new();
155
156    if !tcx.is_mir_available(def_id) {
157        return globals;
158    }
159
160    let body = tcx.optimized_mir(def_id);
161
162    for bb in body.basic_blocks.iter() {
163        for stmt in &bb.statements {
164            if let StatementKind::Assign(assign) = &stmt.kind {
165                let (lhs, rhs) = &**assign;
166                if let Rvalue::Use(Operand::Constant(c), ..) = rhs {
167                    if let Some(static_def_id) = c.check_static_ptr(tcx) {
168                        globals.entry(static_def_id).or_default().push(lhs.local);
169                    }
170                }
171            }
172        }
173    }
174
175    globals
176}
177
178/// Scans MIR for calls to unsafe functions and returns the set of callee DefIds.
179pub fn get_unsafe_callees(tcx: TyCtxt<'_>, def_id: DefId) -> HashSet<DefId> {
180    let mut unsafe_callees = HashSet::new();
181    if tcx.is_mir_available(def_id) {
182        let body = tcx.optimized_mir(def_id);
183        for bb in body.basic_blocks.iter() {
184            if let TerminatorKind::Call { func, .. } = &bb.terminator().kind {
185                if let Operand::Constant(func_constant) = func {
186                    if let ty::FnDef(callee_def_id, _) = func_constant.const_.ty().kind() {
187                        if check_safety(tcx, *callee_def_id) == Safety::Unsafe {
188                            unsafe_callees.insert(*callee_def_id);
189                        }
190                    }
191                }
192            }
193        }
194    }
195    unsafe_callees
196}
197
198/// Collect all unsafe MIR checkpoints in `def_id` with full per-checkpoint metadata.
199pub fn collect_unsafe_callsites<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId) -> Vec<Checkpoint<'tcx>> {
200    let mut checkpoints = Vec::new();
201    if !tcx.is_mir_available(def_id) {
202        return checkpoints;
203    }
204
205    let body = tcx.optimized_mir(def_id);
206    for (bb, data) in body.basic_blocks.iter_enumerated() {
207        let TerminatorKind::Call {
208            func,
209            args,
210            fn_span,
211            ..
212        } = &data.terminator().kind
213        else {
214            continue;
215        };
216
217        let Operand::Constant(func_constant) = func else {
218            continue;
219        };
220
221        let ty::FnDef(callee_def_id, callee_args) = func_constant.const_.ty().kind() else {
222            continue;
223        };
224        #[cfg(rapx_ge_99)]
225        let callee_args = callee_args.skip_binder();
226
227        if check_safety(tcx, *callee_def_id) != Safety::Unsafe {
228            continue;
229        }
230
231        // Normalize a trait-method callee to the concrete impl method so that
232        // inline `#[rapx::requires]` contracts (which live on the impl, not the
233        // trait declaration) are found during contract lookup.
234        let resolved_callee =
235            resolve_callee_impl(tcx, def_id, *callee_def_id, callee_args).unwrap_or(*callee_def_id);
236
237        checkpoints.push(Checkpoint {
238            caller: def_id,
239            callee: Some(resolved_callee),
240            block: bb,
241            span: *fn_span,
242            args: args.iter().map(|arg| arg.node.clone()).collect(),
243            kind: CheckpointKind::UnsafeCall,
244            is_ref: false,
245            is_mut_ref: false,
246            destination: None,
247        });
248    }
249
250    checkpoints
251}
252
253/// Resolve a (possibly trait-method) callee to the concrete impl method that
254/// will actually be dispatched, given the caller context and the callee's
255/// generic arguments.
256///
257/// This matters for contract lookup: `#[rapx::requires(...)]` annotations are
258/// attached to the impl method, but in a generic caller the MIR `FnDef` refers
259/// to the trait method declaration.  Resolving to the impl method lets the
260/// verifier find those inline contracts.  Returns `None` when the callee cannot
261/// be resolved to a distinct concrete item (e.g. still generic/virtual), in
262/// which case callers should keep the original DefId.
263fn resolve_callee_impl<'tcx>(
264    tcx: TyCtxt<'tcx>,
265    caller_def_id: DefId,
266    callee_def_id: DefId,
267    callee_args: ty::GenericArgsRef<'tcx>,
268) -> Option<DefId> {
269    // Only trait-associated methods need remapping; inherent/free functions
270    // already point at their concrete definition.
271    let assoc = tcx.opt_associated_item(callee_def_id)?;
272    if assoc.trait_container(tcx).is_none() {
273        return None;
274    }
275
276    let typing_env = ty::TypingEnv::post_analysis(tcx, caller_def_id);
277    let instance = ty::Instance::try_resolve(tcx, typing_env, callee_def_id, callee_args)
278        .ok()
279        .flatten()?;
280
281    let resolved = match instance.def {
282        ty::InstanceKind::Item(def_id) => def_id,
283        _ => return None,
284    };
285
286    if resolved == callee_def_id {
287        None
288    } else {
289        Some(resolved)
290    }
291}
292
293/// Metadata for a single raw pointer dereference operation found in MIR.
294#[derive(Clone, Debug)]
295pub struct RawPtrDerefInfo<'tcx> {
296    pub block: BasicBlock,
297    pub ptr_operand: Operand<'tcx>,
298    pub pointee_ty: Ty<'tcx>,
299    pub is_read: bool,
300    pub is_ref: bool,
301    pub is_mut_ref: bool,
302    pub destination: Local,
303}
304
305/// Collect all raw pointer dereference operations in `def_id` as
306/// metadata records (block, pointer operand, pointee type, read-vs-write).
307pub fn collect_raw_ptr_deref_info<'tcx>(
308    tcx: TyCtxt<'tcx>,
309    def_id: DefId,
310) -> Vec<RawPtrDerefInfo<'tcx>> {
311    let mut infos = Vec::new();
312    if !tcx.is_mir_available(def_id) {
313        return infos;
314    }
315
316    let body = tcx.optimized_mir(def_id);
317    // Filter: only check statements from the function's own source file,
318    // not from inlined library code (Vec, Box, etc.).
319    let fn_span = tcx.def_span(def_id);
320    let local_file = tcx.sess.source_map().lookup_char_pos(fn_span.lo()).file;
321
322    for (bb, data) in body.basic_blocks.iter_enumerated() {
323        for stmt in &data.statements {
324            let stmt_file = tcx
325                .sess
326                .source_map()
327                .lookup_char_pos(stmt.source_info.span.lo())
328                .file;
329            if !std::ptr::addr_eq(
330                std::sync::Arc::as_ptr(&stmt_file),
331                std::sync::Arc::as_ptr(&local_file),
332            ) {
333                continue;
334            }
335            let StatementKind::Assign(assign) = &stmt.kind else {
336                continue;
337            };
338            let (lhs, rhs) = &**assign;
339
340            let is_write = place_has_raw_deref(tcx, &body, lhs);
341            let (is_read, is_ref, is_mut_ref) = match rhs {
342                Rvalue::Use(Operand::Copy(place) | Operand::Move(place), ..) => {
343                    (place_has_raw_deref(tcx, &body, place), false, false)
344                }
345                Rvalue::Ref(_, borrow_kind, place) => {
346                    let is_mut = matches!(borrow_kind, BorrowKind::Mut { .. });
347                    (place_has_raw_deref(tcx, &body, place), true, is_mut)
348                }
349                _ => (false, false, false),
350            };
351
352            if !is_write && !is_read {
353                continue;
354            }
355
356            let deref_place = if is_write {
357                lhs
358            } else {
359                match rhs {
360                    Rvalue::Use(Operand::Copy(place) | Operand::Move(place), ..)
361                    | Rvalue::Ref(_, _, place) => place,
362                    _ => continue,
363                }
364            };
365
366            let Some(ptr_operand) = ptr_operand_for_deref_place(deref_place) else {
367                continue;
368            };
369
370            let Some(pointee_ty) = deref_place_pointee_ty(&body, deref_place) else {
371                continue;
372            };
373
374            infos.push(RawPtrDerefInfo {
375                block: bb,
376                ptr_operand,
377                pointee_ty,
378                is_read,
379                is_ref,
380                is_mut_ref,
381                destination: lhs.local,
382            });
383        }
384    }
385
386    infos
387}
388
389/// Return the pointee type of the raw pointer being dereferenced.
390fn deref_place_pointee_ty<'tcx>(body: &Body<'tcx>, place: &Place<'tcx>) -> Option<Ty<'tcx>> {
391    let ty = body.local_decls[place.local].ty;
392    match ty.kind() {
393        TyKind::RawPtr(inner, _) => Some(*inner),
394        _ => None,
395    }
396}
397
398/// Extract the pointer operand from a dereference place.
399fn ptr_operand_for_deref_place<'tcx>(place: &Place<'tcx>) -> Option<Operand<'tcx>> {
400    use rustc_middle::ty::List;
401
402    let first_deref_idx = place
403        .projection
404        .iter()
405        .position(|p| matches!(p.kind(), ProjectionElem::Deref));
406
407    if let Some(idx) = first_deref_idx
408        && idx > 0
409    {
410        return None;
411    }
412
413    Some(Operand::Copy(Place {
414        local: place.local,
415        projection: List::empty(),
416    }))
417}
418
419/// Metadata for a `static mut` access found in MIR.
420#[derive(Clone, Debug)]
421pub struct StaticMutAccessInfo<'tcx> {
422    /// Basic block containing the access.
423    pub block: BasicBlock,
424    /// The pointee type (i.e. the type of the static itself, `T` in `static mut X: T`).
425    pub ty: Ty<'tcx>,
426    /// The MIR operand holding the pointer to the static.
427    pub ptr_operand: Operand<'tcx>,
428}
429
430/// Collect all basic blocks that reference mutable statics in `def_id`.
431///
432/// Mutable statics appear as `Constant` operands whose `check_static_ptr` points
433/// to a `static mut` item.  Both reads and writes are detected here; the
434/// conservative `Init` property will be checked regardless of direction.
435pub fn collect_static_mut_access_info<'tcx>(
436    tcx: TyCtxt<'tcx>,
437    def_id: DefId,
438) -> Vec<StaticMutAccessInfo<'tcx>> {
439    let mut infos = Vec::new();
440    if !tcx.is_mir_available(def_id) {
441        return infos;
442    }
443
444    let body = tcx.optimized_mir(def_id);
445    for (bb, data) in body.basic_blocks.iter_enumerated() {
446        for stmt in &data.statements {
447            if let StatementKind::Assign(assign) = &stmt.kind {
448                let (_lhs, rhs) = &**assign;
449                if let Rvalue::Use(op @ Operand::Constant(c), ..) = rhs {
450                    if let Some(static_id) = c.check_static_ptr(tcx) {
451                        if matches!(tcx.static_mutability(static_id), Some(m) if m.is_mut()) {
452                            let ty = tcx.type_of(static_id).skip_binder();
453                            infos.push(StaticMutAccessInfo {
454                                block: bb,
455                                ty,
456                                ptr_operand: op.clone(),
457                            });
458                        }
459                    }
460                }
461            }
462        }
463
464        if let Some(terminator) = &data.terminator {
465            if let TerminatorKind::Call { args, .. } = &terminator.kind {
466                for arg in args {
467                    match &arg.node {
468                        op @ Operand::Constant(c) => {
469                            if let Some(static_id) = c.check_static_ptr(tcx) {
470                                if matches!(tcx.static_mutability(static_id), Some(m) if m.is_mut())
471                                {
472                                    let ty = tcx.type_of(static_id).skip_binder();
473                                    infos.push(StaticMutAccessInfo {
474                                        block: bb,
475                                        ty,
476                                        ptr_operand: op.clone(),
477                                    });
478                                }
479                            }
480                        }
481                        _ => {}
482                    }
483                }
484            }
485        }
486    }
487
488    infos
489}