From 73729d23ac13275c0d28d23bc1b1f6056104e5d9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 4 Sep 2006 15:08:29 +0000 Subject: Fusion de la branche "traces": - Ajout de traces d'evenements d'E/S dans les semantiques - Ajout constructions switch et allocation dynamique - Initialisation des variables globales - Portage Coq 8.1 beta Debut d'integration du front-end C: - Traduction Clight -> Csharpminor dans cfrontend/ - Modifications de Csharpminor et Globalenvs en consequence. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@72 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/RTL.v | 123 +++++++++++++++++++++++++++++++++++----------------------- 1 file changed, 75 insertions(+), 48 deletions(-) (limited to 'backend/RTL.v') diff --git a/backend/RTL.v b/backend/RTL.v index ac9a4159..4a3f8e8c 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -4,12 +4,13 @@ after Cminor. *) -Require Import Relations. +(*Require Import Relations.*) Require Import Coqlib. Require Import Maps. Require Import AST. Require Import Integers. Require Import Values. +Require Import Events. Require Import Mem. Require Import Globalenvs. Require Import Op. @@ -54,6 +55,10 @@ Inductive instruction: Set := function name), giving it the values of registers [args] as arguments. It stores the return value in [dest] and branches to [succ]. *) + | Ialloc: reg -> reg -> node -> instruction + (** [Ialloc arg dest succ] allocates a fresh block of size + the contents of register [arg], stores a pointer to this + block in [dest], and branches to [succ]. *) | Icond: condition -> list reg -> node -> node -> instruction (** [Icond cond args ifso ifnot] evaluates the boolean condition [cond] over the values of registers [args]. If the condition @@ -85,11 +90,19 @@ Record function: Set := mkfunction { in the CFG. [fn_code_wf] asserts that all instructions of the function have nodes no greater than [fn_nextpc]. *) -Definition program := AST.program function. +Definition fundef := AST.fundef function. + +Definition program := AST.program fundef. + +Definition funsig (fd: fundef) := + match fd with + | Internal f => f.(fn_sig) + | External ef => ef.(ef_sig) + end. (** * Operational semantics *) -Definition genv := Genv.t function. +Definition genv := Genv.t fundef. Definition regset := Regmap.t val. Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset := @@ -102,7 +115,8 @@ Section RELSEM. Variable ge: genv. -Definition find_function (ros: reg + ident) (rs: regset) : option function := +Definition find_function + (ros: reg + ident) (rs: regset) : option fundef := match ros with | inl r => Genv.find_funct ge rs#r | inr symb => @@ -132,66 +146,73 @@ Definition find_function (ros: reg + ident) (rs: regset) : option function := and memory state [m]. The final state is [pc'], [rs'] and [m']. *) Inductive exec_instr: code -> val -> - node -> regset -> mem -> + node -> regset -> mem -> trace -> node -> regset -> mem -> Prop := | exec_Inop: forall c sp pc rs m pc', c!pc = Some(Inop pc') -> - exec_instr c sp pc rs m pc' rs m + exec_instr c sp pc rs m E0 pc' rs m | exec_Iop: forall c sp pc rs m op args res pc' v, c!pc = Some(Iop op args res pc') -> eval_operation ge sp op rs##args = Some v -> - exec_instr c sp pc rs m pc' (rs#res <- v) m + exec_instr c sp pc rs m E0 pc' (rs#res <- v) m | exec_Iload: forall c sp pc rs m chunk addr args dst pc' a v, c!pc = Some(Iload chunk addr args dst pc') -> eval_addressing ge sp addr rs##args = Some a -> Mem.loadv chunk m a = Some v -> - exec_instr c sp pc rs m pc' (rs#dst <- v) m + exec_instr c sp pc rs m E0 pc' (rs#dst <- v) m | exec_Istore: forall c sp pc rs m chunk addr args src pc' a m', c!pc = Some(Istore chunk addr args src pc') -> eval_addressing ge sp addr rs##args = Some a -> Mem.storev chunk m a rs#src = Some m' -> - exec_instr c sp pc rs m pc' rs m' + exec_instr c sp pc rs m E0 pc' rs m' | exec_Icall: - forall c sp pc rs m sig ros args res pc' f vres m', + forall c sp pc rs m sig ros args res pc' f vres m' t, c!pc = Some(Icall sig ros args res pc') -> find_function ros rs = Some f -> - sig = f.(fn_sig) -> - exec_function f rs##args m vres m' -> - exec_instr c sp pc rs m pc' (rs#res <- vres) m' + funsig f = sig -> + exec_function f rs##args m t vres m' -> + exec_instr c sp pc rs m t pc' (rs#res <- vres) m' + | exec_Ialloc: + forall c sp pc rs m pc' arg res sz m' b, + c!pc = Some(Ialloc arg res pc') -> + rs#arg = Vint sz -> + Mem.alloc m 0 (Int.signed sz) = (m', b) -> + exec_instr c sp pc rs m E0 pc' (rs#res <- (Vptr b Int.zero)) m' | exec_Icond_true: forall c sp pc rs m cond args ifso ifnot, c!pc = Some(Icond cond args ifso ifnot) -> eval_condition cond rs##args = Some true -> - exec_instr c sp pc rs m ifso rs m + exec_instr c sp pc rs m E0 ifso rs m | exec_Icond_false: forall c sp pc rs m cond args ifso ifnot, c!pc = Some(Icond cond args ifso ifnot) -> eval_condition cond rs##args = Some false -> - exec_instr c sp pc rs m ifnot rs m + exec_instr c sp pc rs m E0 ifnot rs m (** [exec_instrs ge c sp pc rs m pc' rs' m'] is the reflexive transitive closure of [exec_instr]. It corresponds to the execution of zero, one or finitely many transitions. *) with exec_instrs: code -> val -> - node -> regset -> mem -> + node -> regset -> mem -> trace -> node -> regset -> mem -> Prop := | exec_refl: forall c sp pc rs m, - exec_instrs c sp pc rs m pc rs m + exec_instrs c sp pc rs m E0 pc rs m | exec_one: - forall c sp pc rs m pc' rs' m', - exec_instr c sp pc rs m pc' rs' m' -> - exec_instrs c sp pc rs m pc' rs' m' + forall c sp pc rs m t pc' rs' m', + exec_instr c sp pc rs m t pc' rs' m' -> + exec_instrs c sp pc rs m t pc' rs' m' | exec_trans: - forall c sp pc1 rs1 m1 pc2 rs2 m2 pc3 rs3 m3, - exec_instrs c sp pc1 rs1 m1 pc2 rs2 m2 -> - exec_instrs c sp pc2 rs2 m2 pc3 rs3 m3 -> - exec_instrs c sp pc1 rs1 m1 pc3 rs3 m3 + forall c sp pc1 rs1 m1 t1 pc2 rs2 m2 t2 pc3 rs3 m3 t3, + exec_instrs c sp pc1 rs1 m1 t1 pc2 rs2 m2 -> + exec_instrs c sp pc2 rs2 m2 t2 pc3 rs3 m3 -> + t3 = t1 ** t2 -> + exec_instrs c sp pc1 rs1 m1 t3 pc3 rs3 m3 (** [exec_function ge f args m res m'] executes a function application. [f] is the called function, [args] the values of its arguments, @@ -205,17 +226,21 @@ with exec_instrs: code -> val -> (Non-parameter registers are initialized to [Vundef].) Before returning, the stack activation block is freed. *) -with exec_function: function -> list val -> mem -> - val -> mem -> Prop := - | exec_funct: - forall f m m1 stk args pc rs m2 or vres, +with exec_function: fundef -> list val -> mem -> trace -> + val -> mem -> Prop := + | exec_funct_internal: + forall f m m1 stk args t pc rs m2 or vres, Mem.alloc m 0 f.(fn_stacksize) = (m1, stk) -> - exec_instrs f.(fn_code) (Vptr stk Int.zero) + exec_instrs f.(fn_code) (Vptr stk Int.zero) f.(fn_entrypoint) (init_regs args f.(fn_params)) m1 - pc rs m2 -> + t pc rs m2 -> f.(fn_code)!pc = Some(Ireturn or) -> vres = regmap_optget or Vundef rs -> - exec_function f args m vres (Mem.free m2 stk). + exec_function (Internal f) args m t vres (Mem.free m2 stk) + | exec_funct_external: + forall ef args m t res, + event_match ef args t res -> + exec_function (External ef) args m t res m. Scheme exec_instr_ind_3 := Minimality for exec_instr Sort Prop with exec_instrs_ind_3 := Minimality for exec_instrs Sort Prop @@ -224,12 +249,13 @@ Scheme exec_instr_ind_3 := Minimality for exec_instr Sort Prop (** Some derived execution rules. *) Lemma exec_step: - forall c sp pc1 rs1 m1 pc2 rs2 m2 pc3 rs3 m3, - exec_instr c sp pc1 rs1 m1 pc2 rs2 m2 -> - exec_instrs c sp pc2 rs2 m2 pc3 rs3 m3 -> - exec_instrs c sp pc1 rs1 m1 pc3 rs3 m3. + forall c sp pc1 rs1 m1 t1 pc2 rs2 m2 t2 pc3 rs3 m3 t3, + exec_instr c sp pc1 rs1 m1 t1 pc2 rs2 m2 -> + exec_instrs c sp pc2 rs2 m2 t2 pc3 rs3 m3 -> + t3 = t1 ** t2 -> + exec_instrs c sp pc1 rs1 m1 t3 pc3 rs3 m3. Proof. - intros. eapply exec_trans. apply exec_one. eauto. eauto. + intros. eapply exec_trans. apply exec_one. eauto. eauto. auto. Qed. Lemma exec_Iop': @@ -237,7 +263,7 @@ Lemma exec_Iop': c!pc = Some(Iop op args res pc') -> eval_operation ge sp op rs##args = Some v -> rs' = (rs#res <- v) -> - exec_instr c sp pc rs m pc' rs' m. + exec_instr c sp pc rs m E0 pc' rs' m. Proof. intros. subst rs'. eapply exec_Iop; eauto. Qed. @@ -248,7 +274,7 @@ Lemma exec_Iload': eval_addressing ge sp addr rs##args = Some a -> Mem.loadv chunk m a = Some v -> rs' = (rs#dst <- v) -> - exec_instr c sp pc rs m pc' rs' m. + exec_instr c sp pc rs m E0 pc' rs' m. Proof. intros. subst rs'. eapply exec_Iload; eauto. Qed. @@ -257,16 +283,16 @@ Qed. is defined in the CFG. *) Lemma exec_instr_present: - forall c sp pc rs m pc' rs' m', - exec_instr c sp pc rs m pc' rs' m' -> + forall c sp pc rs m t pc' rs' m', + exec_instr c sp pc rs m t pc' rs' m' -> c!pc <> None. Proof. induction 1; congruence. Qed. Lemma exec_instrs_present: - forall c sp pc rs m pc' rs' m', - exec_instrs c sp pc rs m pc' rs' m' -> + forall c sp pc rs m t pc' rs' m', + exec_instrs c sp pc rs m t pc' rs' m' -> c!pc' <> None -> c!pc <> None. Proof. induction 1; intros. @@ -280,14 +306,14 @@ End RELSEM. (** Execution of whole programs. As in Cminor, we call the ``main'' function with no arguments and observe its return value. *) -Definition exec_program (p: program) (r: val) : Prop := +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 m, Genv.find_symbol ge p.(prog_main) = Some b /\ Genv.find_funct_ptr ge b = Some f /\ - f.(fn_sig) = mksignature nil (Some Tint) /\ - exec_function ge f nil m0 r m. + funsig f = mksignature nil (Some Tint) /\ + exec_function ge f nil m0 t r m. (** * Operations on RTL abstract syntax *) @@ -304,14 +330,15 @@ Definition successors (f: function) (pc: node) : list node := | Iload chunk addr args dst s => s :: nil | Istore chunk addr args src s => s :: nil | Icall sig ros args res s => s :: nil + | Ialloc arg res s => s :: nil | Icond cond args ifso ifnot => ifso :: ifnot :: nil | Ireturn optarg => nil end end. Lemma successors_correct: - forall ge f sp pc rs m pc' rs' m', - exec_instr ge f.(fn_code) sp pc rs m pc' rs' m' -> + forall ge f sp pc rs m t pc' rs' m', + exec_instr ge f.(fn_code) sp pc rs m t pc' rs' m' -> In pc' (successors f pc). Proof. intros ge f. unfold successors. generalize (fn_code f). @@ -345,5 +372,5 @@ Definition transf_function (f: function) : function := f.(fn_entrypoint) f.(fn_nextpc) (transf_code_wf f.(fn_code) f.(fn_nextpc) f.(fn_code_wf)). - + End TRANSF. -- cgit