From aa80cc9035cf8e247af6e614ffc4a6d2444c8b6f Mon Sep 17 00:00:00 2001 From: John Li Date: Thu, 12 Aug 2021 08:30:00 -0700 Subject: [PATCH] Extraction for Steel.C.Array --- examples/steel/arraystructs/Steel.C.Array.fst | 4 ++ .../steel/arraystructs/Steel.C.Array.fsti | 29 +++++++++++- src/extraction/FStar.Extraction.Kremlin.fs | 47 ++++++++++++++++++- 3 files changed, 78 insertions(+), 2 deletions(-) diff --git a/examples/steel/arraystructs/Steel.C.Array.fst b/examples/steel/arraystructs/Steel.C.Array.fst index cc18cf407dd..3ac9b1d12cd 100644 --- a/examples/steel/arraystructs/Steel.C.Array.fst +++ b/examples/steel/arraystructs/Steel.C.Array.fst @@ -28,6 +28,10 @@ let array_elements_pcm let array_pcm t n = S.prod_pcm (array_elements_pcm t n) +let array_view_type_sized t n' n = array_view_type t n + +let unfold_array_view_type_sized t n' n = () + [@"opaque_to_smt"] let rec raise_list_array_domain (t: Type u#0) diff --git a/examples/steel/arraystructs/Steel.C.Array.fsti b/examples/steel/arraystructs/Steel.C.Array.fsti index 2fb44bfae5c..c73580fe2d7 100644 --- a/examples/steel/arraystructs/Steel.C.Array.fsti +++ b/examples/steel/arraystructs/Steel.C.Array.fsti @@ -22,6 +22,10 @@ open Steel.Effect open FStar.Ghost open Steel.Effect.Atomic +open Steel.C.Typedef +open Steel.C.PCM +open Typenat + #set-options "--ide_id_info_off" /// A library for arrays in Steel @@ -32,9 +36,20 @@ val array_pcm_carrier (t: Type u#0) (n: Ghost.erased size_t) : Type u#0 val array_pcm (t: Type u#0) (n: Ghost.erased size_t) : Tot (Steel.C.PCM.pcm (array_pcm_carrier t n)) // FIXME: how to produce array type t[n] as the type of some struct field? -let array_view_type (t: Type u#0) (n: size_t) : Type u#0 = +let array_view_type (t: Type u#0) (n: size_t) +: Type u#0 = Seq.lseq t (size_v n) +/// A variant of array_view_type, which records the length of the +/// array in Type as a Typenat, for extraction +let size_t_of (n': Type u#0) = n:size_t{n' == nat_t_of_nat (size_v n)} +val array_view_type_sized (t: Type u#0) (n': Type u#0) (n: size_t_of n') +: Type u#0 +val unfold_array_view_type_sized + (t: Type u#0) (n': Type u#0) (n: size_t_of n') +: Lemma (array_view_type_sized t n' n == array_view_type t n) + [SMTPat (array_view_type_sized t n' n)] + val array_view (t: Type u#0) (n: size_t) : Pure (Steel.C.Ref.sel_view (array_pcm t n) (array_view_type t n) false) (requires (size_v n > 0)) @@ -49,6 +64,18 @@ val array (base: Type u#0) (t:Type u#0) : Type u#0 val len (#base: Type) (#t: Type) (a: array base t) : GTot size_t let length (#base: Type) (#t: Type) (a: array base t) : GTot nat = size_v (len a) +// TODO +val array_is_unit (t: Type0) (n: size_t) (a: array_pcm_carrier t n) +: b:bool{b <==> a == one (array_pcm t n)} + +let array_typedef_sized (t: Type0) (n': Type0) (n: size_t_of n'{size_v n > 0}): typedef = { + carrier = array_pcm_carrier t n; + pcm = array_pcm t n; + view_type = array_view_type_sized t n' n; + view = array_view t n; + is_unit = array_is_unit t n; +} + /// Combining the elements above to create an array vprop /// TODO: generalize to any view diff --git a/src/extraction/FStar.Extraction.Kremlin.fs b/src/extraction/FStar.Extraction.Kremlin.fs index 0b6768f7911..078539810d5 100644 --- a/src/extraction/FStar.Extraction.Kremlin.fs +++ b/src/extraction/FStar.Extraction.Kremlin.fs @@ -190,6 +190,7 @@ and typ = | TApp of lident * list | TTuple of list | TConstBuf of typ + | TArray of typ * constant (** Versioned binary writing/reading of ASTs *) @@ -598,6 +599,17 @@ and translate_type_decl env ty: option = | Some fields -> print_endline "Got fields:"; + // Unlike in arguments, fixed-size arrays in structs do not decay to pointers + let rec translate_field_type env ty = + match ty with + | MLTY_Named ([t; n; _], p) + when Syntax.string_of_mlpath p = "Steel.C.Array.array_view_type_sized" + // TODO add support for fixed-size arrays to Steel.C.Array.fsti + -> + let int_of_typenat s = failwith "unimplemented" in // TODO + TArray (translate_field_type env t, (UInt32, int_of_typenat n)) + | t -> translate_type env t + in List.fold_left (fun () (field, ty) -> BU.print2 " %s : %s\n" @@ -610,7 +622,7 @@ and translate_type_decl env ty: option = (fun (field, ty) -> BU.print1 "Translating %s.\n" (FStar.Extraction.ML.Code.string_of_mlty ([], "") ty); - (field, translate_type env ty)) + (field, translate_field_type env ty)) fields) in match ty with @@ -730,6 +742,19 @@ and translate_type env t: typ = | MLTY_Named ([_; arg; _; _], p) when Syntax.string_of_mlpath p = "Steel.C.Reference.ref" + -> + let rec skip_array_view_types ty = + match ty with + | MLTY_Named ([ty; _; _], p) when + Syntax.string_of_mlpath p = "Steel.C.Array.array_view_type_sized" + -> + skip_array_view_types ty + | _ -> ty + in + TBuf (translate_type env (skip_array_view_types arg)) + + | MLTY_Named ([_; arg], p) when + Syntax.string_of_mlpath p = "Steel.C.Array.array" -> TBuf (translate_type env arg) @@ -1212,6 +1237,26 @@ and translate_expr env e: expr = EBufRead (translate_expr env r, EConstant (UInt32, "0")), translate_expr env x) + | MLE_App ({expr=MLE_TApp ({expr=MLE_Name p}, [_; _])}, [r]) + when string_of_mlpath p = "Steel.C.Array.ref_of_array" -> + translate_expr env r + + | MLE_App ({expr=MLE_TApp ({expr=MLE_Name p}, [_; _])}, [r]) + when string_of_mlpath p = "Steel.C.Array.mk_array_of_ref" -> + translate_expr env r + + | MLE_App ({expr=MLE_TApp ({expr=MLE_Name p}, [_; _])}, [_; r]) + when string_of_mlpath p = "Steel.C.Array.intro_varray" -> + translate_expr env r + + | MLE_App ({expr=MLE_TApp ({expr=MLE_Name p}, [_; _])}, [r; i]) + when string_of_mlpath p = "Steel.C.Array.index" -> + EBufRead (translate_expr env r, translate_expr env i) + + | MLE_App ({expr=MLE_TApp ({expr=MLE_Name p}, [_; _])}, [r; i; x]) + when string_of_mlpath p = "Steel.C.Array.upd" -> + EBufWrite (translate_expr env r, translate_expr env i, translate_expr env x) + | MLE_App (head, args) -> EApp (translate_expr env head, List.map (translate_expr env) args)