Adding rules for intptr casts + examples.

Co-authored-by: Michael Sammler <msammler@mpi-sws.org>

_CoqProject

@@ -43,3 +43,4 @@
 -Q _build/default/examples/proofs/talk_demo1 refinedc.examples.talk_demo1
 -Q _build/default/examples/proofs/talk_demo2 refinedc.examples.talk_demo2
 -Q _build/default/examples/proofs/talk_demo3 refinedc.examples.talk_demo3
+-Q _build/default/examples/proofs/intptr refinedc.examples.intptr

examples/intptr.c

+#include <refinedc.h>
+#include <stddef.h>
+
+[[rc::args("&own<int<i32>>")]]
+[[rc::returns("int<size_t>")]]
+size_t int_ptr(int* p){
+  size_t i = (size_t) p;
+  return i;
+}
+
+[[rc::parameters("p1 : loc", "p2 : loc")]]
+[[rc::args("p1 @ &own<int<i32>>", "p2 @ &own<int<i32>>")]]
+[[rc::returns("{p1.2 `min` p2.2} @ int<size_t>")]]
+size_t min_ptr_val(int *p1, int *p2){
+  size_t i1 = (size_t) p1;
+  size_t i2 = (size_t) p2;
+
+  if(i1 <= i2){
+    return i1;
+  }
+
+  return i2;
+}
+
+[[rc::parameters("p : loc")]]
+[[rc::args("p @ &own<int<i32>>")]]
+[[rc::returns("{(None, p.2)} @ &own<singleton_place<{(None, p.2)}>>")]]
+int* roundtrip1(int* p){
+  size_t i = (size_t) p;
+  void *q = (void*) i;
+  return q;
+}
+
+[[rc::parameters("p : loc", "n : Z")]]
+[[rc::args("p @ &own<n @ int<i32>>")]]
+[[rc::returns("p @ &own<n @ int<i32>>")]]
+int* roundtrip2(int* p){
+  size_t i = (size_t) p;
+  int *q = (void*) i;
+  return rc_copy_alloc_id(q, p);
+}
+
+[[rc::parameters("p : loc", "n : Z")]]
+[[rc::args("p @ &own<n @ int<i32>>")]]
+[[rc::returns("n @ int<i32>")]]
+[[rc::ensures("p @ &own<n @ int<i32>>")]]
+int roundtrip_and_read(int* p){
+  size_t i = (size_t) p;
+  int *q = (int*) i;
+  int *r = rc_copy_alloc_id(q, p);
+  return *r;
+}

examples/proofs/intptr/dune

+; Generated by [refinedc], do not edit.
+(coq.theory
+ (flags -w -notation-overridden -w -redundant-canonical-projection)
+ (name refinedc.examples.intptr)
+ (theories refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))

examples/proofs/intptr/generated_code.v

