Merge of the newmem and newextcalls branches:

- Revised memory model with concrete representation of ints & floats,
  and per-byte access permissions
- Revised Globalenvs implementation
- Matching changes in all languages and proofs.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1282 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

10 files changed, 122 insertions, 109 deletions

diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 60c3d34..fe6cf86 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -18,7 +18,7 @@ Require Import AST.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
-Require Import Mem.
+Require Import Memory.
 Require Import Events.
 Require Import Globalenvs.
 Require Import Smallstep.
@@ -126,7 +126,7 @@ Inductive instruction : Type :=
   | Peqv: ireg -> ireg -> ireg -> instruction                 (**r bitwise not-xor *)
   | Pextsb: ireg -> ireg -> instruction                       (**r 8-bit sign extension *)
   | Pextsh: ireg -> ireg -> instruction                       (**r 16-bit sign extension *)
-  | Pfreeframe: int -> instruction                            (**r deallocate stack frame and restore previous frame *)
+  | Pfreeframe: Z -> Z -> int -> instruction                  (**r deallocate stack frame and restore previous frame *)
   | Pfabs: freg -> freg -> instruction                        (**r float absolute value *)
   | Pfadd: freg -> freg -> freg -> instruction                (**r float addition *)
   | Pfcmpu: freg -> freg -> instruction                       (**r float comparison *)
@@ -285,7 +285,7 @@ lbl:    .long   0x43300000, 0x00000000
   This cannot be expressed in our memory model, which does not reflect
   the fact that stack frames are adjacent and allocated/freed
   following a stack discipline.
-- [Pfreeframe ofs]: in the formal semantics, this pseudo-instruction
+- [Pfreeframe lo hi ofs]: in the formal semantics, this pseudo-instruction
   reads the word at offset [ofs] in the block pointed by [r1] (the
   stack pointer), frees this block, and sets [r1] to the value of the
   word at offset [ofs].  In the printed PowerPC assembly code, this
@@ -349,7 +349,7 @@ Module Pregmap := EMap(PregEq).
   [Vzero] or [Vone]. *)
   
 Definition regset := Pregmap.t val.
-Definition genv := Genv.t fundef.
+Definition genv := Genv.t fundef unit.
 
 Notation "a # b" := (a b) (at level 1, only parsing).
 Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level).
