Merge pull request #797 from hacspec/fix-potentially-looping-predicat…

…e-id Fix potentially looping predicate_id.
hacspec · Jul 24, 2024 · 3ddbf4b · 3ddbf4b
2 parents cd6e258 + 94124d2
commit 3ddbf4b
Show file tree

Hide file tree

Showing 4 changed files with 11,767 additions and 4 deletions.
diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs
@@ -8,11 +8,13 @@ pub enum ImplExprPathChunk {
     AssocItem {
         item: AssocItem,
         predicate: Binder<TraitPredicate>,
+        #[value(predicate.predicate_id(tcx))]
         predicate_id: PredicateId,
         index: usize,
     },
     Parent {
         predicate: Binder<TraitPredicate>,
+        #[value(predicate.predicate_id(tcx))]
         predicate_id: PredicateId,
         index: usize,
     },
@@ -92,12 +94,10 @@ pub mod rustc {
             AssocItem {
                 item: AssocItem,
                 predicate: PolyTraitPredicate<'tcx>,
-                predicate_id: PredicateId,
                 index: usize,
             },
             Parent {
                 predicate: PolyTraitPredicate<'tcx>,
-                predicate_id: PredicateId,
                 index: usize,
             },
         }
@@ -229,7 +229,6 @@ pub mod rustc {
                             cons(
                                 PathChunk::Parent {
                                     predicate: p,
-                                    predicate_id: p.predicate_id(s),
                                     index,
                                 },
                                 path,
@@ -246,7 +245,6 @@ pub mod rustc {
                                         cons(
                                             PathChunk::AssocItem {
                                                 item,
-                                                predicate_id: p.predicate_id(s),
                                                 predicate: p,
                                                 index,
                                             },

diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap
@@ -26,6 +26,26 @@ exit = 0
 diagnostics = []
 
 [stdout.files]
+"Traits.Block_size.fst" = '''
+module Traits.Block_size
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+class t_BlockSizeUser (v_Self: Type0) = { f_BlockSize:Type0 }
+
+class t_ParBlocksSizeUser (v_Self: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_10960599340086055385:t_BlockSizeUser v_Self
+}
+
+class t_BlockBackend (v_Self: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_15949286759387124191:t_ParBlocksSizeUser v_Self;
+  f_proc_block_pre:Alloc.Vec.t_Vec _ Alloc.Alloc.t_Global -> bool;
+  f_proc_block_post:Alloc.Vec.t_Vec _ Alloc.Alloc.t_Global -> Prims.unit -> bool;
+  f_proc_block:x0: Alloc.Vec.t_Vec _ Alloc.Alloc.t_Global
+    -> Prims.Pure Prims.unit (f_proc_block_pre x0) (fun result -> f_proc_block_post x0 result)
+}
+'''
 "Traits.For_clauses.Issue_495_.Minimized_3_.fst" = '''
 module Traits.For_clauses.Issue_495_.Minimized_3_
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"