+From refinedc.lang Require Export notation.
+From refinedc.lang Require Import tactics.
+From refinedc.typing Require Import annotations.
+Set Default Proof Using "Type".
+
+(* Generated from [examples/intptr.c]. *)
+Section code.
+  Definition file_0 : string := "examples/intptr.c".
+  Definition loc_2 : location_info := LocationInfo file_0 7 2 7 24.
+  Definition loc_3 : location_info := LocationInfo file_0 8 2 8 11.
+  Definition loc_4 : location_info := LocationInfo file_0 8 9 8 10.
+  Definition loc_5 : location_info := LocationInfo file_0 8 9 8 10.
+  Definition loc_6 : location_info := LocationInfo file_0 7 13 7 23.
+  Definition loc_7 : location_info := LocationInfo file_0 7 22 7 23.
+  Definition loc_8 : location_info := LocationInfo file_0 7 22 7 23.
+  Definition loc_13 : location_info := LocationInfo file_0 15 2 15 26.
+  Definition loc_14 : location_info := LocationInfo file_0 16 2 16 26.
+  Definition loc_15 : location_info := LocationInfo file_0 18 2 20 3.
+  Definition loc_16 : location_info := LocationInfo file_0 22 2 22 12.
+  Definition loc_17 : location_info := LocationInfo file_0 22 9 22 11.
+  Definition loc_18 : location_info := LocationInfo file_0 22 9 22 11.
+  Definition loc_19 : location_info := LocationInfo file_0 18 14 20 3.
+  Definition loc_20 : location_info := LocationInfo file_0 19 4 19 14.
+  Definition loc_21 : location_info := LocationInfo file_0 19 11 19 13.
+  Definition loc_22 : location_info := LocationInfo file_0 19 11 19 13.
+  Definition loc_24 : location_info := LocationInfo file_0 18 5 18 13.
+  Definition loc_25 : location_info := LocationInfo file_0 18 5 18 7.
+  Definition loc_26 : location_info := LocationInfo file_0 18 5 18 7.
+  Definition loc_27 : location_info := LocationInfo file_0 18 11 18 13.
+  Definition loc_28 : location_info := LocationInfo file_0 18 11 18 13.
+  Definition loc_29 : location_info := LocationInfo file_0 16 14 16 25.
+  Definition loc_30 : location_info := LocationInfo file_0 16 23 16 25.
+  Definition loc_31 : location_info := LocationInfo file_0 16 23 16 25.
+  Definition loc_34 : location_info := LocationInfo file_0 15 14 15 25.
+  Definition loc_35 : location_info := LocationInfo file_0 15 23 15 25.
+  Definition loc_36 : location_info := LocationInfo file_0 15 23 15 25.
+  Definition loc_41 : location_info := LocationInfo file_0 29 2 29 24.
+  Definition loc_42 : location_info := LocationInfo file_0 30 2 30 22.
+  Definition loc_43 : location_info := LocationInfo file_0 31 2 31 11.
+  Definition loc_44 : location_info := LocationInfo file_0 31 9 31 10.
+  Definition loc_45 : location_info := LocationInfo file_0 31 9 31 10.
+  Definition loc_46 : location_info := LocationInfo file_0 30 12 30 21.
+  Definition loc_47 : location_info := LocationInfo file_0 30 20 30 21.
+  Definition loc_48 : location_info := LocationInfo file_0 30 20 30 21.
+  Definition loc_51 : location_info := LocationInfo file_0 29 13 29 23.
+  Definition loc_52 : location_info := LocationInfo file_0 29 22 29 23.
+  Definition loc_53 : location_info := LocationInfo file_0 29 22 29 23.
+  Definition loc_58 : location_info := LocationInfo file_0 38 2 38 24.
+  Definition loc_59 : location_info := LocationInfo file_0 39 2 39 21.
+  Definition loc_60 : location_info := LocationInfo file_0 40 2 40 47.
+  Definition loc_61 : location_info := LocationInfo file_0 40 9 40 46.
+  Definition loc_62 : location_info := LocationInfo file_0 40 35 40 38.
+  Definition loc_63 : location_info := LocationInfo file_0 40 35 40 38.
+  Definition loc_64 : location_info := LocationInfo file_0 40 42 40 45.
+  Definition loc_65 : location_info := LocationInfo file_0 40 42 40 45.
+  Definition loc_66 : location_info := LocationInfo file_0 39 11 39 20.
+  Definition loc_67 : location_info := LocationInfo file_0 39 19 39 20.
+  Definition loc_68 : location_info := LocationInfo file_0 39 19 39 20.
+  Definition loc_71 : location_info := LocationInfo file_0 38 13 38 23.
+  Definition loc_72 : location_info := LocationInfo file_0 38 22 38 23.
+  Definition loc_73 : location_info := LocationInfo file_0 38 22 38 23.
+  Definition loc_78 : location_info := LocationInfo file_0 48 2 48 24.
+  Definition loc_79 : location_info := LocationInfo file_0 49 2 49 20.
+  Definition loc_80 : location_info := LocationInfo file_0 50 2 50 49.
+  Definition loc_81 : location_info := LocationInfo file_0 51 2 51 12.
+  Definition loc_82 : location_info := LocationInfo file_0 51 9 51 11.
+  Definition loc_83 : location_info := LocationInfo file_0 51 9 51 11.
+  Definition loc_84 : location_info := LocationInfo file_0 51 10 51 11.
+  Definition loc_85 : location_info := LocationInfo file_0 51 10 51 11.
+  Definition loc_86 : location_info := LocationInfo file_0 50 11 50 48.
+  Definition loc_87 : location_info := LocationInfo file_0 50 37 50 40.
+  Definition loc_88 : location_info := LocationInfo file_0 50 37 50 40.
+  Definition loc_89 : location_info := LocationInfo file_0 50 44 50 47.
+  Definition loc_90 : location_info := LocationInfo file_0 50 44 50 47.
+  Definition loc_93 : location_info := LocationInfo file_0 49 11 49 19.
+  Definition loc_94 : location_info := LocationInfo file_0 49 18 49 19.
+  Definition loc_95 : location_info := LocationInfo file_0 49 18 49 19.
+  Definition loc_98 : location_info := LocationInfo file_0 48 13 48 23.
+  Definition loc_99 : location_info := LocationInfo file_0 48 22 48 23.
+  Definition loc_100 : location_info := LocationInfo file_0 48 22 48 23.
+
+  (* Definition of function [int_ptr]. *)
+  Definition impl_int_ptr : function := {|
+    f_args := [
+      ("p", LPtr)
+    ];
+    f_local_vars := [
+      ("i", it_layout size_t)
+    ];
+    f_init := "#0";
+    f_code := (
+      <[ "#0" :=
+        "i" <-{ it_layout size_t }
+          LocInfoE loc_6 (UnOp (CastOp $ IntOp size_t) (PtrOp) (LocInfoE loc_7 (use{LPtr} (LocInfoE loc_8 ("p"))))) ;
+        locinfo: loc_3 ;
+        Return (LocInfoE loc_4 (use{it_layout size_t} (LocInfoE loc_5 ("i"))))
+      ]> $∅
+    )%E
+  |}.
+
+  (* Definition of function [min_ptr_val]. *)
+  Definition impl_min_ptr_val : function := {|
+    f_args := [
+      ("p1", LPtr);
+      ("p2", LPtr)
+    ];
+    f_local_vars := [
+      ("i2", it_layout size_t);
+      ("i1", it_layout size_t)
+    ];
+    f_init := "#0";
+    f_code := (
+      <[ "#0" :=
+        "i1" <-{ it_layout size_t }
+          LocInfoE loc_34 (UnOp (CastOp $ IntOp size_t) (PtrOp) (LocInfoE loc_35 (use{LPtr} (LocInfoE loc_36 ("p1"))))) ;
+        "i2" <-{ it_layout size_t }
+          LocInfoE loc_29 (UnOp (CastOp $ IntOp size_t) (PtrOp) (LocInfoE loc_30 (use{LPtr} (LocInfoE loc_31 ("p2"))))) ;
+        locinfo: loc_24 ;
+        if: LocInfoE loc_24 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_24 ((LocInfoE loc_25 (use{it_layout size_t} (LocInfoE loc_26 ("i1")))) ≤{IntOp size_t, IntOp size_t} (LocInfoE loc_27 (use{it_layout size_t} (LocInfoE loc_28 ("i2")))))))
+        then
+        locinfo: loc_20 ;
+          Goto "#2"
+        else
+        locinfo: loc_16 ;
+          Goto "#3"
+      ]> $
+      <[ "#1" :=
+        locinfo: loc_16 ;
+        Return (LocInfoE loc_17 (use{it_layout size_t} (LocInfoE loc_18 ("i2"))))
+      ]> $
+      <[ "#2" :=
+        locinfo: loc_20 ;
+        Return (LocInfoE loc_21 (use{it_layout size_t} (LocInfoE loc_22 ("i1"))))
+      ]> $
+      <[ "#3" :=
+        locinfo: loc_16 ;
+        Goto "#1"
+      ]> $∅
+    )%E
+  |}.
+
+  (* Definition of function [roundtrip1]. *)
+  Definition impl_roundtrip1 : function := {|
+    f_args := [
+      ("p", LPtr)
+    ];
+    f_local_vars := [
+      ("i", it_layout size_t);
+      ("q", LPtr)
+    ];
+    f_init := "#0";
+    f_code := (
+      <[ "#0" :=
+        "i" <-{ it_layout size_t }
+          LocInfoE loc_51 (UnOp (CastOp $ IntOp size_t) (PtrOp) (LocInfoE loc_52 (use{LPtr} (LocInfoE loc_53 ("p"))))) ;
+        "q" <-{ LPtr }
+          LocInfoE loc_46 (UnOp (CastOp $ PtrOp) (IntOp size_t) (LocInfoE loc_47 (use{it_layout size_t} (LocInfoE loc_48 ("i"))))) ;
+        locinfo: loc_43 ;
+        Return (LocInfoE loc_44 (use{LPtr} (LocInfoE loc_45 ("q"))))
+      ]> $∅
+    )%E
+  |}.
+
+  (* Definition of function [roundtrip2]. *)
+  Definition impl_roundtrip2 : function := {|
+    f_args := [
+      ("p", LPtr)
+    ];
+    f_local_vars := [
+      ("i", it_layout size_t);
+      ("q", LPtr)
+    ];
+    f_init := "#0";
+    f_code := (
+      <[ "#0" :=
+        "i" <-{ it_layout size_t }
+          LocInfoE loc_71 (UnOp (CastOp $ IntOp size_t) (PtrOp) (LocInfoE loc_72 (use{LPtr} (LocInfoE loc_73 ("p"))))) ;
+        "q" <-{ LPtr }
+          LocInfoE loc_66 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_66 (UnOp (CastOp $ PtrOp) (IntOp size_t) (LocInfoE loc_67 (use{it_layout size_t} (LocInfoE loc_68 ("i"))))))) ;
+        locinfo: loc_60 ;
+        Return (LocInfoE loc_61 (CopyAllocId (LocInfoE loc_64 (use{LPtr} (LocInfoE loc_65 ("q")))) (LocInfoE loc_62 (use{LPtr} (LocInfoE loc_63 ("p"))))))
+      ]> $∅
+    )%E
+  |}.
+
+  (* Definition of function [roundtrip_and_read]. *)
+  Definition impl_roundtrip_and_read : function := {|
+    f_args := [
+      ("p", LPtr)
+    ];
+    f_local_vars := [
+      ("i", it_layout size_t);
+      ("r", LPtr);
+      ("q", LPtr)
+    ];
+    f_init := "#0";
+    f_code := (
+      <[ "#0" :=
+        "i" <-{ it_layout size_t }
+          LocInfoE loc_98 (UnOp (CastOp $ IntOp size_t) (PtrOp) (LocInfoE loc_99 (use{LPtr} (LocInfoE loc_100 ("p"))))) ;
+        "q" <-{ LPtr }
+          LocInfoE loc_93 (UnOp (CastOp $ PtrOp) (IntOp size_t) (LocInfoE loc_94 (use{it_layout size_t} (LocInfoE loc_95 ("i"))))) ;
+        "r" <-{ LPtr }
+          LocInfoE loc_86 (CopyAllocId (LocInfoE loc_89 (use{LPtr} (LocInfoE loc_90 ("q")))) (LocInfoE loc_87 (use{LPtr} (LocInfoE loc_88 ("p"))))) ;
+        locinfo: loc_81 ;
+        Return (LocInfoE loc_82 (use{it_layout i32} (LocInfoE loc_84 (!{LPtr} (LocInfoE loc_85 ("r"))))))
+      ]> $∅
+    )%E
+  |}.
+End code.

