Add precise filtering of which items to translate

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.26"
+let supported_charon_version = "0.1.27"

charon-ml/src/GAstOfJson.ml

@@ -1401,6 +1401,7 @@ and gtranslated_crate_of_json
     | `Assoc
         [
           ("crate_name", name);
+          ("real_crate_name", _);
           ("id_to_file", id_to_file);
           ("all_ids", _);
           ("type_decls", types);

charon-ml/src/LlbcOfJson.ml

@@ -181,43 +181,42 @@ let split_global (gid_conv : global_id_converter) global :
   (global_decl, fun_decl)
 
 let crate_of_json (js : json) : (crate, string) result =
-  combine_error_msgs js __FUNCTION__
-    begin
-      let* crate = gcrate_of_json expr_body_of_json js in
-      (* When deserializing the globals, we split the global declarations
-       * between the globals themselves and their bodies, which are simply
-       * functions with no arguments. We add the global bodies to the list
-       * of function declarations: the (fresh) ids we use for those bodies
-       * are simply given by: [num_functions + global_id] *)
-      let gid_conv =
-        { fun_count = List.length (FunDeclId.Map.bindings crate.fun_decls) }
-      in
-      let globals, global_bodies =
-        List.split
-          (List.map
-             (fun (_, g) -> split_global gid_conv g)
-             (GlobalDeclId.Map.bindings crate.global_decls))
-      in
+  begin
+    let* crate = gcrate_of_json expr_body_of_json js in
+    (* When deserializing the globals, we split the global declarations
+     * between the globals themselves and their bodies, which are simply
+     * functions with no arguments. We add the global bodies to the list
+     * of function declarations: the (fresh) ids we use for those bodies
+     * are simply given by: [num_functions + global_id] *)
+    let gid_conv =
+      { fun_count = List.length (FunDeclId.Map.bindings crate.fun_decls) }
+    in
+    let globals, global_bodies =
+      List.split
+        (List.map
+           (fun (_, g) -> split_global gid_conv g)
+           (GlobalDeclId.Map.bindings crate.global_decls))
+    in
 
-      (* Add the global bodies to the list of functions *)
-      let fun_decls =
-        List.fold_left
-          (fun m (d : fun_decl) -> FunDeclId.Map.add d.def_id d m)
-          crate.fun_decls global_bodies
-      in
-      let global_decls =
-        GlobalDeclId.Map.of_list
-          (List.map (fun (d : global_decl) -> (d.def_id, d)) globals)
-      in
+    (* Add the global bodies to the list of functions *)
+    let fun_decls =
+      List.fold_left
+        (fun m (d : fun_decl) -> FunDeclId.Map.add d.def_id d m)
+        crate.fun_decls global_bodies
+    in
+    let global_decls =
+      GlobalDeclId.Map.of_list
+        (List.map (fun (d : global_decl) -> (d.def_id, d)) globals)
+    in
 
-      Ok
-        {
-          name = crate.name;
-          declarations = crate.declarations;
-          type_decls = crate.type_decls;
-          fun_decls;
-          global_decls;
-          trait_decls = crate.trait_decls;
-          trait_impls = crate.trait_impls;
-        }
-    end
+    Ok
+      {
+        name = crate.name;
+        declarations = crate.declarations;
+        type_decls = crate.type_decls;
+        fun_decls;
+        global_decls;
+        trait_decls = crate.trait_decls;
+        trait_impls = crate.trait_impls;
+      }
+  end

charon-ml/tests/Test_NameMatcher.ml

@@ -159,7 +159,7 @@ module PatternTest = struct
     else true
 end
 
-(* This reads the output generated from the `ui/name-matcher-tests.rs` test
+(* This reads the output generated from the `ui/ml-name-matcher-tests.rs` test
    file, and verifies that for each `#[pattern::...]` annotation, the item
    matches the pattern. See the `PatternTest` module for details of what
    annotations are available. *)

charon-ml/tests/Tests.ml

@@ -15,4 +15,5 @@ let () =
 let () = Test_Deserialize.run_tests "../../../tests/serialized"
 
 let () =
-  Test_NameMatcher.run_tests "../../../tests/serialized/name-matcher-tests.llbc"
+  Test_NameMatcher.run_tests
+    "../../../tests/serialized/ml-name-matcher-tests.llbc"

charon/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "charon"
-version = "0.1.26"
+version = "0.1.27"
 authors = ["Son Ho <hosonmarc@gmail.com>"]
 edition = "2021"
 
@@ -50,9 +50,12 @@ env_logger = { version = "0.11", features = ["color"] }
 hashlink = { version = "0.9", features = ["serde_impl"] }
 im = "15.1.0"
 index_vec = { version = "0.1.3", features = ["serde"] }
+indoc = "2"
 itertools = "0.13"
 lazy_static = "1.4.0"
 log = "0.4.17"
+nom = "7.1.3"
+nom-supreme = "0.8.0"
 petgraph = "0.6.2"
 pretty = "0.12"
 regex = "1.7.1"

charon/src/ast/assumed.rs

@@ -5,8 +5,9 @@
 //! we ignore the disambiguators (see [crate::names] and [crate::names_utils]).
 // TODO: rename to "primitive"
 
+use crate::ast;
+use crate::names::*;
 use crate::types::*;
-use crate::ullbc_ast;
 use macros::EnumIsA;
 
 // Built-in functions
