From 355b4abcee015c3fae9ac5653c25259e104a886c Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 4 Aug 2007 07:27:50 +0000 Subject: Fusion des modifications faites sur les branches "tailcalls" et "smallstep". En particulier: - Semantiques small-step depuis RTL jusqu'a PPC - Cminor independant du processeur - Ajout passes Selection et Reload - Ajout des langages intermediaires CminorSel et LTLin correspondants - Ajout des tailcalls depuis Cminor jusqu'a PPC git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Mach.v | 256 +++++---------------------------------------------------- 1 file changed, 22 insertions(+), 234 deletions(-) (limited to 'backend/Mach.v') diff --git a/backend/Mach.v b/backend/Mach.v index f61620d1..05805ec5 100644 --- a/backend/Mach.v +++ b/backend/Mach.v @@ -1,7 +1,8 @@ -(** The Mach intermediate language: abstract syntax and semantics. +(** The Mach intermediate language: abstract syntax. Mach is the last intermediate language before generation of assembly - code. + code. This file defines the abstract syntax for Mach; two dynamic + semantics are given in modules [Machabstr] and [Machconcr]. *) Require Import Coqlib. @@ -14,7 +15,6 @@ Require Import Events. Require Import Globalenvs. Require Import Op. Require Import Locations. -Require Conventions. (** * Abstract syntax *) @@ -30,8 +30,8 @@ Require Conventions. the caller. These instructions implement a more concrete view of the activation - record than the the [Bgetstack] and [Bsetstack] instructions of - Linear: actual offsets are used instead of abstract stack slots; the + record than the the [Lgetstack] and [Lsetstack] instructions of + Linear: actual offsets are used instead of abstract stack slots, and the distinction between the caller's frame and the callee's frame is made explicit. *) @@ -45,6 +45,7 @@ Inductive instruction: Set := | Mload: memory_chunk -> addressing -> list mreg -> mreg -> instruction | Mstore: memory_chunk -> addressing -> list mreg -> mreg -> instruction | Mcall: signature -> mreg + ident -> instruction + | Mtailcall: signature -> mreg + ident -> instruction | Malloc: instruction | Mlabel: label -> instruction | Mgoto: label -> instruction @@ -105,238 +106,25 @@ Fixpoint find_label (lbl: label) (c: code) {struct c} : option code := | i1 :: il => if is_label lbl i1 then Some il else find_label lbl il end. -(** 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. *) - -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. - -Definition align_16_top (lo hi: Z) := - Zmax 0 (((hi - lo + 15) / 16) * 16 + lo). - -Section RELSEM. - -Variable ge: genv. +Lemma find_label_incl: + forall lbl c c', find_label lbl c = Some c' -> incl c' c. +Proof. + induction c; simpl; intros. discriminate. + destruct (is_label lbl a). inv H. auto with coqlib. eauto with coqlib. +Qed. -Definition find_function (ros: mreg + ident) (rs: regset) : option fundef := +Definition find_function_ptr + (ge: genv) (ros: mreg + ident) (rs: regset) : option block := 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 + | inl r => + match rs r with + | Vptr b ofs => if Int.eq ofs Int.zero then Some b else None + | _ => None end + | inr symb => + Genv.find_symbol ge symb end. -(** 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 (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 (Conventions.loc_arguments sg) args. - -(** [exec_instr ge f sp c rs m c' rs' m'] reflects the execution of - the first instruction in the current instruction sequence [c]. - [c'] is the current instruction sequence after this execution. - [rs] and [rs'] map machine registers to values, respectively - before and after instruction execution. [m] and [m'] are the - memory states before and after. *) - -Inductive exec_instr: - function -> val -> - code -> regset -> mem -> trace -> - code -> regset -> mem -> Prop := - | exec_Mlabel: - forall f sp lbl c rs m, - exec_instr f sp - (Mlabel lbl :: c) rs m - E0 c rs m - | exec_Mgetstack: - forall f sp ofs ty dst c rs m v, - load_stack m sp ty ofs = Some v -> - exec_instr f sp - (Mgetstack ofs ty dst :: c) rs m - E0 c (rs#dst <- v) m - | exec_Msetstack: - forall f sp src ofs ty c rs m m', - store_stack m sp ty ofs (rs src) = Some m' -> - exec_instr f sp - (Msetstack src ofs ty :: c) rs m - E0 c rs m' - | exec_Mgetparam: - forall f sp parent ofs ty dst c rs m v, - load_stack m sp Tint (Int.repr 0) = Some parent -> - load_stack m parent ty ofs = Some v -> - exec_instr f sp - (Mgetparam ofs ty dst :: c) rs m - E0 c (rs#dst <- v) m - | exec_Mop: - forall f sp op args res c rs m v, - eval_operation ge sp op rs##args = Some v -> - exec_instr f sp - (Mop op args res :: c) rs m - E0 c (rs#res <- v) m - | exec_Mload: - forall 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 -> - exec_instr f sp - (Mload chunk addr args dst :: c) rs m - E0 c (rs#dst <- v) m - | exec_Mstore: - forall 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' -> - exec_instr f sp - (Mstore chunk addr args src :: c) rs m - E0 c rs m' - | exec_Mcall: - forall f sp sig ros c rs m f' t rs' m', - find_function ros rs = Some f' -> - exec_function f' sp rs m t rs' m' -> - exec_instr f sp - (Mcall sig ros :: c) rs m - t c rs' m' - | exec_Malloc: - forall f sp c rs m sz m' blk, - rs (Conventions.loc_alloc_argument) = Vint sz -> - Mem.alloc m 0 (Int.signed sz) = (m', blk) -> - exec_instr f sp - (Malloc :: c) rs m - E0 c (rs#Conventions.loc_alloc_result <- - (Vptr blk Int.zero)) m' - | exec_Mgoto: - forall f sp lbl c rs m c', - find_label lbl f.(fn_code) = Some c' -> - exec_instr f sp - (Mgoto lbl :: c) rs m - E0 c' rs m - | exec_Mcond_true: - forall f sp cond args lbl c rs m c', - eval_condition cond rs##args = Some true -> - find_label lbl f.(fn_code) = Some c' -> - exec_instr f sp - (Mcond cond args lbl :: c) rs m - E0 c' rs m - | exec_Mcond_false: - forall f sp cond args lbl c rs m, - eval_condition cond rs##args = Some false -> - exec_instr f sp - (Mcond cond args lbl :: c) rs m - E0 c rs m - -with exec_instrs: - function -> val -> - code -> regset -> mem -> trace -> - code -> regset -> mem -> Prop := - | exec_refl: - forall f sp c rs m, - exec_instrs f sp c rs m E0 c rs m - | exec_one: - forall f sp c rs m t c' rs' m', - exec_instr f sp c rs m t c' rs' m' -> - exec_instrs f sp c rs m t c' rs' m' - | exec_trans: - forall f sp c1 rs1 m1 t1 c2 rs2 m2 t2 c3 rs3 m3 t3, - exec_instrs f sp c1 rs1 m1 t1 c2 rs2 m2 -> - exec_instrs f sp c2 rs2 m2 t2 c3 rs3 m3 -> - t3 = t1 ** t2 -> - exec_instrs f sp c1 rs1 m1 t3 c3 rs3 m3 - -(** In addition to reserving the word at offset 0 in the activation - record for maintaining the linking of activation records, - we need to reserve the word at offset 12 to store the return address - into the caller. However, the return address (a pointer within - the code of the caller) is not precisely known at this point: - it will be determined only after the final translation to PowerPC - assembly code. Therefore, we simply reserve that word in the strongest - sense of the word ``reserve'': we make sure that whatever pointer - is stored there at function entry keeps the same value until the - final return instruction, and that the return value and final memory - state are the same regardless of the return address. - This is captured in the evaluation rule [exec_function] - that quantifies universally over all possible values of the return - address, and pass this value to [exec_function_body]. In other - terms, the inference rule [exec_function] has an infinity of - premises, one for each possible return address. Such infinitely - branching inference rules are uncommon in operational semantics, - but cause no difficulties in Coq. *) - -with exec_function_body: - function -> val -> val -> - regset -> mem -> trace -> regset -> mem -> Prop := - | exec_funct_body: - forall f parent ra rs m t rs' m1 m2 m3 m4 stk c, - Mem.alloc m (- f.(fn_framesize)) - (align_16_top (- f.(fn_framesize)) f.(fn_stacksize)) - = (m1, stk) -> - let sp := Vptr stk (Int.repr (-f.(fn_framesize))) in - store_stack m1 sp Tint (Int.repr 0) parent = Some m2 -> - store_stack m2 sp Tint (Int.repr 12) ra = Some m3 -> - exec_instrs f sp - f.(fn_code) rs m3 - t (Mreturn :: c) rs' m4 -> - load_stack m4 sp Tint (Int.repr 0) = Some parent -> - load_stack m4 sp Tint (Int.repr 12) = Some ra -> - exec_function_body f parent ra rs m t rs' (Mem.free m4 stk) - -with exec_function: - fundef -> val -> regset -> mem -> trace -> regset -> mem -> Prop := - | exec_funct_internal: - forall f parent rs m t rs' m', - (forall ra, - Val.has_type ra Tint -> - exec_function_body f parent ra rs m t rs' m') -> - exec_function (Internal f) parent rs m t rs' m' - | exec_funct_external: - forall ef parent args res rs1 rs2 m t, - event_match ef args t res -> - extcall_arguments rs1 m parent ef.(ef_sig) args -> - rs2 = (rs1#(Conventions.loc_result ef.(ef_sig)) <- res) -> - exec_function (External ef) parent rs1 m t rs2 m. - -Scheme exec_instr_ind4 := Minimality for exec_instr Sort Prop - with exec_instrs_ind4 := Minimality for exec_instrs Sort Prop - with exec_function_body_ind4 := Minimality for exec_function_body Sort Prop - with exec_function_ind4 := Minimality for exec_function Sort Prop. - -End RELSEM. - -Definition exec_program (p: program) (t: trace) (r: val) : Prop := - let ge := Genv.globalenv p in - let m0 := Genv.init_mem p in - exists b, exists f, exists rs, exists m, - Genv.find_symbol ge p.(prog_main) = Some b /\ - Genv.find_funct_ptr ge b = Some f /\ - exec_function ge f (Vptr Mem.nullptr Int.zero) (Regmap.init Vundef) m0 - t rs m /\ - rs R3 = r. +Definition align_16_top (lo hi: Z) := + Zmax 0 (((hi - lo + 15) / 16) * 16 + lo). -- cgit