Merge pull request #540 from Nadrieril/lazy-translate-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 <[email protected]>"]
 edition = "2021"
 license = "Apache-2.0"

charon/src/ast/gast.rs

@@ -4,9 +4,9 @@ use crate::ids::Vector;
 use crate::llbc_ast;
 use crate::ullbc_ast;
 use derive_generic_visitor::{Drive, DriveMut};
+use indexmap::IndexMap;
 use macros::{EnumIsA, EnumToGetters};
 use serde::{Deserialize, Serialize};
-use std::collections::HashMap;
 
 /// A variable
 #[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
@@ -242,12 +242,12 @@ pub struct TraitDecl {
     pub consts: Vec<(TraitItemName, Ty)>,
     /// Records associated constants that have a default value.
     #[charon::opaque]
-    pub const_defaults: HashMap<TraitItemName, GlobalDeclRef>,
+    pub const_defaults: IndexMap<TraitItemName, GlobalDeclRef>,
     /// The associated types declared in the trait.
     pub types: Vec<TraitItemName>,
     /// Records associated types that have a default value.
     #[charon::opaque]
-    pub type_defaults: HashMap<TraitItemName, Ty>,
+    pub type_defaults: IndexMap<TraitItemName, Ty>,
     /// List of trait clauses that apply to each associated type. This is used during translation,
     /// but the `lift_associated_item_clauses` pass moves them to be parent clauses later. Hence
     /// this is empty after that pass.

charon/src/ast/meta.rs

@@ -185,9 +185,8 @@ pub enum ItemOpacity {
     /// Translate the item fully.
     Transparent,
     /// Translate the item depending on the normal rust visibility of its contents: for types, we
-    /// translate fully if it is a struct with public fields or an enum; for functions and globals
-    /// this is equivalent to `Opaque`; for trait decls and impls this is equivalent to
-    /// `Transparent`.
+    /// translate fully if it is a struct with public fields or an enum; for other items this is
+    /// equivalent to `Opaque`.
     Foreign,
     /// Translate the item name and signature, but not its contents. For function and globals, this
     /// means we don't translate the body (the code); for ADTs, this means we don't translate the

charon/src/ast/visitor.rs

@@ -15,6 +15,7 @@ use std::{any::Any, collections::HashMap};
 use crate::ast::*;
 use derive_generic_visitor::*;
 use index_vec::Idx;
+use indexmap::IndexMap;
 
 /// An overrideable visitor trait that can be used to conveniently traverse the whole contents of
 /// an item. This is useful when e.g. dealing with types, which show up pretty much everywhere in
@@ -105,6 +106,22 @@ impl<K: Any, T: AstVisitable> AstVisitable for HashMap<K, T> {
     }
 }
 
+/// Manual impl that only visits the values
+impl<K: Any, T: AstVisitable> AstVisitable for IndexMap<K, T> {
+    fn drive<V: VisitAst>(&self, v: &mut V) -> ControlFlow<V::Break> {
+        for x in self.values() {
+            v.visit(x)?;
+        }
+        Continue(())
+    }
+    fn drive_mut<V: VisitAstMut>(&mut self, v: &mut V) -> ControlFlow<V::Break> {
+        for x in self.values_mut() {
+            v.visit(x)?;
+        }
+        Continue(())
+    }
+}
+
 /// A smaller visitor group just for function bodies. This explores statements, places and
 /// operands, but does not recurse into types.
 ///
@@ -133,8 +150,10 @@ impl<K: Any, T: AstVisitable> AstVisitable for HashMap<K, T> {
         llbc_ast::ExprBody, llbc_ast::RawStatement, llbc_ast::Switch,
         ullbc_ast::BlockData, ullbc_ast::ExprBody, ullbc_ast::RawStatement,
         ullbc_ast::RawTerminator, ullbc_ast::SwitchTargets,
+        Body, Opaque,
         for<T: BodyVisitable> Box<T>,
         for<T: BodyVisitable> Option<T>,
+        for<T: BodyVisitable, E: BodyVisitable> Result<T, E>,
         for<A: BodyVisitable, B: BodyVisitable> (A, B),
         for<T: BodyVisitable> Vec<T>,
         for<I: Idx, T: BodyVisitable> Vector<I, T>,

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,
         }
     }
 
@@ -872,7 +876,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
         *opacity
     }
 
-    pub(crate) fn register_id(
+    pub(crate) fn register_id_no_enqueue(
         &mut self,
         src: &Option<DepSource>,
         id: TransItemSource,
@@ -898,7 +902,6 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
                     }
                 };
                 // Add the id to the queue of declarations to translate