examples/proofs/intptr/generated_proof_int_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_ptr.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Typing proof for [int_ptr]. *)
+  Lemma type_int_ptr :
+    ⊢ typed_function impl_int_ptr type_of_int_ptr.
+  Proof.
+    start_function "int_ptr" ([]) => arg_p local_i.
+    split_blocks ((
+      ∅
+    )%I : gmap label (iProp Σ)) ((
+      ∅
+    )%I : gmap label (iProp Σ)).
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "int_ptr" "#0".
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+    all: print_sidecondition_goal "int_ptr".
+  Qed.
+End proof_int_ptr.

examples/proofs/intptr/generated_proof_min_ptr_val.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_min_ptr_val.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Typing proof for [min_ptr_val]. *)
+  Lemma type_min_ptr_val :
+    ⊢ typed_function impl_min_ptr_val type_of_min_ptr_val.
+  Proof.
+    start_function "min_ptr_val" ([p1 p2]) => arg_p1 arg_p2 local_i2 local_i1.
+    split_blocks ((
+      ∅
+    )%I : gmap label (iProp Σ)) ((
+      ∅
+    )%I : gmap label (iProp Σ)).
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "min_ptr_val" "#0".
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+    all: print_sidecondition_goal "min_ptr_val".
+  Qed.
+End proof_min_ptr_val.

