Cleanup a bit and explore crates starting with the root module

charon-ml/src/PrintGAst.ml

@@ -118,8 +118,8 @@ let gfun_decl_to_string (env : ('a, 'b) fmt_env) (indent : string)
       in
 
       (* Put everything together *)
-      fun_sig_with_name_to_string env indent indent_incr (Some "opaque")
-        (Some name) (Some inputs) sg
+      fun_sig_with_name_to_string env indent indent_incr None (Some name)
+        (Some inputs) sg
       ^ indent ^ "\n{\n" ^ locals ^ "\n\n" ^ body ^ "\n" ^ indent ^ "}"
 
 let trait_decl_to_string (env : ('a, 'b) fmt_env) (indent : string)

charon/src/assumed.rs

@@ -80,7 +80,7 @@ pub fn is_marker_trait(name: &Name) -> bool {
     false
 }
 
-pub fn get_type_id_from_name(name: &TypeName) -> Option<AssumedTy> {
+pub fn get_type_id_from_name(name: &Name) -> Option<AssumedTy> {
     if name.equals_ref_name(&BOX_NAME) {
         Option::Some(AssumedTy::Box)
     } else if name.equals_ref_name(&PTR_UNIQUE_NAME) {
@@ -103,7 +103,7 @@ pub fn get_name_from_type_id(id: AssumedTy) -> Vec<String> {
     }
 }
 
-fn get_fun_id_from_name_full(name: &FunName) -> Option<FunId> {
+fn get_fun_id_from_name_full(name: &Name) -> Option<FunId> {
     if name.equals_ref_name(&PANIC_NAME) {
         Option::Some(FunId::Panic)
     } else if name.equals_ref_name(&BEGIN_PANIC_NAME) {
@@ -148,7 +148,7 @@ fn get_fun_id_from_name_full(name: &FunName) -> Option<FunId> {
     }
 }
 
-pub fn get_fun_id_from_name(name: &FunName) -> Option<ullbc_ast::AssumedFunId> {
+pub fn get_fun_id_from_name(name: &Name) -> Option<ullbc_ast::AssumedFunId> {
     match get_fun_id_from_name_full(name) {
         Option::Some(id) => {
             let id = match id {
@@ -166,7 +166,7 @@ pub fn get_fun_id_from_name(name: &FunName) -> Option<ullbc_ast::AssumedFunId> {
 /// assumed 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(name: &TypeName) -> Option<Vec<bool>> {
+pub fn type_to_used_params(name: &Name) -> Option<Vec<bool>> {
     trace!("{:?}", name);
     match get_type_id_from_name(name) {
         Option::None => Option::None,
@@ -195,7 +195,7 @@ pub struct FunInfo {
 }
 
 /// See the comments for [type_to_used_params]
-pub fn function_to_info(name: &FunName) -> Option<FunInfo> {
+pub fn function_to_info(name: &Name) -> Option<FunInfo> {
     trace!("{:?}", name);
     match get_fun_id_from_name_full(name) {
         Option::None => Option::None,

charon/src/gast.rs

@@ -4,8 +4,7 @@
 pub use crate::expressions::*;
 pub use crate::gast_utils::*;
 use crate::meta::Meta;
-use crate::names::GlobalName;
-use crate::names::{FunName, Name};
+use crate::names::Name;
 pub use crate::types::GlobalDeclId;
 pub use crate::types::TraitClauseId;
 use crate::types::*;
@@ -95,7 +94,7 @@ pub struct GFunDecl<T> {
     pub def_id: FunDeclId::Id,
     /// The meta data associated with the declaration.
     pub meta: Meta,
-    pub name: FunName,
+    pub name: Name,
     /// The signature contains the inputs/output types *with* non-erased regions.
     /// It also contains the list of region and type parameters.
     pub signature: FunSig,
@@ -113,7 +112,7 @@ pub struct GGlobalDecl<T> {
     pub def_id: GlobalDeclId::Id,
     /// The meta data associated with the declaration.
     pub meta: Meta,
-    pub name: GlobalName,
+    pub name: Name,
     pub ty: Ty,
     pub body: Option<GExprBody<T>>,
 }

charon/src/names.rs

@@ -63,11 +63,3 @@ pub struct ImplElem {
 pub struct Name {
     pub name: Vec<PathElem>,
 }
-
-// TODO: remove those
-pub type ModuleName = Name;
-pub type TypeName = Name;
-pub type ItemName = Name;
-pub type FunName = Name;
-pub type GlobalName = Name;
-pub type HirItemName = Name;

charon/src/names_utils.rs

@@ -217,7 +217,7 @@ impl Serialize for Name {
 
 impl<'tcx, 'ctx> TransCtx<'tcx, 'ctx> {
     /// Retrieve an item name from a [DefId].
-    pub fn extended_def_id_to_name(&mut self, def_id: &hax::ExtendedDefId) -> ItemName {
+    pub fn extended_def_id_to_name(&mut self, def_id: &hax::ExtendedDefId) -> Name {
         trace!("{:?}", def_id);
 
         // We have to be a bit careful when retrieving names from def ids. For instance,
@@ -395,7 +395,7 @@ impl<'tcx, 'ctx> TransCtx<'tcx, 'ctx> {
     ///
     /// Rk.: this function is only used by [crate::register], and implemented with this
     /// context in mind.
-    pub fn hir_item_to_name(&mut self, item: &Item) -> Option<HirItemName> {
+    pub fn hir_item_to_name(&mut self, item: &Item) -> Option<Name> {
         // We have to create a hax state, which is annoying...
         let state = self.make_hax_state_with_id(item.owner_id.to_def_id());
         let def_id = item.owner_id.to_def_id().sinto(&state);
@@ -429,12 +429,12 @@ impl<'tcx, 'ctx> TransCtx<'tcx, 'ctx> {
     }
 
     // TODO: remove
-    pub fn item_def_id_to_name(&mut self, def_id: rustc_span::def_id::DefId) -> ItemName {
+    pub fn item_def_id_to_name(&mut self, def_id: rustc_span::def_id::DefId) -> Name {
         let state = self.make_hax_state_with_id(def_id);
         self.extended_def_id_to_name(&def_id.sinto(&state))
     }
 
-    pub fn def_id_to_name(&mut self, def_id: &hax::DefId) -> ItemName {
+    pub fn def_id_to_name(&mut self, def_id: &hax::DefId) -> Name {
         // We have to create a hax state, which is annoying...
         let state = self.make_hax_state_with_id(def_id.rust_def_id.unwrap());
         self.extended_def_id_to_name(&def_id.rust_def_id.unwrap().sinto(&state))

charon/src/translate_crate_to_ullbc.rs

@@ -83,16 +83,19 @@ impl<'tcx, 'ctx> TransCtx<'tcx, 'ctx> {
             match self.hir_item_to_name(item) {
                 Option::None => {
                     // This kind of item is to be ignored
+                    trace!("Ignoring {:?} (ignoring item kind)", item.item_id());
                     return;
                 }
                 Option::Some(item_name) => {
                     if self.crate_info.is_opaque_decl(&item_name) {
+                        trace!("Ignoring {:?} (marked as opaque)", item.item_id());
                         return;
                     }
                     // Continue
                 }
             }
         }
+        trace!("Registering {:?}", item.item_id());
 
         // Case disjunction on the item kind.
         let def_id = item.owner_id.to_def_id();
@@ -239,13 +242,21 @@ pub fn translate<'tcx, 'ctx>(
 
     // First push all the items in the stack of items to translate.
     //
-    // The way rustc works is as follows:
-    // - we call it on the root of the crate (for instance "main.rs"), and it
-    //   explores all the files from there (typically listed through statements
-    //   of the form "mod MODULE_NAME")
-    // - the other files in the crate are Module items in the HIR graph
+    // We explore the crate by starting with the root module.
+    //
+    // Remark: It is important to do like this (and not iterate over all the items)
+    // if we want the "opaque" options (to ignore parts of the crate) to work.
+    // For instance, if we mark "foo::bar" as opaque, we will ignore the module
+    // "foo::bar" altogether (we will not even look at the items).
+    // If we look at the items, we risk registering items just by looking
+    // at their name. For instance, if we check the item `foo::bar::{foo::bar::Ty}::f`,
+    // then by converting the Rust name to an LLBC name, we will actually register
+    // the name "foo::bar::Ty" (so that we can generate the "impl" path element
+    // `{foo::bar::Ty}`), which means we will register the item `foo::bar::Ty`.
+    // We could make the name translation work differently if we do have to
+    // explore all the items in the crate.
     let hir = tcx.hir();
-    for item_id in hir.items() {
+    for item_id in hir.root_module().item_ids {
         let item_id = item_id.hir_id();
         let node = hir.find(item_id).unwrap();
         let item = match node {

charon/src/translate_ctx.rs

@@ -421,9 +421,7 @@ impl<'tcx, 'ctx> TransCtx<'tcx, 'ctx> {
         {
             // Retrieve the id of the implemented trait decl
             let id = self.tcx.trait_id_of_impl(rust_id).unwrap();
-            if self.register_trait_decl_id(id).is_none() {
-                return None;
-            }
+            let _ = self.register_trait_decl_id(id)?;
         }
 
         match self.trait_impl_id_map.get(&rust_id) {

charon/src/translate_types.rs

@@ -589,6 +589,9 @@ impl<'tcx, 'ctx> TransCtx<'tcx, 'ctx> {
         // If yes, ignore it, otherwise, dive into the body. Note that for
         // external types we have to check the body: if the body is
         // public, we translate it, otherwise we consider the type as opaque.
+        // For instance, because `core::option::Option` is public, we can
+        // manipulate its variants. If we encounter this type, we must retrieve
+        // its definition.
         let is_local = rust_id.is_local();
         let kind = if !is_transparent {
             TypeDeclKind::Opaque

charon/src/types.rs

@@ -2,7 +2,7 @@
 
 pub use crate::gast::TraitItemName;
 use crate::meta::Meta;
-use crate::names::TypeName;
+use crate::names::Name;
 pub use crate::types_utils::*;
 use crate::values::Literal;
 use derivative::Derivative;
@@ -314,7 +314,7 @@ pub struct TypeDecl {
     /// [true] if the type decl is a local type decl, [false] if is comes from
     /// an external crate.
     pub is_local: bool,
-    pub name: TypeName,
+    pub name: Name,
     pub generics: GenericParams,
     pub preds: Predicates,
     /// The type kind: enum, struct, or opaque.

tests-polonius/Makefile

@@ -1,7 +1,7 @@
 CURRENT_DIR = $(shell pwd)
 CHARON ?= $(CURRENT_DIR)/../bin/charon
 DEST ?= .
-OPTIONS = --polonius
+OPTIONS += --polonius
 NOT_ALL_TESTS ?=
 
 .PHONY: all