Check generics inside bodies too

charon/Cargo.toml

@@ -76,7 +76,8 @@ tracing = { version = "0.1", features = [ "max_level_trace" ] }
 wait-timeout = { version = "0.2.0", optional = true }
 which = "7.0"
 
-hax-frontend-exporter = { git = "https://github.com/hacspec/hax", branch = "main", optional = true }
+# hax-frontend-exporter = { git = "https://github.com/hacspec/hax", branch = "main", optional = true }
+hax-frontend-exporter = { git = "https://github.com/Nadrieril/hax", branch = "fix-call-generics", optional = true }
 # hax-frontend-exporter = { path = "../../hax/frontend/exporter", optional = true }
 macros = { path = "./macros" }
 

charon/src/ast/types.rs

@@ -242,7 +242,7 @@ pub struct Binder<T> {
 /// be filled. We group in a different place the predicates which are not
 /// trait clauses, because those enforce constraints but do not need to
 /// be filled with witnesses/instances.
-#[derive(Debug, Default, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
+#[derive(Default, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
 pub struct GenericParams {
     pub regions: Vector<RegionId, RegionVar>,
     pub types: Vector<TypeVarId, TypeVar>,

charon/src/ast/types_utils.rs

@@ -190,11 +190,11 @@ impl GenericArgs {
             types,
             const_generics,
             trait_refs,
-        } = &mut self;
-        regions.extend(other.regions.iter().cloned());
-        types.extend(other.types.iter().cloned());
-        const_generics.extend(other.const_generics.iter().cloned());
-        trait_refs.extend(other.trait_refs.iter().cloned());
+        } = other;
+        self.regions.extend_from_slice(regions);
+        self.types.extend_from_slice(types);
+        self.const_generics.extend_from_slice(const_generics);
+        self.trait_refs.extend_from_slice(trait_refs);
         self
     }
 }

charon/src/ast/visitor.rs

@@ -44,12 +44,12 @@ use index_vec::Idx;
         CastKind, ClosureInfo, ClosureKind, ConstantExpr, ConstGenericVar, ConstGenericVarId,
         Disambiguator, ExistentialPredicate, Field, FieldId, FieldProjKind, FloatTy, FloatValue,
         FnOperand, FunId, FunIdOrTraitMethodRef, FunSig, ImplElem, IntegerTy, Literal, LiteralTy,
-        llbc_ast::Block, llbc_ast::ExprBody, llbc_ast::RawStatement, llbc_ast::Statement, llbc_ast::Switch,
+        llbc_ast::Block, llbc_ast::ExprBody, llbc_ast::RawStatement, llbc_ast::Switch,
         Locals, Name, NullOp, Opaque, Operand, PathElem, Place, PlaceKind, ProjectionElem, RawConstantExpr,
         RefKind, RegionId, RegionVar, Rvalue, ScalarValue, TraitClause, TraitClauseId, TraitItemName,
         TraitRefKind, TraitTypeConstraint, TranslatedCrate, TyKind, TypeDeclKind, TypeId, TypeVar, TypeVarId,
         ullbc_ast::BlockData, ullbc_ast::BlockId, ullbc_ast::ExprBody, ullbc_ast::RawStatement,
-        ullbc_ast::RawTerminator, ullbc_ast::Statement, ullbc_ast::SwitchTargets, ullbc_ast::Terminator,
+        ullbc_ast::RawTerminator, ullbc_ast::SwitchTargets, ullbc_ast::Terminator,
         UnOp, Var, Variant, VariantId, VarId,
         for<T: AstVisitable> Box<T>,
         for<T: AstVisitable> Option<T>,
@@ -67,6 +67,7 @@ use index_vec::Idx;
         for<T: AstVisitable + Idx> DeBruijnVar<T>,
         for<T: AstVisitable> RegionBinder<T>,
         for<T: AstVisitable> Binder<T>,
+        llbc_statement: llbc_ast::Statement, ullbc_statement: ullbc_ast::Statement,
         AggregateKind, FnPtr, ItemKind, ItemMeta, Span,
         BodyId, FunDeclId, GlobalDeclId, TypeDeclId, TraitDeclId, TraitImplId,
         FunDecl, GlobalDecl, TypeDecl, TraitDecl, TraitImpl,

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

@@ -112,9 +112,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                     generics,
                     trait_refs
                 );
