Free!

theories/c_translation/translation.v

@@ -16,17 +16,12 @@ Definition a_alloc : val := λ: "x1" "x2",
 Notation "'allocᶜ' ( e1 , e2 )" := (a_alloc e1%E e2%E) (at level 80) : expr_scope.
 
 Definition a_free_check : val :=
-  rec: "go" "env" "l" "i" "n" :=
-  if: "i" < "n" then
-    assert: (mset_member ("l", "i") "env" = #false);;
-    "go" "env" "l" (#1 + "i") "n"
-  else #().
-
-(* DF: following the discussion with Robbert, it seems that we cannot
-   prove this function right now, because our ghost state cannot
-   account that we hold permission for the *whole* array.
-   
-   See the RustBelt paper for the trick to make it work. *)
+  rec: "go" "env" "l" "n" :=
+  if: "n" = #0 then #() else
+  let: "n" := "n" - #1 in
+  assert: (mset_member ("l", "n") "env" = #false);;
+  "go" "env" "l" "n".
+
 Definition a_free : val := λ: "x",
   "v" ←ᶜ "x";;ᶜ
   a_atomic_env (λ: "env",
@@ -38,17 +33,16 @@ Definition a_free : val := λ: "x",
        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. *)
+          (* We need to make sure `i = 0` and that all `0 ... length of block`
+          are unlocked. *)
           assert: ("i" = #0);;
           let: "n" := llength "ll" in
-          a_free_check "env" "ll" #0 "n";;
+          a_free_check "env" "l" "n";;
          "l" <- NONE
        end
     end
   ).
+Notation "'freeᶜ' ( e )" := (a_free e%E) (at level 80) : expr_scope.
 
 Definition a_store : val := λ: "x1" "x2",
   "vv" ←ᶜ "x1" |||ᶜ "x2" ;;ᶜ
@@ -214,7 +208,7 @@ Section proofs.
     AWP e2 @ R {{ Ψ2 }} -∗
     (∀ v1 v2, Ψ1 v1 -∗ Ψ2 v2 -∗ ∃ n : nat,
               ⌜ v1 = #n ⌝ ∧ ⌜ n ≠ 0%nat ⌝ ∧
-              ∀ l, l ↦C∗ replicate n v2 -∗ Φ (cloc_to_val l)) -∗
+              ∀ cl, block_info cl n -∗ cl ↦C∗ replicate n v2 -∗ Φ (cloc_to_val cl)) -∗
     AWP allocᶜ(e1, e2) @ R {{ Φ }}.
   Proof.
     iIntros "H1 H2 HΦ".
@@ -230,13 +224,60 @@ Section proofs.
     iIntros (env). iDestruct 1 as (X σ HX) "[Hlocks Hσ]". iIntros "$". wp_pures.
     wp_apply (lreplicate_spec with "[//]"); iIntros (ll Hll).
     wp_alloc l as "Hl".
-    iMod (full_locking_heap_alloc_upd with "Hσ Hl") as (?) "[Hσ Hl]"; first done.
-    wp_pures. iIntros "!>". rewrite cloc_to_val_eq.
+    iMod (full_locking_heap_alloc_upd with "Hσ Hl")
+      as (?) "(Hσ & Hinfo & Hl)"; first done.
+    { by destruct n. }
+    wp_pures. iIntros "!>". rewrite cloc_to_val_eq replicate_length.
     iSplitL "Hlocks Hσ".
     - iExists X, _. iFrame.
       iIntros "!%". intros w Hw. destruct (HX _ Hw) as (cl&Hcl&Hin).
       exists cl; split; first done. by rewrite locked_locs_alloc_heap.
-    - by iApply ("HΦ" $! (CLoc l 0)).
+    - iApply ("HΦ" $! (CLoc l 0) with "Hinfo Hl").
+  Qed.
+
+  Lemma a_free_spec R Φ e :
+    AWP e @ R {{ v, ∃ cl ws, ⌜ v = cloc_to_val cl ⌝ ∧
+                             block_info cl (length ws) ∗ cl ↦C∗ ws ∗ Φ #() }} -∗
+    AWP freeᶜ(e) @ R {{ Φ }}.
+  Proof.
+    iIntros "H".
+    awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam. awp_pures.
+    iApply awp_bind. iApply (awp_wand with "H"). clear v.
+    iIntros (v). iDestruct 1 as (cl ws ->) "(Hinfo & Hcl & HΦ)". awp_pures.
+    iApply awp_atomic_env. iIntros (env) "Henv HR". wp_pures.
+    rewrite cloc_to_val_eq. wp_pures.
+    iDestruct "Henv" as (X σ HX) "[Hlocks Hσ]".
+    iAssert ⌜ ∀ i : nat, is_Some (ws !! i) → (cl +∗ i) ∉ locked_locs σ⌝%I as %Hlocked.
+    { iIntros (i [w Hi]). rewrite /mapsto_list.
+      iDestruct (big_sepL_lookup with "Hcl") as "H"; first done.
+      by iApply (full_locking_heap_unlocked with "[$]"). }
+    iMod (full_locking_heap_free_upd with "Hσ Hinfo Hcl")
+      as (ll Hoff Hl) "[Hl Hclose]".
+    wp_load. wp_pures. rewrite Hoff.
+    wp_apply wp_assert; wp_pures; iSplit; first done.
+    iNext; wp_pures. wp_apply (llength_spec with "[//]"); iIntros "_"; wp_pures.
+    iAssert (∀ Ψ (n : nat), ⌜ n ≤ length ws ⌝ →
+      (is_mset env X -∗ Ψ #()) -∗ WP a_free_check env #(cloc_base cl) #n {{ Ψ }})%I
+      with "[Hlocks]" as "Hcheck".
+    { iIntros (Ψ n Hn) "HΨ". iInduction n as [|n] "IH" forall (Ψ Hn).
+      { wp_lam; wp_pures. by iApply "HΨ". }
+      wp_lam; wp_pures. wp_apply wp_assert.
+      rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
+      wp_apply (mset_member_spec with "Hlocks"); iIntros "Hlocks"; case_bool_decide.
+      { destruct (HX (#(cloc_base cl), #n)%V) as (cl'&[= <-]&?); first done.
+        destruct (Hlocked n); first by (apply lookup_lt_is_Some_2; lia).
+        destruct cl; simplify_eq/=. by rewrite /cloc_plus /= Z.add_0_r. }
+      wp_op. iSplit; first done. iNext; wp_pures.
+      iApply ("IH" with "[%] Hlocks HΨ"). lia. }
+    wp_apply ("Hcheck" with "[//]"); iIntros "Hlock". wp_pures. wp_store.
+    iIntros "!> {$HΦ $HR}". iExists X, _.
+    iFrame "Hlock". iSplit; last by iApply "Hclose".
+    iPureIntro; intros w Hw. destruct (HX _ Hw) as (cl'&Hcl&Hin).
+    exists cl';  split; first done. apply locked_locs_free_heap; first done.
+    intros (?&?&?). destruct (Hlocked (Z.to_nat (cloc_offset cl'))).
+    { apply lookup_lt_is_Some_2, Nat2Z.inj_lt. rewrite Z2Nat.id; lia. }
+    destruct cl, cl'; simplify_eq/=.
+    by rewrite /cloc_plus /= Z.add_0_r Z2Nat.id; last lia.
   Qed.
 
   Lemma a_store_spec R Φ Ψ1 Ψ2 e1 e2 :

theories/tests/memcpy.v

@@ -15,7 +15,8 @@ Lemma memcpy_spec `{amonadG Σ} lxs lys xs ys n R :
   lxs ↦C∗ xs -∗ lys ↦C∗ ys -∗
   AWP memcpy (cloc_to_val lxs, (cloc_to_val lys, #n))%V @ R {{ _, lxs ↦C∗ ys ∗ lys ↦C∗ ys }}.
 Proof.
-  iIntros (Hlen <-) "Hxs Hys". awp_lam. vcg. iIntros (p _ q _) "Hp Hq".
+  iIntros (Hlen <-) "Hxs Hys". awp_lam. vcg.
+  iIntros (p) "_ _"; iIntros (q) "_ _ Hp Hq".
   iApply (awp_wand _ (λ _, lxs ↦C∗ ys ∗ lys ↦C∗ ys)%I with "[-]");
     [|iIntros (v) "H"; by vcg_continue].
   iInduction xs as [|x xs] "IH" forall (lxs lys ys Hlen);

theories/vcgen/vcgen.v

@@ -99,12 +99,15 @@ Section vcg.
     | Some di =>
        ∀ cl,
          let i := length E in
+         block_info cl (S (Z.to_nat (dint_interp di))) -∗
          (cl +∗ 1) ↦C∗ replicate (Z.to_nat (dint_interp di)) (dval_interp E dv2) -∗
          Φ (E ++ [cl]) (denv_insert i ULvl 1 dv2 m) (dLocV (dLoc (dLocKnown i) (dInt 0 None)))
     | _ =>
        wand_denv_interp E m (∃ n : nat,
          ⌜ dval_interp E dv1 = #n ⌝ ∧ ⌜ n ≠ O ⌝ ∧ ∀ cl,
-         cl ↦C∗ replicate n (dval_interp E dv2) -∗ vcg_wp_continuation E Φ (cloc_to_val cl))
+           block_info cl n -∗
+           cl ↦C∗ replicate n (dval_interp E dv2) -∗
+           vcg_wp_continuation E Φ (cloc_to_val cl))
     end%I.
 
   Definition vcg_wp_load (E : known_locs) (dv : dval) (m : denv)
@@ -562,7 +565,8 @@ Section vcg_spec.
     denv_interp E m -∗
     vcg_wp_alloc E dv1 dv2 m Φ -∗
     ∃ n : nat, ⌜dval_interp E dv1 = #n⌝ ∧ ⌜ n ≠ O%nat ⌝ ∧
-               (∀ cl, cl ↦C∗ replicate n (dval_interp E dv2) -∗
+               (∀ cl, block_info cl n -∗
+                      cl ↦C∗ replicate n (dval_interp E dv2) -∗
                       vcg_wp_continuation E Φ (cloc_to_val cl)).
   Proof.
     iIntros (???) "Hm H". rewrite /vcg_wp_alloc.
@@ -570,7 +574,7 @@ Section vcg_spec.
     { iApply (wand_denv_interp_spec with "H Hm"). }
     iExists (S (Z.to_nat (dint_interp di))); simpl.
     iSplit; first by eauto using succ_nat_of_dval_Some.
-    iSplit; first done. iIntros (cl) "[Hcl Hcls]".
+    iSplit; first done. iIntros (cl) "Hinfo [Hcl Hcls]".
     assert (dloc_var_interp (E ++ [cl]) (length E) = cl) as Hcl.
     { by rewrite /dloc_var_interp (list_lookup_middle _ []). }
     iExists (E ++ [cl]), (dLocV (dLoc (dLocKnown (length E)) (dInt 0 None))),
@@ -580,7 +584,7 @@ Section vcg_spec.
     iSplit; first by eauto using denv_wf_insert_extend.
     iSplit.
     { by rewrite /dloc_wf /= /dloc_var_wf (list_lookup_middle _ []). }
-    iSplitL "Hcl Hm"; last by iApply ("H" with "Hcls").
+    iSplitL "Hcl Hm"; last by iApply ("H" with "Hinfo Hcls").
     iApply denv_insert_interp; eauto using denv_wf_mono, prefix_app_r.
     iSplitL "Hm".
     { iApply (denv_interp_mono with "Hm"); eauto using prefix_app_r. }
@@ -713,9 +717,9 @@ Section vcg_spec.
           eauto using denv_wf_mono, dval_wf_mono.
         { iApply denv_merge_interp; eauto using denv_wf_mono.
           iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. }
-        iExists _; repeat (iSplit; first done). iIntros (cl) "Hcl".
+        iExists _; repeat (iSplit; first done). iIntros (cl) "Hinfo Hcl".
         rewrite (dval_interp_mono E E'); eauto.
-        by iApply vcg_wp_continuation_mono; last by iApply "H".
+        by iApply vcg_wp_continuation_mono; last by iApply ("H" with "Hinfo").
       + iDestruct (vcg_sp_correct with "Hm") as "[Hm' H1]"; eauto.
         iApply (a_alloc_spec with "H1 [H Hm']").
         { iApply ("IH" with "[] [] Hm' H"); eauto. }
@@ -725,8 +729,8 @@ Section vcg_spec.
         { iApply denv_merge_interp; eauto using denv_wf_mono.
           iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. }
         rewrite (dval_interp_mono E E'); eauto.
-        iExists _; repeat (iSplit; first done). iIntros (cl) "Hcl".
-        by iApply vcg_wp_continuation_mono; last by iApply "H".
+        iExists _; repeat (iSplit; first done). iIntros (cl) "Hinfo Hcl".
+        by iApply vcg_wp_continuation_mono; last by iApply ("H" with "Hinfo").
     - (* load *)
       iApply a_load_spec_exists_frac. iApply (awp_wand with "[-]").
       { iApply ("IH" with "[] [] Hm H"); eauto. }