Use maps instead of vectors for the trait clause params

Author: sonmarcho

charon/src/assumed.rs

@@ -11,7 +11,7 @@ use crate::ullbc_ast;
 use macros::EnumIsA;
 
 /// Ignore the builtin/auto traits like [core::marker::Sized] or [core::marker::Sync].
-pub const IGNORE_BUILTIN_MARKER_TRAITS: bool = false;
+pub const IGNORE_BUILTIN_MARKER_TRAITS: bool = true;
 
 // Ignored traits (includes marker traits, and others)
 pub static MARKER_SIZED_NAME: [&str; 3] = ["core", "marker", "Sized"];

charon/src/reorder_decls.rs

@@ -406,7 +406,7 @@ impl Deps {
 
     fn visit_generics_and_preds(&mut self, generics: &GenericParams, preds: &Predicates) {
         // Visit the traits referenced in the generics
-        for clause in &generics.trait_clauses {
+        for clause in generics.trait_clauses.values() {
             self.visit_trait_clause(clause);
         }
 

charon/src/translate_ctx.rs

@@ -21,7 +21,7 @@ use rustc_hir::def_id::DefId;
 use rustc_middle::ty::TyCtxt;
 use rustc_session::Session;
 use std::cmp::{Ord, Ordering, PartialOrd};
-use std::collections::{BTreeSet, HashMap, HashSet, VecDeque};
+use std::collections::{BTreeMap, BTreeSet, HashMap, HashSet, VecDeque};
 use std::fmt;
 
 /// Macro to either panic or return on error, depending on the CLI options
@@ -953,14 +953,22 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
 
     /// Retrieve the *local* trait clauses available in the current environment
     /// (we filter the parent of those clauses, etc.).
-    pub(crate) fn get_local_trait_clauses(&self) -> TraitClauseId::Vector<TraitClause> {
-        let clauses: TraitClauseId::Vector<TraitClause> = self
+    pub(crate) fn get_local_trait_clauses(&self) -> BTreeMap<TraitClauseId::Id, TraitClause> {
+        let clauses: Vec<TraitClause> = self
             .trait_clauses
             .iter()
             .filter_map(|(_, x)| x.to_local_trait_clause())
             .collect();
         // Sanity check
-        assert!(clauses.iter_indexed_values().all(|(i, c)| c.clause_id == i));
+        if !crate::assumed::IGNORE_BUILTIN_MARKER_TRAITS {
+            use crate::id_vector::ToUsize;
+            assert!(clauses
+                .iter()
+                .enumerate()
+                .all(|(i, c)| c.clause_id.to_usize() == i));
+        }
+        let clauses: BTreeMap<TraitClauseId::Id, TraitClause> =
+            clauses.into_iter().map(|x| (x.clause_id, x)).collect();
         clauses
     }
 

charon/src/translate_traits.rs

@@ -403,7 +403,7 @@ impl<'tcx, 'ctx> TransCtx<'tcx, 'ctx> {
                 .join("\n");
             let generic_clauses = generics
                 .trait_clauses
-                .iter()
+                .values()
                 .map(|c| c.fmt_with_ctx(&ctx))
                 .collect::<Vec<String>>()
                 .join("\n");

charon/src/types.rs

@@ -8,6 +8,7 @@ use macros::{
     generate_index_type, EnumAsGetters, EnumIsA, EnumToGetters, VariantIndexArity, VariantName,
 };
 use serde::Serialize;
+use std::collections::BTreeMap;
 
 pub type FieldName = String;
 
@@ -299,7 +300,10 @@ pub struct GenericParams {
     pub types: TypeVarId::Vector<TypeVar>,
     pub const_generics: ConstGenericVarId::Vector<ConstGenericVar>,
     // TODO: rename to match [GenericArgs]?
-    pub trait_clauses: TraitClauseId::Vector<TraitClause>,
+    // Remark: this is an OrdMap, not a vector, because due to the filtering
+    // of some trait clauses (for the marker traits for instance) the indexation
+    // is not contiguous.
+    pub trait_clauses: BTreeMap<TraitClauseId::Id, TraitClause>,
 }
 
 generate_index_type!(TraitClauseId);

charon/src/types_utils.rs

@@ -7,6 +7,7 @@ use crate::values::*;
 use hax_frontend_exporter as hax;
 use im::HashMap;
 use macros::make_generic_in_borrows;
+use std::collections::BTreeMap;
 use std::iter::Iterator;
 
 impl DeBruijnId {
@@ -93,7 +94,7 @@ impl GenericParams {
             regions: RegionId::Vector::new(),
             types: TypeVarId::Vector::new(),
             const_generics: ConstGenericVarId::Vector::new(),
-            trait_clauses: TraitClauseId::Vector::new(),
+            trait_clauses: BTreeMap::new(),
         }
     }
 
@@ -120,7 +121,7 @@ impl GenericParams {
             for x in const_generics {
                 params.push(x.to_string());
             }
-            for x in trait_clauses {
+            for x in trait_clauses.values() {
                 params.push(x.fmt_with_ctx(ctx));
             }
             format!("<{}>", params.join(", "))
@@ -154,7 +155,7 @@ impl GenericParams {
         };
 
         let mut clauses = Vec::new();
-        for x in trait_clauses {
+        for x in trait_clauses.values() {
             clauses.push(x.fmt_with_ctx(ctx));
         }
         (params, clauses)
@@ -1373,7 +1374,7 @@ pub trait TypeVisitor {
         for cg in g.const_generics.iter() {
             self.visit_const_generic_var(cg);
         }
-        for t in g.trait_clauses.iter() {
+        for (_, t) in g.trait_clauses.iter() {
             self.visit_trait_clause(t);
         }
     }