Commit 6f90c357 by Dan Frumin

### update the store_strong example

parent 042974cc
 ... @@ -3,8 +3,41 @@ From iris_c.vcgen Require Import proofmode. ... @@ -3,8 +3,41 @@ From iris_c.vcgen Require Import proofmode. From iris_c.lib Require Import mset list. From iris_c.lib Require Import mset list. From iris.algebra Require Import frac_auth csum excl agree. From iris.algebra Require Import frac_auth csum excl agree. (** This example is meant to demonstrate the usage of atomic rules for the primitive operations, as well as for function calls. In this file we verify the following program: #include #include int storeme(int * l) { *l = 10; return 10; } int main() { int * l = calloc(sizeof(int), 1); int r = storeme(l) + ( *l = 11 ); printf("*l = %d, r = %d\n", *l, r); return 0; } We prove that the result value r is always 21 and that the value store in l is either 10 or 11. To prove this specification we use an invariant that tracks whether the left/right hand side of the plus operator has been executed. This is achived using the ghost state variables `γl` and `γr`. The invariant guarantees that if `γl ≔ b1 ∗ γr ≔ b2`, then we have four possible situations by case-analysis. match b1, b2 with | false, false => l ↦C #0 | true, false => l ↦C #10 | false, true => l ↦C[LLvl] #11 | true, true => l ↦C #10 ∨ l ↦C[LLvl] #11 end. *) Definition storeme : val := λᶜ "l", Definition storeme : val := λᶜ "l", c_ret "l" =ᶜ ♯ 10 ;ᶜ ♯ 10. c_ret "l" =ᶜ ♯ 10 ;ᶜ ♯ 10. (* want to have a sequence point at the end of the function *) Definition test : val := λᶜ "l", Definition test : val := λᶜ "l", callᶜ (c_ret storeme) (c_ret "l") +ᶜ (c_ret "l" =ᶜ ♯11). callᶜ (c_ret storeme) (c_ret "l") +ᶜ (c_ret "l" =ᶜ ♯11). ... @@ -12,41 +45,7 @@ Definition test : val := λᶜ "l", ... @@ -12,41 +45,7 @@ Definition test : val := λᶜ "l", Section test. Section test. Context `{cmonadG Σ, !inG Σ (authR (optionUR (exclR boolC)))}. Context `{cmonadG Σ, !inG Σ (authR (optionUR (exclR boolC)))}. Lemma cwp_store_hard R Φ Ψ1 Ψ2 e1 e2 : (** Basic specification for `storeme' *) CWP e1 @ R {{ Ψ1 }} -∗ CWP e2 @ R {{ Ψ2 }} -∗ (∀ v1 v2, Ψ1 v1 -∗ Ψ2 v2 -∗ R -∗ ∃ cl w, ⌜ v1 = cloc_to_val cl ⌝ ∧ cl ↦C w ∗ (cl ↦C[LLvl] v2 ={⊤}=∗ R ∗ Φ v2)) -∗ CWP e1 =ᶜ e2 @ R {{ Φ }}. Proof. iIntros "H1 H2 HΦ". cwp_apply (cwp_wp with "H2"); iIntros (v2) "H2". cwp_apply (cwp_wp with "H1"); iIntros (v1) "H1". Transparent c_store. unfold c_store. cwp_lam. cwp_pures. iApply cwp_bind. iApply (cwp_par with "H1 H2"). iIntros "!>" (w1 w2) "H1 H2 !>". cwp_pures. iApply cwp_atomic_env. iIntros (env). iDestruct 1 as (X σ HX) "[Hlocks Hσ]". iIntros "HR". iDestruct ("HΦ" with "H1 H2 HR") as (cl w ->) "[Hl HΦ]". iDestruct (full_locking_heap_unlocked with "Hl Hσ") as %Hw1. iDestruct (mapsto_offset_non_neg with "Hl") as %?. assert ((#(cloc_base cl), #(cloc_offset cl))%V ∉ X) as HclX. { intros Hcl. destruct (HX _ Hcl) as (cl'&[=]%cloc_to_of_val&?). naive_solver. } iMod (full_locking_heap_store_upd with "Hσ Hl") as (k ll vs Hl Hi) "[Hl Hclose]". wp_pures. rewrite cloc_to_val_eq. wp_pures. wp_apply (mset_add_spec with "[\$]"); first done. iIntros "Hlocks /="; wp_pures. wp_load; wp_pures. iEval (rewrite -(Z2Nat.id (cloc_offset cl)) //). wp_apply (linsert_spec with "[//]"); [eauto|]. iIntros (ll' Hl'). iApply wp_fupd. wp_store. iMod ("Hclose" \$! _ LLvl with "[//] Hl") as "[Hσ Hl]". iMod ("HΦ" with "Hl") as "[\$ \$]". iIntros "!> !>". iExists ({[(#(cloc_base cl), #(cloc_offset cl))%V]} ∪ X), _. iFrame "Hσ Hlocks". iPureIntro. rewrite locked_locs_lock. set_solver. Qed. Lemma storeme_spec R cl v Φ : Lemma storeme_spec R cl v Φ : cl ↦C v -∗ (cl ↦C #10 -∗ Φ #10) -∗ cl ↦C v -∗ (cl ↦C #10 -∗ Φ #10) -∗ CWP storeme (cloc_to_val cl) @ R {{ Φ }}. CWP storeme (cloc_to_val cl) @ R {{ Φ }}. ... @@ -54,6 +53,7 @@ Section test. ... @@ -54,6 +53,7 @@ Section test. iIntros "? H". iApply cwp_fun; simpl. vcg; iIntros "? !>". by iApply "H". iIntros "? H". iApply cwp_fun; simpl. vcg; iIntros "? !>". by iApply "H". Qed. Qed. (** Ghost state definitions and lemmas *) Definition gpointsto γ (b : bool) := own γ (◯ (Excl' b)). Definition gpointsto γ (b : bool) := own γ (◯ (Excl' b)). Notation "γ '≔' b" := (gpointsto γ b) (at level 80). Notation "γ '≔' b" := (gpointsto γ b) (at level 80). Definition gauth γ b := own γ (● (Excl' b)). Definition gauth γ b := own γ (● (Excl' b)). ... @@ -80,6 +80,15 @@ Section test. ... @@ -80,6 +80,15 @@ Section test. by iFrame. by iFrame. Qed. Qed. (** The correctness of the test function. *) Definition test_inv cl γl γr : iProp Σ := (∃ b1 b2, gauth γl b1 ∗ gauth γr b2 ∗ match b1, b2 with | false, false => cl ↦C #0 | true, false => cl ↦C #10 | false, true => cl ↦C[LLvl] #11 | _, _ => cl ↦C #10 ∨ cl ↦C[LLvl] #11 end)%I. Lemma test_spec R cl `{inG Σ testR, inG Σ fracR} : Lemma test_spec R cl `{inG Σ testR, inG Σ fracR} : cl ↦C #0%nat -∗ cl ↦C #0%nat -∗ CWP "x" ←ᶜ test (cloc_to_val cl);ᶜ c_ret "x" @ R {{ v, ⌜ v = #21 ⌝ ∧ CWP "x" ←ᶜ test (cloc_to_val cl);ᶜ c_ret "x" @ R {{ v, ⌜ v = #21 ⌝ ∧ ... @@ -88,15 +97,7 @@ Section test. ... @@ -88,15 +97,7 @@ Section test. iIntros "Hl". iApply cwp_seq_bind. iApply cwp_fun. simpl. iIntros "Hl". iApply cwp_seq_bind. iApply cwp_fun. simpl. iMod gnew as (γl) "[H1 lb]". iMod gnew as (γl) "[H1 lb]". iMod gnew as (γr) "[H2 rb]". iMod gnew as (γr) "[H2 rb]". set (test_inv := (∃ b1 b2, gauth γl b1 ∗ gauth γr b2 ∗ iApply (cwp_insert_res _ _ (test_inv cl γl γr) with "[H1 H2 Hl]"). match b1, b2 with | false, false => cl ↦C #0 | true, false => cl ↦C #10 | false, true => cl ↦C[LLvl] #11 | _, _ => cl ↦C #10 ∨ cl ↦C[LLvl] #11 end )%I). iApply (cwp_insert_res _ _ test_inv with "[H1 H2 Hl]"). { iNext. iExists false,false. iFrame. } { iNext. iExists false,false. iFrame. } iApply (cwp_bin_op _ _ (λ v, ⌜v = #10⌝ ∗ γl ≔ true)%I iApply (cwp_bin_op _ _ (λ v, ⌜v = #10⌝ ∗ γl ≔ true)%I (λ v, ⌜v = #11⌝ ∗ γr ≔ true)%I (λ v, ⌜v = #11⌝ ∗ γr ≔ true)%I ... @@ -115,12 +116,13 @@ Section test. ... @@ -115,12 +116,13 @@ Section test. iIntros "Hl". iFrame "R". iIntros "Hl". iFrame "R". iSplitR "lb"; last by (vcg_continue; eauto with iFrame). iSplitR "lb"; last by (vcg_continue; eauto with iFrame). iExists _,_; eauto with iFrame. iExists _,_; eauto with iFrame. - iApply (cwp_store_hard _ _ (λ v, ⌜v = cloc_to_val cl⌝)%I - iApply (cwp_store _ _ (λ v, ⌜v = cloc_to_val cl⌝)%I (λ v, ⌜v = #11⌝)%I). (λ v, ⌜v = #11⌝)%I). 1,2: vcg; eauto. 1,2: vcg; eauto. iIntros (? ? -> ->) "[H R]". unfold test_inv. iIntros (? ? -> ->) "[H R]". unfold test_inv. iDestruct "H" as (b1 b2) "(H1 & H2 & H)". iDestruct "H" as (b1 b2) "(H1 & H2 & H)". iDestruct (gagree with "rb H2") as %<-. iDestruct (gagree with "rb H2") as %<-. iModIntro. destruct b1; iEval (simpl) in "H". destruct b1; iEval (simpl) in "H". + iExists cl, _. iFrame. iSplit; first done. + iExists cl, _. iFrame. iSplit; first done. iIntros "Hl". iIntros "Hl". ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!