Semantics of free(): remove requirement size > 0 (#509)

Zero-sized blocks work fine, with a slightly different proof of memory
injections in Events.v.

Co-authored-by: xavier.leroy@college-de-france.fr

Author: josuemoreau

cfrontend/Cexec.v

@@ -508,7 +508,6 @@ Definition do_ef_free
   | Vptr b lo :: nil =>
       do vsz <- Mem.load Mptr m b (Ptrofs.unsigned lo - size_chunk Mptr);
       do sz <- do_alloc_size vsz;
-      check (zlt 0 (Ptrofs.unsigned sz));
       do m' <- Mem.free m b (Ptrofs.unsigned lo - size_chunk Mptr) (Ptrofs.unsigned lo + Ptrofs.unsigned sz);
       Some(w, E0, Vundef, m')
   | Vint n :: nil =>
@@ -630,7 +629,7 @@ Proof with try congruence.
   replace (Vlong Int64.zero) with Vnullptr. split; constructor.
   unfold Vnullptr; rewrite H0; auto.
 + destruct vargs... mydestr.
-  split. apply SIZE in Heqo0. econstructor; eauto. congruence. lia.
+  split. apply SIZE in Heqo0. econstructor; eauto. congruence.
   constructor.
 - (* EF_memcpy *)
   unfold do_ef_memcpy. destruct vargs... destruct v... destruct vargs...
@@ -687,7 +686,7 @@ Proof.
   inv H0. erewrite SIZE by eauto. rewrite H1, H2. auto.
 - (* EF_free *)
   inv H; unfold do_ef_free.
-+ inv H0. rewrite H1. erewrite SIZE by eauto. rewrite zlt_true. rewrite H3. auto. lia.
++ inv H0. rewrite H1. erewrite SIZE by eauto. rewrite H2. auto.
 + inv H0. unfold Vnullptr; destruct Archi.ptr64; auto.
 - (* EF_memcpy *)
   inv H; unfold do_ef_memcpy.

common/Events.v

@@ -1068,7 +1068,6 @@ Inductive extcall_free_sem (ge: Senv.t):
               list val -> mem -> trace -> val -> mem -> Prop :=
   | extcall_free_sem_ptr: forall b lo sz m m',
       Mem.load Mptr m b (Ptrofs.unsigned lo - size_chunk Mptr) = Some (Vptrofs sz) ->
-      Ptrofs.unsigned sz > 0 ->
       Mem.free m b (Ptrofs.unsigned lo - size_chunk Mptr) (Ptrofs.unsigned lo + Ptrofs.unsigned sz) = Some m' ->
       extcall_free_sem ge (Vptr b lo :: nil) m E0 Vundef m'
   | extcall_free_sem_null: forall m,
@@ -1090,13 +1089,13 @@ Proof.
 (* readonly *)
 - eapply unchanged_on_readonly; eauto. inv H.
 + eapply Mem.free_unchanged_on; eauto.
-  intros. red; intros. elim H6.
+  intros. red; intros. elim H5.
   apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem.
   eapply Mem.free_range_perm; eauto.
 + apply Mem.unchanged_on_refl.
 (* mem extends *)
 - inv H.
-+ inv H1. inv H8. inv H6.
++ inv H1. inv H7. inv H5.
   exploit Mem.load_extends; eauto. intros [v' [A B]].
   assert (v' = Vptrofs sz).
   { unfold Vptrofs in *; destruct Archi.ptr64; inv B; auto. }
@@ -1108,7 +1107,7 @@ Proof.
   unfold loc_out_of_bounds; intros.
   assert (Mem.perm m1 b i Max Nonempty).
   { apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem.
-    eapply Mem.free_range_perm. eexact H4. eauto. }
+    eapply Mem.free_range_perm. eexact H3. eauto. }
   tauto.
 + inv H1. inv H5. replace v2 with Vnullptr.
   exists Vundef; exists m1'; intuition auto.
@@ -1117,18 +1116,17 @@ Proof.
   unfold Vnullptr in *; destruct Archi.ptr64; inv H3; auto.
 (* mem inject *)
 - inv H0.
-+ inv H2. inv H7. inv H9.
++ inv H2. inv H6. inv H8.
   exploit Mem.load_inject; eauto. intros [v' [A B]].
   assert (v' = Vptrofs sz).
   { unfold Vptrofs in *; destruct Archi.ptr64; inv B; auto. }
   subst v'.
   assert (P: Mem.range_perm m1 b (Ptrofs.unsigned lo - size_chunk Mptr) (Ptrofs.unsigned lo + Ptrofs.unsigned sz) Cur Freeable).
     eapply Mem.free_range_perm; eauto.
-  exploit Mem.address_inject; eauto.
-    apply Mem.perm_implies with Freeable; auto with mem.
-    apply P. instantiate (1 := lo).
-    generalize (size_chunk_pos Mptr); lia.
-  intro EQ.
+  assert (EQ: Ptrofs.unsigned (Ptrofs.add lo (Ptrofs.repr delta)) = Ptrofs.unsigned lo + delta).
+  { eapply Mem.address_inject_gen with (p := Freeable); eauto.
+    right. apply P.
+    generalize (size_chunk_pos Mptr), (Ptrofs.unsigned_range sz); lia. }
   exploit Mem.free_parallel_inject; eauto. intros (m2' & C & D).
   exists f, Vundef, m2'; split.
   apply extcall_free_sem_ptr with (sz := sz) (m' := m2').

common/Memory.v

@@ -3262,15 +3262,42 @@ Qed.
 (** The following lemmas establish the absence of machine integer overflow
   during address computations. *)
 
+Lemma address_inject_gen:
+  forall f m1 m2 b1 ofs1 b2 delta p,
+  inject f m1 m2 ->
+  perm m1 b1 (Ptrofs.unsigned ofs1) Cur p \/ perm m1 b1 (Ptrofs.unsigned ofs1 - 1) Cur p ->
+  f b1 = Some (b2, delta) ->
+  Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)) = Ptrofs.unsigned ofs1 + delta.
+Proof.
+  intros.
+  assert (perm m1 b1 (Ptrofs.unsigned ofs1) Max Nonempty
+       \/ perm m1 b1 (Ptrofs.unsigned ofs1 - 1) Max Nonempty)
+  by (destruct H0; eauto with mem).
+  exploit mi_representable; eauto. intros [A B].
+  assert (0 <= delta <= Ptrofs.max_unsigned).
+    generalize (Ptrofs.unsigned_range ofs1). lia.
+  unfold Ptrofs.add. repeat rewrite Ptrofs.unsigned_repr; lia.
+Qed.
+
 Lemma address_inject:
   forall f m1 m2 b1 ofs1 b2 delta p,
   inject f m1 m2 ->
   perm m1 b1 (Ptrofs.unsigned ofs1) Cur p ->
   f b1 = Some (b2, delta) ->
   Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)) = Ptrofs.unsigned ofs1 + delta.
+Proof.
+  intros; eapply address_inject_gen; eauto.
+Qed.
+
+Lemma address_inject_1:
+  forall f m1 m2 b1 ofs1 b2 delta p,
+  inject f m1 m2 ->
+  perm m1 b1 (Ptrofs.unsigned ofs1 - 1) Cur p ->
+  f b1 = Some (b2, delta) ->
+  Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)) = Ptrofs.unsigned ofs1 + delta.
 Proof.
   intros.
-  assert (perm m1 b1 (Ptrofs.unsigned ofs1) Max Nonempty) by eauto with mem.
+  assert (perm m1 b1 (Ptrofs.unsigned ofs1 - 1) Max Nonempty) by eauto with mem.
   exploit mi_representable; eauto. intros [A B].
   assert (0 <= delta <= Ptrofs.max_unsigned).
     generalize (Ptrofs.unsigned_range ofs1). lia.