Skip to content

Commit

Permalink
Use intrinsic_name to get the intrinsic name (#3114)
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
adpaco-aws committed Mar 28, 2024
1 parent f5f1e94 commit d2b8c27
Showing 1 changed file with 3 additions and 20 deletions.
23 changes: 3 additions & 20 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -69,7 +69,7 @@ impl<'tcx> GotocCtx<'tcx> {
/// Handles codegen for non returning intrinsics
/// Non returning intrinsics are not associated with a destination
pub fn codegen_never_return_intrinsic(&mut self, instance: Instance, span: Span) -> Stmt {
let intrinsic = instance.mangled_name();
let intrinsic = instance.intrinsic_name().unwrap();

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

Expand Down Expand Up @@ -112,8 +112,8 @@ impl<'tcx> GotocCtx<'tcx> {
place: &Place,
span: Span,
) -> Stmt {
let intrinsic_sym = instance.trimmed_name();
let intrinsic = intrinsic_sym.as_str();
let intrinsic_name = instance.intrinsic_name().unwrap();
let intrinsic = intrinsic_name.as_str();
let loc = self.codegen_span_stable(span);
debug!(?instance, "codegen_intrinsic");
debug!(?fargs, "codegen_intrinsic");
Expand Down Expand Up @@ -288,23 +288,6 @@ impl<'tcx> GotocCtx<'tcx> {
}};
}

/// Gets the basename of an intrinsic given its trimmed name.
///
/// For example, given `arith_offset::<u8>` this returns `arith_offset`.
fn intrinsic_basename(name: &str) -> &str {
let scope_sep_count = name.matches("::").count();
// We expect at most one `::` separator from trimmed intrinsic names
debug_assert!(
scope_sep_count < 2,
"expected at most one `::` in intrinsic name, but found {scope_sep_count} in `{name}`"
);
let name_split = name.split_once("::");
if let Some((base_name, _type_args)) = name_split { base_name } else { name }
}
// The trimmed name includes type arguments if the intrinsic was defined
// on generic types, but we only need the basename for the match below.
let intrinsic = intrinsic_basename(intrinsic);

if let Some(stripped) = intrinsic.strip_prefix("simd_shuffle") {
assert!(fargs.len() == 3, "`simd_shuffle` had unexpected arguments {fargs:?}");
let n: u64 = self.simd_shuffle_length(stripped, farg_types, span);
Expand Down

0 comments on commit d2b8c27

Please sign in to comment.