examples/proofs/intptr/generated_proof_roundtrip1.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_roundtrip1.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Typing proof for [roundtrip1]. *)
+  Lemma type_roundtrip1 :
+    ⊢ typed_function impl_roundtrip1 type_of_roundtrip1.
+  Proof.
+    start_function "roundtrip1" (p) => arg_p local_i local_q.
+    split_blocks ((
+      ∅
+    )%I : gmap label (iProp Σ)) ((
+      ∅
+    )%I : gmap label (iProp Σ)).
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "roundtrip1" "#0".
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+    all: print_sidecondition_goal "roundtrip1".
+  Qed.
+End proof_roundtrip1.

examples/proofs/intptr/generated_proof_roundtrip2.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_roundtrip2.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Typing proof for [roundtrip2]. *)
+  Lemma type_roundtrip2 :
+    ⊢ typed_function impl_roundtrip2 type_of_roundtrip2.
+  Proof.
+    start_function "roundtrip2" ([p n]) => arg_p local_i local_q.
+    split_blocks ((
+      ∅
+    )%I : gmap label (iProp Σ)) ((
+      ∅
+    )%I : gmap label (iProp Σ)).
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "roundtrip2" "#0".
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+    all: print_sidecondition_goal "roundtrip2".
+  Qed.
+End proof_roundtrip2.

