summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.depend10
-rw-r--r--Makefile2
-rw-r--r--arm/Asmgenproof.v106
-rw-r--r--arm/Asmgenproof1.v10
-rw-r--r--arm/Asmgenretaddr.v2
-rw-r--r--backend/Machabstr.v337
-rw-r--r--backend/Machabstr2concr.v1160
-rw-r--r--backend/Machsem.v (renamed from backend/Machconcr.v)9
-rw-r--r--backend/RTLtyping.v3
-rw-r--r--backend/Stackingproof.v20
-rw-r--r--doc/index.html3
-rw-r--r--driver/Compiler.v1
-rw-r--r--ia32/Asmgenproof.v106
-rw-r--r--ia32/Asmgenproof1.v10
-rw-r--r--ia32/Asmgenretaddr.v2
-rw-r--r--powerpc/Asmgenproof.v108
-rw-r--r--powerpc/Asmgenproof1.v10
-rw-r--r--powerpc/Asmgenretaddr.v2
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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-21 16:17:11 +0000