Disallow creation of out of bounds pointers

theories/lang/lang.v

@@ -230,11 +230,12 @@ Inductive eval_bin_op : bin_op → op_type → op_type → state → val → val
     val_to_Z_weak v1 it = Some o →
     val_to_loc v2 = Some l →
     (* TODO: should we have an alignment check here? *)
-    0 ≤ o →
+    heap_state_loc_in_bounds (l offset{ly}ₗ o) 0 σ.(st_heap) →
     eval_bin_op (PtrOffsetOp ly) (IntOp it) PtrOp σ v1 v2 (val_of_loc (l offset{ly}ₗ o))
 | PtrNegOffsetOpIP v1 v2 σ o l ly it:
     val_to_Z_weak v1 it = Some o →
     val_to_loc v2 = Some l →
+    heap_state_loc_in_bounds (l offset{ly}ₗ -o) 0 σ.(st_heap) →
     (* TODO: should we have an alignment check here? *)
     eval_bin_op (PtrNegOffsetOp ly) (IntOp it) PtrOp σ v1 v2 (val_of_loc (l offset{ly}ₗ -o))
 | EqOpPNull v1 v2 σ l v:

theories/lang/lifting.v

@@ -426,13 +426,15 @@ Qed.
 Lemma wp_ptr_offset Φ vl l E it o ly vo:
   val_to_loc vl = Some l →
   val_to_Z_weak vo it = Some o →
-  0 ≤ o →
+  loc_in_bounds (l offset{ly}ₗ o) 0 -∗
   ▷ Φ (val_of_loc (l offset{ly}ₗ o)) -∗
   WP Val vl at_offset{ ly , PtrOp, IntOp it} Val vo @ E {{ Φ }}.
 Proof.
-  iIntros (Hvl Hvo Ho) "HΦ".
+  iIntros (Hvl Hvo) "Hl HΦ".
   iApply wp_binop_det. iSplit; last done.
-  iIntros (σ v) "_ !%". split.
+  iIntros (σ v) "Hσ".
+  iDestruct (loc_in_bounds_to_heap_loc_in_bounds with "Hl Hσ") as %?.
+  iPureIntro. split.
   - inversion 1. by simplify_eq.
   - move => ->. by apply PtrOffsetOpIP.
 Qed.
@@ -440,12 +442,15 @@ Qed.
 Lemma wp_ptr_neg_offset Φ vl l E it o ly vo:
   val_to_loc vl = Some l →
   val_to_Z_weak vo it = Some o →
+  loc_in_bounds (l offset{ly}ₗ -o) 0 -∗
   ▷ Φ (val_of_loc (l offset{ly}ₗ -o)) -∗
   WP Val vl at_neg_offset{ ly , PtrOp, IntOp it} Val vo @ E {{ Φ }}.
 Proof.
-  iIntros (Hvl Hvo) "HΦ".
+  iIntros (Hvl Hvo) "Hl HΦ".
   iApply wp_binop_det. iSplit; last done.
-  iIntros (σ v) "_ !%". split.
+  iIntros (σ v) "Hσ".
+  iDestruct (loc_in_bounds_to_heap_loc_in_bounds with "Hl Hσ") as %?.
+  iPureIntro. split.
   - inversion 1. by simplify_eq.
   - move => ->. by apply PtrNegOffsetOpIP.
 Qed.
@@ -453,24 +458,23 @@ Qed.
 Lemma wp_get_member Φ vl l sl n E:
   val_to_loc vl = Some l →
   is_Some (index_of sl.(sl_members) n) →
+  loc_in_bounds l (ly_size sl) -∗
   ▷ Φ (val_of_loc (l at{sl}ₗ n)) -∗
   WP Val vl at{sl} n @ E {{ Φ }}.
 Proof.
-  iIntros (Hvl [i Hi]) "HΦ".
+  iIntros (Hvl [i Hi]) "#Hl HΦ".
   rewrite /GetMember/GetMemberLoc/offset_of Hi /=.
   have [|v Hv]:= (val_of_Z_is_Some size_t (offset_of_idx sl.(sl_members) i)). {
-    split; first by rewrite /min_int/=; lia.  by apply offset_of_bound.
+    split; first by rewrite /min_int/=; lia. by apply offset_of_bound.
   }
   rewrite Hv /=. move: Hv => /val_to_of_Z Hv.
