Commit 102057c0 authored by Michael Sammler's avatar Michael Sammler
Browse files

add valid_ptr requirement to copy alloc id

parent 1d82de6f
Pipeline #48737 passed with stage
in 33 minutes and 43 seconds
......@@ -10,7 +10,7 @@
/**** Casting a pointer to an integer ***************************************/
// Cast a pointer to an integer, keeping the provenance.
// Cast a pointer to an integer, keeping the provenance.
[[rc::parameters("l : loc")]]
[[rc::args("l @ &own<int<i32>>")]]
[[rc::returns("l @ intptr<uintptr_t>")]]
......@@ -151,7 +151,9 @@ int roundtrip_and_read4(int* 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));
......
......@@ -188,18 +188,18 @@ Section code.
Definition loc_249 : location_info := LocationInfo file_0 146 16 146 29.
Definition loc_250 : location_info := LocationInfo file_0 146 28 146 29.
Definition loc_251 : location_info := LocationInfo file_0 146 28 146 29.
Definition loc_256 : location_info := LocationInfo file_0 156 2 156 28.
Definition loc_257 : location_info := LocationInfo file_0 157 2 157 73.
Definition loc_258 : location_info := LocationInfo file_0 157 9 157 72.
Definition loc_259 : location_info := LocationInfo file_0 157 36 157 39.
Definition loc_260 : location_info := LocationInfo file_0 157 36 157 39.
Definition loc_261 : location_info := LocationInfo file_0 157 41 157 44.
Definition loc_262 : location_info := LocationInfo file_0 157 41 157 44.
Definition loc_263 : location_info := LocationInfo file_0 156 12 156 27.
Definition loc_264 : location_info := LocationInfo file_0 156 20 156 27.
Definition loc_265 : location_info := LocationInfo file_0 156 21 156 22.
Definition loc_266 : location_info := LocationInfo file_0 156 21 156 22.
Definition loc_267 : location_info := LocationInfo file_0 156 25 156 26.
Definition loc_256 : location_info := LocationInfo file_0 158 2 158 28.
Definition loc_257 : location_info := LocationInfo file_0 159 2 159 73.
Definition loc_258 : location_info := LocationInfo file_0 159 9 159 72.
Definition loc_259 : location_info := LocationInfo file_0 159 36 159 39.
Definition loc_260 : location_info := LocationInfo file_0 159 36 159 39.
Definition loc_261 : location_info := LocationInfo file_0 159 41 159 44.
Definition loc_262 : location_info := LocationInfo file_0 159 41 159 44.
Definition loc_263 : location_info := LocationInfo file_0 158 12 158 27.
Definition loc_264 : location_info := LocationInfo file_0 158 20 158 27.
Definition loc_265 : location_info := LocationInfo file_0 158 21 158 22.
Definition loc_266 : location_info := LocationInfo file_0 158 21 158 22.
Definition loc_267 : location_info := LocationInfo file_0 158 25 158 26.
(* Definition of function [int_ptr1]. *)
Definition impl_int_ptr1 : function := {|
......
......@@ -76,6 +76,6 @@ Section spec.
(* Specifications for function [int_to_ptr]. *)
Definition type_of_int_to_ptr :=
fn( p : loc; (p @ (intptr (uintptr_t))); True)
() : (), (p @ (&own (place (p)))); True.
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.
......@@ -34,66 +34,66 @@ Section code.
Definition loc_29 : location_info := LocationInfo file_0 28 16 28 22.
Definition loc_30 : location_info := LocationInfo file_0 28 23 28 24.
Definition loc_31 : location_info := LocationInfo file_0 28 23 28 24.
Definition loc_36 : location_info := LocationInfo file_0 36 2 36 30.
Definition loc_37 : location_info := LocationInfo file_0 37 2 37 121.
Definition loc_38 : location_info := LocationInfo file_0 37 9 37 120.
Definition loc_39 : location_info := LocationInfo file_0 37 35 37 38.
Definition loc_40 : location_info := LocationInfo file_0 37 35 37 38.
Definition loc_41 : location_info := LocationInfo file_0 37 40 37 68.
Definition loc_42 : location_info := LocationInfo file_0 37 49 37 67.
Definition loc_43 : location_info := LocationInfo file_0 37 50 37 51.
Definition loc_44 : location_info := LocationInfo file_0 37 50 37 51.
Definition loc_45 : location_info := LocationInfo file_0 37 54 37 66.
Definition loc_46 : location_info := LocationInfo file_0 37 54 37 55.
Definition loc_47 : location_info := LocationInfo file_0 37 54 37 55.
Definition loc_48 : location_info := LocationInfo file_0 37 58 37 66.
Definition loc_49 : location_info := LocationInfo file_0 37 59 37 60.
Definition loc_50 : location_info := LocationInfo file_0 37 64 37 65.
Definition loc_51 : location_info := LocationInfo file_0 36 16 36 29.
Definition loc_52 : location_info := LocationInfo file_0 36 28 36 29.
Definition loc_53 : location_info := LocationInfo file_0 36 28 36 29.
Definition loc_58 : location_info := LocationInfo file_0 42 2 42 15.
Definition loc_59 : location_info := LocationInfo file_0 44 2 44 24.
Definition loc_60 : location_info := LocationInfo file_0 45 2 45 26.
Definition loc_61 : location_info := LocationInfo file_0 47 2 47 36.
Definition loc_62 : location_info := LocationInfo file_0 48 2 48 13.
Definition loc_63 : location_info := LocationInfo file_0 48 9 48 12.
Definition loc_64 : location_info := LocationInfo file_0 48 9 48 12.
Definition loc_65 : location_info := LocationInfo file_0 48 10 48 12.
Definition loc_66 : location_info := LocationInfo file_0 48 10 48 12.
Definition loc_67 : location_info := LocationInfo file_0 47 15 47 35.
Definition loc_68 : location_info := LocationInfo file_0 47 26 47 35.
Definition loc_69 : location_info := LocationInfo file_0 47 26 47 31.
Definition loc_70 : location_info := LocationInfo file_0 47 26 47 31.
Definition loc_71 : location_info := LocationInfo file_0 47 32 47 34.
Definition loc_72 : location_info := LocationInfo file_0 47 32 47 34.
Definition loc_75 : location_info := LocationInfo file_0 45 9 45 24.
Definition loc_76 : location_info := LocationInfo file_0 45 9 45 19.
Definition loc_77 : location_info := LocationInfo file_0 45 9 45 15.
Definition loc_78 : location_info := LocationInfo file_0 45 9 45 15.
Definition loc_79 : location_info := LocationInfo file_0 45 16 45 18.
Definition loc_80 : location_info := LocationInfo file_0 45 16 45 18.
Definition loc_81 : location_info := LocationInfo file_0 45 23 45 24.
Definition loc_82 : location_info := LocationInfo file_0 44 13 44 23.
Definition loc_83 : location_info := LocationInfo file_0 44 13 44 16.
Definition loc_84 : location_info := LocationInfo file_0 44 13 44 16.
Definition loc_85 : location_info := LocationInfo file_0 44 17 44 19.
Definition loc_86 : location_info := LocationInfo file_0 44 18 44 19.
Definition loc_87 : location_info := LocationInfo file_0 44 21 44 22.
Definition loc_90 : location_info := LocationInfo file_0 42 13 42 14.
Definition loc_95 : location_info := LocationInfo file_0 57 2 57 30.
Definition loc_96 : location_info := LocationInfo file_0 58 2 58 27.
Definition loc_97 : location_info := LocationInfo file_0 58 9 58 26.
Definition loc_98 : location_info := LocationInfo file_0 58 9 58 21.
Definition loc_99 : location_info := LocationInfo file_0 58 9 58 10.
Definition loc_100 : location_info := LocationInfo file_0 58 9 58 10.
Definition loc_101 : location_info := LocationInfo file_0 58 13 58 21.
Definition loc_102 : location_info := LocationInfo file_0 58 14 58 15.
Definition loc_103 : location_info := LocationInfo file_0 58 19 58 20.
Definition loc_104 : location_info := LocationInfo file_0 58 25 58 26.
Definition loc_105 : location_info := LocationInfo file_0 57 16 57 29.
Definition loc_106 : location_info := LocationInfo file_0 57 28 57 29.
Definition loc_107 : location_info := LocationInfo file_0 57 28 57 29.
Definition loc_36 : location_info := LocationInfo file_0 37 2 37 30.
Definition loc_37 : location_info := LocationInfo file_0 38 2 38 121.
Definition loc_38 : location_info := LocationInfo file_0 38 9 38 120.
Definition loc_39 : location_info := LocationInfo file_0 38 35 38 38.
Definition loc_40 : location_info := LocationInfo file_0 38 35 38 38.
Definition loc_41 : location_info := LocationInfo file_0 38 40 38 68.
Definition loc_42 : location_info := LocationInfo file_0 38 49 38 67.
Definition loc_43 : location_info := LocationInfo file_0 38 50 38 51.
Definition loc_44 : location_info := LocationInfo file_0 38 50 38 51.
Definition loc_45 : location_info := LocationInfo file_0 38 54 38 66.
Definition loc_46 : location_info := LocationInfo file_0 38 54 38 55.
Definition loc_47 : location_info := LocationInfo file_0 38 54 38 55.
Definition loc_48 : location_info := LocationInfo file_0 38 58 38 66.
Definition loc_49 : location_info := LocationInfo file_0 38 59 38 60.
Definition loc_50 : location_info := LocationInfo file_0 38 64 38 65.
Definition loc_51 : location_info := LocationInfo file_0 37 16 37 29.
Definition loc_52 : location_info := LocationInfo file_0 37 28 37 29.
Definition loc_53 : location_info := LocationInfo file_0 37 28 37 29.
Definition loc_58 : location_info := LocationInfo file_0 43 2 43 15.
Definition loc_59 : location_info := LocationInfo file_0 45 2 45 24.
Definition loc_60 : location_info := LocationInfo file_0 46 2 46 26.
Definition loc_61 : location_info := LocationInfo file_0 48 2 48 36.
Definition loc_62 : location_info := LocationInfo file_0 49 2 49 13.
Definition loc_63 : location_info := LocationInfo file_0 49 9 49 12.
Definition loc_64 : location_info := LocationInfo file_0 49 9 49 12.
Definition loc_65 : location_info := LocationInfo file_0 49 10 49 12.
Definition loc_66 : location_info := LocationInfo file_0 49 10 49 12.
Definition loc_67 : location_info := LocationInfo file_0 48 15 48 35.
Definition loc_68 : location_info := LocationInfo file_0 48 26 48 35.
Definition loc_69 : location_info := LocationInfo file_0 48 26 48 31.
Definition loc_70 : location_info := LocationInfo file_0 48 26 48 31.
Definition loc_71 : location_info := LocationInfo file_0 48 32 48 34.
Definition loc_72 : location_info := LocationInfo file_0 48 32 48 34.
Definition loc_75 : location_info := LocationInfo file_0 46 9 46 24.
Definition loc_76 : location_info := LocationInfo file_0 46 9 46 19.
Definition loc_77 : location_info := LocationInfo file_0 46 9 46 15.
Definition loc_78 : location_info := LocationInfo file_0 46 9 46 15.
Definition loc_79 : location_info := LocationInfo file_0 46 16 46 18.
Definition loc_80 : location_info := LocationInfo file_0 46 16 46 18.
Definition loc_81 : location_info := LocationInfo file_0 46 23 46 24.
Definition loc_82 : location_info := LocationInfo file_0 45 13 45 23.
Definition loc_83 : location_info := LocationInfo file_0 45 13 45 16.
Definition loc_84 : location_info := LocationInfo file_0 45 13 45 16.
Definition loc_85 : location_info := LocationInfo file_0 45 17 45 19.
Definition loc_86 : location_info := LocationInfo file_0 45 18 45 19.
Definition loc_87 : location_info := LocationInfo file_0 45 21 45 22.
Definition loc_90 : location_info := LocationInfo file_0 43 13 43 14.
Definition loc_95 : location_info := LocationInfo file_0 58 2 58 30.
Definition loc_96 : location_info := LocationInfo file_0 59 2 59 27.
Definition loc_97 : location_info := LocationInfo file_0 59 9 59 26.
Definition loc_98 : location_info := LocationInfo file_0 59 9 59 21.
Definition loc_99 : location_info := LocationInfo file_0 59 9 59 10.
Definition loc_100 : location_info := LocationInfo file_0 59 9 59 10.
Definition loc_101 : location_info := LocationInfo file_0 59 13 59 21.
Definition loc_102 : location_info := LocationInfo file_0 59 14 59 15.
Definition loc_103 : location_info := LocationInfo file_0 59 19 59 20.
Definition loc_104 : location_info := LocationInfo file_0 59 25 59 26.
Definition loc_105 : location_info := LocationInfo file_0 58 16 58 29.
Definition loc_106 : location_info := LocationInfo file_0 58 28 58 29.
Definition loc_107 : location_info := LocationInfo file_0 58 28 58 29.
(* Definition of function [tag_of]. *)
Definition impl_tag_of : function := {|
......
......@@ -13,7 +13,7 @@ Section proof_tag.
typed_function (impl_tag global_tag_of) type_of_tag.
Proof.
Open Scope printing_sugar.
start_function "tag" ([[r t] ty]) => arg_p arg_t local_old_t.
start_function "tag" ([[[r t] ty] P]) => arg_p arg_t local_old_t.
split_blocks ((
)%I : gmap label (iProp Σ)) ((
......
......@@ -12,7 +12,7 @@ Section proof_untag.
typed_function impl_untag type_of_untag.
Proof.
Open Scope printing_sugar.
start_function "untag" ([r ty]) => arg_p local_i.
start_function "untag" ([[r ty] P]) => arg_p local_i.
split_blocks ((
)%I : gmap label (iProp Σ)) ((
......
......@@ -19,12 +19,12 @@ Section spec.
(* Specifications for function [tag]. *)
Definition type_of_tag :=
fn( (r, t, ty) : (loc * Z) * Z * type; (r @ (tagged_ptr (Own) (TAG_MOD) (ty))), (t @ (int (u8))); 0 t < TAG_MOD)
fn( (r, t, ty, P) : (loc * Z) * Z * type * (iProp Σ); (r @ (tagged_ptr (Own) (TAG_MOD) (ty))), (t @ (int (u8))); 0 t < TAG_MOD AllocAlive ty Own P (P))
() : (), (((r.1, t)) @ (tagged_ptr (Own) (TAG_MOD) (ty))); True.
(* Specifications for function [untag]. *)
Definition type_of_untag :=
fn( (r, ty) : (loc * Z) * type; (r @ (tagged_ptr (Own) (TAG_MOD) (ty))); True)
fn( (r, ty, P) : (loc * Z) * type * (iProp Σ); (r @ (tagged_ptr (Own) (TAG_MOD) (ty))); AllocAlive ty Own P (P))
() : (), ((r.1) @ (&own (ty))); True.
(* Specifications for function [test]. *)
......
......@@ -20,17 +20,18 @@ tag_t tag_of(void* p){
return ((uintptr_t) p) % TAG_MOD;
}
[[rc::parameters("r: {loc * Z}", "t: Z", "ty: type")]]
[[rc::parameters("r: {loc * Z}", "t: Z", "ty: type", "P : {iProp Σ}")]]
[[rc::args("r @ tagged_ptr<Own, TAG_MOD, ty>", "t @ int<u8>")]]
[[rc::requires("{0 ≤ t < TAG_MOD}")]]
[[rc::requires("{0 ≤ t < TAG_MOD}", "{AllocAlive ty Own P}", "[P]")]]
[[rc::returns("{(r.1, t)} @ tagged_ptr<Own, TAG_MOD, ty>")]]
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);
}
[[rc::parameters("r: {loc * Z}", "ty: type")]]
[[rc::parameters("r: {loc * Z}", "ty: type", "P : {iProp Σ}")]]
[[rc::args("r @ tagged_ptr<Own, TAG_MOD, ty>")]]
[[rc::requires("{AllocAlive ty Own P}", "[P]")]]
[[rc::returns("{r.1} @ &own<ty>")]]
void* untag(void* p){
uintptr_t i = (uintptr_t) p;
......
......@@ -15,7 +15,7 @@ struct
[[rc::refined_by("base : loc", "given : Z", "remaining : Z")]]
[[rc::let("z_cur : Z = {(base.2 + given * PAGE_SIZE)%Z}")]]
[[rc::let("z_end : Z = {(base.2 + (given + remaining) * PAGE_SIZE)%Z}")]]
[[rc::constraints("{0 ≤ given}", "{0 ≤ remaining}",
[[rc::constraints("{0 ≤ given}", "{0 ≤ remaining}", "[alloc_global base]",
"{base.2 + (given + remaining) * PAGE_SIZE <= max_int u64}")]]
region {
[[rc::field("z_end @ int<uintptr_t>")]] uintptr_t end;
......@@ -76,7 +76,7 @@ void *hyp_early_alloc_contig(unsigned int nr_pages){
[[rc::constraints("[(base +ₗ given * PAGE_SIZE) ◁ₗ zeroed (PAGES i)]")]]
[[rc::constraints("[(base +ₗ (given + i) * PAGE_SIZE) ◁ₗ uninit (PAGES (Z.to_nat n - i)%nat)]")]]
[[rc::constraints("global mem : {(base, given + n, remaining - n)%Z} @ region")]]
[[rc::constraints("{i ≤ n}")]]
[[rc::constraints("{i ≤ n}", "{0 ≤ given}")]]
for (i = 0; i < nr_pages; i++) {
rc_unfold(base);
p = ret + (i << PAGE_SHIFT);
......@@ -99,7 +99,7 @@ void *hyp_early_alloc_page(void *arg){
[[rc::parameters("l : loc", "n : Z", "s : Z")]]
[[rc::args("l @ &own<uninit<PAGES<{Z.to_nat n}>>>", "s @ int<u32>")]]
[[rc::requires("{s = (n * PAGE_SIZE)%Z}")]]
[[rc::requires("{s = (n * PAGE_SIZE)%Z}", "[alloc_global l]")]]
[[rc::requires("global mem : uninit<struct_region>")]]
[[rc::ensures("global mem : {(l, 0, n)} @ region")]]
[[rc::tactics("all: rewrite -> ly_size_PAGES in *; solve_goal.")]]
......
......@@ -26,7 +26,8 @@ Section proof_hyp_early_alloc_contig.
((base + given * PAGE_SIZE) ◁ₗ zeroed (PAGES i))
((base + (given + i) * PAGE_SIZE) ◁ₗ uninit (PAGES (Z.to_nat n - i)%nat))
(global_with_type "mem" Own (((base, given + n, remaining - n)%Z) @ (region)))
i n
i n
0 given
]> $
)%I : gmap label (iProp Σ)) ((
......
......@@ -31,6 +31,7 @@ Section spec.
]) (
0 given
0 remaining
(alloc_global base)
base.2 + (given + remaining) * PAGE_SIZE <= max_int u64
)
)%I.
......@@ -58,6 +59,7 @@ Section spec.
]) (
0 given
0 remaining
(alloc_global base)
base.2 + (given + remaining) * PAGE_SIZE <= max_int u64
)
)%I.
......@@ -108,7 +110,7 @@ Section spec.
(* Specifications for function [hyp_early_alloc_init]. *)
Definition type_of_hyp_early_alloc_init :=
fn( (l, n, s) : loc * Z * Z; (l @ (&own (uninit (PAGES (Z.to_nat n))))), (s @ (int (u32))); s = (n * PAGE_SIZE)%Z (global_with_type "mem" Own (uninit (struct_region))))
fn( (l, n, s) : loc * Z * Z; (l @ (&own (uninit (PAGES (Z.to_nat n))))), (s @ (int (u32))); s = (n * PAGE_SIZE)%Z (alloc_global l) (global_with_type "mem" Own (uninit (struct_region))))
() : (), (void); (global_with_type "mem" Own (((l, 0, n)) @ (region))).
End spec.
......
......@@ -99,6 +99,12 @@ Section definitions.
Global Instance alloc_alive_tl id dq a : Timeless (alloc_alive id dq a).
Proof. rewrite alloc_alive_eq. by apply _. Qed.
Definition alloc_global (l : loc) : iProp Σ :=
id, l.1 = Some id alloc_alive id DfracDiscarded true.
Global Instance alloc_global_tl l : Timeless (alloc_global l).
Proof. by apply _. Qed.
Global Instance alloc_global_pers l : Persistent (alloc_global l).
Proof. rewrite /alloc_global alloc_alive_eq. by apply _. Qed.
(** * Function table stuff. *)
(** [fntbl_entry l f] persistently records the information that function
......@@ -358,6 +364,19 @@ Section loc_in_bounds.
move => ?. rewrite (le_plus_minus m n) // -loc_in_bounds_split. iIntros "[$ _]".
Qed.
Lemma loc_in_bounds_offset l1 l2 (n m : nat):
l1.1 = l2.1
l1.2 l2.2 ->
l2.2 + m l1.2 + n ->
loc_in_bounds l1 n - loc_in_bounds l2 m.
Proof.
move => ???. have ->: (l2 = l1 + (l2.2 - l1.2)).
{ rewrite /shift_loc. destruct l1, l2 => /=. f_equal; [done| lia]. }
have -> : n = (Z.to_nat (l2.2 - l1.2) + Z.to_nat (n - (l2.2 - l1.2)))%nat by lia.
rewrite -loc_in_bounds_split. iIntros "[_ Hlib]". rewrite Z2Nat.id; [|lia].
iApply (loc_in_bounds_shorten with "Hlib"). lia.
Qed.
Lemma loc_in_bounds_to_heap_loc_in_bounds l σ n:
loc_in_bounds l n - state_ctx σ - heap_state_loc_in_bounds l n σ.(st_heap).
Proof.
......@@ -774,8 +793,12 @@ Section alloc_alive.
iRight. iExists a, q, _. iFrame. by destruct v.
Qed.
Lemma alloc_alive_loc_to_alloc_id_alive l σ:
alloc_alive_loc l - state_ctx σ - aid, l.1 = Some aid alloc_id_alive aid σ.(st_heap).
Lemma alloc_global_alive l:
alloc_global l - alloc_alive_loc l.
Proof. iIntros "(%id&%&Ha)". rewrite alloc_alive_loc_eq. iLeft. eauto. Qed.
Lemma alloc_alive_loc_to_block_alive l σ:
alloc_alive_loc l - state_ctx σ - block_alive l σ.(st_heap).
Proof.
rewrite alloc_alive_loc_eq.
iIntros "[H|H]".
......@@ -795,9 +818,8 @@ Section alloc_alive.
loc_in_bounds l 0 - alloc_alive_loc l - state_ctx σ - valid_ptr l σ.(st_heap).
Proof.
iIntros "Hin Ha Hσ".
iDestruct (alloc_alive_loc_to_alloc_id_alive with "Ha Hσ") as %[?[??]].
iDestruct (loc_in_bounds_to_heap_loc_in_bounds with "Hin Hσ") as %?.
iPureIntro. split; last done. by eexists.
iDestruct (alloc_alive_loc_to_block_alive with "Ha Hσ") as %?.
by iDestruct (loc_in_bounds_to_heap_loc_in_bounds with "Hin Hσ") as %?.
Qed.
End alloc_alive.
......
......@@ -431,10 +431,12 @@ comparing pointers? (see lambda rust) *)
| CopyAllocIdPS l1 l2 v1 v2 σ:
val_to_loc v1 = Some l1
val_to_loc v2 = Some l2
valid_ptr (l2.1, l1.2) σ.(st_heap)
expr_step (CopyAllocId PtrOp (Val v1) (Val v2)) σ [] (Val (val_of_loc (l2.1, l1.2))) σ []
| CopyAllocIdIS it l1 l2 v1 v2 σ:
val_to_loc v1 = Some l1
val_to_loc_weak v2 it = Some l2
valid_ptr (l2.1, l1.2) σ.(st_heap)
expr_step (CopyAllocId (IntOp it) (Val v1) (Val v2)) σ [] (Val (val_of_loc (l2.1, l1.2))) σ []
| IfES v it e1 e2 n σ:
val_to_Z_weak v it = Some n
......
......@@ -373,10 +373,19 @@ Qed.
Lemma wp_copy_alloc_id Φ l1 l2 v1 v2 E:
val_to_loc v1 = Some l1
val_to_loc v2 = Some l2
Φ (val_of_loc (l2.1, l1.2)) - WP CopyAllocId PtrOp (Val v1) (Val v2) @ E {{ Φ }}.
loc_in_bounds (l2.1, l1.2) 0 -
alloc_alive_loc l2 Φ (val_of_loc (l2.1, l1.2)) -
WP CopyAllocId PtrOp (Val v1) (Val v2) @ E {{ Φ }}.
Proof.
iIntros (Hl1 Hl2) "HΦ". iApply wp_lift_expr_step => //.
iIntros (σ1) "Hctx !>". iSplit; first by eauto 8 using CopyAllocIdPS.
iIntros (Hl1 Hl2) "Hl HΦ". iApply wp_lift_expr_step => //.
iIntros (σ1) "Hctx !>".
iAssert valid_ptr (l2.1, l1.2) σ1.(st_heap)%I as %?. {
iSplit; [ |iApply (loc_in_bounds_to_heap_loc_in_bounds with "Hl Hctx")].
iApply (alloc_alive_loc_to_block_alive with "[HΦ] Hctx").
iDestruct "HΦ" as "[Halive _]". by iApply alloc_alive_loc_mono; [|done].
}
iDestruct "HΦ" as "[_ HΦ]".
iSplit; first by eauto 8 using CopyAllocIdPS.
iIntros "!>" (???? Hstep ?) "!>". inv_expr_step. iSplit => //. iFrame.
by iApply wp_value.
Qed.
......@@ -384,10 +393,19 @@ Qed.
Lemma wp_copy_alloc_id_int Φ it l1 l2 v1 v2 E:
val_to_loc v1 = Some l1
val_to_loc_weak v2 it = Some l2
Φ (val_of_loc (l2.1, l1.2)) - WP CopyAllocId (IntOp it) (Val v1) (Val v2) @ E {{ Φ }}.
loc_in_bounds (l2.1, l1.2) 0 -
alloc_alive_loc l2 Φ (val_of_loc (l2.1, l1.2)) -
WP CopyAllocId (IntOp it) (Val v1) (Val v2) @ E {{ Φ }}.
Proof.
iIntros (Hl1 Hl2) "HΦ". iApply wp_lift_expr_step => //.
iIntros (σ1) "Hctx !>". iSplit; first by eauto 8 using CopyAllocIdIS.
iIntros (Hl1 Hl2) "Hl HΦ". iApply wp_lift_expr_step => //.
iIntros (σ1) "Hctx !>".
iAssert valid_ptr (l2.1, l1.2) σ1.(st_heap)%I as %?. {
iSplit; [ |iApply (loc_in_bounds_to_heap_loc_in_bounds with "Hl Hctx")].
iApply (alloc_alive_loc_to_block_alive with "[HΦ] Hctx").
iDestruct "HΦ" as "[Halive _]". by iApply alloc_alive_loc_mono; [|done].
}
iDestruct "HΦ" as "[_ HΦ]".
iSplit; first by eauto 8 using CopyAllocIdIS.
iIntros "!>" (???? Hstep ?) "!>". inv_expr_step. iSplit => //. iFrame.
by iApply wp_value.
Qed.
......@@ -469,10 +487,8 @@ Proof.
}
rewrite Hv /=. move: Hv => /val_to_of_Z Hv.
iApply wp_ptr_offset; [done| by apply: val_to_Z_to_int_repr_Z | | ].
{ have ? := offset_of_idx_le_size sl i.
have -> : (ly_size sl = offset_of_idx (sl_members sl) i + (ly_size sl - offset_of_idx (sl_members sl) i))%nat by lia.
rewrite -loc_in_bounds_split offset_loc_sz1 //.
iDestruct "Hl" as "[_ Hl]". iApply (loc_in_bounds_shorten with "Hl"). lia. }
{ have ? := offset_of_idx_le_size sl i. rewrite offset_loc_sz1 //.
iApply (loc_in_bounds_offset with "Hl"); simpl; [done| destruct l => /=; lia | destruct l => /=; lia ]. }
by rewrite offset_loc_sz1.
Qed.
Lemma wp_get_member_union Φ vl l ul n E:
......
......@@ -223,9 +223,7 @@ Section array.
iDestruct "HP" as (? Hlen) "HP".
have [|ty ?]:= lookup_lt_is_Some_2 tys (Z.to_nat i). lia.
iApply wp_ptr_offset => //; [by apply val_to_of_loc | | ].
{ have -> : length tys = (Z.to_nat i + (length tys - Z.to_nat i))%nat by lia.
rewrite Nat.mul_add_distr_l -loc_in_bounds_split Nat2Z.inj_mul Z2Nat.id; [|lia].
iDestruct "Hb" as "[_ Hb]". iApply (loc_in_bounds_shorten with "Hb"). nia. }
{ iApply (loc_in_bounds_offset with "Hb"); simpl; [done| destruct l => /=; lia | destruct l => /=; nia]. }
iIntros "!#". iExists _. iSplit => //.
iDestruct (big_sepL_insert_acc with "Hl") as "[Hl Hc]" => //. rewrite Z2Nat.id//.
iApply ("HP" $! ty with "[//] Hl"). iIntros (l' ty2 β2 typ R) "Hl' Htyp HT".
......
......@@ -51,6 +51,12 @@ Inductive FICLocSemantic : Set :=.
Global Instance find_in_context_type_loc_semantic_inst `{!typeG Σ} l :
FindInContext (FindLoc l) 2%nat FICLocSemantic :=
λ T, i2p (find_in_context_type_loc_id l T).
Global Instance find_in_context_loc_in_bounds_semantic_inst `{!typeG Σ} l :
FindInContext (FindLocInBounds l) 2%nat FICLocSemantic :=
λ T, i2p (find_in_context_loc_in_bounds l T).
Global Instance find_in_context_loc_in_bounds_type_semantic_inst `{!typeG Σ} l :
FindInContext (FindLocInBounds l) 3%nat FICLocSemantic :=
λ T, i2p (find_in_context_loc_in_bounds_loc l T).
Lemma tac_solve_loc_eq `{!typeG Σ} l1 β1 ty1 l2 β2 ty2:
l1 = l2
......@@ -60,6 +66,14 @@ Proof. by move => ->. Qed.
Hint Extern 10 (FindHypEqual FICLocSemantic (_ ◁ₗ{_} _) (_ ◁ₗ{_} _) _) =>
(notypeclasses refine (tac_solve_loc_eq _ _ _ _ _ _ _); solve_loc_eq) : typeclass_instances.
Lemma tac_loc_in_bounds_solve_loc_eq `{!typeG Σ} l1 l2 n1 n2:
l1 = l2
FindHypEqual FICLocSemantic (loc_in_bounds l1 n1) (loc_in_bounds l2 n2) (loc_in_bounds l1 n2).
Proof. by move => ->. Qed.
Hint Extern 10 (FindHypEqual FICLocSemantic (loc_in_bounds _ _) (loc_in_bounds _ _) _) =>
(notypeclasses refine (tac_loc_in_bounds_solve_loc_eq _ _ _ _ _); solve_loc_eq) : typeclass_instances.
Section test.
Context (l : loc).
Context (id : option alloc_id).
......@@ -100,4 +114,7 @@ Section test.
Goal ((l + (n1 + (i + j)%nat) * n2) = (l + (n1 + i + j) * n2))%Z.
solve_loc_eq. Qed.
Goal (l = (l.1, l.2 * 1))%Z.
solve_loc_eq. Qed.
End test.
......@@ -129,6 +129,8 @@ Section programs.
Lemma type_copy_aid_intptr v1 P1 v2 p2 it T:
( p1,
subsume P1 (v1 ◁ᵥ p1 @ frac_ptr Own (place p1)) (
(loc_in_bounds (p2.1, p1.2) 0 True)
(alloc_alive_loc p2 True)
T (val_of_loc (p2.1, p1.2)) (t2mt (value void* (val_of_loc (p2.1, p1.2))))