examples/proofs/intptr/generated_proof_roundtrip_and_read.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_roundtrip_and_read.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Typing proof for [roundtrip_and_read]. *)
+  Lemma type_roundtrip_and_read :
+    ⊢ typed_function impl_roundtrip_and_read type_of_roundtrip_and_read.
+  Proof.
+    start_function "roundtrip_and_read" ([p n]) => arg_p local_i local_r local_q.
+    split_blocks ((
+      ∅
+    )%I : gmap label (iProp Σ)) ((
+      ∅
+    )%I : gmap label (iProp Σ)).
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "roundtrip_and_read" "#0".
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+    all: print_sidecondition_goal "roundtrip_and_read".
+  Qed.
+End proof_roundtrip_and_read.

examples/proofs/intptr/generated_spec.v

+From refinedc.typing Require Import typing.
+From refinedc.examples.intptr Require Import generated_code.
+Set Default Proof Using "Type".
+
+(* Generated from [examples/intptr.c]. *)
+Section spec.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Type definitions. *)
+
+  (* Specifications for function [int_ptr]. *)
+  Definition type_of_int_ptr :=
+    fn(∀ () : (); (&own (int (i32))); True)
+      → ∃ () : (), (int (size_t)); True.
+
+  (* Specifications for function [min_ptr_val]. *)
+  Definition type_of_min_ptr_val :=
+    fn(∀ (p1, p2) : loc * loc; (p1 @ (&own (int (i32)))), (p2 @ (&own (int (i32)))); True)
+      → ∃ () : (), ((p1.2 `min` p2.2) @ (int (size_t))); True.
+
+  (* Specifications for function [roundtrip1]. *)
+  Definition type_of_roundtrip1 :=
+    fn(∀ p : loc; (p @ (&own (int (i32)))); True)
+      → ∃ () : (), (((None, p.2)) @ (&own (singleton_place ((None, p.2))))); True.
+
+  (* Specifications for function [roundtrip2]. *)
+  Definition type_of_roundtrip2 :=
+    fn(∀ (p, n) : loc * Z; (p @ (&own (n @ (int (i32))))); True)
+      → ∃ () : (), (p @ (&own (n @ (int (i32))))); True.
+
+  (* Specifications for function [roundtrip_and_read]. *)
+  Definition type_of_roundtrip_and_read :=
+    fn(∀ (p, n) : loc * Z; (p @ (&own (n @ (int (i32))))); True)
+      → ∃ () : (), (n @ (int (i32))); (p ◁ₗ (n @ (int (i32)))).
+End spec.

examples/proofs/intptr/proof_files

+generated_proof_int_ptr.v
+generated_proof_min_ptr_val.v
+generated_proof_roundtrip1.v
+generated_proof_roundtrip2.v
+generated_proof_roundtrip_and_read.v

frontend/ail_to_coq.ml

@@ -200,6 +200,11 @@ let is_macro_annot e =
   | MacroString("rc_macro") :: _ -> true
   | _ -> false
 
+let is_copy_alloc_id_annot e =
+  match macro_annot_to_list e with
+  | MacroString("rc_copy_alloc_id") :: _ -> true
+  | _ -> false
+
 let rec op_type_of loc Ctype.(Ctype(_, c_ty)) =
   match c_ty with
   | Void                -> not_impl loc "op_type_of (Void)"
@@ -502,9 +507,18 @@ let rec translate_expr : bool -> op_type option -> ail_expr -> expr * calls =
           in
           let (args, es) = process_rest rest in
           let (e3, l) = translate e3 in
