diff --git a/engine/backends/coq/coq/coq_backend.ml b/engine/backends/coq/coq/coq_backend.ml index 0093790ef..34338363f 100644 --- a/engine/backends/coq/coq/coq_backend.ml +++ b/engine/backends/coq/coq/coq_backend.ml @@ -677,8 +677,8 @@ let hardcoded_coq_headers = Open Scope Z_scope.\n\ Open Scope bool_scope.\n" -let translate _ (_bo : BackendOptions.t) (items : AST.item list) : - Types.file list = +let translate _ (_bo : BackendOptions.t) ~(bundles : AST.item list list) + (items : AST.item list) : Types.file list = U.group_items_by_namespace items |> Map.to_alist |> List.map ~f:(fun (ns, items) -> diff --git a/engine/backends/coq/ssprove/ssprove_backend.ml b/engine/backends/coq/ssprove/ssprove_backend.ml index 72a64451f..6db7387c9 100644 --- a/engine/backends/coq/ssprove/ssprove_backend.ml +++ b/engine/backends/coq/ssprove/ssprove_backend.ml @@ -2404,8 +2404,8 @@ let hardcoded_coq_headers = Import choice.Choice.Exports.\n\n\ Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations.\n" -let translate _ (_bo : BackendOptions.t) (items : AST.item list) : - Types.file list = +let translate _ (_bo : BackendOptions.t) ~(bundles : AST.item list list) + (items : AST.item list) : Types.file list = let analysis_data = StaticAnalysis.analyse items in U.group_items_by_namespace items |> Map.to_alist diff --git a/engine/backends/easycrypt/easycrypt_backend.ml b/engine/backends/easycrypt/easycrypt_backend.ml index abc2c38cd..ac3c74f50 100644 --- a/engine/backends/easycrypt/easycrypt_backend.ml +++ b/engine/backends/easycrypt/easycrypt_backend.ml @@ -332,8 +332,8 @@ let translate' (_bo : BackendOptions.t) (items : AST.item list) : doit Stdlib.Format.err_formatter items; [] -let translate _ (bo : BackendOptions.t) (items : AST.item list) : - Types.file list = +let translate _ (bo : BackendOptions.t) ~(bundles : AST.item list list) + (items : AST.item list) : Types.file list = try translate' bo items with Assert_failure (file, line, col) -> Diagnostics.failure ~context:(Backend FStar) ~span:(Span.dummy ()) diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 91ac4843a..667db2f41 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -97,6 +97,11 @@ module Context = struct } end +(** Convers a namespace to a module name *) +let module_name (ns : string * string list) : string = + String.concat ~sep:"." + (List.map ~f:(map_first_letter String.uppercase) (fst ns :: snd ns)) + module Make (Attrs : Attrs.WITH_ITEMS) (Ctx : sig val ctx : Context.t @@ -857,19 +862,17 @@ struct list = match e.v with | Alias { name; item } -> - let pat = - F.pat - @@ F.AST.PatVar - (F.id @@ U.Concrete_ident_view.to_definition_name name, None, []) - in - F.decls ~quals:[ F.AST.Unfold_for_unification_and_vcgen ] - @@ F.AST.TopLevelLet - ( NoLetQualifier, - [ (pat, F.term @@ F.AST.Name (pconcrete_ident item)) ] ) + (* These should come from bundled items (in the case of cyclic module dependencies). + We make use of this f* feature: https://github.com/FStarLang/FStar/pull/3369 *) + let bundle = U.Concrete_ident_view.to_namespace item |> module_name in + [ + `VerbatimImpl + ( Printf.sprintf "include %s {%s as %s}" bundle + (U.Concrete_ident_view.to_definition_name item) + (U.Concrete_ident_view.to_definition_name name), + `Newline ); + ] | Fn { name; generics; body; params } -> - let is_rec = - Set.mem (U.Reducers.collect_concrete_idents#visit_expr () body) name - in let name = F.id @@ U.Concrete_ident_view.to_definition_name name in let pat = F.pat @@ F.AST.PatVar (name, None, []) in let generics = FStarBinder.of_generics e.span generics in @@ -882,7 +885,7 @@ struct params in let pat = F.pat @@ F.AST.PatApp (pat, pat_args) in - let qualifier = F.AST.(if is_rec then Rec else NoLetQualifier) in + let qualifier = F.AST.(NoLetQualifier) in let impl = F.decl ~fsti:false @@ F.AST.TopLevelLet (qualifier, [ (pat, pexpr body) ]) @@ -1554,13 +1557,10 @@ let strings_of_item ~signature_only (bo : BackendOptions.t) m items if interface_mode then [ (`Impl s, `Newline); (`Intf s, `Newline) ] else [ (`Impl s, `Newline) ]) -(** Convers a namespace to a module name *) -let module_name (ns : string * string list) : string = - String.concat ~sep:"." - (List.map ~f:(map_first_letter String.uppercase) (fst ns :: snd ns)) +type rec_prefix = NonRec | FirstMutRec | MutRec -let string_of_items ~signature_only ~mod_name (bo : BackendOptions.t) m items : - string * string = +let string_of_items ~signature_only ~mod_name ~bundles (bo : BackendOptions.t) m + items : string * string = let collect_trait_goal_idents = object inherit [_] Visitors.reduce as super @@ -1600,14 +1600,48 @@ let string_of_items ~signature_only ~mod_name (bo : BackendOptions.t) m items : |> String.concat ~sep:"") ^ "\n\n" in - let strings = - List.concat_map ~f:(strings_of_item ~signature_only bo m items) items - |> List.map - ~f: - ((function - | `Impl s -> `Impl (String.strip s) - | `Intf s -> `Intf (String.strip s)) - *** Fn.id) + let map_string ~f (str, space) = + ((match str with `Impl s -> `Impl (f s) | `Intf s -> `Intf (f s)), space) + in + let replace_in_strs ~pattern ~with_ = + List.map + ~f: + (map_string ~f:(fun str -> + String.substr_replace_first ~pattern ~with_ str)) + in + + (* Each of these bundles contains recursive items (mutually if the bundle has more than one element). + We know that these items will already be grouped together but we need to add the `rec` qualifier + to the first one (in the case of functions). And to replace the `let`/`type` keyword by `and` + for the other elements coming after. *) + let first_in_bundles = Array.create (List.length bundles) None in + let get_recursivity_prefix it = + match + List.findi bundles ~f:(fun _ bundle -> + List.mem bundle it ~equal:[%eq: item]) + with + | Some (i, _) -> ( + match first_in_bundles.(i) with + | Some first_it when [%eq: item] first_it it -> FirstMutRec + | Some _ -> MutRec + | None -> + first_in_bundles.(i) <- Some it; + FirstMutRec) + | None -> NonRec + in + let strings its = + List.concat_map + ~f:(fun item -> + let recursivity_prefix = get_recursivity_prefix item in + let strs = strings_of_item ~signature_only bo m items item in + match (recursivity_prefix, item.v) with + | FirstMutRec, Fn _ -> + replace_in_strs ~pattern:"let" ~with_:"let rec" strs + | MutRec, Fn _ -> replace_in_strs ~pattern:"let" ~with_:"and" strs + | MutRec, Type _ -> replace_in_strs ~pattern:"type" ~with_:"and" strs + | _ -> strs) + its + |> List.map ~f:(map_string ~f:String.strip) |> List.filter ~f:(fst >> (function `Impl s | `Intf s -> String.is_empty s) >> not) in @@ -1617,7 +1651,7 @@ let string_of_items ~signature_only ~mod_name (bo : BackendOptions.t) m items : ~f:(fun (s, space) -> let* s = filter s in Some (s, space)) - strings + (strings items) in let n = List.length l - 1 in let lines = @@ -1643,8 +1677,8 @@ let fstar_headers (bo : BackendOptions.t) = in [ opts; "open Core"; "open FStar.Mul" ] |> String.concat ~sep:"\n" -let translate m (bo : BackendOptions.t) (items : AST.item list) : - Types.file list = +let translate m (bo : BackendOptions.t) ~(bundles : AST.item list list) + (items : AST.item list) : Types.file list = let show_view Concrete_ident.{ crate; path; definition } = crate :: (path @ [ definition ]) |> String.concat ~sep:"::" in @@ -1663,7 +1697,7 @@ let translate m (bo : BackendOptions.t) (items : AST.item list) : in let mod_name = module_name ns in let impl, intf = - string_of_items ~signature_only ~mod_name bo m items + string_of_items ~signature_only ~mod_name ~bundles bo m items in let make ~ext body = if String.is_empty body then None @@ -1681,7 +1715,6 @@ let translate m (bo : BackendOptions.t) (items : AST.item list) : [ make ~ext:"fst" impl; make ~ext:"fsti" intf ]) open Phase_utils -module DepGraph = Dependencies.Make (InputLanguage) module DepGraphR = Dependencies.Make (Features.Rust) module TransformToInputLanguage = @@ -1765,6 +1798,5 @@ let apply_phases (bo : BackendOptions.t) (items : Ast.Rust.item list) : |> List.map ~f:unsize_as_identity |> List.map ~f:unsize_as_identity |> List.map ~f:U.Mappers.add_typ_ascription - (* |> DepGraph.name_me *) in items diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index 1cea56cc5..f66a1ea14 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -865,8 +865,8 @@ module Make (Options : OPTS) : MAKE = struct end) end -let translate m (bo : BackendOptions.t) (items : AST.item list) : - Types.file list = +let translate m (bo : BackendOptions.t) ~(bundles : AST.item list list) + (items : AST.item list) : Types.file list = let (module M : MAKE) = (module Make (struct let options = bo diff --git a/engine/bin/lib.ml b/engine/bin/lib.ml index 67d19d0b7..efa2d60ed 100644 --- a/engine/bin/lib.ml +++ b/engine/bin/lib.ml @@ -112,6 +112,9 @@ let run (options : Types.engine_options) : Types.output = ([%show: Diagnostics.Backend.t] M.backend)); let items = apply_phases backend_options items in let with_items = Attrs.with_items items in + let module DepGraph = Dependencies.Make (InputLanguage) in + let items = DepGraph.bundle_cyclic_modules items in + let bundles, _ = DepGraph.recursive_bundles items in let items = List.filter items ~f:(fun (i : AST.item) -> Attrs.late_skip i.attrs |> not) @@ -119,7 +122,7 @@ let run (options : Types.engine_options) : Types.output = Logs.info (fun m -> m "Translating items with backend %s" ([%show: Diagnostics.Backend.t] M.backend)); - let items = translate with_items backend_options items in + let items = translate with_items backend_options items ~bundles in items in let diagnostics, files = diff --git a/engine/lib/backend.ml b/engine/lib/backend.ml index 83007df16..0dfb6ea26 100644 --- a/engine/lib/backend.ml +++ b/engine/lib/backend.ml @@ -31,6 +31,7 @@ module type T = sig val translate : (module Attrs.WITH_ITEMS) -> BackendOptions.t -> + bundles:AST.item list list -> AST.item list -> Types.file list diff --git a/engine/lib/dependencies.ml b/engine/lib/dependencies.ml index 6cff71f6d..1cfb0ba3b 100644 --- a/engine/lib/dependencies.ml +++ b/engine/lib/dependencies.ml @@ -6,7 +6,8 @@ module Make (F : Features.T) = struct open Ast open AST - let ident_of (item : item) : Concrete_ident.t = item.ident + let ident_of (item : item) : Concrete_ident.t = + match item.v with Type { name; _ } -> name | _ -> item.ident module Namespace = struct module T = struct @@ -153,6 +154,76 @@ module Make (F : Features.T) = struct (of_graph g).mut_rec_bundles end + module CyclicDep = struct + (* We are looking for dependencies between items that give a cyclic dependency at the module level + (but not necessarily at the item level). All the items belonging to such a cycle should be bundled + together. *) + (* The algorithm is to take the transitive closure of the items dependency graph and look + for paths of length 3 that in terms of modules have the form A -> B -> A (A != B) *) + (* To compute the bundles, we keep a second (undirected graph) where an edge between two items + means they should be in the same bundle. The bundles are the connected components of this graph. *) + module Bundle = struct + type t = Concrete_ident.t list + + module G = Graph.Persistent.Graph.Concrete (Concrete_ident) + module CC = Graph.Components.Undirected (G) + + let cycles g = CC.components_list g + end + + let of_graph' (g : G.t) (mod_graph_cycles : Namespace.Set.t list) : + Bundle.t list = + let closure = Oper.transitive_closure g in + + let bundles_graph = + G.fold_vertex + (fun start (bundles_graph : Bundle.G.t) -> + let start_mod = Namespace.of_concrete_ident start in + let cycle_modules = + List.filter mod_graph_cycles ~f:(fun cycle -> + Set.mem cycle start_mod) + |> List.reduce ~f:Set.union + in + match cycle_modules with + | Some cycle_modules -> + let bundles_graph = + G.fold_succ + (fun interm bundles_graph -> + let interm_mod = Namespace.of_concrete_ident interm in + if + (not ([%eq: Namespace.t] interm_mod start_mod)) + && Set.mem cycle_modules interm_mod + then + G.fold_succ + (fun dest bundles_graph -> + let dest_mod = Namespace.of_concrete_ident dest in + if [%eq: Namespace.t] interm_mod dest_mod then + let g = + Bundle.G.add_edge bundles_graph start interm + in + let g = Bundle.G.add_edge g interm dest in + g + else bundles_graph) + g start bundles_graph + else bundles_graph) + g start bundles_graph + in + + bundles_graph + | None -> bundles_graph) + closure Bundle.G.empty + in + + let bundles = Bundle.cycles bundles_graph in + bundles + + let of_graph (g : G.t) (mod_graph_cycles : Namespace.Set.t list) : + Bundle.t list = + match mod_graph_cycles with + | [] -> [] + | _ -> of_graph' g mod_graph_cycles + end + open Graph.Graphviz.Dot (struct include G @@ -182,7 +253,6 @@ module Make (F : Features.T) = struct let of_items (items : item list) : G.t = let ig = ItemGraph.of_items ~original_items:items items in - assert (ItemGraph.MutRec.all_homogeneous_namespace ig); List.map ~f:(ident_of >> (Namespace.of_concrete_ident &&& Fn.id)) items |> Map.of_alist_multi (module Namespace) |> Map.map @@ -199,6 +269,9 @@ module Make (F : Features.T) = struct module SCC = Graph.Components.Make (G) + let cycles g : Namespace.Set.t list = + SCC.scc_list g |> List.map ~f:(Set.of_list (module Namespace)) + open Graph.Graphviz.Dot (struct include G @@ -343,61 +416,102 @@ module Make (F : Features.T) = struct (* Construct the new item `f item` (say `item'`), and create a "symbolic link" to `item'`. Returns a pair that consists in the symbolic link and in `item'`. *) - let shallow_copy (f : item -> item) (item : item) : item * item = + let shallow_copy (f : item -> item) + (variants_renamings : + concrete_ident * concrete_ident -> + (concrete_ident * concrete_ident) list) (item : item) : item list = let item' = f item in - ({ item with v = Alias { name = item.ident; item = item'.ident } }, item') + let old_new = (ident_of item, ident_of item') in + let aliases = + List.map (old_new :: variants_renamings old_new) + ~f:(fun (old_ident, new_ident) -> + { item with v = Alias { name = old_ident; item = new_ident } }) + in + item' :: aliases - let name_me' (items : item list) : item list = + let bundle_cyclic_modules (items : item list) : item list = let g = ItemGraph.of_items ~original_items:items items in let from_ident ident : item option = List.find ~f:(fun i -> [%equal: Concrete_ident.t] i.ident ident) items in - let non_mut_rec, mut_rec_bundles = - let b = ItemGraph.MutRec.of_graph g in + let mut_rec_bundles = + let mod_graph_cycles = ModGraph.of_items items |> ModGraph.cycles in + let bundles = ItemGraph.CyclicDep.of_graph g mod_graph_cycles in let f = List.filter_map ~f:from_ident in - (f b.non_mut_rec, List.map ~f b.mut_rec_bundles) + List.map ~f bundles in - let transform (bundle : item list) = + + let transform (bundle : item list) it = let ns : Concrete_ident.t = Concrete_ident.Create.fresh_module ~from:(List.map ~f:ident_of bundle) in let new_name_under_ns : Concrete_ident.t -> Concrete_ident.t = Concrete_ident.Create.move_under ~new_parent:ns in + let new_names = List.map ~f:(ident_of >> new_name_under_ns) bundle in + let duplicates = + new_names |> List.find_all_dups ~compare:Concrete_ident.compare + in + (* Verify name clashes *) + (* In case of clash, add hash *) + let add_prefix id = + if + not + (List.mem duplicates (new_name_under_ns id) + ~equal:Concrete_ident.equal) + then id + else + Concrete_ident.Create.map_last + ~f:(fun name -> name ^ (Concrete_ident.hash id |> Int.to_string)) + id + in let renamings = - List.map ~f:(ident_of >> (Fn.id &&& new_name_under_ns)) bundle - |> Map.of_alist_exn (module Concrete_ident) + List.map + ~f:(ident_of >> (Fn.id &&& (add_prefix >> new_name_under_ns))) + bundle + in + let variants_renamings (previous_name, new_name) = + match from_ident previous_name with + | Some { v = Type { variants; _ }; _ } -> + List.map variants ~f:(fun { name; _ } -> + ( name, + Concrete_ident.Create.move_under ~new_parent:new_name name )) + | _ -> [] + in + + let renamings = + Map.of_alist_exn + (module Concrete_ident) + (renamings @ List.concat_map ~f:variants_renamings renamings) in let rename = let renamer _lvl i = Map.find renamings i |> Option.value ~default:i in (U.Mappers.rename_concrete_idents renamer)#visit_item ExprLevel in - let shallow, bundle = - List.map ~f:(shallow_copy rename) bundle |> List.unzip - in - bundle @ shallow + shallow_copy rename variants_renamings it in - let mut_rec_bundles = - List.map - ~f:(fun bundle -> + let maybe_transform_item it = + match + List.find + ~f:(fun bundle -> List.mem bundle it ~equal:[%eq: item]) + mut_rec_bundles + with + | Some bundle -> if List.map ~f:ident_of bundle |> ItemGraph.MutRec.Bundle.homogeneous_namespace - then bundle - else transform bundle) - mut_rec_bundles + then [ it ] + else transform bundle it + | None -> [ it ] in - non_mut_rec @ List.concat_map ~f:Fn.id mut_rec_bundles + List.concat_map items ~f:maybe_transform_item - let name_me (items : item list) : item list = - let h f name items = - let file = Stdlib.open_out @@ "/tmp/graph_" ^ name ^ ".dot" in - f file items; - Stdlib.close_out file + let recursive_bundles (items : item list) : item list list * item list = + let g = ItemGraph.of_items ~original_items:items items in + let bundles = ItemGraph.MutRec.of_graph g in + let from_ident ident : item option = + List.find ~f:(fun i -> [%equal: Concrete_ident.t] i.ident ident) items in - h ItemGraph.print "items_before" items; - let items = name_me' items in - h ItemGraph.print "items_after" items; - h ModGraph.print "mods" items; - items + let f = List.filter_map ~f:from_ident in + (List.map ~f bundles.mut_rec_bundles, f bundles.non_mut_rec) end diff --git a/engine/lib/dependencies.mli b/engine/lib/dependencies.mli index b73e39a1c..5c39773de 100644 --- a/engine/lib/dependencies.mli +++ b/engine/lib/dependencies.mli @@ -2,8 +2,9 @@ module Make (F : Features.T) : sig module AST : module type of Ast.Make (F) val uid_associated_items : AST.item list -> Ast.attrs -> AST.item list - val name_me : AST.item list -> AST.item list + val bundle_cyclic_modules : AST.item list -> AST.item list val sort : AST.item list -> AST.item list + val recursive_bundles : AST.item list -> AST.item list list * AST.item list val filter_by_inclusion_clauses : Types.inclusion_clause list -> AST.item list -> AST.item list diff --git a/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap b/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap new file mode 100644 index 000000000..453e0d2a1 --- /dev/null +++ b/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap @@ -0,0 +1,294 @@ +--- +source: test-harness/src/harness.rs +expression: snapshot +info: + kind: + Translate: + backend: fstar + info: + name: cyclic-modules + manifest: cyclic-modules/Cargo.toml + description: ~ + spec: + optional: false + broken: false + issue_id: ~ + positive: true + snapshot: + stderr: false + stdout: true + include_flag: ~ + backend_options: ~ +--- +exit = 0 + +[stdout] +diagnostics = [] + +[stdout.files] +"Cyclic_modules.B.fst" = ''' +module Cyclic_modules.B +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +include Cyclic_modules.Rec_bundle_507852343 {g as g} +''' +"Cyclic_modules.C.fst" = ''' +module Cyclic_modules.C +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +let i (_: Prims.unit) : Prims.unit = () +''' +"Cyclic_modules.D.fst" = ''' +module Cyclic_modules.D +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +include Cyclic_modules.E.Rec_bundle_868781766 {d1 as d1} + +include Cyclic_modules.E.Rec_bundle_868781766 {d2 as d2} +''' +"Cyclic_modules.De.fst" = ''' +module Cyclic_modules.De +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +include Cyclic_modules.E.Rec_bundle_868781766 {de1 as de1} +''' +"Cyclic_modules.E.Rec_bundle_868781766.fst" = ''' +module Cyclic_modules.E.Rec_bundle_868781766 +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +let d1 (_: Prims.unit) : Prims.unit = () + +let e1 (_: Prims.unit) : Prims.unit = d1 () + +let de1 (_: Prims.unit) : Prims.unit = e1 () + +let d2 (_: Prims.unit) : Prims.unit = de1 () +''' +"Cyclic_modules.E.fst" = ''' +module Cyclic_modules.E +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +include Cyclic_modules.E.Rec_bundle_868781766 {e1 as e1} +''' +"Cyclic_modules.Enums_a.fst" = ''' +module Cyclic_modules.Enums_a +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +include Cyclic_modules.Enums_b.Rec_bundle_573885887 {t_T240131830 as t_T} + +include Cyclic_modules.Enums_b.Rec_bundle_573885887 {T240131830_A as T_A} + +include Cyclic_modules.Enums_b.Rec_bundle_573885887 {T240131830_B as T_B} + +include Cyclic_modules.Enums_b.Rec_bundle_573885887 {T240131830_C as T_C} + +include Cyclic_modules.Enums_b.Rec_bundle_573885887 {T240131830_D as T_D} +''' +"Cyclic_modules.Enums_b.Rec_bundle_573885887.fst" = ''' +module Cyclic_modules.Enums_b.Rec_bundle_573885887 +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +type t_T366415196 = + | T366415196_A : t_T366415196 + | T366415196_B : t_T366415196 + | T366415196_C : Alloc.Vec.t_Vec t_T240131830 Alloc.Alloc.t_Global -> t_T366415196 + +and t_U = + | U_A : t_U + | U_B : t_U + | U_C : Alloc.Vec.t_Vec t_T240131830 Alloc.Alloc.t_Global -> t_U + +and t_T240131830 = + | T240131830_A : t_T240131830 + | T240131830_B : t_T240131830 + | T240131830_C : Alloc.Vec.t_Vec t_U Alloc.Alloc.t_Global -> t_T240131830 + | T240131830_D : Alloc.Vec.t_Vec t_T366415196 Alloc.Alloc.t_Global -> t_T240131830 +''' +"Cyclic_modules.Enums_b.fst" = ''' +module Cyclic_modules.Enums_b +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +include Cyclic_modules.Enums_b.Rec_bundle_573885887 {t_T366415196 as t_T} + +include Cyclic_modules.Enums_b.Rec_bundle_573885887 {T366415196_A as T_A} + +include Cyclic_modules.Enums_b.Rec_bundle_573885887 {T366415196_B as T_B} + +include Cyclic_modules.Enums_b.Rec_bundle_573885887 {T366415196_C as T_C} + +include Cyclic_modules.Enums_b.Rec_bundle_573885887 {t_U as t_U} + +include Cyclic_modules.Enums_b.Rec_bundle_573885887 {U_A as U_A} + +include Cyclic_modules.Enums_b.Rec_bundle_573885887 {U_B as U_B} + +include Cyclic_modules.Enums_b.Rec_bundle_573885887 {U_C as U_C} + +let f (_: Prims.unit) : t_T = T_A <: t_T +''' +"Cyclic_modules.Rec.fst" = ''' +module Cyclic_modules.Rec +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +type t_T = + | T_t1 : t_T + | T_t2 : t_T + +let t_T_cast_to_repr (x: t_T) : isize = + match x with + | T_t1 -> isz 0 + | T_t2 -> isz 1 + +let rec hf (x: t_T) : t_T = + match x with + | T_t1 -> hf (T_t2 <: t_T) + | T_t2 -> x + +let rec g1 (x: t_T) : t_T = + match x with + | T_t1 -> g2 x + | T_t2 -> T_t1 <: t_T + +and g2 (x: t_T) : t_T = + match x with + | T_t1 -> g1 x + | T_t2 -> hf x +''' +"Cyclic_modules.Rec1_same_name.fst" = ''' +module Cyclic_modules.Rec1_same_name +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +include Cyclic_modules.Rec2_same_name.Rec_bundle_784146069 {f533409751 as f} +''' +"Cyclic_modules.Rec2_same_name.Rec_bundle_784146069.fst" = ''' +module Cyclic_modules.Rec2_same_name.Rec_bundle_784146069 +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +let rec f533409751 (x: i32) : i32 = f91805216 x + +and f91805216 (x: i32) : i32 = if x >. 0l then f533409751 (x -! 1l <: i32) else 0l +''' +"Cyclic_modules.Rec2_same_name.fst" = ''' +module Cyclic_modules.Rec2_same_name +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +include Cyclic_modules.Rec2_same_name.Rec_bundle_784146069 {f91805216 as f} +''' +"Cyclic_modules.Rec_bundle_507852343.fst" = ''' +module Cyclic_modules.Rec_bundle_507852343 +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +let f (_: Prims.unit) : Prims.unit = () + +let g (_: Prims.unit) : Prims.unit = f () + +let h (_: Prims.unit) : Prims.unit = + let _:Prims.unit = g () in + Cyclic_modules.C.i () +''' +"Cyclic_modules.Typ_a.fst" = ''' +module Cyclic_modules.Typ_a +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +include Cyclic_modules.Typ_b.Rec_bundle_684725220 {t_T as t_T} + +include Cyclic_modules.Typ_b.Rec_bundle_684725220 {T_T as T_T} + +include Cyclic_modules.Typ_b.Rec_bundle_445945170 {t_TRec as t_TRec} + +include Cyclic_modules.Typ_b.Rec_bundle_445945170 {TRec_T as TRec_T} + +include Cyclic_modules.Typ_b.Rec_bundle_445945170 {TRec_Empty as TRec_Empty} +''' +"Cyclic_modules.Typ_b.Rec_bundle_445945170.fst" = ''' +module Cyclic_modules.Typ_b.Rec_bundle_445945170 +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +type t_TRec = + | TRec_T : t_T1Rec -> t_TRec + | TRec_Empty : t_TRec + +and t_T1Rec = | T1Rec_T1 : Alloc.Boxed.t_Box t_T2Rec Alloc.Alloc.t_Global -> t_T1Rec + +and t_T2Rec = | T2Rec_T2 : t_TRec -> t_T2Rec +''' +"Cyclic_modules.Typ_b.Rec_bundle_684725220.fst" = ''' +module Cyclic_modules.Typ_b.Rec_bundle_684725220 +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +type t_T1 = | T1_T1 : t_T1 + +type t_T = | T_T : t_T1 -> t_T + +type t_T2 = | T2_T2 : t_T -> t_T2 +''' +"Cyclic_modules.Typ_b.fst" = ''' +module Cyclic_modules.Typ_b +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +include Cyclic_modules.Typ_b.Rec_bundle_684725220 {t_T1 as t_T1} + +include Cyclic_modules.Typ_b.Rec_bundle_684725220 {T1_T1 as T1_T1} + +let t_T1_cast_to_repr (x: t_T1) : isize = match x with | T1_T1 -> isz 0 + +include Cyclic_modules.Typ_b.Rec_bundle_684725220 {t_T2 as t_T2} + +include Cyclic_modules.Typ_b.Rec_bundle_684725220 {T2_T2 as T2_T2} + +include Cyclic_modules.Typ_b.Rec_bundle_445945170 {t_T1Rec as t_T1Rec} + +include Cyclic_modules.Typ_b.Rec_bundle_445945170 {T1Rec_T1 as T1Rec_T1} + +include Cyclic_modules.Typ_b.Rec_bundle_445945170 {t_T2Rec as t_T2Rec} + +include Cyclic_modules.Typ_b.Rec_bundle_445945170 {T2Rec_T2 as T2Rec_T2} +''' +"Cyclic_modules.fst" = ''' +module Cyclic_modules +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +include Cyclic_modules.Rec_bundle_507852343 {f as f} + +include Cyclic_modules.Rec_bundle_507852343 {h as h} + +let h2 (_: Prims.unit) : Prims.unit = Cyclic_modules.C.i () +''' diff --git a/tests/Cargo.lock b/tests/Cargo.lock index 48a1e7c04..79d1a6115 100644 --- a/tests/Cargo.lock +++ b/tests/Cargo.lock @@ -217,6 +217,10 @@ dependencies = [ "cfg-if", ] +[[package]] +name = "cyclic-modules" +version = "0.1.0" + [[package]] name = "dyn" version = "0.1.0" diff --git a/tests/Cargo.toml b/tests/Cargo.toml index f96370e8a..10969e04d 100644 --- a/tests/Cargo.toml +++ b/tests/Cargo.toml @@ -33,6 +33,7 @@ members = [ "recursion", "functions", "guards", + "cyclic-modules", "unsafe", ] resolver = "2" diff --git a/tests/cyclic-modules/Cargo.toml b/tests/cyclic-modules/Cargo.toml new file mode 100644 index 000000000..092cfd078 --- /dev/null +++ b/tests/cyclic-modules/Cargo.toml @@ -0,0 +1,9 @@ +[package] +name = "cyclic-modules" +version = "0.1.0" +edition = "2021" + +[dependencies] + +[package.metadata.hax-tests] +into."fstar" = { broken = false, snapshot = "stdout", issue_id = "396" } diff --git a/tests/cyclic-modules/src/lib.rs b/tests/cyclic-modules/src/lib.rs new file mode 100644 index 000000000..daa7050eb --- /dev/null +++ b/tests/cyclic-modules/src/lib.rs @@ -0,0 +1,120 @@ +mod typ_a { + pub enum TRec { + T(super::typ_b::T1Rec), + Empty, + } + pub enum T { + T(super::typ_b::T1), + } +} +mod typ_b { + pub enum T1Rec { + T1(Box), + } + pub enum T2Rec { + T2(super::typ_a::TRec), + } + + pub enum T1 { + T1, + } + pub enum T2 { + T2(super::typ_a::T), + } +} + +fn f() {} +mod b { + pub fn g() { + super::f() + } +} +fn h() { + b::g(); + c::i() +} +fn h2() { + c::i() +} +mod c { + pub fn i() {} +} +mod d { + pub fn d1() {} + pub fn d2() { + super::de::de1() + } +} +mod e { + pub fn e1() { + super::d::d1() + } +} +mod de { + pub fn de1() { + super::e::e1() + } +} + +mod rec { + enum T { + t1, + t2, + } + pub fn g1(x: T) -> T { + match x { + T::t1 => g2(x), + T::t2 => T::t1, + } + } + pub fn g2(x: T) -> T { + match x { + T::t1 => g1(x), + T::t2 => hf(x), + } + } + pub fn hf(x: T) -> T { + match x { + T::t1 => hf(T::t2), + T::t2 => x, + } + } +} + +mod rec1_same_name { + pub fn f(x: i32) -> i32 { + super::rec2_same_name::f(x) + } +} +mod rec2_same_name { + pub fn f(x: i32) -> i32 { + if x > 0 { + super::rec1_same_name::f(x - 1) + } else { + 0 + } + } +} +mod enums_a { + pub enum T { + A, + B, + C(Vec), + D(Vec), + } +} +mod enums_b { + pub enum U { + A, + B, + C(Vec), + } + pub enum T { + A, + B, + C(Vec), + } + pub fn f() -> T { + T::A + } +}