Add NULL pointers.

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.
 

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,10 +29,13 @@ 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: "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 (* double free *)
+         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
@@ -43,32 +46,41 @@ Definition a_free : val := λ: "x",
           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
+    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.
 
 Definition a_load : val := λ: "x",
   "v" ←ᶜ "x";;ᶜ
   a_atomic_env (λ: "env",
-    let: "l" := Fst "v" in
-    let: "i" := Snd "v" in
+    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" :=
   (a_load e)%E (at level 9, right associativity) : expr_scope.
@@ -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 /=".

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.