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::{RelevantPlaces, call_args_uses_at, operand_uses},
17};
18
19use super::types::{BackwardItem, ForgetReason, KeepReason};
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<BackwardItem<'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(BackwardItem::Forget {
50                reason: ForgetReason::UnknownCall,
51            });
52        }
53        items.push(BackwardItem::Terminator {
54            block,
55            kind: if summary.unsupported {
56                KeepReason::UnknownEffect
57            } else {
58                KeepReason::PointerFlow
59            },
60        });
61        relevant.remove_all(&defs);
62        relevant.extend(call_args_uses_at(args, &summary.return_depends_on_args));
63        return;
64    }
65
66    let relevant_written_arg = summary.may_write_args.iter().any(|index| {
67        args.get(*index)
68            .is_some_and(|arg| operand_uses(&arg.node).intersects(relevant))
69    });
70    let summarized_write = !summary.may_write_args.is_empty();
71    if relevant_written_arg
72        || summarized_write
73        || (summary.unsupported && arg_uses.intersects(relevant))
74    {
75        if summary.unsupported {
76            items.push(BackwardItem::Forget {
77                reason: ForgetReason::UnknownCall,
78            });
79        }
80        items.push(BackwardItem::Terminator {
81            block,
82            kind: if summary.unsupported {
83                KeepReason::UnknownEffect
84            } else {
85                KeepReason::PointerFlow
86            },
87        });
88        relevant.extend(call_args_uses_at(args, &summary.may_write_args));
89    }
90}
rapx/verify/slicer/call_visit.rs

rapx/verify/slicer/
call_visit.rs