-  iApply wp_binop_det. iSplit; last done.
-  iIntros (σ v') "_ !%". split.
-  - inversion 1; simplify_eq. rewrite offset_loc_sz1; last done.
-    apply val_to_Z_to_int_repr_Z in Hv. by simplify_eq.
-  - move => ->. rewrite -(offset_loc_sz1 u8) //.
-    apply: PtrOffsetOpIP => //; last lia.
-    by rewrite /val_to_Z_weak /val_to_int_repr Hv.
+  iApply wp_ptr_offset; [done| by apply: val_to_Z_to_int_repr_Z | | ].
+  { have ? := offset_of_idx_le_size sl i.
+    have -> : (ly_size sl = offset_of_idx (sl_members sl) i + (ly_size sl - offset_of_idx (sl_members sl) i))%nat by lia.
+    rewrite -loc_in_bounds_split offset_loc_sz1 //.
+    iDestruct "Hl" as "[_ Hl]". iApply (loc_in_bounds_shorten with "Hl"). lia. }
+  by rewrite offset_loc_sz1.
 Qed.
-
 Lemma wp_get_member_union Φ vl l ul n E:
   val_to_loc vl = Some l →
   Φ (val_of_loc (l at_union{ul}ₗ n)) -∗ WP Val vl at_union{ul} n @ E {{ Φ }}.

theories/lang/notation.v

@@ -290,6 +290,10 @@ Proof.
   naive_solver.
 Qed.
 
+Lemma offset_of_idx_le_size sl i:
+  (offset_of_idx (sl_members sl) i ≤ ly_size sl)%nat.
+Proof. apply: sum_list_with_take. Qed.
+
 Lemma offset_of_bound i sl:
   offset_of_idx sl.(sl_members) i ≤ max_int size_t.
 Proof.

theories/typing/array.v

@@ -222,7 +222,10 @@ Section array.
     iDestruct ("HP" with "Hv") as (Hv) "HP".
     iDestruct "HP" as (? Hlen) "HP".
     have [|ty ?]:= lookup_lt_is_Some_2 tys (Z.to_nat i). lia.
-    iApply wp_ptr_offset => //. by apply val_to_of_loc.
+    iApply wp_ptr_offset => //; [by apply val_to_of_loc | | ].
+    { have -> : length tys = (Z.to_nat i + (length tys - Z.to_nat i))%nat by lia.
+      rewrite Nat.mul_add_distr_l -loc_in_bounds_split Nat2Z.inj_mul Z2Nat.id; [|lia].
+      iDestruct "Hb" as "[_ Hb]". iApply (loc_in_bounds_shorten with "Hb"). nia. }
     iIntros "!#". iExists _. iSplit => //.
     iDestruct (big_sepL_insert_acc with "Hl") as "[Hl Hc]" => //. rewrite Z2Nat.id//.
     iApply ("HP" $! ty with "[//] Hl"). iIntros (l' ty2 β2 typ R) "Hl' Htyp HT".

theories/typing/bytes.v

@@ -152,10 +152,13 @@ Section bytewise.
     move: (Hint) => /val_to_Z_weak_in_range?.
     iDestruct ("HT" with "[//]") as (??) "HT".
     iDestruct (split_bytewise (Z.to_nat n) with "Hp") as "[H1 H2]"; [lia..|].
-    iApply wp_ptr_offset. by apply val_to_of_loc. done. done.
-    iModIntro. rewrite offset_loc_sz1//.
-    iApply ("HΦ" with "[H2]"). 2: iApply ("HT" with "H1 []"). rewrite Z2Nat.id; [|lia]. by iFrame.
-    by iPureIntro.
+    rewrite -!(offset_loc_sz1 u8)// Z2Nat.id; [|lia].
+    iDestruct (loc_in_bounds_in_bounds with "H2") as "#?".
+    iApply wp_ptr_offset; [ by apply val_to_of_loc | done | |].
+    { iApply loc_in_bounds_shorten; [|done]; lia. }
+    iModIntro. iApply ("HΦ" with "[H2]"). 2: iApply ("HT" with "H1 []").
+    - by iFrame.
+    - by iPureIntro.
   Qed.
   Global Instance type_add_bytewise_inst v2 β P ly (p : loc) n it:
     TypedBinOp v2 (v2 ◁ᵥ n @ int it)%I p (p ◁ₗ{β} bytewise P ly) (PtrOffsetOp u8) (IntOp it) PtrOp :=

theories/typing/own.v

@@ -155,13 +155,18 @@ Section own.
   Qed.
 
   Lemma type_offset_of_sub v1 l s m P ly T:
-    ⌜ly_size ly = 1%nat⌝ ∗ (P -∗ T (val_of_loc l) (t2mt (l @ frac_ptr Own (place l)))) -∗
+    ⌜ly_size ly = 1%nat⌝ ∗ (
+      (P -∗ loc_in_bounds l 0 ∗ True) ∧ (P -∗ T (val_of_loc l) (t2mt (l @ frac_ptr Own (place l))))) -∗
     typed_bin_op v1 (v1 ◁ᵥ offsetof s m) (l at{s}ₗ m) P (PtrNegOffsetOp ly) (IntOp size_t) PtrOp T.
   Proof.
     iDestruct 1 as (Hly) "HT". iIntros ([n [Ho Hi]]) "HP". iIntros (Φ) "HΦ".
-    iApply wp_ptr_neg_offset. by apply val_to_of_loc. done. iModIntro.
-    rewrite offset_loc_sz1 // /GetMemberLoc shift_loc_assoc Ho /= Z.add_opp_diag_r shift_loc_0.
-    iApply "HΦ"; [ | by iApply "HT"]. done.
+    iAssert (loc_in_bounds l 0) as "#Hlib".
+    { iDestruct "HT" as "[HT _]". by iDestruct ("HT" with "HP") as "[$ _]". }
+    iDestruct "HT" as "[_ HT]".
+    iApply wp_ptr_neg_offset. by apply val_to_of_loc. done.
+    all: rewrite offset_loc_sz1 // /GetMemberLoc shift_loc_assoc Ho /= Z.add_opp_diag_r shift_loc_0.
+    1: done.
+    iModIntro. iApply "HΦ"; [ | by iApply "HT"]. done.
   Qed.
   Global Instance type_offset_of_sub_inst v1 l s m P ly:
     TypedBinOp v1 (v1 ◁ᵥ offsetof s m) (l at{s}ₗ m) P (PtrNegOffsetOp ly) (IntOp size_t) PtrOp :=

theories/typing/padded.v

@@ -199,10 +199,13 @@ Section padded.
     move: (Hint) => /val_to_Z_weak_in_range?.
     iDestruct ("HT" with "[//]") as (???) "HT".
     iDestruct (split_padded (Z.to_nat n) with "Hp") as "[H1 H2]"; [lia..|].
-    iApply wp_ptr_offset. by apply val_to_of_loc. done. done.
-    iModIntro. rewrite offset_loc_sz1//.
-    iApply ("HΦ" with "[H2]"). 2: iApply ("HT" with "H1 []"). rewrite Z2Nat.id; [|lia]. by iFrame.
-    by iPureIntro.
+    rewrite -!(offset_loc_sz1 u8)// Z2Nat.id; [|lia].
+    iDestruct (loc_in_bounds_in_bounds with "H2") as "#?".
+    iApply wp_ptr_offset; [ by apply val_to_of_loc | done | |].
+    { iApply loc_in_bounds_shorten; [|done]; lia. }
+    iModIntro. iApply ("HΦ" with "[H2]"). 2: iApply ("HT" with "H1 []").
+    - by iFrame.
+    - by iPureIntro.
   Qed.
   Global Instance type_add_padded_inst v2 β ly lyty ty (p : loc) n it:
     TypedBinOp v2 (v2 ◁ᵥ n @ int it)%I p (p ◁ₗ{β} padded ty lyty ly)%I (PtrOffsetOp u8) (IntOp it) PtrOp :=

theories/typing/struct.v

@@ -214,8 +214,9 @@ Section struct.
     iDestruct 1 as (i ty1 Hi Hn) "HP".
     move: (Hi) => /field_index_of_to_index_of[? Hi2].
     iIntros (Φ) "Hs HΦ" => /=.
+    iDestruct (loc_in_bounds_in_bounds with "Hs") as "#Hlib".
     iApply (wp_step_fupd with "[Hs]"). done. 2: by iApply (do_strip_guarded with "Hs"). solve_ndisj.
-    iApply wp_get_member. by apply val_to_of_loc. by eauto.
+    iApply wp_get_member. by apply val_to_of_loc. by eauto. done.
     iIntros "!# [% [% [#Hb Hs]]] !#". iExists _. iSplit => //.
     iDestruct (big_sepL_insert_acc with "Hs") as "[Hl Hs]" => //=. by eapply pad_struct_lookup_field.
     rewrite /GetMemberLoc/offset_of Hi2/=.