Monomorphize code via --monomorphize

charon-ml/src/NameMatcher.ml

@@ -1029,7 +1029,7 @@ and const_generic_to_pattern (ctx : ctx) (c : to_pat_config) (m : constraints)
 
 and generic_args_to_pattern (ctx : ctx) (c : to_pat_config) (m : constraints)
     (generics : T.generic_args) : generic_args =
-  let { regions; types; const_generics; trait_refs = _ } : T.generic_args =
+  let ({ regions; types; const_generics; trait_refs = _ } : T.generic_args) =
     generics
   in
   let regions = List.map (region_to_pattern m) regions in

charon-ml/src/PrintTypes.ml

@@ -371,7 +371,7 @@ let trait_clause_to_string (env : 'a fmt_env) (clause : trait_clause) : string =
 
 let generic_params_to_strings (env : 'a fmt_env) (generics : generic_params) :
     string list * string list =
-  let { regions; types; const_generics; trait_clauses; _ } : generic_params =
+  let ({ regions; types; const_generics; trait_clauses; _ } : generic_params) =
     generics
   in
   let regions = List.map region_var_to_string regions in

charon-ml/src/generated/Generated_GAst.ml

@@ -399,6 +399,7 @@ and cli_options = {
   skip_borrowck : bool;
       (** If activated, this skips borrow-checking of the crate. *)
   no_code_duplication : bool;
+  monomorphize : bool;
   extract_opaque_bodies : bool;
       (** Usually we skip the bodies of foreign methods and structs with private fields. When this
         flag is on, we don't.

charon-ml/src/generated/Generated_GAstOfJson.ml

@@ -1611,6 +1611,7 @@ and cli_options_of_json (ctx : of_json_ctx) (js : json) :
           ("use_polonius", use_polonius);
           ("skip_borrowck", skip_borrowck);
           ("no_code_duplication", no_code_duplication);
+          ("monomorphize", monomorphize);
           ("extract_opaque_bodies", extract_opaque_bodies);
           ("translate_all_methods", translate_all_methods);
           ("include", include_);
@@ -1643,6 +1644,7 @@ and cli_options_of_json (ctx : of_json_ctx) (js : json) :
         let* use_polonius = bool_of_json ctx use_polonius in
         let* skip_borrowck = bool_of_json ctx skip_borrowck in
         let* no_code_duplication = bool_of_json ctx no_code_duplication in
+        let* monomorphize = bool_of_json ctx monomorphize 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
@@ -1678,6 +1680,7 @@ and cli_options_of_json (ctx : of_json_ctx) (js : json) :
              use_polonius;
              skip_borrowck;
              no_code_duplication;
+             monomorphize;
              extract_opaque_bodies;
              translate_all_methods;
              included;

charon.opam

@@ -9,6 +9,9 @@ description: """
    Charon. Charon acts as an interface between the rustc compiler and program
    verification projects.  Its purpose is to process Rust .rs files and convert
    them into files easy to handle by program verifiers."""
+maintainer: [
+  "Son Ho" "Jonathan Protzenko" "Aymeric Fromherz" "Sidney Congard"
+]
 authors: ["Son Ho" "Jonathan Protzenko" "Aymeric Fromherz" "Sidney Congard"]
 license: "Apache-2.0"
 homepage: "https://github.com/AeneasVerif/charon"

charon/src/ids/vector.rs

@@ -264,6 +264,17 @@ where
         self.vector.indices()
     }
 
+    pub fn retain(&mut self, mut f: impl FnMut(&mut T) -> bool) {
+        self.vector.iter_mut().for_each(|opt| {
+            if let Some(x) = opt {
+                if !f(x) {
+                    *opt = None;
+                    self.elem_count -= 1;
+                }
+            }
+        });
+    }
+
     /// Like `Vec::split_off`.
     pub fn split_off(&mut self, at: usize) -> Self {
         let mut ret = Self {

charon/src/options.rs

@@ -88,7 +88,7 @@ pub struct CliOpts {
               b0: switch x [true -> goto b1; false -> goto b2]
               b1: y := 0; goto b3
               b2: y := 1; goto b3
-              b3: return y      
+              b3: return y
               ```
 
             We want to reconstruct the control-flow as:
@@ -120,6 +120,9 @@ pub struct CliOpts {
     "))]
     #[serde(default)]
     pub no_code_duplication: bool,
+    #[clap(long = "monomorphize")]
+    #[serde(default)]
+    pub monomorphize: bool,
     /// Usually we skip the bodies of foreign methods and structs with private fields. When this
     /// flag is on, we don't.
     #[clap(long = "extract-opaque-bodies")]
@@ -285,6 +288,8 @@ pub struct TranslateOptions {
     /// Whether to hide the `Sized`, `Sync`, `Send` and `Unpin` marker traits anywhere they show
     /// up.
     pub hide_marker_traits: bool,
+    /// Monomorphize functions.
+    pub monomorphize: bool,
     /// Do not merge the chains of gotos.
     pub no_merge_goto_chains: bool,
     /// Print the llbc just after control-flow reconstruction.
@@ -365,6 +370,7 @@ impl TranslateOptions {
             mir_level,
             no_code_duplication: options.no_code_duplication,
             hide_marker_traits: options.hide_marker_traits,
+            monomorphize: options.monomorphize,
             no_merge_goto_chains: options.no_merge_goto_chains,
             print_built_llbc: options.print_built_llbc,
             item_opacities,

charon/src/transform/check_generics.rs

@@ -237,7 +237,7 @@ impl VisitAst for CheckGenericsVisitor<'_> {
             }
             GenericsSource::Builtin => return,
             GenericsSource::Other => {
-                self.error("`GenericsSource::Other` should now exist in the charon AST");
+                self.error("`GenericsSource::Other` should not exist in the charon AST");
                 return;
             }
         };

charon/src/transform/mod.rs

@@ -13,6 +13,7 @@ pub mod inline_local_panic_functions;
 pub mod insert_assign_return_unit;
 pub mod lift_associated_item_clauses;
 pub mod merge_goto_chains;
+pub mod monomorphize;
 pub mod ops_to_function_calls;
 pub mod prettify_cfg;
 pub mod reconstruct_asserts;
@@ -127,6 +128,8 @@ pub static ULLBC_PASSES: &[Pass] = &[
     // # Micro-pass: remove the drops of locals whose type is `Never` (`!`). This
     // is in preparation of the next transformation.
     UnstructuredBody(&remove_drop_never::Transform),
+    // Monomorphize the functions and types.
+    UnstructuredBody(&monomorphize::Transform),
 ];
 
 /// Body cleanup passes after control flow reconstruction.