From 5a4bd6f2636df432383bb3144f91816742d2fa53 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 9 Apr 2011 17:16:55 +0000 Subject: Renamed Machconcr into Machsem. Removed Machabstr and Machabstr2concr, now useless following the reengineering of Stacking. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1633 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- .depend | 10 +- Makefile | 2 +- arm/Asmgenproof.v | 106 ++--- arm/Asmgenproof1.v | 10 +- arm/Asmgenretaddr.v | 2 +- backend/Machabstr.v | 337 ------------- backend/Machabstr2concr.v | 1160 --------------------------------------------- backend/Machconcr.v | 266 ----------- backend/Machsem.v | 267 +++++++++++ backend/RTLtyping.v | 3 +- backend/Stackingproof.v | 20 +- doc/index.html | 3 +- driver/Compiler.v | 1 + ia32/Asmgenproof.v | 106 ++--- ia32/Asmgenproof1.v | 10 +- ia32/Asmgenretaddr.v | 2 +- powerpc/Asmgenproof.v | 108 ++--- powerpc/Asmgenproof1.v | 10 +- powerpc/Asmgenretaddr.v | 2 +- 19 files changed, 464 insertions(+), 1961 deletions(-) delete mode 100644 backend/Machabstr.v delete mode 100644 backend/Machabstr2concr.v delete mode 100644 backend/Machconcr.v create mode 100644 backend/Machsem.v 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/Machconcr.v deleted file mode 100644 index 3f2a2e1..0000000 --- a/backend/Machconcr.v +++ /dev/null @@ -1,266 +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: concrete semantics. *) - -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 Conventions. -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 - stack pointer. More precisely: -- [Mgetstack ofs ty r] is a memory load at offset [ofs * 4] relative - to the stack pointer. -- [Msetstack r ofs ty] is a memory store at offset [ofs * 4] relative - to the stack pointer. -- [Mgetparam ofs ty r] is a memory load at offset [ofs * 4] - relative to the pointer found at offset 0 from the stack pointer. - The semantics maintain a linked structure of activation records, - 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 -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 -by the Asm code generated by [Asmgen] to save the return address into -the caller at the beginning of a function, then restore it and jump to -it at the end of a function. The Mach concrete semantics does not -attach any particular meaning to the pointer stored in this reserved -location, but makes sure that it is preserved during execution of a -function. The [return_address_offset] predicate from module -[Asmgenretaddr] is used to guess the value of the return address that -the Asm code generated later will store in the reserved location. -*) - -Definition chunk_of_type (ty: typ) := - match ty with Tint => Mint32 | Tfloat => Mfloat64 end. - -Definition load_stack (m: mem) (sp: val) (ty: typ) (ofs: int) := - Mem.loadv (chunk_of_type ty) m (Val.add sp (Vint ofs)). - -Definition store_stack (m: mem) (sp: val) (ty: typ) (ofs: int) (v: val) := - Mem.storev (chunk_of_type ty) m (Val.add sp (Vint ofs)) v. - -(** Extract the values of the arguments of an external call. *) - -Inductive extcall_arg: regset -> mem -> val -> loc -> val -> Prop := - | extcall_arg_reg: forall rs m sp r, - extcall_arg rs m sp (R r) (rs r) - | extcall_arg_stack: forall rs m sp ofs ty v, - load_stack m sp ty (Int.repr (Stacklayout.fe_ofs_arg + 4 * ofs)) = Some v -> - extcall_arg rs m sp (S (Outgoing ofs ty)) v. - -Inductive extcall_args: regset -> mem -> val -> list loc -> list val -> Prop := - | extcall_args_nil: forall rs m sp, - extcall_args rs m sp nil nil - | extcall_args_cons: forall rs m sp l1 ll v1 vl, - extcall_arg rs m sp l1 v1 -> extcall_args rs m sp ll vl -> - extcall_args rs m sp (l1 :: ll) (v1 :: vl). - -Definition extcall_arguments - (rs: regset) (m: mem) (sp: val) (sg: signature) (args: list val) : Prop := - extcall_args rs m sp (loc_arguments sg) args. - -(** Mach execution states. *) - -Inductive stackframe: Type := - | Stackframe: - forall (f: block) (**r pointer to calling function *) - (sp: val) (**r stack pointer in calling function *) - (retaddr: val) (**r Asm return address in calling function *) - (c: code), (**r program point in calling function *) - stackframe. - -Inductive state: Type := - | State: - forall (stack: list stackframe) (**r call stack *) - (f: block) (**r pointer to current function *) - (sp: val) (**r stack pointer *) - (c: code) (**r current program point *) - (rs: regset) (**r register state *) - (m: mem), (**r memory state *) - state - | Callstate: - forall (stack: list stackframe) (**r call stack *) - (f: block) (**r pointer to 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. - -Definition parent_sp (s: list stackframe) : val := - match s with - | nil => Vptr Mem.nullptr Int.zero - | Stackframe f sp ra c :: s' => sp - end. - -Definition parent_ra (s: list stackframe) : val := - match s with - | nil => Vzero - | Stackframe f sp ra c :: s' => ra - end. - -Section RELSEM. - -Variable ge: genv. - -Inductive step: state -> trace -> state -> Prop := - | exec_Mlabel: - forall s f sp lbl c rs m, - step (State s f sp (Mlabel lbl :: c) rs m) - E0 (State s f sp c rs m) - | exec_Mgetstack: - forall s f sp ofs ty dst c rs m v, - load_stack m sp ty ofs = Some v -> - step (State s f sp (Mgetstack ofs ty dst :: c) rs m) - E0 (State s f sp c (rs#dst <- v) m) - | exec_Msetstack: - forall s f sp src ofs ty c rs m m', - store_stack m sp ty ofs (rs src) = Some m' -> - step (State s f sp (Msetstack src ofs ty :: c) rs m) - E0 (State s f sp c rs m') - | exec_Mgetparam: - forall s fb f sp ofs ty dst c rs m v, - 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 -> - step (State s fb sp (Mgetparam ofs ty dst :: c) rs m) - E0 (State s fb sp c (rs # IT1 <- Vundef # dst <- v) m) - | exec_Mop: - forall s f sp op args res c rs m v, - eval_operation ge sp op rs##args m = Some v -> - step (State s f sp (Mop op args res :: c) rs m) - E0 (State s f sp c ((undef_op op rs)#res <- v) m) - | exec_Mload: - forall s f sp chunk addr args dst c rs 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 m) - E0 (State s f sp c ((undef_temps rs)#dst <- v) m) - | exec_Mstore: - forall s f sp chunk addr args src c rs 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 m) - E0 (State s f sp c (undef_temps rs) m') - | exec_Mcall: - forall s fb sp sig ros c rs m f f' ra, - find_function_ptr ge ros rs = Some f' -> - Genv.find_funct_ptr ge fb = Some (Internal f) -> - Asmgenretaddr.return_address_offset f c ra -> - step (State s fb sp (Mcall sig ros :: c) rs m) - E0 (Callstate (Stackframe fb sp (Vptr fb ra) c :: s) - f' rs m) - | exec_Mtailcall: - forall s fb stk soff sig ros c rs m f f' m', - find_function_ptr ge ros rs = Some f' -> - Genv.find_funct_ptr ge fb = Some (Internal f) -> - load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) -> - load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) -> - Mem.free m stk 0 f.(fn_stacksize) = Some m' -> - step (State s fb (Vptr stk soff) (Mtailcall sig ros :: c) rs m) - E0 (Callstate s f' rs m') - | exec_Mbuiltin: - forall s f sp rs 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 m) - t (State s f sp b ((undef_temps rs)#res <- v) m') - | exec_Mgoto: - forall s fb f sp lbl c rs m c', - Genv.find_funct_ptr ge fb = Some (Internal f) -> - find_label lbl f.(fn_code) = Some c' -> - step (State s fb sp (Mgoto lbl :: c) rs m) - E0 (State s fb sp c' rs m) - | exec_Mcond_true: - forall s fb f sp cond args lbl c rs m c', - eval_condition cond rs##args m = Some true -> - Genv.find_funct_ptr ge fb = Some (Internal f) -> - find_label lbl f.(fn_code) = Some c' -> - step (State s fb sp (Mcond cond args lbl :: c) rs m) - E0 (State s fb sp c' (undef_temps rs) m) - | exec_Mcond_false: - forall s f sp cond args lbl c rs m, - eval_condition cond rs##args m = Some false -> - step (State s f sp (Mcond cond args lbl :: c) rs m) - E0 (State s f sp c (undef_temps rs) m) - | exec_Mjumptable: - forall s fb f sp arg tbl c rs m n lbl c', - rs arg = Vint n -> - list_nth_z tbl (Int.unsigned n) = Some lbl -> - Genv.find_funct_ptr ge fb = Some (Internal f) -> - find_label lbl f.(fn_code) = Some c' -> - step (State s fb sp (Mjumptable arg tbl :: c) rs m) - E0 (State s fb sp c' (undef_temps rs) m) - | exec_Mreturn: - forall s fb stk soff c rs m f m', - Genv.find_funct_ptr ge fb = Some (Internal f) -> - load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) -> - load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) -> - Mem.free m stk 0 f.(fn_stacksize) = Some m' -> - step (State s fb (Vptr stk soff) (Mreturn :: c) rs m) - E0 (Returnstate s rs m') - | exec_function_internal: - forall s fb rs m f m1 m2 m3 stk, - Genv.find_funct_ptr ge fb = Some (Internal f) -> - Mem.alloc m 0 f.(fn_stacksize) = (m1, stk) -> - 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 -> - step (Callstate s fb rs m) - E0 (State s fb sp f.(fn_code) (undef_temps rs) m3) - | exec_function_external: - forall s fb rs m t rs' ef args res m', - Genv.find_funct_ptr ge fb = Some (External ef) -> - external_call ef ge args m t res m' -> - extcall_arguments rs m (parent_sp s) (ef_sig ef) args -> - rs' = (rs#(loc_result (ef_sig ef)) <- res) -> - step (Callstate s fb rs m) - t (Returnstate s rs' m') - | exec_return: - forall s f sp ra c rs m, - step (Returnstate (Stackframe f sp ra c :: s) rs m) - E0 (State s f sp c rs m). - -End RELSEM. - -Inductive initial_state (p: program): state -> Prop := - | initial_state_intro: forall fb m0, - let ge := Genv.globalenv p in - Genv.init_mem p = Some m0 -> - Genv.find_symbol ge p.(prog_main) = Some fb -> - initial_state p (Callstate nil fb (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/Machsem.v b/backend/Machsem.v new file mode 100644 index 0000000..1a167a9 --- /dev/null +++ b/backend/Machsem.v @@ -0,0 +1,267 @@ +(* *********************************************************************) +(* *) +(* 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: operational semantics. *) + +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 Conventions. +Require Import Mach. +Require Stacklayout. +Require Asmgenretaddr. + +(** 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. +- [Msetstack r ofs ty] is a memory store at offset [ofs * 4] relative + to the stack pointer. +- [Mgetparam ofs ty r] is a memory load at offset [ofs * 4] + relative to the pointer found at offset 0 from the stack pointer. + The semantics maintain a linked structure of activation records, + 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 +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 +by the Asm code generated by [Asmgen] to save the return address into +the caller at the beginning of a function, then restore it and jump to +it at the end of a function. The Mach concrete semantics does not +attach any particular meaning to the pointer stored in this reserved +location, but makes sure that it is preserved during execution of a +function. The [return_address_offset] predicate from module +[Asmgenretaddr] is used to guess the value of the return address that +the Asm code generated later will store in the reserved location. +*) + +Definition chunk_of_type (ty: typ) := + match ty with Tint => Mint32 | Tfloat => Mfloat64 end. + +Definition load_stack (m: mem) (sp: val) (ty: typ) (ofs: int) := + Mem.loadv (chunk_of_type ty) m (Val.add sp (Vint ofs)). + +Definition store_stack (m: mem) (sp: val) (ty: typ) (ofs: int) (v: val) := + Mem.storev (chunk_of_type ty) m (Val.add sp (Vint ofs)) v. + +(** Extract the values of the arguments of an external call. *) + +Inductive extcall_arg: regset -> mem -> val -> loc -> val -> Prop := + | extcall_arg_reg: forall rs m sp r, + extcall_arg rs m sp (R r) (rs r) + | extcall_arg_stack: forall rs m sp ofs ty v, + load_stack m sp ty (Int.repr (Stacklayout.fe_ofs_arg + 4 * ofs)) = Some v -> + extcall_arg rs m sp (S (Outgoing ofs ty)) v. + +Inductive extcall_args: regset -> mem -> val -> list loc -> list val -> Prop := + | extcall_args_nil: forall rs m sp, + extcall_args rs m sp nil nil + | extcall_args_cons: forall rs m sp l1 ll v1 vl, + extcall_arg rs m sp l1 v1 -> extcall_args rs m sp ll vl -> + extcall_args rs m sp (l1 :: ll) (v1 :: vl). + +Definition extcall_arguments + (rs: regset) (m: mem) (sp: val) (sg: signature) (args: list val) : Prop := + extcall_args rs m sp (loc_arguments sg) args. + +(** Mach execution states. *) + +Inductive stackframe: Type := + | Stackframe: + forall (f: block) (**r pointer to calling function *) + (sp: val) (**r stack pointer in calling function *) + (retaddr: val) (**r Asm return address in calling function *) + (c: code), (**r program point in calling function *) + stackframe. + +Inductive state: Type := + | State: + forall (stack: list stackframe) (**r call stack *) + (f: block) (**r pointer to current function *) + (sp: val) (**r stack pointer *) + (c: code) (**r current program point *) + (rs: regset) (**r register state *) + (m: mem), (**r memory state *) + state + | Callstate: + forall (stack: list stackframe) (**r call stack *) + (f: block) (**r pointer to 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. + +Definition parent_sp (s: list stackframe) : val := + match s with + | nil => Vptr Mem.nullptr Int.zero + | Stackframe f sp ra c :: s' => sp + end. + +Definition parent_ra (s: list stackframe) : val := + match s with + | nil => Vzero + | Stackframe f sp ra c :: s' => ra + end. + +Section RELSEM. + +Variable ge: genv. + +Inductive step: state -> trace -> state -> Prop := + | exec_Mlabel: + forall s f sp lbl c rs m, + step (State s f sp (Mlabel lbl :: c) rs m) + E0 (State s f sp c rs m) + | exec_Mgetstack: + forall s f sp ofs ty dst c rs m v, + load_stack m sp ty ofs = Some v -> + step (State s f sp (Mgetstack ofs ty dst :: c) rs m) + E0 (State s f sp c (rs#dst <- v) m) + | exec_Msetstack: + forall s f sp src ofs ty c rs m m', + store_stack m sp ty ofs (rs src) = Some m' -> + step (State s f sp (Msetstack src ofs ty :: c) rs m) + E0 (State s f sp c rs m') + | exec_Mgetparam: + forall s fb f sp ofs ty dst c rs m v, + 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 -> + step (State s fb sp (Mgetparam ofs ty dst :: c) rs m) + E0 (State s fb sp c (rs # IT1 <- Vundef # dst <- v) m) + | exec_Mop: + forall s f sp op args res c rs m v, + eval_operation ge sp op rs##args m = Some v -> + step (State s f sp (Mop op args res :: c) rs m) + E0 (State s f sp c ((undef_op op rs)#res <- v) m) + | exec_Mload: + forall s f sp chunk addr args dst c rs 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 m) + E0 (State s f sp c ((undef_temps rs)#dst <- v) m) + | exec_Mstore: + forall s f sp chunk addr args src c rs 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 m) + E0 (State s f sp c (undef_temps rs) m') + | exec_Mcall: + forall s fb sp sig ros c rs m f f' ra, + find_function_ptr ge ros rs = Some f' -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> + Asmgenretaddr.return_address_offset f c ra -> + step (State s fb sp (Mcall sig ros :: c) rs m) + E0 (Callstate (Stackframe fb sp (Vptr fb ra) c :: s) + f' rs m) + | exec_Mtailcall: + forall s fb stk soff sig ros c rs m f f' m', + find_function_ptr ge ros rs = Some f' -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> + load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) -> + load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) -> + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> + step (State s fb (Vptr stk soff) (Mtailcall sig ros :: c) rs m) + E0 (Callstate s f' rs m') + | exec_Mbuiltin: + forall s f sp rs 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 m) + t (State s f sp b ((undef_temps rs)#res <- v) m') + | exec_Mgoto: + forall s fb f sp lbl c rs m c', + Genv.find_funct_ptr ge fb = Some (Internal f) -> + find_label lbl f.(fn_code) = Some c' -> + step (State s fb sp (Mgoto lbl :: c) rs m) + E0 (State s fb sp c' rs m) + | exec_Mcond_true: + forall s fb f sp cond args lbl c rs m c', + eval_condition cond rs##args m = Some true -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> + find_label lbl f.(fn_code) = Some c' -> + step (State s fb sp (Mcond cond args lbl :: c) rs m) + E0 (State s fb sp c' (undef_temps rs) m) + | exec_Mcond_false: + forall s f sp cond args lbl c rs m, + eval_condition cond rs##args m = Some false -> + step (State s f sp (Mcond cond args lbl :: c) rs m) + E0 (State s f sp c (undef_temps rs) m) + | exec_Mjumptable: + forall s fb f sp arg tbl c rs m n lbl c', + rs arg = Vint n -> + list_nth_z tbl (Int.unsigned n) = Some lbl -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> + find_label lbl f.(fn_code) = Some c' -> + step (State s fb sp (Mjumptable arg tbl :: c) rs m) + E0 (State s fb sp c' (undef_temps rs) m) + | exec_Mreturn: + forall s fb stk soff c rs m f m', + Genv.find_funct_ptr ge fb = Some (Internal f) -> + load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) -> + load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) -> + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> + step (State s fb (Vptr stk soff) (Mreturn :: c) rs m) + E0 (Returnstate s rs m') + | exec_function_internal: + forall s fb rs m f m1 m2 m3 stk, + Genv.find_funct_ptr ge fb = Some (Internal f) -> + Mem.alloc m 0 f.(fn_stacksize) = (m1, stk) -> + 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 -> + step (Callstate s fb rs m) + E0 (State s fb sp f.(fn_code) (undef_temps rs) m3) + | exec_function_external: + forall s fb rs m t rs' ef args res m', + Genv.find_funct_ptr ge fb = Some (External ef) -> + external_call ef ge args m t res m' -> + extcall_arguments rs m (parent_sp s) (ef_sig ef) args -> + rs' = (rs#(loc_result (ef_sig ef)) <- res) -> + step (Callstate s fb rs m) + t (Returnstate s rs' m') + | exec_return: + forall s f sp ra c rs m, + step (Returnstate (Stackframe f sp ra c :: s) rs m) + E0 (State s f sp c rs m). + +End RELSEM. + +Inductive initial_state (p: program): state -> Prop := + | initial_state_intro: forall fb m0, + let ge := Genv.globalenv p in + Genv.init_mem p = Some m0 -> + Genv.find_symbol ge p.(prog_main) = Some fb -> + initial_state p (Callstate nil fb (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/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.
  • Mach: like Linear, with a more concrete view of the activation record.
    -See also: Machabstr abstract semantics for Mach.
    -See also: Machconcr concrete semantics for Mach. +See also: Machabstr operational semantics for Mach.
  • Asm: abstract syntax for PowerPC assembly code. 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. -- cgit v1.2.3