Fix visibility analysis and do not traverse CAbstractStruct into type…

… definitions

This fixes #247

src/Inlining.ml

@@ -210,6 +210,7 @@ let cross_call_analysis files =
    * be safely marked as private. The invariant is not established yet. *)
   let private_or_internal = Hashtbl.create 41 in
   let safely_inline = Hashtbl.create 41 in
+  let c_abstract_structs = Hashtbl.create 41 in
 
   (* Constants that will end up being mutable in Wasm because of the compilation
    * scheme of constants as little-endian encoded pre-laid out byte literals
@@ -229,6 +230,9 @@ let cross_call_analysis files =
         (* -static-header takes precedence over private, see CStarToC11.ml *)
         Hashtbl.add private_or_internal name T.Private;
 
+      if List.mem AbstractStruct flags then
+        Hashtbl.add c_abstract_structs name ();
+
       if List.mem Inline flags then
         Hashtbl.add safely_inline name ();
 
@@ -369,19 +373,20 @@ let cross_call_analysis files =
         Hashtbl.find_opt private_or_internal (lid_of_decl d) = Some T.Private
 
       method private remove_and_visit name =
+        (* KPrint.bprintf "Remove_and_visit %a with mode %s\n" plid name *)
+        (*   (match !mode with `Public -> "public" | `Internal -> "internal"); *)
         if Hashtbl.mem private_or_internal name then begin
-          (* KPrint.bprintf "Remove_and_visit %a with mode %s\n" plid name *)
-          (*   (match !mode with `Public -> "public" | `Internal -> "internal"); *)
           match !mode with
           | `Internal ->
               Hashtbl.replace private_or_internal name T.Internal
           | `Public ->
               Hashtbl.remove private_or_internal name
         end;
-        if not (Hashtbl.mem seen name) || mode_lt (Hashtbl.find seen name) !mode then begin
+        if (not (Hashtbl.mem seen name) || mode_lt (Hashtbl.find seen name) !mode) then begin
           Hashtbl.replace seen name !mode;
-          try super#visit_decl () (Hashtbl.find decl_map name)
-          with Not_found -> ()
+          if not (Hashtbl.mem c_abstract_structs name) then
+            try super#visit_decl () (Hashtbl.find decl_map name)
+            with Not_found -> ()
         end
 
       method! visit_TQualified () name =
@@ -409,7 +414,10 @@ let cross_call_analysis files =
         (* We visit any non-private declaration; static header takes precedence
            over private. *)
         let name = lid_of_decl d in
-        if not (self#still_private d) || Helpers.is_static_header name then begin
+        let flags = flags_of_decl d in
+        if (not (self#still_private d) || Helpers.is_static_header name) &&
+          not (List.mem AbstractStruct flags)
+        then begin
           mode :=
             match Hashtbl.find private_or_internal name with
             | exception Not_found -> `Public
@@ -443,6 +451,7 @@ let cross_call_analysis files =
         | T.Private -> flags
         | T.Internal -> Internal :: List.filter ((<>) Private) flags
       in
+      (* KPrint.bprintf "%a: %s\n" plid name (String.concat " " (List.map show_flag flags)); *)
       if !Options.cc = "compcert" then
         keep_if safely_inline Inline name flags
       else

test/AbstractStruct2.fst

@@ -0,0 +1,30 @@
+module AbstractStruct2
+module HS = FStar.HyperStack
+module B = LowStar.Buffer
+
+open FStar.HyperStack.ST
+
+[@@CAbstractStruct]
+noeq
+type handle = {
+  something: bool;
+  another: AbstractStructAbstract.t AbstractStructParameter.param;
+}
+
+let init (_:unit) =
+  let h = {
+    something = false;
+    another = AbstractStructAbstract.make AbstractStructParameter.({ param_one = true; param_two = false })
+  } in
+  B.malloc HS.root h 1ul
+
+open LowStar.BufferOps
+open AbstractStructParameter
+open AbstractStructAbstract
+
+let main () =
+  let p  = init () in
+  if (read (!*p).another).param_two then
+    1l
+  else
+    0l

test/AbstractStruct2.fsti

@@ -0,0 +1,13 @@
+module AbstractStruct2
+open FStar.HyperStack.ST
+module B = LowStar.Buffer
+
+[@@CAbstractStruct]
+val handle : Type0
+
+val init (_:unit)
+  : ST (B.pointer handle)
+       (requires fun _ -> True)
+       (ensures fun _ handle h1 -> B.live h1 handle)
+
+val main: unit -> St Int32.t

test/AbstractStructAbstract.fst

@@ -0,0 +1,6 @@
+module AbstractStructAbstract
+
+type t a = (bool & a)
+
+let make #a x = (false, x)
+let read #a t = snd t

test/AbstractStructAbstract.fsti

@@ -0,0 +1,6 @@
+module AbstractStructAbstract
+
+val t (a:Type0) : Type0
+
+val make (#a:Type0) (x:a) : t a
+val read (#a:Type0) (x:t a) : a

test/AbstractStructParameter.fsti

@@ -0,0 +1,7 @@
+module AbstractStructParameter
+
+[@@CAbstractStruct]
+type param = {
+  param_one: bool;
+  param_two: bool
+}

test/Makefile

@@ -9,7 +9,8 @@ KRML		= $(KRML_BIN) $(KOPTS) $(TEST_OPTS)
 # HigherOrder6?) and helper files that are required for multiple-module tests
 BROKEN		= \
   HigherOrder6.fst ForwardDecl.fst BlitNull.fst \
-  Ctypes1.fst Ctypes2.fst Ctypes3.fst Ctypes4.fst Abstract.fsti
+  Ctypes1.fst Ctypes2.fst Ctypes3.fst Ctypes4.fst \
+  AbstractStructAbstract.fst
 
 # Lowlevel is not really broken, but its test shouldn't be run since it's a
 # special file and doesn't have a main.