charon_driver/translate/
resolve_path.rs

1//! Machinery to resolve a string path into a `DefId`. Based on `clippy_utils::def_path_res`.
2use std::sync::Arc;
3
4use hax_frontend_exporter::{self as hax, BaseState, SInto};
5use itertools::Itertools;
6use rustc_ast::Mutability;
7use rustc_hir::def_id::{CrateNum, DefId, LOCAL_CRATE};
8use rustc_middle::ty::{fast_reject::SimplifiedType, FloatTy, IntTy, TyCtxt, UintTy};
9use rustc_span::symbol::Symbol;
10
11fn find_primitive_impls<'tcx>(
12    tcx: TyCtxt<'tcx>,
13    name: &str,
14) -> impl Iterator<Item = DefId> + use<'tcx> {
15    let ty = match name {
16        "bool" => SimplifiedType::Bool,
17        "char" => SimplifiedType::Char,
18        "str" => SimplifiedType::Str,
19        "array" => SimplifiedType::Array,
20        "slice" => SimplifiedType::Slice,
21        // FIXME: rustdoc documents these two using just `pointer`.
22        //
23        // Maybe this is something we should do here too.
24        "const_ptr" => SimplifiedType::Ptr(Mutability::Not),
25        "mut_ptr" => SimplifiedType::Ptr(Mutability::Mut),
26        "isize" => SimplifiedType::Int(IntTy::Isize),
27        "i8" => SimplifiedType::Int(IntTy::I8),
28        "i16" => SimplifiedType::Int(IntTy::I16),
29        "i32" => SimplifiedType::Int(IntTy::I32),
30        "i64" => SimplifiedType::Int(IntTy::I64),
31        "i128" => SimplifiedType::Int(IntTy::I128),
32        "usize" => SimplifiedType::Uint(UintTy::Usize),
33        "u8" => SimplifiedType::Uint(UintTy::U8),
34        "u16" => SimplifiedType::Uint(UintTy::U16),
35        "u32" => SimplifiedType::Uint(UintTy::U32),
36        "u64" => SimplifiedType::Uint(UintTy::U64),
37        "u128" => SimplifiedType::Uint(UintTy::U128),
38        "f32" => SimplifiedType::Float(FloatTy::F32),
39        "f64" => SimplifiedType::Float(FloatTy::F64),
40        _ => {
41            return [].iter().copied();
42        }
43    };
44    tcx.incoherent_impls(ty).iter().copied()
45}
46
47/// Resolves a def path like `std::vec::Vec`.
48///
49/// Can return multiple resolutions when there are multiple versions of the same crate, e.g.
50/// `memchr::memchr` could return the functions from both memchr 1.0 and memchr 2.0.
51///
52/// Also returns multiple results when there are multiple paths under the same name e.g. `std::vec`
53/// would have both a [`DefKind::Mod`] and [`DefKind::Macro`].
54///
55/// This function is expensive and should be used sparingly.
56///
57/// If the path does not correspond to an existing item, return the first subpath that doesn't
58/// correspond to an item.
59pub fn def_path_def_ids<'a, 'tcx>(
60    s: &impl BaseState<'tcx>,
61    path: &'a [&'a str],
62) -> Result<Vec<DefId>, &'a [&'a str]> {
63    let tcx = s.base().tcx;
64    let mut items = vec![];
65    for (i, &segment_str) in path.iter().enumerate() {
66        if i == 0 {
67            let segment = Symbol::intern(segment_str);
68            items = tcx
69                .crates(())
70                .iter()
71                .copied()
72                .chain([LOCAL_CRATE])
73                .filter(move |&num| tcx.crate_name(num) == segment)
74                // Also consider "crate" a valid name for the local crate.
75                .chain(if segment_str == "crate" {
76                    Some(LOCAL_CRATE)
77                } else {
78                    None
79                })
80                .map(CrateNum::as_def_id)
81                .collect_vec();
82            items.extend(find_primitive_impls(tcx, segment_str));
83        } else {
84            items = items
85                .into_iter()
86                .flat_map(|def_id| {
87                    let hax_def: Arc<hax::FullDef> = def_id.sinto(s).full_def(s);
88                    hax_def.nameable_children(s)
89                })
90                .filter(|(child_name, _)| *child_name == segment_str)
91                .filter_map(|(_, def_id)| def_id.as_rust_def_id())
92                .collect();
93        }
94        if items.is_empty() {
95            return Err(&path[..=i]);
96        }
97    }
98    Ok(items)
99}
charon_driver/translate/resolve_path.rs

charon_driver/translate/
resolve_path.rs
