Add an API to get the basename of an intrinsic

[adpaco-aws]

Context: In Kani we used to get the basename of intrinsic instances with mangled_name() until rust-lang/rust#121309 landed in the Rust compiler. Then some intrinsics became inlineable so their names became qualified, and this made our match on the intrinsic name to fail in those cases, leaving them as unsupported constructs as in this example:

warning: Found the following unsupported constructs:
             - _RNvNtCscyGW2MM2t5j_4core10intrinsics8unlikelyCs1eohKeNmpdS_5arith (3)
             - caller_location (1)
             - foreign function (1)
         
         Verification will fail if one or more of these constructs is reachable.
         See https://model-checking.github.io/kani/rust-feature-support.html for more details.

[...]

Failed Checks: _RNvNtCscyGW2MM2t5j_4core10intrinsics8unlikelyCs1eohKeNmpdS_5arith is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/new/choose
 File: "/home/ubuntu/.rustup/toolchains/nightly-2024-02-18-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/num/mod.rs", line 25, in core::num::<impl i8>::checked_add

In model-checking/kani#3048 we switched to using trimmed_name() to work around this, but that API may include type arguments if the intrinsic is defined on generics. So in those cases, we tweak the name to remove the type parameters as follows:

        /// 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);

However, this looks a little fragile and we probably shouldn't be doing it ourselves in the first place. Therefore, would it be possible to add an API to get the basename of an intrinsic? Or, if it's more appropriate, an API that removes the type arguments from the trimmed name as we're doing now.

[oli-obk]

In the compiler we have a intrinsic query that returns just the plain intrinsic name. We could add that info to the InstanceDef::Intrinsic variant, or just provide a way to go from DefId to intrinsic name

[celinval]

I like the idea of adding it to the InstanceKind::Intrinsic variant.

[adpaco-aws]

I've tried adding it to InstanceKind::Intrinsic but Symbol doesn't implement Copy:

error[E0204]: the trait `Copy` cannot be implemented for this type
   --> compiler/stable_mir/src/mir/mono.rs:24:10
    |
24  | #[derive(Copy, Clone, Debug, PartialEq, Eq, Hash)]
    |          ^^^^ in this derive macro expansion
...
29  |     Intrinsic { basename: Symbol },
    |                 ---------------- this field does not implement `Copy`
    |
   ::: /home/ubuntu/rust/library/core/src/marker.rs:411:1
    |
411 | pub macro Copy($item:item) {
    | -------------- in this expansion of `#[derive(Copy)]`

which makes me think that this may not be the best option.

[celinval]

another possibility is to add a method pub fn intrinsic_name(&self) -> Option<Symbol> to Instance

[adpaco-aws]

Closing as this was completed in rust-lang/rust#122203