diff --git a/lib/DataTypes.ml b/lib/DataTypes.ml index d13d6431..ee0f90b7 100644 --- a/lib/DataTypes.ml +++ b/lib/DataTypes.ml @@ -687,22 +687,14 @@ let remove_unit_buffers = object (self) end -let remove_unit_fields = object (self) +let build_unit_field_table erasable_fields = object (self) inherit [_] map - val erasable_fields = Hashtbl.create 41 - val mutable atoms = [] - method private is_erasable = function | TUnit -> true | _ -> false - method private default_value = function - | TUnit -> EUnit - | TAny -> EAny - | t -> Warn.fatal_error "default_value: %a" ptyp t - method! visit_DType _ lid flags n_cgs n type_def = match type_def with | Variant branches -> @@ -737,6 +729,19 @@ let remove_unit_fields = object (self) Some (f, (t, m)) ) fields +end + +let remove_unit_fields erasable_fields = object (self) + + inherit [_] map + + val mutable atoms = [] + + method private default_value = function + | TUnit -> EUnit + | TAny -> EAny + | t -> Warn.fatal_error "default_value: %a" ptyp t + (* As we're about to visit a pattern, we collect binders for now-defunct * fields, and replace them with default values in the corresponding branch. *) method! visit_branch _ (binders, pat, expr) = @@ -1369,7 +1374,9 @@ let simplify files = (* Unit elimination, after monomorphization *) let optimize files = let files = remove_unit_buffers#visit_files () files in - let files = remove_unit_fields#visit_files () files in + let tbl = Hashtbl.create 41 in + let files = (build_unit_field_table tbl)#visit_files () files in + let files = (remove_unit_fields tbl)#visit_files () files in files (* For Rust, we leave `match` nodes in the AST -- Rust *does* have diff --git a/lib/Monomorphization.ml b/lib/Monomorphization.ml index 8fe68e6c..c91e6e19 100644 --- a/lib/Monomorphization.ml +++ b/lib/Monomorphization.ml @@ -332,114 +332,145 @@ 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) = - (* 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 lid, args, cgs = n in - (* White, gray or black? *) - match Hashtbl.find state n with - | exception Not_found -> - let chosen_lid, flag = self#lid_of n in - if Options.debug "data-types-traversal" then - KPrint.bprintf "visiting %a: Not_found --> %a\n" ptyp (fold_tapp n) plid chosen_lid; - 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); - (* For tuples, we immediately know how to generate a definition. *) - let fields = List.mapi (fun i arg -> Some (self#field_at i), (arg, false)) args in - self#record (DType (chosen_lid, [ Common.Private ] @ flag, 0, 0, Flat fields)); - Hashtbl.replace state n (Black, chosen_lid) - end else begin - (* This specific node has not been visited yet. *) - Hashtbl.add state n (Gray, chosen_lid); - - let subst fields = List.map (fun (field, (t, m)) -> - field, (DeBruijn.subst_tn args (DeBruijn.subst_ctn' cgs t), m) - ) fields in - assert (not (Hashtbl.mem map lid) || not (has_variables args) && not (has_cg_variables cgs)); - begin match Hashtbl.find map lid with - | exception Not_found -> - (* Unknown, external non-polymorphic lid, e.g. Prims.int *) - Hashtbl.replace state n (Black, chosen_lid) - | flags, ((Variant _ | Flat _ | Union _) as def) when under_ref && not (Hashtbl.mem seen_declarations lid) -> - (* FORWARD DECLARATION: this is unrelated to monomorphization (but we do it - here anyway). An occurrence of `t*` appears before the definition of `t`; we - pick a name, insert a forward declaration for `t`, then remember that *once we - have see the definition of `t`*, we will insert the monomorphized `t___ts` at that - specific location. - - The comment below furthermore tries to explain why we do things this way (as - opposed to inserting the monomorphized `t___ts` immediately). - - Because this looks up a definition in the global map, the - definitions are reordered according to the traversal order, which - is generally a good idea (we accept more programs!), EXCEPT - when the user relies on mutual recursion behind a reference - (pointer) type. In that case, following the type dependency graph is - generally not a good idea, since we may go from a valid - ordering to an invalid one (see tests/MutualStruct.fst). So, - the intent here (i.e., when under a ref type) is that: - - tuple types ALWAYS get monomorphized on-demand (see - above) - - abbreviations are fine and won't cause further issues - - data types, however, need to have their names allocated and a - forward reference inserted (TODO: at most once), then the - specific choice of type arguments need to be recorded as - something we want to visit later (once we're done with this - particular traversal)... *) - if Options.debug "data-types-traversal" then - KPrint.bprintf "DEFERRING %a\n" ptyp (fold_tapp n); - if match def with Union _ -> true | _ -> false then - self#record (DType (chosen_lid, flags, 0, 0, Forward FUnion)) - else - self#record (DType (chosen_lid, flags, 0, 0, Forward FStruct)); - Hashtbl.add pending_monomorphizations lid (args, cgs); - (* FORWARD DECLARATIONS: remove us from the state to make sure future occurences of the - same situation send us through this codepath again *) - Hashtbl.remove state n - | 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 - 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 - 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) -> + (* 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 + fst3 n + else + (* We recursively visit the arguments. This avoids inconsistencies where + the map would previously record both t> and t 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 lid, args, cgs = n in + (* White, gray or black? *) + match Hashtbl.find state n with + | exception Not_found -> + let chosen_lid, flag = self#lid_of n in + if Options.debug "data-types-traversal" then + KPrint.bprintf "visiting %a: Not_found --> %a\n" ptyp (fold_tapp n) plid chosen_lid; + let flag = if fst3 best_hint = n then thd3 best_hint @ flag else flag in + if lid = tuple_lid then begin + assert (args <> []); + Hashtbl.add state n (Gray, chosen_lid); + (* For tuples, we immediately know how to generate a definition. *) + let fields = List.mapi (fun i arg -> Some (self#field_at i), (arg, false)) args in + self#record (DType (chosen_lid, [ Common.Private ] @ flag, 0, 0, Flat fields)); + Hashtbl.replace state n (Black, chosen_lid) + end else begin + (* This specific node has not been visited yet. *) + Hashtbl.add state n (Gray, chosen_lid); + + let subst fields = List.map (fun (field, (t, m)) -> + field, (DeBruijn.subst_tn args (DeBruijn.subst_ctn' cgs t), m) + ) fields in + assert (not (Hashtbl.mem map lid) || not (has_variables args) && not (has_cg_variables cgs)); + begin match Hashtbl.find map lid with + | exception Not_found -> + (* Unknown, external non-polymorphic lid, e.g. Prims.int *) + Hashtbl.replace state n (Black, chosen_lid) + | flags, ((Variant _ | Flat _ | Union _) as def) when under_ref && not (Hashtbl.mem seen_declarations lid) -> + (* FORWARD DECLARATION: this is unrelated to monomorphization (but we do it + here anyway). An occurrence of `t*` appears before the definition of `t`; we + pick a name, insert a forward declaration for `t`, then remember that *once we + have see the definition of `t`, we will insert the monomorphized `t___ts` at that + specific location. + + The comment below furthermore tries to explain why we do things this way (as + opposed to inserting the monomorphized `t___ts` immediately). + + Because this looks up a definition in the global map, the + definitions are reordered according to the traversal order, which + is generally a good idea (we accept more programs!), EXCEPT + when the user relies on mutual recursion behind a reference + (pointer) type. In that case, following the type dependency graph is + generally not a good idea, since we may go from a valid + ordering to an invalid one (see tests/MutualStruct.fst). So, + the intent here (i.e., when under a ref type) is that: + - tuple types ALWAYS get monomorphized on-demand (see + above) + - abbreviations are fine and won't cause further issues + - data types, however, need to have their names allocated and a + forward reference inserted (TODO: at most once), then the + specific choice of type arguments need to be recorded as + something we want to visit later (once we're done with this + particular traversal)... *) + if Options.debug "data-types-traversal" then + KPrint.bprintf "DEFERRING %a\n" ptyp (fold_tapp n); + if match def with Union _ -> true | _ -> false then + self#record (DType (chosen_lid, flags, 0, 0, Forward FUnion)) + else + self#record (DType (chosen_lid, flags, 0, 0, Forward FStruct)); + Hashtbl.add pending_monomorphizations lid (args, cgs); + (* FORWARD DECLARATIONS: remove us from the state to make sure future occurences of the + same situation send us through this codepath again *) + Hashtbl.remove state n + | 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)); + 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)); + 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)); + 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 - f, t - ) fields in - 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 - 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) - end - end; - chosen_lid - | Gray, chosen_lid -> - (* FORWARD DECLARATION: simple case of a recursive type that needs a forward declaration *) - if Options.debug "data-types-traversal" then - KPrint.bprintf "visiting %a: Gray\n" ptyp (fold_tapp n); - begin match Hashtbl.find map lid with - | exception Not_found -> - () - | flags, Union _ -> - self#record (DType (chosen_lid, flags, 0, 0, Forward FUnion)) - | flags, _ -> - self#record (DType (chosen_lid, flags, 0, 0, Forward FStruct)) - end; - chosen_lid - | Black, chosen_lid -> - if Options.debug "data-types-traversal" then - KPrint.bprintf "visiting %a: Black\n" ptyp (fold_tapp n); - chosen_lid + if args <> [] || cgs <> [] then + 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) + end + end; + chosen_lid + | Gray, chosen_lid -> + (* FORWARD DECLARATION: simple case of a recursive type that needs a + forward declaration. + + We still insert something to deal with cases like + + typedef struct s { + void f(t x); + } t; + *) + if Options.debug "data-types-traversal" then + KPrint.bprintf "visiting %a: Gray\n" ptyp (fold_tapp n); + begin match Hashtbl.find map lid with + | exception Not_found -> + () + | flags, Union _ -> + self#record (DType (chosen_lid, flags, 0, 0, Forward FUnion)) + | flags, _ -> + self#record (DType (chosen_lid, flags, 0, 0, Forward FStruct)) + end; + chosen_lid + | Black, chosen_lid -> + if Options.debug "data-types-traversal" then + KPrint.bprintf "visiting %a: Black\n" ptyp (fold_tapp n); + chosen_lid (* Top-level, non-parameterized declarations are root of our graph traversal. * This also visits, via occurrences in code, applications of parameterized @@ -514,18 +545,13 @@ let monomorphize_data_types map = object(self) | DType (lid, _, n_cgs, n, (Flat _ | Variant _ | Abbrev _ | Union _)) -> assert (n = 0 && n_cgs = 0); - (* Regular traversal logic, as below. *) - ignore (self#visit_decl false d); - (* FORWARD DECLARATIONS: we force a visit of this (non-polymorphic) type definition, for - the sole side-effect of remembering that we have seen it, and that further occurrences - of it need not generate a forward declaration (i.e. mark it Black, because - under_ref=false). - - Note that `visit_node` will insert our own definition in the pending list, flushed by - `clear` -- ignore and don't insert twice. *) - ignore (self#visit_node false (lid, [], [])); + (* 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); Hashtbl.add seen_declarations lid (); - self#clear () + self#clear () @ [ d ] | _ -> (* Not a type, e.g. a global; needs to be retained. *) diff --git a/test/Makefile b/test/Makefile index 208b6615..783768da 100644 --- a/test/Makefile +++ b/test/Makefile @@ -85,7 +85,7 @@ FSTAR = $(FSTAR_EXE) \ --trivial_pre_for_unannotated_effectful_fns false \ --cmi --warn_error -274 -all: $(FILES) rust $(WASM_FILES) $(CUSTOM) ctypes-test sepcomp-test rust-val-test bundle-test +all: $(FILES) rust $(WASM_FILES) $(CUSTOM) ctypes-test sepcomp-test rust-val-test bundle-test rust-propererasure-bundle-test # Needs node wasm: $(WASM_FILES) @@ -299,6 +299,10 @@ rust-val-test: +$(MAKE) -C rust-val .PHONY: rust-val-test +rust-propererasure-bundle-test: + +$(MAKE) -C rust-propererasure-bundle +.PHONY: rust-propererasure-bundle-test + CTYPES_HAND_WRITTEN_FILES=Client.ml Makefile .PHONY: $(LOWLEVEL_DIR)/Client.native diff --git a/test/MutualStruct.fst b/test/MutualStruct.fst index 5d0d9ffc..24737460 100644 --- a/test/MutualStruct.fst +++ b/test/MutualStruct.fst @@ -87,7 +87,7 @@ and object6_pair = { } *) -// This test extracts. It should compile, but the C compiler complains with object7_pair incomplete because KaRaMeL extracted it too early +// This test extracts and compiles. noeq type object7_tagged = { @@ -110,3 +110,58 @@ and object7_pair = { object7_pair_fst: object7; object7_pair_snd: object7; } + +// This test extracts and compiles. + +noeq +type slice (a: Type0) : Type0 = { elt: ref a; len: U64.t; } + +[@@no_auto_projectors] +noeq +type object8_map = { + object8_map_length_size: U8.t; + object8_map_ptr: slice object8_map_entry; +} + +and object8_array = { + object8_array_length_size: U8.t; + object8_array_ptr: slice object8_raw; +} + +and object8_raw = +| OBJECT8_Case_Simple: v: U8.t -> object8_raw +| OBJECT8_Case_Array: v: object8_array -> object8_raw +| OBJECT8_Case_Map: v: object8_map -> object8_raw + +and object8_map_entry = { + object8_map_entry_key: object8_raw; + object8_map_entry_value: object8_raw; +} + +let f8 (x: object8_map) : Tot bool = true + +// This test extracts, but has failed to compile since #664 + +[@@no_auto_projectors] +noeq +type object9_array = { + object9_array_length_size: U8.t; + object9_array_ptr: slice object9_raw; +} + +and object9_map = { + object9_map_length_size: U8.t; + object9_map_ptr: slice object9_map_entry; +} + +and object9_raw = +| OBJECT9_Case_Simple: v: U8.t -> object9_raw +| OBJECT9_Case_Array: v: object9_array -> object9_raw +| OBJECT9_Case_Map: v: object9_map -> object9_raw + +and object9_map_entry = { + object9_map_entry_key: object9_raw; + object9_map_entry_value: object9_raw; +} + +let f9 (x: object9_map) : Tot bool = true diff --git a/test/Rustpropererasure.fst b/test/Rustpropererasure.fst new file mode 100644 index 00000000..132d2ec9 --- /dev/null +++ b/test/Rustpropererasure.fst @@ -0,0 +1,22 @@ +module Rustpropererasure +open FStar.HyperStack.ST + +module G = FStar.Ghost +module U32 = FStar.UInt32 + +noeq type slice (t: Type0) : Type0 = { len: U32.t ; ptr: ref t } + +inline_for_extraction +noeq +type cbor_string = { + cbor_string_type: U32.t; + cbor_string_size: U32.t; + cbor_string_ptr: slice U32.t; + cbor_string_perm: Ghost.erased bool; +} + +let cbor_string_reset_perm (p: Ghost.erased bool) (c: cbor_string) : cbor_string = { + c with cbor_string_perm = p && c.cbor_string_perm +} + +let main_ () = 0ul diff --git a/test/rust-propererasure-bundle/.gitignore b/test/rust-propererasure-bundle/.gitignore new file mode 100644 index 00000000..e6c287e3 --- /dev/null +++ b/test/rust-propererasure-bundle/.gitignore @@ -0,0 +1,2 @@ +*.krml +*.rs diff --git a/test/rust-propererasure-bundle/Base.fst b/test/rust-propererasure-bundle/Base.fst new file mode 100644 index 00000000..0c9d8cf3 --- /dev/null +++ b/test/rust-propererasure-bundle/Base.fst @@ -0,0 +1,17 @@ +module Base +open FStar.HyperStack.ST + +module G = FStar.Ghost +module U32 = FStar.UInt32 +module C = C + +noeq type slice (t: Type0) : Type0 = { len: U32.t ; ptr: ref t } + +inline_for_extraction +noeq +type cbor_string = { + cbor_string_type: U32.t; + cbor_string_size: U32.t; + cbor_string_ptr: slice U32.t; + cbor_string_perm: Ghost.erased bool; +} diff --git a/test/rust-propererasure-bundle/Caller.fst b/test/rust-propererasure-bundle/Caller.fst new file mode 100644 index 00000000..b9c0d119 --- /dev/null +++ b/test/rust-propererasure-bundle/Caller.fst @@ -0,0 +1,9 @@ +module Caller +open FStar.HyperStack.ST + +module U32 = FStar.UInt32 + +let h (c: Base.cbor_string) : U32.t = + Derived.g c + +let main_ () : St Int32.t = 0l diff --git a/test/rust-propererasure-bundle/Derived.fst b/test/rust-propererasure-bundle/Derived.fst new file mode 100644 index 00000000..eabe1352 --- /dev/null +++ b/test/rust-propererasure-bundle/Derived.fst @@ -0,0 +1,7 @@ +module Derived +open FStar.HyperStack.ST + +module U32 = FStar.UInt32 + +let g (c: Base.cbor_string) : U32.t = + c.Base.cbor_string_type diff --git a/test/rust-propererasure-bundle/Makefile b/test/rust-propererasure-bundle/Makefile new file mode 100644 index 00000000..f6c7f7d9 --- /dev/null +++ b/test/rust-propererasure-bundle/Makefile @@ -0,0 +1,70 @@ +include ../../Makefile.common + +ifeq (3.81,$(MAKE_VERSION)) + $(error You seem to be using the OSX antiquated Make version. Hint: brew \ + install make, then invoke gmake instead of make) +endif + +FSTAR_EXE ?= fstar.exe + +TEST_OPTS = -warn-error @4 -verbose -skip-makefiles +KRML_BIN = ../../_build/default/src/Karamel.exe +KRML = $(KRML_BIN) -fstar $(FSTAR_EXE) $(KOPTS) $(TEST_OPTS) +CACHE_DIR = .cache +FSTAR = $(FSTAR_EXE) --cache_checked_modules \ + --cache_dir $(CACHE_DIR) \ + --include ../../krmllib/compat --include ../../krmllib/obj \ + --include ../../krmllib --include ../../runtime \ + --ext optimize_let_vc \ + --already_cached 'Prims FStar C TestLib Spec.Loops -C.Compat -C.Nullity LowStar WasmSupport' \ + --trivial_pre_for_unannotated_effectful_fns false \ + --cmi --warn_error -274 +SED=$(shell which gsed >/dev/null 2>&1 && echo gsed || echo sed) + +all: derived.rust-test + +FSTAR_FILES=$(wildcard *.fst *.fsti) + +.PRECIOUS: %.krml + +# Use F*'s dependency mechanism and fill out the missing rules. + +ifndef MAKE_RESTARTS +ifndef NODEPEND +.depend: .FORCE + $(FSTAR) --dep full $(FSTAR_FILES) --extract 'krml:*,-Prims' --output_deps_to $@ + +.PHONY: .FORCE +.FORCE: +endif +endif + +include .depend + +$(CACHE_DIR)/%.checked: | .depend + $(call run-with-log,$(FSTAR) $(OTHERFLAGS) $< && touch $@,[RUST_PROPERERASURE_BUNDLE_VERIFY] $*,$(CACHE_DIR)/$*) + +%.krml: | .depend + $(call run-with-log,$(FSTAR) $(OTHERFLAGS) --codegen krml \ + --extract_module $(basename $(notdir $(subst .checked,,$<))) \ + $(notdir $(subst .checked,,$<))\ + ,[RUST_PROPERERASURE_BUNDLE_EXTRACT_KRML] $(basename $*),$*) + +######## +# Rust # +######## + +.PRECIOUS: %.rs +derived.rs: $(ALL_KRML_FILES) $(KRML_BIN) + $(KRML) -minimal -bundle 'FStar.*,LowStar.*,C,C.*,Prims' -bundle 'Base+Caller=Derived[rename=Derived]' \ + -backend rust $(EXTRA) -tmpdir $(dir $@) $(filter %.krml,$^) + $(SED) -i 's/\(patterns..\)/\1\nmod lowstar { pub mod ignore { pub fn ignore(_x: T) {}}}\n/' $@ + echo 'fn main () { let r = main_ (); if r != 0 { println!("main_ returned: {}\\n", r); panic!() } }' >> $@ + +%.rust-test: %.rs + rustc $< -o $*.exe && ./$*.exe + +clean: + rm -rf .cache .depend *.krml *.rs *.exe *.output *.err *.cmd *.time + +.PHONY: all clean