Merge pull request #494 from Nadrieril/fix-printer

charon-ml/src/PrintTypes.ml

@@ -365,25 +365,12 @@ let trait_type_constraint_to_string (env : 'a fmt_env)
 
 (** Helper to format "where" clauses *)
 let clauses_to_string (indent : string) (indent_incr : string)
-    (num_inherited_clauses : int) (clauses : string list) : string =
+    (clauses : string list) : string =
   if clauses = [] then ""
   else
     let env_clause s = indent ^ indent_incr ^ s ^ "," in
     let clauses = List.map env_clause clauses in
-    let inherited, local =
-      Collections.List.split_at clauses num_inherited_clauses
-    in
-    let delim1 =
-      if inherited <> [] then [ indent ^ "  // Inherited clauses" ] else []
-    in
-    let delim2 =
-      if inherited <> [] && local <> [] then [ indent ^ "  // Local clauses" ]
-      else []
-    in
-    let clauses =
-      List.concat [ [ indent ^ "where" ]; delim1; inherited; delim2; local ]
-    in
-    "\n" ^ String.concat "\n" clauses
+    "\n" ^ indent ^ "where\n" ^ String.concat "\n" clauses
 
 (** Helper to format "where" clauses *)
 let predicates_and_trait_clauses_to_string (env : 'a fmt_env) (indent : string)
@@ -413,7 +400,7 @@ let predicates_and_trait_clauses_to_string (env : 'a fmt_env) (indent : string)
   in
   (* Split between the inherited clauses and the local clauses *)
   let clauses =
-    clauses_to_string indent indent_incr 0
+    clauses_to_string indent indent_incr
       (List.concat
          [
            trait_clauses; regions_outlive; types_outlive; trait_type_constraints;

charon-ml/src/TypesUtils.ml

@@ -36,6 +36,7 @@ let type_decl_get_fields (def : type_decl)
   match (def.kind, opt_variant_id) with
   | Enum variants, Some variant_id -> (VariantId.nth variants variant_id).fields
   | Struct fields, None -> fields
+  | Union fields, None -> fields
   | _ ->
       let opt_variant_id =
         match opt_variant_id with

charon-ml/tests/Test_Deserialize.ml

@@ -33,8 +33,9 @@ let run_tests (folder : string) : unit =
             exit 1
         | Ok m ->
             log#linfo (lazy ("Deserialized: " ^ file));
-            log#ldebug
-              (lazy ("\n" ^ PrintLlbcAst.Crate.crate_to_string m ^ "\n")))
+            (* Test that pretty-printing doesn't crash *)
+            let printed = PrintLlbcAst.Crate.crate_to_string m in
+            log#ldebug (lazy ("\n" ^ printed ^ "\n")))
       llbc_files
   in
 

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

@@ -1415,7 +1415,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
     ) -> Result<FunSig, Error> {
         let span = item_meta.span;
 
-        let generics = self.translate_def_generics(span, def)?;
+        let mut generics = self.translate_def_generics(span, def)?;
 
         let signature = match &def.kind {
             hax::FullDefKind::Closure { args, .. } => &args.sig,
@@ -1456,7 +1456,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
 
         // Translate the signature
         trace!("signature of {def_id:?}:\n{:?}", signature.value);
-        let inputs: Vec<Ty> = signature
+        let mut inputs: Vec<Ty> = signature
             .value
             .inputs
             .iter()
@@ -1486,11 +1486,46 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                     hax::ClosureKind::FnMut => ClosureKind::FnMut,
                     hax::ClosureKind::FnOnce => ClosureKind::FnOnce,
                 };
+
+                assert_eq!(inputs.len(), 1);
+                let tuple_arg = inputs.pop().unwrap();
+
                 let state: Vector<TypeVarId, Ty> = args
                     .upvar_tys
                     .iter()
                     .map(|ty| self.translate_ty(span, &ty))
                     .try_collect()?;
+                // Add the state of the closure as first parameter.
+                let state_ty = {
+                    // Group the state types into a tuple
+                    let state_ty =
+                        TyKind::Adt(TypeId::Tuple, GenericArgs::new_from_types(state.clone()))
+                            .into_ty();
+                    // Depending on the kind of the closure, add a reference
+                    match &kind {
+                        ClosureKind::FnOnce => state_ty,
+                        ClosureKind::Fn | ClosureKind::FnMut => {
+                            let rid = generics
+                                .regions
+                                .push_with(|index| RegionVar { index, name: None });
+                            let r = Region::Var(DeBruijnVar::free(rid));
+                            let mutability = if kind == ClosureKind::Fn {
+                                RefKind::Shared
+                            } else {
+                                RefKind::Mut
+                            };
+                            TyKind::Ref(r, state_ty, mutability).into_ty()
+                        }
+                    }
+                };
+                inputs.push(state_ty);
+
+                // Unpack the tupled arguments to match the body locals.
+                let TyKind::Adt(TypeId::Tuple, tuple_args) = tuple_arg.kind() else {
+                    error_or_panic!(self, span, "Closure argument is not a tuple")
+                };
+                inputs.extend(tuple_args.types.iter().cloned());
+
                 Some(ClosureInfo { kind, state })
             }
             _ => None,

charon/src/transform/update_closure_signatures.rs

@@ -1,6 +1,6 @@
-//! # Micro-pass: the first local variable of closures is (a borrow to) the
-//! closure itself. This is not consistent with the closure signature,
-//! which ignores this first variable. This micro-pass updates this.
+//! # Micro-pass: the first local variable of closures is (a borrow to) the closure itself. This is
+//! not consistent with the closure signature, which represents the captured state as a tuple. This
+//! micro-pass updates this.
 use derive_visitor::{visitor_enter_fn_mut, DriveMut, VisitorMut};
 
 use crate::ids::Vector;
@@ -54,59 +54,16 @@ fn transform_function(
         ..
     } = &mut def.signature;
     if let Some(info) = closure_info {
-        // Update the signature.
-        // We add as first parameter the state of the closure, that is
-        // a borrow to a tuple (of borrows, usually).
-        // Remark: the types used in the closure state may contain erased
-        // regions. In particular, the regions coming from the parent
-        // function are often erased. TODO:
-        // However, we introduce fresh regions for the state (in particular
-        // because it is easy to do so).
-
-        // Group the types into a tuple
-        let num_fields = info.state.len();
-        let state = TyKind::Adt(
-            TypeId::Tuple,
-            GenericArgs::new_from_types(info.state.clone()),
-        )
-        .into_ty();
-        // Depending on the kind of the closure, add a reference
-        let mut state = match &info.kind {
-            ClosureKind::FnOnce => state,
-            ClosureKind::Fn | ClosureKind::FnMut => {
-                // We introduce an erased region, that we replace later
-                //let index = RegionId::new(generics.regions.len());
-                //generics.regions.push_back(RegionVar { index, name: None });
-
-                let mutability = if info.kind == ClosureKind::Fn {
-                    RefKind::Shared
-                } else {
-                    RefKind::Mut
-                };
-                //let r = Region::BVar(DeBruijnId::new(0), index);
-                TyKind::Ref(Region::Erased, state, mutability).into_ty()
-            }
-        };
-
-        // Explore the state and introduce fresh regions for the erased
-        // regions we find.
+        // Explore the state and introduce fresh regions for the erased regions we find.
         let mut visitor = Ty::visit_inside(InsertRegions {
             regions: &mut generics.regions,
             depth: 0,
         });
-        state.drive_mut(&mut visitor);
-
-        // Update the inputs (slightly annoying to push to the front of
-        // a vector...).
-        let mut original_inputs = std::mem::take(inputs);
-        let mut ninputs = vec![state.clone()];
-        ninputs.append(&mut original_inputs);
-        *inputs = ninputs;
+        inputs[0].drive_mut(&mut visitor);
 
         // Update the body.
-        // We change the type of the local variable of index 1, which is
-        // a reference to the closure itself, so that it has the type of
-        // (a reference to) the state of the closure.
+        // We change the type of the local variable of index 1, which is a reference to the closure
+        // itself, so that it has the type of (a reference to) the state of the closure.
         //
         // For instance, in the example below:
         // ```text
@@ -124,17 +81,17 @@ fn transform_function(
         // ```
         // We also update the corresponding field accesses in the body of
         // the function.
-
         if let Some(body) = body {
-            body.locals.arg_count += 1;
-
             // Update the type of the local 1 (which is the closure)
             assert!(body.locals.vars.len() > 1);
             let state_var = &mut body.locals.vars[1];
-            state_var.ty = state;
+            state_var.ty = inputs[0].clone();
             state_var.name = Some("state".to_string());
 
             // Update the body, and in particular the accesses to the states
+            // TODO: translate to ADT field access
+            // TODO: handle directly during translation
+            let num_fields = info.state.len();
             body.body
                 .drive_mut(&mut visitor_enter_fn_mut(|pe: &mut ProjectionElem| {
                     if let ProjectionElem::Field(pk @ FieldProjKind::ClosureState, _) = pe {

charon/tests/cargo/dependencies.out

@@ -1,6 +1,6 @@
 # Final LLBC before serialization:
 
-fn test_cargo_dependencies::silly_incr::closure(@1: (), @2: (u32)) -> u32
+fn test_cargo_dependencies::silly_incr::closure(@1: (), @2: u32) -> u32
 {
     let @0: u32; // return
     let state@1: (); // arg #1