rapx/verify/slicer/
call_visit.rs

1//! Call-terminator visiting logic.
2//!
3//! When the backward visitor encounters a call terminator, it delegates to this
4//! module, which consults the interprocedural dependency summaries to decide
5//! which arguments flow through to the destination and whether the call may
6//! modify relevant state.
7
8use crate::compat::{FxHashMap, Spanned};
9use rustc_hir::def_id::DefId;
10use rustc_middle::mir::{BasicBlock, Body, Operand, Place};
11use rustc_middle::ty::{TyCtxt, TyKind};
12
13use crate::analysis::dataflow::types::DataflowGraph;
14
15use super::super::{
16    call_summary,
17    def_use::{PlaceKey, RelevantPlaces, call_args_uses_at, operand_uses},
18};
19
20use super::types::RelevantItem;
21
22/// Visit a call terminator using an interprocedural dependency summary.
23pub(crate) fn visit<'tcx>(
24    tcx: TyCtxt<'tcx>,
25    def_id: DefId,
26    block: BasicBlock,
27    func: &Operand<'tcx>,
28    args: &[Spanned<Operand<'tcx>>],
29    destination: &Place<'tcx>,
30    flow: &DataflowGraph,
31    body: &Body<'tcx>,
32    relevant: &mut RelevantPlaces,
33    items: &mut Vec<RelevantItem<'tcx>>,
34) {
35    let mut defs = RelevantPlaces::new();
36    defs.insert_mir_place(destination);
37
38    let tpos = body.basic_blocks[block].statements.len();
39    let mut arg_uses = RelevantPlaces::new();
40    for &edge_idx in &flow.node(destination.local).in_edges {
41        let edge = &flow.edges[edge_idx];
42        if edge.block == block.as_usize() && edge.statement_index == tpos {
43            arg_uses.insert_local(edge.src);
44        }
45    }
46
47    let summary = call_summary::dependency_summary(tcx, func, args.len(), &call_context_from_args(args));
48
49    if defs.intersects(relevant) {
50        if summary.unsupported {
51            items.push(RelevantItem::UnknownCall);
52        }
53        items.push(RelevantItem::Terminator { def_id, block, switch_succ: None });
54        relevant.remove_all(&defs);
55        relevant.extend(call_args_uses_at(args, &summary.return_depends_on_args));
56        return;
57    }
58
59    // A call returning a pointer/reference (e.g. `get_unchecked`, `as_ptr`,
60    // `Box::new`'s `NonNull` destination) carries the callee's provenance even
61    // when its destination is not *value*-relevant.  Keep it so the forward VM
62    // applies the call's effect (and thus the provenance/alloc) instead of
63    // relying on the backward `propagate_pass` re-application.  Deliberately
64    // *not* applied to must-write calls (e.g. `MaybeUninit::write`), whose
65    // write effect is tracked separately below via `must_write_args`.
66    let dest_is_ptr = matches!(
67        body.local_decls[destination.local].ty.kind(),
68        TyKind::RawPtr(..) | TyKind::Ref(..)
69    );
70    if dest_is_ptr && summary.must_write_args.is_empty() {
71        if summary.unsupported {
72            items.push(RelevantItem::UnknownCall);
73        }
74        items.push(RelevantItem::Terminator { def_id, block, switch_succ: None });
75        relevant.remove_all(&defs);
76        relevant.extend(call_args_uses_at(args, &summary.return_depends_on_args));
77        return;
78    }
79
80    let relevant_written_arg = summary.must_write_args.iter().any(|index| {
81        args.get(*index)
82            .is_some_and(|arg| operand_uses(&arg.node).intersects(relevant))
83    });
84    let summarized_write = !summary.must_write_args.is_empty();
85    if relevant_written_arg
86        || summarized_write
87        || (summary.unsupported && arg_uses.intersects(relevant))
88    {
89        if summary.unsupported {
90            items.push(RelevantItem::UnknownCall);
91        }
92        items.push(RelevantItem::Terminator { def_id, block, switch_succ: None });
93        relevant.extend(call_args_uses_at(args, &summary.must_write_args));
94    }
95
96    // If the contract requires the length of a place (via `Len(place)`),
97    // and this call is a `slice::len()` whose argument traces to the
98    // same origin, add the destination to relevance so the length term
99    // is available for the contract obligation.
100    if !relevant.need_len.is_empty() {
101        let callee = crate::helpers::mir_utils::dep_callee_def_id(func);
102        if crate::verify::api_classify::is_len(callee) {
103            if let Some(first) = args.first() {
104                let arg_place = crate::helpers::mir_utils::operand_place(&first.node);
105                if let Some(arg_key) = arg_place {
106                    let matches = relevant.need_len.contains(&arg_key)
107                        || relevant.need_len.iter().any(|nl| {
108                            crate::verify::def_use::trace_place_origin(flow, nl)
109                                == crate::verify::def_use::trace_place_origin(flow, &arg_key)
110                        });
111                    if matches {
112                        let dest_key = PlaceKey::from_mir_place(destination);
113                        if relevant.places.insert(dest_key.clone()) {
114                            relevant.just_added.insert(dest_key.clone());
115                        }
116                        if let Some(local) = dest_key.local() {
117                            relevant.locals.insert(local);
118                        }
119                        items.push(RelevantItem::Terminator { def_id, block, switch_succ: None });
120                    }
121                }
122            }
123        }
124    }
125}
126
127/// Build a concrete `CallContext` from the call's literal arguments so the
128/// backward slicer prunes callee paths the same way the forward VM does. Only
129/// constant integer arguments are carried; symbolic arguments are absent.
130fn call_context_from_args(args: &[Spanned<Operand<'_>>]) -> call_summary::CallContext {
131    let mut concrete = FxHashMap::default();
132    for (i, arg) in args.iter().enumerate() {
133        if let Some(v) = crate::helpers::mir_utils::operand_const_u64(&arg.node) {
134            concrete.insert(i, v as i128);
135        }
136    }
137    call_summary::CallContext { concrete }
138}
rapx/verify/slicer/call_visit.rs

rapx/verify/slicer/
call_visit.rs
