Merge pull request #213 from FStarLang/protz_eaddrof

Support for C eaddrof, union and array types

kremlib/dist/generic/FStar_Pervasives.h

@@ -31,6 +31,7 @@ typedef void *FStar_Pervasives_pattern;
 #define FStar_Pervasives_UnfoldFully 11
 #define FStar_Pervasives_UnfoldAttr 12
 #define FStar_Pervasives_UnfoldQual 13
+#define FStar_Pervasives_Unmeta 14
 
 typedef uint8_t FStar_Pervasives_norm_step_tags;
 
@@ -87,6 +88,8 @@ extern bool FStar_Pervasives_uu___is_UnfoldQual(FStar_Pervasives_norm_step proje
 extern Prims_list__Prims_string
 *FStar_Pervasives___proj__UnfoldQual__item___0(FStar_Pervasives_norm_step projectee);
 
+extern bool FStar_Pervasives_uu___is_Unmeta(FStar_Pervasives_norm_step projectee);
+
 extern FStar_Pervasives_norm_step FStar_Pervasives_simplify;
 
 extern FStar_Pervasives_norm_step FStar_Pervasives_weak;
@@ -116,6 +119,8 @@ extern FStar_Pervasives_norm_step FStar_Pervasives_delta_attr(Prims_list__Prims_
 extern FStar_Pervasives_norm_step
 FStar_Pervasives_delta_qualifier(Prims_list__Prims_string *s);
 
+extern FStar_Pervasives_norm_step FStar_Pervasives_unmeta;
+
 typedef struct Prims_list__FStar_Pervasives_norm_step_s Prims_list__FStar_Pervasives_norm_step;
 
 typedef struct Prims_list__FStar_Pervasives_norm_step_s

kremlib/dist/generic/FStar_UInt_8_16_32_64.h

@@ -14,6 +14,8 @@
 
 
 
+extern Prims_int FStar_UInt64_n;
+
 extern bool FStar_UInt64_uu___is_Mk(uint64_t projectee);
 
 extern Prims_int FStar_UInt64___proj__Mk__item__v(uint64_t projectee);
@@ -22,6 +24,14 @@ extern Prims_int FStar_UInt64_v(uint64_t x);
 
 extern uint64_t FStar_UInt64_uint_to_t(Prims_int x);
 
+extern uint64_t FStar_UInt64_zero;
+
+extern uint64_t FStar_UInt64_one;
+
+extern uint64_t FStar_UInt64_minus(uint64_t a);
+
+extern uint32_t FStar_UInt64_n_minus_one;
+
 static inline uint64_t FStar_UInt64_eq_mask(uint64_t a, uint64_t b)
 {
   uint64_t x = a ^ b;

kremlib/dist/generic/Makefile.include

@@ -1,5 +1,5 @@
 USER_TARGET=libkremlib.a
 USER_CFLAGS=
 USER_C_FILES=testlib.c prims.c lowstar_printf.c fstar_uint8.c fstar_uint64.c fstar_uint32.c fstar_uint16.c fstar_string.c fstar_io.c fstar_int8.c fstar_int64.c fstar_int32.c fstar_int16.c fstar_hyperstack_io.c fstar_dyn.c fstar_date.c fstar_char.c fstar_bytes.c c_string.c c.c
-ALL_C_FILES=WasmSupport.c FStar_ModifiesGen.c FStar_VConfig.c FStar_Order.c
-ALL_H_FILES=Prims.h FStar_BitVector.h FStar_UInt.h FStar_UInt_8_16_32_64.h FStar_UInt128.h LowStar_Endianness.h C_Failure.h FStar_String.h LowStar_Printf.h FStar_HyperStack_IO.h TestLib.h C_String.h C.h FStar_Bytes.h FStar_Char.h FStar_IO.h FStar_Float.h FStar_Monotonic_HyperStack.h C_Loops.h WasmSupport.h FStar_Int_Cast.h FStar_Int.h FStar_Int8.h FStar_Int32.h FStar_Int64.h FStar_All.h FStar_Monotonic_Heap.h FStar_ST.h FStar_Kremlin_Endianness.h FStar_ModifiesGen.h FStar_VConfig.h FStar_Order.h FStar_Date.h FStar_HyperStack_All.h FStar_HyperStack_ST.h FStar_Monotonic_HyperHeap.h FStar_Int16.h FStar_Math_Lib.h FStar_Mul.h FStar_Pervasives.h
+ALL_C_FILES=WasmSupport.c FStar_ModifiesGen.c FStar_Order.c FStar_VConfig.c
+ALL_H_FILES=Prims.h FStar_BitVector.h FStar_UInt.h FStar_UInt_8_16_32_64.h FStar_UInt128.h LowStar_Endianness.h C_Failure.h FStar_String.h LowStar_Printf.h FStar_HyperStack_IO.h TestLib.h C_String.h C.h FStar_Bytes.h FStar_Char.h FStar_IO.h FStar_Float.h FStar_Monotonic_HyperStack.h C_Loops.h WasmSupport.h FStar_Int_Cast.h FStar_Int.h FStar_Int8.h FStar_Int32.h FStar_Int64.h FStar_All.h FStar_Monotonic_Heap.h FStar_ST.h FStar_Kremlin_Endianness.h FStar_ModifiesGen.h FStar_Order.h FStar_Date.h FStar_HyperStack_All.h FStar_HyperStack_ST.h FStar_Monotonic_HyperHeap.h FStar_VConfig.h FStar_Int16.h FStar_Math_Lib.h FStar_Mul.h FStar_Pervasives.h

kremlib/dist/generic/libkremlib.def

@@ -14,6 +14,19 @@ EXPORTS
   WasmSupport_betole32
   WasmSupport_betole64
   WasmSupport_memzero
+  FStar_Order_uu___is_Lt
+  FStar_Order_uu___is_Eq
+  FStar_Order_uu___is_Gt
+  FStar_Order_ge
+  FStar_Order_le
+  FStar_Order_ne
+  FStar_Order_gt
+  FStar_Order_lt
+  FStar_Order_eq
+  FStar_Order_lex
+  FStar_Order_order_from_int
+  FStar_Order_int_of_order
+  FStar_Order_compare_int
   FStar_VConfig___proj__Mkvconfig__item__initial_fuel
   FStar_VConfig___proj__Mkvconfig__item__max_fuel
   FStar_VConfig___proj__Mkvconfig__item__initial_ifuel
@@ -41,16 +54,3 @@ EXPORTS
   FStar_VConfig___proj__Mkvconfig__item__z3seed
   FStar_VConfig___proj__Mkvconfig__item__trivial_pre_for_unannotated_effectful_fns
   FStar_VConfig___proj__Mkvconfig__item__reuse_hint_for
-  FStar_Order_uu___is_Lt
-  FStar_Order_uu___is_Eq
-  FStar_Order_uu___is_Gt
-  FStar_Order_ge
-  FStar_Order_le
-  FStar_Order_ne
-  FStar_Order_gt
-  FStar_Order_lt
-  FStar_Order_eq
-  FStar_Order_lex
-  FStar_Order_order_from_int
-  FStar_Order_int_of_order
-  FStar_Order_compare_int

kremlib/dist/minimal/FStar_UInt_8_16_32_64.h

@@ -16,14 +16,22 @@
 
 
 
-extern bool FStar_UInt64_uu___is_Mk(uint64_t projectee);
+extern Prims_int FStar_UInt64_n;
 
 extern Prims_int FStar_UInt64___proj__Mk__item__v(uint64_t projectee);
 
 extern Prims_int FStar_UInt64_v(uint64_t x);
 
 extern uint64_t FStar_UInt64_uint_to_t(Prims_int x);
 
+extern uint64_t FStar_UInt64_zero;
+
+extern uint64_t FStar_UInt64_one;
+
+extern uint64_t FStar_UInt64_minus(uint64_t a);
+
+extern uint32_t FStar_UInt64_n_minus_one;
+
 static inline uint64_t FStar_UInt64_eq_mask(uint64_t a, uint64_t b)
 {
   uint64_t x = a ^ b;
@@ -56,8 +64,6 @@ extern uint64_t FStar_UInt64_of_string(Prims_string uu___);
 
 extern Prims_int FStar_UInt32_n;
 
-extern bool FStar_UInt32_uu___is_Mk(uint32_t projectee);
-
 extern Prims_int FStar_UInt32___proj__Mk__item__v(uint32_t projectee);
 
 extern Prims_int FStar_UInt32_v(uint32_t x);
@@ -104,8 +110,6 @@ extern uint32_t FStar_UInt32_of_string(Prims_string uu___);
 
 extern Prims_int FStar_UInt16_n;
 
-extern bool FStar_UInt16_uu___is_Mk(uint16_t projectee);
-
 extern Prims_int FStar_UInt16___proj__Mk__item__v(uint16_t projectee);
 
 extern Prims_int FStar_UInt16_v(uint16_t x);
@@ -152,8 +156,6 @@ extern uint16_t FStar_UInt16_of_string(Prims_string uu___);
 
 extern Prims_int FStar_UInt8_n;
 
-extern bool FStar_UInt8_uu___is_Mk(uint8_t projectee);
-
 extern Prims_int FStar_UInt8___proj__Mk__item__v(uint8_t projectee);
 
 extern Prims_int FStar_UInt8_v(uint8_t x);

src/DataTypes.ml

@@ -35,10 +35,16 @@ let remove_unused_type_arguments files =
 
     let def_map = Helpers.build_map files (fun map d ->
       match d with
-      | DType (lid, _, n, d) -> Hashtbl.add map lid (n, d)
+      | DType (lid, _, n, d) ->
+          Hashtbl.add map lid (`Typ (n, d))
+      | DFunction (_, _, n, t_ret, lid, bs, body) ->
+          let ts = List.map (fun b -> b.typ) bs in
+          Hashtbl.add map lid (`Fun (n, t_ret :: ts, body))
       | _ -> ()
     ) in
 
+    (* An ad-hoc reduce visitor over the bool monoid that simply returns true if
+      there is an occurrence of the i-th type parameter.*)
     let find_ith valuation = object(self)
       inherit [_] reduce
       method zero = false
@@ -47,20 +53,35 @@ let remove_unused_type_arguments files =
 
       method! visit_TBound (j, n) i =
         j = n - i - 1
-      method! visit_TApp env lid args =
+
+      method private visit_app env lid args =
         let args = List.mapi (fun i arg ->
           if valuation (lid, i) then
             self#visit_typ env arg
           else
             self#zero
         ) args in
         List.fold_left self#plus self#zero args
+
+      method! visit_TApp env lid args =
+        self#visit_app env lid args
+
+      method! visit_ETApp env e args =
+        let lid = assert_elid e.node in
+        self#visit_app (fst env) lid args
     end in
 
     let equations (lid, i) valuation =
       try
-        let n, def = Hashtbl.find def_map lid in
-        (find_ith valuation)#visit_type_def (i, n) def
+        match Hashtbl.find def_map lid with
+        | `Typ (n, def) ->
+            (find_ith valuation)#visit_type_def (i, n) def
+        | `Fun (n, ts, def) ->
+            (* This is an approximation because this LFP is not mutually
+               recursive with private-functions unused argument elimination. *)
+            List.fold_left (||) false
+              ((find_ith valuation)#visit_expr_w (i, n) def ::
+                List.map ((find_ith valuation)#visit_typ (i, n)) ts)
       with Not_found ->
         true
     in
@@ -79,10 +100,10 @@ let remove_unused_type_arguments files =
         if i = n then
           kept, def
         else
-          if uses_nth lid (n - i - 1) then
+          if uses_nth lid i then
             chop (kept + 1) (i + 1) def
           else
-            let def = (new DeBruijn.subst_t TAny)#visit_type_def i def in
+            let def = (new DeBruijn.subst_t TAny)#visit_type_def (n - i - 1) def in
             chop kept (i + 1) def
       in
       let n, def = chop 0 0 def in
@@ -101,6 +122,39 @@ let remove_unused_type_arguments files =
         TApp (lid, args)
       else
         TQualified lid
+
+    method! visit_DFunction env cc flags n ret lid binders def =
+      let binders = self#visit_binders_w env binders in
+      let ret = self#visit_typ env ret in
+      let def = self#visit_expr_w env def in
+      let rec chop kept i (def, binders, ret) =
+        if i = n then
+          kept, (def, binders, ret)
+        else
+          if uses_nth lid i then
+            chop (kept + 1) (i + 1) (def, binders, ret)
+          else
+            let def = DeBruijn.subst_te TAny (n - i - 1) def in
+            let binders = List.map (fun { node; typ } -> { node; typ = DeBruijn.subst_t TAny (n - i - 1) typ }) binders in
+            let ret = DeBruijn.subst_t TAny (n - i - 1) ret in
+            chop kept (i + 1) (def, binders, ret)
+      in
+      let n, (def, binders, ret) = chop 0 0 (def, binders, ret) in
+      DFunction (cc, flags, n, ret, lid, binders, def)
+
+    method! visit_ETApp env e args =
+      let lid = assert_elid e.node in
+      let args = List.map (self#visit_typ_wo env) args in
+      let args = KList.filter_mapi (fun i arg ->
+        if uses_nth lid i then
+          Some arg
+        else
+          None
+      ) args in
+      if List.length args > 0 then
+        ETApp (e, args)
+      else
+        e.node
   end in
 
   NamingHints.hints := List.map (fun ((head, args), hint) ->

src/InputAst.ml

@@ -40,6 +40,7 @@ and decl =
        * for it. *)
   | DExternal2 of (calling_convention option * flag list * lident * typ * string list)
       (** New variant that keeps names of arguments *)
+  | DUntaggedUnion of (lident * flag list * int * (ident * typ) list)
 
 and fields_t =
   (ident * (typ * bool)) list
@@ -101,6 +102,7 @@ and expr =
   | EAbortT of (string * typ)
   | EComment of (string * expr * string)
   | EStandaloneComment of string
+  | EAddrOf of expr
 
 and branches =
   branch list
@@ -145,6 +147,8 @@ and typ =
   | TApp of (lident * typ list)
   | TTuple of typ list
   | TConstBuf of typ
+  | TArray of (typ * K.t)
+    (** For flat arrays within structs. *)
 
 let flatten_arrow =
   let rec flatten_arrow acc = function

src/InputAstToAst.ml

@@ -56,6 +56,8 @@ let rec mk_decl = function
         Variant (List.map (fun (ident, fields) -> ident, mk_tfields fields) branches))
   | I.DTypeAbstractStruct name ->
       DType (name, [], 0, Forward)
+  | I.DUntaggedUnion (name, flags, n, branches) ->
+      DType (name, flags, n, Union (List.map (fun (f, t) -> f, mk_typ t) branches))
 
 and mk_binders bs =
   List.map mk_binder bs
@@ -95,6 +97,8 @@ and mk_typ = function
       TApp (lid, List.map mk_typ ts)
   | I.TTuple ts ->
       TTuple (List.map mk_typ ts)
+  | I.TArray (t, c) ->
+      TArray (mk_typ t, c)
 
 and mk_expr = function
   | I.EBound i ->
@@ -179,6 +183,8 @@ and mk_expr = function
       mk (EComment (before, mk_expr e, after))
   | I.EStandaloneComment s ->
       mk (EStandaloneComment s)
+  | I.EAddrOf e ->
+      mk (EAddrOf (mk_expr e))
 
 and mk_branches branches =
   List.map mk_branch branches