Fix declaration order and enum mangling issues

lib/AstToCStar.ml

@@ -209,6 +209,18 @@ let whitelisted_tapp e =
 
 let no_return_type_lids = ref []
 
+(* Table for resolving type abbreviations, used to normalize types before
+   mangle_enum so that aliases and canonical types produce the same name. *)
+let type_abbrevs: (lident, typ) Hashtbl.t = Hashtbl.create 256
+
+let rec resolve_abbrev (t: typ): typ =
+  match t with
+  | TQualified lid ->
+    (match Hashtbl.find_opt type_abbrevs lid with
+    | Some t' -> resolve_abbrev t'
+    | None -> t)
+  | _ -> t
+
 (* For field names, we simply avoid keywords. This is potentially incorrect, e.g. a record with fields
    `switch` and `switch0` would see both fields mapped to the same name. Ideally, we would maintain a
    global mapping of fields (per type), just like we do for enums -- see lib/Simplify.ml,
@@ -381,7 +393,7 @@ and mk_expr env in_stmt under_initializer_list e =
   | EBound var ->
       CStar.Var (find env var)
   | EEnum lident ->
-      CStar.Qualified (GlobalNames.mangle_enum lident e.typ)
+      CStar.Qualified (GlobalNames.mangle_enum lident (resolve_abbrev e.typ))
   | EQualified lident ->
       if LidSet.mem lident env.ifdefs then
         Warn.(maybe_fatal_error (KPrint.bsprintf "%a" Loc.ploc env.location, IfDef lident));
@@ -687,7 +699,7 @@ and mk_stmts env e ret_type =
           List.map (fun (lid, e) ->
             (match lid with
             | SConstant k -> `Int k
-            | SEnum lid -> `Ident (GlobalNames.mangle_enum lid e0.typ)
+            | SEnum lid -> `Ident (GlobalNames.mangle_enum lid (resolve_abbrev e0.typ))
             | _ -> failwith "impossible"),
             mk_block env return_pos e
           ) branches, default) :: comment e0.meta @ acc
@@ -1027,6 +1039,15 @@ and mk_program m name env decls =
   List.rev decls
 
 and mk_files files m ifdefs macros =
+  (* Build abbreviation table for enum type resolution *)
+  Hashtbl.clear type_abbrevs;
+  List.iter (fun (_, decls) ->
+    List.iter (fun d ->
+      match d with
+      | DType (lid, _, _, _, Abbrev t) -> Hashtbl.replace type_abbrevs lid t
+      | _ -> ()
+    ) decls
+  ) files;
   let env = { empty with ifdefs; macros } in
   List.map (fun file ->
     let name, program = file in

lib/Monomorphization.ml

@@ -332,26 +332,16 @@ let monomorphize_data_types map = object(self)
    * order declarations as they are needed, including that of the node we are
    * visiting. *)
   method private visit_node (under_ref: bool) (n: node) =
-    (* Fast-path:
-       - there are no type arguments (so: nothing to monomorphize here)
-       - we are not under a ref (so: no forward declarations to insert here),
-       - we are not visiting ourselves either (so: no hopeful forward declaration to insert here)
-       --> we do not visit this lid, and do not self#record it.
-
-       1. If we saw this lid, great.
-       2. If we haven't seen this lid yet, no problem, its contents will be
-          visited through self#visit_decl in the case where n = 0 && n_cgs = 0,
-          and it will be inserted in its original spot, which has the nice
-          side-effect of preserving the source order.*)
-    if snd3 n = [] && thd3 n = [] && not under_ref && Option.map fst @@ Hashtbl.find_opt state n <> Some Gray then
+    (* Fast-path: non-polymorphic type that has already been fully processed. *)
+    if snd3 n = [] && thd3 n = [] && not under_ref && (match Hashtbl.find_opt state n with Some (Black, _) -> true | _ -> false) then
       fst3 n
     else
       (* We recursively visit the arguments. This avoids inconsistencies where
          the map would previously record both t<u<v>> and t<u__v> which then
          required renormalizations and didn't work anyhow.
 
          Because we have no equirecursive types, this should not loop *)
-      let n = fst3 n, List.map (self#visit_typ under_ref) (snd3 n), thd3 n in
+      let n = fst3 n, List.map (self#visit_typ true) (snd3 n), thd3 n in
       let lid, args, cgs = n in
       (* White, gray or black? *)
       match Hashtbl.find state n with
@@ -418,28 +408,24 @@ let monomorphize_data_types map = object(self)
             | flags, Variant branches ->
                 let branches = List.map (fun (cons, fields) -> cons, subst fields) branches in
                 let branches = self#visit_branches_t under_ref branches in
-                if args <> [] || cgs <> [] then
-                  self#record (DType (chosen_lid, flag @ flags, 0, 0, Variant branches));
+                self#record (DType (chosen_lid, flag @ flags, 0, 0, Variant branches));
                 Hashtbl.replace state n (Black, chosen_lid)
             | flags, Flat fields ->
                 let fields = self#visit_fields_t_opt under_ref (subst fields) in
-                if args <> [] || cgs <> [] then
-                  self#record (DType (chosen_lid, flag @ flags, 0, 0, Flat fields));
+                self#record (DType (chosen_lid, flag @ flags, 0, 0, Flat fields));
                 Hashtbl.replace state n (Black, chosen_lid)
             | flags, Union fields ->
                 let fields = List.map (fun (f, t) ->
                   let t = DeBruijn.subst_tn args t in
                   let t = self#visit_typ under_ref t in
                   f, t
                 ) fields in
-                if args <> [] || cgs <> [] then
-                  self#record (DType (chosen_lid, flag @ flags, 0, 0, Union fields));
+                self#record (DType (chosen_lid, flag @ flags, 0, 0, Union fields));
                 Hashtbl.replace state n (Black, chosen_lid)
             | flags, Abbrev t ->
                 let t = DeBruijn.subst_tn args t in
                 let t = self#visit_typ under_ref t in
-                if args <> [] || cgs <> [] then
-                  self#record (DType (chosen_lid, flag @ flags, 0, 0, Abbrev t));
+                self#record (DType (chosen_lid, flag @ flags, 0, 0, Abbrev t));
                 Hashtbl.replace state n (Black, chosen_lid)
             | _ ->
                 Hashtbl.replace state n (Black, chosen_lid)
@@ -545,13 +531,12 @@ let monomorphize_data_types map = object(self)
 
       | DType (lid, _, n_cgs, n, (Flat _ | Variant _ | Abbrev _ | Union _)) ->
           assert (n = 0 && n_cgs = 0);
-          (* This was not inserted earlier (see comment at the beginning of
-             visit_node, so we visit it here *)
-          Hashtbl.add state (lid, [], []) (Gray, lid);
-          let d = self#visit_decl false d in
-          Hashtbl.replace state (lid, [], []) (Black, lid);
+          (* Visit the declaration to trigger processing of referenced types *)
+          ignore (self#visit_decl false d);
+          (* Ensure the type itself is recorded in the correct DFS order *)
+          ignore (self#visit_node false (lid, [], []));
           Hashtbl.add seen_declarations lid ();
-          self#clear () @ [ d ]
+          self#clear ()
 
       | _ ->
           (* Not a type, e.g. a global; needs to be retained. *)

lib/Simplify.ml

@@ -1486,7 +1486,8 @@ and hoist_expr tbl loc pos e =
   | EFlat fields ->
       let lhs, fields = List.split (List.map (fun (ident, expr) ->
         let is_array = match e.typ, ident with
-          | TQualified lid, Some ident -> Helpers.is_array (Hashtbl.find tbl (lid, ident)) 
+          | TQualified lid, Some ident ->
+              (match Hashtbl.find_opt tbl (lid, ident) with Some t -> Helpers.is_array t | None -> false)
           | _ -> false
         in
         (* The rationale is that one must NOT hoist "ebufcreate" nodes that encode array

test/DeclOrder.fst

@@ -0,0 +1,42 @@
+module DeclOrder
+
+open FStar.HyperStack.ST
+module U32 = FStar.UInt32
+
+(* This test exercises the declaration ordering fix for non-polymorphic
+   types. The polymorphic wrapper 'box' triggers monomorphisation.
+   Type 'outer' uses box<inner> by value, so inner must be emitted
+   before the monomorphised box<inner>, which must be emitted before
+   outer. Without the DFS-ordering fix (commits d72e7fa0 and c105d056),
+   non-polymorphic types like 'inner' were deferred to source position,
+   appearing after the types that embed them by value. *)
+
+noeq
+type box ([@@@strictly_positive] a: Type0) = {
+  value: a;
+  tag: U32.t
+}
+
+noeq
+type outer = {
+  wrapped: box inner;
+  extra: U32.t
+}
+
+and inner = {
+  x: U32.t;
+  y: U32.t
+}
+
+let make_inner (): inner =
+  { x = 1ul; y = 2ul }
+
+let make_outer (): outer =
+  { wrapped = { value = make_inner (); tag = 0ul }; extra = 42ul }
+
+let main () =
+  let o = make_outer () in
+  if o.extra = 42ul then 0l else 1l
+
+
+

test/EnumAliasHelper.fst

@@ -0,0 +1,5 @@
+module EnumAliasHelper
+
+type status = | Active | Inactive
+
+let get_status (): status = Active

test/EnumAliasResolve.fst

@@ -0,0 +1,18 @@
+module EnumAliasResolve
+
+(* Establish dependency so both .krml files are extracted and bundled. *)
+let _dep: EnumAliasHelper.status = EnumAliasHelper.Active
+
+(* This type has the same constructor names (Active, Inactive) as
+   EnumAliasHelper.status. The DataTypes pass will share the tag enum,
+   making one type an abbreviation of the other. Without resolve_abbrev
+   in AstToCStar, mangle_enum produces the wrong name for the alias type. *)
+type mode = | Active | Inactive
+
+let check_mode (m: mode): FStar.Int32.t =
+  match m with
+  | Active -> 1l
+  | Inactive -> 0l
+
+let main () =
+  if check_mode Active = 1l then 0l else 1l

test/Makefile

@@ -47,7 +47,7 @@ endif
 FILES		= \
   $(patsubst %.fst,%.test,$(filter-out Unused_A.fst StaticHeaderAPI.fst \
     StaticHeaderLib.fst NameCollisionHelper.fst ML16Externals.fst MemCpyModel.fst \
-    Lowlevel.fst PrivateInclude1.fst $(BROKEN),$(wildcard *.fst))) \
+    Lowlevel.fst PrivateInclude1.fst EnumAliasHelper.fst $(BROKEN),$(wildcard *.fst))) \
   $(CRYPTO_FILES) \
   $(patsubst %.fst,%.test,$(wildcard ../book/*.fst ../book/notfslit/*.fst))
 

test/MutualStruct.fst

@@ -140,7 +140,7 @@ and object8_map_entry = {
 
 let f8 (x: object8_map) : Tot bool = true
 
-// This test extracts, but has failed to compile since #664
+// This test extracts and compiles.
 
 [@@no_auto_projectors]
 noeq