diff --git a/theories/c_translation/monad.v b/theories/c_translation/monad.v index ce87b410a1607d62f42bf20e452b1a20c442ac75..b9049199a1d391d9cbb5c817867a08a60843d826 100644 --- a/theories/c_translation/monad.v +++ b/theories/c_translation/monad.v @@ -63,7 +63,7 @@ Section a_wp. Definition env_inv (env : val) : iProp Σ := (∃ (X : gset val) (σ : gmap cloc (lvl * val)), - ⌜ ∀ v, v ∈ X → ∃ cl, cloc_of_val v = Some cl ∧ cl ∈ locked_locs σ ⌝ ∧ + ⌜ ∀ v, v ∈ X → ∃ cl, cloc_of_val (SOMEV v) = Some cl ∧ cl ∈ locked_locs σ ⌝ ∧ is_mset env X ∗ full_locking_heap σ)%I. diff --git a/theories/c_translation/translation.v b/theories/c_translation/translation.v index 02a6c6a4ef3f6b08888b08610ee5e53432826215..61902389dc7d60d42ed7bf1e9c68bc5e40726eaf 100644 --- a/theories/c_translation/translation.v +++ b/theories/c_translation/translation.v @@ -11,7 +11,7 @@ Definition a_alloc : val := λ: "x1" "x2", "vv" ←ᶜ "x1" |||ᶜ "x2" ;;ᶜ let: "n" := Fst "vv" in let: "v" := Snd "vv" in - a_atomic_env (λ: <>, (ref (SOME (lreplicate "n" "v")), #0)). + a_atomic_env (λ: <>, SOME (ref (SOME (lreplicate "n" "v")), #0)). Notation "'allocᶜ' ( e1 , e2 )" := (a_alloc e1%E e2%E) (at level 80) : expr_scope. Definition a_free_check : val := @@ -29,32 +29,40 @@ Definition a_free_check : val := Definition a_free : val := λ: "x", "v" ←ᶜ "x";;ᶜ a_atomic_env (λ: "env", - let: "l" := Fst "v" in - let: "i" := Snd "v" in - match: !"l" with - NONE => assert: #false (* double free *) - | SOME "ll" => - (* We need to make sure `i = 0` and that all `0 ... length of block` are - unlocked. TODO: this means we need to change the spec of `alloc` back so - that we can actually establish we initially have the pointer to the first - element of the array. *) - assert: ("i" = #0);; - let: "n" := llength "ll" in - a_free_check "env" "ll" #0 "n";; - "l" <- NONE + match: "v" with + NONE => assert: #false (* null pointer *) + | SOME "li" => + let: "l" := Fst "li" in + let: "i" := Snd "li" in + match: !"l" with + NONE => assert: #false (* location already freed, double free *) + | SOME "ll" => + (* We need to make sure `i = 0` and that all `0 ... length of block` are + unlocked. TODO: this means we need to change the spec of `alloc` back so + that we can actually establish we initially have the pointer to the first + element of the array. *) + assert: ("i" = #0);; + let: "n" := llength "ll" in + a_free_check "env" "ll" #0 "n";; + "l" <- NONE + end end ). Definition a_store : val := λ: "x1" "x2", "vv" ←ᶜ "x1" |||ᶜ "x2" ;;ᶜ a_atomic_env (λ: "env", - let: "l" := Fst (Fst "vv") in - let: "i" := Snd (Fst "vv") in - let: "v" := Snd "vv" in - mset_add ("l", "i") "env" ;; - match: !"l" with - NONE => assert: #false (* store after free *) - | SOME "ll" => "l" <- SOME (linsert "i" "v" "ll") ;; "v" + match: Fst "vv" with + NONE => assert: #false (* null pointer *) + | SOME "li" => + let: "l" := Fst "li" in + let: "i" := Snd "li" in + let: "v" := Snd "vv" in + mset_add ("l", "i") "env" ;; + match: !"l" with + NONE => assert: #false (* store after free *) + | SOME "ll" => "l" <- SOME (linsert "i" "v" "ll") ;; "v" + end end ). Notation "e1 =ᶜ e2" := (a_store e1%E e2%E) (at level 80) : expr_scope. @@ -62,12 +70,16 @@ Notation "e1 =ᶜ e2" := (a_store e1%E e2%E) (at level 80) : expr_scope. Definition a_load : val := λ: "x", "v" ←ᶜ "x";;ᶜ a_atomic_env (λ: "env", - let: "l" := Fst "v" in - let: "i" := Snd "v" in - assert: (mset_member ("l", "i") "env" = #false);; - match: !"l" with - NONE => assert: #false (* load after free *) - | SOME "ll" => llookup "i" "ll" + match: "v" with + NONE => assert: #false (* null pointer *) + | SOME "li" => + let: "l" := Fst "li" in + let: "i" := Snd "li" in + assert: (mset_member ("l", "i") "env" = #false);; + match: !"l" with + NONE => assert: #false (* load after free *) + | SOME "ll" => llookup "i" "ll" + end end ). Notation "∗ᶜ e" := @@ -126,16 +138,25 @@ Inductive cbin_op := Definition a_ptr_plus : val := λ: "x" "y", (* all binds should be non-sequenced *) - "lo" ←ᶜ ("x" |||ᶜ "y");;ᶜ - let: "o'" := Snd "lo" + Snd (Fst "lo") in - a_ret (Fst (Fst "lo"), "o'"). + "vv" ←ᶜ ("x" |||ᶜ "y");;ᶜ + match: Fst "vv" with + NONE => assert #false (* null pointer *) + | SOME "li" => a_ret (SOME (Fst "li", Snd "vv" + Snd "li")) + end. Definition a_ptr_lt : val := λ: "x" "y", (* all binds should be non-sequenced *) "pq" ←ᶜ ("x" |||ᶜ "y");;ᶜ - let: "p" := Fst "pq" in - let: "q" := Snd "pq" in - if: Fst "p" = Fst "q" then a_ret (Snd "p" < Snd "q") else a_ret #false. + match: Fst "pq" with + NONE => assert #false (* null pointer *) + | SOME "p" => + match: Snd "pq" with + NONE => assert #false (* null pointer *) + | SOME "q" => + if: Fst "p" = Fst "q" + then a_ret (Snd "p" < Snd "q") else a_ret #false + end + end. Definition a_bin_op (op : cbin_op) : val := (* all binds should be non-sequenced *) @@ -234,9 +255,8 @@ Section proofs. iIntros (env). iDestruct 1 as (X σ HX) "[Hlocks Hσ]". iIntros "HR". iDestruct (full_locking_heap_unlocked with "Hl Hσ") as %Hw1. iDestruct (mapsto_offset_non_neg with "Hl") as %?. - assert (cloc_to_val cl ∉ X) as HclX. + assert ((#(cloc_loc cl), #(cloc_offset cl))%V ∉ X) as HclX. { intros Hcl. destruct (HX _ Hcl) as (cl'&[=]%cloc_to_of_val&?). naive_solver. } - rewrite cloc_to_val_eq in HclX. iMod (full_locking_heap_store_upd with "Hσ Hl") as (ll vs Hl Hi) "[Hl Hclose]". wp_pures. rewrite cloc_to_val_eq. wp_pures. wp_apply (mset_add_spec with "[$]"); first done. @@ -247,10 +267,8 @@ Section proofs. iApply wp_fupd. wp_store. iMod ("Hclose" $! _ LLvl with "[//] Hl") as "[Hσ Hl]". iIntros "!> !> {$HR}". iSplitL "Hlocks Hσ"; last by iApply "HΦ". - iExists ({[cloc_to_val cl]} ∪ X), _. iFrame "Hσ". rewrite locked_locs_lock. - iSplit; last by rewrite cloc_to_val_eq. iPureIntro. - intros v [->%elem_of_singleton|?]%elem_of_union; last set_solver. - eexists. split; [apply (cloc_of_to_val cl)|set_solver]. + iExists ({[(#(cloc_loc cl), #(cloc_offset cl))%V]} ∪ X), _. + iFrame "Hσ Hlocks". iPureIntro. rewrite locked_locs_lock. set_solver. Qed. Lemma a_load_spec_exists_frac R Φ e : @@ -266,9 +284,8 @@ Section proofs. iApply awp_atomic_env. iIntros (env) "Henv HR". iDestruct "Henv" as (X σ HX) "[Hlocks Hσ]". iDestruct (full_locking_heap_unlocked with "Hl Hσ") as %Hv. - assert (cloc_to_val cl ∉ X) as HclX. + assert ((#(cloc_loc cl), #(cloc_offset cl))%V ∉ X) as HclX. { intros Hcl. destruct (HX _ Hcl) as (?&[=]%cloc_to_of_val&?); naive_solver. } - rewrite cloc_to_val_eq in HclX. iMod (full_locking_heap_load_upd with "Hσ Hl") as (ll vs Hl Hi) "[Hl Hclose]". wp_pures. rewrite cloc_to_val_eq. wp_pures. wp_apply wp_assert. wp_apply (mset_member_spec with "Hlocks"); iIntros "Hlocks /=". diff --git a/theories/lib/locking_heap.v b/theories/lib/locking_heap.v index ddc8b570dc88fc21e36b4dba3ab984a496e7b6b6..c7d91c02a56e7c66e21d7c53851df7a0b9df7830 100644 --- a/theories/lib/locking_heap.v +++ b/theories/lib/locking_heap.v @@ -117,10 +117,10 @@ Section definitions. CLoc (cloc_loc cl) (i + cloc_offset cl). Definition cloc_to_val (cl : cloc) : val := - locked (#(cloc_loc cl), #(cloc_offset cl))%V. + locked (SOMEV (#(cloc_loc cl), #(cloc_offset cl)))%V. Definition cloc_of_val (v : val) : option cloc := match v return option cloc with - | (LitV (LitLoc l), LitV (LitInt i))%V => Some (CLoc l i) + | SOMEV (LitV (LitLoc l), LitV (LitInt i))%V => Some (CLoc l i) | _ => None end. @@ -242,7 +242,7 @@ Section properties. Lemma cloc_plus_plus cl i j : cloc_plus (cloc_plus cl i) j = cloc_plus cl (i + j). Proof. by rewrite /cloc_plus /= Z.add_assoc (Z.add_comm i j). Qed. - Lemma cloc_to_val_eq : cloc_to_val = λ cl, (#(cloc_loc cl), #(cloc_offset cl))%V. + Lemma cloc_to_val_eq : cloc_to_val = λ cl, SOMEV (#(cloc_loc cl), #(cloc_offset cl))%V. Proof. rewrite /cloc_to_val. by unlock. Qed. Lemma cloc_of_to_val cl : cloc_of_val (cloc_to_val cl) = Some cl. Proof. destruct cl. by rewrite cloc_to_val_eq. Qed.