Change rc_copy_alloc_id to do the cast.

examples/intptr.c

@@ -97,8 +97,8 @@ int* roundtrip2(int* p){
 [[rc::returns("p @ &own<n @ int<i32>>")]]
 int* roundtrip3(int* p){
   uintptr_t i = (uintptr_t) p;
-  int *q = (void*) (i + 0); // ← The provenance is lost here.
-  return rc_copy_alloc_id(q, p); // ← Copy provenance from [p].
+  uintptr_t k = i + 0; // ← The provenance is lost here.
+  return rc_copy_alloc_id(k, p); // ← Copy provenance from [p].
 }
 
 // Roundrip cast with flow of ownership.
@@ -118,10 +118,10 @@ int roundtrip_and_read1(int* p){
 [[rc::args("l @ &own<n @ int<i32>>")]]
 [[rc::returns("n @ int<i32>")]]
 [[rc::ensures("own l : n @ int<i32>")]]
-int roundtrip_and_read2(int* p){
+int roundtrip_and_read2(int *p){
   uintptr_t i = (uintptr_t) p;
-  int *q = (int*) (i * 1);
-  q = rc_copy_alloc_id(q, p);
+  uintptr_t j = i * 1;
+  int *q = (int*) rc_copy_alloc_id(j, p);
   int r = *q;
   return r;
 }
@@ -131,9 +131,9 @@ int roundtrip_and_read2(int* p){
 [[rc::args("p @ &own<n @ int<i32>>")]]
 [[rc::returns("n @ int<i32>")]]
 [[rc::ensures("own p : n @ int<i32>")]]
-int roundtrip_and_read3(int* p){
+int roundtrip_and_read3(int *p){
   uintptr_t i = (uintptr_t) p;
-  int *q = rc_copy_alloc_id((int*) (i * 1), p);
+  int *q = (int*) rc_copy_alloc_id(i * 1, p);
   return *q;
 }
 
@@ -144,17 +144,7 @@ int roundtrip_and_read3(int* p){
 [[rc::ensures("own p : n @ int<i32>")]]
 int roundtrip_and_read4(int* p){
   uintptr_t i = (uintptr_t) p;
-  int *q = (int*) (i * 1);
-  return *(rc_copy_alloc_id(q, p));
-}
-
-// Copy the provenance from an int.
-[[rc::parameters("p : loc")]]
-[[rc::args("p @ intptr<uintptr_t>")]]
-[[rc::requires("[alloc_alive_loc p]", "[loc_in_bounds p 0]")]] // TODO: get rid of the loc_in_bounds sidecondition
-[[rc::returns("p @ &own<place<p>>")]]
-[[rc::ensures("[alloc_alive_loc p]")]]
-void* int_to_ptr(uintptr_t p){
-  void *q = (void*) (p * 1);
-  return (rc_copy_alloc_id(q, p));
+  uintptr_t j = i * 1;
+  int *q = (int*) rc_copy_alloc_id(j, p);
+  return *q;
 }

examples/proofs/intptr/generated_proof_int_to_ptr.v

-From refinedc.typing Require Import typing.
-From refinedc.examples.intptr Require Import generated_code.
-From refinedc.examples.intptr Require Import generated_spec.
-Set Default Proof Using "Type".
-
-(* Generated from [examples/intptr.c]. *)
-Section proof_int_to_ptr.
-  Context `{!typeG Σ} `{!globalG Σ}.
-
-  (* Typing proof for [int_to_ptr]. *)
-  Lemma type_int_to_ptr :
-    ⊢ typed_function impl_int_to_ptr type_of_int_to_ptr.
-  Proof.
-    Open Scope printing_sugar.
-    start_function "int_to_ptr" (p) => arg_p local_q.
-    split_blocks ((
-      ∅
-    )%I : gmap label (iProp Σ)) ((
-      ∅
-    )%I : gmap label (iProp Σ)).
-    - repeat liRStep; liShow.
-      all: print_typesystem_goal "int_to_ptr" "#0".
-    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
-    all: print_sidecondition_goal "int_to_ptr".
-  Qed.
-End proof_int_to_ptr.

examples/proofs/intptr/generated_proof_roundtrip3.v

@@ -12,7 +12,7 @@ Section proof_roundtrip3.
     ⊢ typed_function impl_roundtrip3 type_of_roundtrip3.
   Proof.
     Open Scope printing_sugar.
-    start_function "roundtrip3" ([p n]) => arg_p local_i local_q.
+    start_function "roundtrip3" ([p n]) => arg_p local_i local_k.
     split_blocks ((
       ∅
     )%I : gmap label (iProp Σ)) ((

examples/proofs/intptr/generated_proof_roundtrip_and_read2.v

@@ -12,7 +12,7 @@ Section proof_roundtrip_and_read2.
     ⊢ typed_function impl_roundtrip_and_read2 type_of_roundtrip_and_read2.
   Proof.
     Open Scope printing_sugar.
-    start_function "roundtrip_and_read2" ([l n]) => arg_p local_i local_r local_q.
+    start_function "roundtrip_and_read2" ([l n]) => arg_p local_i local_r local_q local_j.
     split_blocks ((
       ∅
     )%I : gmap label (iProp Σ)) ((

examples/proofs/intptr/generated_proof_roundtrip_and_read4.v

@@ -12,7 +12,7 @@ Section proof_roundtrip_and_read4.
     ⊢ typed_function impl_roundtrip_and_read4 type_of_roundtrip_and_read4.
   Proof.
     Open Scope printing_sugar.
-    start_function "roundtrip_and_read4" ([p n]) => arg_p local_i local_q.
+    start_function "roundtrip_and_read4" ([p n]) => arg_p local_i local_q local_j.
     split_blocks ((
       ∅
     )%I : gmap label (iProp Σ)) ((

examples/proofs/intptr/generated_spec.v

@@ -73,9 +73,4 @@ Section spec.
   Definition type_of_roundtrip_and_read4 :=
     fn(∀ (p, n) : loc * Z; (p @ (&own (n @ (int (i32))))); True)
       → ∃ () : (), (n @ (int (i32))); (p ◁ₗ (n @ (int (i32)))).
-
-  (* Specifications for function [int_to_ptr]. *)
-  Definition type_of_int_to_ptr :=
-    fn(∀ p : loc; (p @ (intptr (uintptr_t))); (alloc_alive_loc p) ∗ (loc_in_bounds p 0))
-      → ∃ () : (), (p @ (&own (place (p)))); (alloc_alive_loc p).
 End spec.

examples/proofs/intptr/proof_files

 generated_proof_int_ptr1.v
 generated_proof_int_ptr2.v
 generated_proof_int_ptr3.v
-generated_proof_int_to_ptr.v
 generated_proof_min_ptr_val1.v
 generated_proof_min_ptr_val2.v
 generated_proof_roundtrip1.v

examples/proofs/tagged_ptr/generated_code.v

@@ -15,92 +15,90 @@ Section code.
   Definition loc_8 : location_info := LocationInfo file_0 20 28 20 29.
   Definition loc_9 : location_info := LocationInfo file_0 20 33 20 34.
   Definition loc_12 : location_info := LocationInfo file_0 29 2 29 26.
-  Definition loc_13 : location_info := LocationInfo file_0 30 2 30 139.
-  Definition loc_14 : location_info := LocationInfo file_0 30 9 30 138.
+  Definition loc_13 : location_info := LocationInfo file_0 30 2 30 164.
+  Definition loc_14 : location_info := LocationInfo file_0 30 9 30 163.
   Definition loc_15 : location_info := LocationInfo file_0 30 35 30 38.
   Definition loc_16 : location_info := LocationInfo file_0 30 35 30 38.
-  Definition loc_17 : location_info := LocationInfo file_0 30 40 30 77.
-  Definition loc_18 : location_info := LocationInfo file_0 30 49 30 76.
-  Definition loc_19 : location_info := LocationInfo file_0 30 50 30 71.
-  Definition loc_20 : location_info := LocationInfo file_0 30 50 30 63.
-  Definition loc_21 : location_info := LocationInfo file_0 30 62 30 63.
-  Definition loc_22 : location_info := LocationInfo file_0 30 62 30 63.
-  Definition loc_23 : location_info := LocationInfo file_0 30 66 30 71.
-  Definition loc_24 : location_info := LocationInfo file_0 30 66 30 71.
-  Definition loc_25 : location_info := LocationInfo file_0 30 74 30 75.
-  Definition loc_26 : location_info := LocationInfo file_0 30 74 30 75.
-  Definition loc_27 : location_info := LocationInfo file_0 29 16 29 25.
+  Definition loc_17 : location_info := LocationInfo file_0 30 40 30 67.
+  Definition loc_18 : location_info := LocationInfo file_0 30 41 30 62.
+  Definition loc_19 : location_info := LocationInfo file_0 30 41 30 54.
+  Definition loc_20 : location_info := LocationInfo file_0 30 53 30 54.
+  Definition loc_21 : location_info := LocationInfo file_0 30 53 30 54.
+  Definition loc_22 : location_info := LocationInfo file_0 30 57 30 62.
+  Definition loc_23 : location_info := LocationInfo file_0 30 57 30 62.
+  Definition loc_24 : location_info := LocationInfo file_0 30 65 30 66.
+  Definition loc_25 : location_info := LocationInfo file_0 30 65 30 66.
+  Definition loc_26 : location_info := LocationInfo file_0 29 16 29 25.
+  Definition loc_27 : location_info := LocationInfo file_0 29 16 29 22.
   Definition loc_28 : location_info := LocationInfo file_0 29 16 29 22.
-  Definition loc_29 : location_info := LocationInfo file_0 29 16 29 22.
+  Definition loc_29 : location_info := LocationInfo file_0 29 23 29 24.
   Definition loc_30 : location_info := LocationInfo file_0 29 23 29 24.
-  Definition loc_31 : location_info := LocationInfo file_0 29 23 29 24.
-  Definition loc_36 : location_info := LocationInfo file_0 39 2 39 19.
-  Definition loc_37 : location_info := LocationInfo file_0 39 9 39 18.
+  Definition loc_35 : location_info := LocationInfo file_0 39 2 39 19.
+  Definition loc_36 : location_info := LocationInfo file_0 39 9 39 18.
+  Definition loc_37 : location_info := LocationInfo file_0 39 9 39 12.
   Definition loc_38 : location_info := LocationInfo file_0 39 9 39 12.
-  Definition loc_39 : location_info := LocationInfo file_0 39 9 39 12.
+  Definition loc_39 : location_info := LocationInfo file_0 39 13 39 14.
   Definition loc_40 : location_info := LocationInfo file_0 39 13 39 14.
-  Definition loc_41 : location_info := LocationInfo file_0 39 13 39 14.
-  Definition loc_42 : location_info := LocationInfo file_0 39 16 39 17.
-  Definition loc_45 : location_info := LocationInfo file_0 48 2 48 30.
-  Definition loc_46 : location_info := LocationInfo file_0 49 2 49 121.
-  Definition loc_47 : location_info := LocationInfo file_0 49 9 49 120.
+  Definition loc_41 : location_info := LocationInfo file_0 39 16 39 17.
+  Definition loc_44 : location_info := LocationInfo file_0 48 2 48 30.
+  Definition loc_45 : location_info := LocationInfo file_0 49 2 49 137.
+  Definition loc_46 : location_info := LocationInfo file_0 49 9 49 136.
+  Definition loc_47 : location_info := LocationInfo file_0 49 35 49 38.
   Definition loc_48 : location_info := LocationInfo file_0 49 35 49 38.
-  Definition loc_49 : location_info := LocationInfo file_0 49 35 49 38.
-  Definition loc_50 : location_info := LocationInfo file_0 49 40 49 68.
-  Definition loc_51 : location_info := LocationInfo file_0 49 49 49 67.
-  Definition loc_52 : location_info := LocationInfo file_0 49 50 49 51.
-  Definition loc_53 : location_info := LocationInfo file_0 49 50 49 51.
-  Definition loc_54 : location_info := LocationInfo file_0 49 54 49 66.
-  Definition loc_55 : location_info := LocationInfo file_0 49 54 49 55.
-  Definition loc_56 : location_info := LocationInfo file_0 49 54 49 55.
-  Definition loc_57 : location_info := LocationInfo file_0 49 58 49 66.
-  Definition loc_58 : location_info := LocationInfo file_0 49 59 49 60.
-  Definition loc_59 : location_info := LocationInfo file_0 49 64 49 65.
-  Definition loc_60 : location_info := LocationInfo file_0 48 16 48 29.
-  Definition loc_61 : location_info := LocationInfo file_0 48 28 48 29.
-  Definition loc_62 : location_info := LocationInfo file_0 48 28 48 29.
-  Definition loc_67 : location_info := LocationInfo file_0 54 2 54 15.
-  Definition loc_68 : location_info := LocationInfo file_0 56 2 56 24.
-  Definition loc_69 : location_info := LocationInfo file_0 57 2 57 26.
-  Definition loc_70 : location_info := LocationInfo file_0 59 2 59 36.
-  Definition loc_71 : location_info := LocationInfo file_0 60 2 60 13.
-  Definition loc_72 : location_info := LocationInfo file_0 60 9 60 12.
-  Definition loc_73 : location_info := LocationInfo file_0 60 9 60 12.
-  Definition loc_74 : location_info := LocationInfo file_0 60 10 60 12.
-  Definition loc_75 : location_info := LocationInfo file_0 60 10 60 12.
-  Definition loc_76 : location_info := LocationInfo file_0 59 15 59 35.
-  Definition loc_77 : location_info := LocationInfo file_0 59 26 59 35.
-  Definition loc_78 : location_info := LocationInfo file_0 59 26 59 31.
-  Definition loc_79 : location_info := LocationInfo file_0 59 26 59 31.
-  Definition loc_80 : location_info := LocationInfo file_0 59 32 59 34.
-  Definition loc_81 : location_info := LocationInfo file_0 59 32 59 34.
-  Definition loc_84 : location_info := LocationInfo file_0 57 9 57 24.
-  Definition loc_85 : location_info := LocationInfo file_0 57 9 57 19.
-  Definition loc_86 : location_info := LocationInfo file_0 57 9 57 15.
-  Definition loc_87 : location_info := LocationInfo file_0 57 9 57 15.
-  Definition loc_88 : location_info := LocationInfo file_0 57 16 57 18.
-  Definition loc_89 : location_info := LocationInfo file_0 57 16 57 18.
-  Definition loc_90 : location_info := LocationInfo file_0 57 23 57 24.
-  Definition loc_91 : location_info := LocationInfo file_0 56 13 56 23.
-  Definition loc_92 : location_info := LocationInfo file_0 56 13 56 16.
-  Definition loc_93 : location_info := LocationInfo file_0 56 13 56 16.
-  Definition loc_94 : location_info := LocationInfo file_0 56 17 56 19.
-  Definition loc_95 : location_info := LocationInfo file_0 56 18 56 19.
-  Definition loc_96 : location_info := LocationInfo file_0 56 21 56 22.
-  Definition loc_99 : location_info := LocationInfo file_0 54 13 54 14.
-  Definition loc_104 : location_info := LocationInfo file_0 69 2 69 30.
-  Definition loc_105 : location_info := LocationInfo file_0 70 2 70 27.
-  Definition loc_106 : location_info := LocationInfo file_0 70 9 70 26.
-  Definition loc_107 : location_info := LocationInfo file_0 70 9 70 21.
-  Definition loc_108 : location_info := LocationInfo file_0 70 9 70 10.
-  Definition loc_109 : location_info := LocationInfo file_0 70 9 70 10.
-  Definition loc_110 : location_info := LocationInfo file_0 70 13 70 21.
-  Definition loc_111 : location_info := LocationInfo file_0 70 14 70 15.
-  Definition loc_112 : location_info := LocationInfo file_0 70 19 70 20.
-  Definition loc_113 : location_info := LocationInfo file_0 70 25 70 26.
-  Definition loc_114 : location_info := LocationInfo file_0 69 16 69 29.
-  Definition loc_115 : location_info := LocationInfo file_0 69 28 69 29.
-  Definition loc_116 : location_info := LocationInfo file_0 69 28 69 29.
+  Definition loc_49 : location_info := LocationInfo file_0 49 40 49 58.
+  Definition loc_50 : location_info := LocationInfo file_0 49 41 49 42.
+  Definition loc_51 : location_info := LocationInfo file_0 49 41 49 42.
+  Definition loc_52 : location_info := LocationInfo file_0 49 45 49 57.
+  Definition loc_53 : location_info := LocationInfo file_0 49 45 49 46.
+  Definition loc_54 : location_info := LocationInfo file_0 49 45 49 46.
+  Definition loc_55 : location_info := LocationInfo file_0 49 49 49 57.
+  Definition loc_56 : location_info := LocationInfo file_0 49 50 49 51.
+  Definition loc_57 : location_info := LocationInfo file_0 49 55 49 56.
+  Definition loc_58 : location_info := LocationInfo file_0 48 16 48 29.
+  Definition loc_59 : location_info := LocationInfo file_0 48 28 48 29.
+  Definition loc_60 : location_info := LocationInfo file_0 48 28 48 29.
+  Definition loc_65 : location_info := LocationInfo file_0 54 2 54 15.
+  Definition loc_66 : location_info := LocationInfo file_0 56 2 56 24.
+  Definition loc_67 : location_info := LocationInfo file_0 57 2 57 26.
+  Definition loc_68 : location_info := LocationInfo file_0 59 2 59 36.
+  Definition loc_69 : location_info := LocationInfo file_0 60 2 60 13.
+  Definition loc_70 : location_info := LocationInfo file_0 60 9 60 12.
+  Definition loc_71 : location_info := LocationInfo file_0 60 9 60 12.
+  Definition loc_72 : location_info := LocationInfo file_0 60 10 60 12.
+  Definition loc_73 : location_info := LocationInfo file_0 60 10 60 12.
+  Definition loc_74 : location_info := LocationInfo file_0 59 15 59 35.
+  Definition loc_75 : location_info := LocationInfo file_0 59 26 59 35.
+  Definition loc_76 : location_info := LocationInfo file_0 59 26 59 31.
+  Definition loc_77 : location_info := LocationInfo file_0 59 26 59 31.
+  Definition loc_78 : location_info := LocationInfo file_0 59 32 59 34.
+  Definition loc_79 : location_info := LocationInfo file_0 59 32 59 34.
+  Definition loc_82 : location_info := LocationInfo file_0 57 9 57 24.
+  Definition loc_83 : location_info := LocationInfo file_0 57 9 57 19.
+  Definition loc_84 : location_info := LocationInfo file_0 57 9 57 15.
+  Definition loc_85 : location_info := LocationInfo file_0 57 9 57 15.
+  Definition loc_86 : location_info := LocationInfo file_0 57 16 57 18.
+  Definition loc_87 : location_info := LocationInfo file_0 57 16 57 18.
+  Definition loc_88 : location_info := LocationInfo file_0 57 23 57 24.
+  Definition loc_89 : location_info := LocationInfo file_0 56 13 56 23.
+  Definition loc_90 : location_info := LocationInfo file_0 56 13 56 16.
+  Definition loc_91 : location_info := LocationInfo file_0 56 13 56 16.
+  Definition loc_92 : location_info := LocationInfo file_0 56 17 56 19.
+  Definition loc_93 : location_info := LocationInfo file_0 56 18 56 19.
+  Definition loc_94 : location_info := LocationInfo file_0 56 21 56 22.
+  Definition loc_97 : location_info := LocationInfo file_0 54 13 54 14.
+  Definition loc_102 : location_info := LocationInfo file_0 69 2 69 30.
+  Definition loc_103 : location_info := LocationInfo file_0 70 2 70 27.
+  Definition loc_104 : location_info := LocationInfo file_0 70 9 70 26.
+  Definition loc_105 : location_info := LocationInfo file_0 70 9 70 21.
+  Definition loc_106 : location_info := LocationInfo file_0 70 9 70 10.
+  Definition loc_107 : location_info := LocationInfo file_0 70 9 70 10.
+  Definition loc_108 : location_info := LocationInfo file_0 70 13 70 21.
+  Definition loc_109 : location_info := LocationInfo file_0 70 14 70 15.
+  Definition loc_110 : location_info := LocationInfo file_0 70 19 70 20.
+  Definition loc_111 : location_info := LocationInfo file_0 70 25 70 26.
+  Definition loc_112 : location_info := LocationInfo file_0 69 16 69 29.
+  Definition loc_113 : location_info := LocationInfo file_0 69 28 69 29.
+  Definition loc_114 : location_info := LocationInfo file_0 69 28 69 29.
 
   (* Definition of function [tag_of]. *)
   Definition impl_tag_of : function := {|
@@ -131,9 +129,9 @@ Section code.
     f_code := (
       <[ "#0" :=
         "old_t" <-{ it_layout u8 }
-          LocInfoE loc_27 (Call (LocInfoE loc_29 (global_tag_of)) [@{expr} LocInfoE loc_30 (use{void*} (LocInfoE loc_31 ("p"))) ]) ;
+          LocInfoE loc_26 (Call (LocInfoE loc_28 (global_tag_of)) [@{expr} LocInfoE loc_29 (use{void*} (LocInfoE loc_30 ("p"))) ]) ;
         locinfo: loc_13 ;
-        Return (LocInfoE loc_14 (CopyAllocId (PtrOp) (LocInfoE loc_17 (UnOp (CastOp $ PtrOp) (IntOp uintptr_t) (LocInfoE loc_18 ((LocInfoE loc_19 ((LocInfoE loc_20 (UnOp (CastOp $ IntOp uintptr_t) (PtrOp) (LocInfoE loc_21 (use{void*} (LocInfoE loc_22 ("p")))))) -{IntOp uintptr_t, IntOp uintptr_t} (LocInfoE loc_23 (UnOp (CastOp $ IntOp uintptr_t) (IntOp u8) (LocInfoE loc_23 (use{it_layout u8} (LocInfoE loc_24 ("old_t")))))))) +{IntOp uintptr_t, IntOp uintptr_t} (LocInfoE loc_25 (UnOp (CastOp $ IntOp uintptr_t) (IntOp u8) (LocInfoE loc_25 (use{it_layout u8} (LocInfoE loc_26 ("t")))))))))) (LocInfoE loc_15 (use{void*} (LocInfoE loc_16 ("p"))))))
+        Return (LocInfoE loc_14 (CopyAllocId (IntOp uintptr_t) (LocInfoE loc_17 ((LocInfoE loc_18 ((LocInfoE loc_19 (UnOp (CastOp $ IntOp uintptr_t) (PtrOp) (LocInfoE loc_20 (use{void*} (LocInfoE loc_21 ("p")))))) -{IntOp uintptr_t, IntOp uintptr_t} (LocInfoE loc_22 (UnOp (CastOp $ IntOp uintptr_t) (IntOp u8) (LocInfoE loc_22 (use{it_layout u8} (LocInfoE loc_23 ("old_t")))))))) +{IntOp uintptr_t, IntOp uintptr_t} (LocInfoE loc_24 (UnOp (CastOp $ IntOp uintptr_t) (IntOp u8) (LocInfoE loc_24 (use{it_layout u8} (LocInfoE loc_25 ("t")))))))) (LocInfoE loc_15 (use{void*} (LocInfoE loc_16 ("p"))))))
       ]> $∅
     )%E
   |}.
@@ -148,9 +146,9 @@ Section code.
     f_init := "#0";
     f_code := (
       <[ "#0" :=
-        locinfo: loc_36 ;
-        Return (LocInfoE loc_37 (Call (LocInfoE loc_39 (global_tag)) [@{expr} LocInfoE loc_40 (use{void*} (LocInfoE loc_41 ("p"))) ;
-               LocInfoE loc_42 (UnOp (CastOp $ IntOp u8) (IntOp i32) (LocInfoE loc_42 (i2v 0 i32))) ]))
+        locinfo: loc_35 ;
+        Return (LocInfoE loc_36 (Call (LocInfoE loc_38 (global_tag)) [@{expr} LocInfoE loc_39 (use{void*} (LocInfoE loc_40 ("p"))) ;
+               LocInfoE loc_41 (UnOp (CastOp $ IntOp u8) (IntOp i32) (LocInfoE loc_41 (i2v 0 i32))) ]))
       ]> $∅
     )%E
   |}.
@@ -167,9 +165,9 @@ Section code.
     f_code := (
       <[ "#0" :=
         "i" <-{ it_layout uintptr_t }
-          LocInfoE loc_60 (UnOp (CastOp $ IntOp uintptr_t) (PtrOp) (LocInfoE loc_61 (use{void*} (LocInfoE loc_62 ("p"))))) ;
-        locinfo: loc_46 ;
-        Return (LocInfoE loc_47 (CopyAllocId (PtrOp) (LocInfoE loc_50 (UnOp (CastOp $ PtrOp) (IntOp uintptr_t) (LocInfoE loc_51 ((LocInfoE loc_52 (use{it_layout uintptr_t} (LocInfoE loc_53 ("i")))) -{IntOp uintptr_t, IntOp uintptr_t} (LocInfoE loc_54 ((LocInfoE loc_55 (use{it_layout uintptr_t} (LocInfoE loc_56 ("i")))) %{IntOp uintptr_t, IntOp uintptr_t} (LocInfoE loc_57 (UnOp (CastOp $ IntOp uintptr_t) (IntOp i32) (LocInfoE loc_57 ((LocInfoE loc_58 (i2v 1 i32)) <<{IntOp i32, IntOp i32} (LocInfoE loc_59 (i2v 3 i32)))))))))))) (LocInfoE loc_48 (use{void*} (LocInfoE loc_49 ("p"))))))
+          LocInfoE loc_58 (UnOp (CastOp $ IntOp uintptr_t) (PtrOp) (LocInfoE loc_59 (use{void*} (LocInfoE loc_60 ("p"))))) ;
+        locinfo: loc_45 ;
+        Return (LocInfoE loc_46 (CopyAllocId (IntOp uintptr_t) (LocInfoE loc_49 ((LocInfoE loc_50 (use{it_layout uintptr_t} (LocInfoE loc_51 ("i")))) -{IntOp uintptr_t, IntOp uintptr_t} (LocInfoE loc_52 ((LocInfoE loc_53 (use{it_layout uintptr_t} (LocInfoE loc_54 ("i")))) %{IntOp uintptr_t, IntOp uintptr_t} (LocInfoE loc_55 (UnOp (CastOp $ IntOp uintptr_t) (IntOp i32) (LocInfoE loc_55 ((LocInfoE loc_56 (i2v 1 i32)) <<{IntOp i32, IntOp i32} (LocInfoE loc_57 (i2v 3 i32)))))))))) (LocInfoE loc_47 (use{void*} (LocInfoE loc_48 ("p"))))))
       ]> $∅
     )%E
   |}.
@@ -187,16 +185,16 @@ Section code.
     f_code := (
       <[ "#0" :=
         "x" <-{ it_layout size_t }
-          LocInfoE loc_99 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_99 (i2v 0 i32))) ;
+          LocInfoE loc_97 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_97 (i2v 0 i32))) ;
         "tp" <-{ void* }
-          LocInfoE loc_91 (Call (LocInfoE loc_93 (global_tag)) [@{expr} LocInfoE loc_94 (&(LocInfoE loc_95 ("x"))) ;
-          LocInfoE loc_96 (UnOp (CastOp $ IntOp u8) (IntOp i32) (LocInfoE loc_96 (i2v 1 i32))) ]) ;
-        locinfo: loc_69 ;
-        assert: (LocInfoE loc_84 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_84 ((LocInfoE loc_85 (UnOp (CastOp $ IntOp i32) (IntOp u8) (LocInfoE loc_85 (Call (LocInfoE loc_87 (global_tag_of)) [@{expr} LocInfoE loc_88 (use{void*} (LocInfoE loc_89 ("tp"))) ])))) ={IntOp i32, IntOp i32} (LocInfoE loc_90 (i2v 1 i32)))))) ;
+          LocInfoE loc_89 (Call (LocInfoE loc_91 (global_tag)) [@{expr} LocInfoE loc_92 (&(LocInfoE loc_93 ("x"))) ;
+          LocInfoE loc_94 (UnOp (CastOp $ IntOp u8) (IntOp i32) (LocInfoE loc_94 (i2v 1 i32))) ]) ;
+        locinfo: loc_67 ;
+        assert: (LocInfoE loc_82 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_82 ((LocInfoE loc_83 (UnOp (CastOp $ IntOp i32) (IntOp u8) (LocInfoE loc_83 (Call (LocInfoE loc_85 (global_tag_of)) [@{expr} LocInfoE loc_86 (use{void*} (LocInfoE loc_87 ("tp"))) ])))) ={IntOp i32, IntOp i32} (LocInfoE loc_88 (i2v 1 i32)))))) ;
         "px" <-{ void* }
-          LocInfoE loc_76 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_77 (Call (LocInfoE loc_79 (global_untag)) [@{expr} LocInfoE loc_80 (use{void*} (LocInfoE loc_81 ("tp"))) ]))) ;
-        locinfo: loc_71 ;
-        Return (LocInfoE loc_72 (use{it_layout size_t} (LocInfoE loc_74 (!{void*} (LocInfoE loc_75 ("px"))))))
+          LocInfoE loc_74 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_75 (Call (LocInfoE loc_77 (global_untag)) [@{expr} LocInfoE loc_78 (use{void*} (LocInfoE loc_79 ("tp"))) ]))) ;
+        locinfo: loc_69 ;
+        Return (LocInfoE loc_70 (use{it_layout size_t} (LocInfoE loc_72 (!{void*} (LocInfoE loc_73 ("px"))))))
       ]> $∅
     )%E
   |}.