@@ -651,12 +651,16 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
       OK (nextinstr (rs#rd <- (Val.sign_ext 8 rs#r1))) m
   | Pextsh rd r1 =>
       OK (nextinstr (rs#rd <- (Val.sign_ext 16 rs#r1))) m
-  | Pfreeframe ofs =>
+  | Pfreeframe lo hi ofs =>
       match Mem.loadv Mint32 m (Val.add rs#GPR1 (Vint ofs)) with
       | None => Error
       | Some v =>
           match rs#GPR1 with
-          | Vptr stk ofs => OK (nextinstr (rs#GPR1 <- v)) (Mem.free m stk)
+          | Vptr stk ofs =>
+              match Mem.free m stk lo hi with
+              | None => Error
+              | Some m' => OK (nextinstr (rs#GPR1 <- v)) m'
+              end
           | _ => Error
           end
       end
@@ -874,23 +878,23 @@ Inductive step: state -> trace -> state -> Prop :=
       exec_instr c i rs m = OK rs' m' ->
       step (State rs m) E0 (State rs' m')
   | exec_step_external:
-      forall b ef args res rs m t rs',
+      forall b ef args res rs m t rs' m',
       rs PC = Vptr b Int.zero ->
       Genv.find_funct_ptr ge b = Some (External ef) ->
-      event_match ef args t res ->
+      external_call ef args m t res m' ->
       extcall_arguments rs m ef.(ef_sig) args ->
       rs' = (rs#(loc_external_result ef.(ef_sig)) <- res
                #PC <- (rs LR)) ->
-      step (State rs m) t (State rs' m).
+      step (State rs m) t (State rs' m').
 
 End RELSEM.
 
 (** Execution of whole programs. *)
 
 Inductive initial_state (p: program): state -> Prop :=
-  | initial_state_intro:
+  | initial_state_intro: forall m0,
+      Genv.init_mem p = Some m0 ->
       let ge := Genv.globalenv p in
-      let m0 := Genv.init_mem p in
       let rs0 :=
         (Pregmap.init Vundef)
         # PC <- (symbol_offset ge p.(prog_main) Int.zero)
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index 2c65ca4..ca42d56 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -19,7 +19,7 @@ Require Import AST.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
-Require Import Mem.
+Require Import Memory.
 Require Import Globalenvs.
 Require Import Op.
 Require Import Locations.
@@ -487,12 +487,12 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) :=
       Pmtctr (ireg_of r) :: 
       Plwz GPR12 (Cint f.(fn_retaddr_ofs)) GPR1 ::
       Pmtlr GPR12 ::
-      Pfreeframe f.(fn_link_ofs) :: 
+      Pfreeframe (-f .(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: 
       Pbctr :: k
   | Mtailcall sig (inr symb) =>
       Plwz GPR12 (Cint f.(fn_retaddr_ofs)) GPR1 ::
       Pmtlr GPR12 ::
-      Pfreeframe f.(fn_link_ofs) :: 
+      Pfreeframe (-f .(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: 
       Pbs symb :: k
   | Mlabel lbl =>
       Plabel lbl :: k
@@ -508,7 +508,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) :=
   | Mreturn =>
       Plwz GPR12 (Cint f.(fn_retaddr_ofs)) GPR1 ::
       Pmtlr GPR12 ::
-      Pfreeframe f.(fn_link_ofs) ::
+      Pfreeframe (-f .(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) ::
       Pblr :: k
   end.
 
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index a2fc610..5be4734 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -19,7 +19,7 @@ Require Import AST.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
-Require Import Mem.
+Require Import Memory.
 Require Import Events.
 Require Import Globalenvs.
 Require Import Smallstep.
@@ -55,7 +55,7 @@ Lemma functions_translated:
   Genv.find_funct_ptr ge b = Some f ->
   exists tf, Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = Errors.OK tf.
 Proof
-  (Genv.find_funct_ptr_transf_partial transf_fundef TRANSF).
+  (Genv.find_funct_ptr_transf_partial transf_fundef _ TRANSF).
 
 Lemma functions_transl:
   forall f b,
@@ -776,13 +776,25 @@ Proof.
   rewrite <- H. apply eval_operation_preserved. exact symbols_preserved.
 Qed.
 
+Remark loadv_8_signed_unsigned:
+  forall m a v,
+  Mem.loadv Mint8signed m a = Some v ->
+  exists v', Mem.loadv Mint8unsigned m a = Some v' /\ v = Val.sign_ext 8 v'.
+Proof.
+  unfold Mem.loadv; intros. destruct a; try congruence.
+  generalize (Mem.load_int8_signed_unsigned m b (Int.signed i)).
+  rewrite H. destruct (Mem.load Mint8unsigned m b (Int.signed i)).
+  simpl; intros. exists v0; split; congruence.
+  simpl; congruence.
+Qed.
+
 Lemma exec_Mload_prop:
   forall (s : list stackframe) (fb : block) (sp : val)
          (chunk : memory_chunk) (addr : addressing) (args : list mreg)
          (dst : mreg) (c : list Mach.instruction) (ms : mreg -> val)
          (m : mem) (a v : val),
   eval_addressing ge sp addr ms ## args = Some a ->
-  loadv chunk m a = Some v ->
+  Mem.loadv chunk m a = Some v ->
   exec_instr_prop (Machconcr.State s fb sp (Mload chunk addr args dst :: c) ms m)
                E0 (Machconcr.State s fb sp c (Regmap.set dst v ms) m).
 Proof.
@@ -797,11 +809,7 @@ Proof.
   try (eapply transl_load_correct; eauto;
        intros; simpl; unfold preg_of; rewrite H6; auto).
   (* Mint8signed *)
-  generalize (loadv_8_signed_unsigned m a).
-  rewrite H0. 
-  caseEq (loadv Mint8unsigned m a);
-  [idtac | simpl;intros;discriminate].
-  intros v' LOAD' EQ. simpl in EQ. injection EQ. intro EQ1. clear EQ.
+  exploit loadv_8_signed_unsigned; eauto. intros [v' [LOAD EQ]].
   assert (X1: forall (cst : constant) (r1 : ireg) (rs1 : regset),
     exec_instr tge (transl_function f) (Plbz (ireg_of dst) cst r1) rs1 m =
     load1 tge Mint8unsigned (preg_of dst) cst r1 rs1 m).
@@ -815,30 +823,46 @@ Proof.
                 Mint8unsigned addr args 
                 (Pextsb (ireg_of dst) (ireg_of dst) :: transl_code f c) 
                 ms sp rs m dst a v'
-                X1 X2 AG H3 H7 LOAD').
+                X1 X2 AG H3 H7 LOAD).
   intros [rs2 [EX1 AG1]].
   exists (nextinstr (rs2#(ireg_of dst) <- v)).
   split. eapply exec_straight_trans. eexact EX1.
   apply exec_straight_one. simpl. 
   rewrite <- (ireg_val _ _ _ dst AG1);auto. rewrite Regmap.gss. 
-  rewrite EQ1. reflexivity. reflexivity. 
+  rewrite EQ. reflexivity. reflexivity. 
   eauto with ppcgen.
 Qed.
 
+Lemma storev_8_signed_unsigned:
+  forall m a v,
+  Mem.storev Mint8signed m a v = Mem.storev Mint8unsigned m a v.
+Proof.
+  intros. unfold Mem.storev. destruct a; auto.
+  apply Mem.store_signed_unsigned_8.
+Qed.
+
+Lemma storev_16_signed_unsigned:
+  forall m a v,
+  Mem.storev Mint16signed m a v = Mem.storev Mint16unsigned m a v.
+Proof.
+  intros. unfold Mem.storev. destruct a; auto.
+  apply Mem.store_signed_unsigned_16.
+Qed.
+
 Lemma exec_Mstore_prop:
   forall (s : list stackframe) (fb : block) (sp : val)
          (chunk : memory_chunk) (addr : addressing) (args : list mreg)
          (src : mreg) (c : list Mach.instruction) (ms : mreg -> val)
          (m m' : mem) (a : val),
   eval_addressing ge sp addr ms ## args = Some a ->
-  storev chunk m a (ms src) = Some m' ->
+  Mem.storev chunk m a (ms src) = Some m' ->
   exec_instr_prop (Machconcr.State s fb sp (Mstore chunk addr args src :: c) ms m) E0
                   (Machconcr.State s fb sp c ms m').
 Proof.
   intros; red; intros; inv MS.
   generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
   intro WTI; inversion WTI.
-  rewrite <- (eval_addressing_preserved symbols_preserved) in H.
+  rewrite <- (eval_addressing_preserved _ _ symbols_preserved) in H.
   left; eapply exec_straight_steps; eauto with coqlib. 
   destruct chunk; simpl; simpl in H6;
   try (rewrite storev_8_signed_unsigned in H0);
@@ -928,14 +952,15 @@ Qed.
 Lemma exec_Mtailcall_prop:
   forall (s : list stackframe) (fb stk : block) (soff : int)
          (sig : signature) (ros : mreg + ident) (c : list Mach.instruction)
-         (ms : Mach.regset) (m : mem) (f: Mach.function) (f' : block),
+         (ms : Mach.regset) (m : mem) (f: Mach.function) (f' : block) m',
   find_function_ptr ge ros ms = Some f' ->
   Genv.find_funct_ptr ge fb = Some (Internal f) ->
   load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) ->
   load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
+  Mem.free m stk (- f.(fn_framesize)) f.(fn_stacksize) = Some m' ->
   exec_instr_prop
           (Machconcr.State s fb (Vptr stk soff) (Mtailcall sig ros :: c) ms m) E0
-          (Callstate s f' ms (free m stk)).
+          (Callstate s f' ms m').
 Proof.
   intros; red; intros; inv MS.
   assert (f0 = f) by congruence. subst f0.
@@ -953,9 +978,9 @@ Proof.
   set (rs6 := rs5#PC <- (rs5 CTR)).
   assert (exec_straight tge (transl_function f)
             (transl_code f (Mtailcall sig (inl ident m0) :: c)) rs m 
-            (Pbctr :: transl_code f c) rs5 (free m stk)).
+            (Pbctr :: transl_code f c) rs5 m').
   simpl. apply exec_straight_step with rs2 m. 
-  simpl. rewrite <- (ireg_val _ _ _ _ AG H6). reflexivity. reflexivity.
+  simpl. rewrite <- (ireg_val _ _ _ _ AG H7). reflexivity. reflexivity.
   apply exec_straight_step with rs3 m.
   simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low.
   change (rs2 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG). 
@@ -966,13 +991,13 @@ Proof.
   apply exec_straight_one. 
   simpl. change (rs4 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG).
   unfold load_stack in H1; simpl in H1. 
-  simpl. rewrite H1. reflexivity. reflexivity.
-  left; exists (State rs6 (free m stk)); split.
+  simpl. rewrite H1. rewrite H3. reflexivity. reflexivity.
+  left; exists (State rs6 m'); split.
   (* execution *)
   eapply plus_right'. eapply exec_straight_exec; eauto.
   econstructor.
   change (rs5 PC) with (Val.add (Val.add (Val.add (Val.add (rs PC) Vone) Vone) Vone) Vone).
-  rewrite <- H7; simpl. eauto.
+  rewrite <- H8; simpl. eauto.
   eapply functions_transl; eauto. 
   eapply find_instr_tail.
   repeat (eapply code_tail_next_int; auto). eauto. 
@@ -983,7 +1008,7 @@ Proof.
     unfold rs4, rs3, rs2; auto 10 with ppcgen.
   assert (AG5: agree ms (parent_sp s) rs5).
     unfold rs5. apply agree_nextinstr.
-    split. reflexivity. intros. inv AG4. rewrite H12. 
+    split. reflexivity. intros. inv AG4. rewrite H13. 
     rewrite Pregmap.gso; auto with ppcgen.
   unfold rs6; auto with ppcgen.
   change (rs6 PC) with (ms m0). 
@@ -996,7 +1021,7 @@ Proof.
   set (rs5 := rs4#PC <- (Vptr f' Int.zero)).
   assert (exec_straight tge (transl_function f)
             (transl_code f (Mtailcall sig (inr mreg i) :: c)) rs m 
-            (Pbs i :: transl_code f c) rs4 (free m stk)).
+            (Pbs i :: transl_code f c) rs4 m').
   simpl. apply exec_straight_step with rs2 m. 
   simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low.
   rewrite <- (sp_val _ _ _ AG). 
@@ -1007,13 +1032,13 @@ Proof.
   apply exec_straight_one. 
   simpl. change (rs3 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG).
   unfold load_stack in H1; simpl in H1.
-  simpl. rewrite H1. reflexivity. reflexivity.
-  left; exists (State rs5 (free m stk)); split.
+  simpl. rewrite H1. rewrite H3. reflexivity. reflexivity.
+  left; exists (State rs5 m'); split.
   (* execution *)
   eapply plus_right'. eapply exec_straight_exec; eauto.
   econstructor.
   change (rs4 PC) with (Val.add (Val.add (Val.add (rs PC) Vone) Vone) Vone).
-  rewrite <- H7; simpl. eauto.
+  rewrite <- H8; simpl. eauto.
   eapply functions_transl; eauto. 
   eapply find_instr_tail.
   repeat (eapply code_tail_next_int; auto). eauto. 
@@ -1025,7 +1050,7 @@ Proof.
     unfold rs3, rs2; auto 10 with ppcgen.
   assert (AG4: agree ms (parent_sp s) rs4).
     unfold rs4. apply agree_nextinstr.
-    split. reflexivity. intros. inv AG3. rewrite H12. 
+    split. reflexivity. intros. inv AG3. rewrite H13. 
     rewrite Pregmap.gso; auto with ppcgen.
   unfold rs5; auto with ppcgen.
 Qed.
@@ -1191,12 +1216,13 @@ Qed.
 
 Lemma exec_Mreturn_prop:
   forall (s : list stackframe) (fb stk : block) (soff : int)
-         (c : list Mach.instruction) (ms : Mach.regset) (m : mem) (f: Mach.function),
+         (c : list Mach.instruction) (ms : Mach.regset) (m : mem) (f: Mach.function) m',
   Genv.find_funct_ptr ge fb = Some (Internal f) ->
   load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) ->
   load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
+  Mem.free m stk (- f.(fn_framesize)) f.(fn_stacksize) = Some m' ->
   exec_instr_prop (Machconcr.State s fb (Vptr stk soff) (Mreturn :: c) ms m) E0
-                  (Returnstate s ms (free m stk)).
+                  (Returnstate s ms m').
 Proof.
   intros; red; intros; inv MS.
   assert (f0 = f) by congruence. subst f0.
@@ -1206,7 +1232,7 @@ Proof.
   set (rs5 := rs4#PC <- (parent_ra s)).
   assert (exec_straight tge (transl_function f)
             (transl_code f (Mreturn :: c)) rs m 
-            (Pblr :: transl_code f c) rs4 (free m stk)).
+            (Pblr :: transl_code f c) rs4 m').
   simpl. apply exec_straight_three with rs2 m rs3 m.
   simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low.
   unfold load_stack in H1. simpl in H1. 
@@ -1216,18 +1242,18 @@ Proof.
   simpl. change (rs3 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG).
   simpl. 
   unfold load_stack in H0. simpl in H0.
-  rewrite H0. reflexivity.
+  rewrite H0. rewrite H2. reflexivity.
   reflexivity. reflexivity. reflexivity.
-  left; exists (State rs5 (free m stk)); split.
+  left; exists (State rs5 m'); split.
   (* execution *)
-  apply plus_right' with E0 (State rs4 (free m stk)) E0.
+  apply plus_right' with E0 (State rs4 m') E0.
   eapply exec_straight_exec; eauto.
   inv AT. econstructor.
   change (rs4 PC) with (Val.add (Val.add (Val.add (rs PC) Vone) Vone) Vone). 
-  rewrite <- H3. simpl. eauto.
+  rewrite <- H4. simpl. eauto.
   apply functions_transl; eauto.
-  generalize (functions_transl_no_overflow _ _ H4); intro NOOV.
-  simpl in H5. eapply find_instr_tail. 
+  generalize (functions_transl_no_overflow _ _ H5); intro NOOV.
+  simpl in H6. eapply find_instr_tail. 
   eapply code_tail_next_int; auto.
   eapply code_tail_next_int; auto.
   eapply code_tail_next_int; eauto.
@@ -1249,7 +1275,7 @@ Lemma exec_function_internal_prop:
   forall (s : list stackframe) (fb : block) (ms : Mach.regset)
          (m : mem) (f : function) (m1 m2 m3 : mem) (stk : block),
   Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  alloc m (- fn_framesize f) (fn_stacksize f) = (m1, stk) ->
+  Mem.alloc m (- fn_framesize f) (fn_stacksize f) = (m1, stk) ->
   let sp := Vptr stk (Int.repr (- fn_framesize f)) in
   store_stack m1 sp Tint f.(fn_link_ofs) (parent_sp s) = Some m2 ->
   store_stack m2 sp Tint f.(fn_retaddr_ofs) (parent_ra s) = Some m3 ->
@@ -1258,7 +1284,7 @@ Lemma exec_function_internal_prop:
 Proof.
   intros; red; intros; inv MS.
   assert (WTF: wt_function f).
-    generalize (Genv.find_funct_ptr_prop wt_fundef wt_prog H); intro TY.
+    generalize (Genv.find_funct_ptr_prop wt_fundef _ _ wt_prog H); intro TY.
     inversion TY; auto.
   exploit functions_transl; eauto. intro TFIND.
   generalize (functions_transl_no_overflow _ _ H); intro NOOV.
@@ -1307,19 +1333,19 @@ Qed.
 Lemma exec_function_external_prop:
   forall (s : list stackframe) (fb : block) (ms : Mach.regset)
          (m : mem) (t0 : trace) (ms' : RegEq.t -> val)
-         (ef : external_function) (args : list val) (res : val),
+         (ef : external_function) (args : list val) (res : val) (m': mem),
   Genv.find_funct_ptr ge fb = Some (External ef) ->
-  event_match ef args t0 res ->
+  external_call ef args m t0 res m' ->
   Machconcr.extcall_arguments ms m (parent_sp s) (ef_sig ef) args ->
   ms' = Regmap.set (Conventions.loc_result (ef_sig ef)) res ms ->
   exec_instr_prop (Machconcr.Callstate s fb ms m)
-               t0 (Machconcr.Returnstate s ms' m).
+               t0 (Machconcr.Returnstate s ms' m').
 Proof.
   intros; red; intros; inv MS.
   exploit functions_translated; eauto.
   intros [tf [A B]]. simpl in B. inv B. 
   left; exists (State (rs#(loc_external_result (ef_sig ef)) <- res #PC <- (rs LR))
-                m); split.
+                m'); split.
   apply plus_one. eapply exec_step_external; eauto. 
   eapply extcall_arguments_match; eauto. 
   econstructor; eauto.
@@ -1367,14 +1393,14 @@ Proof.
   intros. inversion H. unfold ge0 in *.
   econstructor; split.
   econstructor.
+  eapply Genv.init_mem_transf_partial; eauto.
   replace (symbol_offset (Genv.globalenv tprog) (prog_main tprog) Int.zero)
      with (Vptr fb Int.zero).
-  rewrite (Genv.init_mem_transf_partial _ _ TRANSF).
   econstructor; eauto. constructor.
   split. auto. intros. repeat rewrite Pregmap.gso; auto with ppcgen.
   unfold symbol_offset. 
   rewrite (transform_partial_program_main _ _ TRANSF). 
-  rewrite symbols_preserved. unfold ge; rewrite H0. auto.
+  rewrite symbols_preserved. unfold ge; rewrite H1. auto.
 Qed.
 
 Lemma transf_final_states:
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index 7329e53..60c4969 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -18,7 +18,7 @@ Require Import AST.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
-Require Import Mem.
+Require Import Memory.
 Require Import Globalenvs.
 Require Import Op.
 Require Import Locations.
diff --git a/powerpc/Asmgenretaddr.v b/powerpc/Asmgenretaddr.v
index d414752..d55635b 100644
--- a/powerpc/Asmgenretaddr.v
+++ b/powerpc/Asmgenretaddr.v
@@ -22,7 +22,7 @@ Require Import AST.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
-Require Import Mem.
+Require Import Memory.
 Require Import Globalenvs.
 Require Import Op.
 Require Import Locations.
diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v
index 2e28d23..b5e2e8e 100644
--- a/powerpc/ConstpropOpproof.v
+++ b/powerpc/ConstpropOpproof.v
@@ -17,7 +17,7 @@ Require Import AST.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
-Require Import Mem.
+Require Import Memory.
 Require Import Globalenvs.
 Require Import Op.
 Require Import Registers.
diff --git a/powerpc/Op.v b/powerpc/Op.v
index c6e196f..7a9aa50 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -29,7 +29,8 @@ Require Import AST.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
-Require Import Mem.
+Require Import Memdata.
+Require Import Memory.
 Require Import Globalenvs.
 
 Set Implicit Arguments.
@@ -182,7 +183,7 @@ Definition offset_sp (sp: val) (delta: int) : option val :=
   end.
 
 Definition eval_operation
-    (F: Type) (genv: Genv.t F) (sp: val)
+    (F V: Type) (genv: Genv.t F V) (sp: val)
     (op: operation) (vl: list val): option val :=
   match op, vl with
   | Omove, v1::nil => Some v1
@@ -265,7 +266,7 @@ Definition eval_operation
   end.
 
 Definition eval_addressing
-    (F: Type) (genv: Genv.t F) (sp: val)
+    (F V: Type) (genv: Genv.t F V) (sp: val)
     (addr: addressing) (vl: list val) : option val :=
   match addr, vl with
   | Aindexed n, Vptr b1 n1 :: nil =>
@@ -360,9 +361,9 @@ Qed.
 
 Section GENV_TRANSF.
 
-Variable F1 F2: Type.
-Variable ge1: Genv.t F1.
-Variable ge2: Genv.t F2.
+Variable F1 F2 V1 V2: Type.
+Variable ge1: Genv.t F1 V1.
+Variable ge2: Genv.t F2 V2.
 Hypothesis agree_on_symbols:
   forall (s: ident), Genv.find_symbol ge2 s = Genv.find_symbol ge1 s.
 
@@ -480,25 +481,14 @@ Definition type_of_addressing (addr: addressing) : list typ :=
   | Ainstack _ => nil
   end.
 
-Definition type_of_chunk (c: memory_chunk) : typ :=
-  match c with
-  | Mint8signed => Tint
-  | Mint8unsigned => Tint
-  | Mint16signed => Tint
-  | Mint16unsigned => Tint
-  | Mint32 => Tint
-  | Mfloat32 => Tfloat
-  | Mfloat64 => Tfloat
-  end.
-
 (** Weak type soundness results for [eval_operation]:
   the result values, when defined, are always of the type predicted
   by [type_of_operation]. *)
 
 Section SOUNDNESS.
 
-Variable A: Type.
-Variable genv: Genv.t A.
+Variable A V: Type.
+Variable genv: Genv.t A V.
 
 Lemma type_of_operation_sound:
   forall op vl sp v,
@@ -548,8 +538,7 @@ Proof.
   destruct v; destruct chunk; exact I.
   intros until v. unfold Mem.loadv. 
   destruct addr; intros; try discriminate.
-  generalize (Mem.load_inv _ _ _ _ _ H0).
-  intros [X Y].  subst v.  apply H.
+  eapply Mem.load_type; eauto.
 Qed.
 
 End SOUNDNESS.
@@ -560,8 +549,8 @@ End SOUNDNESS.
 
 Section EVAL_OP_TOTAL.
 
-Variable F: Type.
-Variable genv: Genv.t F.
+Variable F V: Type.
+Variable genv: Genv.t F V.
 
 Definition find_symbol_offset (id: ident) (ofs: int) : val :=
   match Genv.find_symbol genv id with
@@ -746,8 +735,8 @@ End EVAL_OP_TOTAL.
 
 Section EVAL_LESSDEF.
 
-Variable F: Type.
-Variable genv: Genv.t F.
+Variable F V: Type.
+Variable genv: Genv.t F V.
 
 Ltac InvLessdef :=
   match goal with
@@ -834,7 +823,7 @@ End EVAL_LESSDEF.
 Definition op_for_binary_addressing (addr: addressing) : operation := Oadd.
 
 Lemma eval_op_for_binary_addressing:
-  forall (F: Type) (ge: Genv.t F) sp addr args v,
+  forall (F V: Type) (ge: Genv.t F V) sp addr args v,
   (length args >= 2)%nat ->
   eval_addressing ge sp addr args = Some v ->
   eval_operation ge sp (op_for_binary_addressing addr) args = Some v.
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 10170f9..a1e5afe 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -288,7 +288,8 @@ let print_instruction oc labels = function
       fprintf oc "	extsb	%a, %a\n" ireg r1 ireg r2
   | Pextsh(r1, r2) ->
       fprintf oc "	extsh	%a, %a\n" ireg r1 ireg r2
-  | Pfreeframe ofs ->
+  | Pfreeframe(lo, hi, ofs) ->
+      (* Note: could also do an add on GPR1 using lo and hi *)
       fprintf oc "	lwz	%a, %ld(%a)\n" ireg GPR1  (camlint_of_coqint ofs)  ireg GPR1
   | Pfabs(r1, r2) ->
       fprintf oc "	fabs	%a, %a\n" freg r1 freg r2
diff --git a/powerpc/SelectOp.v b/powerpc/SelectOp.v
index 2f4d76e..d03645e 100644
--- a/powerpc/SelectOp.v
+++ b/powerpc/SelectOp.v
@@ -42,7 +42,7 @@ Require Import AST.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
-Require Import Mem.
+Require Import Memory.
 Require Import Globalenvs.
 Require Cminor.
 Require Import Op.
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index 2736e9e..d4a45da 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -18,7 +18,7 @@ Require Import AST.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
-Require Import Mem.
+Require Import Memory.
 Require Import Events.
 Require Import Globalenvs.
 Require Import Smallstep.
@@ -657,25 +657,18 @@ Qed.
 
 Lemma loadv_cast:
   forall chunk addr v,
-  loadv chunk m addr = Some v ->
+  Mem.loadv chunk m addr = Some v ->
   match chunk with
-  | Mint8signed => loadv chunk m addr = Some(Val.sign_ext 8 v)
-  | Mint8unsigned => loadv chunk m addr = Some(Val.zero_ext 8 v)
-  | Mint16signed => loadv chunk m addr = Some(Val.sign_ext 16 v)
-  | Mint16unsigned => loadv chunk m addr = Some(Val.zero_ext 16 v)
-  | Mfloat32 => loadv chunk m addr = Some(Val.singleoffloat v)
+  | Mint8signed => v = Val.sign_ext 8 v
+  | Mint8unsigned => v = Val.zero_ext 8 v
+  | Mint16signed => v = Val.sign_ext 16 v
+  | Mint16unsigned => v = Val.zero_ext 16 v
+  | Mfloat32 => v = Val.singleoffloat v
   | _ => True
   end.
 Proof.
-  intros. rewrite H. destruct addr; simpl in H; try discriminate.
-  exploit Mem.load_inv; eauto. 
-  set (v' := (getN (pred_size_chunk chunk) (Int.signed i) (contents (blocks m b)))).
-  intros [A B]. subst v. destruct chunk; auto; destruct v'; simpl; auto.
-  rewrite Int.sign_ext_idem; auto. compute; auto.
-  rewrite Int.zero_ext_idem; auto. compute; auto.
-  rewrite Int.sign_ext_idem; auto. compute; auto.
-  rewrite Int.zero_ext_idem; auto. compute; auto.
-  rewrite Float.singleoffloat_idem; auto.
+  intros. destruct addr; simpl in H; try discriminate.
+  eapply Mem.load_cast. eauto.
 Qed.
 
 Theorem eval_cast8signed:
@@ -686,7 +679,7 @@ Proof.
   intros until v; unfold cast8signed; case (cast8signed_match a); intros; InvEval.
   EvalOp. simpl. subst v. destruct v1; simpl; auto.
   rewrite Int.sign_ext_idem. reflexivity. compute; auto.
-  inv H. econstructor; eauto. apply (loadv_cast _ _ _ H7). 
+  inv H. econstructor; eauto. rewrite H7. decEq. apply (loadv_cast _ _ _ H7). 
   EvalOp.
 Qed.
 
@@ -698,7 +691,7 @@ Proof.
   intros until v; unfold cast8unsigned; case (cast8unsigned_match a); intros; InvEval.
   EvalOp. simpl. subst v. destruct v1; simpl; auto.
   rewrite Int.zero_ext_idem. reflexivity. compute; auto.
-  inv H. econstructor; eauto. apply (loadv_cast _ _ _ H7). 
+  inv H. econstructor; eauto. rewrite H7. decEq. apply (loadv_cast _ _ _ H7). 
   EvalOp.
 Qed.
 
@@ -710,7 +703,7 @@ Proof.
   intros until v; unfold cast16signed; case (cast16signed_match a); intros; InvEval.
   EvalOp. simpl. subst v. destruct v1; simpl; auto.
   rewrite Int.sign_ext_idem. reflexivity. compute; auto.
-  inv H. econstructor; eauto. apply (loadv_cast _ _ _ H7). 
+  inv H. econstructor; eauto. rewrite H7. decEq. apply (loadv_cast _ _ _ H7). 
   EvalOp.
 Qed.
 
@@ -722,7 +715,7 @@ Proof.
   intros until v; unfold cast16unsigned; case (cast16unsigned_match a); intros; InvEval.
   EvalOp. simpl. subst v. destruct v1; simpl; auto.
   rewrite Int.zero_ext_idem. reflexivity. compute; auto.
-  inv H. econstructor; eauto. apply (loadv_cast _ _ _ H7). 
+  inv H. econstructor; eauto. rewrite H7. decEq. apply (loadv_cast _ _ _ H7). 
   EvalOp.
 Qed.
 
@@ -733,7 +726,7 @@ Theorem eval_singleoffloat:
 Proof. 
   intros until v; unfold singleoffloat; case (singleoffloat_match a); intros; InvEval.
   EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Float.singleoffloat_idem. reflexivity.
-  inv H. econstructor; eauto. apply (loadv_cast _ _ _ H7). 
+  inv H. econstructor; eauto. rewrite H7. decEq. apply (loadv_cast _ _ _ H7). 
   EvalOp.
 Qed.