@@ -35,10 +36,10 @@ pub struct FunInfo {
 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) -> ullbc_ast::AssumedFunId {
+    pub fn to_ullbc_builtin_fun(self) -> ast::AssumedFunId {
         match self {
-            BuiltinFun::BoxNew => ullbc_ast::AssumedFunId::BoxNew,
-            BuiltinFun::BoxFree => ullbc_ast::AssumedFunId::BoxFree,
+            BuiltinFun::BoxNew => ast::AssumedFunId::BoxNew,
+            BuiltinFun::BoxFree => ast::AssumedFunId::BoxFree,
             BuiltinFun::Panic => panic!(),
         }
     }
@@ -56,14 +57,16 @@ impl BuiltinFun {
     }
 }
 
-pub fn get_name_from_type_id(id: AssumedTy) -> Vec<String> {
-    let name: &[_] = match id {
-        AssumedTy::Box => &["alloc", "boxed", "Box"],
-        AssumedTy::Str => &["Str"],
-        AssumedTy::Array => &["Array"],
-        AssumedTy::Slice => &["Slice"],
-    };
-    name.iter().map(|s| s.to_string()).collect()
+impl AssumedTy {
+    pub fn get_name(self) -> Name {
+        let name: &[_] = match self {
+            AssumedTy::Box => &["alloc", "boxed", "Box"],
+            AssumedTy::Str => &["Str"],
+            AssumedTy::Array => &["Array"],
+            AssumedTy::Slice => &["Slice"],
+        };
+        Name::from_path(name)
+    }
 }
 
 /// When translating from MIR to ULLBC, we ignore some type parameters for some

charon/src/ast/krate.rs

@@ -81,8 +81,11 @@ pub enum AnyTransItem<'ctx> {
 /// The data of a translated crate.
 #[derive(Default, Clone, Drive, DriveMut, Serialize, Deserialize)]
 pub struct TranslatedCrate {
-    /// The name of the crate.
+    /// The name that the user requested for the crate. This may differ from what rustc reports as
+    /// the name of the crate.
     pub crate_name: String,
+    /// The name of the crate according to rustc.
+    pub real_crate_name: String,
 
     /// File names to ids and vice-versa
     #[drive(skip)]

charon/src/ast/names_utils.rs

@@ -3,7 +3,6 @@
 //! For now, we have one function per object kind (type, trait, function,
 //! module): many of them could be factorized (will do).
 use crate::names::*;
-use std::collections::HashSet;
 
 impl PathElem {
     fn equals_ident(&self, id: &str) -> bool {
@@ -56,29 +55,4 @@ impl Name {
     pub fn equals_ref_name(&self, ref_name: &[&str]) -> bool {
         self.compare_with_ref_name(true, ref_name)
     }
-
-    /// Compare the name to a constant array.
-    /// This ignores disambiguators.
-    pub fn prefix_is_same(&self, ref_name: &[&str]) -> bool {
-        self.compare_with_ref_name(false, ref_name)
-    }
-
-    /// Return `true` if the name identifies an item inside the module: `krate::module`
-    pub fn is_in_module(&self, krate: &String, module: &String) -> bool {
-        self.prefix_is_same(&[krate, module])
-    }
-
-    /// Similar to [Name::is_in_module]
-    pub fn is_in_modules(&self, krate: &String, modules: &HashSet<String>) -> bool {
-        if self.len() >= 2 {
-            match (&self.name[0], &self.name[1]) {
-                (PathElem::Ident(s0, _), PathElem::Ident(s1, _)) => {
-                    s0 == krate && modules.contains(s1)
-                }
-                _ => false,
-            }
-        } else {
-            false
-        }
-    }
 }

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

@@ -1,7 +1,6 @@
 use crate::translate::translate_crate_to_ullbc;
 use charon_lib::export;
 use charon_lib::options;
-use charon_lib::options::MirLevel;
 use charon_lib::reorder_decls::compute_reordered_decls;
 use charon_lib::transform::{LLBC_PASSES, ULLBC_PASSES};
 use charon_lib::ullbc_to_llbc;
@@ -203,26 +202,6 @@ pub fn translate(tcx: TyCtxt, internal: &mut CharonCallbacks) -> export::CrateDa
     trace!();
     let options = &internal.options;
 
-    // Retrieve the crate name: if the user specified a custom name, use
-    // it, otherwise retrieve it from Rustc.
-    let crate_name: String = options.crate_name.as_deref().map_or_else(
-        || {
-            tcx.crate_name(rustc_span::def_id::LOCAL_CRATE)
-                .to_ident_string()
-        },
-        |x: &str| x.to_string(),
-    );
-    trace!("# Crate: {}", crate_name);
-
-    // Adjust the level of MIR we extract, depending on the options
-    let mir_level = if options.mir_optimized {
-        MirLevel::Optimized
-    } else if options.mir_promoted {
-        MirLevel::Promoted
-    } else {
-        MirLevel::Built
-    };
-
     // Some important notes about crates and how to interact with rustc:
     // - when calling rustc, we should give it the root of the crate, for
     //   instance the "main.rs" file. From there, rustc will load all the
@@ -233,7 +212,7 @@ pub fn translate(tcx: TyCtxt, internal: &mut CharonCallbacks) -> export::CrateDa
     // # Translate the declarations in the crate.
     // We translate the declarations in an ad-hoc order, and do not group
     // the mutually recursive groups - we do this in the next step.
-    let mut ctx = translate_crate_to_ullbc::translate(crate_name, options, tcx, mir_level);
+    let mut ctx = translate_crate_to_ullbc::translate(options, tcx);
 
     if options.print_ullbc {
         info!("# ULLBC after translation from MIR:\n\n{ctx}\n");