Translate intrinsic names

Author: N1ark

charon-ml/src/GAst.ml

@@ -31,7 +31,7 @@ type 'body body =
   | Body of 'body gexpr_body
   | TraitMethodWithoutDefault
   | Extern of string
-  | Intrinsic of string
+  | Intrinsic of { name : string; arg_names : string list }
   | Opaque
   | Missing
   | Error of error

charon-ml/src/LlbcAstUtils.ml

@@ -96,7 +96,12 @@ class ['self] map_crate =
         | Body b -> Body (self#visit_expr_body env b)
         | TraitMethodWithoutDefault -> TraitMethodWithoutDefault
         | Extern sym -> Extern (self#visit_string env sym)
-        | Intrinsic sym -> Intrinsic (self#visit_string env sym)
+        | Intrinsic { name; arg_names } ->
+            Intrinsic
+              {
+                name = self#visit_string env name;
+                arg_names = List.map (self#visit_string env) arg_names;
+              }
         | Opaque -> Opaque
         | Missing -> Missing
         | Error err -> Error (self#visit_error env err)
@@ -231,7 +236,9 @@ class ['self] iter_crate =
       | Body b -> self#visit_expr_body env b
       | TraitMethodWithoutDefault -> ()
       | Extern sym -> self#visit_string env sym
-      | Intrinsic sym -> self#visit_string env sym
+      | Intrinsic { name; arg_names } ->
+          self#visit_string env name;
+          List.iter (self#visit_string env) arg_names
       | Opaque -> ()
       | Missing -> ()
       | Error err -> self#visit_error env err

charon-ml/src/LlbcOfJson.ml

@@ -22,9 +22,12 @@ let expr_body_of_json (ctx : of_json_ctx) (js : json) :
     | `Assoc [ ("Extern", sym) ] ->
         let* sym = string_of_json ctx sym in
         Ok (Extern sym)
-    | `Assoc [ ("Intrinsic", name) ] ->
+    | `Assoc
+        [ ("Intrinsic", `Assoc [ ("name", name); ("arg_names", arg_names) ]) ]
+      ->
         let* name = string_of_json ctx name in
-        Ok (Intrinsic name)
+        let* arg_names = list_of_json string_of_json ctx arg_names in
+        Ok (Intrinsic { name; arg_names })
     | `String "Opaque" -> Ok Opaque
     | `String "Missing" -> Ok Missing
     | `Assoc [ ("Error", e) ] ->

charon-ml/src/PrintGAst.ml

@@ -125,9 +125,9 @@ let gfun_decl_to_string (env : 'a fmt_env) (indent : string)
       fun_sig_with_name_to_string env indent indent_incr
         (Some ("extern:" ^ sym))
         (Some name) None sg
-  | Intrinsic sym ->
+  | Intrinsic { name; _ } ->
       fun_sig_with_name_to_string env indent indent_incr
-        (Some ("intrinsic:" ^ sym))
+        (Some ("intrinsic:" ^ name))
         (Some name) None sg
   | Error err ->
       fun_sig_with_name_to_string env indent indent_incr

charon-ml/src/UllbcOfJson.ml

@@ -20,9 +20,12 @@ let expr_body_of_json (ctx : of_json_ctx) (js : json) :
     | `Assoc [ ("Extern", sym) ] ->
         let* sym = string_of_json ctx sym in
         Ok (Extern sym)
-    | `Assoc [ ("Intrinsic", name) ] ->
+    | `Assoc
+        [ ("Intrinsic", `Assoc [ ("name", name); ("arg_names", arg_names) ]) ]
+      ->
         let* name = string_of_json ctx name in
-        Ok (Intrinsic name)
+        let* arg_names = list_of_json string_of_json ctx arg_names in
+        Ok (Intrinsic { name; arg_names })
     | `String "Opaque" -> Ok Opaque
     | `String "Missing" -> Ok Missing
     | `Assoc [ ("Error", e) ] ->

charon/src/ast/gast.rs

@@ -100,10 +100,17 @@ pub enum Body {
     /// The body of the function item we add for each trait method declaration, if the trait
     /// doesn't provide a default for that method.
     TraitMethodWithoutDefault,
-    /// Function declared in an `extern { ... }` block. The string is the foreign symbol name.
+    /// Function declared in an `extern { ... }` block.
     Extern(#[drive(skip)] String),
     /// Rust intrinsic function.
-    Intrinsic(#[drive(skip)] String),
+    Intrinsic {
+        /// The intrinsic name.
+        #[drive(skip)]
+        name: String,
+        /// The argument names, None if not available.
+        #[drive(skip)]
+        arg_names: Vec<Option<String>>,
+    },
     /// A body that the user chose not to translate, based on opacity settings like
     /// `--include`/`--opaque`.
     Opaque,

charon/src/ast/gast_utils.rs

@@ -16,7 +16,7 @@ impl Body {
             Body::Unstructured(..) | Body::Structured(..) => true,
             Body::TraitMethodWithoutDefault
             | Body::Extern(..)
-            | Body::Intrinsic(..)
+            | Body::Intrinsic { .. }
             | Body::Opaque
             | Body::Missing
             | Body::Error(..) => false,

charon/src/bin/charon-driver/translate/translate_functions.rs

@@ -69,4 +69,25 @@ impl ItemTransCtx<'_, '_> {
         };
         Ok(fun_id)
     }
+
+    /// Translate the names of the arguments of this definition, if they are available,
+    /// otherwise naming arguments `arg0`, `arg1`, etc.
+    /// Note that the names of the arguments are not always available, even when
+    /// we can retrieve the MIR body, in which case we also fall back to `argN`.
+    pub fn translate_argument_names(
+        &mut self,
+        span: Span,
+        def: &hax::FullDef,
+        n_args: usize,
+    ) -> Vec<Option<String>> {
+        let Ok(Some(body)) = self.get_mir(def.this(), span) else {
+            return vec![None; n_args];
+        };
+        body.local_decls
+            .iter_enumerated()
+            .skip(1)
+            .take(body.arg_count)
+            .map(|(index, _)| hax::name_of_local(index, &body.var_debug_info))
+            .collect()
+    }
 }

charon/src/bin/charon-driver/translate/translate_items.rs

@@ -604,9 +604,10 @@ impl ItemTransCtx<'_, '_> {
             .then(|| self.register_item(span, def.this(), TransItemSourceKind::Global));
 
         let body = if let Some(name) = intrinsic_name {
-            Body::Intrinsic(name)
-        } else if let Some(symbol_name) = self.t_ctx.extern_item_symbol_name(def) {
-            Body::Extern(symbol_name)
+            let arg_names = self.translate_argument_names(span, def, signature.inputs.len());
+            Body::Intrinsic { name, arg_names }
+        } else if let Some(name) = self.t_ctx.extern_item_symbol_name(def) {
+            Body::Extern(name)
         } else if item_meta.opacity.with_private_contents().is_opaque() {
             Body::Opaque
         } else if is_trait_method_decl_without_default {

charon/src/pretty/fmt_with_ctx.rs

@@ -252,7 +252,7 @@ impl<C: AstFormatter> FmtWithCtx<C> for gast::Body {
             }
             Body::TraitMethodWithoutDefault => write!(f, "= <method_without_default_body>"),
             Body::Extern(name) => write!(f, "= <extern:{name}>"),
-            Body::Intrinsic(name) => write!(f, "= <intrinsic:{name}>"),
+            Body::Intrinsic { name, .. } => write!(f, "= <intrinsic:{name}>"),
             Body::Opaque => write!(f, "= <opaque>"),
             Body::Missing => write!(f, "= <missing>"),
             Body::Error(error) => write!(f, "= error(\"{}\")", error.msg),
@@ -588,9 +588,19 @@ impl<C: AstFormatter> FmtWithCtx<C> for FunDecl {
         let arg_names = match &self.body {
             Body::Unstructured(body) => args_of_locals(&body.locals),
             Body::Structured(body) => args_of_locals(&body.locals),
+            Body::Intrinsic { arg_names, .. } => arg_names
+                .iter()
+                .enumerate()
+                .map(|(i, name)| {
+                    let id = LocalId::new(i + 1);
+                    match name {
+                        Some(name) => format!("{name}_{id}"),
+                        None => format!("_{id}"),
+                    }
+                })
+                .collect(),
             Body::Error(..)
             | Body::Extern(..)
-            | Body::Intrinsic(..)
             | Body::Missing
             | Body::Opaque
             | Body::TraitMethodWithoutDefault => (0..n_args)