Rename "assumed" to "builtin"

charon-ml/src/CharonVersion.ml

@@ -1,3 +1,3 @@
 (* This is an automatically generated file, generated from `charon/Cargo.toml`. *)
 (* To re-generate this file, rune `make` in the root directory *)
-let supported_charon_version = "0.1.32"
+let supported_charon_version = "0.1.33"

charon-ml/src/Expressions.ml

@@ -20,30 +20,11 @@ module FunDeclId = Types.FunDeclId
   *)
 type var_id = VarId.id [@@deriving show, ord]
 
-(** An assumed function identifier, identifying a function coming from a
+(** An built-in function identifier, identifying a function coming from a
     standard library.
  *)
 type assumed_fun_id =
   | BoxNew  (** `alloc::boxed::Box::new` *)
-  | BoxFree
-      (** `alloc::alloc::box_free`
-          This is actually an unsafe function, but the rust compiler sometimes
-          introduces it when going to MIR.
-
-          Also, in practice, deallocation is performed as follows in MIR:
-          ```text
-          alloc::alloc::box_free::<T, std::alloc::Global>(
-              move (b.0: std::ptr::Unique<T>),
-              move (b.1: std::alloc::Global))
-          ```
-          When translating from MIR to ULLBC, we do as if the MIR was actually the
-          following (this is hardcoded - see [crate::register] and [crate::translate_functions_to_ullbc]):
-          ```text
-          alloc::alloc::box_free::<T>(move b)
-          ```
-
-          Also see the comments in [crate::assumed::type_to_used_params].
-       *)
   | ArrayIndexShared
       (** Converted from [ProjectionElem::Index].
 
@@ -421,7 +402,7 @@ type operand =
 and aggregate_kind =
   | AggregatedAdt of type_id * variant_id option * generic_args
   | AggregatedArray of ty * const_generic
-      (** We don't put this with the ADT cas because this is the only assumed type
+      (** We don't put this with the ADT cas because this is the only built-in type
           with aggregates, and it is a primitive type. In particular, it makes
           sense to treat it differently because it has a variable number of fields.
        *)

charon-ml/src/GAstOfJson.ml

@@ -361,9 +361,9 @@ and type_id_of_json (js : json) : (type_id, string) result =
         let* adt = type_decl_id_of_json adt in
         Ok (TAdtId adt)
     | `String "Tuple" -> Ok TTuple
-    | `Assoc [ ("Assumed", assumed) ] ->
-        let* assumed = assumed_ty_of_json assumed in
-        Ok (TAssumed assumed)
+    | `Assoc [ ("Builtin", builtin) ] ->
+        let* builtin = assumed_ty_of_json builtin in
+        Ok (TAssumed builtin)
     | _ -> Error "")
 
 and const_generic_of_json (js : json) : (const_generic, string) result =
@@ -915,7 +915,6 @@ and assumed_fun_id_of_json (js : json) : (assumed_fun_id, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with
     | `String "BoxNew" -> Ok BoxNew
-    | `String "BoxFree" -> Ok BoxFree
     | `String "ArrayIndexShared" -> Ok ArrayIndexShared
     | `String "ArrayIndexMut" -> Ok ArrayIndexMut
     | `String "ArrayToSliceShared" -> Ok ArrayToSliceShared
@@ -931,9 +930,9 @@ and fun_id_of_json (js : json) : (fun_id, string) result =
     | `Assoc [ ("Regular", regular) ] ->
         let* regular = fun_decl_id_of_json regular in
         Ok (FRegular regular)
-    | `Assoc [ ("Assumed", assumed) ] ->
-        let* assumed = assumed_fun_id_of_json assumed in
-        Ok (FAssumed assumed)
+    | `Assoc [ ("Builtin", builtin) ] ->
+        let* builtin = assumed_fun_id_of_json builtin in
+        Ok (FAssumed builtin)
     | _ -> Error "")
 
 and fun_id_or_trait_method_ref_of_json (js : json) :

charon-ml/src/NameMatcher.ml

@@ -612,7 +612,6 @@ and match_expr_with_const_generic (ctx : ctx) (c : match_config) (m : maps)
 let assumed_fun_id_to_string (fid : E.assumed_fun_id) : string =
   match fid with
   | BoxNew -> "alloc::boxed::{Box<@T, alloc::alloc::Global>}::new"
-  | BoxFree -> "alloc::alloc::box_free"
   | ArrayIndexShared -> "ArrayIndexShared"
   | ArrayIndexMut -> "ArrayIndexMut"
   | ArrayToSliceShared -> "ArrayToSliceShared"
@@ -655,9 +654,6 @@ let match_fn_ptr (ctx : ctx) (c : match_config) (p : pattern) (func : E.fn_ptr)
                   true
               | _ -> false)
           | _ -> false)
-      | BoxFree ->
-          let name = to_name [ "alloc"; "alloc"; "box_free" ] in
-          match_name_with_generics ctx c p name func.generics
       | _ ->
           let name = assumed_fun_id_to_string fid in
           match_name_with_generics ctx c p (to_name [ name ]) func.generics)
@@ -998,12 +994,6 @@ let fn_ptr_to_pattern (ctx : ctx) (c : to_pat_config)
               PImpl (EComp box_impl);
               PIdent ("new", args);
             ]
-        | BoxFree ->
-            [
-              PIdent ("alloc", []);
-              PIdent ("alloc", []);
-              PIdent ("box_free", args);
-            ]
         | _ ->
             let fid = assumed_fun_id_to_string fid in
             [ PIdent (fid, args) ])

charon-ml/src/PrintExpressions.ml

@@ -100,7 +100,6 @@ let binop_to_string (binop : binop) : string =
 let assumed_fun_id_to_string (aid : assumed_fun_id) : string =
   match aid with
   | BoxNew -> "alloc::boxed::Box::new"
-  | BoxFree -> "alloc::alloc::box_free"
   | ArrayIndexShared -> "@ArrayIndexShared"
   | ArrayIndexMut -> "@ArrayIndexMut"
   | ArrayToSliceShared -> "@ArrayToSliceShared"

charon-ml/src/Types.ml

@@ -283,16 +283,16 @@ class virtual ['self] map_ty_base =
         { index; name }
   end
 
-(** Assumed types identifiers.
+(** Builtin types identifiers.
 
-    WARNING: for now, all the assumed types are covariant in the generic
+    WARNING: for now, all the built-in types are covariant in the generic
     parameters (if there are). Adding types which don't satisfy this
     will require to update the code abstracting the signatures (to properly
     take into account the lifetime constraints).
 
     TODO: update to not hardcode the types (except `Box` maybe) and be more
     modular.
-    TODO: move to assumed.rs?
+    TODO: move to builtins.rs?
  *)
 type assumed_ty =
   | TBox  (** Boxes are de facto a primitive type. *)
@@ -302,7 +302,7 @@ type assumed_ty =
 
 (** Type identifier.
 
-    Allows us to factorize the code for assumed types, adts and tuples
+    Allows us to factorize the code for built-in types, adts and tuples
  *)
 and type_id =
   | TAdtId of type_decl_id
@@ -313,12 +313,12 @@ and type_id =
        *)
   | TTuple
   | TAssumed of assumed_ty
-      (** Assumed type. Either a primitive type like array or slice, or a
+      (** Built-in type. Either a primitive type like array or slice, or a
           non-primitive type coming from a standard library
           and that we handle like a primitive type. Types falling into this
           category include: Box, Vec, Cell...
           The Array and Slice types were initially modelled as primitive in
-          the [Ty] type. We decided to move them to assumed types as it allows
+          the [Ty] type. We decided to move them to built-in types as it allows
           for more uniform treatment throughout the codebase.
        *)
 
@@ -335,7 +335,7 @@ and ty =
           Note that here ADTs are very general. They can be:
           - user-defined ADTs
           - tuples (including `unit`, which is a 0-tuple)
-          - assumed types (includes some primitive types, e.g., arrays or slices)
+          - built-in types (includes some primitive types, e.g., arrays or slices)
           The information on the nature of the ADT is stored in (`TypeId`)[TypeId].
           The last list is used encode const generics, e.g., the size of an array
 

charon/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "charon"
-version = "0.1.32"
+version = "0.1.33"
 authors = ["Son Ho <hosonmarc@gmail.com>"]
 edition = "2021"
 license = "Apache-2.0"

charon/src/ast/assumed.rs → charon/src/ast/builtins.rs

@@ -1,4 +1,4 @@
-//! This file contains information about the assumed functions/types/traits definitions
+//! This file contains information about the builtin functions/types/traits definitions
 //!
 //! **IMPORTANT**:
 //! When checking whether names are equal to one of the reference names below,
@@ -14,7 +14,7 @@ use macros::EnumIsA;
 // We treat this one specially in the `inline_local_panic_functions` pass. See there for details.
 pub static EXPLICIT_PANIC_NAME: &[&str] = &["core", "panicking", "panic_explicit"];
 
-/// We redefine identifiers for assumed functions here, instead of reusing the
+/// We redefine identifiers for built-in functions here, instead of reusing the
 /// identifiers from [ullbc_ast], because:
 /// - some of the functions (the panic functions) will actually not be translated
 ///   to functions: there are thus missing identifiers.
@@ -24,63 +24,42 @@ pub static EXPLICIT_PANIC_NAME: &[&str] = &["core", "panicking", "panic_explicit
 pub enum BuiltinFun {
     Panic,
     BoxNew,
-    BoxFree,
-}
-
-pub struct FunInfo {
-    pub used_type_params: Vec<bool>,
-    // TODO: rename. "value_args"?
-    pub used_args: Vec<bool>,
 }
 
 impl BuiltinFun {
     /// Converts to the ullbc equivalent. Panics if `self` is `Panic` as this should be handled
     /// separately.
-    pub fn to_ullbc_builtin_fun(self) -> ast::AssumedFunId {
+    pub fn to_ullbc_builtin_fun(self) -> ast::BuiltinFunId {
         match self {
-            BuiltinFun::BoxNew => ast::AssumedFunId::BoxNew,
-            BuiltinFun::BoxFree => ast::AssumedFunId::BoxFree,
+            BuiltinFun::BoxNew => ast::BuiltinFunId::BoxNew,
             BuiltinFun::Panic => panic!(),
         }
     }
-
-    /// See the comments for [type_to_used_params]
-    pub fn to_fun_info(self) -> Option<FunInfo> {
-        match self {
-            BuiltinFun::Panic => None,
-            BuiltinFun::BoxNew => None,
-            BuiltinFun::BoxFree => Some(FunInfo {
-                used_type_params: vec![true, false],
-                used_args: vec![true, false],
-            }),
-        }
-    }
 }
 
-impl AssumedTy {
+impl BuiltinTy {
     pub fn get_name(self) -> Name {
         let name: &[_] = match self {
-            AssumedTy::Box => &["alloc", "boxed", "Box"],
-            AssumedTy::Str => &["Str"],
-            AssumedTy::Array => &["Array"],
-            AssumedTy::Slice => &["Slice"],
+            BuiltinTy::Box => &["alloc", "boxed", "Box"],
+            BuiltinTy::Str => &["Str"],
+            BuiltinTy::Array => &["Array"],
+            BuiltinTy::Slice => &["Slice"],
         };
         Name::from_path(name)
     }
 }
 
-/// When translating from MIR to ULLBC, we ignore some type parameters for some
-/// assumed types.
+/// When translating from MIR to ULLBC, we ignore some type parameters for some builtin types.
 /// For instance, many types like box or vec are parameterized (in MIR) by an allocator
 /// (`std::alloc::Allocator`): we ignore it.
-pub fn type_to_used_params(id: AssumedTy) -> Vec<bool> {
+pub fn type_to_used_params(id: BuiltinTy) -> Vec<bool> {
     match id {
-        AssumedTy::Box => {
+        BuiltinTy::Box => {
             vec![true, false]
         }
-        AssumedTy::Str => {
+        BuiltinTy::Str => {
             vec![]
         }
-        AssumedTy::Array | AssumedTy::Slice => vec![true],
+        BuiltinTy::Array | BuiltinTy::Slice => vec![true],
     }
 }

charon/src/ast/expressions.rs

@@ -268,10 +268,11 @@ pub enum FunId {
     /// A primitive function, coming from a standard library (for instance:
     /// `alloc::boxed::Box::new`).
     /// TODO: rename to "Primitive"
-    Assumed(AssumedFunId),
+    #[charon::rename("FAssumed")]
+    Builtin(BuiltinFunId),
 }
 
-/// An assumed function identifier, identifying a function coming from a
+/// An built-in function identifier, identifying a function coming from a
 /// standard library.
 #[derive(
     Debug,
@@ -287,27 +288,10 @@ pub enum FunId {
     Drive,
     DriveMut,
 )]
-pub enum AssumedFunId {
+#[charon::rename("AssumedFunId")]
+pub enum BuiltinFunId {
     /// `alloc::boxed::Box::new`
     BoxNew,
-    /// `alloc::alloc::box_free`
-    /// This is actually an unsafe function, but the rust compiler sometimes
-    /// introduces it when going to MIR.
-    ///
-    /// Also, in practice, deallocation is performed as follows in MIR:
-    /// ```text
-    /// alloc::alloc::box_free::<T, std::alloc::Global>(
-    ///     move (b.0: std::ptr::Unique<T>),
-    ///     move (b.1: std::alloc::Global))
-    /// ```
-    /// When translating from MIR to ULLBC, we do as if the MIR was actually the
-    /// following (this is hardcoded - see [crate::register] and [crate::translate_functions_to_ullbc]):
-    /// ```text
-    /// alloc::alloc::box_free::<T>(move b)
-    /// ```
-    ///
-    /// Also see the comments in [crate::assumed::type_to_used_params].
-    BoxFree,
     /// Converted from [ProjectionElem::Index].
     ///
     /// Signature: `fn<T,N>(&[T;N], usize) -> &T`
@@ -565,7 +549,7 @@ pub enum Rvalue {
 #[charon::variants_prefix("Aggregated")]
 pub enum AggregateKind {
     Adt(TypeId, Option<VariantId>, GenericArgs),
-    /// We don't put this with the ADT cas because this is the only assumed type
+    /// We don't put this with the ADT cas because this is the only built-in type
     /// with aggregates, and it is a primitive type. In particular, it makes
     /// sense to treat it differently because it has a variable number of fields.
     Array(Ty, ConstGeneric),

charon/src/ast/gast_utils.rs

@@ -18,8 +18,8 @@ pub fn make_locals_generator(locals: &mut Vector<VarId, Var>) -> impl FnMut(Ty)
 }
 
 impl FunIdOrTraitMethodRef {
-    pub fn mk_assumed(aid: AssumedFunId) -> Self {
-        Self::Fun(FunId::Assumed(aid))
+    pub fn mk_builtin(aid: BuiltinFunId) -> Self {
+        Self::Fun(FunId::Builtin(aid))
     }
 }
 

charon/src/ast/mod.rs

@@ -1,4 +1,4 @@
-pub mod assumed;
+pub mod builtins;
 pub mod expressions;
 pub mod expressions_utils;
 pub mod gast;
@@ -18,7 +18,7 @@ pub mod values;
 pub mod values_utils;
 
 // Re-export everything except llbc/ullbc, for convenience.
-pub use assumed::*;
+pub use builtins::*;
 pub use expressions::*;
 pub use gast::*;
 pub use krate::*;