@@ -213,9 +211,9 @@ Section code.
     f_code := (
       <[ "#0" :=
         "i" <-{ it_layout uintptr_t }
-          LocInfoE loc_114 (UnOp (CastOp $ IntOp uintptr_t) (PtrOp) (LocInfoE loc_115 (use{void*} (LocInfoE loc_116 ("p"))))) ;
-        locinfo: loc_105 ;
-        Return (LocInfoE loc_106 ((LocInfoE loc_107 ((LocInfoE loc_108 (use{it_layout uintptr_t} (LocInfoE loc_109 ("i")))) %{IntOp uintptr_t, IntOp uintptr_t} (LocInfoE loc_110 (UnOp (CastOp $ IntOp uintptr_t) (IntOp i32) (LocInfoE loc_110 ((LocInfoE loc_111 (i2v 1 i32)) <<{IntOp i32, IntOp i32} (LocInfoE loc_112 (i2v 3 i32)))))))) ={IntOp uintptr_t, IntOp uintptr_t} (LocInfoE loc_113 (UnOp (CastOp $ IntOp uintptr_t) (IntOp i32) (LocInfoE loc_113 (i2v 0 i32))))))
+          LocInfoE loc_112 (UnOp (CastOp $ IntOp uintptr_t) (PtrOp) (LocInfoE loc_113 (use{void*} (LocInfoE loc_114 ("p"))))) ;
+        locinfo: loc_103 ;
+        Return (LocInfoE loc_104 ((LocInfoE loc_105 ((LocInfoE loc_106 (use{it_layout uintptr_t} (LocInfoE loc_107 ("i")))) %{IntOp uintptr_t, IntOp uintptr_t} (LocInfoE loc_108 (UnOp (CastOp $ IntOp uintptr_t) (IntOp i32) (LocInfoE loc_108 ((LocInfoE loc_109 (i2v 1 i32)) <<{IntOp i32, IntOp i32} (LocInfoE loc_110 (i2v 3 i32)))))))) ={IntOp uintptr_t, IntOp uintptr_t} (LocInfoE loc_111 (UnOp (CastOp $ IntOp uintptr_t) (IntOp i32) (LocInfoE loc_111 (i2v 0 i32))))))
       ]> $∅
     )%E
   |}.

