Fix long-standing issue with C Abstract Structs

krmllib/dist/generic/FStar_Issue.h

@@ -46,6 +46,8 @@ FStar_Issue_range_of_issue(FStar_Issue_issue i);
 
 extern Prims_list__Prims_string *FStar_Issue_context_of_issue(FStar_Issue_issue i);
 
+extern FStar_Pprint_document FStar_Issue_issue_to_doc(FStar_Issue_issue i);
+
 extern Prims_string FStar_Issue_render_issue(FStar_Issue_issue i);
 
 extern FStar_Issue_issue

krmllib/dist/generic/FStar_Order.c

@@ -6,6 +6,8 @@
 
 #include "FStar_Order.h"
 
+#include "Prims.h"
+
 bool FStar_Order_uu___is_Lt(FStar_Order_order projectee)
 {
   switch (projectee)

krmllib/dist/generic/FStar_Order.h

@@ -7,7 +7,6 @@
 #ifndef __FStar_Order_H
 #define __FStar_Order_H
 
-#include "Prims.h"
 #include <inttypes.h>
 #include "krmllib.h"
 #include "krml/internal/compat.h"

lib/Bundles.ml

@@ -254,8 +254,8 @@ let empty_deps = { internal = StringSet.empty; public = StringSet.empty }
 let drop_dinstinction { internal; public } =
   List.of_seq (StringSet.to_seq (StringSet.union internal public))
 
-class record_everything gen_dep = object
-  inherit [_] reduce
+class record_everything (gen_dep: ?constructor:unit -> lident -> _) = object(self)
+  inherit [_] reduce as super
   method plus { internal = i1; public = p1 } { internal = i2; public = p2 } =
     { internal = StringSet.union i1 i2; public = StringSet.union p1 p2 }
   method zero = empty_deps
@@ -265,6 +265,14 @@ class record_everything gen_dep = object
     gen_dep lid
   method! visit_TApp () lid _ =
     gen_dep lid
+  method! visit_EFlat ((_, t) as env) fields =
+    match t with
+    | TQualified lid ->
+        self#plus
+          (gen_dep ~constructor:() lid)
+          (super#visit_EFlat env fields)
+    | _ ->
+        super#visit_EFlat env fields
 end
 
 let direct_dependencies_with_internal files file_of =
@@ -278,15 +286,24 @@ let direct_dependencies_with_internal files file_of =
     ) set decls
   ) LidSet.empty files in
 
