Stricter formal semantics for free

backend/Inliningproof.v

@@ -1177,6 +1177,8 @@ Proof.
     instantiate (1 := sp'). auto.
     (* offset is representable *)
     instantiate (1 := dstk ctx). generalize (Z.le_max_r (fn_stacksize f) 0). lia.
+    (* negative offsets are not revealed *)
+    right; lia.
     (* size of target block is representable *)
     intros. right. exploit SSZ2; eauto with mem. inv FB; lia.
     (* we have full permissions on sp' at and above dstk ctx *)

backend/Unusedglobproof.v

@@ -1196,6 +1196,7 @@ Proof.
   apply Q2 in H0. destruct H0. subst.
   left. apply Mem.perm_cur. eapply Mem.perm_implies; eauto.
   apply P1. lia.
+- apply init_meminj_invert in H. tauto.
 Qed.
 
 End INIT_MEM.

backend/ValueDomain.v

@@ -5035,6 +5035,9 @@ Proof.
 - (* perm inv *)
   intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst.
   rewrite Z.add_0_r in H2. auto.
+- (* metadata *)
+  intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst.
+  auto.
 Qed.
 
 Lemma inj_of_bc_preserves_globals:

cfrontend/Cexec.v

@@ -505,18 +505,17 @@ Definition do_ef_free
        (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
   match vargs with
   | Vptr b lo :: nil =>
-      do vsz <- Mem.load Mptr m b (Ptrofs.unsigned lo - size_chunk Mptr);
+      check (Ptrofs.eq_dec lo Ptrofs.zero);
+      do vsz <- Mem.load Mptr m b (- size_chunk Mptr);
       do sz <- do_alloc_size vsz;
-      do m' <- Mem.free m b (Ptrofs.unsigned lo - size_chunk Mptr) (Ptrofs.unsigned lo + Ptrofs.unsigned sz);
+      do m' <- Mem.free m b (- size_chunk Mptr) (Ptrofs.unsigned sz);
       Some(w, E0, Vundef, m')
   | Vint n :: nil =>
-      if Int.eq_dec n Int.zero && negb Archi.ptr64
-      then Some(w, E0, Vundef, m)
-      else None
+      check (Int.eq_dec n Int.zero && negb Archi.ptr64);
+      Some(w, E0, Vundef, m)
   | Vlong n :: nil =>
-      if Int64.eq_dec n Int64.zero && Archi.ptr64
-      then Some(w, E0, Vundef, m)
-      else None
+      check (Int64.eq_dec n Int64.zero && Archi.ptr64);
+      Some(w, E0, Vundef, m)
   | _ => None
   end.
 
@@ -628,7 +627,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.
+  split. apply SIZE in Heqo0. subst v. econstructor; eauto.
   constructor.
 - (* EF_memcpy *)
   unfold do_ef_memcpy. destruct vargs... destruct v... destruct vargs...
@@ -685,7 +684,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 H2. auto.
++ inv H0. rewrite dec_eq_true. 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.

cfrontend/Cminorgenproof.v

@@ -817,24 +817,23 @@ Lemma match_callstack_alloc_variables_rec:
 Proof.
   intros until cs; intros VALID REPRES STKSIZE STKPERMS.
   induction 1; intros f1 NOREPET COMPAT SEP1 SEP2 UNBOUND MCS MINJ.
-  (* base case *)
+- (* base case *)
   simpl in MCS. exists f1; auto.
-  (* inductive case *)
+- (* inductive case *)
   simpl in NOREPET. inv NOREPET.
-(* exploit Mem.alloc_result; eauto. intros RES.
-  exploit Mem.nextblock_alloc; eauto. intros NB.*)
   exploit (COMPAT id sz). auto with coqlib. intros [ofs [CENV [ALIGNED [LOB HIB]]]].
   exploit Mem.alloc_left_mapped_inject.
     eexact MINJ.
     eexact H.
     eexact VALID.
-    instantiate (1 := ofs). zify. lia.
+    instantiate (1 := ofs). lia.
+    right; lia.
     intros. exploit STKSIZE; eauto. lia.
-    intros. apply STKPERMS. zify. lia.
+    intros. apply STKPERMS. lia.
     replace (sz - 0) with sz by lia. auto.
     intros. eapply SEP2. eauto with coqlib. eexact CENV. eauto. eauto. lia.
-  intros [f2 [A [B [C D]]]].
-  exploit (IHalloc_variables f2); eauto.
+  intros (f2 & A & B & C & D).
+  eapply (IHalloc_variables f2); eauto.
     red; intros. eapply COMPAT. auto with coqlib.
     red; intros. eapply SEP1; eauto with coqlib.
     red; intros. exploit Mem.perm_alloc_inv; eauto. destruct (eq_block b b1); intros P.

common/Events.v

@@ -1060,10 +1060,10 @@ Qed.
 
 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) ->
-      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_ptr: forall b sz m m',
+      Mem.load Mptr m b (- size_chunk Mptr) = Some (Vptrofs sz) ->
+      Mem.free m b (- size_chunk Mptr) (Ptrofs.unsigned sz) = Some m' ->
+      extcall_free_sem ge (Vptr b Ptrofs.zero :: nil) m E0 Vundef m'
   | extcall_free_sem_null: forall m,
       extcall_free_sem ge (Vnullptr :: nil) m E0 Vundef m.
 
@@ -1115,25 +1115,22 @@ Proof.
   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.
-  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. }
+  assert (delta = 0).
+  { eapply Mem.mi_metadata; eauto.
+    instantiate (1 := - size_chunk Mptr). eauto with mem.
+    generalize (size_chunk_pos Mptr). lia. }
+  subst delta.
   exploit Mem.free_parallel_inject; eauto. intros (m2' & C & D).
+  rewrite ! Z.add_0_r in *.
   exists f, Vundef, m2'; split.
-  apply extcall_free_sem_ptr with (sz := sz) (m' := m2').
-    rewrite EQ. rewrite <- A. f_equal. lia.
-    auto. auto.
-    rewrite ! EQ. rewrite <- C. f_equal; lia.
+  apply extcall_free_sem_ptr with (sz := sz) (m' := m2'); auto.
   split. auto.
   split. auto.
   split. eapply Mem.free_unchanged_on; eauto. unfold loc_unmapped. intros; congruence.
   split. eapply Mem.free_unchanged_on; eauto. unfold loc_out_of_reach.
     intros. red; intros. eelim H2; eauto.
     apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem.
-    apply P. lia.
+    eapply Mem.free_range_perm; eauto. lia.
   split. auto.
   red; intros. congruence.
 + inv H2. inv H6. replace v' with Vnullptr.