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::Spanned;
9use rustc_middle::mir::{BasicBlock, Body, Operand, Place};
10use rustc_middle::ty::TyCtxt;
11
12use crate::analysis::dataflow::types::DataflowGraph;
13
14use super::super::{
15    call_summary,
16    def_use::{PlaceKey, RelevantPlaces, call_args_uses_at, operand_uses},
17};
18
19use super::types::RelevantItem;
20
21/// Visit a call terminator using an interprocedural dependency summary.
22pub(crate) fn visit<'tcx>(
23    tcx: TyCtxt<'tcx>,
24    block: BasicBlock,
25    func: &Operand<'tcx>,
26    args: &[Spanned<Operand<'tcx>>],
27    destination: &Place<'tcx>,
28    flow: &DataflowGraph,
29    body: &Body<'tcx>,
30    relevant: &mut RelevantPlaces,
31    items: &mut Vec<RelevantItem<'tcx>>,
32) {
33    let mut defs = RelevantPlaces::new();
34    defs.insert_mir_place(destination);
35
36    let tpos = body.basic_blocks[block].statements.len();
37    let mut arg_uses = RelevantPlaces::new();
38    for &edge_idx in &flow.node(destination.local).in_edges {
39        let edge = &flow.edges[edge_idx];
40        if edge.block == block.as_usize() && edge.statement_index == tpos {
41            arg_uses.insert_local(edge.src);
42        }
43    }
44
45    let summary = call_summary::dependency_summary(tcx, func, args.len());
46
47    if defs.intersects(relevant) {
48        if summary.unsupported {
49            items.push(RelevantItem::Forget);
50        }
51        items.push(RelevantItem::Terminator { block });
52        relevant.remove_all(&defs);
53        relevant.extend(call_args_uses_at(args, &summary.return_depends_on_args));
54        return;
55    }
56
57    let relevant_written_arg = summary.may_write_args.iter().any(|index| {
58        args.get(*index)
59            .is_some_and(|arg| operand_uses(&arg.node).intersects(relevant))
60    });
61    let summarized_write = !summary.may_write_args.is_empty();
62    if relevant_written_arg
63        || summarized_write
64        || (summary.unsupported && arg_uses.intersects(relevant))
65    {
66        if summary.unsupported {
67            items.push(RelevantItem::Forget);
68        }
69        items.push(RelevantItem::Terminator { block });
70        relevant.extend(call_args_uses_at(args, &summary.may_write_args));
71    }
72
73    // If the contract requires the length of a place (via `Len(place)`),
74    // and this call is a `slice::len()` whose argument traces to the
75    // same origin, add the destination to relevance so the length term
76    // is available for the contract obligation.
77    if !relevant.need_len.is_empty() {
78        let name = crate::helpers::mir_utils::call_name(tcx, func);
79        if name.ends_with("::len") || name.contains("::len(") {
80            if let Some(first) = args.first() {
81                let arg_place = match &first.node {
82                    Operand::Copy(p) | Operand::Move(p) => Some(PlaceKey::from_mir_place(p)),
83                    _ => None,
84                };
85                if let Some(arg_key) = arg_place {
86                    let matches = relevant.need_len.contains(&arg_key)
87                        || relevant
88                            .need_len
89                            .iter()
90                            .any(|nl| {
91                                crate::verify::def_use::trace_place_origin(flow, nl)
92                                    == crate::verify::def_use::trace_place_origin(flow, &arg_key)
93                            });
94                    if matches {
95                        let dest_key = PlaceKey::from_mir_place(destination);
96                        if relevant.places.insert(dest_key.clone()) {
97                            relevant.just_added.insert(dest_key.clone());
98                        }
99                        if let Some(local) = dest_key.local() {
100                            relevant.locals.insert(local);
101                        }
102                        items.push(RelevantItem::Terminator { block });
103                    }
104                }
105            }
106        }
107    }
108}
rapx/verify/slicer/call_visit.rs

rapx/verify/slicer/
call_visit.rs
