Skip to content

Commit d2b8c27

Browse files
authored
Use intrinsic_name to get the intrinsic name (#3114)
Let's close the loop and use `intrinsic_name`, the StableMIR API we added in rust-lang/rust#122203, to retrieve the intrinsic name and avoid post-processing it.
1 parent f5f1e94 commit d2b8c27

File tree

1 file changed

+3
-20
lines changed

1 file changed

+3
-20
lines changed

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

Lines changed: 3 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -69,7 +69,7 @@ impl<'tcx> GotocCtx<'tcx> {
6969
/// Handles codegen for non returning intrinsics
7070
/// Non returning intrinsics are not associated with a destination
7171
pub fn codegen_never_return_intrinsic(&mut self, instance: Instance, span: Span) -> Stmt {
72-
let intrinsic = instance.mangled_name();
72+
let intrinsic = instance.intrinsic_name().unwrap();
7373

7474
debug!("codegen_never_return_intrinsic:\n\tinstance {:?}\n\tspan {:?}", instance, span);
7575

@@ -112,8 +112,8 @@ impl<'tcx> GotocCtx<'tcx> {
112112
place: &Place,
113113
span: Span,
114114
) -> Stmt {
115-
let intrinsic_sym = instance.trimmed_name();
116-
let intrinsic = intrinsic_sym.as_str();
115+
let intrinsic_name = instance.intrinsic_name().unwrap();
116+
let intrinsic = intrinsic_name.as_str();
117117
let loc = self.codegen_span_stable(span);
118118
debug!(?instance, "codegen_intrinsic");
119119
debug!(?fargs, "codegen_intrinsic");
@@ -288,23 +288,6 @@ impl<'tcx> GotocCtx<'tcx> {
288288
}};
289289
}
290290

291-
/// Gets the basename of an intrinsic given its trimmed name.
292-
///
293-
/// For example, given `arith_offset::<u8>` this returns `arith_offset`.
294-
fn intrinsic_basename(name: &str) -> &str {
295-
let scope_sep_count = name.matches("::").count();
296-
// We expect at most one `::` separator from trimmed intrinsic names
297-
debug_assert!(
298-
scope_sep_count < 2,
299-
"expected at most one `::` in intrinsic name, but found {scope_sep_count} in `{name}`"
300-
);
301-
let name_split = name.split_once("::");
302-
if let Some((base_name, _type_args)) = name_split { base_name } else { name }
303-
}
304-
// The trimmed name includes type arguments if the intrinsic was defined
305-
// on generic types, but we only need the basename for the match below.
306-
let intrinsic = intrinsic_basename(intrinsic);
307-
308291
if let Some(stripped) = intrinsic.strip_prefix("simd_shuffle") {
309292
assert!(fargs.len() == 3, "`simd_shuffle` had unexpected arguments {fargs:?}");
310293
let n: u64 = self.simd_shuffle_length(stripped, farg_types, span);

0 commit comments

Comments
 (0)