RFC: stable memory block names for globals

Makefile

@@ -63,7 +63,7 @@ VLIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \
 # Parts common to the front-ends and the back-end (in common/)
 
 COMMON=Errors.v AST.v Linking.v \
-  Events.v Globalenvs.v Memdata.v Memtype.v Memory.v \
+  Events.v Globalenvs.v Memdata.v Memtype.v Memory.v BlockNames.v \
   Values.v Smallstep.v Behaviors.v Switch.v Determinism.v Unityping.v \
   Separation.v
 

backend/Deadcodeproof.v

@@ -48,8 +48,8 @@ Record magree (m1 m2: mem) (P: locset) : Prop := mk_magree {
     forall b ofs,
     Mem.perm m1 b ofs Cur Readable ->
     P b ofs ->
-    memval_lessdef (ZMap.get ofs (PMap.get b (Mem.mem_contents m1)))
-                   (ZMap.get ofs (PMap.get b (Mem.mem_contents m2)));
+    memval_lessdef (ZMap.get ofs (BMap.get b (Mem.mem_contents m1)))
+                   (ZMap.get ofs (BMap.get b (Mem.mem_contents m2)));
   ma_nextblock:
     Mem.nextblock m2 = Mem.nextblock m1
 }.
@@ -165,7 +165,7 @@ Proof.
   intuition eauto using Mem.perm_storebytes_1, Mem.perm_storebytes_2.
 - rewrite (Mem.storebytes_mem_contents _ _ _ _ _ H0).
   rewrite (Mem.storebytes_mem_contents _ _ _ _ _ ST2).
