Merge pull request #421 from Nadrieril/hashcons

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.44"
+let supported_charon_version = "0.1.45"

charon-ml/src/Types.ml

@@ -436,7 +436,6 @@ and type_id =
           for more uniform treatment throughout the codebase.
        *)
 
-(** A type. *)
 and ty =
   | TAdt of type_id * generic_args
       (** An ADT.

charon/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "charon"
-version = "0.1.44"
+version = "0.1.45"
 authors = ["Son Ho <[email protected]>"]
 edition = "2021"
 license = "Apache-2.0"
@@ -65,7 +65,7 @@ rustc_version = "0.4"
 serde_json = { version = "1.0.91", features = ["unbounded_depth"] }
 serde-map-to-array = { version = "1.1.1", features = ["std"] }
 serde_stacker = "0.1.11"
-serde = { version = "1.0.152", features = ["derive"] }
+serde = { version = "1.0.152", features = ["derive", "rc"] }
 stacker = "0.1"
 take_mut = "0.2.2"
 toml = { version = "0.8", features = ["parse"] }

charon/src/ast/types.rs

@@ -1,5 +1,5 @@
-use crate::ast::*;
 use crate::ids::Vector;
+use crate::{ast::*, common::hash_consing::HashConsed};
 use derivative::Derivative;
 use derive_visitor::{Drive, DriveMut, Event, Visitor, VisitorMut};
 use macros::{EnumAsGetters, EnumIsA, EnumToGetters, VariantIndexArity, VariantName};
@@ -648,6 +648,19 @@ pub enum ConstGeneric {
 }
 
 /// A type.
+#[derive(Debug, Clone, Hash, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
+pub struct Ty(HashConsed<TyKind>);
+
+impl Ty {
+    pub fn new(kind: TyKind) -> Self {
+        Ty(HashConsed::new(kind))
+    }
+
+    pub fn kind(&self) -> &TyKind {
+        self.0.inner()
+    }
+}
+
 #[derive(
     Debug,
     Clone,
@@ -665,7 +678,8 @@ pub enum ConstGeneric {
     DriveMut,
 )]
 #[charon::variants_prefix("T")]