-                let used_params = None;
-                let generics =
-                    self.translate_generic_args(span, used_params, generics, trait_refs, None)?;
+                let generics = self.translate_generic_args(span, generics, trait_refs, None)?;
 
                 let global_id = self.register_global_decl_id(span, id);
                 RawConstantExpr::Global(GlobalDeclRef {

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

@@ -131,7 +131,6 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                     impl_id: self.register_trait_impl_id(span, impl_id),
                     generics: self.translate_generic_args(
                         span,
-                        None,
                         impl_generics,
                         impl_required_impl_exprs,
                         None,
@@ -669,7 +668,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
 
                         // Translate the substitution
                         let generics =
-                            self.translate_generic_args(span, None, substs, trait_refs, None)?;
+                            self.translate_generic_args(span, substs, trait_refs, None)?;
 
                         let type_id = self.translate_type_id(span, adt_id)?;
                         // Sanity check
@@ -688,21 +687,20 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                         let akind = AggregateKind::Adt(type_id, variant_id, field_id, generics);
                         Ok(Rvalue::Aggregate(akind, operands_t))
                     }
-                    hax::AggregateKind::Closure(def_id, substs, trait_refs, sig) => {
-                        trace!("Closure:\n\n- def_id: {:?}\n\n- sig:\n{:?}", def_id, sig);
+                    hax::AggregateKind::Closure(def_id, closure_args) => {
+                        trace!(
+                            "Closure:\n\n- def_id: {:?}\n\n- sig:\n{:?}",
+                            def_id,
+                            closure_args.tupled_sig
+                        );
 
                         // Retrieve the late-bound variables.
-                        let binder = match self.t_ctx.hax_def(def_id)?.kind() {
-                            hax::FullDefKind::Closure { args, .. } => args.sig.as_ref().rebind(()),
-                            _ => unreachable!(),
-                        };
-
+                        let binder = closure_args.tupled_sig.as_ref().rebind(());
                         // Translate the substitution
                         let generics = self.translate_generic_args(
                             span,
-                            None,
-                            substs,
-                            trait_refs,
+                            &closure_args.parent_args,
+                            &closure_args.parent_trait_refs,
                             Some(binder),
                         )?;
 
@@ -785,7 +783,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
         };
 
         // Translate the type parameters
-        let generics = self.translate_generic_args(span, None, substs, trait_refs, binder)?;
+        let generics = self.translate_generic_args(span, substs, trait_refs, binder)?;
 
         // Translate the arguments
         let args = args
@@ -1005,26 +1003,13 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
             }
             TerminatorKind::Call {
                 fun,
-                generics,
                 args,
                 destination,
                 target,
-                trait_refs,
-                trait_info,
                 unwind: _, // We model unwinding as an effet, we don't represent it in control flow
-                call_source: _,
                 fn_span: _,
-            } => self.translate_function_call(
-                statements,
-                span,
-                fun,
-                generics,
-                args,
-                destination,
-                target,
-                trait_refs,
-                trait_info,
-            )?,
+                ..
+            } => self.translate_function_call(statements, span, fun, args, destination, target)?,
             TerminatorKind::Assert {
                 cond,
                 expected,
@@ -1127,12 +1112,9 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
         statements: &mut Vec<Statement>,
         span: Span,
         fun: &hax::FunOperand,
-        generics: &Vec<hax::GenericArg>,
         args: &Vec<hax::Spanned<hax::Operand>>,
         destination: &hax::Place,
         target: &Option<hax::BasicBlock>,
-        trait_refs: &Vec<hax::ImplExpr>,
-        trait_info: &Option<hax::ImplExpr>,
     ) -> Result<RawTerminator, Error> {
         trace!();
         // There are two cases, depending on whether this is a "regular"
@@ -1141,7 +1123,12 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
         let lval = self.translate_place(span, destination)?;
         let next_block = target.map(|target| self.translate_basic_block_id(target));
         let (fn_operand, args) = match fun {
-            hax::FunOperand::Id(def_id) => {
+            hax::FunOperand::Static {
+                def_id,
+                generics,
+                trait_refs,
+                trait_info,
+            } => {
                 // Translate the function operand - should be a constant: we don't
                 // support closures for now
                 trace!("func: {:?}", def_id);
@@ -1171,7 +1158,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                     }
                 }
             }
-            hax::FunOperand::Move(p) => {
+            hax::FunOperand::DynamicMove(p) => {
                 // Call to a local function pointer
                 // The function
                 let p = self.translate_place(span, p)?;
@@ -1418,7 +1405,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
         self.translate_def_generics(span, def)?;
 
         let signature = match &def.kind {
-            hax::FullDefKind::Closure { args, .. } => &args.sig,
+            hax::FullDefKind::Closure { args, .. } => &args.tupled_sig,
             hax::FullDefKind::Fn { sig, .. } => sig,
             hax::FullDefKind::AssocFn { sig, .. } => sig,
             hax::FullDefKind::Ctor {

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

@@ -44,8 +44,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
     ) -> Result<PolyTraitDeclRef, Error> {
         self.translate_region_binder(span, bound_trait_ref, move |ctx, trait_ref| {
             let trait_id = ctx.register_trait_decl_id(span, &trait_ref.def_id);
-            let generics =
-                ctx.translate_generic_args(span, None, &trait_ref.generic_args, &[], None)?;
+            let generics = ctx.translate_generic_args(span, &trait_ref.generic_args, &[], None)?;
             Ok(TraitDeclRef { trait_id, generics })
         })
     }
@@ -67,8 +66,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
     ) -> Result<TraitDeclRef, Error> {
         let trait_id = self.register_trait_decl_id(span, &trait_ref.def_id);
         // For now a trait has no required bounds, so we pass an empty list.
-        let generics =
-            self.translate_generic_args(span, None, &trait_ref.generic_args, &[], None)?;
+        let generics = self.translate_generic_args(span, &trait_ref.generic_args, &[], None)?;
         Ok(TraitDeclRef { trait_id, generics })
     }
 
@@ -225,7 +223,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                 generics,
             } => {
                 let impl_id = self.register_trait_impl_id(span, impl_def_id);
-                let generics = self.translate_generic_args(span, None, generics, nested, None)?;
+                let generics = self.translate_generic_args(span, generics, nested, None)?;
                 TraitRef {
                     kind: TraitRefKind::TraitImpl(impl_id, generics),
                     trait_decl_ref,

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

@@ -192,13 +192,8 @@ impl BodyTransCtx<'_, '_> {
         let trait_id = self.register_trait_decl_id(span, implemented_trait_id);
         let implemented_trait = {
             let implemented_trait = &trait_pred.trait_ref;
-            let generics = self.translate_generic_args(
-                span,
-                None,
-                &implemented_trait.generic_args,
-                &[],
-                None,
-            )?;
+            let generics =
+                self.translate_generic_args(span, &implemented_trait.generic_args, &[], None)?;
             TraitDeclRef { trait_id, generics }
         };
 

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

@@ -144,19 +144,25 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
             } => {
                 trace!("Adt: {:?}", def_id);
 
+                // Translate the type parameters instantiation
+                let mut generics = self.translate_generic_args(span, substs, trait_refs, None)?;
+
                 // Retrieve the type identifier
                 let type_id = self.translate_type_id(span, def_id)?;
 
-                // Retrieve the list of used arguments
-                let used_params = if let TypeId::Builtin(builtin_ty) = type_id {
-                    Some(builtins::type_to_used_params(builtin_ty))
-                } else {
-                    None
-                };
-
-                // Translate the type parameters instantiation
-                let generics =
-                    self.translate_generic_args(span, used_params, substs, trait_refs, None)?;
+                // Filter the type arguments.
+                // TODO: do this in a micro-pass
+                if let TypeId::Builtin(builtin_ty) = type_id {
+                    let used_args = builtins::type_to_used_params(builtin_ty);
+                    error_assert!(self, span, generics.types.len() == used_args.len());
+                    let types = std::mem::take(&mut generics.types)
+                        .into_iter()
+                        .zip(used_args)
+                        .filter(|(_, used)| *used)
+                        .map(|(ty, _)| ty)
+                        .collect();
+                    generics.types = types;
+                }
 
                 // Return the instantiated ADT
                 TyKind::Adt(type_id, generics)
@@ -262,7 +268,13 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                 trace!("PlaceHolder");
                 error_or_panic!(self, span, "Unsupported type: placeholder")
             }
-            hax::TyKind::Arrow(box sig) => {
+            hax::TyKind::Arrow(box sig)
+            | hax::TyKind::Closure(
+                _,
+                hax::ClosureArgs {
+                    untupled_sig: sig, ..
+                },
+            ) => {
                 trace!("Arrow");
                 trace!("bound vars: {:?}", sig.bound_vars);
                 let sig = self.translate_region_binder(span, sig, |ctx, sig| {
@@ -295,31 +307,17 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
     pub fn translate_generic_args(
         &mut self,
         span: Span,
-        used_params: Option<Vec<bool>>,
         substs: &[hax::GenericArg],
         trait_refs: &[hax::ImplExpr],
         late_bound: Option<hax::Binder<()>>,
     ) -> Result<GenericArgs, Error> {
         use hax::GenericArg::*;
         trace!("{:?}", substs);
 
-        // Filter the parameters
-        let substs: Vec<&hax::GenericArg> = match used_params {
-            None => substs.iter().collect(),
-            Some(used_args) => {
-                error_assert!(self, span, substs.len() == used_args.len());
-                substs
-                    .iter()
-                    .zip(used_args.into_iter())
-                    .filter_map(|(param, used)| if used { Some(param) } else { None })
-                    .collect()
-            }
-        };
-
         let mut regions = Vector::new();
         let mut types = Vector::new();
         let mut const_generics = Vector::new();
-        for param in substs.iter() {
+        for param in substs {
             match param {
                 Type(param_ty) => {
                     types.push(self.translate_ty(span, param_ty)?);
@@ -663,7 +661,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
         // [TyCtxt.generics_of] gives us the early-bound parameters. We add the late-bound
         // parameters here.
         let signature = match &def.kind {
-            hax::FullDefKind::Closure { args, .. } => Some(&args.sig),
+            hax::FullDefKind::Closure { args, .. } => Some(&args.tupled_sig),
             hax::FullDefKind::Fn { sig, .. } => Some(sig),
             hax::FullDefKind::AssocFn { sig, .. } => Some(sig),
             _ => None,

charon/src/ids/vector.rs

@@ -118,6 +118,14 @@ where
         self.push_all(it).for_each(|_| ())
     }
 
+    pub fn extend_from_slice(&mut self, other: &Self)
+    where
+        T: Clone,
+    {
+        self.vector.extend_from_slice(&other.vector);
+        self.real_len += other.real_len;
+    }
+
     /// Map each entry to a new one, keeping the same ids.
     pub fn map<U>(self, mut f: impl FnMut(T) -> U) -> Vector<I, U> {
         Vector {