Add a flag to control the translation of methods

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.66"
+let supported_charon_version = "0.1.67"

charon-ml/src/generated/Generated_GAst.ml

@@ -413,6 +413,10 @@ and cli_options = {
       (** Usually we skip the bodies of foreign methods and structs with private fields. When this
         flag is on, we don't.
      *)
+  translate_all_methods : bool;
+      (** Usually we skip the provided methods that aren't used. When this flag is on, we translate
+        them all.
+     *)
   included : string list;
       (** Whitelist of items to translate. These use the name-matcher syntax. *)
   opaque : string list;

charon-ml/src/generated/Generated_GAstOfJson.ml

@@ -1624,6 +1624,7 @@ and cli_options_of_json (ctx : of_json_ctx) (js : json) :
           ("use_polonius", use_polonius);
           ("no_code_duplication", no_code_duplication);
           ("extract_opaque_bodies", extract_opaque_bodies);
+          ("translate_all_methods", translate_all_methods);
           ("include", include_);
           ("opaque", opaque);
           ("exclude", exclude);
@@ -1654,6 +1655,7 @@ and cli_options_of_json (ctx : of_json_ctx) (js : json) :
         let* use_polonius = bool_of_json ctx use_polonius in
         let* no_code_duplication = bool_of_json ctx no_code_duplication in
         let* extract_opaque_bodies = bool_of_json ctx extract_opaque_bodies in
+        let* translate_all_methods = bool_of_json ctx translate_all_methods in
         let* included = list_of_json string_of_json ctx include_ in
         let* opaque = list_of_json string_of_json ctx opaque in
         let* exclude = list_of_json string_of_json ctx exclude in
@@ -1687,6 +1689,7 @@ and cli_options_of_json (ctx : of_json_ctx) (js : json) :
              use_polonius;
              no_code_duplication;
              extract_opaque_bodies;
+             translate_all_methods;
              included;
              opaque;
              exclude;

charon/Cargo.toml

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

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

@@ -52,6 +52,9 @@ pub struct TranslateOptions {
     pub item_opacities: Vec<(NamePattern, ItemOpacity)>,
     /// List of traits for which we transform associated types to type parameters.
     pub remove_associated_types: Vec<NamePattern>,
+    /// Usually we skip the provided methods that aren't used. When this flag is on, we translate
+    /// them all.
+    pub translate_all_methods: bool,
 }
 
 impl TranslateOptions {
@@ -123,6 +126,7 @@ impl TranslateOptions {
             mir_level,
             item_opacities,
             remove_associated_types,
+            translate_all_methods: options.translate_all_methods,
         }
     }
 

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

@@ -8,7 +8,6 @@ use hax_frontend_exporter as hax;
 use indexmap::IndexMap;
 use itertools::Itertools;
 use rustc_hir::def_id::DefId;
-use std::collections::HashMap;
 use std::mem;
 use std::sync::Arc;
 
@@ -101,12 +100,14 @@ impl BodyTransCtx<'_, '_> {
                             // `remove_unused_methods` pass.
                             // FIXME: this triggers the translation of traits used in the method
                             // clauses, despite the fact that we may end up not needing them.
-                            let fun_id =
-                                if hax_item.has_value && !item_meta.opacity.is_transparent() {
-                                    bt_ctx.register_fun_decl_id_no_enqueue(item_span, item_def_id)
-                                } else {
-                                    bt_ctx.register_fun_decl_id(item_span, item_def_id)
-                                };
+                            let fun_id = if bt_ctx.t_ctx.options.translate_all_methods
+                                || item_meta.opacity.is_transparent()
+                                || !hax_item.has_value
+                            {
+                                bt_ctx.register_fun_decl_id(item_span, item_def_id)
+                            } else {
+                                bt_ctx.register_fun_decl_id_no_enqueue(item_span, item_def_id)
+                            };
 
                             // TODO: there's probably a cleaner way to write this
                             assert_eq!(bt_ctx.binding_levels.len(), 2);
@@ -278,13 +279,14 @@ impl BodyTransCtx<'_, '_> {
                                     // We insert the `Binder<FunDeclRef>` unconditionally here, and
                                     // remove the ones that correspond to untranslated functions in
                                     // the `remove_unused_methods` pass.
-                                    let fun_id = if *is_override
-                                        && !item_meta.opacity.is_transparent()
+                                    let fun_id = if bt_ctx.t_ctx.options.translate_all_methods
+                                        || item_meta.opacity.is_transparent()
+                                        || !*is_override
                                     {
+                                        bt_ctx.register_fun_decl_id(item_span, item_def_id)
+                                    } else {
                                         bt_ctx
                                             .register_fun_decl_id_no_enqueue(item_span, item_def_id)
-                                    } else {
-                                        bt_ctx.register_fun_decl_id(item_span, item_def_id)
                                     };
 
                                     // TODO: there's probably a cleaner way to write this

charon/src/options.rs

@@ -120,6 +120,11 @@ pub struct CliOpts {
     #[clap(long = "extract-opaque-bodies")]
     #[serde(default)]
     pub extract_opaque_bodies: bool,
+    /// Usually we skip the provided methods that aren't used. When this flag is on, we translate
+    /// them all.
+    #[clap(long = "translate-all-methods")]
+    #[serde(default)]
+    pub translate_all_methods: bool,
     /// Whitelist of items to translate. These use the name-matcher syntax.
     #[clap(
         long = "include",