Commit 14fdc0df authored by Michael Sammler's avatar Michael Sammler
Browse files

add type_alive

parent af9df26c
Pipeline #49097 passed with stage
in 16 minutes and 18 seconds
......@@ -14,91 +14,91 @@ Section code.
Definition loc_7 : location_info := LocationInfo file_0 19 27 19 35.
Definition loc_8 : location_info := LocationInfo file_0 19 28 19 29.
Definition loc_9 : location_info := LocationInfo file_0 19 33 19 34.
Definition loc_12 : location_info := LocationInfo file_0 28 2 28 26.
Definition loc_13 : location_info := LocationInfo file_0 29 2 29 164.
Definition loc_14 : location_info := LocationInfo file_0 29 9 29 163.
Definition loc_15 : location_info := LocationInfo file_0 29 35 29 38.
Definition loc_16 : location_info := LocationInfo file_0 29 35 29 38.
Definition loc_17 : location_info := LocationInfo file_0 29 40 29 67.
Definition loc_18 : location_info := LocationInfo file_0 29 41 29 62.
Definition loc_19 : location_info := LocationInfo file_0 29 41 29 54.
Definition loc_20 : location_info := LocationInfo file_0 29 53 29 54.
Definition loc_21 : location_info := LocationInfo file_0 29 53 29 54.
Definition loc_22 : location_info := LocationInfo file_0 29 57 29 62.
Definition loc_23 : location_info := LocationInfo file_0 29 57 29 62.
Definition loc_24 : location_info := LocationInfo file_0 29 65 29 66.
Definition loc_25 : location_info := LocationInfo file_0 29 65 29 66.
Definition loc_26 : location_info := LocationInfo file_0 28 16 28 25.
Definition loc_27 : location_info := LocationInfo file_0 28 16 28 22.
Definition loc_28 : location_info := LocationInfo file_0 28 16 28 22.
Definition loc_29 : location_info := LocationInfo file_0 28 23 28 24.
Definition loc_30 : location_info := LocationInfo file_0 28 23 28 24.
Definition loc_35 : location_info := LocationInfo file_0 38 2 38 19.
Definition loc_36 : location_info := LocationInfo file_0 38 9 38 18.
Definition loc_37 : location_info := LocationInfo file_0 38 9 38 12.
Definition loc_38 : location_info := LocationInfo file_0 38 9 38 12.
Definition loc_39 : location_info := LocationInfo file_0 38 13 38 14.
Definition loc_40 : location_info := LocationInfo file_0 38 13 38 14.
Definition loc_41 : location_info := LocationInfo file_0 38 16 38 17.
Definition loc_44 : location_info := LocationInfo file_0 47 2 47 30.
Definition loc_45 : location_info := LocationInfo file_0 48 2 48 137.
Definition loc_46 : location_info := LocationInfo file_0 48 9 48 136.
Definition loc_47 : location_info := LocationInfo file_0 48 35 48 38.
Definition loc_48 : location_info := LocationInfo file_0 48 35 48 38.
Definition loc_49 : location_info := LocationInfo file_0 48 40 48 58.
Definition loc_50 : location_info := LocationInfo file_0 48 41 48 42.
Definition loc_51 : location_info := LocationInfo file_0 48 41 48 42.
Definition loc_52 : location_info := LocationInfo file_0 48 45 48 57.
Definition loc_53 : location_info := LocationInfo file_0 48 45 48 46.
Definition loc_54 : location_info := LocationInfo file_0 48 45 48 46.
Definition loc_55 : location_info := LocationInfo file_0 48 49 48 57.
Definition loc_56 : location_info := LocationInfo file_0 48 50 48 51.
Definition loc_57 : location_info := LocationInfo file_0 48 55 48 56.
Definition loc_58 : location_info := LocationInfo file_0 47 16 47 29.
Definition loc_59 : location_info := LocationInfo file_0 47 28 47 29.
Definition loc_60 : location_info := LocationInfo file_0 47 28 47 29.
Definition loc_65 : location_info := LocationInfo file_0 53 2 53 15.
Definition loc_66 : location_info := LocationInfo file_0 55 2 55 24.
Definition loc_67 : location_info := LocationInfo file_0 56 2 56 26.
Definition loc_68 : location_info := LocationInfo file_0 58 2 58 36.
Definition loc_69 : location_info := LocationInfo file_0 59 2 59 13.
Definition loc_70 : location_info := LocationInfo file_0 59 9 59 12.
Definition loc_71 : location_info := LocationInfo file_0 59 9 59 12.
Definition loc_72 : location_info := LocationInfo file_0 59 10 59 12.
Definition loc_73 : location_info := LocationInfo file_0 59 10 59 12.
Definition loc_74 : location_info := LocationInfo file_0 58 15 58 35.
Definition loc_75 : location_info := LocationInfo file_0 58 26 58 35.
Definition loc_76 : location_info := LocationInfo file_0 58 26 58 31.
Definition loc_77 : location_info := LocationInfo file_0 58 26 58 31.
Definition loc_78 : location_info := LocationInfo file_0 58 32 58 34.
Definition loc_79 : location_info := LocationInfo file_0 58 32 58 34.
Definition loc_82 : location_info := LocationInfo file_0 56 9 56 24.
Definition loc_83 : location_info := LocationInfo file_0 56 9 56 19.
Definition loc_84 : location_info := LocationInfo file_0 56 9 56 15.
Definition loc_85 : location_info := LocationInfo file_0 56 9 56 15.
Definition loc_86 : location_info := LocationInfo file_0 56 16 56 18.
Definition loc_87 : location_info := LocationInfo file_0 56 16 56 18.
Definition loc_88 : location_info := LocationInfo file_0 56 23 56 24.
Definition loc_89 : location_info := LocationInfo file_0 55 13 55 23.
Definition loc_90 : location_info := LocationInfo file_0 55 13 55 16.
Definition loc_91 : location_info := LocationInfo file_0 55 13 55 16.
Definition loc_92 : location_info := LocationInfo file_0 55 17 55 19.
Definition loc_93 : location_info := LocationInfo file_0 55 18 55 19.
Definition loc_94 : location_info := LocationInfo file_0 55 21 55 22.
Definition loc_97 : location_info := LocationInfo file_0 53 13 53 14.
Definition loc_102 : location_info := LocationInfo file_0 68 2 68 30.
Definition loc_103 : location_info := LocationInfo file_0 69 2 69 27.
Definition loc_104 : location_info := LocationInfo file_0 69 9 69 26.
Definition loc_105 : location_info := LocationInfo file_0 69 9 69 21.
Definition loc_106 : location_info := LocationInfo file_0 69 9 69 10.
Definition loc_107 : location_info := LocationInfo file_0 69 9 69 10.
Definition loc_108 : location_info := LocationInfo file_0 69 13 69 21.
Definition loc_109 : location_info := LocationInfo file_0 69 14 69 15.
Definition loc_110 : location_info := LocationInfo file_0 69 19 69 20.
Definition loc_111 : location_info := LocationInfo file_0 69 25 69 26.
Definition loc_112 : location_info := LocationInfo file_0 68 16 68 29.
Definition loc_113 : location_info := LocationInfo file_0 68 28 68 29.
Definition loc_114 : location_info := LocationInfo file_0 68 28 68 29.
Definition loc_12 : location_info := LocationInfo file_0 27 2 27 26.
Definition loc_13 : location_info := LocationInfo file_0 28 2 28 164.
Definition loc_14 : location_info := LocationInfo file_0 28 9 28 163.
Definition loc_15 : location_info := LocationInfo file_0 28 35 28 38.
Definition loc_16 : location_info := LocationInfo file_0 28 35 28 38.
Definition loc_17 : location_info := LocationInfo file_0 28 40 28 67.
Definition loc_18 : location_info := LocationInfo file_0 28 41 28 62.
Definition loc_19 : location_info := LocationInfo file_0 28 41 28 54.
Definition loc_20 : location_info := LocationInfo file_0 28 53 28 54.
Definition loc_21 : location_info := LocationInfo file_0 28 53 28 54.
Definition loc_22 : location_info := LocationInfo file_0 28 57 28 62.
Definition loc_23 : location_info := LocationInfo file_0 28 57 28 62.
Definition loc_24 : location_info := LocationInfo file_0 28 65 28 66.
Definition loc_25 : location_info := LocationInfo file_0 28 65 28 66.
Definition loc_26 : location_info := LocationInfo file_0 27 16 27 25.
Definition loc_27 : location_info := LocationInfo file_0 27 16 27 22.
Definition loc_28 : location_info := LocationInfo file_0 27 16 27 22.
Definition loc_29 : location_info := LocationInfo file_0 27 23 27 24.
Definition loc_30 : location_info := LocationInfo file_0 27 23 27 24.
Definition loc_35 : location_info := LocationInfo file_0 36 2 36 19.
Definition loc_36 : location_info := LocationInfo file_0 36 9 36 18.
Definition loc_37 : location_info := LocationInfo file_0 36 9 36 12.
Definition loc_38 : location_info := LocationInfo file_0 36 9 36 12.
Definition loc_39 : location_info := LocationInfo file_0 36 13 36 14.
Definition loc_40 : location_info := LocationInfo file_0 36 13 36 14.
Definition loc_41 : location_info := LocationInfo file_0 36 16 36 17.
Definition loc_44 : location_info := LocationInfo file_0 44 2 44 30.
Definition loc_45 : location_info := LocationInfo file_0 45 2 45 137.
Definition loc_46 : location_info := LocationInfo file_0 45 9 45 136.
Definition loc_47 : location_info := LocationInfo file_0 45 35 45 38.
Definition loc_48 : location_info := LocationInfo file_0 45 35 45 38.
Definition loc_49 : location_info := LocationInfo file_0 45 40 45 58.
Definition loc_50 : location_info := LocationInfo file_0 45 41 45 42.
Definition loc_51 : location_info := LocationInfo file_0 45 41 45 42.
Definition loc_52 : location_info := LocationInfo file_0 45 45 45 57.
Definition loc_53 : location_info := LocationInfo file_0 45 45 45 46.
Definition loc_54 : location_info := LocationInfo file_0 45 45 45 46.
Definition loc_55 : location_info := LocationInfo file_0 45 49 45 57.
Definition loc_56 : location_info := LocationInfo file_0 45 50 45 51.
Definition loc_57 : location_info := LocationInfo file_0 45 55 45 56.
Definition loc_58 : location_info := LocationInfo file_0 44 16 44 29.
Definition loc_59 : location_info := LocationInfo file_0 44 28 44 29.
Definition loc_60 : location_info := LocationInfo file_0 44 28 44 29.
Definition loc_65 : location_info := LocationInfo file_0 50 2 50 15.
Definition loc_66 : location_info := LocationInfo file_0 52 2 52 24.
Definition loc_67 : location_info := LocationInfo file_0 53 2 53 26.
Definition loc_68 : location_info := LocationInfo file_0 55 2 55 36.
Definition loc_69 : location_info := LocationInfo file_0 56 2 56 13.
Definition loc_70 : location_info := LocationInfo file_0 56 9 56 12.
Definition loc_71 : location_info := LocationInfo file_0 56 9 56 12.
Definition loc_72 : location_info := LocationInfo file_0 56 10 56 12.
Definition loc_73 : location_info := LocationInfo file_0 56 10 56 12.
Definition loc_74 : location_info := LocationInfo file_0 55 15 55 35.
Definition loc_75 : location_info := LocationInfo file_0 55 26 55 35.
Definition loc_76 : location_info := LocationInfo file_0 55 26 55 31.
Definition loc_77 : location_info := LocationInfo file_0 55 26 55 31.
Definition loc_78 : location_info := LocationInfo file_0 55 32 55 34.
Definition loc_79 : location_info := LocationInfo file_0 55 32 55 34.
Definition loc_82 : location_info := LocationInfo file_0 53 9 53 24.
Definition loc_83 : location_info := LocationInfo file_0 53 9 53 19.
Definition loc_84 : location_info := LocationInfo file_0 53 9 53 15.
Definition loc_85 : location_info := LocationInfo file_0 53 9 53 15.
Definition loc_86 : location_info := LocationInfo file_0 53 16 53 18.
Definition loc_87 : location_info := LocationInfo file_0 53 16 53 18.
Definition loc_88 : location_info := LocationInfo file_0 53 23 53 24.
Definition loc_89 : location_info := LocationInfo file_0 52 13 52 23.
Definition loc_90 : location_info := LocationInfo file_0 52 13 52 16.
Definition loc_91 : location_info := LocationInfo file_0 52 13 52 16.
Definition loc_92 : location_info := LocationInfo file_0 52 17 52 19.
Definition loc_93 : location_info := LocationInfo file_0 52 18 52 19.
Definition loc_94 : location_info := LocationInfo file_0 52 21 52 22.
Definition loc_97 : location_info := LocationInfo file_0 50 13 50 14.
Definition loc_102 : location_info := LocationInfo file_0 65 2 65 30.
Definition loc_103 : location_info := LocationInfo file_0 66 2 66 27.
Definition loc_104 : location_info := LocationInfo file_0 66 9 66 26.
Definition loc_105 : location_info := LocationInfo file_0 66 9 66 21.
Definition loc_106 : location_info := LocationInfo file_0 66 9 66 10.
Definition loc_107 : location_info := LocationInfo file_0 66 9 66 10.
Definition loc_108 : location_info := LocationInfo file_0 66 13 66 21.
Definition loc_109 : location_info := LocationInfo file_0 66 14 66 15.
Definition loc_110 : location_info := LocationInfo file_0 66 19 66 20.
Definition loc_111 : location_info := LocationInfo file_0 66 25 66 26.
Definition loc_112 : location_info := LocationInfo file_0 65 16 65 29.
Definition loc_113 : location_info := LocationInfo file_0 65 28 65 29.
Definition loc_114 : location_info := LocationInfo file_0 65 28 65 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] P]) => arg_p arg_t local_old_t.
start_function "tag" ([[r t] ty]) => arg_p arg_t local_old_t.
split_blocks ((
)%I : gmap label (iProp Σ)) ((
......
......@@ -12,7 +12,7 @@ Section proof_tag_of.
typed_function impl_tag_of type_of_tag_of.
Proof.
Open Scope printing_sugar.
start_function "tag_of" ([[[r ty] v] P]) => arg_p.
start_function "tag_of" ([[r ty] v]) => arg_p.
split_blocks ((
)%I : gmap label (iProp Σ)) ((
......
......@@ -13,7 +13,7 @@ Section proof_untag.
typed_function (impl_untag global_tag) type_of_untag.
Proof.
Open Scope printing_sugar.
start_function "untag" ([[r ty] P]) => arg_p.
start_function "untag" ([r ty]) => arg_p.
split_blocks ((
)%I : gmap label (iProp Σ)) ((
......
......@@ -12,7 +12,7 @@ Section proof_untag2.
typed_function impl_untag2 type_of_untag2.
Proof.
Open Scope printing_sugar.
start_function "untag2" ([[r ty] P]) => arg_p local_i.
start_function "untag2" ([r ty]) => arg_p local_i.
split_blocks ((
)%I : gmap label (iProp Σ)) ((
......
......@@ -14,23 +14,23 @@ Section spec.
(* Specifications for function [tag_of]. *)
Definition type_of_tag_of :=
fn( (r, ty, v, P) : (loc * Z) * type * val * (iProp Σ); (at_value (v) (r @ (&tagged (TAG_MOD) (ty)))); AllocAlive ty Own P (P))
() : (), ((r.2) @ (int (u8))); (v ◁ᵥ (r @ (&tagged (TAG_MOD) (ty)))) 0 r.2 < TAG_MOD (P).
fn( (r, ty, v) : (loc * Z) * type * val; (at_value (v) (r @ (&tagged (TAG_MOD) (ty)))); (type_alive_own ty))
() : (), ((r.2) @ (int (u8))); (v ◁ᵥ (r @ (&tagged (TAG_MOD) (ty)))) 0 r.2 < TAG_MOD.
(* Specifications for function [tag]. *)
Definition type_of_tag :=
fn( (r, t, ty, P) : (loc * Z) * Z * type * (iProp Σ); (r @ (&tagged (TAG_MOD) (ty))), (t @ (int (u8))); 0 t < TAG_MOD AllocAlive ty Own P (P))
() : (), (((r.1, t)) @ (&tagged (TAG_MOD) (ty))); (P).
fn( (r, t, ty) : (loc * Z) * Z * type; (r @ (&tagged (TAG_MOD) (ty))), (t @ (int (u8))); 0 t < TAG_MOD (type_alive_own ty))
() : (), (((r.1, t)) @ (&tagged (TAG_MOD) (ty))); True.
(* Specifications for function [untag]. *)
Definition type_of_untag :=
fn( (r, ty, P) : (loc * Z) * type * (iProp Σ); (r @ (&tagged (TAG_MOD) (ty))); AllocAlive ty Own P (P))
() : (), ((r.1) @ (&own (ty))); (P).
fn( (r, ty) : (loc * Z) * type; (r @ (&tagged (TAG_MOD) (ty))); (type_alive_own ty))
() : (), ((r.1) @ (&own (ty))); True.
(* Specifications for function [untag2]. *)
Definition type_of_untag2 :=
fn( (r, ty, P) : (loc * Z) * type * (iProp Σ); (r @ (&tagged (TAG_MOD) (ty))); AllocAlive ty Own P (P))
() : (), ((r.1) @ (&own (ty))); (P).
fn( (r, ty) : (loc * Z) * type; (r @ (&tagged (TAG_MOD) (ty))); (type_alive_own ty))
() : (), ((r.1) @ (&own (ty))); True.
(* Specifications for function [test]. *)
Definition type_of_test :=
......
......@@ -10,39 +10,36 @@ typedef unsigned char tag_t;
//@rc::inlined Notation TAG_MOD := (8%nat) (only parsing).
[[rc::parameters("r: {loc * Z}", "ty: type", "v: val", "P: {iProp Σ}")]]
[[rc::parameters("r: {loc * Z}", "ty: type", "v: val")]]
[[rc::args("at_value<v, r @ &tagged<TAG_MOD, ty>>")]]
[[rc::requires("{AllocAlive ty Own P}", "[P]")]]
[[rc::requires("[type_alive_own ty]")]]
[[rc::returns("{r.2} @ int<u8>")]]
[[rc::ensures("v : r @ &tagged<TAG_MOD, ty>", "{0 ≤ r.2 < TAG_MOD}", "[P]")]]
[[rc::ensures("v : r @ &tagged<TAG_MOD, ty>", "{0 ≤ r.2 < TAG_MOD}")]]
tag_t tag_of(void* p){
return ((uintptr_t) p) % TAG_MOD;
}
[[rc::parameters("r: {loc * Z}", "t: Z", "ty: type", "P: {iProp Σ}")]]
[[rc::parameters("r: {loc * Z}", "t: Z", "ty: type")]]
[[rc::args("r @ &tagged<TAG_MOD, ty>", "t @ int<u8>")]]
[[rc::requires("{0 ≤ t < TAG_MOD}", "{AllocAlive ty Own P}", "[P]")]]
[[rc::requires("{0 ≤ t < TAG_MOD}", "[type_alive_own ty]")]]
[[rc::returns("{(r.1, t)} @ &tagged<TAG_MOD, ty>")]]
[[rc::ensures("[P]")]]
void* tag(void* p, tag_t t){
tag_t old_t = tag_of(p);
return rc_copy_alloc_id((uintptr_t) p - old_t + t, p);
}
[[rc::parameters("r: {loc * Z}", "ty: type", "P: {iProp Σ}")]]
[[rc::parameters("r: {loc * Z}", "ty: type")]]
[[rc::args("r @ &tagged<TAG_MOD, ty>")]]
[[rc::requires("{AllocAlive ty Own P}", "[P]")]]
[[rc::requires("[type_alive_own ty]")]]
[[rc::returns("{r.1} @ &own<ty>")]]
[[rc::ensures("[P]")]]
void* untag(void* p){
return tag(p, 0);
}
[[rc::parameters("r: {loc * Z}", "ty: type", "P: {iProp Σ}")]]
[[rc::parameters("r: {loc * Z}", "ty: type")]]
[[rc::args("r @ &tagged<TAG_MOD, ty>")]]
[[rc::requires("{AllocAlive ty Own P}", "[P]")]]
[[rc::requires("[type_alive_own ty]")]]
[[rc::returns("{r.1} @ &own<ty>")]]
[[rc::ensures("[P]")]]
void* untag2(void* p){
uintptr_t i = (uintptr_t) p;
return rc_copy_alloc_id(i - i % TAG_MOD, p);
......
......@@ -541,9 +541,28 @@ Section typing.
subsume (l ◁ₗ{β} ty) (alloc_alive_loc l) T.
Proof. iIntros "[HP $] Hl". by iApply (alloc_alive_alive with "HP"). Qed.
Global Instance subsume_alloc_alive_inst ty β l P `{!AllocAlive ty β P} :
Subsume (l ◁ₗ{β} ty) (alloc_alive_loc l) :=
Subsume (l ◁ₗ{β} ty) (alloc_alive_loc l) | 5 :=
λ T, i2p (subsume_alloc_alive ty β l P T).
Lemma subsume_alloc_alive_type_alive ty β l T :
type_alive ty β T -
subsume (l ◁ₗ{β} ty) (alloc_alive_loc l) T.
Proof. iIntros "[Ha $] Hl". rewrite /type_alive. by iApply "Ha". Qed.
Global Instance subsume_alloc_alive_type_alive_inst ty β l :
Subsume (l ◁ₗ{β} ty) (alloc_alive_loc l) | 50 :=
λ T, i2p (subsume_alloc_alive_type_alive ty β l T).
Lemma simplify_goal_type_alive ty β P `{!AllocAlive ty β P} T :
T ( P) -
simplify_goal (type_alive ty β) T.
Proof.
iIntros "HT". iExists _. iFrame. rewrite /type_alive. iIntros "#HP !>" (?) "Hl".
by iApply (alloc_alive_alive with "HP Hl").
Qed.
Global Instance simplify_goal_type_alive_inst ty β P `{!AllocAlive ty β P} :
SimplifyGoal (type_alive ty β) (Some 0%N) :=
λ T, i2p (simplify_goal_type_alive ty β P T).
Lemma subsume_loc_in_bounds_leq (l : loc) (n1 n2 : nat) T :
n2 n1%nat T -
subsume (loc_in_bounds l n1) (loc_in_bounds l n2) T.
......
......@@ -336,6 +336,10 @@ Class AllocAlive `{!typeG Σ} (ty : type) (β : own_state) (P : iProp Σ) := {
Arguments alloc_alive_alive {_ _} _ _ _ {_} _.
Hint Mode AllocAlive + + + + - : typeclass_instances.
Definition type_alive `{!typeG Σ} (ty : type) (β : own_state) : iProp Σ :=
( l, ty.(ty_own) β l - alloc_alive_loc l).
Notation type_alive_own ty := (type_alive ty Own).
Section alloc_alive.
Context `{!typeG Σ}.
......@@ -356,11 +360,17 @@ Section alloc_alive.
IntroPersistent (alloc_global l) (alloc_global l).
Proof. constructor. by iIntros "#H !>". Qed.
Global Instance intro_persistent_type_alive ty β:
IntroPersistent (type_alive ty β) (type_alive ty β).
Proof. constructor. by iIntros "#H !>". Qed.
Global Instance AllocAlive_simpl_and ty β P P' `{!AllocAlive ty β P'} `{!IsProtected P} :
SimplAndUnsafe true (AllocAlive ty β P) (λ T, P = P' T).
Proof. by move => T [-> ?]. Qed.
End alloc_alive.
Typeclasses Opaque type_alive.
Notation "l ◁ₗ{ β } ty" := (ty_own ty β l) (at level 15, format "l ◁ₗ{ β } ty") : bi_scope.
Notation "l ◁ₗ ty" := (ty_own ty Own l) (at level 15) : bi_scope.
Notation "v ◁ᵥ ty" := (ty_own_val ty v) (at level 15) : bi_scope.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment