From 8a07279be78b9e504d0ea304bca72c49fdad0b37 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 17 Oct 2007 08:55:24 +0000 Subject: Utilisation d'une monade avec types dependants pour garder trace des proprietes state_incr git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@419 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/RTLgen.v | 190 ++++++++++++++++++++++++++++++++++++++++++------------- 1 file changed, 146 insertions(+), 44 deletions(-) (limited to 'backend/RTLgen.v') diff --git a/backend/RTLgen.v b/backend/RTLgen.v index 2fe13e5..52a6c8a 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -40,6 +40,41 @@ Record state: Set := mkstate { st_wf: forall (pc: positive), Plt pc st_nextnode \/ st_code!pc = None }. +(** Operations over the global state satisfy a crucial monotonicity property: + nodes are only added to the CFG, but are never removed nor their + instructions are changed; similarly, fresh nodes and fresh registers + are only consumed, but never reused. This property is captured by + the following predicate over states, which we show is a partial + order. *) + +Inductive state_incr: state -> state -> Prop := + state_incr_intro: + forall (s1 s2: state), + Ple s1.(st_nextnode) s2.(st_nextnode) -> + Ple s1.(st_nextreg) s2.(st_nextreg) -> + (forall pc, Plt pc s1.(st_nextnode) -> s2.(st_code)!pc = s1.(st_code)!pc) -> + state_incr s1 s2. + +Lemma state_incr_refl: + forall s, state_incr s s. +Proof. + intros. apply state_incr_intro. + apply Ple_refl. apply Ple_refl. intros; auto. +Qed. +Hint Resolve state_incr_refl: rtlg. + +Lemma state_incr_trans: + forall s1 s2 s3, state_incr s1 s2 -> state_incr s2 s3 -> state_incr s1 s3. +Proof. + intros. inversion H. inversion H0. apply state_incr_intro. + apply Ple_trans with (st_nextnode s2); assumption. + apply Ple_trans with (st_nextreg s2); assumption. + intros. transitivity (s2.(st_code)!pc). + apply H8. apply Plt_Ple_trans with s1.(st_nextnode); auto. + apply H3; auto. +Qed. +Hint Resolve state_incr_trans: rtlg. + (** ** The state and error monad *) (** The translation functions can fail to produce RTL code, for instance @@ -50,36 +85,52 @@ Record state: Set := mkstate { to modify the global state. These luxuries are not available in Coq, however. Instead, we use a monadic encoding of the translation: translation functions take the current global state as argument, - and return either [Error msg] to denote an error, or [OK r s] to denote - success. [s] is the modified state, and [r] the result value of the - translation function. In the error case, [msg] is an error message - (see modules [Errors]) describing the problem. + and return either [Error msg] to denote an error, + or [OK r s incr] to denote success. [s] is the modified state, [r] + the result value of the translation function. and [incr] a proof + that the final state is in the [state_incr] relation with the + initial state. In the error case, [msg] is an error message (see + modules [Errors]) describing the problem. We now define this monadic encoding -- the ``state and error'' monad -- as well as convenient syntax to express monadic computations. *) -Set Implicit Arguments. +Inductive res (A: Set) (s: state): Set := + | Error: Errors.errmsg -> res A s + | OK: A -> forall (s': state), state_incr s s' -> res A s. + +Implicit Arguments OK [A s]. +Implicit Arguments Error [A s]. + +Definition mon (A: Set) : Set := forall (s: state), res A s. -Inductive res (A: Set) : Set := - | Error: Errors.errmsg -> res A - | OK: A -> state -> res A. +Definition ret (A: Set) (x: A) : mon A := + fun (s: state) => OK x s (state_incr_refl s). -Definition mon (A: Set) : Set := state -> res A. +Implicit Arguments ret [A]. -Definition ret (A: Set) (x: A) : mon A := fun (s: state) => OK x s. +Definition error (A: Set) (msg: Errors.errmsg) : mon A := fun (s: state) => Error msg. -Definition error (A: Set) (msg: Errors.errmsg) : mon A := fun (s: state) => Error A msg. +Implicit Arguments error [A]. Definition bind (A B: Set) (f: mon A) (g: A -> mon B) : mon B := fun (s: state) => match f s with - | Error msg => Error B msg - | OK a s' => g a s' + | Error msg => Error msg + | OK a s' i => + match g a s' with + | Error msg => Error msg + | OK b s'' i' => OK b s'' (state_incr_trans s s' s'' i i') + end end. +Implicit Arguments bind [A B]. + Definition bind2 (A B C: Set) (f: mon (A * B)) (g: A -> B -> mon C) : mon C := bind f (fun xy => g (fst xy) (snd xy)). +Implicit Arguments bind2 [A B C]. + Notation "'do' X <- A ; B" := (bind A (fun X => B)) (at level 200, X ident, A at level 100, B at level 200). Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B)) @@ -89,7 +140,7 @@ Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B)) (** The initial state (empty CFG). *) -Lemma init_state_wf: +Remark init_state_wf: forall pc, Plt pc 1%positive \/ (PTree.empty instruction)!pc = None. Proof. intros; right; apply PTree.gempty. Qed. @@ -99,7 +150,7 @@ Definition init_state : state := (** Adding a node with the given instruction to the CFG. Return the label of the new node. *) -Lemma add_instr_wf: +Remark add_instr_wf: forall s i pc, let n := s.(st_nextnode) in Plt pc (Psucc n) \/ (PTree.set n i s.(st_code))!pc = None. @@ -112,6 +163,20 @@ Proof. right; assumption. Qed. +Remark add_instr_incr: + forall s i, + let n := s.(st_nextnode) in + state_incr s (mkstate s.(st_nextreg) + (Psucc n) + (PTree.set n i s.(st_code)) + (add_instr_wf s i)). +Proof. + constructor; simpl. + apply Ple_succ. + apply Ple_refl. + intros. apply PTree.gso. apply Plt_ne; auto. +Qed. + Definition add_instr (i: instruction) : mon node := fun s => let n := s.(st_nextnode) in @@ -119,13 +184,14 @@ Definition add_instr (i: instruction) : mon node := (mkstate s.(st_nextreg) (Psucc n) (PTree.set n i s.(st_code)) - (add_instr_wf s i)). + (add_instr_wf s i)) + (add_instr_incr s i). (** [add_instr] can be decomposed in two steps: reserving a fresh CFG node, and filling it later with an instruction. This is needed to compile loops. *) -Lemma reserve_instr_wf: +Remark reserve_instr_wf: forall s pc, Plt pc (Psucc s.(st_nextnode)) \/ s.(st_code)!pc = None. Proof. @@ -134,13 +200,14 @@ Proof. right; auto. Qed. -Definition reserve_instr : mon node := - fun s => - let n := s.(st_nextnode) in - OK n (mkstate s.(st_nextreg) (Psucc n) s.(st_code) - (reserve_instr_wf s)). +Definition reserve_instr (s: state): (node * state)%type := + let n := s.(st_nextnode) in + (n, mkstate s.(st_nextreg) + (Psucc n) + s.(st_code) + (reserve_instr_wf s)). -Lemma update_instr_wf: +Remark update_instr_wf: forall s n i, Plt n s.(st_nextnode) -> forall pc, @@ -152,24 +219,62 @@ Proof. rewrite PTree.gso; auto. exact (st_wf s pc). Qed. -Definition update_instr (n: node) (i: instruction) : mon unit := - fun s => - match plt n s.(st_nextnode) with - | left PEQ => - OK tt (mkstate s.(st_nextreg) s.(st_nextnode) - (PTree.set n i s.(st_code)) - (@update_instr_wf s n i PEQ)) - | right _ => - Error unit (Errors.msg "RTLgen.update_instr") +Definition update_instr (n: node) (i: instruction) (s: state) : state := + match plt n s.(st_nextnode) with + | left PLT => + mkstate s.(st_nextreg) + s.(st_nextnode) + (PTree.set n i s.(st_code)) + (update_instr_wf s n i PLT) + | right _ => s (* never happens *) + end. + +Remark add_loop_incr: + forall s1 s3 i, + let n := fst (reserve_instr s1) in + let s2 := snd (reserve_instr s1) in + state_incr s2 s3 -> + state_incr s1 (update_instr n i s3). +Proof. + intros. inv H. unfold update_instr. destruct (plt n (st_nextnode s3)). + constructor; simpl. + apply Ple_trans with (st_nextnode s2). + unfold s2; simpl. apply Ple_succ. auto. + assumption. + intros. rewrite PTree.gso. rewrite H2. reflexivity. + unfold s2; simpl. apply Plt_trans_succ. auto. + apply Plt_ne. assumption. + elim n0. apply Plt_Ple_trans with (st_nextnode s2). + unfold n, s2; simpl; apply Plt_succ. auto. +Qed. + +Definition add_loop (body: node -> mon node) : mon node := + fun (s1: state) => + let nloop := fst(reserve_instr s1) in + let s2 := snd(reserve_instr s1) in + match body nloop s2 with + | Error msg => Error msg + | OK nbody s3 i => + OK nbody (update_instr nloop (Inop nbody) s3) + (add_loop_incr s1 s3 (Inop nbody) i) end. (** Generate a fresh RTL register. *) +Remark new_reg_incr: + forall s, + state_incr s (mkstate (Psucc s.(st_nextreg)) + s.(st_nextnode) s.(st_code) s.(st_wf)). +Proof. + constructor; simpl. apply Ple_refl. apply Ple_succ. auto. +Qed. + Definition new_reg : mon reg := fun s => OK s.(st_nextreg) (mkstate (Psucc s.(st_nextreg)) - s.(st_nextnode) s.(st_code) s.(st_wf)). + s.(st_nextnode) s.(st_code) s.(st_wf)) + (new_reg_incr s). (** ** Operations on mappings *) @@ -193,7 +298,7 @@ Fixpoint add_vars (map: mapping) (names: list ident) Definition find_var (map: mapping) (name: ident) : mon reg := match PTree.get name map.(map_vars) with - | None => error reg (Errors.MSG "RTLgen: unbound variable " :: Errors.CTX name :: nil) + | None => error (Errors.MSG "RTLgen: unbound variable " :: Errors.CTX name :: nil) | Some r => ret r end. @@ -202,7 +307,7 @@ Definition add_letvar (map: mapping) (r: reg) : mapping := Definition find_letvar (map: mapping) (idx: nat) : mon reg := match List.nth_error map.(map_letvars) idx with - | None => error reg (Errors.msg "RTLgen: unbound let variable") + | None => error (Errors.msg "RTLgen: unbound let variable") | Some r => ret r end. @@ -311,7 +416,7 @@ with transl_exprlist (map: mapping) (al: exprlist) (rl: list reg) (nd: node) | Econs b bs, r :: rs => do no <- transl_exprlist map bs rs nd; transl_expr map b r no | _, _ => - error node (Errors.msg "RTLgen.transl_exprlist") + error (Errors.msg "RTLgen.transl_exprlist") end. (** Generation of code for variable assignments. *) @@ -344,7 +449,7 @@ Parameter compile_switch: nat -> table -> comptree. Definition transl_exit (nexits: list node) (n: nat) : mon node := match nth_error nexits n with - | None => error node (Errors.msg "RTLgen: wrong exit") + | None => error (Errors.msg "RTLgen: wrong exit") | Some ne => ret ne end. @@ -415,10 +520,7 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node) do nfalse <- transl_stmt map sfalse nd nexits nret rret; transl_condition map a ntrue nfalse | Sloop sbody => - do nloop <- reserve_instr; - do nbody <- transl_stmt map sbody nloop nexits nret rret; - do x <- update_instr nloop (Inop nbody); - ret nbody + add_loop (fun nloop => transl_stmt map sbody nloop nexits nret rret) | Sblock sbody => transl_stmt map sbody nd (nd :: nexits) nret rret | Sexit n => @@ -430,12 +532,12 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node) do ns <- transl_switch r nexits t; transl_expr map a r ns) else - error node (Errors.msg "RTLgen: wrong switch") + error (Errors.msg "RTLgen: wrong switch") | Sreturn opt_a => match opt_a, rret with | None, None => ret nret | Some a, Some r => transl_expr map a r nret - | _, _ => error node (Errors.msg "RTLgen: type mismatch on return") + | _, _ => error (Errors.msg "RTLgen: type mismatch on return") end | Stailcall sig b cl => do rf <- alloc_reg map b; @@ -465,7 +567,7 @@ Definition transl_fun (f: CminorSel.function) : mon (node * list reg) := Definition transl_function (f: CminorSel.function) : Errors.res RTL.function := match transl_fun f init_state with | Error msg => Errors.Error msg - | OK (nentry, rparams) s => + | OK (nentry, rparams) s i => Errors.OK (RTL.mkfunction f.(CminorSel.fn_sig) rparams -- cgit v1.2.3