From 7e5a7dafcf17990f41b6570f06294ee8769ed797 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Tue, 4 Feb 2025 10:55:52 +0100 Subject: [PATCH 01/13] Add an Assumed decl node to MiniRust for external definitions --- lib/MiniRust.ml | 11 ++++++++++- lib/OptimizeMiniRust.ml | 1 + lib/PrintMiniRust.ml | 3 +++ 3 files changed, 14 insertions(+), 1 deletion(-) diff --git a/lib/MiniRust.ml b/lib/MiniRust.ml index 126936e7..1b8d6c0f 100644 --- a/lib/MiniRust.ml +++ b/lib/MiniRust.ml @@ -196,6 +196,14 @@ type decl = generic_params: generic_param list; meta: meta; } + (* We need to keep assumed/external functions to perform mutability inference + at the MiniRust level. However, these nodes will not be printed at code + generation *) + | Assumed of { + name: name; + parameters: typ list; + return_type: typ; + } and item = (* Not supporting tuples yet *) @@ -383,7 +391,8 @@ let name_of_decl (d: decl) = | Enumeration { name; _ } | Struct { name; _ } | Function { name; _ } - | Constant { name; _ } -> + | Constant { name; _ } + | Assumed {name; _ } -> name let zero_usize: expr = Constant (Constant.SizeT, "0") diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml index df45f34d..64b3a030 100644 --- a/lib/OptimizeMiniRust.ml +++ b/lib/OptimizeMiniRust.ml @@ -1248,6 +1248,7 @@ let compute_derives files = match decl with | Function _ -> failwith "impossible" | Constant _ -> failwith "impossible" + | Assumed _ -> failwith "impossible" | Alias _ -> TraitSet.empty | Struct { fields; _ } -> let ts = List.map (fun (sf: struct_field) -> traits sf.typ) fields in diff --git a/lib/PrintMiniRust.ml b/lib/PrintMiniRust.ml index fb134864..9a4c5345 100644 --- a/lib/PrintMiniRust.ml +++ b/lib/PrintMiniRust.ml @@ -605,6 +605,9 @@ let rec print_decl env (d: decl) = group @@ group (print_meta meta ^^ string "type" ^/^ string target_name ^^ print_generic_params generic_params ^/^ equals) ^/^ group (print_typ env body ^^ semi) + (* Assumed declarations correspond to externals, which were propagated for mutability inference purposes. + We do not emit them *) + | Assumed _ -> empty and print_derives traits = group @@ From 664b72deabed439e54e24a7d4bce0b4247638429 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Tue, 4 Feb 2025 11:24:46 +0100 Subject: [PATCH 02/13] Support assumed functions in Rust mutability inference --- lib/AstToMiniRust.ml | 9 +++++++-- lib/OptimizeMiniRust.ml | 5 +++++ 2 files changed, 12 insertions(+), 2 deletions(-) diff --git a/lib/AstToMiniRust.ml b/lib/AstToMiniRust.ml index 4edfed00..0a9ab653 100644 --- a/lib/AstToMiniRust.ml +++ b/lib/AstToMiniRust.ml @@ -1400,8 +1400,13 @@ let translate_decl env (d: Ast.decl): MiniRust.decl option = let meta = translate_meta flags in Some (MiniRust.Constant { name; typ; body; meta }) - | DExternal _ -> - None + | DExternal (_, _, _, _, lid, _, _) -> + let name, parameters, return_type = + match lookup_decl env lid with + | name, Function (_, parameters, return_type) -> name, parameters, return_type + | _ -> failwith " impossible" + in + Some (MiniRust.Assumed { name; parameters; return_type }) | DType (lid, flags, _, _, decl) -> let name = lookup_type env lid in diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml index 64b3a030..09ba2807 100644 --- a/lib/OptimizeMiniRust.ml +++ b/lib/OptimizeMiniRust.ml @@ -669,6 +669,8 @@ let infer_function (env: env) valuation (d: decl): decl = the traversal does not add or remove any bindings, but only increases the mutability, we can do a direct replacement instead of a more complex merge *) Function { f with body; parameters } + (* Assumed functions already have their mutability specified, we skip them *) + | Assumed _ -> d | _ -> assert false @@ -1021,6 +1023,8 @@ let infer_mut_borrows files = List.filter_map (function | Function { parameters; name; _ } -> Some (name, List.map (fun (p: MiniRust.binding) -> p.typ) parameters) + | Assumed { name; parameters; _ } -> + Some (name, parameters) | _ -> None ) decls) files)) @@ -1044,6 +1048,7 @@ let infer_mut_borrows files = else match infer_function env valuation (NameMap.find name definitions) with | Function { parameters; _ } -> distill (List.map (fun (b: MiniRust.binding) -> b.typ) parameters) + | Assumed { parameters; _ } -> distill parameters | _ -> failwith "impossible" in From cb85f58efc682fe8ec85da228935793f7d5f95c4 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Tue, 4 Feb 2025 13:29:42 +0100 Subject: [PATCH 03/13] Preserve mutablity information when translating external definitions --- lib/AstToMiniRust.ml | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) diff --git a/lib/AstToMiniRust.ml b/lib/AstToMiniRust.ml index 0a9ab653..66a4c4ef 100644 --- a/lib/AstToMiniRust.ml +++ b/lib/AstToMiniRust.ml @@ -416,17 +416,24 @@ let translate_unknown_lid (m, n) = let m = compress_prefix m in List.map String.lowercase_ascii m @ [ n ] -let borrow_kind_of_bool _b: MiniRust.borrow_kind = - Shared +let borrow_kind_of_bool b: MiniRust.borrow_kind = + if b then Shared (* Constant pointer case *) + else Mut type config = { box: bool; lifetime: MiniRust.lifetime option; + (* Rely on the Ast type to set borrow mutability. + Should always be set to false to correctly infer + mutability in a later pass, except when translating + external (assumed) declarations *) + keep_mut: bool; } let default_config = { box = false; lifetime = None; + keep_mut = false; } let rec translate_type_with_config (env: env) (config: config) (t: Ast.typ): MiniRust.typ = @@ -440,7 +447,7 @@ let rec translate_type_with_config (env: env) (config: config) (t: Ast.typ): Min MiniRust.box (Slice (translate_type_with_config env config t)) (* Vec (translate_type_with_config env config t) *) else - Ref (config.lifetime, borrow_kind_of_bool b, Slice (translate_type_with_config env config t)) + Ref (config.lifetime, (if config.keep_mut then borrow_kind_of_bool b else Shared), Slice (translate_type_with_config env config t)) | TArray (t, c) -> Array (translate_type_with_config env config t, int_of_string (snd c)) | TQualified lid -> let generic_params = @@ -1272,7 +1279,7 @@ let bind_decl env (d: Ast.decl): env = | DExternal (_, _, _, type_parameters, lid, t, _param_names) -> let name = translate_unknown_lid lid in - push_decl env lid (name, make_poly (translate_type env t) type_parameters) + push_decl env lid (name, make_poly (translate_type_with_config env {default_config with keep_mut = true} t) type_parameters) | DType (lid, _flags, _, _, decl) -> let env, name = @@ -1299,7 +1306,7 @@ let bind_decl env (d: Ast.decl): env = in let fields = List.map (fun (f, (t, _m)) -> let f = Option.get f in - { MiniRust.name = f; visibility = Some Pub; typ = translate_type_with_config env { box; lifetime } t } + { MiniRust.name = f; visibility = Some Pub; typ = translate_type_with_config env { box; lifetime; keep_mut = false } t } ) fields in { env with struct_fields = DataTypeMap.add (`Struct lid) fields env.struct_fields } @@ -1316,7 +1323,7 @@ let bind_decl env (d: Ast.decl): env = List.fold_left (fun env (cons, fields) -> let cons_lid = `Variant (lid, cons) in let fields = List.map (fun (f, (t, _)) -> - { MiniRust.name = f; visibility = Some Pub; typ = translate_type_with_config env { box; lifetime } t } + { MiniRust.name = f; visibility = Some Pub; typ = translate_type_with_config env { box; lifetime; keep_mut = false } t } ) fields in { env with From b7deff6ae83be3cb0056793510dce8871f758e60 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Tue, 4 Feb 2025 13:42:54 +0100 Subject: [PATCH 04/13] Erase borrow kinds during Ast to MiniRust translation when matching types --- lib/AstToMiniRust.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/lib/AstToMiniRust.ml b/lib/AstToMiniRust.ml index 66a4c4ef..015aaacb 100644 --- a/lib/AstToMiniRust.ml +++ b/lib/AstToMiniRust.ml @@ -594,9 +594,9 @@ and translate_array (env: env) is_toplevel (init: Ast.expr): env * MiniRust.expr and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env * MiniRust.expr = (* KPrint.bprintf "translate_expr_with_type: %a @@ %a\n" PrintMiniRust.ptyp t_ret PrintAst.Ops.pexpr e; *) - let erase_lifetime_info = (object(self) + let erase_lifetime_and_borrow_kind_info = (object(self) inherit [_] MiniRust.DeBruijn.map - method! visit_Ref env _ bk t = Ref (None, bk, self#visit_typ env t) + method! visit_Ref env _ _ t = Ref (None, Shared, self#visit_typ env t) method! visit_tname _ n _ = Name (n, []) end)#visit_typ () in @@ -662,8 +662,11 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env (* If we reach this case, we perform one last try by erasing the lifetime information in both terms. This is useful to handle, e.g., implicit lifetime annotations or annotations up to alpha-conversion. - Note, this is sound as lifetime mismatches will be caught by the Rust compiler *) - if erase_lifetime_info t = erase_lifetime_info t_ret then + Note, this is sound as lifetime mismatches will be caught by the Rust compiler. + We similarly erase borrow kind information, which should only mismatch when relying + on external, assumed declarations: these will be handled during mutability inference, + and also rechecked by the Rust compiler. *) + if erase_lifetime_and_borrow_kind_info t = erase_lifetime_and_borrow_kind_info t_ret then x else Warn.failwith "type mismatch;\n e=%a\n t=%a (verbose: %s)\n t_ret=%a\n x=%a" From f24deef87ba1e90ae1712b079cff6db1af61824a Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Thu, 14 Nov 2024 13:29:03 -0800 Subject: [PATCH 05/13] Minor --- lib/AstToMiniRust.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/lib/AstToMiniRust.ml b/lib/AstToMiniRust.ml index 015aaacb..1fe40d3c 100644 --- a/lib/AstToMiniRust.ml +++ b/lib/AstToMiniRust.ml @@ -609,7 +609,7 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env (* PrintMiniRust.ptyp t *) (* PrintMiniRust.ptyp t_ret; *) begin match x, t, t_ret with - | _, (MiniRust.Vec _ | Array _), Ref (_, k, Slice _) -> + | _, (App (Name (["Box"], _), [Slice _]) | MiniRust.Vec _ | Array _), Ref (_, k, Slice _) -> Borrow (k, x) | Constant (w, x), Constant UInt32, Constant SizeT -> assert (w = Constant.UInt32); @@ -622,8 +622,6 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env x (* More conversions due to box-ing types. *) - | _, App (Name (["Box"], _), [Slice _]), Ref (_, k, Slice _) -> - Borrow (k, x) | _, Ref (_, _, Slice _), App (Name (["Box"], _), [Slice _]) -> (* COPY *) MethodCall (Borrow (Shared, Deref x), ["into"], []) From 87fe9784f93684540b0d2cc7e5691d72836159b9 Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Wed, 5 Feb 2025 14:04:24 -0800 Subject: [PATCH 06/13] debug --- lib/OptimizeMiniRust.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml index 09ba2807..dadeac19 100644 --- a/lib/OptimizeMiniRust.ml +++ b/lib/OptimizeMiniRust.ml @@ -101,7 +101,8 @@ let distill ts = (* Get the type of the arguments of `name`, based on the current state of `valuation` *) let lookup env valuation name = - (* KPrint.bprintf "lookup: %a\n" PrintMiniRust.pname name; *) + if not (NameMap.mem name env.signatures) then + KPrint.bprintf "ERROR looking up: %a\n" PrintMiniRust.pname name; let ts = NameMap.find name env.signatures in adjust ts (valuation name) From 58a6570499b959777d2d4cf38a870f696ff31706 Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Wed, 5 Feb 2025 14:05:45 -0800 Subject: [PATCH 07/13] nitpick --- lib/AstToMiniRust.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/AstToMiniRust.ml b/lib/AstToMiniRust.ml index 1fe40d3c..2eb817ea 100644 --- a/lib/AstToMiniRust.ml +++ b/lib/AstToMiniRust.ml @@ -609,7 +609,7 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env (* PrintMiniRust.ptyp t *) (* PrintMiniRust.ptyp t_ret; *) begin match x, t, t_ret with - | _, (App (Name (["Box"], _), [Slice _]) | MiniRust.Vec _ | Array _), Ref (_, k, Slice _) -> + | _, (MiniRust.App (Name (["Box"], _), [Slice _]) | MiniRust.Vec _ | Array _), Ref (_, k, Slice _) -> Borrow (k, x) | Constant (w, x), Constant UInt32, Constant SizeT -> assert (w = Constant.UInt32); From 387741bd5c805c222f604417f642cad0dea12ff0 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Mon, 10 Feb 2025 18:18:56 +0100 Subject: [PATCH 08/13] Possibly convert erases borrow kinds to make handling of internals more robust --- lib/AstToMiniRust.ml | 26 ++++++++++++++++---------- lib/OptimizeMiniRust.ml | 3 ++- 2 files changed, 18 insertions(+), 11 deletions(-) diff --git a/lib/AstToMiniRust.ml b/lib/AstToMiniRust.ml index 2eb817ea..38db3812 100644 --- a/lib/AstToMiniRust.ml +++ b/lib/AstToMiniRust.ml @@ -594,9 +594,15 @@ and translate_array (env: env) is_toplevel (init: Ast.expr): env * MiniRust.expr and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env * MiniRust.expr = (* KPrint.bprintf "translate_expr_with_type: %a @@ %a\n" PrintMiniRust.ptyp t_ret PrintAst.Ops.pexpr e; *) - let erase_lifetime_and_borrow_kind_info = (object(self) + let erase_borrow_kind_info = (object(self) inherit [_] MiniRust.DeBruijn.map - method! visit_Ref env _ _ t = Ref (None, Shared, self#visit_typ env t) + method! visit_Ref env a _ t = Ref (a, Shared, self#visit_typ env t) + end)#visit_typ () + in + + let erase_lifetime_info = (object(self) + inherit [_] MiniRust.DeBruijn.map + method! visit_Ref env _ bk t = Ref (None, bk, self#visit_typ env t) method! visit_tname _ n _ = Name (n, []) end)#visit_typ () in @@ -608,7 +614,10 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env (* PrintMiniRust.pexpr x *) (* PrintMiniRust.ptyp t *) (* PrintMiniRust.ptyp t_ret; *) - begin match x, t, t_ret with + (* Mutable borrows were only included for external definitions. + We erase them here; they will be handled during mutability inference, which will + be rechecked by the Rust compiler *) + begin match x, erase_borrow_kind_info t, erase_borrow_kind_info t_ret with | _, (MiniRust.App (Name (["Box"], _), [Slice _]) | MiniRust.Vec _ | Array _), Ref (_, k, Slice _) -> Borrow (k, x) | Constant (w, x), Constant UInt32, Constant SizeT -> @@ -660,17 +669,14 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env (* If we reach this case, we perform one last try by erasing the lifetime information in both terms. This is useful to handle, e.g., implicit lifetime annotations or annotations up to alpha-conversion. - Note, this is sound as lifetime mismatches will be caught by the Rust compiler. - We similarly erase borrow kind information, which should only mismatch when relying - on external, assumed declarations: these will be handled during mutability inference, - and also rechecked by the Rust compiler. *) - if erase_lifetime_and_borrow_kind_info t = erase_lifetime_and_borrow_kind_info t_ret then + Note, this is sound as lifetime mismatches will be caught by the Rust compiler. *) + if erase_lifetime_info t = erase_lifetime_info t_ret then x else - Warn.failwith "type mismatch;\n e=%a\n t=%a (verbose: %s)\n t_ret=%a\n x=%a" + Warn.failwith "type mismatch;\n e=%a\n t=%a (verbose: %s)\n t_ret=%a (verbose: %s)\n x=%a" PrintAst.Ops.pexpr e PrintMiniRust.ptyp t (MiniRust.show_typ t) - PrintMiniRust.ptyp t_ret + PrintMiniRust.ptyp t_ret (MiniRust.show_typ t_ret) PrintMiniRust.pexpr x; end in diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml index dadeac19..af998417 100644 --- a/lib/OptimizeMiniRust.ml +++ b/lib/OptimizeMiniRust.ml @@ -1025,7 +1025,8 @@ let infer_mut_borrows files = | Function { parameters; name; _ } -> Some (name, List.map (fun (p: MiniRust.binding) -> p.typ) parameters) | Assumed { name; parameters; _ } -> - Some (name, parameters) + if List.exists (fun (n, _) -> n = name) builtins then None + else Some (name, parameters) | _ -> None ) decls) files)) From 58a7ffb985b5350bc8c37722cec520b6ed7ea6f6 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Tue, 11 Feb 2025 11:32:53 +0100 Subject: [PATCH 09/13] Filter assumed definitions in MiniRust --- lib/OptimizeMiniRust.ml | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml index af998417..13536fe9 100644 --- a/lib/OptimizeMiniRust.ml +++ b/lib/OptimizeMiniRust.ml @@ -1297,4 +1297,12 @@ let simplify_minirust files = have introduced unit statements *) let files = map_funs remove_trailing_unit#visit_expr files in let files = add_derives (compute_derives files) files in + + (* Remove Assumed definitions, and filter empty files to avoid spurious code generation *) + let files = List.filter_map (fun (x, l) -> + (* Filter out assumed declarations *) + match List.filter (function | Assumed _ -> false | _ -> true) l with + | [] -> None (* No declaration left, we do not keep this file *) + | l -> Some (x, l) + ) files in files From 409c23c0776f3e988cd5200aebd957b2b73fd727 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Tue, 11 Feb 2025 11:33:49 +0100 Subject: [PATCH 10/13] Catch leftover assumed declarations at codegen time --- lib/PrintMiniRust.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lib/PrintMiniRust.ml b/lib/PrintMiniRust.ml index 9a4c5345..11092ba2 100644 --- a/lib/PrintMiniRust.ml +++ b/lib/PrintMiniRust.ml @@ -606,8 +606,8 @@ let rec print_decl env (d: decl) = group (print_meta meta ^^ string "type" ^/^ string target_name ^^ print_generic_params generic_params ^/^ equals) ^/^ group (print_typ env body ^^ semi) (* Assumed declarations correspond to externals, which were propagated for mutability inference purposes. - We do not emit them *) - | Assumed _ -> empty + They should have been filtered out during the MiniRust cleanup *) + | Assumed _ -> failwith "Assumed declaration remaining" and print_derives traits = group @@ From 36b63c99930dbc4f01f3d6c1f08f458f405cbe91 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Mon, 17 Feb 2025 16:45:13 +0100 Subject: [PATCH 11/13] More helpers for basic int types --- lib/Helpers.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/lib/Helpers.ml b/lib/Helpers.ml index 5647d8f6..85abe8b2 100644 --- a/lib/Helpers.ml +++ b/lib/Helpers.ml @@ -28,7 +28,9 @@ end (* Creating AST nodes *********************************************************) let uint8 = TInt K.UInt8 +let uint16 = TInt K.UInt16 let uint32 = TInt K.UInt32 +let uint64 = TInt K.UInt64 let usize = TInt K.SizeT let type_of_op op w = @@ -346,7 +348,7 @@ class ['self] readonly_visitor = object (self: 'self) | EPolyComp _ | EOp _ -> List.for_all (self#visit_expr_w ()) es - | EQualified _ + | EQualified _ when is_readonly_builtin_lid e -> List.for_all (self#visit_expr_w ()) es | ETApp ({ node = EQualified _; _ } as e, _, _, _) From 7c3485b351b843f112e8d514d2829a4ad3dfbe6b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 17 Feb 2025 11:37:52 -0800 Subject: [PATCH 12/13] Run `$FSTAR/.scripts/remove_all_unused_opens.sh krmllib/` --- krmllib/C.String.fst | 3 --- krmllib/C.String.fsti | 1 - krmllib/C.fst | 1 - krmllib/LowStar.Lib.AssocList.fst | 2 -- krmllib/LowStar.Lib.AssocList.fsti | 5 ----- krmllib/LowStar.Lib.LinkedList2.fst | 2 -- krmllib/TestLib.fsti | 1 - krmllib/compat/C.Compat.String.fst | 1 - krmllib/compat/C.Compat.fst | 1 - krmllib/compat/C.Nullity.fsti | 3 --- 10 files changed, 20 deletions(-) diff --git a/krmllib/C.String.fst b/krmllib/C.String.fst index 175f4700..95ef8273 100644 --- a/krmllib/C.String.fst +++ b/krmllib/C.String.fst @@ -1,10 +1,7 @@ module C.String -module U8 = FStar.UInt8 module U32 = FStar.UInt32 -module B = LowStar.Buffer -module M = LowStar.Modifies open FStar.HyperStack.ST diff --git a/krmllib/C.String.fsti b/krmllib/C.String.fsti index 4110693a..1994f50a 100644 --- a/krmllib/C.String.fsti +++ b/krmllib/C.String.fsti @@ -1,6 +1,5 @@ module C.String -module U8 = FStar.UInt8 module U32 = FStar.UInt32 module B = LowStar.Buffer diff --git a/krmllib/C.fst b/krmllib/C.fst index 38840dca..3775a745 100644 --- a/krmllib/C.fst +++ b/krmllib/C.fst @@ -2,7 +2,6 @@ module C open FStar.HyperStack.ST -module HS = FStar.HyperStack module U8 = FStar.UInt8 // This module contains a series of bindings that already exist in C. It receives diff --git a/krmllib/LowStar.Lib.AssocList.fst b/krmllib/LowStar.Lib.AssocList.fst index 30c5f747..14feb70e 100644 --- a/krmllib/LowStar.Lib.AssocList.fst +++ b/krmllib/LowStar.Lib.AssocList.fst @@ -5,8 +5,6 @@ module LowStar.Lib.AssocList module B = LowStar.Buffer module HS = FStar.HyperStack module G = FStar.Ghost -module L = FStar.List.Tot -module U32 = FStar.UInt32 module ST = FStar.HyperStack.ST module M = FStar.Map diff --git a/krmllib/LowStar.Lib.AssocList.fsti b/krmllib/LowStar.Lib.AssocList.fsti index 258ca980..a1d007f8 100644 --- a/krmllib/LowStar.Lib.AssocList.fsti +++ b/krmllib/LowStar.Lib.AssocList.fsti @@ -4,14 +4,9 @@ module LowStar.Lib.AssocList module B = LowStar.Buffer module HS = FStar.HyperStack -module G = FStar.Ghost -module L = FStar.List.Tot -module U32 = FStar.UInt32 module ST = FStar.HyperStack.ST module M = FStar.Map -module LL2 = LowStar.Lib.LinkedList2 -module LL1 = LowStar.Lib.LinkedList open FStar.HyperStack.ST open LowStar.BufferOps diff --git a/krmllib/LowStar.Lib.LinkedList2.fst b/krmllib/LowStar.Lib.LinkedList2.fst index 550680f9..ccd50bd5 100644 --- a/krmllib/LowStar.Lib.LinkedList2.fst +++ b/krmllib/LowStar.Lib.LinkedList2.fst @@ -14,8 +14,6 @@ open LowStar.BufferOps module B = LowStar.Buffer module HS = FStar.HyperStack module G = FStar.Ghost -module L = FStar.List.Tot -module U32 = FStar.UInt32 module ST = FStar.HyperStack.ST module LL1 = LowStar.Lib.LinkedList diff --git a/krmllib/TestLib.fsti b/krmllib/TestLib.fsti index 7c8e23ab..0c365b11 100644 --- a/krmllib/TestLib.fsti +++ b/krmllib/TestLib.fsti @@ -3,7 +3,6 @@ module TestLib open FStar.HyperStack.ST open LowStar.Buffer -module HS = FStar.HyperStack module Buffer = LowStar.Buffer (** Some test routines *) diff --git a/krmllib/compat/C.Compat.String.fst b/krmllib/compat/C.Compat.String.fst index 8594ac42..c065faa5 100644 --- a/krmllib/compat/C.Compat.String.fst +++ b/krmllib/compat/C.Compat.String.fst @@ -1,6 +1,5 @@ module C.Compat.String -module U8 = FStar.UInt8 module U32 = FStar.UInt32 module B = LowStar.Buffer diff --git a/krmllib/compat/C.Compat.fst b/krmllib/compat/C.Compat.fst index b7431f70..3b965c2a 100644 --- a/krmllib/compat/C.Compat.fst +++ b/krmllib/compat/C.Compat.fst @@ -2,7 +2,6 @@ module C.Compat open FStar.HyperStack.ST -module HS = FStar.HyperStack module U8 = FStar.UInt8 // This module contains a series of bindings that already exist in C. It receives diff --git a/krmllib/compat/C.Nullity.fsti b/krmllib/compat/C.Nullity.fsti index fffdac8f..968207ad 100644 --- a/krmllib/compat/C.Nullity.fsti +++ b/krmllib/compat/C.Nullity.fsti @@ -37,9 +37,6 @@ let (!*) (#a: Type) (p: pointer a): (ensures (fun h0 x h1 -> B.live h1 p /\ x == B.get h0 p 0 /\ h1 == h0)) = B.index p 0ul -module U32 = FStar.UInt32 -module Seq = FStar.Seq -module Heap = FStar.Heap (* Two pointers with different reads are disjoint *) From bafc55f80d2d27f6cc1d2479b9d1741851237218 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 17 Feb 2025 11:43:23 -0800 Subject: [PATCH 13/13] Run `$FSTAR/.scripts/remove_all_unused_opens.sh test/` --- test/Ctypes2.fst | 2 -- test/Ctypes4.fst | 1 - test/DataTypesEq.fst | 1 - test/HigherOrder2.fst | 1 - test/HigherOrder4.fst | 1 - test/Layered.fst | 1 - test/LinkedList1.fst | 1 - test/LinkedList2.fst | 1 - test/LinkedList3.fst | 1 - test/Lowlevel.fst | 1 - test/MutualStruct.fst | 1 - test/NoShadow.fst | 1 - test/Rust6.fst | 1 - test/Scope.fst | 1 - test/TotalLoops.fst | 2 -- test/Underspec.fst | 1 - test/hello-system/SystemNative.fsti | 1 - test/sepcomp/b/B.fst | 1 - test/sepcomp/b/D.fst | 1 - 19 files changed, 21 deletions(-) diff --git a/test/Ctypes2.fst b/test/Ctypes2.fst index d28dc264..05f9b7cf 100644 --- a/test/Ctypes2.fst +++ b/test/Ctypes2.fst @@ -4,8 +4,6 @@ open FStar.Mul open FStar.UInt open FStar.HyperStack.ST -module M = LowStar.Modifies -module U16 = FStar.UInt16 module U32 = FStar.UInt32 open Ctypes1 diff --git a/test/Ctypes4.fst b/test/Ctypes4.fst index 0f77378d..78a004d9 100644 --- a/test/Ctypes4.fst +++ b/test/Ctypes4.fst @@ -5,7 +5,6 @@ open FStar.UInt open FStar.HyperStack.ST module B = LowStar.Buffer -module M = LowStar.Modifies module U16 = FStar.UInt16 module U32 = FStar.UInt32 module U128 = FStar.UInt128 diff --git a/test/DataTypesEq.fst b/test/DataTypesEq.fst index d924c952..fa499ece 100644 --- a/test/DataTypesEq.fst +++ b/test/DataTypesEq.fst @@ -1,6 +1,5 @@ module DataTypesEq -module SoBuggy = FStar.HyperStack.ST type t = | A: UInt32.t -> t diff --git a/test/HigherOrder2.fst b/test/HigherOrder2.fst index 3c5eb3fe..720c1168 100644 --- a/test/HigherOrder2.fst +++ b/test/HigherOrder2.fst @@ -1,6 +1,5 @@ module HigherOrder2 -module HS = FStar.HyperStack module HST = FStar.HyperStack.ST module I32 = FStar.Int32 module M = LowStar.Modifies diff --git a/test/HigherOrder4.fst b/test/HigherOrder4.fst index acbc1325..2433223f 100644 --- a/test/HigherOrder4.fst +++ b/test/HigherOrder4.fst @@ -4,7 +4,6 @@ module B = LowStar.Buffer module HS = FStar.HyperStack module HST = FStar.HyperStack.ST module M = LowStar.Modifies -module U32 = FStar.UInt32 module I32 = FStar.Int32 open LowStar.BufferOps diff --git a/test/Layered.fst b/test/Layered.fst index 5c91820e..c227123b 100644 --- a/test/Layered.fst +++ b/test/Layered.fst @@ -1,7 +1,6 @@ module Layered open FStar.HyperStack.ST -module U32 = FStar.UInt32 module HS = FStar.HyperStack inline_for_extraction diff --git a/test/LinkedList1.fst b/test/LinkedList1.fst index 7ee4fdbc..7d7f1edb 100644 --- a/test/LinkedList1.fst +++ b/test/LinkedList1.fst @@ -1,6 +1,5 @@ module LinkedList1 -module B = FStar.Buffer module HS = FStar.HyperStack module G = FStar.Ghost module L = FStar.List.Tot diff --git a/test/LinkedList2.fst b/test/LinkedList2.fst index c43f117a..597c2037 100644 --- a/test/LinkedList2.fst +++ b/test/LinkedList2.fst @@ -4,7 +4,6 @@ module B = FStar.Buffer module CN = C.Nullity module HS = FStar.HyperStack module G = FStar.Ghost -module L = FStar.List.Tot module U32 = FStar.UInt32 module MO = FStar.Modifies diff --git a/test/LinkedList3.fst b/test/LinkedList3.fst index d20b8ee6..a278f249 100644 --- a/test/LinkedList3.fst +++ b/test/LinkedList3.fst @@ -4,7 +4,6 @@ open LowStar.BufferOps module B = LowStar.Buffer module HS = FStar.HyperStack module G = FStar.Ghost -module L = FStar.List.Tot module U32 = FStar.UInt32 module MO = LowStar.Modifies diff --git a/test/Lowlevel.fst b/test/Lowlevel.fst index 7bfad14d..f2300f59 100644 --- a/test/Lowlevel.fst +++ b/test/Lowlevel.fst @@ -7,7 +7,6 @@ open FStar.UInt open FStar.HyperStack.ST module B = LowStar.Buffer -module M = LowStar.Modifies module U16 = FStar.UInt16 module U32 = FStar.UInt32 diff --git a/test/MutualStruct.fst b/test/MutualStruct.fst index 17ca28b7..5d0d9ffc 100644 --- a/test/MutualStruct.fst +++ b/test/MutualStruct.fst @@ -5,7 +5,6 @@ open FStar.HyperStack.ST module U64 = FStar.UInt64 module U8 = FStar.UInt8 -module SZ = FStar.SizeT let main () = C.EXIT_SUCCESS // dummy diff --git a/test/NoShadow.fst b/test/NoShadow.fst index d7a201cc..ca5fad16 100644 --- a/test/NoShadow.fst +++ b/test/NoShadow.fst @@ -2,7 +2,6 @@ module NoShadow module U32 = FStar.UInt32 module U64 = FStar.UInt64 -module HS = FStar.HyperStack open FStar.HyperStack.ST diff --git a/test/Rust6.fst b/test/Rust6.fst index d09cea3c..6783be3a 100644 --- a/test/Rust6.fst +++ b/test/Rust6.fst @@ -4,7 +4,6 @@ open FStar.HyperStack.ST module B = LowStar.Buffer module C = LowStar.ConstBuffer -module HS = FStar.HyperStack inline_for_extraction noextract diff --git a/test/Scope.fst b/test/Scope.fst index 55dc096b..d84a62b3 100644 --- a/test/Scope.fst +++ b/test/Scope.fst @@ -5,7 +5,6 @@ open FStar.Int32 open FStar.HyperStack.ST open TestLib -module B = FStar.Buffer let foo (): Stack bool (fun _ -> true) (fun h0 _ h1 -> h0 == h1) = true diff --git a/test/TotalLoops.fst b/test/TotalLoops.fst index 631eed7c..6f354aa6 100644 --- a/test/TotalLoops.fst +++ b/test/TotalLoops.fst @@ -3,8 +3,6 @@ module TotalLoops open FStar open FStar.Buffer open FStar.HyperStack.ST -module UInt32 = FStar.UInt32 -module UInt64 = FStar.UInt64 let rec fib (x: nat) diff --git a/test/Underspec.fst b/test/Underspec.fst index e63e4da8..a136107a 100644 --- a/test/Underspec.fst +++ b/test/Underspec.fst @@ -1,7 +1,6 @@ module Underspec open FStar.HyperStack.ST -module U32 = FStar.UInt32 (* Checking that the *_underspec operators actually extract and run properly. *) diff --git a/test/hello-system/SystemNative.fsti b/test/hello-system/SystemNative.fsti index 11f71330..a29b84de 100644 --- a/test/hello-system/SystemNative.fsti +++ b/test/hello-system/SystemNative.fsti @@ -13,7 +13,6 @@ module SystemNative module S = FStar.Seq module B = FStar.Buffer module U8 = FStar.UInt8 -module I32 = FStar.UInt8 module U32 = FStar.UInt32 (* Strings *******************************************************************) diff --git a/test/sepcomp/b/B.fst b/test/sepcomp/b/B.fst index 5c83223d..02677355 100644 --- a/test/sepcomp/b/B.fst +++ b/test/sepcomp/b/B.fst @@ -1,5 +1,4 @@ module B -module U32 = FStar.UInt32 module U64 = FStar.UInt64 module Cast = FStar.Int.Cast module A = A.Top diff --git a/test/sepcomp/b/D.fst b/test/sepcomp/b/D.fst index a83390ef..11e5fe53 100644 --- a/test/sepcomp/b/D.fst +++ b/test/sepcomp/b/D.fst @@ -1,5 +1,4 @@ module D -module U32 = FStar.UInt32 module U64 = FStar.UInt64 module Cast = FStar.Int.Cast module A = A.Top