From ddb5ea5b5c431cafb1351963285fa33aa5a09804 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Lennard=20G=C3=A4her?= Date: Sat, 2 Oct 2021 13:51:10 +0200 Subject: [PATCH 1/3] dynamic alloc/free --- theories/lang/ghost_state.v | 4 ++++ theories/lang/lang.v | 30 ++++++++++++++++++++++++++- theories/lang/lifting.v | 41 +++++++++++++++++++++++++++++++++++++ theories/lang/tactics.v | 32 +++++++++++++++++++++++++---- 4 files changed, 102 insertions(+), 5 deletions(-) diff --git a/theories/lang/ghost_state.v b/theories/lang/ghost_state.v index 52345829..e214350d 100644 --- a/theories/lang/ghost_state.v +++ b/theories/lang/ghost_state.v @@ -524,6 +524,10 @@ Section heap. by iDestruct (heap_mapsto_mbyte_agree with "[$]") as %->. Qed. + Lemma heap_mapsto_layout_has_layout l ly : + l ↦|ly| -∗ ⌜l `has_layout_loc` ly⌝. + Proof. iIntros "(% & % & % & ?)". done. Qed. + Lemma heap_alloc_st l h v aid : l.1 = ProvAlloc (Some aid) → heap_range_free h l.2 (length v) → diff --git a/theories/lang/lang.v b/theories/lang/lang.v index 46b80534..5658484f 100644 --- a/theories/lang/lang.v +++ b/theories/lang/lang.v @@ -37,6 +37,7 @@ Inductive expr := | Call (f : expr) (args : list expr) | Concat (es : list expr) | IfE (ot : op_type) (e1 e2 e3 : expr) +| Alloc (ly : layout) (e : expr) | SkipE (e : expr) | StuckE (* stuck expression *) . @@ -53,6 +54,7 @@ Lemma expr_ind (P : expr → Prop) : (∀ (f : expr) (args : list expr), P f → Forall P args → P (Call f args)) → (∀ (es : list expr), Forall P es → P (Concat es)) → (∀ (ot : op_type) (e1 e2 e3 : expr), P e1 → P e2 → P e3 → P (IfE ot e1 e2 e3)) → + (∀ (ly : layout) (e : expr), P e → P (Alloc ly e)) → (∀ (e : expr), P e → P (SkipE e)) → (P StuckE) → ∀ (e : expr), P e. @@ -77,6 +79,7 @@ Inductive stmt := (* m: map from values of e to indices into bs, def: default *) | Switch (it : int_type) (e : expr) (m : gmap Z nat) (bs : list stmt) (def : stmt) | Assign (o : order) (ot : op_type) (e1 e2 : expr) (s : stmt) +| Free (ly : layout) (e : expr) (s : stmt) | SkipS (s : stmt) | StuckS (* stuck statement *) | ExprS (e : expr) (s : stmt) @@ -125,6 +128,7 @@ with rtexpr := | RTCall (f : runtime_expr) (args : list runtime_expr) | RTCAS (ot : op_type) (e1 e2 e3 : runtime_expr) | RTConcat (es : list runtime_expr) +| RTAlloc (ly : layout) (e : runtime_expr) | RTIfE (ot : op_type) (e1 e2 e3 : runtime_expr) | RTSkipE (e : runtime_expr) | RTStuckE @@ -134,6 +138,7 @@ with rtstmt := | RTIfS (ot : op_type) (e : runtime_expr) (s1 s2 : stmt) | RTSwitch (it : int_type) (e : runtime_expr) (m : gmap Z nat) (bs : list stmt) (def : stmt) | RTAssign (o : order) (ot : op_type) (e1 e2 : runtime_expr) (s : stmt) +| RTFree (ly : layout) (e : runtime_expr) (s : stmt) | RTSkipS (s : stmt) | RTStuckS | RTExprS (e : runtime_expr) (s : stmt) @@ -151,6 +156,7 @@ Fixpoint to_rtexpr (e : expr) : runtime_expr := | CAS ot e1 e2 e3 => RTCAS ot (to_rtexpr e1) (to_rtexpr e2) (to_rtexpr e3) | Concat es => RTConcat (to_rtexpr <$> es) | IfE ot e1 e2 e3 => RTIfE ot (to_rtexpr e1) (to_rtexpr e2) (to_rtexpr e3) + | Alloc ly e => RTAlloc ly (to_rtexpr e) | SkipE e => RTSkipE (to_rtexpr e) | StuckE => RTStuckE end. @@ -164,6 +170,7 @@ Definition to_rtstmt (rf : runtime_function) (s : stmt) : runtime_expr := | IfS ot e s1 s2 => RTIfS ot (to_rtexpr e) s1 s2 | Switch it e m bs def => RTSwitch it (to_rtexpr e) m bs def | Assign o ot e1 e2 s => RTAssign o ot (to_rtexpr e1) (to_rtexpr e2) s + | Free ly e s => RTFree ly (to_rtexpr e) s | SkipS s => RTSkipS s | StuckS => RTStuckS | ExprS e s => RTExprS (to_rtexpr e) s @@ -198,6 +205,7 @@ Fixpoint subst (x : var_name) (v : val) (e : expr) : expr := | CAS ly e1 e2 e3 => CAS ly (subst x v e1) (subst x v e2) (subst x v e3) | Concat el => Concat (subst x v <$> el) | IfE ot e1 e2 e3 => IfE ot (subst x v e1) (subst x v e2) (subst x v e3) + | Alloc ly e => Alloc ly (subst x v e) | SkipE e => SkipE (subst x v e) | StuckE => StuckE end. @@ -215,6 +223,7 @@ Fixpoint subst_stmt (xs : list (var_name * val)) (s : stmt) : stmt := | IfS ot e s1 s2 => IfS ot (subst_l xs e) (subst_stmt xs s1) (subst_stmt xs s2) | Switch it e m' bs def => Switch it (subst_l xs e) m' (subst_stmt xs <$> bs) (subst_stmt xs def) | Assign o ot e1 e2 s => Assign o ot (subst_l xs e1) (subst_l xs e2) (subst_stmt xs s) + | Free ly e s => Free ly (subst_l xs e) (subst_stmt xs s) | SkipS s => SkipS (subst_stmt xs s) | StuckS => StuckS | ExprS e s => ExprS (subst_l xs e) (subst_stmt xs s) @@ -459,6 +468,14 @@ comparing pointers? (see lambda rust) *) | IfES v ot e1 e2 b σ: cast_to_bool ot v σ.(st_heap) = Some b → expr_step (IfE ot (Val v) e1 e2) σ [] (if b then e1 else e2) σ [] +| AllocS v l ly σ hs' : + has_layout_val v ly → + has_layout_loc l ly → + alloc_new_block σ.(st_heap) l v hs' → + expr_step (Alloc ly (Val v)) σ [] (Val (val_of_loc l)) {| st_heap := hs'; st_fntbl := σ.(st_fntbl) |} [] +| AllocFailS v ly σ : + has_layout_val v ly → + expr_step (Alloc ly (Val v)) σ [] AllocFailed σ [] (* no rule for StuckE *) . @@ -486,6 +503,11 @@ Inductive stmt_step : stmt → runtime_function → state → list Empty_set → | ReturnS rf σ hs v: free_blocks σ.(st_heap) rf.(rf_locs) hs → (* Deallocate the stack. *) stmt_step (Return (Val v)) rf σ [] (Val v) {| st_fntbl := σ.(st_fntbl); st_heap := hs |} [] +| FreeS ly v l s rf σ hs' : + val_to_loc v = Some l → + has_layout_loc l ly → + free_block σ.(st_heap) l ly hs' → + stmt_step (Free ly (Val v) s) rf σ [] (to_rtstmt rf s) {| st_fntbl := σ.(st_fntbl); st_heap := hs' |} [] | SkipSS rf σ s : stmt_step (SkipS s) rf σ [] (to_rtstmt rf s) σ [] | ExprSS rf σ s v: @@ -514,7 +536,8 @@ Proof. all: repeat select (heap_at _ _ _ _ _) ltac:(fun H => destruct H as [?[?[??]]]). all: try (rewrite /heap_fmap/=; eapply heap_update_heap_state_invariant => //). all: try (unfold has_layout_val in *; by etransitivity). - repeat eapply alloc_new_blocks_invariant => //. + - repeat eapply alloc_new_blocks_invariant => //. + - eapply alloc_new_block_invariant => //. Qed. Lemma stmt_step_preserves_invariant s rf e σ1 σ2 κs efs: @@ -529,6 +552,7 @@ Proof. match goal with H : _ `has_layout_val` _ |- _ => rewrite H end. by destruct o. - move => ??? _ Hfree Hinv. by eapply free_blocks_invariant. + - move => ??? _ _ ???? Hfree Hinv. by eapply free_block_invariant. Qed. Lemma runtime_step_preserves_invariant e1 e2 σ1 σ2 κs efs: @@ -557,6 +581,7 @@ Inductive expr_ectx := | CASRCtx (ot : op_type) (v1 v2 : val) | ConcatCtx (vs : list val) (es : list runtime_expr) | IfECtx (ot : op_type) (e2 e3 : runtime_expr) +| AllocCtx (ly : layout) | SkipECtx . @@ -575,6 +600,7 @@ Definition expr_fill_item (Ki : expr_ectx) (e : runtime_expr) : rtexpr := | CASRCtx ot v1 v2 => RTCAS ot (Val v1) (Val v2) e | ConcatCtx vs es => RTConcat ((Expr <$> (RTVal <$> vs)) ++ e :: es) | IfECtx ot e2 e3 => RTIfE ot e e2 e3 + | AllocCtx ly => RTAlloc ly e | SkipECtx => RTSkipE e end. @@ -584,6 +610,7 @@ Inductive stmt_ectx := | AssignRCtx (o : order) (ot : op_type) (e1 : expr) (s : stmt) | AssignLCtx (o : order) (ot : op_type) (v2 : val) (s : stmt) | ReturnCtx +| FreeCtx (ly : layout) (s : stmt) | IfSCtx (ot : op_type) (s1 s2 : stmt) | SwitchCtx (it : int_type) (m: gmap Z nat) (bs : list stmt) (def : stmt) | ExprSCtx (s : stmt) @@ -594,6 +621,7 @@ Definition stmt_fill_item (Ki : stmt_ectx) (e : runtime_expr) : rtstmt := | AssignRCtx o ot e1 s => RTAssign o ot e1 e s | AssignLCtx o ot v2 s => RTAssign o ot e (Val v2) s | ReturnCtx => RTReturn e + | FreeCtx ly s => RTFree ly e s | IfSCtx ot s1 s2 => RTIfS ot e s1 s2 | SwitchCtx it m bs def => RTSwitch it e m bs def | ExprSCtx s => RTExprS e s diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v index c6b9aafb..80ad9eb3 100644 --- a/theories/lang/lifting.v +++ b/theories/lang/lifting.v @@ -784,6 +784,26 @@ Proof. by iApply (wp_call_bind_ind []). Qed. +Lemma wp_alloc E Φ (l : loc) ly (v : val) : + has_layout_val v ly → + ▷ (∀ l, l ↦ v -∗ freeable l (length v) -∗ ⌜l `has_layout_loc` ly⌝ -∗ Φ (val_of_loc l)) -∗ + WP (Alloc ly (Val v)) @ E {{ Φ }}. +Proof. + iIntros (Hly) "Hwp". + iApply wp_lift_expr_step; first done. + iIntros (hs) "((%&Hhctx&Hactx)&Hfctx)/=". + iModIntro. + iSplit; first by eauto 10 using AllocFailS. + iIntros (??[??]? Hstep _) "!>". inv_expr_step; last first. { + (* Alloc failure case. *) + iModIntro. iSplit; first done. rewrite /state_ctx. iFrame. iSplit; first done. + iApply wp_alloc_failed. + } + iMod (heap_alloc_new_block_upd with "[$Hhctx $Hactx]") as "(Hctx & Hlv & Hlf)" => //. + iDestruct ("Hwp" with "Hlv Hlf [//]") as "Hpost". + iModIntro. iSplit => //. + iFrame "Hctx Hfctx". by iApply wp_value. +Qed. End expr_lifting. (*** Lifting of statements *) @@ -907,6 +927,27 @@ Proof. iSplit; first done. iFrame. by iApply "HWP". Qed. +Lemma wps_free Q Ψ s l ly : + l ↦|ly| -∗ + freeable l (ly.(ly_size)) -∗ + ▷ WPs s {{ Q, Ψ }} -∗ + WPs (Free ly (val_of_loc l) s) {{ Q, Ψ }}. +Proof. + iIntros "Hl Hf HWP". rewrite !stmt_wp_unfold. iIntros (???) "?". subst. + iPoseProof (heap_mapsto_layout_has_layout with "Hl") as "%". + iApply wp_lift_stmt_step. iIntros (σ) "(Hhctx&Hfctx)". + iMod (heap_free_block_upd with "Hl Hf Hhctx") as (σ') "(%Hf & Hhctx)". + iModIntro. iSplit; first by eauto 10 using FreeS, val_to_of_loc. + iNext. iIntros (???? Hstep ?). inv_stmt_step. iModIntro. + iSplitR; first done. + match goal with + | H : val_to_loc _ = Some ?l |- _ => apply val_of_to_loc in H; injection H; intros <-; intros + end. + rewrite (free_block_inj σ.(st_heap) l ly hs' σ'); [ | done..]. + iFrame. + by iApply "HWP". +Qed. + Lemma wps_skip Q Ψ s: (|={⊤}[∅]▷=> WPs s {{ Q, Ψ }}) -∗ WPs SkipS s {{ Q , Ψ }}. Proof. diff --git a/theories/lang/tactics.v b/theories/lang/tactics.v index 72bc68a7..1032e81d 100644 --- a/theories/lang/tactics.v +++ b/theories/lang/tactics.v @@ -18,6 +18,7 @@ Inductive expr := | Call (f : expr) (args : list expr) | Concat (es : list expr) | IfE (op : op_type) (e1 e2 e3 : expr) +| Alloc (ly : layout) (e : expr) | SkipE (e : expr) | StuckE (* new constructors *) @@ -51,6 +52,7 @@ Lemma expr_ind (P : expr → Prop) : (∀ (f : expr) (args : list expr), P f → Forall P args → P (Call f args)) → (∀ (es : list expr), Forall P es → P (Concat es)) → (∀ (ot : op_type) (e1 e2 e3 : expr), P e1 → P e2 → P e3 → P (IfE ot e1 e2 e3)) → + (∀ (ly : layout) (e : expr), P e → P (Alloc ly e)) → (∀ (e : expr), P e → P (SkipE e)) → (P StuckE) → (∀ (ot1 ot2 : op_type) (rit : int_type) (e1 e2 : expr), P e1 → P e2 → P (LogicalAnd ot1 ot2 rit e1 e2)) → @@ -69,17 +71,17 @@ Lemma expr_ind (P : expr → Prop) : (∀ (e : lang.expr), P (Expr e)) → ∀ (e : expr), P e. Proof. move => *. generalize dependent P => P. match goal with | e : expr |- _ => revert e end. - fix FIX 1. move => [ ^e] => ???????? Hcall Hconcat ?????????????? Hstruct Hmacro ?. + fix FIX 1. move => [ ^e] => ???????? Hcall Hconcat ??????????????? Hstruct Hmacro ?. 9: { apply Hcall; [ |apply Forall_true => ?]; by apply: FIX. } 9: { apply Hconcat. apply Forall_true => ?. by apply: FIX. } - 23: { + 24: { apply Hstruct. apply Forall_fmap. apply Forall_true => ?. by apply: FIX. } - 23: { + 24: { apply Hmacro. apply Forall_true => ?. by apply: FIX. } all: auto. @@ -98,6 +100,7 @@ Fixpoint to_expr (e : expr) : lang.expr := | Call f args => lang.Call (to_expr f) (to_expr <$> args) | Concat es => lang.Concat (to_expr <$> es) | IfE ot e1 e2 e3 => lang.IfE ot (to_expr e1) (to_expr e2) (to_expr e3) + | Alloc ly e => lang.Alloc ly (to_expr e) | SkipE e => lang.SkipE (to_expr e) | StuckE => lang.StuckE | LogicalAnd ot1 ot2 rit e1 e2 => notation.LogicalAnd ot1 ot2 rit (to_expr e1) (to_expr e2) @@ -175,6 +178,8 @@ Ltac of_expr e := let e2 := of_expr e2 in let e3 := of_expr e3 in constr:(IfE ot e1 e2 e3) + | lang.Alloc ?ly ?e => + let e := of_expr e in constr:(Alloc ly e) | lang.SkipE ?e => let e := of_expr e in constr:(SkipE e) | lang.StuckE => constr:(StuckE e) @@ -203,6 +208,7 @@ Inductive ectx_item := | CallRCtx (f : val) (vl : list val) (el : list expr) | ConcatCtx (vs : list val) (es : list expr) | IfECtx (ot : op_type) (e2 e3 : expr) +| AllocCtx (ly : layout) | SkipECtx (* new constructors *) | UseCtx (o : order) (ot : op_type) @@ -231,6 +237,7 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr := | CallRCtx f vl el => Call (Val f) ((Val <$> vl) ++ e :: el) | ConcatCtx vs es => Concat ((Val <$> vs) ++ e :: es) | IfECtx ot e2 e3 => IfE ot e e2 e3 + | AllocCtx ly => Alloc ly e | SkipECtx => SkipE e | UseCtx o l => Use o l e | AddrOfCtx => AddrOf e @@ -283,6 +290,9 @@ Fixpoint find_expr_fill (e : expr) (bind_val : bool) : option (list ectx_item * | IfE ot e1 e2 e3 => if find_expr_fill e1 bind_val is Some (Ks, e') then Some (Ks ++ [IfECtx ot e2 e3], e') else Some ([], e) + | Alloc ly e1 => + if find_expr_fill e1 bind_val is Some (Ks, e') then + Some (Ks ++ [AllocCtx ly], e') else Some ([], e) | SkipE e1 => if find_expr_fill e1 bind_val is Some (Ks, e') then Some (Ks ++ [SkipECtx], e') else Some ([], e) @@ -333,6 +343,7 @@ Proof. apply: [lang.CallRCtx _ _ _]| apply: [lang.ConcatCtx _ _]| apply: [lang.IfECtx _ _ _]| + apply: [lang.AllocCtx _]| apply: [lang.SkipECtx]| apply: [lang.DerefCtx _ _]| apply: []| @@ -342,7 +353,7 @@ Proof. apply: [lang.BinOpRCtx _ _ _ _]| apply: []|.. ]). - move: K => [|||||||||||||||||n|||] * //=. + move: K => [||||||||||||||||||n|||] * //=. - (** Call *) do 2 f_equal. rewrite !fmap_app !fmap_cons. repeat f_equal; eauto. @@ -370,6 +381,7 @@ Inductive stmt := | IfS (ot : op_type) (e : expr) (s1 s2 : stmt) | Switch (it : int_type) (e : expr) (m : gmap Z nat) (bs : list stmt) (def : stmt) | Assign (o : order) (ot : op_type) (e1 e2 : expr) (s : stmt) +| Free (ly : layout) (e : expr) (s : stmt) | SkipS (s : stmt) | StuckS | ExprS (e : expr) (s : stmt) @@ -387,6 +399,7 @@ Lemma stmt_ind (P : stmt → Prop): (∀ (ot : op_type) (e : expr) (s1 : stmt), P s1 → ∀ s2 : stmt, P s2 → P (IfS ot e s1 s2)) → (∀ (it : int_type) (e : expr) (m : gmap Z nat) (bs : list stmt) (def : stmt), P def → Forall P bs → P (Switch it e m bs def)) → (∀ (o : order) (ot : op_type) (e1 e2 : expr) (s : stmt), P s → P (Assign o ot e1 e2 s)) → + (∀ (ly : layout) (e : expr) (s : stmt), P s → P (Free ly e s)) → (∀ s : stmt, P s → P (SkipS s)) → (P StuckS) → (∀ (e : expr) (s : stmt), P s → P (ExprS e s)) → @@ -410,6 +423,7 @@ Fixpoint to_stmt (s : stmt) : lang.stmt := | IfS ot e s1 s2 => (if{ot}: to_expr e then to_stmt s1 else to_stmt s2)%E | Switch it e m bs def => lang.Switch it (to_expr e) m (to_stmt <$> bs) (to_stmt def) | Assign o ot e1 e2 s => lang.Assign o ot (to_expr e1) (to_expr e2) (to_stmt s) + | Free ly e s => lang.Free ly (to_expr e) (to_stmt s) | SkipS s => lang.SkipS (to_stmt s) | StuckS => lang.StuckS | ExprS e s => lang.ExprS (to_expr e) (to_stmt s) @@ -455,6 +469,10 @@ Ltac of_stmt s := let e2 := of_expr e2 in let s := of_stmt s in constr:(Assign o ot e1 e2 s) + | lang.Free ?ly ?e ?s => + let e := of_expr e in + let s := of_stmt s in + constr:(Free ly e s) | lang.SkipS ?s => let s := of_stmt s in constr:(SkipS s) @@ -474,6 +492,7 @@ Inductive stmt_ectx := | SwitchCtx (it : int_type) (m: gmap Z nat) (bs : list stmt) (def : stmt) | ExprSCtx (s : stmt) | AssertCtx (ot : op_type) (s : stmt) +| FreeCtx (ly : layout) (s : stmt) . Definition stmt_fill (Ki : stmt_ectx) (e : expr) : stmt := @@ -485,6 +504,7 @@ Definition stmt_fill (Ki : stmt_ectx) (e : expr) : stmt := | IfSCtx ot s1 s2 => IfS ot e s1 s2 | SwitchCtx it m bs def => Switch it e m bs def | AssertCtx ot s => Assert ot e s + | FreeCtx ly s => Free ly e s end. Definition find_stmt_fill (s : stmt) : option (stmt_ectx * expr) := @@ -496,6 +516,7 @@ Definition find_stmt_fill (s : stmt) : option (stmt_ectx * expr) := | Switch it e m bs def => if e is (Val v) then None else Some (SwitchCtx it m bs def, e) | Assign o ot e1 e2 s => if e2 is (Val v) then if e1 is (Val v) then None else Some (AssignLCtx o ot v s, e1) else Some (AssignRCtx o ot e1 s, e2) | Assert ot e s => if e is (Val v) then None else Some (AssertCtx ot s, e) + | Free ly e s => if e is (Val v) then None else Some (FreeCtx ly s, e) end. Lemma find_stmt_fill_correct s Ks e: @@ -515,6 +536,7 @@ Proof. eexists ([StmtCtx (lang.SwitchCtx _ _ _ _) rf])| eexists ([StmtCtx (lang.ExprSCtx _) rf])| eexists ([StmtCtx (lang.IfSCtx _ _ _) rf])| + eexists ([StmtCtx (lang.FreeCtx _ _) rf])| ..] => //=. Qed. @@ -532,6 +554,7 @@ Fixpoint subst_l (xs : list (var_name * val)) (e : expr) : expr := | Call f args => Call (subst_l xs f) (subst_l xs <$> args) | Concat es => Concat (subst_l xs <$> es) | IfE ot e1 e2 e3 => IfE ot (subst_l xs e1) (subst_l xs e2) (subst_l xs e3) + | Alloc ly e => Alloc ly (subst_l xs e) | SkipE e => SkipE (subst_l xs e) | StuckE => StuckE | LogicalAnd ot1 ot2 rit e1 e2 => LogicalAnd ot1 ot2 rit (subst_l xs e1) (subst_l xs e2) @@ -621,6 +644,7 @@ Fixpoint subst_stmt (xs : list (var_name * val)) (s : stmt) : stmt := | IfS ot e s1 s2 => IfS ot (subst_l xs e) (subst_stmt xs s1) (subst_stmt xs s2) | Switch it e m' bs def => Switch it (subst_l xs e) m' (subst_stmt xs <$> bs) (subst_stmt xs def) | Assign o ot e1 e2 s => Assign o ot (subst_l xs e1) (subst_l xs e2) (subst_stmt xs s) + | Free ly e s => Free ly (subst_l xs e) (subst_stmt xs s) | SkipS s => SkipS (subst_stmt xs s) | StuckS => StuckS | ExprS e s => ExprS (subst_l xs e) (subst_stmt xs s) -- GitLab From c61e4490bac1214ef20d9b8add1d2e709827bf4e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Lennard=20G=C3=A4her?= Date: Tue, 5 Oct 2021 18:21:51 +0200 Subject: [PATCH 2/3] alloc kind: either heap or stack allocations --- theories/lang/ghost_state.v | 60 ++++++++++---------- theories/lang/heap.v | 104 +++++++++++++++++++---------------- theories/lang/lang.v | 10 ++-- theories/lang/lifting.v | 6 +- theories/typing/adequacy.v | 8 +-- tutorial/adequacy/adequacy.v | 2 +- 6 files changed, 100 insertions(+), 90 deletions(-) diff --git a/theories/lang/ghost_state.v b/theories/lang/ghost_state.v index e214350d..b62ffe2c 100644 --- a/theories/lang/ghost_state.v +++ b/theories/lang/ghost_state.v @@ -22,7 +22,7 @@ Definition heapUR : ucmra := Class heapG Σ := HeapG { heap_heap_inG :> inG Σ (authR heapUR); heap_heap_name : gname; - heap_alloc_range_map_inG :> ghost_mapG Σ alloc_id (Z * nat); + heap_alloc_range_map_inG :> ghost_mapG Σ alloc_id (Z * nat * alloc_kind); heap_alloc_range_map_name : gname; heap_alloc_alive_map_inG :> ghost_mapG Σ alloc_id bool; heap_alloc_alive_map_name : gname; @@ -39,10 +39,10 @@ Definition to_heap_cellR (hc : heap_cell) : heap_cellR := Definition to_heapUR : heap → heapUR := fmap to_heap_cellR. -Definition to_alloc_rangeR (al : allocation) : (Z * nat) := - (al.(al_start), al.(al_len)). +Definition to_alloc_rangeR (al : allocation) : (Z * nat * alloc_kind) := + (al.(al_start), al.(al_len), al.(al_kind)). -Definition to_alloc_range_map : allocs → gmap alloc_id (Z * nat) := +Definition to_alloc_range_map : allocs → gmap alloc_id (Z * nat * alloc_kind) := fmap to_alloc_rangeR. Definition to_alloc_alive_map : allocs → gmap alloc_id bool := @@ -156,8 +156,8 @@ Section definitions. (** * Freeable *) - Definition freeable_def (l : loc) (n : nat) : iProp Σ := - ∃ id, ⌜l.1 = ProvAlloc (Some id)⌝ ∗ alloc_range id {| al_start := l.2; al_len := n; al_alive := true |} ∗ + Definition freeable_def (l : loc) (n : nat) (k : alloc_kind) : iProp Σ := + ∃ id, ⌜l.1 = ProvAlloc (Some id)⌝ ∗ alloc_range id {| al_start := l.2; al_len := n; al_alive := true; al_kind := k |} ∗ alloc_alive id (DfracOwn 1) true. Definition freeable_aux : seal (@freeable_def). by eexists. Qed. Definition freeable := unseal freeable_aux. @@ -247,13 +247,14 @@ Section alloc_range. Lemma alloc_range_mono id a1 a2 : alloc_same_range a1 a2 → + a1.(al_kind) = a2.(al_kind) → alloc_range id a1 -∗ alloc_range id a2. - Proof. destruct a1 as [???], a2 as [???] => -[/= <- <-]. by rewrite alloc_range_eq. Qed. + Proof. destruct a1 as [????], a2 as [????] => -[/= <- <-] <-. by rewrite alloc_range_eq. Qed. Lemma alloc_range_agree id a1 a2 : alloc_range id a1 -∗ alloc_range id a2 -∗ ⌜alloc_same_range a1 a2⌝. Proof. - destruct a1 as [???], a2 as [???]. rewrite alloc_range_eq /alloc_same_range. + destruct a1 as [????], a2 as [????]. rewrite alloc_range_eq /alloc_same_range. iIntros "H1 H2". by iDestruct (ghost_map_elem_agree with "H1 H2") as %[=->->]. Qed. @@ -280,20 +281,21 @@ Section alloc_range. Lemma alloc_range_lookup am id al : alloc_range_ctx am -∗ alloc_range id al -∗ - ⌜∃ al', am !! id = Some al' ∧ alloc_same_range al al'⌝. + ⌜∃ al', am !! id = Some al' ∧ alloc_same_range al al' ∧ al.(al_kind) = al'.(al_kind)⌝. Proof. rewrite alloc_range_eq. iIntros "Htbl Hf". iDestruct (ghost_map_lookup with "Htbl Hf") as %Hlookup. - iPureIntro. move: Hlookup. rewrite lookup_fmap fmap_Some => -[[???][?[??]]]. + iPureIntro. move: Hlookup. rewrite lookup_fmap fmap_Some => -[[????][?[???]]]. by eexists _. Qed. Lemma alloc_range_ctx_same_range am id al1 al2 : am !! id = Some al1 → alloc_same_range al1 al2 → + al1.(al_kind) = al2.(al_kind) → alloc_range_ctx am = alloc_range_ctx (<[id := al2]> am). Proof. - move => Hid [Heq1 Heq2]. + move => Hid [Heq1 Heq2] Heq3. rewrite /alloc_range_ctx /to_alloc_range_map fmap_insert insert_id; first done. rewrite lookup_fmap Hid /=. destruct al1, al2; naive_solver. Qed. @@ -387,7 +389,7 @@ Section loc_in_bounds. Proof. rewrite loc_in_bounds_eq. iIntros "Hb ((?&?&Hctx&?)&?)". iDestruct "Hb" as (id al ????) "Hb". - iDestruct (alloc_range_lookup with "Hctx Hb") as %[al' [?[??]]]. + iDestruct (alloc_range_lookup with "Hctx Hb") as %[al' [?[[??]?]]]. iExists id, al'. iPureIntro. unfold allocation_in_range, al_end in *. naive_solver lia. Qed. @@ -564,7 +566,7 @@ Section heap. heap_ctx h ==∗ heap_ctx (heap_alloc l.2 v id h) ∗ l ↦ v ∗ - freeable l (length v). + freeable l (length v) al.(al_kind). Proof. iIntros (Hid Hfree Hstart Hlen Hrange) "#Hr Hal Hctx". iMod (heap_alloc_st with "Hctx") as "[$ Hl]" => //. @@ -843,11 +845,11 @@ End alloc_alive. Section alloc_new_blocks. Context `{!heapG Σ}. - Lemma heap_alloc_new_block_upd σ1 l v σ2: - alloc_new_block σ1 l v σ2 → - heap_state_ctx σ1 ==∗ heap_state_ctx σ2 ∗ l ↦ v ∗ freeable l (length v). + Lemma heap_alloc_new_block_upd σ1 l v kind σ2: + alloc_new_block σ1 kind l v σ2 → + heap_state_ctx σ1 ==∗ heap_state_ctx σ2 ∗ l ↦ v ∗ freeable l (length v) kind. Proof. - move => []; clear. move => σ l aid v alloc Haid ???; subst alloc. + move => []; clear. move => σ l aid kind v alloc Haid ???; subst alloc. iIntros "Hctx". iDestruct "Hctx" as (Hinv) "(Hhctx&Hrctx&Hsctx)". iMod (alloc_range_alloc with "Hrctx") as "[$ #Hb]" => //. iMod (alloc_alive_alloc with "Hsctx") as "[$ Hs]" => //. @@ -857,11 +859,11 @@ Section alloc_new_blocks. iModIntro. iFrame. iPureIntro. by eapply alloc_new_block_invariant. Qed. - Lemma heap_alloc_new_blocks_upd σ1 ls vs σ2: - alloc_new_blocks σ1 ls vs σ2 → + Lemma heap_alloc_new_blocks_upd σ1 ls vs kind σ2: + alloc_new_blocks σ1 kind ls vs σ2 → heap_state_ctx σ1 ==∗ heap_state_ctx σ2 ∗ - [∗ list] l; v ∈ ls; vs, l ↦ v ∗ freeable l (length v). + [∗ list] l; v ∈ ls; vs, l ↦ v ∗ freeable l (length v) kind. Proof. move => alloc. iInduction alloc as [σ|] "IH"; first by iIntros "$ !>". iIntros "Hσ". @@ -873,27 +875,27 @@ End alloc_new_blocks. Section free_blocks. Context `{!heapG Σ}. - Lemma heap_free_block_upd σ1 l ly: + Lemma heap_free_block_upd σ1 l ly kind: l ↦|ly| -∗ - freeable l (ly_size ly) -∗ - heap_state_ctx σ1 ==∗ ∃ σ2, ⌜free_block σ1 l ly σ2⌝ ∗ heap_state_ctx σ2. + freeable l (ly_size ly) kind -∗ + heap_state_ctx σ1 ==∗ ∃ σ2, ⌜free_block σ1 kind l ly σ2⌝ ∗ heap_state_ctx σ2. Proof. iIntros "Hl Hfree (Hinv&Hhctx&Hrctx&Hsctx)". iDestruct "Hinv" as %Hinv. rewrite freeable_eq. iDestruct "Hfree" as (aid Haid) "[#Hrange Hkill]". iDestruct "Hl" as (v Hv ?) "Hl". - iDestruct (alloc_alive_lookup with "Hsctx Hkill") as %[[???] [??]]. - iDestruct (alloc_range_lookup with "Hrctx Hrange") as %[al'' [?[??]]]. simplify_eq/=. + iDestruct (alloc_alive_lookup with "Hsctx Hkill") as %[[????k] [??]]. + iDestruct (alloc_range_lookup with "Hrctx Hrange") as %[al'' [?[[??]?]]]. simplify_eq/=. iDestruct (heap_mapsto_lookup_1 (λ st : lock_state, st = RSt 0) with "Hhctx Hl") as %? => //. iExists _. iSplitR. { iPureIntro. by econstructor. } iMod (heap_free_free with "Hhctx Hl") as "Hhctx". rewrite Hv. iFrame => /=. - iMod (alloc_alive_kill _ _ ({| al_start := l.2; al_len := ly_size ly; al_alive := true |}) with "Hsctx Hkill") as "[$ Hd]". + iMod (alloc_alive_kill _ _ ({| al_start := l.2; al_len := ly_size ly; al_alive := true; al_kind := k |}) with "Hsctx Hkill") as "[$ Hd]". erewrite alloc_range_ctx_same_range; [iFrame |done..]. iPureIntro. eapply free_block_invariant => //. by eapply FreeBlock. Qed. - Lemma heap_free_blocks_upd ls σ1: - ([∗ list] l ∈ ls, l.1 ↦|l.2| ∗ freeable l.1 (ly_size l.2)) -∗ - heap_state_ctx σ1 ==∗ ∃ σ2, ⌜free_blocks σ1 ls σ2⌝ ∗ heap_state_ctx σ2. + Lemma heap_free_blocks_upd ls σ1 kind: + ([∗ list] l ∈ ls, l.1 ↦|l.2| ∗ freeable l.1 (ly_size l.2) kind ) -∗ + heap_state_ctx σ1 ==∗ ∃ σ2, ⌜free_blocks σ1 kind ls σ2⌝ ∗ heap_state_ctx σ2. Proof. iInduction ls as [|[l ly] ls] "IH" forall (σ1). { iIntros "_ ? !>". iExists σ1. iFrame. iPureIntro. by constructor. } diff --git a/theories/lang/heap.v b/theories/lang/heap.v index 9aa9a70c..3411ac50 100644 --- a/theories/lang/heap.v +++ b/theories/lang/heap.v @@ -185,11 +185,17 @@ Qed. (** ** Representation of allocations. *) +(** An allocation can either be a stack allocation or a heap allocation. *) +Inductive alloc_kind : Set := + | HeapAlloc + | StackAlloc. + Record allocation := Allocation { - al_start : Z; (* First valid address. *) - al_len : nat; (* Number of allocated byte. *) - al_alive : bool; (* Is the allocation still alive. *) + al_start : Z; (* First valid address. *) + al_len : nat; (* Number of allocated byte. *) + al_alive : bool; (* Is the allocation still alive. *) + al_kind : alloc_kind; (* On the heap or on the stack? *) }. Definition al_end (al : allocation) : Z := @@ -201,7 +207,7 @@ Definition alloc_same_range (al1 al2 : allocation) : Prop := al1.(al_start) = al2.(al_start) ∧ al1.(al_len) = al2.(al_len). Definition killed (al : allocation) : allocation := - {| al_start := al.(al_start); al_len := al.(al_len); al_alive := false; |}. + {| al_start := al.(al_start); al_len := al.(al_len); al_alive := false; al_kind := al.(al_kind) |}. (** Smallest allocatable address (we reserve 0 for NULL). *) Definition min_alloc_start : Z := 1. @@ -262,6 +268,8 @@ Proof. rewrite /valid_ptr => ?. apply: heap_state_loc_in_bounds_has_alloc_id. na Definition addr_in_range_alloc (a : addr) (aid : alloc_id) (st : heap_state) : Prop := ∃ alloc, st.(hs_allocs) !! aid = Some alloc ∧ a ∈ alloc. +Global Instance alloc_kind_eq_dec : EqDecision alloc_kind. +Proof. solve_decision. Qed. Global Instance allocation_eq_dec : EqDecision (allocation). Proof. solve_decision. Qed. Global Instance alloc_id_alive_dec aid st : Decision (alloc_id_alive aid st). @@ -474,57 +482,57 @@ Arguments mem_cast : simpl never. (** ** Allocation and deallocation. *) -Inductive alloc_new_block : heap_state → loc → val → heap_state → Prop := -| AllocNewBlock σ l aid v: - let alloc := Allocation l.2 (length v) true in +Inductive alloc_new_block : heap_state → alloc_kind → loc → val → heap_state → Prop := +| AllocNewBlock σ l aid kind v: + let alloc := Allocation l.2 (length v) true kind in l.1 = ProvAlloc (Some aid) → σ.(hs_allocs) !! aid = None → allocation_in_range alloc → heap_range_free σ.(hs_heap) l.2 (length v) → - alloc_new_block σ l v {| + alloc_new_block σ kind l v {| hs_heap := heap_alloc l.2 v aid σ.(hs_heap); hs_allocs := <[aid := alloc]> σ.(hs_allocs); |}. -Inductive alloc_new_blocks : heap_state → list loc → list val → heap_state → Prop := -| AllocNewBlock_nil σ : - alloc_new_blocks σ [] [] σ -| AllocNewBlock_cons σ σ' σ'' l v ls vs : - alloc_new_block σ l v σ' → - alloc_new_blocks σ' ls vs σ'' → - alloc_new_blocks σ (l :: ls) (v :: vs) σ''. - -Inductive free_block : heap_state → loc → layout → heap_state → Prop := -| FreeBlock σ l aid ly v: - let al_alive := Allocation l.2 ly.(ly_size) true in - let al_dead := Allocation l.2 ly.(ly_size) false in +Inductive alloc_new_blocks : heap_state → alloc_kind → list loc → list val → heap_state → Prop := +| AllocNewBlock_nil σ kind : + alloc_new_blocks σ kind [] [] σ +| AllocNewBlock_cons σ σ' σ'' l v ls kind vs : + alloc_new_block σ kind l v σ' → + alloc_new_blocks σ' kind ls vs σ'' → + alloc_new_blocks σ kind (l :: ls) (v :: vs) σ''. + +Inductive free_block : heap_state → alloc_kind → loc → layout → heap_state → Prop := +| FreeBlock σ l aid ly kind v: + let al_alive := Allocation l.2 ly.(ly_size) true kind in + let al_dead := Allocation l.2 ly.(ly_size) false kind in l.1 = ProvAlloc (Some aid) → σ.(hs_allocs) !! aid = Some al_alive → length v = ly.(ly_size) → heap_lookup_loc l v (λ st, st = RSt 0%nat) σ.(hs_heap) → - free_block σ l ly {| + free_block σ kind l ly {| hs_heap := heap_free l.2 ly.(ly_size) σ.(hs_heap); hs_allocs := <[aid := al_dead]> σ.(hs_allocs); |}. -Inductive free_blocks : heap_state → list (loc * layout) → heap_state → Prop := -| FreeBlocks_nil σ : - free_blocks σ [] σ -| FreeBlocks_cons σ σ' σ'' l ly ls : - free_block σ l ly σ' → - free_blocks σ' ls σ'' → - free_blocks σ ((l, ly) :: ls) σ''. +Inductive free_blocks : heap_state → alloc_kind → list (loc * layout) → heap_state → Prop := +| FreeBlocks_nil σ kind : + free_blocks σ kind [] σ +| FreeBlocks_cons σ σ' σ'' l ly kind ls : + free_block σ kind l ly σ' → + free_blocks σ' kind ls σ'' → + free_blocks σ kind ((l, ly) :: ls) σ''. -Lemma free_block_inj hs l ly hs1 hs2: - free_block hs l ly hs1 → free_block hs l ly hs2 → hs1 = hs2. +Lemma free_block_inj hs l ly kind hs1 hs2: + free_block hs kind l ly hs1 → free_block hs kind l ly hs2 → hs1 = hs2. Proof. destruct l. inversion 1; simplify_eq. by inversion 1; simplify_eq/=. Qed. -Lemma free_blocks_inj hs1 hs2 hs ls: - free_blocks hs ls hs1 → free_blocks hs ls hs2 → hs1 = hs2. +Lemma free_blocks_inj hs1 hs2 hs kind ls: + free_blocks hs kind ls hs1 → free_blocks hs kind ls hs2 → hs1 = hs2. Proof. move Heq: {1}(hs) => hs' Hb. - elim: Hb hs Heq. { move => ?? ->. by inversion 1. } - move => ?????? Hb1 ? IH ??. + elim: Hb hs Heq. { move => ??? ->. by inversion 1. } + move => ??????? Hb1 ? IH ??. inversion 1; simplify_eq. apply: IH; [|done]. by apply: free_block_inj. Qed. @@ -580,25 +588,25 @@ Definition heap_state_invariant (st : heap_state) : Prop := (** ** Lemmas about the heap state invariant. *) -Lemma heap_state_alloc_alive_free_disjoint σ id a n b alloc: +Lemma heap_state_alloc_alive_free_disjoint σ id a n b kind alloc: heap_state_alloc_alive_in_heap σ → alloc_id_alive id σ → heap_range_free σ.(hs_heap) a n → σ.(hs_allocs) !! id = Some alloc → - Allocation a n b ## alloc. + Allocation a n b kind ## alloc. Proof. move => Hin_heap Halive Hfree Hal p Hp1 Hp2. apply (Hin_heap _ _ Hal Halive) in Hp2 as [? Hp2]. rewrite Hfree in Hp2; first done. apply Hp1. Qed. -Lemma alloc_new_block_invariant σ1 σ2 l v : - alloc_new_block σ1 l v σ2 → +Lemma alloc_new_block_invariant σ1 σ2 l v kind : + alloc_new_block σ1 kind l v σ2 → heap_state_invariant σ1 → heap_state_invariant σ2. Proof. move => []; clear. - move => σ1 l aid v alloc Haid Hfresh Halloc Hrange H. + move => σ1 l aid kind v alloc Haid Hfresh Halloc Hrange H. destruct H as (Hi1&Hi2&Hi3&Hi4&Hi5). split_and!. - move => a [id??] /= Ha. destruct (decide (aid = id)) as [->|Hne]. + exists alloc. split => /=; first by rewrite lookup_insert. @@ -650,22 +658,22 @@ Proof. eapply (Hi5 _ _ Hal); [by eexists | done |..]. Qed. -Lemma alloc_new_blocks_invariant σ1 σ2 ls vs : - alloc_new_blocks σ1 ls vs σ2 → +Lemma alloc_new_blocks_invariant σ1 σ2 ls vs kind : + alloc_new_blocks σ1 kind ls vs σ2 → heap_state_invariant σ1 → heap_state_invariant σ2. Proof. - elim => [] // ??????? Hb Hbs IH H. + elim => [] // ???????? Hb Hbs IH H. apply IH. by eapply alloc_new_block_invariant. Qed. -Lemma free_block_invariant σ1 σ2 l ly: - free_block σ1 l ly σ2 → +Lemma free_block_invariant σ1 σ2 l ly kind : + free_block σ1 kind l ly σ2 → heap_state_invariant σ1 → heap_state_invariant σ2. Proof. move => []; clear. - move => σ l aid ly v al_a al_d Haid Hal_a Hlen Hlookup H. + move => σ l aid ly kind v al_a al_d Haid Hal_a Hlen Hlookup H. destruct H as (Hi1&Hi2&Hi3&Hi4&Hi5). split_and!. - move => a hc /= Hhc. assert (¬ (l.2 ≤ a < l.2 + length v)) as Hnot_in. @@ -712,12 +720,12 @@ Proof. erewrite elem_of_disjoint in Hdisj. by eapply Hdisj. Qed. -Lemma free_blocks_invariant σ1 σ2 ls: - free_blocks σ1 ls σ2 → +Lemma free_blocks_invariant σ1 σ2 ls kind : + free_blocks σ1 kind ls σ2 → heap_state_invariant σ1 → heap_state_invariant σ2. Proof. - elim => [] // ?????? Hb Hbs IH H. + elim => [] // ??????? Hb Hbs IH H. apply IH. by eapply free_block_invariant. Qed. diff --git a/theories/lang/lang.v b/theories/lang/lang.v index 5658484f..c48b93ea 100644 --- a/theories/lang/lang.v +++ b/theories/lang/lang.v @@ -446,9 +446,9 @@ comparing pointers? (see lambda rust) *) Forall2 has_layout_loc lsa fn.(f_args).*2 → Forall2 has_layout_loc lsv fn.(f_local_vars).*2 → (* initialize the local vars to poison *) - alloc_new_blocks σ.(st_heap) lsv ((λ p, replicate p.2.(ly_size) MPoison) <$> fn.(f_local_vars)) hs' → + alloc_new_blocks σ.(st_heap) StackAlloc lsv ((λ p, replicate p.2.(ly_size) MPoison) <$> fn.(f_local_vars)) hs' → (* initialize the arguments with the supplied values *) - alloc_new_blocks hs' lsa vs hs'' → + alloc_new_blocks hs' StackAlloc lsa vs hs'' → (* add used blocks allocations *) rf = {| rf_fn := fn'; rf_locs := zip lsa fn.(f_args).*2 ++ zip lsv fn.(f_local_vars).*2; |} → expr_step (Call (Val vf) (Val <$> vs)) σ [] (to_rtstmt rf (Goto fn'.(f_init))) {| st_heap := hs''; st_fntbl := σ.(st_fntbl)|} [] @@ -471,7 +471,7 @@ comparing pointers? (see lambda rust) *) | AllocS v l ly σ hs' : has_layout_val v ly → has_layout_loc l ly → - alloc_new_block σ.(st_heap) l v hs' → + alloc_new_block σ.(st_heap) HeapAlloc l v hs' → expr_step (Alloc ly (Val v)) σ [] (Val (val_of_loc l)) {| st_heap := hs'; st_fntbl := σ.(st_fntbl) |} [] | AllocFailS v ly σ : has_layout_val v ly → @@ -501,12 +501,12 @@ Inductive stmt_step : stmt → runtime_function → state → list Empty_set → rf.(rf_fn).(f_code) !! b = Some s → stmt_step (Goto b) rf σ [] (to_rtstmt rf s) σ [] | ReturnS rf σ hs v: - free_blocks σ.(st_heap) rf.(rf_locs) hs → (* Deallocate the stack. *) + free_blocks σ.(st_heap) StackAlloc rf.(rf_locs) hs → (* Deallocate the stack. *) stmt_step (Return (Val v)) rf σ [] (Val v) {| st_fntbl := σ.(st_fntbl); st_heap := hs |} [] | FreeS ly v l s rf σ hs' : val_to_loc v = Some l → has_layout_loc l ly → - free_block σ.(st_heap) l ly hs' → + free_block σ.(st_heap) HeapAlloc l ly hs' → stmt_step (Free ly (Val v) s) rf σ [] (to_rtstmt rf s) {| st_fntbl := σ.(st_fntbl); st_heap := hs' |} [] | SkipSS rf σ s : stmt_step (SkipS s) rf σ [] (to_rtstmt rf s) σ [] diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v index 80ad9eb3..d816e90e 100644 --- a/theories/lang/lifting.v +++ b/theories/lang/lifting.v @@ -786,7 +786,7 @@ Qed. Lemma wp_alloc E Φ (l : loc) ly (v : val) : has_layout_val v ly → - ▷ (∀ l, l ↦ v -∗ freeable l (length v) -∗ ⌜l `has_layout_loc` ly⌝ -∗ Φ (val_of_loc l)) -∗ + ▷ (∀ l, l ↦ v -∗ freeable l (length v) HeapAlloc -∗ ⌜l `has_layout_loc` ly⌝ -∗ Φ (val_of_loc l)) -∗ WP (Alloc ly (Val v)) @ E {{ Φ }}. Proof. iIntros (Hly) "Hwp". @@ -929,7 +929,7 @@ Qed. Lemma wps_free Q Ψ s l ly : l ↦|ly| -∗ - freeable l (ly.(ly_size)) -∗ + freeable l (ly.(ly_size)) HeapAlloc -∗ ▷ WPs s {{ Q, Ψ }} -∗ WPs (Free ly (val_of_loc l) s) {{ Q, Ψ }}. Proof. @@ -943,7 +943,7 @@ Proof. match goal with | H : val_to_loc _ = Some ?l |- _ => apply val_of_to_loc in H; injection H; intros <-; intros end. - rewrite (free_block_inj σ.(st_heap) l ly hs' σ'); [ | done..]. + rewrite (free_block_inj σ.(st_heap) l ly HeapAlloc hs' σ'); [ | done..]. iFrame. by iApply "HWP". Qed. diff --git a/theories/typing/adequacy.v b/theories/typing/adequacy.v index 0b8d670f..54fb1002 100644 --- a/theories/typing/adequacy.v +++ b/theories/typing/adequacy.v @@ -10,7 +10,7 @@ Set Default Proof Using "Type". Class typePreG Σ := PreTypeG { type_invG :> invGpreS Σ; type_heap_heap_inG :> inG Σ (authR heapUR); - type_heap_alloc_range_map_inG :> ghost_mapG Σ alloc_id (Z * nat); + type_heap_alloc_range_map_inG :> ghost_mapG Σ alloc_id (Z * nat * alloc_kind); type_heap_alloc_alive_map_inG :> ghost_mapG Σ alloc_id bool; type_heap_fntbl_inG :> ghost_mapG Σ addr function; }. @@ -18,7 +18,7 @@ Class typePreG Σ := PreTypeG { Definition typeΣ : gFunctors := #[invΣ; GFunctor (constRF (authR heapUR)); - ghost_mapΣ alloc_id (Z * nat); + ghost_mapΣ alloc_id (Z * nat * alloc_kind); ghost_mapΣ alloc_id bool; ghost_mapΣ addr function]. Instance subG_typePreG {Σ} : subG typeΣ Σ → typePreG Σ. @@ -38,7 +38,7 @@ Definition main_type `{!typeG Σ} (P : iProp Σ) := (** * The main adequacy lemma *) Lemma refinedc_adequacy Σ `{!typePreG Σ} (thread_mains : list loc) (fns : gmap addr function) (gls : list loc) (gvs : list val.val) n t2 σ2 κs hs σ: - alloc_new_blocks initial_heap_state gls gvs hs → + alloc_new_blocks initial_heap_state StackAlloc gls gvs hs → σ = {| st_heap := hs; st_fntbl := fns; |} → (∀ {HtypeG : typeG Σ}, ∃ gl gt, let Hglobals : globalG Σ := {| global_locs := gl; global_initialized_types := gt; |} in @@ -53,7 +53,7 @@ Proof. iMod (own_alloc (● h ⋅ ◯ h)) as (γh) "[Hh _]" => //. { apply auth_both_valid_discrete. split => //. } iMod (ghost_map_alloc fns) as (γf) "[Hf Hfm]". - iMod (ghost_map_alloc_empty (V:=(Z * nat))) as (γr) "Hr". + iMod (ghost_map_alloc_empty (V:=(Z * nat * alloc_kind))) as (γr) "Hr". iMod (ghost_map_alloc_empty (V:=bool)) as (γs) "Hs". set (HheapG := HeapG _ _ γh _ γr _ γs _ γf). set (HrefinedCG := RefinedCG _ _ HheapG). diff --git a/tutorial/adequacy/adequacy.v b/tutorial/adequacy/adequacy.v index 403eb7c6..1afe2511 100644 --- a/tutorial/adequacy/adequacy.v +++ b/tutorial/adequacy/adequacy.v @@ -85,7 +85,7 @@ Section adequate. loc_allocator_state `has_layout_loc` struct_alloc_state → loc_initialized `has_layout_loc` struct_latch → (* TODO: Should we try to show that this assumption is provable? *) - alloc_new_blocks initial_heap_state initial_heap_locs initial_heap_values hs → + alloc_new_blocks initial_heap_state StackAlloc initial_heap_locs initial_heap_values hs → σ = {| st_heap := hs; st_fntbl := fn_lists_to_fns function_addrs functions; |} → NoDup function_addrs → nsteps (Λ := c_lang) n (initial_prog <$> [(fn_loc addr_main); (fn_loc addr_main2)], σ) κs (t2, σ2) → -- GitLab From e465823879c4e1fa585e83e74fdf1a66e33aa995 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Lennard=20G=C3=A4her?= Date: Wed, 6 Oct 2021 10:10:41 +0200 Subject: [PATCH 3/3] incorporate suggestions --- theories/lang/ghost_state.v | 106 +++++++++++++++++------------------ theories/lang/heap.v | 3 +- theories/typing/adequacy.v | 6 +- tutorial/adequacy/adequacy.v | 2 +- 4 files changed, 59 insertions(+), 58 deletions(-) diff --git a/theories/lang/ghost_state.v b/theories/lang/ghost_state.v index b62ffe2c..bf092de6 100644 --- a/theories/lang/ghost_state.v +++ b/theories/lang/ghost_state.v @@ -22,8 +22,8 @@ Definition heapUR : ucmra := Class heapG Σ := HeapG { heap_heap_inG :> inG Σ (authR heapUR); heap_heap_name : gname; - heap_alloc_range_map_inG :> ghost_mapG Σ alloc_id (Z * nat * alloc_kind); - heap_alloc_range_map_name : gname; + heap_alloc_meta_map_inG :> ghost_mapG Σ alloc_id (Z * nat * alloc_kind); + heap_alloc_meta_map_name : gname; heap_alloc_alive_map_inG :> ghost_mapG Σ alloc_id bool; heap_alloc_alive_map_name : gname; heap_fntbl_inG :> ghost_mapG Σ addr function; @@ -39,11 +39,11 @@ Definition to_heap_cellR (hc : heap_cell) : heap_cellR := Definition to_heapUR : heap → heapUR := fmap to_heap_cellR. -Definition to_alloc_rangeR (al : allocation) : (Z * nat * alloc_kind) := +Definition to_alloc_metaR (al : allocation) : (Z * nat * alloc_kind) := (al.(al_start), al.(al_len), al.(al_kind)). -Definition to_alloc_range_map : allocs → gmap alloc_id (Z * nat * alloc_kind) := - fmap to_alloc_rangeR. +Definition to_alloc_meta_map : allocs → gmap alloc_id (Z * nat * alloc_kind) := + fmap to_alloc_metaR. Definition to_alloc_alive_map : allocs → gmap alloc_id bool := fmap al_alive. @@ -53,20 +53,20 @@ Section definitions. (** * Allocation stuff. *) - (** [alloc_range id al] persistently records the information that allocation + (** [alloc_meta id al] persistently records the information that allocation with identifier [id] has a range corresponding to that of [a]. *) - Definition alloc_range_def (id : alloc_id) (al : allocation) : iProp Σ := - id ↪[ heap_alloc_range_map_name ]□ to_alloc_rangeR al. - Definition alloc_range_aux : seal (@alloc_range_def). by eexists. Qed. - Definition alloc_range := unseal alloc_range_aux. - Definition alloc_range_eq : @alloc_range = @alloc_range_def := - seal_eq alloc_range_aux. + Definition alloc_meta_def (id : alloc_id) (al : allocation) : iProp Σ := + id ↪[ heap_alloc_meta_map_name ]□ to_alloc_metaR al. + Definition alloc_meta_aux : seal (@alloc_meta_def). by eexists. Qed. + Definition alloc_meta := unseal alloc_meta_aux. + Definition alloc_meta_eq : @alloc_meta = @alloc_meta_def := + seal_eq alloc_meta_aux. - Global Instance allocs_range_pers id al : Persistent (alloc_range id al). - Proof. rewrite alloc_range_eq. by apply _. Qed. + Global Instance allocs_range_pers id al : Persistent (alloc_meta id al). + Proof. rewrite alloc_meta_eq. by apply _. Qed. - Global Instance allocs_range_tl id al : Timeless (alloc_range id al). - Proof. rewrite alloc_range_eq. by apply _. Qed. + Global Instance allocs_range_tl id al : Timeless (alloc_meta id al). + Proof. rewrite alloc_meta_eq. by apply _. Qed. (** [loc_in_bounds l n] persistently records the information that location [l] and any of its positive offset up to [n] (included) are in range of the @@ -75,7 +75,7 @@ Section definitions. Definition loc_in_bounds_def (l : loc) (n : nat) : iProp Σ := ∃ (id : alloc_id) (al : allocation), ⌜l.1 = ProvAlloc (Some id)⌝ ∗ ⌜al.(al_start) ≤ l.2⌝ ∗ ⌜l.2 + n ≤ al_end al⌝ ∗ - ⌜allocation_in_range al⌝ ∗ alloc_range id al. + ⌜allocation_in_range al⌝ ∗ alloc_meta id al. 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 := @@ -157,7 +157,7 @@ Section definitions. (** * Freeable *) Definition freeable_def (l : loc) (n : nat) (k : alloc_kind) : iProp Σ := - ∃ id, ⌜l.1 = ProvAlloc (Some id)⌝ ∗ alloc_range id {| al_start := l.2; al_len := n; al_alive := true; al_kind := k |} ∗ + ∃ id, ⌜l.1 = ProvAlloc (Some id)⌝ ∗ alloc_meta id {| al_start := l.2; al_len := n; al_alive := true; al_kind := k |} ∗ alloc_alive id (DfracOwn 1) true. Definition freeable_aux : seal (@freeable_def). by eexists. Qed. Definition freeable := unseal freeable_aux. @@ -169,8 +169,8 @@ Section definitions. Definition heap_ctx (h : heap) : iProp Σ := own heap_heap_name (● to_heapUR h). - Definition alloc_range_ctx (ub : allocs) : iProp Σ := - ghost_map_auth heap_alloc_range_map_name 1 (to_alloc_range_map ub). + Definition alloc_meta_ctx (ub : allocs) : iProp Σ := + ghost_map_auth heap_alloc_meta_map_name 1 (to_alloc_meta_map ub). Definition alloc_alive_ctx (ub : allocs) : iProp Σ := ghost_map_auth heap_alloc_alive_map_name 1 (to_alloc_alive_map ub). @@ -181,7 +181,7 @@ Section definitions. Definition heap_state_ctx (st : heap_state) : iProp Σ := ⌜heap_state_invariant st⌝ ∗ heap_ctx st.(hs_heap) ∗ - alloc_range_ctx st.(hs_allocs) ∗ + alloc_meta_ctx st.(hs_allocs) ∗ alloc_alive_ctx st.(hs_allocs). Definition state_ctx (σ:state) : iProp Σ := @@ -241,70 +241,70 @@ Section fntbl. Qed. End fntbl. -Section alloc_range. +Section alloc_meta. Context `{!heapG Σ}. Implicit Types am : allocs. - Lemma alloc_range_mono id a1 a2 : + Lemma alloc_meta_mono id a1 a2 : alloc_same_range a1 a2 → a1.(al_kind) = a2.(al_kind) → - alloc_range id a1 -∗ alloc_range id a2. - Proof. destruct a1 as [????], a2 as [????] => -[/= <- <-] <-. by rewrite alloc_range_eq. Qed. + alloc_meta id a1 -∗ alloc_meta id a2. + Proof. destruct a1 as [????], a2 as [????] => -[/= <- <-] <-. by rewrite alloc_meta_eq. Qed. - Lemma alloc_range_agree id a1 a2 : - alloc_range id a1 -∗ alloc_range id a2 -∗ ⌜alloc_same_range a1 a2⌝. + Lemma alloc_meta_agree id a1 a2 : + alloc_meta id a1 -∗ alloc_meta id a2 -∗ ⌜alloc_same_range a1 a2⌝. Proof. - destruct a1 as [????], a2 as [????]. rewrite alloc_range_eq /alloc_same_range. + destruct a1 as [????], a2 as [????]. rewrite alloc_meta_eq /alloc_same_range. iIntros "H1 H2". by iDestruct (ghost_map_elem_agree with "H1 H2") as %[=->->]. Qed. - Lemma alloc_range_alloc am id al : + Lemma alloc_meta_alloc am id al : am !! id = None → - alloc_range_ctx am ==∗ - alloc_range_ctx (<[id := al]> am) ∗ alloc_range id al. + alloc_meta_ctx am ==∗ + alloc_meta_ctx (<[id := al]> am) ∗ alloc_meta id al. Proof. - move => Hid. rewrite alloc_range_eq. iIntros "Hctx". + move => Hid. rewrite alloc_meta_eq. iIntros "Hctx". iMod (ghost_map_insert_persist with "Hctx") as "[? $]". { by rewrite lookup_fmap fmap_None. } by rewrite -fmap_insert. Qed. - Lemma alloc_range_to_loc_in_bounds l id (n : nat) al: + Lemma alloc_meta_to_loc_in_bounds l id (n : nat) al: l.1 = ProvAlloc (Some id) → al.(al_start) ≤ l.2 ∧ l.2 + n ≤ al_end al → allocation_in_range al → - alloc_range id al -∗ loc_in_bounds l n. + alloc_meta id al -∗ loc_in_bounds l n. Proof. iIntros (?[??]?) "Hr". rewrite loc_in_bounds_eq. iExists id, al. by iFrame "Hr". Qed. - Lemma alloc_range_lookup am id al : - alloc_range_ctx am -∗ - alloc_range id al -∗ + Lemma alloc_meta_lookup am id al : + alloc_meta_ctx am -∗ + alloc_meta id al -∗ ⌜∃ al', am !! id = Some al' ∧ alloc_same_range al al' ∧ al.(al_kind) = al'.(al_kind)⌝. Proof. - rewrite alloc_range_eq. iIntros "Htbl Hf". + rewrite alloc_meta_eq. iIntros "Htbl Hf". iDestruct (ghost_map_lookup with "Htbl Hf") as %Hlookup. iPureIntro. move: Hlookup. rewrite lookup_fmap fmap_Some => -[[????][?[???]]]. by eexists _. Qed. - Lemma alloc_range_ctx_same_range am id al1 al2 : + Lemma alloc_meta_ctx_same_range am id al1 al2 : am !! id = Some al1 → alloc_same_range al1 al2 → al1.(al_kind) = al2.(al_kind) → - alloc_range_ctx am = alloc_range_ctx (<[id := al2]> am). + alloc_meta_ctx am = alloc_meta_ctx (<[id := al2]> am). Proof. move => Hid [Heq1 Heq2] Heq3. - rewrite /alloc_range_ctx /to_alloc_range_map fmap_insert insert_id; first done. + rewrite /alloc_meta_ctx /to_alloc_meta_map fmap_insert insert_id; first done. rewrite lookup_fmap Hid /=. destruct al1, al2; naive_solver. Qed. - Lemma alloc_range_ctx_killed am id al : + Lemma alloc_meta_ctx_killed am id al : am !! id = Some al → - alloc_range_ctx am = alloc_range_ctx (<[id := killed al]> am). - Proof. move => ?. by apply: alloc_range_ctx_same_range. Qed. -End alloc_range. + alloc_meta_ctx am = alloc_meta_ctx (<[id := killed al]> am). + Proof. move => ?. by apply: alloc_meta_ctx_same_range. Qed. +End alloc_meta. Section alloc_alive. Context `{!heapG Σ}. @@ -351,7 +351,7 @@ Section loc_in_bounds. iDestruct "H2" as (?? Hl2 ? Hend ?) "#H2". move: Hl1 Hl2 => /= Hl1 Hl2. iExists id, al. destruct l. unfold al_end in *. simpl in *. simplify_eq. - iDestruct (alloc_range_agree with "H2 H1") as %[? <-]. + iDestruct (alloc_meta_agree with "H2 H1") as %[? <-]. iFrame "H1". iPureIntro. rewrite /shift_loc /= in Hend. naive_solver lia. - iIntros "H". iDestruct "H" as (id al ????) "#H". iSplit; iExists id, al; iFrame "H"; iPureIntro; split_and! => //=; lia. @@ -389,7 +389,7 @@ Section loc_in_bounds. Proof. rewrite loc_in_bounds_eq. iIntros "Hb ((?&?&Hctx&?)&?)". iDestruct "Hb" as (id al ????) "Hb". - iDestruct (alloc_range_lookup with "Hctx Hb") as %[al' [?[[??]?]]]. + iDestruct (alloc_meta_lookup with "Hctx Hb") as %[al' [?[[??]?]]]. iExists id, al'. iPureIntro. unfold allocation_in_range, al_end in *. naive_solver lia. Qed. @@ -561,7 +561,7 @@ Section heap. al.(al_start) = l.2 → al.(al_len) = length v → allocation_in_range al → - alloc_range id al -∗ + alloc_meta id al -∗ alloc_alive id (DfracOwn 1) true -∗ heap_ctx h ==∗ heap_ctx (heap_alloc l.2 v id h) ∗ @@ -574,7 +574,7 @@ Section heap. rewrite heap_mapsto_mbyte_eq /heap_mapsto_mbyte_def. iSplitR "Hal"; last first; last iSplit. - rewrite freeable_eq. iExists id. iFrame. iSplit => //. - by iApply (alloc_range_mono with "Hr"). + by iApply (alloc_meta_mono with "Hr"). - rewrite loc_in_bounds_eq. iExists id, al. iFrame "Hr". rewrite /al_end. iPureIntro. naive_solver lia. - iApply (big_sepL_impl with "Hl"). @@ -851,9 +851,9 @@ Section alloc_new_blocks. Proof. move => []; clear. move => σ l aid kind v alloc Haid ???; subst alloc. iIntros "Hctx". iDestruct "Hctx" as (Hinv) "(Hhctx&Hrctx&Hsctx)". - iMod (alloc_range_alloc with "Hrctx") as "[$ #Hb]" => //. + iMod (alloc_meta_alloc with "Hrctx") as "[$ #Hb]" => //. iMod (alloc_alive_alloc with "Hsctx") as "[$ Hs]" => //. - iDestruct (alloc_range_to_loc_in_bounds l aid (length v) with "[Hb]") + iDestruct (alloc_meta_to_loc_in_bounds l aid (length v) with "[Hb]") as "#Hinb" => //; [done|..]. iMod (heap_alloc with "Hb Hs Hhctx") as "[Hhctx [Hv Hal]]" => //. iModIntro. iFrame. iPureIntro. by eapply alloc_new_block_invariant. @@ -884,12 +884,12 @@ Section free_blocks. rewrite freeable_eq. iDestruct "Hfree" as (aid Haid) "[#Hrange Hkill]". iDestruct "Hl" as (v Hv ?) "Hl". iDestruct (alloc_alive_lookup with "Hsctx Hkill") as %[[????k] [??]]. - iDestruct (alloc_range_lookup with "Hrctx Hrange") as %[al'' [?[[??]?]]]. simplify_eq/=. + iDestruct (alloc_meta_lookup with "Hrctx Hrange") as %[al'' [?[[??]?]]]. simplify_eq/=. iDestruct (heap_mapsto_lookup_1 (λ st : lock_state, st = RSt 0) with "Hhctx Hl") as %? => //. iExists _. iSplitR. { iPureIntro. by econstructor. } iMod (heap_free_free with "Hhctx Hl") as "Hhctx". rewrite Hv. iFrame => /=. iMod (alloc_alive_kill _ _ ({| al_start := l.2; al_len := ly_size ly; al_alive := true; al_kind := k |}) with "Hsctx Hkill") as "[$ Hd]". - erewrite alloc_range_ctx_same_range; [iFrame |done..]. + erewrite alloc_meta_ctx_same_range; [iFrame |done..]. iPureIntro. eapply free_block_invariant => //. by eapply FreeBlock. Qed. diff --git a/theories/lang/heap.v b/theories/lang/heap.v index 3411ac50..274a26d5 100644 --- a/theories/lang/heap.v +++ b/theories/lang/heap.v @@ -188,7 +188,8 @@ Qed. (** An allocation can either be a stack allocation or a heap allocation. *) Inductive alloc_kind : Set := | HeapAlloc - | StackAlloc. + | StackAlloc + | GlobalAlloc. Record allocation := Allocation { diff --git a/theories/typing/adequacy.v b/theories/typing/adequacy.v index 54fb1002..eb010ef0 100644 --- a/theories/typing/adequacy.v +++ b/theories/typing/adequacy.v @@ -10,7 +10,7 @@ Set Default Proof Using "Type". Class typePreG Σ := PreTypeG { type_invG :> invGpreS Σ; type_heap_heap_inG :> inG Σ (authR heapUR); - type_heap_alloc_range_map_inG :> ghost_mapG Σ alloc_id (Z * nat * alloc_kind); + type_heap_alloc_meta_map_inG :> ghost_mapG Σ alloc_id (Z * nat * alloc_kind); type_heap_alloc_alive_map_inG :> ghost_mapG Σ alloc_id bool; type_heap_fntbl_inG :> ghost_mapG Σ addr function; }. @@ -38,7 +38,7 @@ Definition main_type `{!typeG Σ} (P : iProp Σ) := (** * The main adequacy lemma *) Lemma refinedc_adequacy Σ `{!typePreG Σ} (thread_mains : list loc) (fns : gmap addr function) (gls : list loc) (gvs : list val.val) n t2 σ2 κs hs σ: - alloc_new_blocks initial_heap_state StackAlloc gls gvs hs → + alloc_new_blocks initial_heap_state GlobalAlloc gls gvs hs → σ = {| st_heap := hs; st_fntbl := fns; |} → (∀ {HtypeG : typeG Σ}, ∃ gl gt, let Hglobals : globalG Σ := {| global_locs := gl; global_initialized_types := gt; |} in @@ -62,7 +62,7 @@ Proof. set (Hglobals := {| global_locs := gl; global_initialized_types := gt; |}). move => Hwp. iMod (heap_alloc_new_blocks_upd with "[Hh Hr Hs]") as "[Hctx Hmt]" => //. { - rewrite /heap_state_ctx /alloc_range_ctx /to_alloc_range_map /alloc_alive_ctx /to_alloc_alive_map !fmap_empty. + rewrite /heap_state_ctx /alloc_meta_ctx /to_alloc_meta_map /alloc_alive_ctx /to_alloc_alive_map !fmap_empty. by iFrame. } rewrite big_sepL2_sep. iDestruct "Hmt" as "[Hmt Hfree]". diff --git a/tutorial/adequacy/adequacy.v b/tutorial/adequacy/adequacy.v index 1afe2511..28b747d9 100644 --- a/tutorial/adequacy/adequacy.v +++ b/tutorial/adequacy/adequacy.v @@ -85,7 +85,7 @@ Section adequate. loc_allocator_state `has_layout_loc` struct_alloc_state → loc_initialized `has_layout_loc` struct_latch → (* TODO: Should we try to show that this assumption is provable? *) - alloc_new_blocks initial_heap_state StackAlloc initial_heap_locs initial_heap_values hs → + alloc_new_blocks initial_heap_state GlobalAlloc initial_heap_locs initial_heap_values hs → σ = {| st_heap := hs; st_fntbl := fn_lists_to_fns function_addrs functions; |} → NoDup function_addrs → nsteps (Λ := c_lang) n (initial_prog <$> [(fn_loc addr_main); (fn_loc addr_main2)], σ) κs (t2, σ2) → -- GitLab