-  rewrite ! PMap.gsspec. destruct (peq b0 b).
+  rewrite ! BMap.gsspec. destruct (BMap.elt_eq b0 b).
 + subst b0. apply SETN with (access := fun ofs => Mem.perm m1' b ofs Cur Readable /\ Q b ofs); auto.
   intros. destruct H5. eapply ma_memval; eauto.
   eapply Mem.perm_storebytes_2; eauto.
@@ -209,7 +209,7 @@ Proof.
 - exploit ma_perm_inv; eauto.
   intuition eauto using Mem.perm_storebytes_1, Mem.perm_storebytes_2.
 - rewrite (Mem.storebytes_mem_contents _ _ _ _ _ H0).
-  rewrite PMap.gsspec. destruct (peq b0 b).
+  rewrite BMap.gsspec. destruct (BMap.elt_eq b0 b).
 + subst b0. rewrite Mem.setN_outside. eapply ma_memval; eauto. eapply Mem.perm_storebytes_2; eauto.
   destruct (zlt ofs0 ofs); auto. destruct (zle (ofs + Z.of_nat (length bytes1)) ofs0); try omega.
   elim (H1 ofs0). omega. auto.

backend/Inliningproof.v

@@ -349,7 +349,7 @@ Proof.
   intros. red in SEP. destruct (F b) as [[sp1 delta1] |] eqn:?.
   exploit INCR; eauto. intros EQ; rewrite H0 in EQ; inv EQ.
   red; intros; eelim B; eauto. eapply PERM; eauto.
-  red. destruct (plt b (Mem.nextblock m1)); auto.
+  red. destruct (Block.lt_dec b (Mem.nextblock m1)); auto.
   exploit Mem.mi_freeblocks; eauto. congruence.
   exploit SEP; eauto. tauto.
 Qed.
@@ -358,11 +358,11 @@ Qed.
 
 Inductive match_globalenvs (F: meminj) (bound: block): Prop :=
   | mk_match_globalenvs
-      (DOMAIN: forall b, Plt b bound -> F b = Some(b, 0))
-      (IMAGE: forall b1 b2 delta, F b1 = Some(b2, delta) -> Plt b2 bound -> b1 = b2)
-      (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> Plt b bound)
-      (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> Plt b bound)
-      (VARINFOS: forall b gv, Genv.find_var_info ge b = Some gv -> Plt b bound).
+      (DOMAIN: forall b, Block.lt b bound -> F b = Some(b, 0))
+      (IMAGE: forall b1 b2 delta, F b1 = Some(b2, delta) -> Block.lt b2 bound -> b1 = b2)
+      (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> Block.lt b bound)
+      (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> Block.lt b bound)
+      (VARINFOS: forall b gv, Genv.find_var_info ge b = Some gv -> Block.lt b bound).
 
 Lemma find_function_agree:
   forall ros rs fd F ctx rs' bound,
@@ -469,7 +469,7 @@ Inductive match_stacks (F: meminj) (m m': mem):
              list stackframe -> list stackframe -> block -> Prop :=
   | match_stacks_nil: forall bound1 bound
         (MG: match_globalenvs F bound1)
-        (BELOW: Ple bound1 bound),
+        (BELOW: Block.le bound1 bound),
       match_stacks F m m' nil nil bound
   | match_stacks_cons: forall res f sp pc rs stk f' sp' rs' stk' bound fenv ctx
         (MS: match_stacks_inside F m m' stk stk' f' ctx sp' rs')
@@ -481,7 +481,7 @@ Inductive match_stacks (F: meminj) (m m': mem):
         (SSZ1: 0 <= f'.(fn_stacksize) < Ptrofs.max_unsigned)
         (SSZ2: forall ofs, Mem.perm m' sp' ofs Max Nonempty -> 0 <= ofs <= f'.(fn_stacksize))
         (RES: Ple res ctx.(mreg))
-        (BELOW: Plt sp' bound),
+        (BELOW: Block.lt sp' bound),
       match_stacks F m m'
                    (Stackframe res f (Vptr sp Ptrofs.zero) pc rs :: stk)
                    (Stackframe (sreg ctx res) f' (Vptr sp' Ptrofs.zero) (spc ctx pc) rs' :: stk')
@@ -492,7 +492,7 @@ Inductive match_stacks (F: meminj) (m m': mem):
         (SSZ1: 0 <= f'.(fn_stacksize) < Ptrofs.max_unsigned)
         (SSZ2: forall ofs, Mem.perm m' sp' ofs Max Nonempty -> 0 <= ofs <= f'.(fn_stacksize))
         (RET: ctx.(retinfo) = Some (rpc, res))
-        (BELOW: Plt sp' bound),
+        (BELOW: Block.lt sp' bound),
       match_stacks F m m'
                    stk
                    (Stackframe res f' (Vptr sp' Ptrofs.zero) rpc rs' :: stk')
@@ -555,13 +555,13 @@ Qed.
 Lemma match_stacks_bound:
   forall stk stk' bound bound1,
   match_stacks F m m' stk stk' bound ->
-  Ple bound bound1 ->
+  Block.le bound bound1 ->
   match_stacks F m m' stk stk' bound1.
 Proof.
   intros. inv H.
-  apply match_stacks_nil with bound0. auto. eapply Ple_trans; eauto.
-  eapply match_stacks_cons; eauto. eapply Pos.lt_le_trans; eauto.
-  eapply match_stacks_untailcall; eauto. eapply Pos.lt_le_trans; eauto.
+  apply match_stacks_nil with bound0. auto. eapply Block.le_trans; eauto.
+  eapply match_stacks_cons; eauto. blomega.
+  eapply match_stacks_untailcall; eauto. blomega.
 Qed.
 
 Variable F1: meminj.
@@ -571,13 +571,13 @@ Hypothesis INCR: inject_incr F F1.
 Lemma match_stacks_invariant:
   forall stk stk' bound, match_stacks F m m' stk stk' bound ->
   forall (INJ: forall b1 b2 delta,
-               F1 b1 = Some(b2, delta) -> Plt b2 bound -> F b1 = Some(b2, delta))
+               F1 b1 = Some(b2, delta) -> Block.lt b2 bound -> F b1 = Some(b2, delta))
          (PERM1: forall b1 b2 delta ofs,
-               F1 b1 = Some(b2, delta) -> Plt b2 bound ->
+               F1 b1 = Some(b2, delta) -> Block.lt b2 bound ->
                Mem.perm m1 b1 ofs Max Nonempty -> Mem.perm m b1 ofs Max Nonempty)
-         (PERM2: forall b ofs, Plt b bound ->
+         (PERM2: forall b ofs, Block.lt b bound ->
                Mem.perm m' b ofs Cur Freeable -> Mem.perm m1' b ofs Cur Freeable)
-         (PERM3: forall b ofs k p, Plt b bound ->
+         (PERM3: forall b ofs k p, Block.lt b bound ->
                Mem.perm m1' b ofs k p -> Mem.perm m' b ofs k p),
   match_stacks F1 m1 m1' stk stk' bound
 
@@ -587,13 +587,13 @@ with match_stacks_inside_invariant:
   forall rs2
          (RS: forall r, Plt r ctx.(dreg) -> rs2#r = rs1#r)
          (INJ: forall b1 b2 delta,
-               F1 b1 = Some(b2, delta) -> Ple b2 sp' -> F b1 = Some(b2, delta))
+               F1 b1 = Some(b2, delta) -> Block.le b2 sp' -> F b1 = Some(b2, delta))
          (PERM1: forall b1 b2 delta ofs,
-               F1 b1 = Some(b2, delta) -> Ple b2 sp' ->
+               F1 b1 = Some(b2, delta) -> Block.le b2 sp' ->
                Mem.perm m1 b1 ofs Max Nonempty -> Mem.perm m b1 ofs Max Nonempty)
-         (PERM2: forall b ofs, Ple b sp' ->
+         (PERM2: forall b ofs, Block.le b sp' ->
                Mem.perm m' b ofs Cur Freeable -> Mem.perm m1' b ofs Cur Freeable)
-         (PERM3: forall b ofs k p, Ple b sp' ->
+         (PERM3: forall b ofs k p, Block.le b sp' ->
                Mem.perm m1' b ofs k p -> Mem.perm m' b ofs k p),
   match_stacks_inside F1 m1 m1' stk stk' f' ctx sp' rs2.
 
@@ -602,44 +602,30 @@ Proof.
   (* nil *)
   apply match_stacks_nil with (bound1 := bound1).
   inv MG. constructor; auto.
-  intros. apply IMAGE with delta. eapply INJ; eauto. eapply Pos.lt_le_trans; eauto.
-  auto. auto.
+  intros. apply IMAGE with delta. eapply INJ; eauto. blomega. blomega.
+  auto.
   (* cons *)
   apply match_stacks_cons with (fenv := fenv) (ctx := ctx); auto.
-  eapply match_stacks_inside_invariant; eauto.
-  intros; eapply INJ; eauto; xomega.
-  intros; eapply PERM1; eauto; xomega.
-  intros; eapply PERM2; eauto; xomega.
-  intros; eapply PERM3; eauto; xomega.
+  eapply match_stacks_inside_invariant; eauto; blomega.
   eapply agree_regs_incr; eauto.
   eapply range_private_invariant; eauto.
   (* untailcall *)
   apply match_stacks_untailcall with (ctx := ctx); auto.
-  eapply match_stacks_inside_invariant; eauto.
-  intros; eapply INJ; eauto; xomega.
-  intros; eapply PERM1; eauto; xomega.
-  intros; eapply PERM2; eauto; xomega.
-  intros; eapply PERM3; eauto; xomega.
+  eapply match_stacks_inside_invariant; eauto; blomega.
   eapply range_private_invariant; eauto.
 
   induction 1; intros.
   (* base *)
   eapply match_stacks_inside_base; eauto.
-  eapply match_stacks_invariant; eauto.
-  intros; eapply INJ; eauto; xomega.
-  intros; eapply PERM1; eauto; xomega.
-  intros; eapply PERM2; eauto; xomega.
-  intros; eapply PERM3; eauto; xomega.
+  eapply match_stacks_invariant; eauto; blomega.
   (* inlined *)
   apply match_stacks_inside_inlined with (fenv := fenv) (ctx' := ctx'); auto.
   apply IHmatch_stacks_inside; auto.
   intros. apply RS. red in BELOW. xomega.
   apply agree_regs_incr with F; auto.
   apply agree_regs_invariant with rs'; auto.
   intros. apply RS. red in BELOW. xomega.
-  eapply range_private_invariant; eauto.
-    intros. split. eapply INJ; eauto. xomega. eapply PERM1; eauto. xomega.
-    intros. eapply PERM2; eauto. xomega.
+  eapply range_private_invariant; eauto; blomega.
 Qed.
 
 Lemma match_stacks_empty:
@@ -711,10 +697,10 @@ Proof.
   eapply match_stacks_inside_base; eauto.
   eapply match_stacks_invariant; eauto.
   intros. destruct (eq_block b1 b).
-  subst b1. rewrite H1 in H4; inv H4. eelim Plt_strict; eauto.
+  subst b1. rewrite H1 in H4; inv H4. eelim Block.lt_strict; eauto.
   rewrite H2 in H4; auto.
   intros. exploit Mem.perm_alloc_inv; eauto. destruct (eq_block b1 b); intros; auto.
-  subst b1. rewrite H1 in H4. inv H4. eelim Plt_strict; eauto.
+  subst b1. rewrite H1 in H4. inv H4. eelim Block.lt_strict; eauto.
   (* inlined *)
   eapply match_stacks_inside_inlined; eauto.
   eapply IHmatch_stacks_inside; eauto. destruct SBELOW. omega.
@@ -744,7 +730,7 @@ Lemma match_stacks_free_right:
   match_stacks F m m1' stk stk' sp.
 Proof.
   intros. eapply match_stacks_invariant; eauto.
-  intros. eapply Mem.perm_free_1; eauto.
+  intros. eapply Mem.perm_free_1; eauto. blomega.
   intros. eapply Mem.perm_free_3; eauto.
 Qed.
 
@@ -790,32 +776,32 @@ Hypothesis SEP: inject_separated F1 F2 m1 m1'.
 Lemma match_stacks_extcall:
   forall stk stk' bound,
   match_stacks F1 m1 m1' stk stk' bound ->
-  Ple bound (Mem.nextblock m1') ->
+  Block.le bound (Mem.nextblock m1') ->
   match_stacks F2 m2 m2' stk stk' bound
 with match_stacks_inside_extcall:
   forall stk stk' f' ctx sp' rs',
   match_stacks_inside F1 m1 m1' stk stk' f' ctx sp' rs' ->
-  Plt sp' (Mem.nextblock m1') ->
+  Block.lt sp' (Mem.nextblock m1') ->
   match_stacks_inside F2 m2 m2' stk stk' f' ctx sp' rs'.
 Proof.
   induction 1; intros.
   apply match_stacks_nil with bound1; auto.
     inv MG. constructor; intros; eauto.
     destruct (F1 b1) as [[b2' delta']|] eqn:?.
     exploit INCR; eauto. intros EQ; rewrite H0 in EQ; inv EQ. eapply IMAGE; eauto.
-    exploit SEP; eauto. intros [A B]. elim B. red. xomega.
+    exploit SEP; eauto. intros [A B]. elim B. red. blomega.
   eapply match_stacks_cons; eauto.
-    eapply match_stacks_inside_extcall; eauto. xomega.
+    eapply match_stacks_inside_extcall; eauto. blomega.
     eapply agree_regs_incr; eauto.
-    eapply range_private_extcall; eauto. red; xomega.
-    intros. apply SSZ2; auto. apply MAXPERM'; auto. red; xomega.
+    eapply range_private_extcall; eauto. red. blomega.
+    intros. apply SSZ2; auto. apply MAXPERM'; auto. red. blomega.
   eapply match_stacks_untailcall; eauto.
-    eapply match_stacks_inside_extcall; eauto. xomega.
-    eapply range_private_extcall; eauto. red; xomega.
-    intros. apply SSZ2; auto. apply MAXPERM'; auto. red; xomega.
+    eapply match_stacks_inside_extcall; eauto. blomega.
+    eapply range_private_extcall; eauto. red. blomega.
+    intros. apply SSZ2; auto. apply MAXPERM'; auto. red. blomega.
   induction 1; intros.
   eapply match_stacks_inside_base; eauto.
-    eapply match_stacks_extcall; eauto. xomega.
+    eapply match_stacks_extcall; eauto. blomega.
   eapply match_stacks_inside_inlined; eauto.
     eapply agree_regs_incr; eauto.
     eapply range_private_extcall; eauto.
@@ -1043,9 +1029,9 @@ Proof.
   eapply match_stacks_bound with (bound := sp').
   eapply match_stacks_invariant; eauto.
     intros. eapply Mem.perm_free_3; eauto.
-    intros. eapply Mem.perm_free_1; eauto.
-    intros. eapply Mem.perm_free_3; eauto.
-  erewrite Mem.nextblock_free; eauto. red in VB; xomega.
+    intros. eapply Mem.perm_free_1; eauto; blomega.
+    intros. eapply Mem.perm_free_3; eauto. 
+  erewrite Mem.nextblock_free; eauto. blomega.
   eapply agree_val_regs; eauto.
   eapply Mem.free_right_inject; eauto. eapply Mem.free_left_inject; eauto.
   (* show that no valid location points into the stack block being freed *)
@@ -1135,9 +1121,9 @@ Proof.
   eapply match_stacks_bound with (bound := sp').
   eapply match_stacks_invariant; eauto.
     intros. eapply Mem.perm_free_3; eauto.
-    intros. eapply Mem.perm_free_1; eauto.
+    intros. eapply Mem.perm_free_1; eauto. blomega.
     intros. eapply Mem.perm_free_3; eauto.
-  erewrite Mem.nextblock_free; eauto. red in VB; xomega.
+  erewrite Mem.nextblock_free; eauto. blomega.
   destruct or; simpl. apply agree_val_reg; auto. auto.
   eapply Mem.free_right_inject; eauto. eapply Mem.free_left_inject; eauto.
   (* show that no valid location points into the stack block being freed *)
@@ -1175,15 +1161,15 @@ Proof.
   rewrite <- SP in MS0.
   eapply match_stacks_invariant; eauto.
     intros. destruct (eq_block b1 stk).
-    subst b1. rewrite D in H8; inv H8. eelim Plt_strict; eauto.
+    subst b1. rewrite D in H8; inv H8. eelim Block.lt_strict; eauto.
     rewrite E in H8; auto.
     intros. exploit Mem.perm_alloc_inv. eexact H. eauto.
     destruct (eq_block b1 stk); intros; auto.
-    subst b1. rewrite D in H8; inv H8. eelim Plt_strict; eauto.
+    subst b1. rewrite D in H8; inv H8. eelim Block.lt_strict; eauto.
     intros. eapply Mem.perm_alloc_1; eauto.
     intros. exploit Mem.perm_alloc_inv. eexact A. eauto.
     rewrite dec_eq_false; auto.
-  auto. auto. auto. eauto. auto.
+  blomega. auto. auto. eauto. auto.
   rewrite H5. apply agree_regs_init_regs. eauto. auto. inv H1; auto. congruence. auto.
   eapply Mem.valid_new_block; eauto.
   red; intros. split.
@@ -1245,7 +1231,7 @@ Proof.
     eapply match_stacks_extcall with (F1 := F) (F2 := F1) (m1 := m) (m1' := m'0); eauto.
     intros; eapply external_call_max_perm; eauto.
     intros; eapply external_call_max_perm; eauto.
-    xomega.
+    blomega.
     eapply external_call_nextblock; eauto.
     auto. auto.
 
@@ -1302,11 +1288,12 @@ Proof.
   apply match_stacks_nil with (Mem.nextblock m0).
   constructor; intros.
     unfold Mem.flat_inj. apply pred_dec_true; auto.
-    unfold Mem.flat_inj in H. destruct (plt b1 (Mem.nextblock m0)); congruence.
+    unfold Mem.flat_inj in H. destruct (Block.lt_dec b1 (Mem.nextblock m0)); congruence.
     eapply Genv.find_symbol_not_fresh; eauto.
     eapply Genv.find_funct_ptr_not_fresh; eauto.
     eapply Genv.find_var_info_not_fresh; eauto.
-    apply Ple_refl.
+    blomega.
+  erewrite <- Genv.init_mem_genv_next; eauto.
   eapply Genv.initmem_inject; eauto.
 Qed.
 

backend/Stackingproof.v

@@ -2116,11 +2116,11 @@ Proof.
   constructor. red; intros. rewrite H3, loc_arguments_main in H. contradiction.
   red; simpl; auto.
   simpl. rewrite sep_pure. split; auto. split;[|split].
-  eapply Genv.initmem_inject; eauto.
-  simpl. exists (Mem.nextblock m0); split. apply Ple_refl.
+  unfold j. erewrite <- Genv.init_mem_genv_next; eauto. eapply Genv.initmem_inject; eauto.
+  simpl. exists (Mem.nextblock m0); split. apply Block.le_refl.
   unfold j, Mem.flat_inj; constructor; intros.
     apply pred_dec_true; auto.
-    destruct (plt b1 (Mem.nextblock m0)); congruence.
+    destruct (Block.lt_dec b1 (Mem.nextblock m0)); congruence.
     change (Mem.valid_block m0 b0). eapply Genv.find_symbol_not_fresh; eauto.
     change (Mem.valid_block m0 b0). eapply Genv.find_funct_ptr_not_fresh; eauto.
     change (Mem.valid_block m0 b0). eapply Genv.find_var_info_not_fresh; eauto.