Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Use intrinsic_name to get the intrinsic name #3114

Merged
merged 2 commits into from
Mar 28, 2024
Merged

Use intrinsic_name to get the intrinsic name #3114

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
8768e48
Use `intrinsic_name` instead of complicated things
adpaco-aws Mar 27, 2024
aca0310
Merge branch 'main' into intrinsic-name
adpaco-aws Mar 27, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
23 changes: 3 additions & 20 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
View file
Open in desktop
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
Loading