diff --git a/theories/tests/store_strong.v b/theories/tests/store_strong.v index f8d28a87332d1777ed629cc9bec409768c2ae1e3..2141cc9e2ac0c87c4ab37b2323e39761e3fae0c6 100644 --- a/theories/tests/store_strong.v +++ b/theories/tests/store_strong.v @@ -3,8 +3,41 @@ From iris_c.vcgen Require Import proofmode. From iris_c.lib Require Import mset list. 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", - 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", callᶜ (c_ret storeme) (c_ret "l") +ᶜ (c_ret "l" =ᶜ ♯11). @@ -12,41 +45,7 @@ Definition test : val := λᶜ "l", Section test. Context `{cmonadG Σ, !inG Σ (authR (optionUR (exclR boolC)))}. - Lemma cwp_store_hard R Φ Ψ1 Ψ2 e1 e2 : - 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. - + (** Basic specification for `storeme' *) Lemma storeme_spec R cl v Φ : cl ↦C v -∗ (cl ↦C #10 -∗ Φ #10) -∗ CWP storeme (cloc_to_val cl) @ R {{ Φ }}. @@ -54,6 +53,7 @@ Section test. iIntros "? H". iApply cwp_fun; simpl. vcg; iIntros "? !>". by iApply "H". Qed. + (** Ghost state definitions and lemmas *) Definition gpointsto γ (b : bool) := own γ (◯ (Excl' b)). Notation "γ '≔' b" := (gpointsto γ b) (at level 80). Definition gauth γ b := own γ (● (Excl' b)). @@ -80,6 +80,15 @@ Section test. by iFrame. 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} : cl ↦C #0%nat -∗ CWP "x" ←ᶜ test (cloc_to_val cl);ᶜ c_ret "x" @ R {{ v, ⌜ v = #21 ⌝ ∧ @@ -88,15 +97,7 @@ Section test. iIntros "Hl". iApply cwp_seq_bind. iApply cwp_fun. simpl. iMod gnew as (γl) "[H1 lb]". iMod gnew as (γr) "[H2 rb]". - set (test_inv := (∃ 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). - iApply (cwp_insert_res _ _ test_inv with "[H1 H2 Hl]"). + iApply (cwp_insert_res _ _ (test_inv cl γl γr) with "[H1 H2 Hl]"). { iNext. iExists false,false. iFrame. } iApply (cwp_bin_op _ _ (λ v, ⌜v = #10⌝ ∗ γl ≔ true)%I (λ v, ⌜v = #11⌝ ∗ γr ≔ true)%I @@ -115,12 +116,13 @@ Section test. iIntros "Hl". iFrame "R". iSplitR "lb"; last by (vcg_continue; eauto with iFrame). iExists _,_; eauto with iFrame. - - iApply (cwp_store_hard _ _ (λ v, ⌜v = cloc_to_val cl⌝)%I - (λ v, ⌜v = #11⌝)%I). + - iApply (cwp_store _ _ (λ v, ⌜v = cloc_to_val cl⌝)%I + (λ v, ⌜v = #11⌝)%I). 1,2: vcg; eauto. iIntros (? ? -> ->) "[H R]". unfold test_inv. iDestruct "H" as (b1 b2) "(H1 & H2 & H)". iDestruct (gagree with "rb H2") as %<-. + iModIntro. destruct b1; iEval (simpl) in "H". + iExists cl, _. iFrame. iSplit; first done. iIntros "Hl".