Merge pull request #339 from Nadrieril/update-charon

AeneasVerif · Sep 13, 2024 · 23eb092 · 23eb092
2 parents 2987538 + 510ca30
commit 23eb092
Show file tree

Hide file tree

Showing 35 changed files with 232 additions and 271 deletions.
diff --git a/charon-pin b/charon-pin
@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-35736f4af7185e3a1cdf5b296faffec665b8a14f
+82938d10c82d07b24d25de3357c4d3b357382edf
diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml
@@ -36,7 +36,7 @@ let filter_drop_assigns (f : fun_decl) : fun_decl =
         | Drop p1, Assign (p2, _) ->
             if p1 = p2 then (self#visit_statement env st2).content
             else super#visit_Sequence env st1 st2
-        | Drop p1, Sequence ({ content = Assign (p2, _); span = _ }, _) ->
+        | Drop p1, Sequence ({ content = Assign (p2, _); _ }, _) ->
             if p1 = p2 then (self#visit_statement env st2).content
             else super#visit_Sequence env st1 st2
         | _ -> super#visit_Sequence env st1 st2

diff --git a/compiler/Pure.ml b/compiler/Pure.ml
@@ -198,12 +198,6 @@ class ['self] iter_ty_base =
   object (_self : 'self)
     inherit [_] iter_type_id
     inherit! [_] T.iter_const_generic
-    method visit_type_var_id : 'env -> type_var_id -> unit = fun _ _ -> ()
-    method visit_trait_decl_id : 'env -> trait_decl_id -> unit = fun _ _ -> ()
-    method visit_trait_impl_id : 'env -> trait_impl_id -> unit = fun _ _ -> ()
-
-    method visit_trait_clause_id : 'env -> trait_clause_id -> unit =
-      fun _ _ -> ()
 
     method visit_trait_item_name : 'env -> trait_item_name -> unit =
       fun _ _ -> ()
@@ -214,16 +208,6 @@ class ['self] map_ty_base =
   object (_self : 'self)
     inherit [_] map_type_id
     inherit! [_] T.map_const_generic
-    method visit_type_var_id : 'env -> type_var_id -> type_var_id = fun _ x -> x
-
-    method visit_trait_decl_id : 'env -> trait_decl_id -> trait_decl_id =
-      fun _ x -> x
-
-    method visit_trait_impl_id : 'env -> trait_impl_id -> trait_impl_id =
-      fun _ x -> x
-
-    method visit_trait_clause_id : 'env -> trait_clause_id -> trait_clause_id =
-      fun _ x -> x
 
     method visit_trait_item_name : 'env -> trait_item_name -> trait_item_name =
       fun _ x -> x
@@ -234,16 +218,6 @@ class virtual ['self] reduce_ty_base =
   object (self : 'self)
     inherit [_] reduce_type_id
     inherit! [_] T.reduce_const_generic
-    method visit_type_var_id : 'env -> type_var_id -> 'a = fun _ _ -> self#zero
-
-    method visit_trait_decl_id : 'env -> trait_decl_id -> 'a =
-      fun _ _ -> self#zero
-
-    method visit_trait_impl_id : 'env -> trait_impl_id -> 'a =
-      fun _ _ -> self#zero
-
-    method visit_trait_clause_id : 'env -> trait_clause_id -> 'a =
-      fun _ _ -> self#zero
 
     method visit_trait_item_name : 'env -> trait_item_name -> 'a =
       fun _ _ -> self#zero
@@ -255,19 +229,6 @@ class virtual ['self] mapreduce_ty_base =
     inherit [_] mapreduce_type_id
     inherit! [_] T.mapreduce_const_generic
 
-    method visit_type_var_id : 'env -> type_var_id -> type_var_id * 'a =
-      fun _ x -> (x, self#zero)
-
-    method visit_trait_decl_id : 'env -> trait_decl_id -> trait_decl_id * 'a =
-      fun _ x -> (x, self#zero)
-
-    method visit_trait_impl_id : 'env -> trait_impl_id -> trait_impl_id * 'a =
-      fun _ x -> (x, self#zero)
-
-    method visit_trait_clause_id
-        : 'env -> trait_clause_id -> trait_clause_id * 'a =
-      fun _ x -> (x, self#zero)
-
     method visit_trait_item_name
         : 'env -> trait_item_name -> trait_item_name * 'a =
       fun _ x -> (x, self#zero)

diff --git a/flake.lock b/flake.lock
diff --git a/tests/coq/arrays/Arrays.v b/tests/coq/arrays/Arrays.v
@@ -371,7 +371,7 @@ Definition non_copyable_array : result unit :=
 .
 
 (** [arrays::sum]: loop 0:
-    Source: 'tests/src/arrays.rs', lines 247:4-253:1 *)
+    Source: 'tests/src/arrays.rs', lines 248:4-251:5 *)
 Fixpoint sum_loop
   (n : nat) (s : slice u32) (sum1 : u32) (i : usize) : result u32 :=
   match n with
@@ -395,7 +395,7 @@ Definition sum (n : nat) (s : slice u32) : result u32 :=
 .
 
 (** [arrays::sum2]: loop 0:
-    Source: 'tests/src/arrays.rs', lines 258:4-264:1 *)
+    Source: 'tests/src/arrays.rs', lines 259:4-262:5 *)
 Fixpoint sum2_loop
   (n : nat) (s : slice u32) (s2 : slice u32) (sum1 : u32) (i : usize) :
   result u32
@@ -498,7 +498,7 @@ Definition ite : result unit :=
 .
 
 (** [arrays::zero_slice]: loop 0:
-    Source: 'tests/src/arrays.rs', lines 308:4-313:1 *)
+    Source: 'tests/src/arrays.rs', lines 309:4-312:5 *)
 Fixpoint zero_slice_loop
   (n : nat) (a : slice u8) (i : usize) (len : usize) : result (slice u8) :=
   match n with
@@ -522,7 +522,7 @@ Definition zero_slice (n : nat) (a : slice u8) : result (slice u8) :=
 .
 
 (** [arrays::iter_mut_slice]: loop 0:
-    Source: 'tests/src/arrays.rs', lines 317:4-321:1 *)
+    Source: 'tests/src/arrays.rs', lines 318:4-320:5 *)
 Fixpoint iter_mut_slice_loop
   (n : nat) (len : usize) (i : usize) : result unit :=
   match n with
@@ -541,7 +541,7 @@ Definition iter_mut_slice (n : nat) (a : slice u8) : result (slice u8) :=
 .
 
 (** [arrays::sum_mut_slice]: loop 0:
-    Source: 'tests/src/arrays.rs', lines 325:4-331:1 *)
+    Source: 'tests/src/arrays.rs', lines 326:4-329:5 *)
 Fixpoint sum_mut_slice_loop
   (n : nat) (a : slice u32) (i : usize) (s : u32) : result u32 :=
   match n with

diff --git a/tests/coq/betree/Betree_Funs.v b/tests/coq/betree/Betree_Funs.v
@@ -89,7 +89,7 @@ Definition betree_upsert_update
 .
 
 (** [betree::betree::{betree::betree::List<T>}#1::len]: loop 0:
-    Source: 'src/betree.rs', lines 278:8-284:5 *)
+    Source: 'src/betree.rs', lines 279:8-282:9 *)
 Fixpoint betree_List_len_loop
   {T : Type} (n : nat) (self : betree_List_t T) (len : u64) : result u64 :=
   match n with
@@ -111,7 +111,7 @@ Definition betree_List_len
 .
 
 (** [betree::betree::{betree::betree::List<T>}#1::reverse]: loop 0:
-    Source: 'src/betree.rs', lines 305:8-312:5 *)
+    Source: 'src/betree.rs', lines 306:8-310:9 *)
 Fixpoint betree_List_reverse_loop
   {T : Type} (n : nat) (self : betree_List_t T) (out : betree_List_t T) :
   result (betree_List_t T)
@@ -135,7 +135,7 @@ Definition betree_List_reverse
 .
 
 (** [betree::betree::{betree::betree::List<T>}#1::split_at]: loop 0:
-    Source: 'src/betree.rs', lines 289:8-302:5 *)
+    Source: 'src/betree.rs', lines 290:8-300:9 *)
 Fixpoint betree_List_split_at_loop
   {T : Type} (n : nat) (n1 : u64) (beg : betree_List_t T)
   (self : betree_List_t T) :
@@ -204,7 +204,7 @@ Definition betree_ListPairU64T_head_has_key
 .
 
 (** [betree::betree::{betree::betree::List<(u64, T)>}#2::partition_at_pivot]: loop 0:
-    Source: 'src/betree.rs', lines 358:8-370:5 *)
+    Source: 'src/betree.rs', lines 359:8-368:9 *)
 Fixpoint betree_ListPairU64T_partition_at_pivot_loop
   {T : Type} (n : nat) (pivot : u64) (beg : betree_List_t (u64 * T))
   (end1 : betree_List_t (u64 * T)) (self : betree_List_t (u64 * T)) :
@@ -276,7 +276,7 @@ Definition betree_Leaf_split
 .
 
 (** [betree::betree::{betree::betree::Node}#5::lookup_first_message_for_key]: loop 0:
-    Source: 'src/betree.rs', lines 792:4-810:5 *)
+    Source: 'src/betree.rs', lines 796:8-810:5 *)
 Fixpoint betree_Node_lookup_first_message_for_key_loop
   (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
   result ((betree_List_t (u64 * betree_Message_t)) * (betree_List_t (u64 *
@@ -313,7 +313,7 @@ Definition betree_Node_lookup_first_message_for_key
 .
 
 (** [betree::betree::{betree::betree::Node}#5::apply_upserts]: loop 0:
-    Source: 'src/betree.rs', lines 820:4-844:5 *)
+    Source: 'src/betree.rs', lines 821:8-838:9 *)
 Fixpoint betree_Node_apply_upserts_loop
   (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (prev : option u64)
   (key : u64) :
@@ -353,7 +353,7 @@ Definition betree_Node_apply_upserts
 .
 
 (** [betree::betree::{betree::betree::Node}#5::lookup_in_bindings]: loop 0:
-    Source: 'src/betree.rs', lines 649:4-660:5 *)
+    Source: 'src/betree.rs', lines 650:8-660:5 *)
 Fixpoint betree_Node_lookup_in_bindings_loop
   (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) :
   result (option u64)
@@ -476,7 +476,7 @@ with betree_Node_lookup
 .
 
 (** [betree::betree::{betree::betree::Node}#5::filter_messages_for_key]: loop 0:
-    Source: 'src/betree.rs', lines 683:4-692:5 *)
+    Source: 'src/betree.rs', lines 684:8-691:9 *)
 Fixpoint betree_Node_filter_messages_for_key_loop
   (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
   result (betree_List_t (u64 * betree_Message_t))
@@ -508,7 +508,7 @@ Definition betree_Node_filter_messages_for_key
 .
 
 (** [betree::betree::{betree::betree::Node}#5::lookup_first_message_after_key]: loop 0:
-    Source: 'src/betree.rs', lines 694:4-706:5 *)
+    Source: 'src/betree.rs', lines 698:8-704:9 *)
 Fixpoint betree_Node_lookup_first_message_after_key_loop
   (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
   result ((betree_List_t (u64 * betree_Message_t)) * (betree_List_t (u64 *
@@ -595,7 +595,7 @@ Definition betree_Node_apply_to_internal
 .
 
 (** [betree::betree::{betree::betree::Node}#5::apply_messages_to_internal]: loop 0:
-    Source: 'src/betree.rs', lines 518:4-526:5 *)
+    Source: 'src/betree.rs', lines 522:8-525:9 *)
 Fixpoint betree_Node_apply_messages_to_internal_loop
   (n : nat) (msgs : betree_List_t (u64 * betree_Message_t))
   (new_msgs : betree_List_t (u64 * betree_Message_t)) :
@@ -625,7 +625,7 @@ Definition betree_Node_apply_messages_to_internal
 .
 
 (** [betree::betree::{betree::betree::Node}#5::lookup_mut_in_bindings]: loop 0:
-    Source: 'src/betree.rs', lines 664:4-677:5 *)
+    Source: 'src/betree.rs', lines 668:8-675:9 *)
 Fixpoint betree_Node_lookup_mut_in_bindings_loop
   (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) :
   result ((betree_List_t (u64 * u64)) * (betree_List_t (u64 * u64) -> result
@@ -700,7 +700,7 @@ Definition betree_Node_apply_to_leaf
 .
 
 (** [betree::betree::{betree::betree::Node}#5::apply_messages_to_leaf]: loop 0:
-    Source: 'src/betree.rs', lines 463:4-471:5 *)
+    Source: 'src/betree.rs', lines 467:8-470:9 *)
 Fixpoint betree_Node_apply_messages_to_leaf_loop
   (n : nat) (bindings : betree_List_t (u64 * u64))
   (new_msgs : betree_List_t (u64 * betree_Message_t)) :

diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v
@@ -65,7 +65,7 @@ Fixpoint list_nth {T : Type} (n : nat) (l : CList_t T) (i : u32) : result T :=
 .
 
 (** [demo::list_nth1]: loop 0:
-    Source: 'tests/src/demo.rs', lines 56:0-65:1 *)
+    Source: 'tests/src/demo.rs', lines 57:4-65:1 *)
 Fixpoint list_nth1_loop
   {T : Type} (n : nat) (l : CList_t T) (i : u32) : result T :=
   match n with

diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
@@ -18,7 +18,7 @@ Definition hash_key (k : usize) : result usize :=
   Ok k.
 
 (** [hashmap::{hashmap::HashMap<T>}::allocate_slots]: loop 0:
-    Source: 'tests/src/hashmap.rs', lines 63:4-69:5 *)
+    Source: 'tests/src/hashmap.rs', lines 64:8-67:9 *)
 Fixpoint hashMap_allocate_slots_loop
   {T : Type} (n : nat) (slots : alloc_vec_Vec (AList_t T)) (n1 : usize) :
   result (alloc_vec_Vec (AList_t T))
@@ -71,7 +71,7 @@ Definition hashMap_new (T : Type) (n : nat) : result (HashMap_t T) :=
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::clear]: loop 0:
-    Source: 'tests/src/hashmap.rs', lines 97:8-102:5 *)
+    Source: 'tests/src/hashmap.rs', lines 98:8-101:9 *)
 Fixpoint hashMap_clear_loop
   {T : Type} (n : nat) (slots : alloc_vec_Vec (AList_t T)) (i : usize) :
   result (alloc_vec_Vec (AList_t T))
@@ -115,7 +115,7 @@ Definition hashMap_len {T : Type} (self : HashMap_t T) : result usize :=
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::insert_in_list]: loop 0:
-    Source: 'tests/src/hashmap.rs', lines 111:4-128:5 *)
+    Source: 'tests/src/hashmap.rs', lines 1:0-127:9 *)
 Fixpoint hashMap_insert_in_list_loop
   {T : Type} (n : nat) (key : usize) (value : T) (ls : AList_t T) :
   result (bool * (AList_t T))
@@ -185,7 +185,7 @@ Definition hashMap_insert_no_resize
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::move_elements_from_list]: loop 0:
-    Source: 'tests/src/hashmap.rs', lines 194:4-207:5 *)
+    Source: 'tests/src/hashmap.rs', lines 197:12-204:17 *)
 Fixpoint hashMap_move_elements_from_list_loop
   {T : Type} (n : nat) (ntable : HashMap_t T) (ls : AList_t T) :
   result (HashMap_t T)
@@ -212,7 +212,7 @@ Definition hashMap_move_elements_from_list
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::move_elements]: loop 0:
-    Source: 'tests/src/hashmap.rs', lines 182:8-191:5 *)
+    Source: 'tests/src/hashmap.rs', lines 183:8-190:9 *)
 Fixpoint hashMap_move_elements_loop
   {T : Type} (n : nat) (ntable : HashMap_t T)
   (slots : alloc_vec_Vec (AList_t T)) (i : usize) :
@@ -313,7 +313,7 @@ Definition hashMap_insert
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
-    Source: 'tests/src/hashmap.rs', lines 217:4-230:5 *)
+    Source: 'tests/src/hashmap.rs', lines 1:0-229:9 *)
 Fixpoint hashMap_contains_key_in_list_loop
   {T : Type} (n : nat) (key : usize) (ls : AList_t T) : result bool :=
   match n with
@@ -350,7 +350,7 @@ Definition hashMap_contains_key
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::get_in_list]: loop 0:
-    Source: 'tests/src/hashmap.rs', lines 235:4-248:5 *)
+    Source: 'tests/src/hashmap.rs', lines 236:8-248:5 *)
 Fixpoint hashMap_get_in_list_loop
   {T : Type} (n : nat) (key : usize) (ls : AList_t T) : result T :=
   match n with
@@ -385,7 +385,7 @@ Definition hashMap_get
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::get_mut_in_list]: loop 0:
-    Source: 'tests/src/hashmap.rs', lines 256:4-265:5 *)
+    Source: 'tests/src/hashmap.rs', lines 257:8-265:5 *)
 Fixpoint hashMap_get_mut_in_list_loop
   {T : Type} (n : nat) (ls : AList_t T) (key : usize) :
   result (T * (T -> result (AList_t T)))
@@ -450,7 +450,7 @@ Definition hashMap_get_mut
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::remove_from_list]: loop 0:
-    Source: 'tests/src/hashmap.rs', lines 276:4-302:5 *)
+    Source: 'tests/src/hashmap.rs', lines 1:0-299:17 *)
 Fixpoint hashMap_remove_from_list_loop
   {T : Type} (n : nat) (key : usize) (ls : AList_t T) :
   result ((option T) * (AList_t T))

diff --git a/tests/coq/misc/InfiniteLoop.v b/tests/coq/misc/InfiniteLoop.v
@@ -14,7 +14,7 @@ Definition bar : result unit :=
   Ok tt.
 
 (** [infinite_loop::foo]: loop 0:
-    Source: 'tests/src/infinite-loop.rs', lines 6:0-10:1 *)
+    Source: 'tests/src/infinite-loop.rs', lines 8:8-8:13 *)
 Fixpoint foo_loop (n : nat) : result unit :=
   match n with | O => Fail_ OutOfFuel | S n1 => _ <- bar; foo_loop n1 end
 .