-pub enum Ty {
+#[charon::rename("Ty")]
+pub enum TyKind {
     /// An ADT.
     /// Note that here ADTs are very general. They can be:
     /// - user-defined ADTs
@@ -698,9 +712,9 @@ pub enum Ty {
     Never,
     // We don't support floating point numbers on purpose (for now)
     /// A borrow
-    Ref(Region, Box<Ty>, RefKind),
+    Ref(Region, Ty, RefKind),
     /// A raw pointer.
-    RawPtr(Box<Ty>, RefKind),
+    RawPtr(Ty, RefKind),
     /// A trait associated type
     ///
     /// Ex.:
@@ -721,7 +735,7 @@ pub enum Ty {
     /// This is essentially a "constrained" function signature:
     /// arrow types can only contain generic lifetime parameters
     /// (no generic types), no predicates, etc.
-    Arrow(Vector<RegionId, RegionVar>, Vec<Ty>, Box<Ty>),
+    Arrow(Vector<RegionId, RegionVar>, Vec<Ty>, Ty),
 }
 
 /// Builtin types identifiers.

charon/src/ast/types_utils.rs

@@ -74,7 +74,7 @@ impl GenericParams {
             types: self
                 .types
                 .iter_indexed()
-                .map(|(id, _)| Ty::TypeVar(id))
+                .map(|(id, _)| TyKind::TypeVar(id).into_ty())
                 .collect(),
             const_generics: self
                 .const_generics
@@ -225,8 +225,8 @@ impl IntegerTy {
 impl Ty {
     /// Return true if it is actually unit (i.e.: 0-tuple)
     pub fn is_unit(&self) -> bool {
-        match self {
-            Ty::Adt(TypeId::Tuple, args) => {
+        match self.kind() {
+            TyKind::Adt(TypeId::Tuple, args) => {
                 assert!(args.regions.is_empty());
                 assert!(args.const_generics.is_empty());
                 args.types.is_empty()
@@ -237,35 +237,35 @@ impl Ty {
 
     /// Return the unit type
     pub fn mk_unit() -> Ty {
-        Ty::Adt(TypeId::Tuple, GenericArgs::empty())
+        TyKind::Adt(TypeId::Tuple, GenericArgs::empty()).into_ty()
     }
 
     /// Return true if this is a scalar type
     pub fn is_scalar(&self) -> bool {
-        match self {
-            Ty::Literal(kind) => kind.is_integer(),
+        match self.kind() {
+            TyKind::Literal(kind) => kind.is_integer(),
             _ => false,
         }
     }
 
     pub fn is_unsigned_scalar(&self) -> bool {
-        match self {
-            Ty::Literal(LiteralTy::Integer(kind)) => kind.is_unsigned(),
+        match self.kind() {
+            TyKind::Literal(LiteralTy::Integer(kind)) => kind.is_unsigned(),
             _ => false,
         }
     }
 
     pub fn is_signed_scalar(&self) -> bool {
-        match self {
-            Ty::Literal(LiteralTy::Integer(kind)) => kind.is_signed(),
+        match self.kind() {
+            TyKind::Literal(LiteralTy::Integer(kind)) => kind.is_signed(),
             _ => false,
         }
     }
 
     /// Return true if the type is Box
     pub fn is_box(&self) -> bool {
-        match self {
-            Ty::Adt(TypeId::Builtin(BuiltinTy::Box), generics) => {
+        match self.kind() {
+            TyKind::Adt(TypeId::Builtin(BuiltinTy::Box), generics) => {
                 assert!(generics.regions.is_empty());
                 assert!(generics.types.len() == 1);
                 assert!(generics.const_generics.is_empty());
@@ -276,8 +276,8 @@ impl Ty {
     }
 
     pub fn as_box(&self) -> Option<&Ty> {
-        match self {
-            Ty::Adt(TypeId::Builtin(BuiltinTy::Box), generics) => {
+        match self.kind() {
+            TyKind::Adt(TypeId::Builtin(BuiltinTy::Box), generics) => {
                 assert!(generics.regions.is_empty());
                 assert!(generics.types.len() == 1);
                 assert!(generics.const_generics.is_empty());
@@ -288,6 +288,29 @@ impl Ty {
     }
 }
 
+impl TyKind {
+    pub fn into_ty(self) -> Ty {
+        Ty::new(self)
+    }
+}
+
+impl From<TyKind> for Ty {
+    fn from(kind: TyKind) -> Ty {
+        kind.into_ty()
+    }
+}
+
+/// Convenience for migration purposes.
+impl std::ops::Deref for Ty {
+    type Target = TyKind;
+
+    fn deref(&self) -> &Self::Target {
+        self.kind()
+    }
+}
+/// For deref patterns.
+unsafe impl std::ops::DerefPure for Ty {}
+
 impl Field {
     /// The new name for this field, as suggested by the `#[charon::rename]` attribute.
     pub fn renamed_name(&self) -> Option<&str> {

charon/src/ast/values_utils.rs

@@ -230,7 +230,7 @@ impl ScalarValue {
     pub fn to_constant(self) -> ConstantExpr {
         ConstantExpr {
             value: RawConstantExpr::Literal(Literal::Scalar(self)),
-            ty: Ty::Literal(LiteralTy::Integer(self.get_integer_ty())),
+            ty: TyKind::Literal(LiteralTy::Integer(self.get_integer_ty())).into_ty(),
         }
     }
 }

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

@@ -18,7 +18,7 @@ pub fn extract_constants_at_top_level(level: MirLevel) -> bool {
 }
 
 /// Are boxe manipulations desugared to very low-level code using raw pointers,
-/// unique and non-null pointers? See [crate::types::Ty::RawPtr] for detailed explanations.
+/// unique and non-null pointers? See [crate::types::TyKind::RawPtr] for detailed explanations.
 pub fn boxes_are_desugared(level: MirLevel) -> bool {
     match level {
         MirLevel::Built => false,

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

@@ -1,6 +1,7 @@
 //! The translation contexts.
 use super::translate_types::translate_bound_region_kind_name;
 use charon_lib::ast::*;
+use charon_lib::common::hash_by_addr::HashByAddr;
 use charon_lib::formatter::{FmtCtx, IntoFormatter};
 use charon_lib::ids::{MapGenerator, Vector};
 use charon_lib::name_matcher::NamePattern;
@@ -258,6 +259,9 @@ pub(crate) struct BodyTransCtx<'tcx, 'ctx, 'ctx1> {
     /// (For traits only) accumulated trait clauses on associated types.
     pub item_trait_clauses: HashMap<TraitItemName, Vector<TraitClauseId, TraitClause>>,
 
+    /// Cache the translation of types. This harnesses the deduplication of `TyKind` that hax does.
+    pub type_trans_cache: HashMap<HashByAddr<Arc<hax::TyKind>>, Ty>,
+
     /// The "regular" variables
     pub vars: Vector<VarId, ast::Var>,
     /// The map from rust variable indices to translated variables indices.
@@ -912,6 +916,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
             const_generic_vars_map: Default::default(),
             parent_trait_clauses: Default::default(),
             item_trait_clauses: Default::default(),
+            type_trans_cache: Default::default(),
             vars: Default::default(),
             vars_map: Default::default(),
             blocks: Default::default(),
@@ -1046,6 +1051,8 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         let var_ids = self.translate_region_binder(span, binder, &mut region_vars)?;
         self.region_vars[0] = region_vars;
         self.bound_region_vars.push_front(var_ids);
+        // Translation of types depends on bound variables, we must not mix that up.
+        self.type_trans_cache = Default::default();
 
         Ok(())
     }
@@ -1069,13 +1076,16 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         let var_ids = self.translate_region_binder(span, binder, &mut bound_vars)?;
         self.bound_region_vars.push_front(var_ids);
         self.region_vars.push_front(bound_vars);
+        // Translation of types depends on bound variables, we must not mix that up.
+        let old_ty_cache = std::mem::take(&mut self.type_trans_cache);
 
         // Call the continuation
         let res = f(self);
 
         // Reset
         self.bound_region_vars.pop_front();
         self.region_vars.pop_front();
+        self.type_trans_cache = old_ty_cache;
 
         // Return
         res

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

@@ -300,11 +300,11 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 match kind {
                     hax::ProjectionElem::Deref => {
                         // We use the type to disambiguate
-                        match current_ty {
-                            Ty::Ref(_, _, _) | Ty::RawPtr(_, _) => {
+                        match current_ty.kind() {
+                            TyKind::Ref(_, _, _) | TyKind::RawPtr(_, _) => {
                                 projection.push(ProjectionElem::Deref);
                             }
-                            Ty::Adt(TypeId::Builtin(BuiltinTy::Box), generics) => {
+                            TyKind::Adt(TypeId::Builtin(BuiltinTy::Box), generics) => {
                                 // This case only happens in some MIR levels
                                 assert!(!boxes_are_desugared(self.t_ctx.options.mir_level));
                                 assert!(generics.regions.is_empty());
@@ -324,7 +324,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                         use hax::ProjectionElemFieldKind::*;
                         let proj_elem = match field_kind {
                             Tuple(id) => {
-                                let (_, generics) = current_ty.as_adt().unwrap();
+                                let (_, generics) = current_ty.kind().as_adt().unwrap();
                                 let field_id = translate_field_id(*id);
                                 let proj_kind = FieldProjKind::Tuple(generics.types.len());
                                 ProjectionElem::Field(proj_kind, field_id)
@@ -336,20 +336,20 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                             } => {
                                 let field_id = translate_field_id(*index);
                                 let variant_id = variant.map(translate_variant_id);
-                                match current_ty {
-                                    Ty::Adt(TypeId::Adt(type_id), ..) => {
-                                        let proj_kind = FieldProjKind::Adt(type_id, variant_id);
+                                match current_ty.kind() {
+                                    TyKind::Adt(TypeId::Adt(type_id), ..) => {
+                                        let proj_kind = FieldProjKind::Adt(*type_id, variant_id);
                                         ProjectionElem::Field(proj_kind, field_id)
                                     }
-                                    Ty::Adt(TypeId::Tuple, generics) => {
+                                    TyKind::Adt(TypeId::Tuple, generics) => {
                                         assert!(generics.regions.is_empty());
                                         assert!(variant.is_none());
                                         assert!(generics.const_generics.is_empty());
                                         let proj_kind = FieldProjKind::Tuple(generics.types.len());
 
                                         ProjectionElem::Field(proj_kind, field_id)
                                     }
-                                    Ty::Adt(TypeId::Builtin(BuiltinTy::Box), generics) => {
+                                    TyKind::Adt(TypeId::Builtin(BuiltinTy::Box), generics) => {
                                         assert!(!boxes_are_desugared(self.t_ctx.options.mir_level));
 
                                         // Some more sanity checks
@@ -487,8 +487,8 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
             }
             hax::Rvalue::Len(place) => {
                 let (place, ty) = self.translate_place_with_type(span, place)?;
-                let cg = match &ty {
-                    Ty::Adt(
+                let cg = match ty.kind() {
+                    TyKind::Adt(
                         TypeId::Builtin(aty @ (BuiltinTy::Array | BuiltinTy::Slice)),
                         generics,
                     ) => {
@@ -515,8 +515,8 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                     | hax::CastKind::IntToFloat
                     | hax::CastKind::FloatToInt
                     | hax::CastKind::FloatToFloat => {
-                        let tgt_ty = *tgt_ty.as_literal().unwrap();
-                        let src_ty = *src_ty.as_literal().unwrap();
+                        let tgt_ty = *tgt_ty.kind().as_literal().unwrap();
+                        let src_ty = *src_ty.kind().as_literal().unwrap();
                         Ok(Rvalue::UnaryOp(
                             UnOp::Cast(CastKind::Scalar(src_ty, tgt_ty)),
                             operand,
@@ -546,17 +546,17 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                     )),
                     hax::CastKind::PointerCoercion(hax::PointerCoercion::Unsize) => {
                         let unop = if let (
-                            Ty::Ref(
+                            TyKind::Ref(
                                 _,
-                                deref!(Ty::Adt(TypeId::Builtin(BuiltinTy::Array), generics)),
+                                deref!(TyKind::Adt(TypeId::Builtin(BuiltinTy::Array), generics)),
                                 kind1,
                             ),
-                            Ty::Ref(
+                            TyKind::Ref(
                                 _,
-                                deref!(Ty::Adt(TypeId::Builtin(BuiltinTy::Slice), generics1)),
+                                deref!(TyKind::Adt(TypeId::Builtin(BuiltinTy::Slice), generics1)),
                                 kind2,
                             ),
-                        ) = (&src_ty, &tgt_ty)
+                        ) = (src_ty.kind(), tgt_ty.kind())
                         {
                             // In MIR terminology, we go from &[T; l] to &[T] which means we
                             // effectively "unsize" the type, as `l` no longer appears in the
@@ -607,7 +607,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
             )),
             hax::Rvalue::Discriminant(place) => {
                 let (place, ty) = self.translate_place_with_type(span, place)?;
-                if let Ty::Adt(TypeId::Adt(adt_id), _) = &ty {
+                if let TyKind::Adt(TypeId::Adt(adt_id), _) = ty.kind() {
                     Ok(Rvalue::Discriminant(place, *adt_id))
                 } else {
                     error_or_panic!(
@@ -1106,7 +1106,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 Ok(SwitchTargets::If(if_block, then_block))
             }
             hax::SwitchTargets::SwitchInt(_, targets_map, otherwise) => {
-                let int_ty = *switch_ty.as_literal().unwrap().as_integer().unwrap();
+                let int_ty = *switch_ty.kind().as_literal().unwrap().as_integer().unwrap();
                 let targets_map: Vec<(ScalarValue, BlockId)> = targets_map
                     .iter()
                     .map(|(v, tgt)| {