Merge pull request #1030 from hacspec/avoid-bundling-use-items

Avoid bundling use items.
cryspen · Oct 24, 2024 · 00c7853 · 00c7853
2 parents f5550da + cf39d49
commit 00c7853
Show file tree

Hide file tree

Showing 2 changed files with 33 additions and 26 deletions.
diff --git a/engine/lib/dependencies.ml b/engine/lib/dependencies.ml
@@ -393,7 +393,16 @@ module Make (F : Features.T) = struct
     in
     let mut_rec_bundles =
       let mod_graph_cycles = ModGraph.of_items items |> ModGraph.cycles in
-      let bundles = ItemGraph.CyclicDep.of_mod_sccs items mod_graph_cycles in
+      (* `Use` items shouldn't be bundled as they have no dependencies
+          and they have dummy names. *)
+      let non_use_items =
+        List.filter
+          ~f:(fun item -> match item.v with Use _ -> false | _ -> true)
+          items
+      in
+      let bundles =
+        ItemGraph.CyclicDep.of_mod_sccs non_use_items mod_graph_cycles
+      in
       let f = List.filter_map ~f:from_ident in
       List.map ~f bundles
     in

diff --git a/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap b/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap
@@ -32,7 +32,7 @@ module Cyclic_modules.B
 open Core
 open FStar.Mul
 
-include Cyclic_modules.Rec_bundle_194616565 {g as g}
+include Cyclic_modules.Rec_bundle_805309848 {g as g}
 '''
 "Cyclic_modules.C.fst" = '''
 module Cyclic_modules.C
@@ -272,8 +272,8 @@ open FStar.Mul
 
 include Cyclic_modules.Rec1_same_name.Rec_bundle_213192514 {f91805216 as f}
 '''
-"Cyclic_modules.Rec_bundle_194616565.fst" = '''
-module Cyclic_modules.Rec_bundle_194616565
+"Cyclic_modules.Rec_bundle_805309848.fst" = '''
+module Cyclic_modules.Rec_bundle_805309848
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 open Core
 open FStar.Mul
@@ -356,45 +356,43 @@ module Cyclic_modules
 open Core
 open FStar.Mul
 
-include Cyclic_modules.Rec_bundle_194616565 {v_DUMMY as v_DUMMY}
+include Cyclic_modules.Rec_bundle_805309848 {b as b}
 
-include Cyclic_modules.Rec_bundle_194616565 {b as b}
+include Cyclic_modules.Rec_bundle_805309848 {c as c}
 
-include Cyclic_modules.Rec_bundle_194616565 {c as c}
+include Cyclic_modules.Rec_bundle_805309848 {d as d}
 
-include Cyclic_modules.Rec_bundle_194616565 {d as d}
+include Cyclic_modules.Rec_bundle_805309848 {de as de}
 
-include Cyclic_modules.Rec_bundle_194616565 {de as de}
+include Cyclic_modules.Rec_bundle_805309848 {disjoint_cycle_a as disjoint_cycle_a}
 
-include Cyclic_modules.Rec_bundle_194616565 {disjoint_cycle_a as disjoint_cycle_a}
+include Cyclic_modules.Rec_bundle_805309848 {disjoint_cycle_b as disjoint_cycle_b}
 
-include Cyclic_modules.Rec_bundle_194616565 {disjoint_cycle_b as disjoint_cycle_b}
+include Cyclic_modules.Rec_bundle_805309848 {e as e}
 
-include Cyclic_modules.Rec_bundle_194616565 {e as e}
+include Cyclic_modules.Rec_bundle_805309848 {enums_a as enums_a}
 
-include Cyclic_modules.Rec_bundle_194616565 {enums_a as enums_a}
+include Cyclic_modules.Rec_bundle_805309848 {enums_b as enums_b}
 
-include Cyclic_modules.Rec_bundle_194616565 {enums_b as enums_b}
+include Cyclic_modules.Rec_bundle_805309848 {m1 as m1}
 
-include Cyclic_modules.Rec_bundle_194616565 {m1 as m1}
+include Cyclic_modules.Rec_bundle_805309848 {m2 as m2}
 
-include Cyclic_modules.Rec_bundle_194616565 {m2 as m2}
+include Cyclic_modules.Rec_bundle_805309848 {v_rec as v_rec}
 
-include Cyclic_modules.Rec_bundle_194616565 {v_rec as v_rec}
+include Cyclic_modules.Rec_bundle_805309848 {rec1_same_name as rec1_same_name}
 
-include Cyclic_modules.Rec_bundle_194616565 {rec1_same_name as rec1_same_name}
+include Cyclic_modules.Rec_bundle_805309848 {rec2_same_name as rec2_same_name}
 
-include Cyclic_modules.Rec_bundle_194616565 {rec2_same_name as rec2_same_name}
+include Cyclic_modules.Rec_bundle_805309848 {std as std}
 
-include Cyclic_modules.Rec_bundle_194616565 {std as std}
+include Cyclic_modules.Rec_bundle_805309848 {typ_a as typ_a}
 
-include Cyclic_modules.Rec_bundle_194616565 {typ_a as typ_a}
+include Cyclic_modules.Rec_bundle_805309848 {typ_b as typ_b}
 
-include Cyclic_modules.Rec_bundle_194616565 {typ_b as typ_b}
+include Cyclic_modules.Rec_bundle_805309848 {f as f}
 
-include Cyclic_modules.Rec_bundle_194616565 {f as f}
+include Cyclic_modules.Rec_bundle_805309848 {h as h}
 
-include Cyclic_modules.Rec_bundle_194616565 {h as h}
-
-include Cyclic_modules.Rec_bundle_194616565 {h2 as h2}
+include Cyclic_modules.Rec_bundle_805309848 {h2 as h2}
 '''