+  let c_abstract_struct = List.fold_left (fun set (_, decls) ->
+    List.fold_left (fun set decl ->
+      if List.mem Common.AbstractStruct (Ast.flags_of_decl decl) then
+        LidSet.add (Ast.lid_of_decl decl) set
+      else
+        set
+    ) set decls
+  ) LidSet.empty files in
+
   List.fold_left (fun by_file file ->
-    let gen_dep (callee: lident) =
+    let gen_dep ?constructor (callee: lident) =
       match file_of callee with
       | Some f when f <> fst file && not (Helpers.is_primitive callee) ->
           let is_internal = LidSet.mem callee internal in
           if Options.debug "dependencies" then
             KPrint.bprintf "In file %s, reference to %a (in %sheader %s)\n"
               (fst file) PrintAst.plid callee (if is_internal then "internal " else "") f;
-          if is_internal then
+          if is_internal || constructor = Some () && LidSet.mem callee c_abstract_struct then
             { empty_deps with internal = StringSet.singleton f }
           else
             { empty_deps with public = StringSet.singleton f }
@@ -318,11 +335,15 @@ let direct_dependencies_with_internal files file_of =
 
       method! visit_DType env name flags n_cgs n def =
         let is_c_abstract_struct = List.mem Common.AbstractStruct flags in
-        if self#concerns_us flags then
-          if is_c_abstract_struct then
+        if is_c_abstract_struct then
+          (* In `header_deps`, a C abstract struct always concerns us because it appears both in the
+             public (forward declaration, no body) and in the internal header (actual declaration). *)
+          if which = `Public then
             super#visit_DType env name flags n_cgs n (Abbrev TUnit)
           else
             super#visit_DType env name flags n_cgs n def
+        else if self#concerns_us flags then
+          super#visit_DType env name flags n_cgs n def
         else
           super#zero
 

lib/CStarToC11.ml

@@ -1391,9 +1391,9 @@ let either f1 f2 x =
   | [] -> f2 x
   | l -> l
 
-let if_private_or_abstract_struct f d =
+let if_private f d =
   let flags = flags_of_decl d in
-  if List.mem Private flags || List.mem AbstractStruct flags then
+  if List.mem Private flags then
     f d
   else
     []
@@ -1404,8 +1404,9 @@ let if_public f d =
   else
     []
 
-let if_internal f d =
-  if List.mem Internal (flags_of_decl d) then
+let if_internal_or_abstract_struct f d =
+  let flags = flags_of_decl d in
+  if List.mem Internal flags || List.mem AbstractStruct flags then
     (* let _ = KPrint.bprintf "%a is internal\n" PrintAst.Ops.plid (lid_of_decl d) in *)
     f d
   else
@@ -1448,7 +1449,7 @@ let mk_file m decls =
       none
       (either
         (mk_function_or_global_body m)
-        (if_private_or_abstract_struct (mk_type_or_external m C))))
+        (if_private (mk_type_or_external m C))))
     decls
 
 let mk_files (map: GlobalNames.mapping) files =
@@ -1500,10 +1501,10 @@ let mk_public_header (m: GlobalNames.mapping) decls =
 (* Private part if not already a static header, empty otherwise. *)
 let mk_internal_header (m: GlobalNames.mapping) decls =
   List.concat_map
-    (if_internal (
+    (if_internal_or_abstract_struct (
       (if_header_inline_static m
         (mk_static (either (mk_function_or_global_body m) (mk_type_or_external m ~is_inline_static:true C)))
-        (either (mk_function_or_global_stub m) (mk_type_or_external m H)))))
+        (either (mk_function_or_global_stub m) (mk_type_or_external m C)))))
     decls
 
 let mk_headers (map: GlobalNames.mapping)

lib/Inlining.ml

@@ -223,10 +223,18 @@ let cross_call_analysis files =
       inlining: inlining;
       wasm_mutable: bool;
       wasm_needs_getter: bool;
+      abstract_struct: bool;
     }
   end in
   let open T in
 
+  let pvis b = function
+    | Private -> Buffer.add_string b "Private"
+    | Internal -> Buffer.add_string b "Internal"
+    | Public -> Buffer.add_string b "Public"
+    | Workspace -> Buffer.add_string b "Workspace"
+  in
+
   (* We associate to each declaration some initial information. Three fields may
      change after initially filling the map:
      - visibility may go upward along the visibility lattice (this is only a
@@ -238,14 +246,19 @@ let cross_call_analysis files =
   let info_map = Helpers.build_map files (fun map d ->
     let f = flags_of_decl d in
     let name = lid_of_decl d in
+    let abstract_struct = List.mem Common.AbstractStruct f in
     let visibility =
-      if List.mem Common.Private f then
-        Private
-      else if List.mem Common.Internal f then
+      if List.mem Common.Internal f || abstract_struct then
+        (* C abstract structs start at internal, since their body is going to be in the internal
+           header. *)
         Internal
+      else if List.mem Common.Private f then
+        Private
       else
         Public
     in
+    if Options.debug "visibility-fixpoint" then
+      KPrint.bprintf "[initial visibility] %a: %a\n" plid name pvis visibility;
     let inlining =
       let is_static_inline = Helpers.is_static_header name in
       let is_inline = List.mem Common.Inline f || List.mem Common.MustInline f in
@@ -269,21 +282,14 @@ let cross_call_analysis files =
     in
     let wasm_needs_getter = false in
     let callers = LidSet.empty in
-    Hashtbl.add map (lid_of_decl d) { visibility; inlining; wasm_mutable; wasm_needs_getter; callers }
+    Hashtbl.add map (lid_of_decl d) { visibility; inlining; wasm_mutable; wasm_needs_getter; callers; abstract_struct }
   ) in
 
   (* We keep track of the declarations we have seen so far. Since the
      declarations are quasi-topologically ordered, a forward reference to
      another function indicates that there is mutual recursion. *)
   let seen = ref LidSet.empty in
 
-  let pvis b = function
-    | Private -> Buffer.add_string b "Private"
-    | Internal -> Buffer.add_string b "Internal"
-    | Public -> Buffer.add_string b "Public"
-    | Workspace -> Buffer.add_string b "Workspace"
-  in
-
   (* T.Visibility forms a trivial lattice where Private <= Internal <= Public *)
   let lub: visibility -> visibility -> visibility = max in
 
@@ -301,6 +307,10 @@ let cross_call_analysis files =
   let record_call_from_to caller callee =
     try
       let info = Hashtbl.find info_map callee in
+      if Options.debug "visibility-fixpoint" then
+        KPrint.bprintf "[visibility-fixpoint] recording cross-call from %a (%s) to %a (%s)\n"
+          plid caller (Option.value ~default:"<none>" (file_of caller))
+          plid callee (Option.value ~default:"<none>" (file_of callee));
       Hashtbl.replace info_map callee { info with callers = LidSet.add caller info.callers }
     with Not_found ->
       (* External type currently modeled as an lid without a definition (sigh) *)
@@ -492,9 +502,8 @@ let cross_call_analysis files =
           (visit true)#visit_expr_w () e
       | DExternal (_, _, _, _, _, t, _) ->
           (visit false)#visit_typ () t
-      | DType (_, flags, _, _, d) ->
-          if not (List.mem Common.AbstractStruct flags) then
-            (visit false)#visit_type_def () d
+      | DType (_, _flags, _, _, d) ->
+          (visit false)#visit_type_def () d
       end;
       seen := LidSet.add lid !seen
     ) decls
@@ -514,21 +523,35 @@ let cross_call_analysis files =
     if not (Hashtbl.mem info_map lid) then
       Warn.fatal_error "No equation for %a" plid lid;
     let info = Hashtbl.find info_map lid in
-    LidSet.fold (fun caller v -> lub v (valuation caller)) info.callers info.visibility
+    let adjust caller =
+      if (Hashtbl.find info_map caller).abstract_struct then
+        Internal
+      else
+        valuation caller
+    in
+    LidSet.fold (fun caller v -> lub v (adjust caller)) info.callers info.visibility
   ) in
 
   (* Adjust definitions based on `info_map` updated with fixpoint *)
   let files = List.map (fun (f, decls) ->
     f, List.map (fun d ->
       let lid = lid_of_decl d in
       let info = Hashtbl.find info_map lid in
+      let old_vis = info.visibility in
+      (* Fixpoint computation *)
       let info = { info with visibility = valuation (lid_of_decl d) } in
+      (* C abstract structs are treated as internal for the purposes of visibility computation,
+         but the convention is that they end up being marked as public for CStarToC11 to do the
+         right thing. (This may need fixing.) *)
+      let info = { info with visibility = if info.abstract_struct then Public else info.visibility } in
       if Options.debug "visibility-fixpoint" then
-        KPrint.bprintf "[adjustment]: %a: %a, wasm: mut %b getter %b\n"
-          plid lid pvis info.visibility info.wasm_mutable info.wasm_needs_getter;
+        KPrint.bprintf "[adjustment]: %a: %a --> %a, wasm: mut %b getter %b\n"
+          plid lid pvis old_vis pvis info.visibility info.wasm_mutable info.wasm_needs_getter;
+
       let remove_if cond flag flags = if cond then List.filter ((<>) flag) flags else flags in
       let add_if cond flag flags = if cond && not (List.mem flag flags) then flag :: flags else flags in
       let adjust flags =
+
         let flags = remove_if (info.inlining = Nope) Common.Inline flags in
         let flags = remove_if (info.inlining = Nope) Common.MustInline flags in
         let flags = remove_if (info.visibility <> Private) Common.Private flags in

lib/Monomorphization.ml

@@ -248,7 +248,7 @@ let monomorphize_data_types map = object(self)
   (* Current file, for warning purposes. *)
   val mutable current_file = ""
   (* Possibly populated with something relevant *)
-  val mutable best_hint: node * lident = (dummy_lid, [], []), dummy_lid
+  val mutable best_hint: node * lident * flag list = (dummy_lid, [], []), dummy_lid, []
   (* For forward references, a map from lid to its pending monomorphizations
      (type arguments) *)
   val pending_monomorphizations: (lident, (typ list * cg list)) Hashtbl.t = Hashtbl.create 41
@@ -314,15 +314,15 @@ let monomorphize_data_types map = object(self)
     let lid, ts, cgs = n in
     if ts = [] && cgs = [] then
       lid, []
-    else if fst best_hint = n then
-      snd best_hint, []
+    else if fst3 best_hint = n then
+      snd3 best_hint, []
     else
       let name, flags = NameGen.gen_lid lid ts (Cg cgs) in
       if Options.debug "monomorphization" then
         KPrint.bprintf "No hint provided for %a\n  current best hint: %a -> %a\n  picking: %a\n"
           ptyp (fold_tapp (lid, ts, []))
-          ptyp (fold_tapp (fst best_hint))
-          plid (snd best_hint)
+          ptyp (fold_tapp (fst3 best_hint))
+          plid (snd3 best_hint)
           plid name;
       name, flags
 
@@ -345,6 +345,7 @@ let monomorphize_data_types map = object(self)
         if Options.debug "data-types-traversal" then
           KPrint.bprintf "visiting %a: Not_found\n" ptyp (fold_tapp n);
         let chosen_lid, flag = self#lid_of n in
+        let flag = if fst3 best_hint = n then thd3 best_hint @ flag else flag in
         if lid = tuple_lid then begin
           Hashtbl.add state n (Gray, chosen_lid, false);
           let args = List.map (self#visit_typ under_ref) args in
@@ -450,16 +451,16 @@ let monomorphize_data_types map = object(self)
       if Options.debug "data-types-traversal" then
         KPrint.bprintf "decl %a\n" plid (lid_of_decl d);
       match d with
-      | DType (lid, _, 0, 0, Abbrev (TTuple args)) when not !Options.keep_tuples && not (Hashtbl.mem state (tuple_lid, args, [])) ->
+      | DType (lid, flags, 0, 0, Abbrev (TTuple args)) when not !Options.keep_tuples && not (Hashtbl.mem state (tuple_lid, args, [])) ->
           Hashtbl.remove map lid;
           if Options.debug "monomorphization" then
             KPrint.bprintf "%a abbreviation for %a\n" plid lid ptyp (TApp (tuple_lid, args));
-          best_hint <- (tuple_lid, args, []), lid;
+          best_hint <- (tuple_lid, args, []), lid, flags;
           ignore (self#visit_node false (tuple_lid, args, []));
           Hashtbl.add seen_declarations lid ();
           self#clear ()
 
-      | DType (lid, _, 0, 0, Abbrev ((TApp _ | TCgApp _) as t)) when not (Hashtbl.mem state (flatten_tapp t)) ->
+      | DType (lid, flags, 0, 0, Abbrev ((TApp _ | TCgApp _) as t)) when not (Hashtbl.mem state (flatten_tapp t)) ->
           (* We have not yet monomorphized this type, and conveniently, we have
              a type abbreviation that provides us with a name hint! We simply
              ditch the type abbreviation and replace it with a monomorphization
@@ -478,9 +479,9 @@ let monomorphize_data_types map = object(self)
           let abbrev_for_gc_type = Hashtbl.mem map hd && List.mem Common.GcType (fst (Hashtbl.find map hd)) in
 
           if abbrev_for_gc_type then
-            best_hint <- (hd, args, cgs), (fst lid, snd lid ^ "_gc")
+            best_hint <- (hd, args, cgs), (fst lid, snd lid ^ "_gc"), flags
           else
-            best_hint <- (hd, args, cgs), lid;
+            best_hint <- (hd, args, cgs), lid, flags;
 
           ignore (self#visit_node false (hd, args, cgs));
 

lib/Options.ml

@@ -1,7 +1,7 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
 (* Licensed under the Apache 2.0 and MIT Licenses. *)
 
-type include_ = All | HeaderOnly of string | COnly of string
+type include_ = All | InternalOnly of string | HeaderOnly of string | COnly of string
 
 type compiler_flavor =
   | Generic
@@ -27,6 +27,7 @@ let compiler_flavor_of_string = function
 
 let pinc b = function
   | All -> Buffer.add_string b "*"
+  | InternalOnly h
   | HeaderOnly h -> Buffer.add_string b h; Buffer.add_string b ".h"
   | COnly h -> Buffer.add_string b h; Buffer.add_string b ".c"