-          (locate(Macro(name, args, es, e3)), l)
+          (locate (Macro(name, args, es, e3)), l)
        | _ -> not_impl loc "wrong macro"
        end
+    | AilEcond(e1,e2,e3) when is_const_0 e1 && is_copy_alloc_id_annot e2 ->
+       let e2 =
+         match macro_annot_to_list e2 with
+         | [_; MacroExpr(e2)] -> e2
+         | _                  -> not_impl loc "wrong copy alloc id annotation"
+       in
+       let (e2, l2) = translate_expr lval None e2 in
+       let (e3, l3) = translate_expr lval None e3 in
+       (locate (CopyAID(e3, e2)), l2 @ l3)
     | AilEcond(e1,e2,e3)           -> not_impl loc "expr cond"
     | AilEcast(q,c_ty,e)           ->
         begin

frontend/coq_ast.ml

@@ -54,6 +54,7 @@ and expr_aux =
   | AnnotExpr of int * coq_expr * expr
   | Struct    of string * (string * expr) list
   | Macro     of string * string list * expr list * expr
+  | CopyAID   of expr * expr
 
 type stmt = stmt_aux Location.located
 and stmt_aux =

frontend/coq_pp.ml

@@ -196,7 +196,7 @@ let rec pp_expr : Coq_ast.expr pp = fun ff e ->
         in
         List.iteri fn fs;
         pp "@]@;]@]"
-    | Macro(name, args, es, e)                ->
+    | Macro(name, args, es, e)      ->
         pp "@[@[<hov 2>CheckedMacroE (%s %s) [" name (String.concat " " args);
         let fn i e =
           let s = if i = List.length es - 1 then "" else " ;" in
@@ -204,6 +204,8 @@ let rec pp_expr : Coq_ast.expr pp = fun ff e ->
         in
         List.iteri fn es;
         pp "@]@;] (%a : expr)@]" pp_expr e
+    | CopyAID(e1, e2)               ->
+        pp "CopyAllocId (%a) (%a)" pp_expr e1 pp_expr e2
   in
   match Location.get e.loc with
   | Some(d) when !print_expr_locs ->

include/refinedc.h

@@ -39,4 +39,6 @@
 #define RC_MACRO_EXPR(expr) "EXPR", expr
 #define RC_MACRO(name, m, ...) (0 ? ("rc_macro", #name, __VA_ARGS__, (m)) : (m))
 
+#define rc_copy_alloc_id(to, from) (0 ? ("rc_copy_alloc_id", (from)) : (to))
+
 #endif

theories/lang/heap.v

@@ -60,7 +60,9 @@ Section definitions.
     seal_eq allocs_entry_aux.
 
   Definition loc_in_bounds_def (l : loc) (n : nat) : iProp Σ :=
-    ∃ id a, ⌜l.1 = Some id ∧ alloc_start a ≤ l.2 ∧ l.2 + n ≤ alloc_end a⌝ ∗ allocs_entry id a.
+    ∃ id a, ⌜l.1 = Some id ∧ alloc_start a ≤ l.2 ∧
+             l.2 + n ≤ alloc_end a ∧ in_range_allocation a⌝ ∗
+             allocs_entry id a.
   Definition loc_in_bounds_aux : seal (@loc_in_bounds_def). by eexists. Qed.
   Definition loc_in_bounds := unseal loc_in_bounds_aux.
   Definition loc_in_bounds_eq : @loc_in_bounds = @loc_in_bounds_def :=
@@ -212,9 +214,10 @@ Section allocs.
   Lemma allocs_entry_to_loc_in_bounds l aid (n : nat) a:
     l.1 = Some aid →
     alloc_start a ≤ l.2 ∧ l.2 + n ≤ alloc_end a →
+    in_range_allocation a →
     allocs_entry aid a -∗ loc_in_bounds l n.
   Proof.
-    iIntros (??) "?". rewrite loc_in_bounds_eq/loc_in_bounds_def.
+    iIntros (?[??]?) "?". rewrite loc_in_bounds_eq/loc_in_bounds_def.
     iExists _, _. by iFrame.
   Qed.
 
@@ -243,14 +246,14 @@ Section loc_in_bounds.
   Proof.
     rewrite loc_in_bounds_eq. iSplit.
     - iIntros "[H1 H2]".