examples/tagged_ptr.c

@@ -27,7 +27,7 @@ tag_t tag_of(void* p){
 [[rc::ensures("[P]")]]
 void* tag(void* p, tag_t t){
   tag_t old_t = tag_of(p);
-  return rc_copy_alloc_id((void*) ((uintptr_t) p - old_t + t), p);
+  return rc_copy_alloc_id((uintptr_t) p - old_t + t, p);
 }
 
 [[rc::parameters("r: {loc * Z}", "ty: type", "P : {iProp Σ}")]]
@@ -46,7 +46,7 @@ void* untag(void* p){
 [[rc::ensures("[P]")]]
 void* untag2(void* p){
   uintptr_t i = (uintptr_t) p;
-  return rc_copy_alloc_id((void*) (i - i % TAG_MOD), p);
+  return rc_copy_alloc_id(i - i % TAG_MOD, p);
 }
 
 [[rc::returns("{0} @ int<size_t>")]]

frontend/ail_to_coq.ml

@@ -524,14 +524,14 @@ let rec translate_expr : bool -> op_type option -> ail_expr -> expr =
     | AilEcond(e1,e2,e3) when is_const_0 e1 && is_copy_alloc_id_annot e2 ->
        let (e2, e3) =
          match macro_annot_to_list e2 with
-         | [_; MacroExpr(e2); MacroExpr(e3)] -> (e2, e3)
-         | _                                 ->
+         | [_; MacroExpr(e2); MacroExpr(e3); _] -> (e2, e3)
+         | _                                    ->
              not_impl loc "wrong copy alloc id annotation"
        in
-       let ot2 = op_type_of_tc (loc_of e2) (tc_of e2) in
+       let ot3 = op_type_of_tc (loc_of e3) (tc_of e3) in
        let e2 = translate_expr false None e2 in
        let e3 = translate_expr false None e3 in
-       let e = locate (CopyAID(ot2, e3, e2)) in
+       let e = locate (CopyAID(ot3, e3, e2)) in
        if lval then locate (LValue(e)) else e
     | AilEcond(e1,e2,e3)           ->
        let ty = op_type_of_tc (loc_of e1) (tc_of e1) in

include/refinedc.h

@@ -42,6 +42,6 @@
 // Note that rc_copy_alloc_id exposes the provenance of [from] by casting it
 // to an integer (throwing away the result).
 #define rc_copy_alloc_id(to, from) \
-  (0 ? ("rc_copy_alloc_id", (from), (to)) : ((uintptr_t) (from), (to)))
+  (0 ? ("rc_copy_alloc_id", (from), (to), (void*) (to)) : ((uintptr_t) (from), (void*) (to)))
 
 #endif

linux/pkvm/early_alloc.c

@@ -80,10 +80,10 @@ void *hyp_early_alloc_contig(unsigned int nr_pages){
   for (i = 0; i < nr_pages; i++) {
     rc_unfold(base);
     p = ret + (i << PAGE_SHIFT);
-    clear_page(rc_copy_alloc_id((void *)(p), base));
+    clear_page(rc_copy_alloc_id(p, base));
   }
 
-  return rc_copy_alloc_id((void *) ret, base);
+  return rc_copy_alloc_id(ret, base);
 }
 
 [[rc::parameters("base : loc", "given : Z", "remaining : Z")]]

theories/lang/lang.v

@@ -32,7 +32,7 @@ Inductive expr :=
 | Val (v : val)
 | UnOp (op : un_op) (ot : op_type) (e : expr)
 | BinOp (op : bin_op) (ot1 ot2 : op_type) (e1 e2 : expr)
-| CopyAllocId (ot2 : op_type) (e1 : expr) (e2 : expr)
+| CopyAllocId (ot1 : op_type) (e1 : expr) (e2 : expr)
 | Deref (o : order) (ly : layout) (e : expr)
 | CAS (ot : op_type) (e1 e2 e3 : expr)
 | Call (f : expr) (args : list expr)
@@ -48,7 +48,7 @@ Lemma expr_ind (P : expr → Prop) :
   (∀ (v : val), P (Val v)) →
   (∀ (op : un_op) (ot : op_type) (e : expr), P e → P (UnOp op ot e)) →
   (∀ (op : bin_op) (ot1 ot2 : op_type) (e1 e2 : expr), P e1 → P e2 → P (BinOp op ot1 ot2 e1 e2)) →
-  (∀ (ot2 : op_type) (e1 e2 : expr), P e1 → P e2 → P (CopyAllocId ot2 e1 e2)) →
+  (∀ (ot1 : op_type) (e1 e2 : expr), P e1 → P e2 → P (CopyAllocId ot1 e1 e2)) →
   (∀ (o : order) (ly : layout) (e : expr), P e → P (Deref o ly e)) →
   (∀ (ot : op_type) (e1 e2 e3 : expr), P e1 → P e2 → P e3 → P (CAS ot e1 e2 e3)) →
   (∀ (f : expr) (args : list expr), P f → Forall P args → P (Call f args)) →
@@ -120,7 +120,7 @@ with rtexpr :=
 | RTVal (v : val)
 | RTUnOp (op : un_op) (ot : op_type) (e : runtime_expr)
 | RTBinOp (op : bin_op) (ot1 ot2 : op_type) (e1 e2 : runtime_expr)
-| RTCopyAllocId (ot2 : op_type) (e1 : runtime_expr) (e2 : runtime_expr)
+| RTCopyAllocId (ot1 : op_type) (e1 : runtime_expr) (e2 : runtime_expr)
 | RTDeref (o : order) (ly : layout) (e : runtime_expr)
 | RTCall (f : runtime_expr) (args : list runtime_expr)
 | RTCAS (ot : op_type) (e1 e2 e3 : runtime_expr)
@@ -144,7 +144,7 @@ Fixpoint to_rtexpr (e : expr) : runtime_expr :=
   | Val v => RTVal v
   | UnOp op ot e => RTUnOp op ot (to_rtexpr e)
   | BinOp op ot1 ot2 e1 e2 => RTBinOp op ot1 ot2 (to_rtexpr e1) (to_rtexpr e2)
-  | CopyAllocId ot2 e1 e2 => RTCopyAllocId ot2 (to_rtexpr e1) (to_rtexpr e2)
+  | CopyAllocId ot1 e1 e2 => RTCopyAllocId ot1 (to_rtexpr e1) (to_rtexpr e2)
   | Deref o ly e => RTDeref o ly (to_rtexpr e)
   | Call f args => RTCall (to_rtexpr f) (to_rtexpr <$> args)
   | CAS ot e1 e2 e3 => RTCAS ot (to_rtexpr e1) (to_rtexpr e2) (to_rtexpr e3)
@@ -190,7 +190,7 @@ Fixpoint subst (x : var_name) (v : val) (e : expr)  : expr :=
   | Val v => Val v
   | UnOp op ot e => UnOp op ot (subst x v e)
   | BinOp op ot1 ot2 e1 e2 => BinOp op ot1 ot2 (subst x v e1) (subst x v e2)
-  | CopyAllocId ot2 e1 e2 => CopyAllocId ot2 (subst x v e1) (subst x v e2)