Add generics to AggregateKind::Closure

AeneasVerif · Dec 4, 2023 · cdf1104 · cdf1104
1 parent a64b1d1
commit cdf1104
Show file tree

Hide file tree

Showing 4 changed files with 26 additions and 6 deletions.
diff --git a/charon/src/expressions.rs b/charon/src/expressions.rs
@@ -382,5 +382,5 @@ pub enum AggregateKind {
     Array(Ty, ConstGeneric),
     /// Aggregated values for closures group the function id together with its
     /// state.
-    Closure(FunDeclId::Id),
+    Closure(FunDeclId::Id, GenericArgs),
 }
diff --git a/charon/src/expressions_utils.rs b/charon/src/expressions_utils.rs
@@ -276,8 +276,13 @@ impl Rvalue {
                     AggregateKind::Array(_, len) => {
                         format!("[{}; {}]", ops_s.join(", "), len.fmt_with_ctx(ctx))
                     }
-                    AggregateKind::Closure(fn_id) => {
-                        format!("{{{}}} {{{}}}", ctx.format_object(*fn_id), ops_s.join(", "))
+                    AggregateKind::Closure(fn_id, generics) => {
+                        format!(
+                            "{{{}{}}} {{{}}}",
+                            ctx.format_object(*fn_id),
+                            generics.fmt_with_ctx_split_trait_refs(ctx),
+                            ops_s.join(", ")
+                        )
                     }
                 }
             }
@@ -464,7 +469,10 @@ pub trait ExprVisitor: crate::types::TypeVisitor {
                 self.visit_ty(ty);
                 self.visit_const_generic(cg);
             }
-            Closure(fn_id) => self.visit_fun_decl_id(fn_id),
+            Closure(fn_id, generics) => {
+                self.visit_fun_decl_id(fn_id);
+                self.visit_generic_args(generics);
+            }
         }
     }
 

diff --git a/charon/src/translate_functions_to_ullbc.rs b/charon/src/translate_functions_to_ullbc.rs
@@ -781,10 +781,21 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                         let akind = AggregateKind::Adt(type_id, variant_id, generics);
                         Ok(Rvalue::Aggregate(akind, operands_t))
                     }
-                    hax::AggregateKind::Closure(def_id, sig) => {
+                    hax::AggregateKind::Closure(def_id, substs, trait_refs, sig) => {
                         trace!("Closure:\n\n- def_id: {:?}\n\n- sig:\n{:?}", def_id, sig);
+
+                        // Translate the substitution
+                        let generics = self.translate_substs_and_trait_refs(
+                            span,
+                            erase_regions,
+                            None,
+                            substs,
+                            trait_refs,
+                        )?;
+
                         let def_id = self.translate_fun_decl_id(def_id.rust_def_id.unwrap());
-                        let akind = AggregateKind::Closure(def_id);
+                        let akind = AggregateKind::Closure(def_id, generics);
+
                         Ok(Rvalue::Aggregate(akind, operands_t))
                     }
                     hax::AggregateKind::Generator(_def_id, _subst, _movability) => {

diff --git a/charon/src/translate_traits.rs b/charon/src/translate_traits.rs
@@ -499,6 +499,7 @@ impl<'tcx, 'ctx> TransCtx<'tcx, 'ctx> {
                 tcx.param_env(rust_id),
                 rust_trait_ref.def_id,
                 rust_trait_ref.substs,
+                None,
             );
             let parent_trait_refs: Vec<TraitRef> =
                 bt_ctx.translate_trait_impl_sources(span, erase_regions, &parent_trait_refs)?;