Merge pull request #1209 from hacspec/descendant-attributes-dependencies

fix(engine) Check attributes of descendants to build dependency graph.
hacspec · Dec 24, 2024 · 8666252 · 8666252
2 parents e40b7d4 + bd7f35b
commit 8666252
Show file tree

Hide file tree

Showing 3 changed files with 34 additions and 26 deletions.
diff --git a/engine/lib/ast_utils.ml b/engine/lib/ast_utils.ml
@@ -655,6 +655,13 @@ module Make (F : Features.T) = struct
               self#zero
           | _ -> super#visit_expr' () e
       end
+
+    let collect_attrs =
+      object (_self)
+        inherit [_] Visitors.reduce
+        inherit [_] expr_list_monoid
+        method! visit_attrs () attrs = attrs
+      end
   end
 
   (** Produces a local identifier which is locally fresh **with respect

diff --git a/engine/lib/dependencies.ml b/engine/lib/dependencies.ml
@@ -88,8 +88,9 @@ module Make (F : Features.T) = struct
         =
       List.concat_map
         ~f:(fun i ->
+          let attrs = U.Reducers.collect_attrs#visit_item () i in
           let assoc =
-            uid_associated_items i.attrs |> List.map ~f:(fun i -> i.ident)
+            uid_associated_items attrs |> List.map ~f:(fun i -> i.ident)
           in
           vertices_of_item i @ assoc |> List.map ~f:(Fn.const i.ident &&& Fn.id))
         items

diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
@@ -130,12 +130,12 @@ module Attributes.Newtype_pattern
 open Core
 open FStar.Mul
 
+let v_MAX: usize = sz 10
+
 type t_SafeIndex = { f_i:f_i: usize{f_i <. v_MAX} }
 
 let impl__SafeIndex__as_usize (self: t_SafeIndex) : usize = self.f_i
 
-let v_MAX: usize = sz 10
-
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl_1 (#v_T: Type0) : Core.Ops.Index.t_Index (t_Array v_T (sz 10)) t_SafeIndex =
   {
@@ -156,6 +156,23 @@ module Attributes.Pre_post_on_traits_and_impls
 open Core
 open FStar.Mul
 
+type t_ViaAdd = | ViaAdd : t_ViaAdd
+
+type t_ViaMul = | ViaMul : t_ViaMul
+
+class t_TraitWithRequiresAndEnsures (v_Self: Type0) = {
+  f_method_pre:self___: v_Self -> x: u8 -> pred: Type0{x <. 100uy ==> pred};
+  f_method_post:self___: v_Self -> x: u8 -> r: u8 -> pred: Type0{pred ==> r >. 88uy};
+  f_method:x0: v_Self -> x1: u8
+    -> Prims.Pure u8 (f_method_pre x0 x1) (fun result -> f_method_post x0 x1 result)
+}
+
+let test
+      (#v_T: Type0)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_TraitWithRequiresAndEnsures v_T)
+      (x: v_T)
+    : u8 = (f_method #v_T #FStar.Tactics.Typeclasses.solve x 99uy <: u8) -! 88uy
+
 class t_Operation (v_Self: Type0) = {
   f_double_pre:x: u8
     -> pred:
@@ -174,17 +191,6 @@ class t_Operation (v_Self: Type0) = {
   f_double:x0: u8 -> Prims.Pure u8 (f_double_pre x0) (fun result -> f_double_post x0 result)
 }
 
-class t_TraitWithRequiresAndEnsures (v_Self: Type0) = {
-  f_method_pre:self___: v_Self -> x: u8 -> pred: Type0{x <. 100uy ==> pred};
-  f_method_post:self___: v_Self -> x: u8 -> r: u8 -> pred: Type0{pred ==> r >. 88uy};
-  f_method:x0: v_Self -> x1: u8
-    -> Prims.Pure u8 (f_method_pre x0 x1) (fun result -> f_method_post x0 x1 result)
-}
-
-type t_ViaAdd = | ViaAdd : t_ViaAdd
-
-type t_ViaMul = | ViaMul : t_ViaMul
-
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl: t_Operation t_ViaAdd =
   {
@@ -218,12 +224,6 @@ let impl_1: t_Operation t_ViaMul =
         (Rust_primitives.Hax.Int.from_machine result <: Hax_lib.Int.t_Int));
     f_double = fun (x: u8) -> x *! 2uy
   }
-
-let test
-      (#v_T: Type0)
-      (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_TraitWithRequiresAndEnsures v_T)
-      (x: v_T)
-    : u8 = (f_method #v_T #FStar.Tactics.Typeclasses.solve x 99uy <: u8) -! 88uy
 '''
 "Attributes.Refined_arithmetic.fst" = '''
 module Attributes.Refined_arithmetic
@@ -466,12 +466,6 @@ module Attributes
 open Core
 open FStar.Mul
 
-type t_Foo = {
-  f_x:u32;
-  f_y:f_y: u32{f_y >. 3ul};
-  f_z:f_z: u32{((f_y +! f_x <: u32) +! f_z <: u32) >. 3ul}
-}
-
 let inlined_code__V: u8 = 12uy
 
 let issue_844_ (v__x: u8)
@@ -484,6 +478,12 @@ let issue_844_ (v__x: u8)
 
 let u32_max: u32 = 90000ul
 
+type t_Foo = {
+  f_x:u32;
+  f_y:f_y: u32{f_y >. 3ul};
+  f_z:f_z: u32{((f_y +! f_x <: u32) +! f_z <: u32) >. 3ul}
+}
+
 let swap_and_mut_req_ens (x y: u32)
     : Prims.Pure (u32 & u32 & u32)
       (requires x <. 40ul && y <. 300ul)