-                self.items_to_translate.insert(id, trans_id);
                 self.id_map.insert(id, trans_id);
                 self.reverse_id_map.insert(trans_id, id);
                 self.translated.all_ids.insert(trans_id);
@@ -918,13 +921,30 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
         item_id
     }
 
+    pub(crate) fn enqueue_id(&mut self, id: impl Into<AnyTransId>) {
+        let id = id.into();
+        let src_id = self.reverse_id_map[&id];
+        self.items_to_translate.insert(src_id, id);
+    }
+
+    /// Register this id and enqueue it for translation.
+    pub(crate) fn register_and_enqueue_id(
+        &mut self,
+        src: &Option<DepSource>,
+        id: TransItemSource,
+    ) -> AnyTransId {
+        let item_id = self.register_id_no_enqueue(src, id);
+        self.enqueue_id(item_id);
+        item_id
+    }
+
     pub(crate) fn register_type_decl_id(
         &mut self,
         src: &Option<DepSource>,
         id: impl Into<DefId>,
     ) -> TypeDeclId {
         *self
-            .register_id(src, TransItemSource::Type(id.into()))
+            .register_and_enqueue_id(src, TransItemSource::Type(id.into()))
             .as_type()
             .unwrap()
     }
@@ -935,7 +955,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
         id: impl Into<DefId>,
     ) -> FunDeclId {
         *self
-            .register_id(src, TransItemSource::Fun(id.into()))
+            .register_and_enqueue_id(src, TransItemSource::Fun(id.into()))
             .as_fun()
             .unwrap()
     }
@@ -946,7 +966,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
         id: impl Into<DefId>,
     ) -> TraitDeclId {
         *self
-            .register_id(src, TransItemSource::TraitDecl(id.into()))
+            .register_and_enqueue_id(src, TransItemSource::TraitDecl(id.into()))
             .as_trait_decl()
             .unwrap()
     }
@@ -968,7 +988,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
         }
 
         *self
-            .register_id(src, TransItemSource::TraitImpl(id))
+            .register_and_enqueue_id(src, TransItemSource::TraitImpl(id))
             .as_trait_impl()
             .unwrap()
     }
@@ -979,7 +999,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
         id: impl Into<DefId>,
     ) -> GlobalDeclId {
         *self
-            .register_id(src, TransItemSource::Global(id.into()))
+            .register_and_enqueue_id(src, TransItemSource::Global(id.into()))
             .as_global()
             .unwrap()
     }
@@ -1051,6 +1071,11 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
         self.blocks_map.get(&rid)
     }
 
+    pub(crate) fn register_id_no_enqueue(&mut self, span: Span, id: TransItemSource) -> AnyTransId {
+        let src = self.make_dep_source(span);
+        self.t_ctx.register_id_no_enqueue(&src, id)
+    }
+
     pub(crate) fn register_type_decl_id(&mut self, span: Span, id: impl Into<DefId>) -> TypeDeclId {
         let src = self.make_dep_source(span);
         self.t_ctx.register_type_decl_id(&src, id)
@@ -1061,6 +1086,17 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
         self.t_ctx.register_fun_decl_id(&src, id)
     }
 
+    pub(crate) fn register_fun_decl_id_no_enqueue(
+        &mut self,
+        span: Span,
+        id: impl Into<DefId>,
+    ) -> FunDeclId {
+        self.register_id_no_enqueue(span, TransItemSource::Fun(id.into()))
+            .as_fun()
+            .copied()
+            .unwrap()
+    }
+
     pub(crate) fn register_global_decl_id(
         &mut self,
         span: Span,

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

@@ -93,7 +93,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
         span: Span,
         def: &hax::FullDef,
     ) -> Result<ItemKind, Error> {
-        let assoc = match &def.kind {
+        let assoc = match def.kind() {
             hax::FullDefKind::AssocTy {
                 associated_item, ..
             }
@@ -124,6 +124,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                 impl_generics,
                 impl_required_impl_exprs,
                 implemented_trait_ref,
+                implemented_trait_item,
                 overrides_default,
                 ..
             } => {
@@ -139,6 +140,12 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                     )?,
                 };
                 let trait_ref = self.translate_trait_ref(span, implemented_trait_ref)?;
+                if matches!(def.kind(), hax::FullDefKind::AssocFn { .. }) {
+                    // Ensure we translate the corresponding decl signature.
+                    // FIXME(self_clause): also ensure we translate associated globals
+                    // consistently; to do once we have clearer `Self` clause handling.
+                    let _ = self.register_fun_decl_id(span, implemented_trait_item);
+                }
                 ItemKind::TraitImpl {
                     impl_ref,
                     trait_ref,