Skip to content

Remove BuiltinFunId #1164

@Nadrieril

Description

@Nadrieril

Today a function call may refer to a BuiltinFunId instead of a FunDecl item. This is annoying because clients need to special-case these, including knowing their signatures. They're all optional today, and to my knowledge only really used by Aeneas. I'd like to get rid of them and instead use the corresponding std functions:

  • BoxNew is just Box::new;
  • ArrayToSliceShared/ArrayToSliceMut are core::array::to_slice/to_slice_mut;
  • ArrayRepeat is std::array::repeat;
  • the various Index variants have equivalents involving the Index trait;
  • PtrFromParts is std::ptr::from_raw_parts;
  • BoxWrite is Box<MaybeUninit<T>>::write;
  • SliceIntoVec is slice::into_vec.

Because these are for the most part introduced in post-translation passes, we'll need to figure out a way to trigger the translation of these functions during translation when needed. I'm thinking a map from lang_item to ItemId could come useful.

Metadata

Metadata

Assignees

No one assigned

    Labels

    S-representationThis feature requires a nontrivial change to the AST of Charon

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions