Renamed Machconcr into Machsem.

Removed Machabstr and Machabstr2concr, now useless following the reengineering 
  of Stacking.


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

18 files changed, 202 insertions, 1699 deletions

diff --git a/.depend b/.depend
index 941c6d7..9e70000 100644
--- a/.depend
+++ b/.depend
@@ -76,14 +76,14 @@ backend/Machtyping.vo backend/Machtyping.glob: backend/Machtyping.v lib/Coqlib.v
 backend/Bounds.vo backend/Bounds.glob: backend/Bounds.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo backend/Linear.vo backend/Lineartyping.vo backend/Conventions.vo
 $(ARCH)/$(VARIANT)/Stacklayout.vo $(ARCH)/$(VARIANT)/Stacklayout.glob: $(ARCH)/$(VARIANT)/Stacklayout.v lib/Coqlib.vo backend/Bounds.vo
 backend/Stacking.vo backend/Stacking.glob: backend/Stacking.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo backend/RTL.vo backend/Locations.vo backend/Linear.vo backend/Bounds.vo backend/Mach.vo backend/Conventions.vo $(ARCH)/$(VARIANT)/Stacklayout.vo
-backend/Stackingproof.vo backend/Stackingproof.glob: backend/Stackingproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo common/Values.vo $(ARCH)/Op.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Locations.vo backend/LTL.vo backend/Linear.vo backend/Lineartyping.vo backend/Mach.vo backend/Machconcr.vo backend/Bounds.vo backend/Conventions.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Stacking.vo
+backend/Stackingproof.vo backend/Stackingproof.glob: backend/Stackingproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo common/Values.vo $(ARCH)/Op.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Locations.vo backend/LTL.vo backend/Linear.vo backend/Lineartyping.vo backend/Mach.vo backend/Machsem.vo backend/Bounds.vo backend/Conventions.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Stacking.vo
 backend/Stackingtyping.vo backend/Stackingtyping.glob: backend/Stackingtyping.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo lib/Integers.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Linear.vo backend/Lineartyping.vo backend/Mach.vo backend/Machtyping.vo backend/Bounds.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Stacking.vo backend/Stackingproof.vo
-backend/Machconcr.vo backend/Machconcr.glob: backend/Machconcr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo $(ARCH)/$(VARIANT)/Stacklayout.vo $(ARCH)/Asmgenretaddr.vo
+backend/Machsem.vo backend/Machsem.glob: backend/Machsem.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo $(ARCH)/$(VARIANT)/Stacklayout.vo $(ARCH)/Asmgenretaddr.vo
 $(ARCH)/Asm.vo $(ARCH)/Asm.glob: $(ARCH)/Asm.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Conventions.vo
 $(ARCH)/Asmgen.vo $(ARCH)/Asmgen.glob: $(ARCH)/Asmgen.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo
 $(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenretaddr.glob: $(ARCH)/Asmgenretaddr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo
-$(ARCH)/Asmgenproof1.vo $(ARCH)/Asmgenproof1.glob: $(ARCH)/Asmgenproof1.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Machconcr.vo backend/Machtyping.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Conventions.vo
-$(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob: $(ARCH)/Asmgenproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Machconcr.vo backend/Machtyping.vo backend/Conventions.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo $(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenproof1.vo
+$(ARCH)/Asmgenproof1.vo $(ARCH)/Asmgenproof1.glob: $(ARCH)/Asmgenproof1.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Machsem.vo backend/Machtyping.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Conventions.vo
+$(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob: $(ARCH)/Asmgenproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Machsem.vo backend/Machtyping.vo backend/Conventions.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo $(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenproof1.vo
 cfrontend/Csyntax.vo cfrontend/Csyntax.glob: cfrontend/Csyntax.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo
 cfrontend/Csem.vo cfrontend/Csem.glob: cfrontend/Csem.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo cfrontend/Csyntax.vo common/Smallstep.vo
 cfrontend/Cstrategy.vo cfrontend/Cstrategy.glob: cfrontend/Cstrategy.v lib/Axioms.vo lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Determinism.vo cfrontend/Csyntax.vo cfrontend/Csem.vo
@@ -98,5 +98,5 @@ cfrontend/Cshmgenproof.vo cfrontend/Cshmgenproof.glob: cfrontend/Cshmgenproof.v
 cfrontend/Csharpminor.vo cfrontend/Csharpminor.glob: cfrontend/Csharpminor.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo backend/Cminor.vo common/Smallstep.vo
 cfrontend/Cminorgen.vo cfrontend/Cminorgen.glob: cfrontend/Cminorgen.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Ordered.vo common/AST.vo lib/Integers.vo common/Memdata.vo cfrontend/Csharpminor.vo backend/Cminor.vo
 cfrontend/Cminorgenproof.vo cfrontend/Cminorgenproof.glob: cfrontend/Cminorgenproof.v lib/Coqlib.vo lib/Intv.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Switch.vo cfrontend/Csharpminor.vo backend/Cminor.vo cfrontend/Cminorgen.vo
-driver/Compiler.vo driver/Compiler.glob: driver/Compiler.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo common/Values.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo cfrontend/Csharpminor.vo backend/Cminor.vo backend/CminorSel.vo backend/RTL.vo backend/LTL.vo backend/LTLin.vo backend/Linear.vo backend/Mach.vo $(ARCH)/Asm.vo cfrontend/Initializers.vo cfrontend/SimplExpr.vo cfrontend/Cshmgen.vo cfrontend/Cminorgen.vo backend/Selection.vo backend/RTLgen.vo backend/Tailcall.vo backend/CastOptim.vo backend/Constprop.vo backend/CSE.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/Reload.vo backend/Stacking.vo $(ARCH)/Asmgen.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/LTLintyping.vo backend/Lineartyping.vo backend/Machtyping.vo cfrontend/SimplExprproof.vo cfrontend/Cshmgenproof.vo cfrontend/Cminorgenproof.vo backend/Selectionproof.vo backend/RTLgenproof.vo backend/Tailcallproof.vo backend/CastOptimproof.vo backend/Constpropproof.vo backend/CSEproof.vo backend/Allocproof.vo backend/Alloctyping.vo backend/Tunnelingproof.vo backend/Tunnelingtyping.vo backend/Linearizeproof.vo backend/Linearizetyping.vo backend/Reloadproof.vo backend/Reloadtyping.vo backend/Stackingproof.vo backend/Stackingtyping.vo $(ARCH)/Asmgenproof.vo
+driver/Compiler.vo driver/Compiler.glob: driver/Compiler.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo common/Values.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo cfrontend/Csharpminor.vo backend/Cminor.vo backend/CminorSel.vo backend/RTL.vo backend/LTL.vo backend/LTLin.vo backend/Linear.vo backend/Mach.vo backend/Machsem.vo $(ARCH)/Asm.vo cfrontend/Initializers.vo cfrontend/SimplExpr.vo cfrontend/Cshmgen.vo cfrontend/Cminorgen.vo backend/Selection.vo backend/RTLgen.vo backend/Tailcall.vo backend/CastOptim.vo backend/Constprop.vo backend/CSE.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/Reload.vo backend/Stacking.vo $(ARCH)/Asmgen.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/LTLintyping.vo backend/Lineartyping.vo backend/Machtyping.vo cfrontend/SimplExprproof.vo cfrontend/Cshmgenproof.vo cfrontend/Cminorgenproof.vo backend/Selectionproof.vo backend/RTLgenproof.vo backend/Tailcallproof.vo backend/CastOptimproof.vo backend/Constpropproof.vo backend/CSEproof.vo backend/Allocproof.vo backend/Alloctyping.vo backend/Tunnelingproof.vo backend/Tunnelingtyping.vo backend/Linearizeproof.vo backend/Linearizetyping.vo backend/Reloadproof.vo backend/Reloadtyping.vo backend/Stackingproof.vo backend/Stackingtyping.vo $(ARCH)/Asmgenproof.vo
 driver/Complements.vo driver/Complements.glob: driver/Complements.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Determinism.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo $(ARCH)/Asm.vo driver/Compiler.vo common/Errors.vo
diff --git a/Makefile b/Makefile
index d995d1d..adfca2c 100644
--- a/Makefile
+++ b/Makefile
@@ -64,7 +64,7 @@ BACKEND=\
   Parallelmove.v Reload.v Reloadproof.v Reloadtyping.v \
   Mach.v Machtyping.v \
   Bounds.v Stacklayout.v Stacking.v Stackingproof.v Stackingtyping.v \
-  Machconcr.v \
+  Machsem.v \
   Asm.v Asmgen.v Asmgenretaddr.v Asmgenproof1.v Asmgenproof.v
 
 # C front-end modules (in cfrontend/)
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index 0a429cc..b7a7ff0 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -27,7 +27,7 @@ Require Import Op.
 Require Import Locations.
 Require Import Conventions.
 Require Import Mach.
-Require Import Machconcr.
+Require Import Machsem.
 Require Import Machtyping.
 Require Import Asm.
 Require Import Asmgen.
@@ -562,7 +562,7 @@ Qed.
 - Mach register values and ARM register values agree.
 *)
 
-Inductive match_stack: list Machconcr.stackframe -> Prop :=
+Inductive match_stack: list Machsem.stackframe -> Prop :=
   | match_stack_nil:
       match_stack nil
   | match_stack_cons: forall fb sp ra c s f,
@@ -575,7 +575,7 @@ Inductive match_stack: list Machconcr.stackframe -> Prop :=
       match_stack s ->
       match_stack (Stackframe fb sp ra c :: s).
 
-Inductive match_states: Machconcr.state -> Asm.state -> Prop :=
+Inductive match_states: Machsem.state -> Asm.state -> Prop :=
   | match_states_intro:
       forall s fb sp c ms m rs f m'
         (STACKS: match_stack s)
@@ -585,7 +585,7 @@ Inductive match_states: Machconcr.state -> Asm.state -> Prop :=
         (AT: transl_code_at_pc (rs PC) fb f c)
         (AG: agree ms sp rs)
         (MEXT: Mem.extends m m'),
-      match_states (Machconcr.State s fb sp c ms m)
+      match_states (Machsem.State s fb sp c ms m)
                    (Asm.State rs m')
   | match_states_call:
       forall s fb ms m rs m'
@@ -594,7 +594,7 @@ Inductive match_states: Machconcr.state -> Asm.state -> Prop :=
         (ATPC: rs PC = Vptr fb Int.zero)
         (ATLR: rs IR14 = parent_ra s)
         (MEXT: Mem.extends m m'),
-      match_states (Machconcr.Callstate s fb ms m)
+      match_states (Machsem.Callstate s fb ms m)
                    (Asm.State rs m')
   | match_states_return:
       forall s ms m rs m'
@@ -602,7 +602,7 @@ Inductive match_states: Machconcr.state -> Asm.state -> Prop :=
         (AG: agree ms (parent_sp s) rs)
         (ATPC: rs PC = parent_ra s)
         (MEXT: Mem.extends m m'),
-      match_states (Machconcr.Returnstate s ms m)
+      match_states (Machsem.Returnstate s ms m)
                    (Asm.State rs m').
 
 Lemma exec_straight_steps:
@@ -620,7 +620,7 @@ Lemma exec_straight_steps:
      /\ agree ms2 sp rs2) ->
   exists st',
   plus step tge (State rs1 m1') E0 st' /\
-  match_states (Machconcr.State s fb sp c2 ms2 m2) st'.
+  match_states (Machsem.State s fb sp c2 ms2 m2) st'.
 Proof.
   intros. destruct H5 as [m2' [A [rs2 [B C]]]].
   exists (State rs2 m2'); split.
@@ -652,22 +652,22 @@ Qed.
   take infinitely many Mach transitions that correspond to zero
   transitions on the ARM side.  Actually, all Mach transitions
   correspond to at least one ARM transition, except the
-  transition from [Machconcr.Returnstate] to [Machconcr.State].
+  transition from [Machsem.Returnstate] to [Machsem.State].
   So, the following integer measure will suffice to rule out
   the unwanted behaviour. *)
 
-Definition measure (s: Machconcr.state) : nat :=
+Definition measure (s: Machsem.state) : nat :=
   match s with
-  | Machconcr.State _ _ _ _ _ _ => 0%nat
-  | Machconcr.Callstate _ _ _ _ => 0%nat
-  | Machconcr.Returnstate _ _ _ => 1%nat
+  | Machsem.State _ _ _ _ _ _ => 0%nat
+  | Machsem.Callstate _ _ _ _ => 0%nat
+  | Machsem.Returnstate _ _ _ => 1%nat
   end.
 
 (** We show the simulation diagram by case analysis on the Mach transition
   on the left.  Since the proof is large, we break it into one lemma
   per transition. *)
 
-Definition exec_instr_prop (s1: Machconcr.state) (t: trace) (s2: Machconcr.state) : Prop :=
+Definition exec_instr_prop (s1: Machsem.state) (t: trace) (s2: Machsem.state) : Prop :=
   forall s1' (MS: match_states s1 s1'),
   (exists s2', plus step tge s1' t s2' /\ match_states s2 s2')
   \/ (measure s2 < measure s1 /\ t = E0 /\ match_states s2 s1')%nat.
@@ -677,8 +677,8 @@ Lemma exec_Mlabel_prop:
   forall (s : list stackframe) (fb : block) (sp : val)
          (lbl : Mach.label) (c : list Mach.instruction) (ms : Mach.regset)
          (m : mem),
-  exec_instr_prop (Machconcr.State s fb sp (Mlabel lbl :: c) ms m) E0
-                  (Machconcr.State s fb sp c ms m).
+  exec_instr_prop (Machsem.State s fb sp (Mlabel lbl :: c) ms m) E0
+                  (Machsem.State s fb sp c ms m).
 Proof.
   intros; red; intros; inv MS.
   left; eapply exec_straight_steps; eauto with coqlib.
@@ -693,8 +693,8 @@ Lemma exec_Mgetstack_prop:
          (ty : typ) (dst : mreg) (c : list Mach.instruction)
          (ms : Mach.regset) (m : mem) (v : val),
   load_stack m sp ty ofs = Some v ->
-  exec_instr_prop (Machconcr.State s fb sp (Mgetstack ofs ty dst :: c) ms m) E0
-                  (Machconcr.State s fb sp c (Regmap.set dst v ms) m).
+  exec_instr_prop (Machsem.State s fb sp (Mgetstack ofs ty dst :: c) ms m) E0
+                  (Machsem.State s fb sp c (Regmap.set dst v ms) m).
 Proof.
   intros; red; intros; inv MS.
   unfold load_stack in H. 
@@ -715,8 +715,8 @@ Lemma exec_Msetstack_prop:
          (ofs : int) (ty : typ) (c : list Mach.instruction)
          (ms : mreg -> val) (m m' : mem),
   store_stack m sp ty ofs (ms src) = Some m' ->
-  exec_instr_prop (Machconcr.State s fb sp (Msetstack src ofs ty :: c) ms m) E0
-                  (Machconcr.State s fb sp c ms m').
+  exec_instr_prop (Machsem.State s fb sp (Msetstack src ofs ty :: c) ms m) E0
+                  (Machsem.State s fb sp c ms m').
 Proof.
   intros; red; intros; inv MS.
   unfold store_stack in H. 
@@ -740,8 +740,8 @@ Lemma exec_Mgetparam_prop:
   Genv.find_funct_ptr ge fb = Some (Internal f) ->
   load_stack m sp Tint f.(fn_link_ofs) = Some (parent_sp s) ->
   load_stack m (parent_sp s) ty ofs = Some v ->
-  exec_instr_prop (Machconcr.State s fb sp (Mgetparam ofs ty dst :: c) ms m) E0
-                  (Machconcr.State s fb sp c (Regmap.set dst v (Regmap.set IT1 Vundef ms)) m).
+  exec_instr_prop (Machsem.State s fb sp (Mgetparam ofs ty dst :: c) ms m) E0
+                  (Machsem.State s fb sp c (Regmap.set dst v (Regmap.set IT1 Vundef ms)) m).
 Proof.
   intros; red; intros; inv MS.
   assert (f0 = f) by congruence. subst f0.
@@ -775,8 +775,8 @@ Lemma exec_Mop_prop:
          (args : list mreg) (res : mreg) (c : list Mach.instruction)
          (ms : mreg -> val) (m : mem) (v : val),
   eval_operation ge sp op ms ## args m = Some v ->
-  exec_instr_prop (Machconcr.State s fb sp (Mop op args res :: c) ms m) E0
-                  (Machconcr.State s fb sp c (Regmap.set res v (undef_op op ms)) m).
+  exec_instr_prop (Machsem.State s fb sp (Mop op args res :: c) ms m) E0
+                  (Machsem.State s fb sp c (Regmap.set res v (undef_op op ms)) m).
 Proof.
   intros; red; intros; inv MS.
   generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
@@ -806,8 +806,8 @@ Lemma exec_Mload_prop:
          (m : mem) (a v : val),
   eval_addressing ge sp addr ms ## args = Some a ->
   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 (undef_temps ms)) m).
+  exec_instr_prop (Machsem.State s fb sp (Mload chunk addr args dst :: c) ms m)
+               E0 (Machsem.State s fb sp c (Regmap.set dst v (undef_temps ms)) m).
 Proof.
   intros; red; intros; inv MS.
   generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
@@ -831,8 +831,8 @@ Lemma exec_Mstore_prop:
          (m m' : mem) (a : val),
   eval_addressing ge sp addr ms ## args = Some a ->
   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 (undef_temps ms) m').
+  exec_instr_prop (Machsem.State s fb sp (Mstore chunk addr args src :: c) ms m) E0
+                  (Machsem.State s fb sp c (undef_temps ms) m').
 Proof.
   intros; red; intros; inv MS.
   generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
@@ -857,7 +857,7 @@ Lemma exec_Mcall_prop:
   find_function_ptr ge ros ms = Some f' ->
   Genv.find_funct_ptr ge fb = Some (Internal f) ->
   return_address_offset f c ra ->
-  exec_instr_prop (Machconcr.State s fb sp (Mcall sig ros :: c) ms m) E0
+  exec_instr_prop (Machsem.State s fb sp (Mcall sig ros :: c) ms m) E0
                   (Callstate (Stackframe fb sp (Vptr fb ra) c :: s) f' ms m).
 Proof.
   intros; red; intros; inv MS.
@@ -919,7 +919,7 @@ Lemma exec_Mtailcall_prop:
   load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
   Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
   exec_instr_prop
-          (Machconcr.State s fb (Vptr stk soff) (Mtailcall sig ros :: c) ms m) E0
+          (Machsem.State s fb (Vptr stk soff) (Mtailcall sig ros :: c) ms m) E0
           (Callstate s f' ms m').
 Proof.
   intros; red; intros; inv MS.
@@ -990,8 +990,8 @@ Lemma exec_Mbuiltin_prop:
          (args : list mreg) (res : mreg) (b : list Mach.instruction)
          (t : trace) (v : val) (m' : mem),
   external_call ef ge ms ## args m t v m' ->
-  exec_instr_prop (Machconcr.State s f sp (Mbuiltin ef args res :: b) ms m) t
-                  (Machconcr.State s f sp b (Regmap.set res v (undef_temps ms)) m').
+  exec_instr_prop (Machsem.State s f sp (Mbuiltin ef args res :: b) ms m) t
+                  (Machsem.State s f sp b (Regmap.set res v (undef_temps ms)) m').
 Proof.
   intros; red; intros; inv MS.
   generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
@@ -1022,8 +1022,8 @@ Lemma exec_Mgoto_prop:
          (m : mem) (c' : Mach.code),
   Genv.find_funct_ptr ge fb = Some (Internal f) ->
   Mach.find_label lbl (fn_code f) = Some c' ->
-  exec_instr_prop (Machconcr.State s fb sp (Mgoto lbl :: c) ms m) E0
-                  (Machconcr.State s fb sp c' ms m).
+  exec_instr_prop (Machsem.State s fb sp (Mgoto lbl :: c) ms m) E0
+                  (Machsem.State s fb sp c' ms m).
 Proof.
   intros; red; intros; inv MS.
   assert (f0 = f) by congruence. subst f0.
@@ -1048,8 +1048,8 @@ Lemma exec_Mcond_true_prop:
   eval_condition cond ms ## args m = Some true ->
   Genv.find_funct_ptr ge fb = Some (Internal f) ->
   Mach.find_label lbl (fn_code f) = Some c' ->
-  exec_instr_prop (Machconcr.State s fb sp (Mcond cond args lbl :: c) ms m) E0
-                  (Machconcr.State s fb sp c' (undef_temps ms) m).
+  exec_instr_prop (Machsem.State s fb sp (Mcond cond args lbl :: c) ms m) E0
+                  (Machsem.State s fb sp c' (undef_temps ms) m).
 Proof.
   intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0.
   generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
@@ -1083,8 +1083,8 @@ Lemma exec_Mcond_false_prop:
          (cond : condition) (args : list mreg) (lbl : Mach.label)
          (c : list Mach.instruction) (ms : mreg -> val) (m : mem),
   eval_condition cond ms ## args m = Some false ->
-  exec_instr_prop (Machconcr.State s fb sp (Mcond cond args lbl :: c) ms m) E0
-                  (Machconcr.State s fb sp c (undef_temps ms) m).
+  exec_instr_prop (Machsem.State s fb sp (Mcond cond args lbl :: c) ms m) E0
+                  (Machsem.State s fb sp c (undef_temps ms) m).
 Proof.
   intros; red; intros; inv MS.
   generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
@@ -1111,8 +1111,8 @@ Lemma exec_Mjumptable_prop:
   Genv.find_funct_ptr ge fb = Some (Internal f) ->
   Mach.find_label lbl (fn_code f) = Some c' ->
   exec_instr_prop
-    (Machconcr.State s fb sp (Mjumptable arg tbl :: c) ms m) E0
-    (Machconcr.State s fb sp c' (undef_temps ms) m).
+    (Machsem.State s fb sp (Mjumptable arg tbl :: c) ms m) E0
+    (Machsem.State s fb sp c' (undef_temps ms) m).
 Proof.
   intros; red; intros; inv MS.
   assert (f0 = f) by congruence. subst f0.
@@ -1164,7 +1164,7 @@ Lemma exec_Mreturn_prop:
   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 0 f.(fn_stacksize) = Some m' ->
-  exec_instr_prop (Machconcr.State s fb (Vptr stk soff) (Mreturn :: c) ms m) E0
+  exec_instr_prop (Machsem.State s fb (Vptr stk soff) (Mreturn :: c) ms m) E0
                   (Returnstate s ms m').
 Proof.
   intros; red; intros; inv MS.
@@ -1225,8 +1225,8 @@ Lemma exec_function_internal_prop:
   let sp := Vptr stk Int.zero 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 ->
-  exec_instr_prop (Machconcr.Callstate s fb ms m) E0
-                  (Machconcr.State s fb sp (fn_code f) (undef_temps ms) m3).
+  exec_instr_prop (Machsem.Callstate s fb ms m) E0
+                  (Machsem.State s fb sp (fn_code f) (undef_temps ms) m3).
 Proof.
   intros; red; intros; inv MS.
   assert (WTF: wt_function f).
@@ -1285,10 +1285,10 @@ Lemma exec_function_external_prop:
          (ef : external_function) (args : list val) (res : val) (m': mem),
   Genv.find_funct_ptr ge fb = Some (External ef) ->
   external_call ef ge args m t0 res m' ->
-  Machconcr.extcall_arguments ms m (parent_sp s) (ef_sig ef) args ->
+  Machsem.extcall_arguments ms m (parent_sp s) (ef_sig ef) args ->
   ms' = Regmap.set (loc_result (ef_sig ef)) res ms ->
-  exec_instr_prop (Machconcr.Callstate s fb ms m)
-               t0 (Machconcr.Returnstate s ms' m').
+  exec_instr_prop (Machsem.Callstate s fb ms m)
+               t0 (Machsem.Returnstate s ms' m').
 Proof.
   intros; red; intros; inv MS.
   exploit functions_translated; eauto.
@@ -1312,8 +1312,8 @@ Qed.
 Lemma exec_return_prop:
   forall (s : list stackframe) (fb : block) (sp ra : val)
          (c : Mach.code) (ms : Mach.regset) (m : mem),
-  exec_instr_prop (Machconcr.Returnstate (Stackframe fb sp ra c :: s) ms m) E0
-                  (Machconcr.State s fb sp c ms m).
+  exec_instr_prop (Machsem.Returnstate (Stackframe fb sp ra c :: s) ms m) E0
+                  (Machsem.State s fb sp c ms m).
 Proof.
   intros; red; intros; inv MS. inv STACKS. simpl in *.
   right. split. omega. split. auto. 
@@ -1321,10 +1321,10 @@ Proof.
 Qed.
 
 Theorem transf_instr_correct:
-  forall s1 t s2, Machconcr.step ge s1 t s2 ->
+  forall s1 t s2, Machsem.step ge s1 t s2 ->
   exec_instr_prop s1 t s2.
 Proof
-  (Machconcr.step_ind ge exec_instr_prop
+  (Machsem.step_ind ge exec_instr_prop
            exec_Mlabel_prop
            exec_Mgetstack_prop
            exec_Msetstack_prop
@@ -1345,7 +1345,7 @@ Proof
            exec_return_prop).
 
 Lemma transf_initial_states:
-  forall st1, Machconcr.initial_state prog st1 ->
+  forall st1, Machsem.initial_state prog st1 ->
   exists st2, Asm.initial_state tprog st2 /\ match_states st1 st2.
 Proof.
   intros. inversion H. unfold ge0 in *.
@@ -1365,7 +1365,7 @@ Qed.
 
 Lemma transf_final_states:
   forall st1 st2 r, 
-  match_states st1 st2 -> Machconcr.final_state st1 r -> Asm.final_state st2 r.
+  match_states st1 st2 -> Machsem.final_state st1 r -> Asm.final_state st2 r.
 Proof.
   intros. inv H0. inv H. constructor. auto.
   compute in H1. exploit ireg_val; eauto. instantiate (1 := R0); auto. 
@@ -1374,9 +1374,9 @@ Qed.
 
 Theorem transf_program_correct:
   forall (beh: program_behavior), not_wrong beh ->
-  Machconcr.exec_program prog beh -> Asm.exec_program tprog beh.
+  Machsem.exec_program prog beh -> Asm.exec_program tprog beh.
 Proof.
-  unfold Machconcr.exec_program, Asm.exec_program; intros.
+  unfold Machsem.exec_program, Asm.exec_program; intros.
   eapply simulation_star_preservation with (measure := measure); eauto.
   eexact transf_initial_states.
   eexact transf_final_states.
diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index fb49cb7..9312f30 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -23,7 +23,7 @@ Require Import Globalenvs.
 Require Import Op.
 Require Import Locations.
 Require Import Mach.
-Require Import Machconcr.
+Require Import Machsem.
 Require Import Machtyping.
 Require Import Asm.
 Require Import Asmgen.
@@ -322,7 +322,7 @@ Qed.
 Lemma extcall_arg_match:
   forall ms sp rs m m' l v,
   agree ms sp rs ->
-  Machconcr.extcall_arg ms m sp l v ->
+  Machsem.extcall_arg ms m sp l v ->
   Mem.extends m m' ->
   exists v', Asm.extcall_arg rs m' l v' /\ Val.lessdef v v'.
 Proof.
@@ -337,7 +337,7 @@ Qed.
 Lemma extcall_args_match:
   forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' ->
   forall ll vl,
-  Machconcr.extcall_args ms m sp ll vl ->
+  Machsem.extcall_args ms m sp ll vl ->
   exists vl', Asm.extcall_args rs m' ll vl' /\ Val.lessdef_list vl vl'.
 Proof.
   induction 3.
@@ -350,11 +350,11 @@ Qed.
 Lemma extcall_arguments_match:
   forall ms m sp rs sg args m',
   agree ms sp rs ->
-  Machconcr.extcall_arguments ms m sp sg args ->
+  Machsem.extcall_arguments ms m sp sg args ->
   Mem.extends m m' ->
   exists args', Asm.extcall_arguments rs m' sg args' /\ Val.lessdef_list args args'.
 Proof.
-  unfold Machconcr.extcall_arguments, Asm.extcall_arguments; intros.
+  unfold Machsem.extcall_arguments, Asm.extcall_arguments; intros.
   eapply extcall_args_match; eauto.
 Qed.
 
diff --git a/arm/Asmgenretaddr.v b/arm/Asmgenretaddr.v
index 97250a6..5238d21 100644
--- a/arm/Asmgenretaddr.v
+++ b/arm/Asmgenretaddr.v
@@ -13,7 +13,7 @@
 (** Predictor for return addresses in generated PPC code.
 
     The [return_address_offset] predicate defined here is used in the
-    concrete semantics for Mach (module [Machconcr]) to determine the
+    semantics for Mach (module [Machsem]) to determine the
     return addresses that are stored in activation records. *)
 
 Require Import Coqlib.
diff --git a/backend/Machabstr.v b/backend/Machabstr.v
deleted file mode 100644
index 23ca895..0000000
--- a/backend/Machabstr.v
+++ /dev/null
@@ -1,337 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(** The Mach intermediate language: abstract semantics. *)
-
-Require Import Coqlib.
-Require Import Maps.
-Require Import AST.
-Require Import Memory.
-Require Import Integers.
-Require Import Values.
-Require Import Memory.
-Require Import Events.
-Require Import Globalenvs.
-Require Import Smallstep.
-Require Import Op.
-Require Import Locations.
-Require Import Conventions.
-Require Import Mach.
-Require Stacklayout.
-
-(** This file defines the "abstract" semantics for the Mach
-  intermediate language, as opposed to the more concrete
-  semantics given in module [Machconcr].
-
-  The only difference with the concrete semantics is the interpretation
-  of the stack access instructions [Mgetstack], [Msetstack] and [Mgetparam].
-  In the concrete semantics, these are interpreted as memory accesses
-  relative to the stack pointer.  In the abstract semantics, these 
-  instructions are interpreted as accesses in a frame environment,
-  not resident in memory.  The frame environment is an additional
-  component of the state.
-
-  Not having the frame data in memory facilitates the proof of
-  the [Stacking] pass, which shows that the generated code executes
-  correctly with the abstract semantics.
-*)
-
-(** * Structure of abstract stack frames *)
-
-(** An abstract stack frame is a mapping from (type, offset) pairs to
-    values.  Like location sets (see module [Locations]), overlap
-    can occur. *)
-
-Definition frame : Type := typ -> Z -> val.
-
-Definition typ_eq: forall (ty1 ty2: typ), {ty1=ty2} + {ty1<>ty2}.
-Proof. decide equality. Defined.
-
-Definition update (ty: typ) (ofs: Z) (v: val) (f: frame) : frame :=
-  fun ty' ofs' => 
-    if zeq ofs ofs' then
-      if typ_eq ty ty' then v else Vundef
-    else
-      if zle (ofs' + AST.typesize ty') ofs then f ty' ofs'
-      else if zle (ofs + AST.typesize ty) ofs' then f ty' ofs'
-      else Vundef.
-
-Lemma update_same:
-  forall ty ofs v fr,
-  update ty ofs v fr ty ofs = v.
-Proof.
-  unfold update; intros. 
-  rewrite zeq_true. rewrite dec_eq_true. auto.
-Qed. 
-
-Lemma update_other:
-  forall ty ofs v fr ty' ofs',
-  ofs + AST.typesize ty <= ofs' \/ ofs' + AST.typesize ty' <= ofs ->
-  update ty ofs v fr ty' ofs' = fr ty' ofs'.
-Proof.
-  unfold update; intros.
-  generalize (AST.typesize_pos ty). 
-  generalize (AST.typesize_pos ty'). intros.
-  rewrite zeq_false.
-  destruct H. rewrite zle_false. apply zle_true. auto. omega.
-  apply zle_true. auto. 
-  omega.
-Qed.
-
-Definition empty_frame : frame := fun ty ofs => Vundef.
-
-Section FRAME_ACCESSES.
-
-Variable f: function.
-
-(** A slot [(ty, ofs)] within a frame is valid in function [f] if it lies
-  within the bounds of [f]'s frame, it does not overlap with
-  the slots reserved for the return address and the back link,
-  and it is aligned on a 4-byte boundary. *)
-
-Inductive slot_valid: typ -> Z -> Prop :=
-  slot_valid_intro:
-    forall ty ofs,
-    0 <= ofs ->
-    ofs + AST.typesize ty <= f.(fn_framesize) ->
-    (ofs + AST.typesize ty <= Int.signed f.(fn_link_ofs)
-       \/ Int.signed f.(fn_link_ofs) + 4 <= ofs) ->
-    (ofs + AST.typesize ty <= Int.signed f.(fn_retaddr_ofs)
-       \/ Int.signed f.(fn_retaddr_ofs) + 4 <= ofs) ->
-    (4 | ofs) ->
-    slot_valid ty ofs.
-
-(** [get_slot f fr ty ofs v] holds if the frame [fr] contains value [v]
-  with type [ty] at word offset [ofs]. *)
-
-Inductive get_slot: frame -> typ -> Z -> val -> Prop :=
-  | get_slot_intro:
-      forall fr ty ofs v,
-      slot_valid ty ofs ->
-      v = fr ty (ofs - f.(fn_framesize)) ->
-      get_slot fr ty ofs v.
-
-(** [set_slot f fr ty ofs v fr'] holds if frame [fr'] is obtained from
-  frame [fr] by storing value [v] with type [ty] at word offset [ofs]. *)
-
-Inductive set_slot: frame -> typ -> Z -> val -> frame -> Prop :=
-  | set_slot_intro:
-      forall fr ty ofs v fr',
-      slot_valid ty ofs ->
-      fr' = update ty (ofs - f.(fn_framesize)) v fr ->
-      set_slot fr ty ofs v fr'.
-
-(** Extract the values of the arguments of an external call. *)
-
-Inductive extcall_arg: regset -> frame -> loc -> val -> Prop :=
-  | extcall_arg_reg: forall rs fr r,
-      extcall_arg rs fr (R r) (rs r)
-  | extcall_arg_stack: forall rs fr ofs ty v,
-      get_slot fr ty (Int.signed (Int.repr (Stacklayout.fe_ofs_arg + 4 * ofs))) v ->
-      extcall_arg rs fr (S (Outgoing ofs ty)) v.
-
-Inductive extcall_args: regset -> frame -> list loc -> list val -> Prop :=
-  | extcall_args_nil: forall rs fr,
-      extcall_args rs fr nil nil
-  | extcall_args_cons: forall rs fr l1 ll v1 vl,
-      extcall_arg rs fr l1 v1 -> extcall_args rs fr ll vl ->
-      extcall_args rs fr (l1 :: ll) (v1 :: vl).
-
-Definition extcall_arguments
-   (rs: regset) (fr: frame) (sg: signature) (args: list val) : Prop :=
-  extcall_args rs fr (loc_arguments sg) args.
-    
-End FRAME_ACCESSES.
-
-(** Mach execution states. *)
-
-Inductive stackframe: Type :=
-  | Stackframe:
-      forall (f: function)      (**r calling function *)
-             (sp: val)          (**r stack pointer in calling function *)
-             (c: code)          (**r program point in calling function *)
-             (fr: frame),       (**r frame state in calling function *)
-      stackframe.
-
-Inductive state: Type :=
-  | State:
-      forall (stack: list stackframe) (**r call stack *)
-             (f: function)            (**r function currently executing *)
-             (sp: val)                (**r stack pointer *)
-             (c: code)                (**r current program point *)
-             (rs: regset)             (**r register state *)
-             (fr: frame)              (**r frame state *)
-             (m: mem),                (**r memory state *)
-      state
-  | Callstate:
-      forall (stack: list stackframe) (**r call stack *)
-             (f: fundef)              (**r function to call *)
-             (rs: regset)             (**r register state *)
-             (m: mem),                (**r memory state *)
-      state
-  | Returnstate:
-      forall (stack: list stackframe) (**r call stack *)
-             (rs: regset)             (**r register state *)
-             (m: mem),                (**r memory state *)
-      state.
-
-(** [parent_frame s] returns the frame of the calling function.
-  It is used to access function parameters that are passed on the stack
-  (the [Mgetparent] instruction).
-  [parent_function s] returns the calling function itself.
-  Suitable defaults are used if there are no calling function. *)
-
-Definition parent_frame (s: list stackframe) : frame :=
-  match s with
-  | nil => empty_frame
-  | Stackframe f sp c fr :: s => fr
-  end.
-
-Definition empty_function := 
-  mkfunction (mksignature nil None) nil 0 0 Int.zero Int.zero.
-
-Definition parent_function (s: list stackframe) : function :=
-  match s with
-  | nil => empty_function
-  | Stackframe f sp c fr :: s => f
-  end.
-
-Section RELSEM.
-
-Variable ge: genv.
-
-Definition find_function (ros: mreg + ident) (rs: regset) : option fundef :=
-  match ros with
-  | inl r => Genv.find_funct ge (rs r)
-  | inr symb =>
-      match Genv.find_symbol ge symb with
-      | None => None
-      | Some b => Genv.find_funct_ptr ge b
-      end
-  end.
-
-Inductive step: state -> trace -> state -> Prop :=
-  | exec_Mlabel:
-      forall s f sp lbl c rs fr m,
-      step (State s f sp (Mlabel lbl :: c) rs fr m)
-        E0 (State s f sp c rs fr m)
-  | exec_Mgetstack:
-      forall s f sp ofs ty dst c rs fr m v,
-      get_slot f fr ty (Int.signed ofs) v ->
-      step (State s f sp (Mgetstack ofs ty dst :: c) rs fr m)
-        E0 (State s f sp c (rs#dst <- v) fr m)
-  | exec_Msetstack:
-     forall s f sp src ofs ty c rs fr m fr',
-      set_slot f fr ty (Int.signed ofs) (rs src) fr' ->
-      step (State s f sp (Msetstack src ofs ty :: c) rs fr m)
-        E0 (State s f sp c rs fr' m)
-  | exec_Mgetparam:
-      forall s f sp ofs ty dst c rs fr m v,
-      get_slot (parent_function s) (parent_frame s) ty (Int.signed ofs) v ->
-      step (State s f sp (Mgetparam ofs ty dst :: c) rs fr m)
-        E0 (State s f sp c (rs # IT1 <- Vundef # dst <- v) fr m)
-  | exec_Mop:
-      forall s f sp op args res c rs fr m v,
-      eval_operation ge sp op rs##args = Some v ->
-      step (State s f sp (Mop op args res :: c) rs fr m)
-        E0 (State s f sp c ((undef_op op rs)#res <- v) fr m)
-  | exec_Mload:
-      forall s f sp chunk addr args dst c rs fr m a v,
-      eval_addressing ge sp addr rs##args = Some a ->
-      Mem.loadv chunk m a = Some v ->
-      step (State s f sp (Mload chunk addr args dst :: c) rs fr m)
-        E0 (State s f sp c ((undef_temps rs)#dst <- v) fr m)
-  | exec_Mstore:
-      forall s f sp chunk addr args src c rs fr m m' a,
-      eval_addressing ge sp addr rs##args = Some a ->
-      Mem.storev chunk m a (rs src) = Some m' ->
-      step (State s f sp (Mstore chunk addr args src :: c) rs fr m)
-        E0 (State s f sp c (undef_temps rs) fr m')
-  | exec_Mcall:
-      forall s f sp sig ros c rs fr m f',
-      find_function ros rs = Some f' ->
-      step (State s f sp (Mcall sig ros :: c) rs fr m)
-        E0 (Callstate (Stackframe f sp c fr :: s) f' rs m)
-  | exec_Mtailcall:
-      forall s f stk soff sig ros c rs fr m f' m',
-      find_function ros rs = Some f' ->
-      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
-      step (State s f (Vptr stk soff) (Mtailcall sig ros :: c) rs fr m)
-        E0 (Callstate s f' rs m')
-  | exec_Mbuiltin:
-      forall s f sp rs fr m ef args res b t v m',
-      external_call ef ge rs##args m t v m' ->
-      step (State s f sp (Mbuiltin ef args res :: b) rs fr m)
-         t (State s f sp b ((undef_temps rs)#res <- v) fr m')
-  | exec_Mgoto:
-      forall s f sp lbl c rs fr m c',
-      find_label lbl f.(fn_code) = Some c' ->
-      step (State s f sp (Mgoto lbl :: c) rs fr m)
-        E0 (State s f sp c' rs fr m)
-  | exec_Mcond_true:
-      forall s f sp cond args lbl c rs fr m c',
-      eval_condition cond rs##args = Some true ->
-      find_label lbl f.(fn_code) = Some c' ->
-      step (State s f sp (Mcond cond args lbl :: c) rs fr m)
-        E0 (State s f sp c' (undef_temps rs) fr m)
-  | exec_Mcond_false:
-      forall s f sp cond args lbl c rs fr m,
-      eval_condition cond rs##args = Some false ->
-      step (State s f sp (Mcond cond args lbl :: c) rs fr m)
-        E0 (State s f sp c (undef_temps rs) fr m)
-  | exec_Mjumptable:
-      forall s f sp arg tbl c rs fr m n lbl c',
-      rs arg = Vint n ->
-      list_nth_z tbl (Int.signed n) = Some lbl ->
-      find_label lbl f.(fn_code) = Some c' ->
-      step (State s f sp (Mjumptable arg tbl :: c) rs fr m)
-        E0 (State s f sp c' (undef_temps rs) fr m)
-  | exec_Mreturn:
-      forall s f stk soff c rs fr m m',
-      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
-      step (State s f (Vptr stk soff) (Mreturn :: c) rs fr m)
-        E0 (Returnstate s rs m')
-  | exec_function_internal:
-      forall s f rs m m' stk,
-      Mem.alloc m 0 f.(fn_stacksize) = (m', stk) ->
-      step (Callstate s (Internal f) rs m)
-        E0 (State s f (Vptr stk (Int.repr (-f.(fn_framesize))))
-                  f.(fn_code) rs empty_frame m')
-  | exec_function_external:
-      forall s ef args res rs1 rs2 m t m',
-      external_call ef ge args m t res m' ->
-      extcall_arguments (parent_function s) rs1 (parent_frame s) (ef_sig ef) args ->
-      rs2 = (rs1#(loc_result (ef_sig ef)) <- res) ->
-      step (Callstate s (External ef) rs1 m)
-         t (Returnstate s rs2 m')
-  | exec_return:
-      forall f sp c fr s rs m,
-      step (Returnstate (Stackframe f sp c fr :: s) rs m)
-        E0 (State s f sp c rs fr m).
-
-End RELSEM.
-
-Inductive initial_state (p: program): state -> Prop :=
-  | initial_state_intro: forall b f m0,
-      let ge := Genv.globalenv p in
-      Genv.init_mem p = Some m0 ->
-      Genv.find_symbol ge p.(prog_main) = Some b ->
-      Genv.find_funct_ptr ge b = Some f ->
-      initial_state p (Callstate nil f (Regmap.init Vundef) m0).
-
-Inductive final_state: state -> int -> Prop :=
-  | final_state_intro: forall rs m r,
-      rs (loc_result (mksignature nil (Some Tint))) = Vint r ->
-      final_state (Returnstate nil rs m) r.
-
-Definition exec_program (p: program) (beh: program_behavior) : Prop :=
-  program_behaves step (initial_state p) final_state (Genv.globalenv p) beh.
diff --git a/backend/Machabstr2concr.v b/backend/Machabstr2concr.v
deleted file mode 100644
index fa7f580..0000000
--- a/backend/Machabstr2concr.v
+++ /dev/null
@@ -1,1160 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(** Simulation between the two semantics for the Mach language. *)
-
-Require Import Axioms.
-Require Import Coqlib.
-Require Import Maps.
-Require Import AST.
-Require Import Integers.
-Require Import Values.
-Require Import Memory.
-Require Import Events.
-Require Import Globalenvs.
-Require Import Smallstep.
-Require Import Op.
-Require Import Locations.
-Require Import Mach.
-Require Import Machtyping.
-Require Import Machabstr.
-Require Import Machconcr.
-Require Import Conventions.
-Require Import Asmgenretaddr.
-
-(** Two semantics were defined for the Mach intermediate language:
-- The concrete semantics (file [Mach]), where the whole activation
-  record resides in memory and the [Mgetstack], [Msetstack] and
-  [Mgetparent] are interpreted as [sp]-relative memory accesses.
-- The abstract semantics (file [Machabstr]), where the activation
-  record is split in two parts: the Cminor stack data, resident in
-  memory, and the frame information, residing not in memory but
-  in additional evaluation environments.
-
-  In this file, we show a simulation result between these
-  semantics: if a program executes with some behaviour [beh] in the
-  abstract semantics, it also executes with the same behaviour in
-  the concrete semantics.  This result bridges the correctness proof
-  in file [Stackingproof] (which uses the abstract Mach semantics
-  as output) and that in file [Asmgenproof] (which uses the concrete
-  Mach semantics as input).
-*)
-
-Remark size_type_chunk:
-  forall ty, size_chunk (chunk_of_type ty) = AST.typesize ty.
-Proof.
-  destruct ty; reflexivity.
-Qed.
-
-(** * Agreement between frames and memory-resident activation records *)
-
-(** ** Agreement for one frame *)
-
-Section FRAME_MATCH.
-
-Variable f: function.
-Hypothesis wt_f: wt_function f.
-
-(** The core idea of the simulation proof is that for all active
-  functions, the memory-allocated activation record, in the concrete 
-  semantics, contains the same data as the Cminor stack block
-  (at positive offsets) and the frame of the function (at negative
-  offsets) in the abstract semantics
-
-  This intuition (activation record = Cminor stack data + frame)
-  is formalized by the following predicate [frame_match fr sp base mm ms].
-  [fr] is a frame and [mm] the current memory state in the abstract
-  semantics. [ms] is the current memory state in the concrete semantics.
-  The stack pointer is [Vptr sp base] in both semantics. *)
-
-Record frame_match (fr: frame)
-                   (sp: block) (base: int) 
-                   (mm ms: mem) : Prop :=
-  mk_frame_match {
-    fm_valid_1: 
-      Mem.valid_block mm sp;
-    fm_valid_2: 
-      Mem.valid_block ms sp;
-    fm_base:
-      base = Int.repr(- f.(fn_framesize));
-    fm_stackdata_pos: 
-      Mem.low_bound mm sp = 0;
-    fm_write_perm:
-      Mem.range_perm ms sp (-f.(fn_framesize)) 0 Freeable;
-    fm_contents_match:
-      forall ty ofs,
-      -f.(fn_framesize) <= ofs -> ofs + AST.typesize ty <= 0 -> (4 | ofs) ->
-      exists v,
-        Mem.load (chunk_of_type ty) ms sp ofs = Some v
-        /\ Val.lessdef (fr ty ofs) v
-  }.
-
-(** The following two innocuous-looking lemmas are the key results
-  showing that [sp]-relative memory accesses in the concrete
-  semantics behave like the direct frame accesses in the abstract
-  semantics.  First, a value [v] that has type [ty] is preserved
-  when stored in memory with chunk [chunk_of_type ty], then read
-  back with the same chunk.  The typing hypothesis is crucial here:
-  for instance, a float value is not preserved when stored
-  and loaded with chunk [Mint32]. *)
-
-Lemma load_result_ty:
-  forall v ty,
-  Val.has_type v ty -> Val.load_result (chunk_of_type ty) v = v.
-Proof.
-  destruct v; destruct ty; simpl; contradiction || reflexivity.
-Qed.
-
-(** Second, computations of [sp]-relative offsets using machine
-  arithmetic (as done in the concrete semantics) never overflows
-  and behaves identically to the offset computations using exact
-  arithmetic (as done in the abstract semantics). *)
-
-Lemma int_add_no_overflow:
-  forall x y,
-  Int.min_signed <= Int.signed x + Int.signed y <= Int.max_signed ->
-  Int.signed (Int.add x y) = Int.signed x + Int.signed y.
-Proof.
-  intros. rewrite Int.add_signed. rewrite Int.signed_repr. auto. auto.
-Qed.
-
-(** Given matching frames and activation records, loading from the
-  activation record (in the concrete semantics) behaves identically
-  to reading the corresponding slot from the frame
-  (in the abstract semantics).  *)
-
-Lemma frame_match_load_stack:
-  forall fr sp base mm ms ty ofs,
-  frame_match fr sp base mm ms ->
-  0 <= Int.signed ofs /\ Int.signed ofs + AST.typesize ty <= f.(fn_framesize) ->
-  (4 | Int.signed ofs) ->
-  exists v,
-     load_stack ms (Vptr sp base) ty ofs = Some v
-  /\ Val.lessdef (fr ty (Int.signed ofs - f.(fn_framesize))) v.
-Proof.
-  intros. inv H. inv wt_f.
-  unfold load_stack, Val.add, Mem.loadv.
-  replace (Int.signed (Int.add (Int.repr (- fn_framesize f)) ofs))
-     with (Int.signed ofs - fn_framesize f).
-  apply fm_contents_match0. omega. omega.
-  apply Zdivide_minus_l; auto. 
-  assert (Int.signed (Int.repr (-fn_framesize f)) = -fn_framesize f).
-    apply Int.signed_repr.
-    assert (0 <= Int.max_signed). compute; congruence. omega.
-  rewrite int_add_no_overflow. rewrite H. omega.
-  rewrite H. split. omega.
-  apply Zle_trans with 0. generalize (AST.typesize_pos ty). omega. 
-  compute; congruence.
-Qed.
-
-Lemma frame_match_get_slot:
-  forall fr sp base mm ms ty ofs v,
-  frame_match fr sp base mm ms ->
-  get_slot f fr ty (Int.signed ofs) v ->
-  exists v', load_stack ms (Vptr sp base) ty ofs = Some v' /\ Val.lessdef v v'.
-Proof.
-  intros. inv H0. inv H1. eapply frame_match_load_stack; eauto.
-Qed.
-
-(** Assigning a value to a frame slot (in the abstract semantics)
-  corresponds to storing this value in the activation record
-  (in the concrete semantics).  Moreover, agreement between frames
-  and activation records is preserved. *)
-
-Lemma frame_match_store_stack:
-  forall fr sp base mm ms ty ofs v v',
-  frame_match fr sp base mm ms ->
-  0 <= Int.signed ofs -> Int.signed ofs + AST.typesize ty <= f.(fn_framesize) ->
-  (4 | Int.signed ofs) ->
-  Val.has_type v ty ->
-  Val.lessdef v v' ->
-  Mem.extends mm ms ->
-  exists ms',
-    store_stack ms (Vptr sp base) ty ofs v' = Some ms' /\
-    frame_match (update ty (Int.signed ofs - f.(fn_framesize)) v fr) sp base mm ms' /\
-    Mem.extends mm ms'.
-Proof.
-  intros. inv H. inv wt_f.
-  unfold store_stack, Val.add, Mem.storev.
-  assert (Int.signed (Int.add (Int.repr (- fn_framesize f)) ofs) =
-          Int.signed ofs - fn_framesize f).
-  assert (Int.signed (Int.repr (-fn_framesize f)) = -fn_framesize f).
-    apply Int.signed_repr. 
-    assert (0 <= Int.max_signed). compute; congruence. omega.
-  rewrite int_add_no_overflow. rewrite H. omega.
-  rewrite H. split. omega.
-  apply Zle_trans with 0. generalize (AST.typesize_pos ty). omega. 
-  compute; congruence.
-  rewrite H.
-  assert ({ ms' | Mem.store (chunk_of_type ty) ms sp (Int.signed ofs - fn_framesize f) v' = Some ms'}).
-    apply Mem.valid_access_store. constructor.
-    apply Mem.range_perm_implies with Freeable; auto with mem.
-    red; intros; apply fm_write_perm0.
-    rewrite <- size_type_chunk in H1.
-    generalize (size_chunk_pos (chunk_of_type ty)).
-    omega.
-    replace (align_chunk (chunk_of_type ty)) with 4.
-    apply Zdivide_minus_l; auto.
-    destruct ty; auto.
-  destruct X as [ms' STORE].
-  exists ms'. 
-  split. exact STORE.
-  (* frame match *)
-  split. constructor.
-  (* valid *)
-  eauto with mem.
-  eauto with mem.
-  (* base *)
-  auto.
-  (* stackdata_pos *)
-  auto.
-  (* write_perm *)
-  red; intros; eauto with mem.
-  (* contents *)
-  intros. 
-  exploit fm_contents_match0; eauto. intros [v0 [LOAD0 VLD0]]. 
-  assert (exists v1, Mem.load (chunk_of_type ty0) ms' sp ofs0 = Some v1).
-    apply Mem.valid_access_load; eauto with mem. 
-  destruct H9 as [v1 LOAD1].
-  exists v1; split; auto.
-  unfold update. 
-  destruct (zeq (Int.signed ofs - fn_framesize f) ofs0). subst ofs0.
-    destruct (typ_eq ty ty0). subst ty0.
-    (* same *)
-    inv H4. 
-    assert (Some v1 = Some (Val.load_result (chunk_of_type ty) v')).
-      rewrite <- LOAD1. eapply Mem.load_store_same; eauto.
-      destruct ty; auto.
-    inv H4. rewrite load_result_ty; auto. 
-    auto.
-    (* mismatch *)
-    auto.
-    destruct (zle (ofs0 + AST.typesize ty0) (Int.signed ofs - fn_framesize f)).
-    (* disjoint *)
-    assert (Some v1 = Some v0).
-      rewrite <- LOAD0; rewrite <- LOAD1. 
-      eapply Mem.load_store_other; eauto.
-      right; left. rewrite size_type_chunk; auto.
-    inv H9. auto.
-    destruct (zle (Int.signed ofs - fn_framesize f + AST.typesize ty)).
-    assert (Some v1 = Some v0).
-      rewrite <- LOAD0; rewrite <- LOAD1. 
-      eapply Mem.load_store_other; eauto.
-      right; right. rewrite size_type_chunk; auto.
-    inv H9. auto.
-    (* overlap *)
-    auto.
-  (* extends *)
-  eapply Mem.store_outside_extends; eauto.
-  left. rewrite fm_stackdata_pos0. 
-  rewrite size_type_chunk. omega.
-Qed.
-
-Lemma frame_match_set_slot:
-  forall fr sp base mm ms ty ofs v fr' v',
-  frame_match fr sp base mm ms ->
-  set_slot f fr ty (Int.signed ofs) v fr' ->
-  Val.has_type v ty ->
-  Val.lessdef v v' ->
-  Mem.extends mm ms ->
-  exists ms',
-    store_stack ms (Vptr sp base) ty ofs v' = Some ms' /\
-    frame_match fr' sp base mm ms' /\
-    Mem.extends mm ms'.
-Proof.
-  intros. inv H0. inv H4. eapply frame_match_store_stack; eauto. 
-Qed.
-
-(** Agreement is preserved by stores within blocks other than the
-  one pointed to by [sp]. *)
-
-Lemma frame_match_store_other:
-  forall fr sp base mm ms chunk b ofs v ms',
-  frame_match fr sp base mm ms ->
-  Mem.store chunk ms b ofs v = Some ms' ->
-  sp <> b ->
-  frame_match fr sp base mm ms'.
-Proof.
-  intros. inv H. constructor; auto.
-  eauto with mem.
-  red; intros; eauto with mem. 
-  intros. exploit fm_contents_match0; eauto. intros [v0 [LOAD LD]].
-  exists v0; split; auto. rewrite <- LOAD. eapply Mem.load_store_other; eauto.
-Qed.
-
-(** Agreement is preserved by parallel stores in the Machabstr
-  and the Machconcr semantics. *)
-
-Lemma frame_match_store:
-  forall fr sp base mm ms chunk b ofs v mm' v' ms',
-  frame_match fr sp base mm ms ->
-  Mem.store chunk mm b ofs v = Some mm' ->
-  Mem.store chunk ms b ofs v' = Some ms' ->
-  frame_match fr sp base mm' ms'.
-Proof.
-  intros. inv H. constructor; auto.
-  eauto with mem.
-  eauto with mem.
-  rewrite (Mem.bounds_store _ _ _ _ _ _ H0). auto.
-  red; intros; eauto with mem.
-  intros. exploit fm_contents_match0; eauto. intros [v0 [LOAD LD]].
-  exists v0; split; auto. rewrite <- LOAD. eapply Mem.load_store_other; eauto.
-  destruct (zeq sp b); auto. subst b. right. 
-  rewrite size_type_chunk. 
-  assert (Mem.valid_access mm chunk sp ofs Nonempty) by eauto with mem.
-  exploit Mem.store_valid_access_3. eexact H0. intro. 
-  exploit Mem.valid_access_in_bounds. eauto. rewrite fm_stackdata_pos0. 
-  omega.
-Qed.
-
-(** Memory allocation of the Cminor stack data block (in the abstract
-  semantics) and of the whole activation record (in the concrete
-  semantics) return memory states that agree according to [frame_match].
-  Moreover, [frame_match] relations over already allocated blocks
-  remain true. *)
-
-Lemma frame_match_new:
-  forall mm ms mm' ms' sp,
-  Mem.alloc mm 0 f.(fn_stacksize) = (mm', sp) ->
-  Mem.alloc ms (- f.(fn_framesize)) f.(fn_stacksize) = (ms', sp) ->
-  frame_match empty_frame sp (Int.repr (-f.(fn_framesize))) mm' ms'.
-Proof.
-  intros. 
-  inv wt_f.
-  constructor; simpl; eauto with mem.
-  rewrite (Mem.bounds_alloc_same _ _ _ _ _ H). auto.
-  red; intros. eapply Mem.perm_alloc_2; eauto. omega.
-  intros. exists Vundef; split.
-  eapply Mem.load_alloc_same'; eauto. 
-  rewrite size_type_chunk. omega.
-  replace (align_chunk (chunk_of_type ty)) with 4; auto.
-  destruct ty; auto.
-  unfold empty_frame. auto.
-Qed.
-
-Lemma frame_match_alloc:
-  forall mm ms fr sp base lom him los his mm' ms' b,
-  frame_match fr sp base mm ms ->
-  Mem.alloc mm lom him = (mm', b) ->
-  Mem.alloc ms los his = (ms', b) ->
-  frame_match fr sp base mm' ms'.
-Proof.
-  intros. inversion H.
-  assert (sp <> b). 
-    apply Mem.valid_not_valid_diff with ms; eauto with mem.
-  constructor; auto.
-  eauto with mem.
-  eauto with mem.
-  rewrite (Mem.bounds_alloc_other _ _ _ _ _ H0); auto.
-  red; intros; eauto with mem.
-  intros. exploit fm_contents_match0; eauto. intros [v [LOAD LD]].
-  exists v; split; auto. eapply Mem.load_alloc_other; eauto. 
-Qed.
-
-(** [frame_match] relations are preserved by freeing a block
-  other than the one pointed to by [sp]. *)
-
-Lemma frame_match_free:
-  forall fr sp base mm ms b lom him los his mm' ms',
-  frame_match fr sp base mm ms ->
-  sp <> b ->
-  Mem.free mm b lom him = Some mm' ->
-  Mem.free ms b los his = Some ms' ->
-  frame_match fr sp base mm' ms'.
-Proof.
-  intros. inversion H. constructor; auto.
-  eauto with mem.
-  eauto with mem.
-  rewrite (Mem.bounds_free _ _ _ _ _ H1). auto.
-  red; intros; eauto with mem. 
-  intros. rewrite (Mem.load_free _ _ _ _ _ H2); auto.
-Qed.
-
-Lemma frame_match_delete:
-  forall fr sp base mm ms mm',
-  frame_match fr sp base mm ms ->
-  Mem.free mm sp 0 f.(fn_stacksize) = Some mm' ->
-  Mem.extends mm ms ->
-  exists ms',
-  Mem.free ms sp (-f.(fn_framesize)) f.(fn_stacksize) = Some ms'
-  /\ Mem.extends mm' ms'.
-Proof.
-  intros. inversion H.
-  assert (Mem.range_perm mm sp 0 (fn_stacksize f) Freeable).
-    eapply Mem.free_range_perm; eauto. 
-  assert ({ ms' | Mem.free ms sp (-f.(fn_framesize)) f.(fn_stacksize) = Some ms' }).
-  apply Mem.range_perm_free. 
-  red; intros. destruct (zlt ofs 0). 
-  apply fm_write_perm0. omega. 
-  eapply Mem.perm_extends; eauto. apply H2. omega.
-  destruct X as [ms' FREE]. exists ms'; split; auto.
-  eapply Mem.free_right_extends; eauto. 
-  eapply Mem.free_left_extends; eauto.
-  intros; red; intros.
-  exploit Mem.perm_in_bounds; eauto. 
-  rewrite (Mem.bounds_free _ _ _ _ _ H0). rewrite fm_stackdata_pos0; intro. 
-  exploit Mem.perm_free_2. eexact H0. instantiate (1 := ofs); omega. eauto. 
-  auto.
-Qed.
-
-(** [frame_match] is preserved by external calls. *)
-
-Lemma frame_match_external_call:
-  forall (ge: genv) fr sp base mm ms mm' ms' ef vargs vres t vargs' vres',
-  frame_match fr sp base mm ms ->
-  Mem.extends mm ms ->
-  external_call ef ge vargs mm t vres mm' ->
-  Mem.extends mm' ms' ->
-  external_call ef ge vargs' ms t vres' ms' ->
-  mem_unchanged_on (loc_out_of_bounds mm) ms ms' ->
-  frame_match fr sp base mm' ms'.
-Proof.
-  intros. destruct H4 as [A B]. inversion H. constructor.
-  eapply external_call_valid_block; eauto.
-  eapply external_call_valid_block; eauto.
-  auto.
-  rewrite (external_call_bounds _ _ _ _ _ _ H1); auto.
-  red; intros. apply A; auto. red. omega.
-  intros. exploit fm_contents_match0; eauto. intros [v [C D]].
-  exists v; split; auto.
-  apply B; auto. 
-  rewrite size_type_chunk; intros; red. omega.
-Qed.
-
-End FRAME_MATCH.
-
-(** ** Accounting for the return address and back link *)
-
-Section EXTEND_FRAME.
-
-Variable f: function.
-Hypothesis wt_f: wt_function f.
-Variable cs: list Machconcr.stackframe.
-
-Definition extend_frame (fr: frame) : frame :=
-  update Tint (Int.signed f.(fn_retaddr_ofs) - f.(fn_framesize)) (parent_ra cs)
-    (update Tint (Int.signed f.(fn_link_ofs) - f.(fn_framesize)) (parent_sp cs)
-      fr).
-
-Lemma get_slot_extends:
-  forall fr ty ofs v,
-  get_slot f fr ty ofs v ->
-  get_slot f (extend_frame fr) ty ofs v.
-Proof.
-  intros. inv H. constructor. auto.
-  inv H0. inv wt_f. generalize (AST.typesize_pos ty); intro.
-  unfold extend_frame. rewrite update_other. rewrite update_other. auto.
-  simpl; omega. simpl; omega.
-Qed.
-
-Lemma update_commut:
-  forall ty1 ofs1 v1 ty2 ofs2 v2 fr,
-  ofs1 + AST.typesize ty1 <= ofs2 \/
-  ofs2 + AST.typesize ty2 <= ofs1 ->
-  update ty1 ofs1 v1 (update ty2 ofs2 v2 fr) =
-  update ty2 ofs2 v2 (update ty1 ofs1 v1 fr).
-Proof.
-  intros. unfold frame.
-  apply extensionality. intro ty. apply extensionality. intro ofs.
-  generalize (AST.typesize_pos ty1).
-  generalize (AST.typesize_pos ty2).
-  generalize (AST.typesize_pos ty); intros.
-  unfold update.
-  set (sz1 := AST.typesize ty1) in *.
-  set (sz2 := AST.typesize ty2) in *.
-  set (sz := AST.typesize ty) in *.
-  destruct (zeq ofs1 ofs).
-  rewrite zeq_false. 
-  destruct (zle (ofs + sz) ofs2). auto.
-  destruct (zle (ofs2 + sz2) ofs). auto.
-  destruct (typ_eq ty1 ty); auto.
-  replace sz with sz1 in z. omegaContradiction. unfold sz1, sz; congruence.
-  omega.
-
-  destruct (zle (ofs + sz) ofs1).
-  auto.
-  destruct (zle (ofs1 + sz1) ofs).
-  auto.
-
-  destruct (zeq ofs2 ofs).
-  destruct (typ_eq ty2 ty); auto.
-  replace sz with sz2 in z. omegaContradiction. unfold sz2, sz; congruence.
-  destruct (zle (ofs + sz) ofs2); auto.
-  destruct (zle (ofs2 + sz2) ofs); auto.
-Qed.
-
-Lemma set_slot_extends:
-  forall fr ty ofs v fr',
-  set_slot f fr ty ofs v fr' ->
-  set_slot f (extend_frame fr) ty ofs v (extend_frame fr').
-Proof.
-  intros. inv H. constructor. auto.
-  inv H0. inv wt_f. generalize (AST.typesize_pos ty); intro.
-  unfold extend_frame. 
-  rewrite (update_commut ty). rewrite (update_commut ty). auto.
-  simpl. omega. 
-  simpl. omega.
-Qed.
-
-Definition is_pointer_or_int (v: val) : Prop :=
-  match v with
-  | Vint _ => True
-  | Vptr _ _ => True
-  | _ => False
-  end.
-
-Remark is_pointer_has_type:
-  forall v, is_pointer_or_int v -> Val.has_type v Tint.
-Proof.
-  intros; destruct v; elim H; exact I. 
-Qed.
-
-Lemma frame_match_load_stack_pointer:
-  forall fr sp base mm ms ty ofs,
-  frame_match f fr sp base mm ms ->
-  0 <= Int.signed ofs /\ Int.signed ofs + AST.typesize ty <= f.(fn_framesize) ->
-  (4 | Int.signed ofs) ->
-  is_pointer_or_int (fr ty (Int.signed ofs - f.(fn_framesize))) ->
-  load_stack ms (Vptr sp base) ty ofs = Some (fr ty (Int.signed ofs - f.(fn_framesize))).
-Proof.
-  intros. exploit frame_match_load_stack; eauto. 
-  intros [v [LOAD LD]]. 
-  inv LD. auto. rewrite <- H4 in H2. elim H2.
-Qed.
-
-Lemma frame_match_load_link:
-  forall fr sp base mm ms,
-  frame_match f (extend_frame fr) sp base mm ms ->
-  is_pointer_or_int (parent_sp cs) ->
-  load_stack ms (Vptr sp base) Tint f.(fn_link_ofs) = Some(parent_sp cs).
-Proof.
-  intros. inversion wt_f.
-  assert (parent_sp cs =
-    extend_frame fr Tint (Int.signed f.(fn_link_ofs) - f.(fn_framesize))).
-  unfold extend_frame. rewrite update_other. rewrite update_same. auto. 
-  simpl. omega.
-  rewrite H1; eapply frame_match_load_stack_pointer; eauto.
-  rewrite <- H1; auto.
-Qed.
-
-Lemma frame_match_load_retaddr:
-  forall fr sp base mm ms,
-  frame_match f (extend_frame fr) sp base mm ms ->
-  is_pointer_or_int (parent_ra cs) ->
-  load_stack ms (Vptr sp base) Tint f.(fn_retaddr_ofs) = Some(parent_ra cs).
-Proof.
-  intros. inversion wt_f.
-  assert (parent_ra cs =
-    extend_frame fr Tint (Int.signed f.(fn_retaddr_ofs) - f.(fn_framesize))).
-  unfold extend_frame. rewrite update_same. auto. 
-  rewrite H1; eapply frame_match_load_stack_pointer; eauto.
-  rewrite <- H1; auto.
-Qed.
-
-Lemma frame_match_function_entry:
-  forall mm ms mm' sp,
-  Mem.extends mm ms ->
-  Mem.alloc mm 0 f.(fn_stacksize) = (mm', sp) ->
-  is_pointer_or_int (parent_sp cs) ->
-  is_pointer_or_int (parent_ra cs) ->
-  let base := Int.repr (-f.(fn_framesize)) in
-  exists ms1, exists ms2, exists ms3,
-  Mem.alloc ms (- f.(fn_framesize)) f.(fn_stacksize) = (ms1, sp) /\
-  store_stack ms1 (Vptr sp base) Tint f.(fn_link_ofs) (parent_sp cs) = Some ms2 /\
-  store_stack ms2 (Vptr sp base) Tint f.(fn_retaddr_ofs) (parent_ra cs) = Some ms3 /\
-  frame_match f (extend_frame empty_frame) sp base mm' ms3 /\
-  Mem.extends mm' ms3.
-Proof.
-  intros. inversion wt_f.
-  exploit Mem.alloc_extends; eauto.
-  instantiate (1 := -f.(fn_framesize)). omega.
-  instantiate (1 := f.(fn_stacksize)). omega.
-  intros [ms1 [A EXT0]].
-  exploit frame_match_new; eauto. fold base. intros FM0.
-  exploit frame_match_store_stack. eauto. eexact FM0. 
-  instantiate (1 := fn_link_ofs f); omega.
-  instantiate (1 := Tint). simpl; omega.
-  auto. apply is_pointer_has_type. eexact H1. constructor. auto.
-  intros [ms2 [STORE1 [FM1 EXT1]]].
-  exploit frame_match_store_stack. eauto. eexact FM1. 
-  instantiate (1 := fn_retaddr_ofs f); omega.
-  instantiate (1 := Tint). simpl; omega.
-  auto. apply is_pointer_has_type. eexact H2. constructor. auto.
-  intros [ms3 [STORE2 [FM2 EXT2]]].
-  exists ms1; exists ms2; exists ms3; auto.
-Qed.
-
-End EXTEND_FRAME.
-
-(** ** The ``less defined than'' relation between register states. *)
-
-Definition regset_lessdef (rs1 rs2: regset) : Prop :=
-  forall r, Val.lessdef (rs1 r) (rs2 r).
-
-Lemma regset_lessdef_list:
-  forall rs1 rs2, regset_lessdef rs1 rs2 ->
-  forall rl, Val.lessdef_list (rs1##rl) (rs2##rl).
-Proof.
-  induction rl; simpl.
-  constructor.
-  constructor; auto.
-Qed.
-
-Lemma regset_lessdef_set:
-  forall rs1 rs2 r v1 v2,
-  regset_lessdef rs1 rs2 -> Val.lessdef v1 v2 ->
-  regset_lessdef (rs1#r <- v1) (rs2#r <- v2).
-Proof.
-  intros; red; intros. unfold Regmap.set.
-  destruct (RegEq.eq r0 r); auto. 
-Qed.
-
-Lemma regset_lessdef_undef_temps:
-  forall rs1 rs2,
-  regset_lessdef rs1 rs2 -> regset_lessdef (undef_temps rs1) (undef_temps rs2).
-Proof.
-  unfold undef_temps. 
-  generalize (int_temporaries ++ float_temporaries).
-  induction l; simpl; intros. auto. apply IHl. apply regset_lessdef_set; auto.
-Qed.
-
-Lemma regset_lessdef_undef_op:
-  forall op rs1 rs2,
-  regset_lessdef rs1 rs2 -> regset_lessdef (undef_op op rs1) (undef_op op rs2).
-Proof.
-  intros. set (D := regset_lessdef_undef_temps _ _ H). 
-  destruct op; simpl; auto.
-Qed.
-
-Lemma regset_lessdef_find_function_ptr:
-  forall ge ros rs1 rs2 fb,
-  find_function_ptr ge ros rs1 = Some fb ->
-  regset_lessdef rs1 rs2 ->
-  find_function_ptr ge ros rs2 = Some fb.
-Proof.
-  unfold find_function_ptr; intros; destruct ros; simpl in *.
-  generalize (H0 m); intro LD; inv LD. auto. rewrite <- H2 in H. congruence.
-  auto.
-Qed.
-
-(** ** Invariant for stacks *)
-
-Section SIMULATION.
-
-Variable p: program.
-Let ge := Genv.globalenv p.
-
-(** The [match_stacks] predicate relates a Machabstr call stack
-  with the corresponding Machconcr stack.  In addition to enforcing
-  the [frame_match] predicate for each stack frame, we also enforce:
-- Proper chaining of activation record on the Machconcr side.
-- Preservation of the return address stored at the bottom of the
-  activation record.
-- Separation between the memory blocks holding the activation records:
-  their addresses increase strictly from caller to callee.
-*)
-
-Definition stack_below (ts: list Machconcr.stackframe) (b: block) : Prop :=
-  match parent_sp ts with
-  | Vptr sp base' => sp < b
-  | _ => False
-  end.
-
-Inductive match_stacks: 
-      list Machabstr.stackframe -> list Machconcr.stackframe ->
-      mem -> mem -> Prop :=
-  | match_stacks_nil: forall mm ms,
-      match_stacks nil nil mm ms
-  | match_stacks_cons: forall fb sp base c fr s f ra ts mm ms,
-      Genv.find_funct_ptr ge fb = Some (Internal f) ->
-      wt_function f ->
-      frame_match f (extend_frame f ts fr) sp base mm ms ->
-      stack_below ts sp ->
-      is_pointer_or_int ra ->
-      match_stacks s ts mm ms ->
-      match_stacks (Machabstr.Stackframe f (Vptr sp base) c fr :: s)
-                   (Machconcr.Stackframe fb (Vptr sp base) ra c :: ts)
-                   mm ms.
-
-Lemma match_stacks_parent_sp_pointer:
-  forall s ts mm ms,
-  match_stacks s ts mm ms -> is_pointer_or_int (Machconcr.parent_sp ts).
-Proof.
-  induction 1; simpl; auto.
-Qed.
-
-Lemma match_stacks_parent_ra_pointer:
-  forall s ts mm ms,
-  match_stacks s ts mm ms -> is_pointer_or_int (Machconcr.parent_ra ts).
-Proof.
-  induction 1; simpl; auto.
-Qed.
-
-(** If [match_stacks] holds, a lookup in the parent frame in the
-  Machabstr semantics corresponds to two memory loads in the
-  Machconcr semantics, one to load the pointer to the parent's
-  activation record, the second to read within this record. *)
-
-Lemma match_stacks_get_parent:
-  forall s ts mm ms ty ofs v,
-  match_stacks s ts mm ms ->
-  get_slot (parent_function s) (parent_frame s) ty (Int.signed ofs) v ->
-  exists v',
-     load_stack ms (Machconcr.parent_sp ts) ty ofs = Some v'
-  /\ Val.lessdef v v'.
-Proof.
-  intros. inv H; simpl in H0. 
-  inv H0. inv H. simpl in H1. elimtype False. generalize (AST.typesize_pos ty). omega.
-  simpl. eapply frame_match_get_slot; eauto.
-  eapply get_slot_extends; eauto. 
-Qed.
-
-(** Preservation of the [match_stacks] invariant
-    by various kinds of memory operations. *)
-
-Remark stack_below_trans:
-  forall ts b b', 
-  stack_below ts b -> b <= b' -> stack_below ts b'.
-Proof.
-  unfold stack_below; intros. 
-  destruct (parent_sp ts); auto. omega.
-Qed.
-
-Lemma match_stacks_store_other:
-  forall s ts ms mm,
-  match_stacks s ts mm ms ->
-  forall chunk b ofs v ms',
-  Mem.store chunk ms b ofs v = Some ms' ->
-  stack_below ts b ->
-  match_stacks s ts mm ms'.
-Proof.
-  induction 1; intros.
-  constructor.
-  red in H6; simpl in H6. 
-  econstructor; eauto.
-  eapply frame_match_store_other; eauto.
-  unfold block; omega.
-  eapply IHmatch_stacks; eauto.
-  eapply stack_below_trans; eauto. omega.
-Qed.
-
-Lemma match_stacks_store_slot:
-  forall s ts ms mm,
-  match_stacks s ts mm ms ->
-  forall ty ofs v ms' b i,
-  stack_below ts b ->
-  store_stack ms (Vptr b i) ty ofs v = Some ms' ->
-  match_stacks s ts mm ms'.
-Proof.
-  intros.
-  unfold store_stack in H1. simpl in H1.
-  inv H.
-  constructor.
-  red in H0; simpl in H0.
-  econstructor; eauto.
-  eapply frame_match_store_other; eauto.
-  unfold block; omega.
-  eapply match_stacks_store_other; eauto. 
-  eapply stack_below_trans; eauto. omega.
-Qed.
-
-Lemma match_stacks_store:
-  forall s ts ms mm,
-  match_stacks s ts mm ms ->
-  forall chunk b ofs v mm' v' ms',
-  Mem.store chunk mm b ofs v = Some mm' ->
-  Mem.store chunk ms b ofs v' = Some ms' ->
-  match_stacks s ts mm' ms'.
-Proof.
-  induction 1; intros.
-  constructor.
-  econstructor; eauto.
-  eapply frame_match_store; eauto.
-Qed.
-
-Lemma match_stacks_alloc:
-  forall s ts ms mm,
-  match_stacks s ts mm ms ->
-  forall lom him mm' b los his ms',
-  Mem.alloc mm lom him = (mm', b) ->
-  Mem.alloc ms los his = (ms', b) ->
-  match_stacks s ts mm' ms'.
-Proof.
-  induction 1; intros.
-  constructor.
-  econstructor; eauto. eapply frame_match_alloc; eauto.
-Qed.
-
-Lemma match_stacks_free:
-  forall s ts ms mm,
-  match_stacks s ts mm ms ->
-  forall b lom him los his mm' ms',
-  Mem.free mm b lom him = Some mm' ->
-  Mem.free ms b los his = Some ms' ->
-  stack_below ts b ->
-  match_stacks s ts mm' ms'.
-Proof.
-  induction 1; intros.
-  constructor.
-  red in H7; simpl in H7.
-  econstructor; eauto.
-  eapply frame_match_free; eauto. unfold block; omega.
-  eapply IHmatch_stacks; eauto.
-  eapply stack_below_trans; eauto. omega.
-Qed.
-
-Lemma match_stacks_function_entry:
-  forall s ts ms mm,
-  match_stacks s ts mm ms ->
-  forall lom him mm' stk los his ms',
-  Mem.alloc mm lom him = (mm', stk) ->
-  Mem.alloc ms los his = (ms', stk) ->
-  match_stacks s ts mm' ms' /\ stack_below ts stk.
-Proof.
-  intros.
-  assert (stk = Mem.nextblock mm) by eauto with mem.
-  split. eapply match_stacks_alloc; eauto.
-  red. inv H; simpl.
-  unfold Mem.nullptr. apply Zgt_lt. apply Mem.nextblock_pos.
-  inv H5. auto. 
-Qed.
-
-Lemma match_stacks_external_call:
-  forall s ts mm ms,
-  match_stacks s ts mm ms ->
-  forall ef vargs t vres mm' ms' vargs' vres',
-  Mem.extends mm ms ->
-  external_call ef ge vargs mm t vres mm' ->
-  Mem.extends mm' ms' ->
-  external_call ef ge vargs' ms t vres' ms' ->
-  mem_unchanged_on (loc_out_of_bounds mm) ms ms' ->
-  match_stacks s ts mm' ms'.
-Proof.
-  induction 1; intros.
-  constructor.
-  econstructor; eauto. 
-  eapply frame_match_external_call; eauto. 
-Qed.
-
-(** ** Invariant between states. *)
-
-(** The [match_state] predicate relates a Machabstr state with
-  a Machconcr state.  In addition to [match_stacks] between the
-  stacks, we ask that
-- The Machabstr frame is properly stored in the activation record,
-  as characterized by [frame_match].
-- The Machconcr memory state extends the Machabstr memory state,
-  in the sense of the [Mem.extends] relation defined in module [Mem]. *)
-
-Inductive match_states:
-            Machabstr.state -> Machconcr.state -> Prop :=
-  | match_states_intro:
-      forall s f sp base c rs fr mm ts trs fb ms
-        (STACKS: match_stacks s ts mm ms)
-        (FM: frame_match f (extend_frame f ts fr) sp base mm ms)
-        (BELOW: stack_below ts sp)
-        (RLD: regset_lessdef rs trs)
-        (MEXT: Mem.extends mm ms)
-        (FIND: Genv.find_funct_ptr ge fb = Some (Internal f)),
-      match_states (Machabstr.State s f (Vptr sp base) c rs fr mm)
-                   (Machconcr.State ts fb (Vptr sp base) c trs ms)
-  | match_states_call:
-      forall s f rs mm ts trs fb ms
-        (STACKS: match_stacks s ts mm ms)
-        (MEXT: Mem.extends mm ms)
-        (RLD: regset_lessdef rs trs)
-        (FIND: Genv.find_funct_ptr ge fb = Some f),
-      match_states (Machabstr.Callstate s f rs mm)
-                   (Machconcr.Callstate ts fb trs ms)
-  | match_states_return:
-      forall s rs mm ts trs ms
-        (STACKS: match_stacks s ts mm ms)
-        (MEXT: Mem.extends mm ms)
-        (RLD: regset_lessdef rs trs),
-      match_states (Machabstr.Returnstate s rs mm)
-                   (Machconcr.Returnstate ts trs ms).
-
-(** * The proof of simulation *)
-
-(** The proof of simulation relies on diagrams of the following form:
-<<
-           st1 --------------- st2
-            |                   |
-           t|                   |t
-            |                   |
-            v                   v
-           st1'--------------- st2'
->>
-  The precondition is matching between the initial states [st1] and
-  [st2], as usual, plus the fact that [st1] is well-typed
-  in the sense of predicate [wt_state] from module [Machtyping].
-  The postcondition is matching between the final states [st1']
-  and [st2'].  The well-typedness of [st2] is not part of the
-  postcondition, since it follows from that of [st1] if the
-  program is well-typed.  (See the subject reduction property
-  in module [Machtyping].)
-*)
-
-Lemma find_function_find_function_ptr:
-  forall ros rs f',
-  find_function ge ros rs = Some f' ->
-  exists fb', Genv.find_funct_ptr ge fb' = Some f' /\ find_function_ptr ge ros rs = Some fb'.
-Proof.
-  intros until f'. destruct ros; simpl.
-  intro. exploit Genv.find_funct_inv; eauto. intros [fb' EQ].
-  rewrite EQ in H. rewrite Genv.find_funct_find_funct_ptr in H.
-  exists fb'; split. auto. rewrite EQ. simpl. auto.
-  destruct (Genv.find_symbol ge i); intro.
-  exists b; auto. congruence.
-Qed.
-
-(** Preservation of arguments to external functions. *)
-
-Lemma transl_extcall_arguments:
-  forall rs s sg args ts trs m ms,
-  Machabstr.extcall_arguments (parent_function s) rs (parent_frame s) sg args ->
-  regset_lessdef rs trs ->
-  match_stacks s ts m ms ->
-  exists targs,
-     extcall_arguments trs ms (parent_sp ts) sg targs
-  /\ Val.lessdef_list args targs.
-Proof.
-  unfold Machabstr.extcall_arguments, extcall_arguments; intros.
-  generalize (loc_arguments sg) args H.
-  induction l; intros; inv H2.
-  exists (@nil val); split; constructor.
-  exploit IHl; eauto. intros [targs [A B]].
-  inv H7. exists (trs r :: targs); split.
-  constructor; auto. constructor. 
-  constructor; auto.
-  exploit match_stacks_get_parent; eauto. intros [targ [C D]]. 
-  exists (targ :: targs); split. 
-  constructor; auto. constructor; auto. 
-  constructor; auto.
-Qed.
-
-Hypothesis wt_prog: wt_program p.
-
-Theorem step_equiv:
-  forall s1 t s2, Machabstr.step ge s1 t s2 ->
-  forall s1' (MS: match_states s1 s1') (WTS: wt_state s1),
-  exists s2', Machconcr.step ge s1' t s2' /\ match_states s2 s2'.
-Proof.
-  induction 1; intros; inv MS.
-
-  (* Mlabel *)
-  econstructor; split.
-  apply exec_Mlabel; auto.
-  econstructor; eauto with coqlib.
-
-  (* Mgetstack *)
-  assert (WTF: wt_function f) by (inv WTS; auto).
-  exploit frame_match_get_slot; eauto. eapply get_slot_extends; eauto. 
-  intros [v' [A B]]. 
-  exists (State ts fb (Vptr sp0 base) c (trs#dst <- v') ms); split.
-  constructor; auto.
-  econstructor; eauto with coqlib. eapply regset_lessdef_set; eauto. 
-
-  (* Msetstack *)
-  assert (WTF: wt_function f) by (inv WTS; auto).
-  assert (Val.has_type (rs src) ty).
-    inv WTS. 
-    generalize (wt_function_instrs _ WTF _ (is_tail_in TAIL)); intro WTI.
-    inv WTI. apply WTRS.
-  exploit frame_match_set_slot. eauto. eauto. 
-    eapply set_slot_extends; eauto.
-    auto. apply RLD. auto. 
-  intros [ms' [STORE [FM' EXT']]].
-  exists (State ts fb (Vptr sp0 base) c trs ms'); split.
-  apply exec_Msetstack; auto.
-  econstructor; eauto.
-  eapply match_stacks_store_slot; eauto.
-
-  (* Mgetparam *)
-  assert (WTF: wt_function f) by (inv WTS; auto).
-  exploit match_stacks_get_parent; eauto. intros [v' [A B]].
-  exists (State ts fb (Vptr sp0 base) c (trs # IT1 <- Vundef # dst <- v') ms); split.
-  eapply exec_Mgetparam; eauto.
-    eapply frame_match_load_link; eauto.
-    eapply match_stacks_parent_sp_pointer; eauto.
-  econstructor; eauto with coqlib.
-  apply regset_lessdef_set; eauto. apply regset_lessdef_set; eauto.  
- 
-  (* Mop *)
-  exploit eval_operation_lessdef. 2: eauto.
-  eapply regset_lessdef_list; eauto. 
-  intros [v' [A B]].
-  exists (State ts fb (Vptr sp0 base) c ((undef_op op trs)#res <- v') ms); split.
-  apply exec_Mop; auto.
-  econstructor; eauto with coqlib. apply regset_lessdef_set; eauto.
-  apply regset_lessdef_undef_op; auto.
-
-  (* Mload *)
-  exploit eval_addressing_lessdef. 2: eauto. eapply regset_lessdef_list; eauto.
-  intros [a' [A B]].
-  exploit Mem.loadv_extends. eauto. eauto. eexact B. 
-  intros [v' [C D]].
-  exists (State ts fb (Vptr sp0 base) c ((undef_temps trs)#dst <- v') ms); split.
-  eapply exec_Mload; eauto.
-  econstructor; eauto with coqlib. apply regset_lessdef_set; eauto.
-  apply regset_lessdef_undef_temps; auto.
-
-  (* Mstore *)
-  exploit eval_addressing_lessdef. 2: eauto. eapply regset_lessdef_list; eauto.
-  intros [a' [A B]].
-  exploit Mem.storev_extends. eauto. eauto. eexact B. apply RLD. 
-  intros [ms' [C D]].
-  exists (State ts fb (Vptr sp0 base) c (undef_temps trs) ms'); split.
-  eapply exec_Mstore; eauto.
-  destruct a; simpl in H0; try congruence. inv B. simpl in C. 
-  econstructor; eauto with coqlib.
-  eapply match_stacks_store. eauto. eexact H0. eexact C.
-  eapply frame_match_store; eauto.
-  apply regset_lessdef_undef_temps; auto.
-
-  (* Mcall *)
-  exploit find_function_find_function_ptr; eauto. 
-  intros [fb' [FIND' FINDFUNCT]].
-  assert (exists ra', return_address_offset f c ra').
-    apply return_address_exists.
-    inv WTS. eapply is_tail_cons_left; eauto.
-  destruct H0 as [ra' RETADDR].
-  econstructor; split.
-  eapply exec_Mcall; eauto. eapply regset_lessdef_find_function_ptr; eauto. 
-  econstructor; eauto. 
-  econstructor; eauto. inv WTS; auto. exact I.
-
-  (* Mtailcall *)
-  assert (WTF: wt_function f) by (inv WTS; auto).
-  exploit find_function_find_function_ptr; eauto. 
-  intros [fb' [FIND' FINDFUNCT]].
-  exploit frame_match_delete; eauto. intros [ms' [A B]].
-  econstructor; split.
-  eapply exec_Mtailcall; eauto.
-    eapply regset_lessdef_find_function_ptr; eauto. 
-    eapply frame_match_load_link; eauto. eapply match_stacks_parent_sp_pointer; eauto.
-    eapply frame_match_load_retaddr; eauto. eapply match_stacks_parent_ra_pointer; eauto.
-  econstructor; eauto. eapply match_stacks_free; eauto.
-
-  (* Mbuiltin *)
-  exploit external_call_mem_extends; eauto. eapply regset_lessdef_list; eauto. 
-  intros [v' [ms' [A [B [C D]]]]].
-  econstructor; split.
-  eapply exec_Mbuiltin. eauto. 
-  econstructor; eauto with coqlib.
-  eapply match_stacks_external_call; eauto. 
-  eapply frame_match_external_call; eauto. 
-  apply regset_lessdef_set; eauto. apply regset_lessdef_undef_temps; auto.
-
-  (* Mgoto *)
-  econstructor; split.
-  eapply exec_Mgoto; eauto.
-  econstructor; eauto.
-
-  (* Mcond *)
-  econstructor; split.
-  eapply exec_Mcond_true; eauto.
-  eapply eval_condition_lessdef; eauto. apply regset_lessdef_list; auto.
-  econstructor; eauto. apply regset_lessdef_undef_temps; auto.
-  econstructor; split.
-  eapply exec_Mcond_false; eauto.
-  eapply eval_condition_lessdef; eauto. apply regset_lessdef_list; auto.
-  econstructor; eauto. apply regset_lessdef_undef_temps; auto.
-
-  (* Mjumptable *)
-  econstructor; split.
-  eapply exec_Mjumptable; eauto.
-  generalize (RLD arg); intro LD. rewrite H in LD. inv LD. auto.  
-  econstructor; eauto. apply regset_lessdef_undef_temps; auto.
-
-  (* Mreturn *)
-  assert (WTF: wt_function f) by (inv WTS; auto).
-  exploit frame_match_delete; eauto. intros [ms' [A B]].
-  econstructor; split.
-  eapply exec_Mreturn; eauto.
-    eapply frame_match_load_link; eauto. eapply match_stacks_parent_sp_pointer; eauto.
-    eapply frame_match_load_retaddr; eauto. eapply match_stacks_parent_ra_pointer; eauto.
-  econstructor; eauto. eapply match_stacks_free; eauto.   
-
-  (* internal function *)
-  assert (WTF: wt_function f). inv WTS. inv H5. auto.
-  exploit frame_match_function_entry. eauto. eauto. eauto. 
-  instantiate (1 := ts). eapply match_stacks_parent_sp_pointer; eauto.
-  eapply match_stacks_parent_ra_pointer; eauto.
-  intros [ms1 [ms2 [ms3 [ALLOC [STORE1 [STORE2 [FM MEXT']]]]]]].
-  econstructor; split.
-  eapply exec_function_internal; eauto.
-  exploit match_stacks_function_entry; eauto. intros [STACKS' BELOW].
-  econstructor; eauto.
-  eapply match_stacks_store_slot with (ms := ms2); eauto.
-  eapply match_stacks_store_slot with (ms := ms1); eauto.
-
-  (* external function *)
-  exploit transl_extcall_arguments; eauto. intros [targs [A B]].
-  exploit external_call_mem_extends; eauto. 
-  intros [tres [ms' [C [D [E F]]]]]. 
-  econstructor; split.
-  eapply exec_function_external. eauto. eexact C. eexact A. reflexivity.  
-  econstructor; eauto.
-  eapply match_stacks_external_call; eauto. 
-  apply regset_lessdef_set; auto. 
-
-  (* return *)
-  inv STACKS.
-  econstructor; split.
-  eapply exec_return. 
-  econstructor; eauto.
-Qed.
-
-Lemma equiv_initial_states:
-  forall st1, Machabstr.initial_state p st1 ->
-  exists st2, Machconcr.initial_state p st2 /\ match_states st1 st2 /\ wt_state st1.
-Proof.
-  intros. inversion H.
-  econstructor; split.
-  econstructor. eauto. eauto. 
-  split. econstructor. constructor. apply Mem.extends_refl.
-  unfold Regmap.init; red; intros. constructor.
-  auto.
-  econstructor. simpl; intros; contradiction.
-  eapply Genv.find_funct_ptr_prop; eauto.
-  red; intros; exact I.
-Qed.
-
-Lemma equiv_final_states:
-  forall st1 st2 r, 
-  match_states st1 st2 /\ wt_state st1 -> Machabstr.final_state st1 r -> Machconcr.final_state st2 r.
-Proof.
-  intros. inv H0. destruct H. inv H. inv STACKS.
-  constructor. 
-  generalize (RLD (loc_result (mksignature nil (Some Tint)))).
-  rewrite H1. intro LD. inv LD. auto. 
-Qed.
-
-Theorem exec_program_equiv:
-  forall (beh: program_behavior), not_wrong beh ->
-  Machabstr.exec_program p beh -> Machconcr.exec_program p beh.
-Proof.
-  unfold Machconcr.exec_program, Machabstr.exec_program; intros.
-  eapply simulation_step_preservation with
-    (step1 := Machabstr.step)
-    (step2 := Machconcr.step)
-    (match_states := fun st1 st2 => match_states st1 st2 /\ wt_state st1).
-  eexact equiv_initial_states.
-  eexact equiv_final_states.
-  intros. destruct H2. exploit step_equiv; eauto.
-  intros [st2' [A B]]. exists st2'; split. auto. split. auto.
-  eapply Machtyping.subject_reduction; eauto. 
-  auto. auto.
-Qed.
-
-End SIMULATION.
diff --git a/backend/Machconcr.v b/backend/Machsem.v
index 3f2a2e1..1a167a9 100644
--- a/backend/Machconcr.v
+++ b/backend/Machsem.v
@@ -10,7 +10,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(** The Mach intermediate language: concrete semantics. *)
+(** The Mach intermediate language: operational semantics. *)
 
 Require Import Coqlib.
 Require Import Maps.
@@ -28,8 +28,9 @@ Require Import Mach.
 Require Stacklayout.
 Require Asmgenretaddr.
 
-(** In the concrete semantics for Mach, the three stack-related Mach
-  instructions are interpreted as memory accesses relative to the
+(** The semantics for Mach is close to that of [Linear]: they differ only
+  on the interpretation of stack slot accesses.  In Mach, these
+  accesses are interpreted as memory accesses relative to the
   stack pointer.  More precisely:
 - [Mgetstack ofs ty r] is a memory load at offset [ofs * 4] relative
   to the stack pointer.
@@ -41,7 +42,7 @@ Require Asmgenretaddr.
   with the current record containing a pointer to the record of the
   caller function at offset 0.
 
-In addition to this linking of activation records, the concrete
+In addition to this linking of activation records, the
 semantics also make provisions for storing a back link at offset
 [f.(fn_link_ofs)] from the stack pointer, and a return address at
 offset [f.(fn_retaddr_ofs)].  The latter stack location will be used
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index a002746..49f339d 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -430,8 +430,7 @@ Qed.
   property: if the execution does not fail because of a failed run-time
   test, the result values and register states match the static
   typing assumptions.  This preservation property will be useful
-  later for the proof of semantic equivalence between
-  [Machabstr] and [Machconcr].
+  later for the proof of semantic equivalence between [Linear] and [Mach].
   Even though we do not need it for [RTL], we show preservation for [RTL]
   here, as a warm-up exercise and because some of the lemmas will be
   useful later. *)
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index c32886c..d651220 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -30,7 +30,7 @@ Require LTL.
 Require Import Linear.
 Require Import Lineartyping.
 Require Import Mach.
-Require Import Machconcr.
+Require Import Machsem.
 Require Import Bounds.
 Require Import Conventions.
 Require Import Stacklayout.
@@ -2215,7 +2215,7 @@ End EXTERNAL_ARGUMENTS.
 - Well-typedness of [f].
 *)
 
-Inductive match_states: Linear.state -> Machconcr.state -> Prop :=
+Inductive match_states: Linear.state -> Machsem.state -> Prop :=
   | match_states_intro:
       forall cs f sp c ls m cs' fb sp' rs m' j tf
         (MINJ: Mem.inject j m m')
@@ -2227,7 +2227,7 @@ Inductive match_states: Linear.state -> Machconcr.state -> Prop :=
         (AGFRAME: agree_frame f j ls (parent_locset cs) m sp m' sp' (parent_sp cs') (parent_ra cs'))
         (TAIL: is_tail c (Linear.fn_code f)),
       match_states (Linear.State cs f (Vptr sp Int.zero) c ls m)
-                  (Machconcr.State cs' fb (Vptr sp' Int.zero) (transl_code (make_env (function_bounds f)) c) rs m')
+                  (Machsem.State cs' fb (Vptr sp' Int.zero) (transl_code (make_env (function_bounds f)) c) rs m')
   | match_states_call:
       forall cs f ls m cs' fb rs m' j tf
         (MINJ: Mem.inject j m m')
@@ -2239,7 +2239,7 @@ Inductive match_states: Linear.state -> Machconcr.state -> Prop :=
         (AGREGS: agree_regs j ls rs)
         (AGLOCS: agree_callee_save ls (parent_locset cs)),
       match_states (Linear.Callstate cs f ls m)
-                  (Machconcr.Callstate cs' fb rs m')
+                  (Machsem.Callstate cs' fb rs m')
   | match_states_return:
       forall cs ls m cs' rs m' j sg 
         (MINJ: Mem.inject j m m')
@@ -2248,12 +2248,12 @@ Inductive match_states: Linear.state -> Machconcr.state -> Prop :=
         (AGREGS: agree_regs j ls rs)
         (AGLOCS: agree_callee_save ls (parent_locset cs)),
       match_states (Linear.Returnstate cs ls m)
-                  (Machconcr.Returnstate cs' rs m').
+                  (Machsem.Returnstate cs' rs m').
 
 Theorem transf_step_correct:
   forall s1 t s2, Linear.step ge s1 t s2 ->
   forall s1' (MS: match_states s1 s1'),
-  exists s2', plus Machconcr.step tge s1' t s2' /\ match_states s2 s2'.
+  exists s2', plus Machsem.step tge s1' t s2' /\ match_states s2 s2'.
 Proof.
   assert (RED: forall f i c,
           transl_code (make_env (function_bounds f)) (i :: c) = 
@@ -2586,7 +2586,7 @@ Qed.
 
 Lemma transf_initial_states:
   forall st1, Linear.initial_state prog st1 ->
-  exists st2, Machconcr.initial_state tprog st2 /\ match_states st1 st2.
+  exists st2, Machsem.initial_state tprog st2 /\ match_states st1 st2.
 Proof.
   intros. inv H.
   exploit function_ptr_translated; eauto. intros [tf [FIND TR]].
@@ -2614,7 +2614,7 @@ Qed.
 
 Lemma transf_final_states:
   forall st1 st2 r, 
-  match_states st1 st2 -> Linear.final_state st1 r -> Machconcr.final_state st2 r.
+  match_states st1 st2 -> Linear.final_state st1 r -> Machsem.final_state st2 r.
 Proof.
   intros. inv H0. inv H. inv STACKS.
   constructor.
@@ -2624,9 +2624,9 @@ Qed.
 
 Theorem transf_program_correct:
   forall (beh: program_behavior), not_wrong beh ->
-  Linear.exec_program prog beh -> Machconcr.exec_program tprog beh.
+  Linear.exec_program prog beh -> Machsem.exec_program tprog beh.
 Proof.
-  unfold Linear.exec_program, Machconcr.exec_program; intros.
+  unfold Linear.exec_program, Machsem.exec_program; intros.
   eapply simulation_plus_preservation; eauto.
   eexact transf_initial_states.
   eexact transf_final_states.
diff --git a/doc/index.html b/doc/index.html
index 9108a58..9e2d79d 100644
--- a/doc/index.html
+++ b/doc/index.html
@@ -130,8 +130,7 @@ replaced by a linear list of instructions with explicit branches and labels.
 spilling, reloading and enforcement of calling conventions.
 <LI> <A HREF="html/Mach.html">Mach</A>: like Linear, with a more concrete
 view of the activation record.  <BR>
-See also: <A HREF="html/Machabstr.html">Machabstr</A> abstract semantics for Mach. <BR>
-See also: <A HREF="html/Machconcr.html">Machconcr</A> concrete semantics for Mach.
+See also: <A HREF="html/Machsem.html">Machabstr</A> operational semantics for Mach. <BR>
 <LI> <A HREF="html/Asm.html">Asm</A>: abstract syntax for PowerPC assembly
 code.
 </UL>
diff --git a/driver/Compiler.v b/driver/Compiler.v
index 025b8af..cf05b3c 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -33,6 +33,7 @@ Require LTL.
 Require LTLin.
 Require Linear.
 Require Mach.
+Require Machsem.
 Require Asm.
 (** Translation passes. *)
 Require Initializers.
diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v
index f596f66..304b5da 100644
--- a/ia32/Asmgenproof.v
+++ b/ia32/Asmgenproof.v
@@ -26,7 +26,7 @@ Require Import Smallstep.
 Require Import Op.
 Require Import Locations.
 Require Import Mach.
-Require Import Machconcr.
+Require Import Machsem.
 Require Import Machtyping.
 Require Import Conventions.
 Require Import Asm.
@@ -562,7 +562,7 @@ Qed.
 - Mach register values and PPC register values agree.
 *)
 
-Inductive match_stack: list Machconcr.stackframe -> Prop :=
+Inductive match_stack: list Machsem.stackframe -> Prop :=
   | match_stack_nil:
       match_stack nil
   | match_stack_cons: forall fb sp ra c s f tf tc,
@@ -572,7 +572,7 @@ Inductive match_stack: list Machconcr.stackframe -> Prop :=
       match_stack s ->
       match_stack (Stackframe fb sp ra c :: s).
 
-Inductive match_states: Machconcr.state -> Asm.state -> Prop :=
+Inductive match_states: Machsem.state -> Asm.state -> Prop :=
   | match_states_intro:
       forall s fb sp c ep ms m m' rs f tf tc
         (STACKS: match_stack s)
@@ -581,7 +581,7 @@ Inductive match_states: Machconcr.state -> Asm.state -> Prop :=
         (AT: transl_code_at_pc (rs PC) fb f c ep tf tc)
         (AG: agree ms sp rs)
         (DXP: ep = true -> rs#EDX = parent_sp s),
-      match_states (Machconcr.State s fb sp c ms m)
+      match_states (Machsem.State s fb sp c ms m)
                    (Asm.State rs m')
   | match_states_call:
       forall s fb ms m m' rs
@@ -590,7 +590,7 @@ Inductive match_states: Machconcr.state -> Asm.state -> Prop :=
         (AG: agree ms (parent_sp s) rs)
         (ATPC: rs PC = Vptr fb Int.zero)
         (ATLR: rs RA = parent_ra s),
-      match_states (Machconcr.Callstate s fb ms m)
+      match_states (Machsem.Callstate s fb ms m)
                    (Asm.State rs m')
   | match_states_return:
       forall s ms m m' rs
@@ -598,7 +598,7 @@ Inductive match_states: Machconcr.state -> Asm.state -> Prop :=
         (MEXT: Mem.extends m m')
         (AG: agree ms (parent_sp s) rs)
         (ATPC: rs PC = parent_ra s),
-      match_states (Machconcr.Returnstate s ms m)
+      match_states (Machsem.Returnstate s ms m)
                    (Asm.State rs m').
 
 Lemma exec_straight_steps:
@@ -614,7 +614,7 @@ Lemma exec_straight_steps:
     /\ (edx_preserved ep i = true -> rs2#EDX = parent_sp s)) ->
   exists st',
   plus step tge (State rs1 m1') E0 st' /\
-  match_states (Machconcr.State s fb sp c ms2 m2) st'.
+  match_states (Machsem.State s fb sp c ms2 m2) st'.
 Proof.
   intros. inversion H2. subst. monadInv H7. 
   exploit H3; eauto. intros [rs2 [A [B C]]]. 
@@ -647,22 +647,22 @@ Qed.
   take infinitely many Mach transitions that correspond to zero
   transitions on the PPC side.  Actually, all Mach transitions
   correspond to at least one Asm transition, except the
-  transition from [Machconcr.Returnstate] to [Machconcr.State].
+  transition from [Machsem.Returnstate] to [Machsem.State].
   So, the following integer measure will suffice to rule out
   the unwanted behaviour. *)
 
-Definition measure (s: Machconcr.state) : nat :=
+Definition measure (s: Machsem.state) : nat :=
   match s with
-  | Machconcr.State _ _ _ _ _ _ => 0%nat
-  | Machconcr.Callstate _ _ _ _ => 0%nat
-  | Machconcr.Returnstate _ _ _ => 1%nat
+  | Machsem.State _ _ _ _ _ _ => 0%nat
+  | Machsem.Callstate _ _ _ _ => 0%nat
+  | Machsem.Returnstate _ _ _ => 1%nat
   end.
 
 (** We show the simulation diagram by case analysis on the Mach transition
   on the left.  Since the proof is large, we break it into one lemma
   per transition. *)
 
-Definition exec_instr_prop (s1: Machconcr.state) (t: trace) (s2: Machconcr.state) : Prop :=
+Definition exec_instr_prop (s1: Machsem.state) (t: trace) (s2: Machsem.state) : Prop :=
   forall s1' (MS: match_states s1 s1'),
   (exists s2', plus step tge s1' t s2' /\ match_states s2 s2')
   \/ (measure s2 < measure s1 /\ t = E0 /\ match_states s2 s1')%nat.
@@ -672,8 +672,8 @@ Lemma exec_Mlabel_prop:
   forall (s : list stackframe) (fb : block) (sp : val)
          (lbl : Mach.label) (c : list Mach.instruction) (ms : Mach.regset)
          (m : mem),
-  exec_instr_prop (Machconcr.State s fb sp (Mlabel lbl :: c) ms m) E0
-                  (Machconcr.State s fb sp c ms m).
+  exec_instr_prop (Machsem.State s fb sp (Mlabel lbl :: c) ms m) E0
+                  (Machsem.State s fb sp c ms m).
 Proof.
   intros; red; intros; inv MS.
   left; eapply exec_straight_steps; eauto; intros. 
@@ -686,8 +686,8 @@ Lemma exec_Mgetstack_prop:
          (ty : typ) (dst : mreg) (c : list Mach.instruction)
          (ms : Mach.regset) (m : mem) (v : val),
   load_stack m sp ty ofs = Some v ->
-  exec_instr_prop (Machconcr.State s fb sp (Mgetstack ofs ty dst :: c) ms m) E0
-                  (Machconcr.State s fb sp c (Regmap.set dst v ms) m).
+  exec_instr_prop (Machsem.State s fb sp (Mgetstack ofs ty dst :: c) ms m) E0
+                  (Machsem.State s fb sp c (Regmap.set dst v ms) m).
 Proof.
   intros; red; intros; inv MS.
   unfold load_stack in H.
@@ -705,8 +705,8 @@ Lemma exec_Msetstack_prop:
          (ofs : int) (ty : typ) (c : list Mach.instruction)
          (ms : mreg -> val) (m m' : mem),
   store_stack m sp ty ofs (ms src) = Some m' ->
-  exec_instr_prop (Machconcr.State s fb sp (Msetstack src ofs ty :: c) ms m) E0
-                  (Machconcr.State s fb sp c ms m').
+  exec_instr_prop (Machsem.State s fb sp (Msetstack src ofs ty :: c) ms m) E0
+                  (Machsem.State s fb sp c ms m').
 Proof.
   intros; red; intros; inv MS.
   unfold store_stack in H.
@@ -727,8 +727,8 @@ Lemma exec_Mgetparam_prop:
   Genv.find_funct_ptr ge fb = Some (Internal f) ->
   load_stack m sp Tint f.(fn_link_ofs) = Some (parent_sp s) ->
   load_stack m (parent_sp s) ty ofs = Some v ->
-  exec_instr_prop (Machconcr.State s fb sp (Mgetparam ofs ty dst :: c) ms m) E0
-                  (Machconcr.State s fb sp c (Regmap.set dst v (Regmap.set IT1 Vundef ms)) m).
+  exec_instr_prop (Machsem.State s fb sp (Mgetparam ofs ty dst :: c) ms m) E0
+                  (Machsem.State s fb sp c (Regmap.set dst v (Regmap.set IT1 Vundef ms)) m).
 Proof.
   intros; red; intros; inv MS.
   assert (f0 = f) by congruence. subst f0.
@@ -768,8 +768,8 @@ Lemma exec_Mop_prop:
          (args : list mreg) (res : mreg) (c : list Mach.instruction)
          (ms : mreg -> val) (m : mem) (v : val),
   eval_operation ge sp op ms ## args m = Some v ->
-  exec_instr_prop (Machconcr.State s fb sp (Mop op args res :: c) ms m) E0
-                  (Machconcr.State s fb sp c (Regmap.set res v (undef_op op ms)) m).
+  exec_instr_prop (Machsem.State s fb sp (Mop op args res :: c) ms m) E0
+                  (Machsem.State s fb sp c (Regmap.set res v (undef_op op ms)) m).
 Proof.
   intros; red; intros; inv MS.
   assert (eval_operation tge sp op ms##args m = Some v). 
@@ -793,8 +793,8 @@ Lemma exec_Mload_prop:
          (m : mem) (a v : val),
   eval_addressing ge sp addr ms ## args = Some a ->
   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 (undef_temps ms)) m).
+  exec_instr_prop (Machsem.State s fb sp (Mload chunk addr args dst :: c) ms m)
+               E0 (Machsem.State s fb sp c (Regmap.set dst v (undef_temps ms)) m).
 Proof.
   intros; red; intros; inv MS.
   assert (eval_addressing tge sp addr ms##args = Some a). 
@@ -816,8 +816,8 @@ Lemma exec_Mstore_prop:
          (m m' : mem) (a : val),
   eval_addressing ge sp addr ms ## args = Some a ->
   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 (undef_temps ms) m').
+  exec_instr_prop (Machsem.State s fb sp (Mstore chunk addr args src :: c) ms m) E0
+                  (Machsem.State s fb sp c (undef_temps ms) m').
 Proof.
   intros; red; intros; inv MS.
   assert (eval_addressing tge sp addr ms##args = Some a). 
@@ -841,7 +841,7 @@ Lemma exec_Mcall_prop:
   find_function_ptr ge ros ms = Some f' ->
   Genv.find_funct_ptr ge fb = Some (Internal f) ->
   return_address_offset f c ra ->
-  exec_instr_prop (Machconcr.State s fb sp (Mcall sig ros :: c) ms m) E0
+  exec_instr_prop (Machsem.State s fb sp (Mcall sig ros :: c) ms m) E0
                   (Callstate (Stackframe fb sp (Vptr fb ra) c :: s) f' ms m).
 Proof.
   intros; red; intros; inv MS.
@@ -902,7 +902,7 @@ Lemma exec_Mtailcall_prop:
   load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
   Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
   exec_instr_prop
-          (Machconcr.State s fb (Vptr stk soff) (Mtailcall sig ros :: c) ms m) E0
+          (Machsem.State s fb (Vptr stk soff) (Mtailcall sig ros :: c) ms m) E0
           (Callstate s f' ms m').
 Proof.
   intros; red; intros; inv MS.
@@ -960,8 +960,8 @@ Lemma exec_Mgoto_prop:
          (m : mem) (c' : Mach.code),
   Genv.find_funct_ptr ge fb = Some (Internal f) ->
   Mach.find_label lbl (fn_code f) = Some c' ->
-  exec_instr_prop (Machconcr.State s fb sp (Mgoto lbl :: c) ms m) E0
-                  (Machconcr.State s fb sp c' ms m).
+  exec_instr_prop (Machsem.State s fb sp (Mgoto lbl :: c) ms m) E0
+                  (Machsem.State s fb sp c' ms m).
 Proof.
   intros; red; intros; inv MS.
   assert (f0 = f) by congruence. subst f0.
@@ -983,8 +983,8 @@ Lemma exec_Mbuiltin_prop:
          (args : list mreg) (res : mreg) (b : list Mach.instruction)
          (t : trace) (v : val) (m' : mem),
   external_call ef ge ms ## args m t v m' ->
-  exec_instr_prop (Machconcr.State s f sp (Mbuiltin ef args res :: b) ms m) t
-                  (Machconcr.State s f sp b (Regmap.set res v (undef_temps ms)) m').
+  exec_instr_prop (Machsem.State s f sp (Mbuiltin ef args res :: b) ms m) t
+                  (Machsem.State s f sp b (Regmap.set res v (undef_temps ms)) m').
 Proof.
   intros; red; intros; inv MS.
   inv AT. monadInv H3. 
@@ -1017,8 +1017,8 @@ Lemma exec_Mcond_true_prop:
   eval_condition cond ms ## args m = Some true ->
   Genv.find_funct_ptr ge fb = Some (Internal f) ->
   Mach.find_label lbl (fn_code f) = Some c' ->
-  exec_instr_prop (Machconcr.State s fb sp (Mcond cond args lbl :: c) ms m) E0
-                  (Machconcr.State s fb sp c' (undef_temps ms) m).
+  exec_instr_prop (Machsem.State s fb sp (Mcond cond args lbl :: c) ms m) E0
+                  (Machsem.State s fb sp c' (undef_temps ms) m).
 Proof.
   intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0.
   exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC.
@@ -1045,8 +1045,8 @@ Lemma exec_Mcond_false_prop:
          (cond : condition) (args : list mreg) (lbl : Mach.label)
          (c : list Mach.instruction) (ms : mreg -> val) (m : mem),
   eval_condition cond ms ## args m = Some false ->
-  exec_instr_prop (Machconcr.State s fb sp (Mcond cond args lbl :: c) ms m) E0
-                  (Machconcr.State s fb sp c (undef_temps ms) m).
+  exec_instr_prop (Machsem.State s fb sp (Mcond cond args lbl :: c) ms m) E0
+                  (Machsem.State s fb sp c (undef_temps ms) m).
 Proof.
   intros; red; intros; inv MS.
   exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC.
@@ -1069,8 +1069,8 @@ Lemma exec_Mjumptable_prop:
   Genv.find_funct_ptr ge fb = Some (Internal f) ->
   Mach.find_label lbl (fn_code f) = Some c' ->
   exec_instr_prop
-    (Machconcr.State s fb sp (Mjumptable arg tbl :: c) rs m) E0
-    (Machconcr.State s fb sp c' (undef_temps rs) m).
+    (Machsem.State s fb sp (Mjumptable arg tbl :: c) rs m) E0
+    (Machsem.State s fb sp c' (undef_temps rs) m).
 Proof.
   intros; red; intros; inv MS.
   assert (f0 = f) by congruence. subst f0.
@@ -1098,7 +1098,7 @@ Lemma exec_Mreturn_prop:
   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 0 f.(fn_stacksize) = Some m' ->
-  exec_instr_prop (Machconcr.State s fb (Vptr stk soff) (Mreturn :: c) ms m) E0
+  exec_instr_prop (Machsem.State s fb (Vptr stk soff) (Mreturn :: c) ms m) E0
                   (Returnstate s ms m').
 Proof.
   intros; red; intros; inv MS.
@@ -1135,8 +1135,8 @@ Lemma exec_function_internal_prop:
   let sp := Vptr stk Int.zero 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 ->
-  exec_instr_prop (Machconcr.Callstate s fb ms m) E0
-                  (Machconcr.State s fb sp (fn_code f) (undef_temps ms) m3).
+  exec_instr_prop (Machsem.Callstate s fb ms m) E0
+                  (Machsem.State s fb sp (fn_code f) (undef_temps ms) m3).
 Proof.
   intros; red; intros; inv MS.
   exploit functions_translated; eauto. intros [tf [A B]]. monadInv B.
@@ -1174,10 +1174,10 @@ Lemma exec_function_external_prop:
          (ef : external_function) (args : list val) (res : val) (m': mem),
   Genv.find_funct_ptr ge fb = Some (External ef) ->
   external_call ef ge args m t0 res m' ->
-  Machconcr.extcall_arguments ms m (parent_sp s) (ef_sig ef) args ->
+  Machsem.extcall_arguments ms m (parent_sp s) (ef_sig ef) args ->
   ms' = Regmap.set (loc_result (ef_sig ef)) res ms ->
-  exec_instr_prop (Machconcr.Callstate s fb ms m)
-               t0 (Machconcr.Returnstate s ms' m').
+  exec_instr_prop (Machsem.Callstate s fb ms m)
+               t0 (Machsem.Returnstate s ms' m').
 Proof.
   intros; red; intros; inv MS.
   exploit functions_translated; eauto.
@@ -1200,8 +1200,8 @@ Qed.
 Lemma exec_return_prop:
   forall (s : list stackframe) (fb : block) (sp ra : val)
          (c : Mach.code) (ms : Mach.regset) (m : mem),
-  exec_instr_prop (Machconcr.Returnstate (Stackframe fb sp ra c :: s) ms m) E0
-                  (Machconcr.State s fb sp c ms m).
+  exec_instr_prop (Machsem.Returnstate (Stackframe fb sp ra c :: s) ms m) E0
+                  (Machsem.State s fb sp c ms m).
 Proof.
   intros; red; intros; inv MS. inv STACKS. simpl in *.
   right. split. omega. split. auto. 
@@ -1210,10 +1210,10 @@ Proof.
 Qed.
 
 Theorem transf_instr_correct:
-  forall s1 t s2, Machconcr.step ge s1 t s2 ->
+  forall s1 t s2, Machsem.step ge s1 t s2 ->
   exec_instr_prop s1 t s2.
 Proof
-  (Machconcr.step_ind ge exec_instr_prop
+  (Machsem.step_ind ge exec_instr_prop
            exec_Mlabel_prop
            exec_Mgetstack_prop
            exec_Msetstack_prop
@@ -1234,7 +1234,7 @@ Proof
            exec_return_prop).
 
 Lemma transf_initial_states:
-  forall st1, Machconcr.initial_state prog st1 ->
+  forall st1, Machsem.initial_state prog st1 ->
   exists st2, Asm.initial_state tprog st2 /\ match_states st1 st2.
 Proof.
   intros. inversion H. unfold ge0 in *.
@@ -1254,7 +1254,7 @@ Qed.
 
 Lemma transf_final_states:
   forall st1 st2 r, 
-  match_states st1 st2 -> Machconcr.final_state st1 r -> Asm.final_state st2 r.
+  match_states st1 st2 -> Machsem.final_state st1 r -> Asm.final_state st2 r.
 Proof.
   intros. inv H0. inv H. constructor. auto. 
   compute in H1. 
@@ -1263,9 +1263,9 @@ Qed.
 
 Theorem transf_program_correct:
   forall (beh: program_behavior), not_wrong beh ->
-  Machconcr.exec_program prog beh -> Asm.exec_program tprog beh.
+  Machsem.exec_program prog beh -> Asm.exec_program tprog beh.
 Proof.
-  unfold Machconcr.exec_program, Asm.exec_program; intros.
+  unfold Machsem.exec_program, Asm.exec_program; intros.
   eapply simulation_star_preservation with (measure := measure); eauto.
   eexact transf_initial_states.
   eexact transf_final_states.
diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v
index 81154f9..eb107ea 100644
--- a/ia32/Asmgenproof1.v
+++ b/ia32/Asmgenproof1.v
@@ -24,7 +24,7 @@ Require Import Globalenvs.
 Require Import Op.
 Require Import Locations.
 Require Import Mach.
-Require Import Machconcr.
+Require Import Machsem.
 Require Import Machtyping.
 Require Import Asm.
 Require Import Asmgen.
@@ -354,7 +354,7 @@ Qed.
 Lemma extcall_arg_match:
   forall ms sp rs m m' l v,
   agree ms sp rs ->
-  Machconcr.extcall_arg ms m sp l v ->
+  Machsem.extcall_arg ms m sp l v ->
   Mem.extends m m' ->
   exists v', Asm.extcall_arg rs m' l v' /\ Val.lessdef v v'.
 Proof.
@@ -369,7 +369,7 @@ Qed.
 Lemma extcall_args_match:
   forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' ->
   forall ll vl,
-  Machconcr.extcall_args ms m sp ll vl ->
+  Machsem.extcall_args ms m sp ll vl ->
   exists vl', Asm.extcall_args rs m' ll vl' /\ Val.lessdef_list vl vl'.
 Proof.
   induction 3.
@@ -382,11 +382,11 @@ Qed.
 Lemma extcall_arguments_match:
   forall ms m sp rs sg args m',
   agree ms sp rs ->
-  Machconcr.extcall_arguments ms m sp sg args ->
+  Machsem.extcall_arguments ms m sp sg args ->
   Mem.extends m m' ->
   exists args', Asm.extcall_arguments rs m' sg args' /\ Val.lessdef_list args args'.
 Proof.
-  unfold Machconcr.extcall_arguments, Asm.extcall_arguments; intros.
+  unfold Machsem.extcall_arguments, Asm.extcall_arguments; intros.
   eapply extcall_args_match; eauto.
 Qed.
 
diff --git a/ia32/Asmgenretaddr.v b/ia32/Asmgenretaddr.v
index 95df712..674a73e 100644
--- a/ia32/Asmgenretaddr.v
+++ b/ia32/Asmgenretaddr.v
@@ -13,7 +13,7 @@
 (** Predictor for return addresses in generated IA32 code.
 
     The [return_address_offset] predicate defined here is used in the
-    concrete semantics for Mach (module [Machconcr]) to determine the
+    semantics for Mach (module [Machsem]) to determine the
     return addresses that are stored in activation records. *)
 
 Require Import Coqlib.
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 8319363..3846a6c 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -27,7 +27,7 @@ Require Import Op.
 Require Import Locations.
 Require Import Conventions.
 Require Import Mach.
-Require Import Machconcr.
+Require Import Machsem.
 Require Import Machtyping.
 Require Import Asm.
 Require Import Asmgen.
@@ -555,7 +555,7 @@ Qed.
 - Mach register values and PPC register values agree.
 *)
 
-Inductive match_stack: list Machconcr.stackframe -> Prop :=
+Inductive match_stack: list Machsem.stackframe -> Prop :=
   | match_stack_nil:
       match_stack nil
   | match_stack_cons: forall fb sp ra c s f,
@@ -568,7 +568,7 @@ Inductive match_stack: list Machconcr.stackframe -> Prop :=
       match_stack s ->
       match_stack (Stackframe fb sp ra c :: s).
 
-Inductive match_states: Machconcr.state -> Asm.state -> Prop :=
+Inductive match_states: Machsem.state -> Asm.state -> Prop :=
   | match_states_intro:
       forall s fb sp c ms m rs m' f
         (STACKS: match_stack s)
@@ -578,7 +578,7 @@ Inductive match_states: Machconcr.state -> Asm.state -> Prop :=
         (AT: transl_code_at_pc (rs PC) fb f c)
         (AG: agree ms sp rs)
         (MEXT: Mem.extends m m'),
-      match_states (Machconcr.State s fb sp c ms m)
+      match_states (Machsem.State s fb sp c ms m)
                    (Asm.State rs m')
   | match_states_call:
       forall s fb ms m rs m'
@@ -587,7 +587,7 @@ Inductive match_states: Machconcr.state -> Asm.state -> Prop :=
         (MEXT: Mem.extends m m')
         (ATPC: rs PC = Vptr fb Int.zero)
         (ATLR: rs LR = parent_ra s),
-      match_states (Machconcr.Callstate s fb ms m)
+      match_states (Machsem.Callstate s fb ms m)
                    (Asm.State rs m')
   | match_states_return:
       forall s ms m rs m'
@@ -595,7 +595,7 @@ Inductive match_states: Machconcr.state -> Asm.state -> Prop :=
         (AG: agree ms (parent_sp s) rs)
         (MEXT: Mem.extends m m')
         (ATPC: rs PC = parent_ra s),
-      match_states (Machconcr.Returnstate s ms m)
+      match_states (Machsem.Returnstate s ms m)
                    (Asm.State rs m').
 
 Lemma exec_straight_steps:
@@ -611,7 +611,7 @@ Lemma exec_straight_steps:
   Mem.extends m2 m2' ->
   exists st',
   plus step tge (State rs1 m1') E0 st' /\
-  match_states (Machconcr.State s fb sp c2 ms2 m2) st'.
+  match_states (Machsem.State s fb sp c2 ms2 m2) st'.
 Proof.
   intros. destruct H4 as [rs2 [A B]].
   exists (State rs2 m2'); split.
@@ -633,7 +633,7 @@ Lemma exec_straight_steps_bis:
         /\ agree ms2 sp rs2) ->
   exists st',
   plus step tge (State rs1 m1') E0 st' /\
-  match_states (Machconcr.State s fb sp c2 ms2 m2) st'.
+  match_states (Machsem.State s fb sp c2 ms2 m2) st'.
 Proof.
   intros. destruct H4 as [m2' [A B]]. 
   eapply exec_straight_steps; eauto.
@@ -663,22 +663,22 @@ Qed.
   take infinitely many Mach transitions that correspond to zero
   transitions on the PPC side.  Actually, all Mach transitions
   correspond to at least one PPC transition, except the
-  transition from [Machconcr.Returnstate] to [Machconcr.State].
+  transition from [Machsem.Returnstate] to [Machsem.State].
   So, the following integer measure will suffice to rule out
   the unwanted behaviour. *)
 
-Definition measure (s: Machconcr.state) : nat :=
+Definition measure (s: Machsem.state) : nat :=
   match s with
-  | Machconcr.State _ _ _ _ _ _ => 0%nat
-  | Machconcr.Callstate _ _ _ _ => 0%nat
-  | Machconcr.Returnstate _ _ _ => 1%nat
+  | Machsem.State _ _ _ _ _ _ => 0%nat
+  | Machsem.Callstate _ _ _ _ => 0%nat
+  | Machsem.Returnstate _ _ _ => 1%nat
   end.
 
 (** We show the simulation diagram by case analysis on the Mach transition
   on the left.  Since the proof is large, we break it into one lemma
   per transition. *)
 
-Definition exec_instr_prop (s1: Machconcr.state) (t: trace) (s2: Machconcr.state) : Prop :=
+Definition exec_instr_prop (s1: Machsem.state) (t: trace) (s2: Machsem.state) : Prop :=
   forall s1' (MS: match_states s1 s1'),
   (exists s2', plus step tge s1' t s2' /\ match_states s2 s2')
   \/ (measure s2 < measure s1 /\ t = E0 /\ match_states s2 s1')%nat.
@@ -688,8 +688,8 @@ Lemma exec_Mlabel_prop:
   forall (s : list stackframe) (fb : block) (sp : val)
          (lbl : Mach.label) (c : list Mach.instruction) (ms : Mach.regset)
          (m : mem),
-  exec_instr_prop (Machconcr.State s fb sp (Mlabel lbl :: c) ms m) E0
-                  (Machconcr.State s fb sp c ms m).
+  exec_instr_prop (Machsem.State s fb sp (Mlabel lbl :: c) ms m) E0
+                  (Machsem.State s fb sp c ms m).
 Proof.
   intros; red; intros; inv MS.
   left; eapply exec_straight_steps; eauto with coqlib.
@@ -703,8 +703,8 @@ Lemma exec_Mgetstack_prop:
          (ty : typ) (dst : mreg) (c : list Mach.instruction)
          (ms : Mach.regset) (m : mem) (v : val),
   load_stack m sp ty ofs = Some v ->
-  exec_instr_prop (Machconcr.State s fb sp (Mgetstack ofs ty dst :: c) ms m) E0
-                  (Machconcr.State s fb sp c (Regmap.set dst v ms) m).
+  exec_instr_prop (Machsem.State s fb sp (Mgetstack ofs ty dst :: c) ms m) E0
+                  (Machsem.State s fb sp c (Regmap.set dst v ms) m).
 Proof.
   intros; red; intros; inv MS.
   unfold load_stack in H. 
@@ -729,8 +729,8 @@ Lemma exec_Msetstack_prop:
          (ofs : int) (ty : typ) (c : list Mach.instruction)
          (ms : mreg -> val) (m m' : mem),
   store_stack m sp ty ofs (ms src) = Some m' ->
-  exec_instr_prop (Machconcr.State s fb sp (Msetstack src ofs ty :: c) ms m) E0
-                  (Machconcr.State s fb sp c ms m').
+  exec_instr_prop (Machsem.State s fb sp (Msetstack src ofs ty :: c) ms m) E0
+                  (Machsem.State s fb sp c ms m').
 Proof.
   intros; red; intros; inv MS.
   unfold store_stack in H. 
@@ -756,8 +756,8 @@ Lemma exec_Mgetparam_prop:
   Genv.find_funct_ptr ge fb = Some (Internal f) ->
   load_stack m sp Tint f.(fn_link_ofs) = Some (parent_sp s) ->
   load_stack m (parent_sp s) ty ofs = Some v ->
-  exec_instr_prop (Machconcr.State s fb sp (Mgetparam ofs ty dst :: c) ms m) E0
-                  (Machconcr.State s fb sp c (Regmap.set dst v (Regmap.set IT1 Vundef ms)) m).
+  exec_instr_prop (Machsem.State s fb sp (Mgetparam ofs ty dst :: c) ms m) E0
+                  (Machsem.State s fb sp c (Regmap.set dst v (Regmap.set IT1 Vundef ms)) m).
 Proof.
   intros; red; intros; inv MS.
   assert (f0 = f) by congruence. subst f0.
@@ -793,8 +793,8 @@ Lemma exec_Mop_prop:
          (args : list mreg) (res : mreg) (c : list Mach.instruction)
          (ms : mreg -> val) (m : mem) (v : val),
   eval_operation ge sp op ms ## args m = Some v ->
-  exec_instr_prop (Machconcr.State s fb sp (Mop op args res :: c) ms m) E0
-                  (Machconcr.State s fb sp c (Regmap.set res v (undef_op op ms)) m).
+  exec_instr_prop (Machsem.State s fb sp (Mop op args res :: c) ms m) E0
+                  (Machsem.State s fb sp c (Regmap.set res v (undef_op op ms)) m).
 Proof.
   intros; red; intros; inv MS.
   generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
@@ -823,8 +823,8 @@ Lemma exec_Mload_prop:
          (m : mem) (a v : val),
   eval_addressing ge sp addr ms ## args = Some a ->
   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 (undef_temps ms)) m).
+  exec_instr_prop (Machsem.State s fb sp (Mload chunk addr args dst :: c) ms m)
+               E0 (Machsem.State s fb sp c (Regmap.set dst v (undef_temps ms)) m).
 Proof.
   intros; red; intros; inv MS.
   generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
@@ -880,8 +880,8 @@ Lemma exec_Mstore_prop:
          (m m' : mem) (a : val),
   eval_addressing ge sp addr ms ## args = Some a ->
   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 (undef_temps ms) m').
+  exec_instr_prop (Machsem.State s fb sp (Mstore chunk addr args src :: c) ms m) E0
+                  (Machsem.State s fb sp c (undef_temps ms) m').
 Proof.
   intros; red; intros; inv MS.
   generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
@@ -905,7 +905,7 @@ Lemma exec_Mcall_prop:
   find_function_ptr ge ros ms = Some f' ->
   Genv.find_funct_ptr ge fb = Some (Internal f) ->
   return_address_offset f c ra ->
-  exec_instr_prop (Machconcr.State s fb sp (Mcall sig ros :: c) ms m) E0
+  exec_instr_prop (Machsem.State s fb sp (Mcall sig ros :: c) ms m) E0
                   (Callstate (Stackframe fb sp (Vptr fb ra) c :: s) f' ms m).
 Proof.
   intros; red; intros; inv MS.
@@ -989,7 +989,7 @@ Lemma exec_Mtailcall_prop:
   load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
   Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
   exec_instr_prop
-          (Machconcr.State s fb (Vptr stk soff) (Mtailcall sig ros :: c) ms m) E0
+          (Machsem.State s fb (Vptr stk soff) (Mtailcall sig ros :: c) ms m) E0
           (Callstate s f' ms m').
 Proof.
   intros; red; intros; inv MS.
@@ -1100,8 +1100,8 @@ Lemma exec_Mbuiltin_prop:
          (args : list mreg) (res : mreg) (b : list Mach.instruction)
          (t : trace) (v : val) (m' : mem),
   external_call ef ge ms ## args m t v m' ->
-  exec_instr_prop (Machconcr.State s f sp (Mbuiltin ef args res :: b) ms m) t
-                  (Machconcr.State s f sp b (Regmap.set res v (undef_temps ms)) m').
+  exec_instr_prop (Machsem.State s f sp (Mbuiltin ef args res :: b) ms m) t
+                  (Machsem.State s f sp b (Regmap.set res v (undef_temps ms)) m').
 Proof.
   intros; red; intros; inv MS.
   generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
@@ -1132,8 +1132,8 @@ Lemma exec_Mgoto_prop:
          (m : mem) (c' : Mach.code),
   Genv.find_funct_ptr ge fb = Some (Internal f) ->
   Mach.find_label lbl (fn_code f) = Some c' ->
-  exec_instr_prop (Machconcr.State s fb sp (Mgoto lbl :: c) ms m) E0
-                  (Machconcr.State s fb sp c' ms m).
+  exec_instr_prop (Machsem.State s fb sp (Mgoto lbl :: c) ms m) E0
+                  (Machsem.State s fb sp c' ms m).
 Proof.
   intros; red; intros; inv MS.
   assert (f0 = f) by congruence. subst f0.
@@ -1158,8 +1158,8 @@ Lemma exec_Mcond_true_prop:
   eval_condition cond ms ## args m = Some true ->
   Genv.find_funct_ptr ge fb = Some (Internal f) ->
   Mach.find_label lbl (fn_code f) = Some c' ->
-  exec_instr_prop (Machconcr.State s fb sp (Mcond cond args lbl :: c) ms m) E0
-                  (Machconcr.State s fb sp c' (undef_temps ms) m).
+  exec_instr_prop (Machsem.State s fb sp (Mcond cond args lbl :: c) ms m) E0
+                  (Machsem.State s fb sp c' (undef_temps ms) m).
 Proof.
   intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0.
   generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
@@ -1198,8 +1198,8 @@ Lemma exec_Mcond_false_prop:
          (cond : condition) (args : list mreg) (lbl : Mach.label)
          (c : list Mach.instruction) (ms : mreg -> val) (m : mem),
   eval_condition cond ms ## args m = Some false ->
-  exec_instr_prop (Machconcr.State s fb sp (Mcond cond args lbl :: c) ms m) E0
-                  (Machconcr.State s fb sp c (undef_temps ms) m).
+  exec_instr_prop (Machsem.State s fb sp (Mcond cond args lbl :: c) ms m) E0
+                  (Machsem.State s fb sp c (undef_temps ms) m).
 Proof.
   intros; red; intros; inv MS.
   generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
@@ -1227,8 +1227,8 @@ Lemma exec_Mjumptable_prop:
   Genv.find_funct_ptr ge fb = Some (Internal f) ->
   Mach.find_label lbl (fn_code f) = Some c' ->
   exec_instr_prop
-    (Machconcr.State s fb sp (Mjumptable arg tbl :: c) rs m) E0
-    (Machconcr.State s fb sp c' (undef_temps rs) m).
+    (Machsem.State s fb sp (Mjumptable arg tbl :: c) rs m) E0
+    (Machsem.State s fb sp c' (undef_temps rs) m).
 Proof.
   intros; red; intros; inv MS.
   assert (f0 = f) by congruence. subst f0.
@@ -1284,7 +1284,7 @@ Lemma exec_Mreturn_prop:
   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 0 f.(fn_stacksize) = Some m' ->
-  exec_instr_prop (Machconcr.State s fb (Vptr stk soff) (Mreturn :: c) ms m) E0
+  exec_instr_prop (Machsem.State s fb (Vptr stk soff) (Mreturn :: c) ms m) E0
                   (Returnstate s ms m').
 Proof.
   intros; red; intros; inv MS.
@@ -1348,8 +1348,8 @@ Lemma exec_function_internal_prop:
   let sp := Vptr stk Int.zero 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 ->
-  exec_instr_prop (Machconcr.Callstate s fb ms m) E0
-                  (Machconcr.State s fb sp (fn_code f) (undef_temps ms) m3).
+  exec_instr_prop (Machsem.Callstate s fb ms m) E0
+                  (Machsem.State s fb sp (fn_code f) (undef_temps ms) m3).
 Proof.
   intros; red; intros; inv MS.
   assert (WTF: wt_function f).
@@ -1411,10 +1411,10 @@ Lemma exec_function_external_prop:
          (ef : external_function) (args : list val) (res : val) (m': mem),
   Genv.find_funct_ptr ge fb = Some (External ef) ->
   external_call ef ge args m t0 res m' ->
-  Machconcr.extcall_arguments ms m (parent_sp s) (ef_sig ef) args ->
+  Machsem.extcall_arguments ms m (parent_sp s) (ef_sig ef) args ->
   ms' = Regmap.set (loc_result (ef_sig ef)) res ms ->
-  exec_instr_prop (Machconcr.Callstate s fb ms m)
-               t0 (Machconcr.Returnstate s ms' m').
+  exec_instr_prop (Machsem.Callstate s fb ms m)
+               t0 (Machsem.Returnstate s ms' m').
 Proof.
   intros; red; intros; inv MS.
   exploit functions_translated; eauto.
@@ -1435,8 +1435,8 @@ Qed.
 Lemma exec_return_prop:
   forall (s : list stackframe) (fb : block) (sp ra : val)
          (c : Mach.code) (ms : Mach.regset) (m : mem),
-  exec_instr_prop (Machconcr.Returnstate (Stackframe fb sp ra c :: s) ms m) E0
-                  (Machconcr.State s fb sp c ms m).
+  exec_instr_prop (Machsem.Returnstate (Stackframe fb sp ra c :: s) ms m) E0
+                  (Machsem.State s fb sp c ms m).
 Proof.
   intros; red; intros; inv MS. inv STACKS. simpl in *.
   right. split. omega. split. auto. 
@@ -1444,10 +1444,10 @@ Proof.
 Qed.
 
 Theorem transf_instr_correct:
-  forall s1 t s2, Machconcr.step ge s1 t s2 ->
+  forall s1 t s2, Machsem.step ge s1 t s2 ->
   exec_instr_prop s1 t s2.
 Proof
-  (Machconcr.step_ind ge exec_instr_prop
+  (Machsem.step_ind ge exec_instr_prop
            exec_Mlabel_prop
            exec_Mgetstack_prop
            exec_Msetstack_prop
@@ -1468,7 +1468,7 @@ Proof
            exec_return_prop).
 
 Lemma transf_initial_states:
-  forall st1, Machconcr.initial_state prog st1 ->
+  forall st1, Machsem.initial_state prog st1 ->
   exists st2, Asm.initial_state tprog st2 /\ match_states st1 st2.
 Proof.
   intros. inversion H. unfold ge0 in *.
@@ -1488,7 +1488,7 @@ Qed.
 
 Lemma transf_final_states:
   forall st1 st2 r, 
-  match_states st1 st2 -> Machconcr.final_state st1 r -> Asm.final_state st2 r.
+  match_states st1 st2 -> Machsem.final_state st1 r -> Asm.final_state st2 r.
 Proof.
   intros. inv H0. inv H. constructor. auto. 
   compute in H1.
@@ -1497,9 +1497,9 @@ Qed.
 
 Theorem transf_program_correct:
   forall (beh: program_behavior), not_wrong beh ->
-  Machconcr.exec_program prog beh -> Asm.exec_program tprog beh.
+  Machsem.exec_program prog beh -> Asm.exec_program tprog beh.
 Proof.
-  unfold Machconcr.exec_program, Asm.exec_program; intros.
+  unfold Machsem.exec_program, Asm.exec_program; intros.
   eapply simulation_star_preservation with (measure := measure); eauto.
   eexact transf_initial_states.
   eexact transf_final_states.
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index 16dd923..a0cdeab 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -23,7 +23,7 @@ Require Import Globalenvs.
 Require Import Op.
 Require Import Locations.
 Require Import Mach.
-Require Import Machconcr.
+Require Import Machsem.
 Require Import Machtyping.
 Require Import Asm.
 Require Import Asmgen.
@@ -486,7 +486,7 @@ Lemma extcall_arg_match:
   forall ms sp rs m m' l v,
   agree ms sp rs ->
   Mem.extends m m' ->
-  Machconcr.extcall_arg ms m sp l v ->
+  Machsem.extcall_arg ms m sp l v ->
   exists v', Asm.extcall_arg rs m' l v' /\ Val.lessdef v v'.
 Proof.
   intros. inv H1.
@@ -503,7 +503,7 @@ Qed.
 Lemma extcall_args_match:
   forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' ->
   forall ll vl,
-  Machconcr.extcall_args ms m sp ll vl ->
+  Machsem.extcall_args ms m sp ll vl ->
   exists vl', Asm.extcall_args rs m' ll vl' /\ Val.lessdef_list vl vl'.
 Proof.
   induction 3; intros. 
@@ -516,10 +516,10 @@ Qed.
 Lemma extcall_arguments_match:
   forall ms m m' sp rs sg args,
   agree ms sp rs -> Mem.extends m m' ->
-  Machconcr.extcall_arguments ms m sp sg args ->
+  Machsem.extcall_arguments ms m sp sg args ->
   exists args', Asm.extcall_arguments rs m' sg args' /\ Val.lessdef_list args args'.
 Proof.
-  unfold Machconcr.extcall_arguments, Asm.extcall_arguments; intros.
+  unfold Machsem.extcall_arguments, Asm.extcall_arguments; intros.
   eapply extcall_args_match; eauto.
 Qed.
 
diff --git a/powerpc/Asmgenretaddr.v b/powerpc/Asmgenretaddr.v
index a15bf73..5b1f7d5 100644
--- a/powerpc/Asmgenretaddr.v
+++ b/powerpc/Asmgenretaddr.v
@@ -13,7 +13,7 @@
 (** Predictor for return addresses in generated PPC code.
 
     The [return_address_offset] predicate defined here is used in the
-    concrete semantics for Mach (module [Machconcr]) to determine the
+    semantics for Mach (module [Machsem]) to determine the
     return addresses that are stored in activation records. *)
 
 Require Import Coqlib.