From a15858a0a8fcea82db02fe8c9bd2ed912210419f Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 18 Aug 2010 09:06:55 +0000 Subject: Merge of branches/full-expr-4: - Csyntax, Csem: source C language has side-effects within expressions, performs implicit casts, and has nondeterministic reduction semantics for expressions - Cstrategy: deterministic red. sem. for the above - Clight: the previous source C language, with pure expressions. Added: temporary variables + implicit casts. - New pass SimplExpr to pull side-effects out of expressions (previously done in untrusted Caml code in cparser/) - Csharpminor: added temporary variables to match Clight. - Cminorgen: adapted, removed cast optimization (moved to back-end) - CastOptim: RTL-level optimization of casts - cparser: transformations Bitfields, StructByValue and StructAssign now work on non-simplified expressions - Added pretty-printers for several intermediate languages, and matching -dxxx command-line flags. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1467 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/RTLgenspec.v | 104 +++++++++++++++++++-------------------------------- 1 file changed, 38 insertions(+), 66 deletions(-) (limited to 'backend/RTLgenspec.v') diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index 0b18a99..22a1e79 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -483,6 +483,27 @@ Proof. intros [A|B]. auto. right; eauto with rtlg. Qed. +Lemma alloc_optreg_valid: + forall dest s1 s2 map r i, + map_valid map s1 -> + alloc_optreg map dest s1 = OK r s2 i -> reg_valid r s2. +Proof. + intros until r. unfold alloc_reg. + case dest; eauto with rtlg. +Qed. +Hint Resolve alloc_optreg_valid: rtlg. + +Lemma alloc_optreg_fresh_or_in_map: + forall map dest s r s' i, + map_valid map s -> + alloc_optreg map dest s = OK r s' i -> + reg_in_map map r \/ reg_fresh r s. +Proof. + intros until s'. unfold alloc_optreg. destruct dest; intros. + left; eauto with rtlg. + right; eauto with rtlg. +Qed. + (** A register is an adequate target for holding the value of an expression if - either the register is associated with a Cminor let-bound variable @@ -736,19 +757,6 @@ with tr_exprlist (c: code): tr_exprlist c map (r1 :: pr) al n1 nd rl -> tr_exprlist c map pr (Econs a1 al) ns nd (r1 :: rl). -(** Auxiliary for the compilation of variable assignments. *) - -Definition tr_store_var (c: code) (map: mapping) - (rs: reg) (id: ident) (ns nd: node): Prop := - exists rv, map.(map_vars)!id = Some rv /\ tr_move c ns rs nd rv. - -Definition tr_store_optvar (c: code) (map: mapping) - (rs: reg) (optid: option ident) (ns nd: node): Prop := - match optid with - | None => ns = nd - | Some id => tr_store_var c map rs id ns nd - end. - (** Auxiliary for the compilation of [switch] statements. *) Definition tr_jumptable (nexits: list node) (tbl: list nat) (ttbl: list node) : Prop := @@ -804,23 +812,21 @@ Inductive tr_stmt (c: code) (map: mapping): tr_expr c map rl b n1 n2 rd None -> c!n2 = Some (Istore chunk addr rl rd nd) -> tr_stmt c map (Sstore chunk addr al b) ns nd nexits ngoto nret rret - | tr_Scall: forall optid sig b cl ns nd nexits ngoto nret rret rd n1 rf n2 n3 rargs, + | tr_Scall: forall optid sig b cl ns nd nexits ngoto nret rret rd n1 rf n2 rargs, tr_expr c map nil b ns n1 rf None -> tr_exprlist c map (rf :: nil) cl n1 n2 rargs -> - c!n2 = Some (Icall sig (inl _ rf) rargs rd n3) -> - tr_store_optvar c map rd optid n3 nd -> - ~reg_in_map map rd -> + c!n2 = Some (Icall sig (inl _ rf) rargs rd nd) -> + reg_map_ok map rd optid -> tr_stmt c map (Scall optid sig b cl) ns nd nexits ngoto nret rret | tr_Stailcall: forall sig b cl ns nd nexits ngoto nret rret n1 rf n2 rargs, tr_expr c map nil b ns n1 rf None -> tr_exprlist c map (rf :: nil) cl n1 n2 rargs -> c!n2 = Some (Itailcall sig (inl _ rf) rargs) -> tr_stmt c map (Stailcall sig b cl) ns nd nexits ngoto nret rret - | tr_Sbuiltin: forall optid ef al ns nd nexits ngoto nret rret rd n1 n2 rargs, + | tr_Sbuiltin: forall optid ef al ns nd nexits ngoto nret rret rd n1 rargs, tr_exprlist c map nil al ns n1 rargs -> - c!n1 = Some (Ibuiltin ef rargs rd n2) -> - tr_store_optvar c map rd optid n2 nd -> - ~reg_in_map map rd -> + c!n1 = Some (Ibuiltin ef rargs rd nd) -> + reg_map_ok map rd optid -> tr_stmt c map (Sbuiltin optid ef al) ns nd nexits ngoto nret rret | tr_Sseq: forall s1 s2 ns nd nexits ngoto nret rret n, tr_stmt c map s2 n nd nexits ngoto nret rret -> @@ -1077,25 +1083,15 @@ Proof. monadInv EQ1. Qed. -Lemma tr_store_var_incr: - forall s1 s2, state_incr s1 s2 -> - forall map rs id ns nd, - tr_store_var s1.(st_code) map rs id ns nd -> - tr_store_var s2.(st_code) map rs id ns nd. -Proof. - intros. destruct H0 as [rv [A B]]. - econstructor; split. eauto. eapply tr_move_incr; eauto. -Qed. - -Lemma tr_store_optvar_incr: - forall s1 s2, state_incr s1 s2 -> - forall map rs optid ns nd, - tr_store_optvar s1.(st_code) map rs optid ns nd -> - tr_store_optvar s2.(st_code) map rs optid ns nd. +Lemma alloc_optreg_map_ok: + forall map optid s1 r s2 i, + map_valid map s1 -> + alloc_optreg map optid s1 = OK r s2 i -> + reg_map_ok map r optid. Proof. - intros until nd. destruct optid; simpl. - apply tr_store_var_incr; auto. - auto. + unfold alloc_optreg; intros. destruct optid. + constructor. unfold find_var in H0. destruct (map_vars map)!i0; monadInv H0. auto. + constructor. eapply new_reg_not_in_map; eauto. Qed. Lemma tr_switch_incr: @@ -1116,32 +1112,10 @@ Proof. intros s1 s2 EXT. generalize tr_expr_incr tr_condition_incr tr_exprlist_incr; intros I1 I2 I3. pose (AT := fun pc i => instr_at_incr s1 s2 pc i EXT). - pose (STV := tr_store_var_incr s1 s2 EXT). - pose (STOV := tr_store_optvar_incr s1 s2 EXT). induction 1; econstructor; eauto. eapply tr_switch_incr; eauto. Qed. -Lemma store_var_charact: - forall map rs id nd s ns s' incr, - store_var map rs id nd s = OK ns s' incr -> - tr_store_var s'.(st_code) map rs id ns nd. -Proof. - intros. monadInv H. generalize EQ. unfold find_var. - caseEq ((map_vars map)!id). 2: intros; discriminate. intros. monadInv EQ1. - exists x; split. auto. eapply add_move_charact; eauto. -Qed. - -Lemma store_optvar_charact: - forall map rs optid nd s ns s' incr, - store_optvar map rs optid nd s = OK ns s' incr -> - tr_store_optvar s'.(st_code) map rs optid ns nd. -Proof. - intros. destruct optid; simpl in H; simpl. - eapply store_var_charact; eauto. - monadInv H. auto. -Qed. - Lemma transl_exit_charact: forall nexits n s ne s' incr, transl_exit nexits n s = OK ne s' incr -> @@ -1218,15 +1192,14 @@ Proof. (* Scall *) econstructor; eauto 4 with rtlg. eapply transl_expr_charact; eauto 3 with rtlg. - apply tr_exprlist_incr with s6. auto. + apply tr_exprlist_incr with s5. auto. eapply transl_exprlist_charact; eauto 3 with rtlg. eapply alloc_regs_target_ok with (s1 := s1); eauto 3 with rtlg. apply regs_valid_cons; eauto 3 with rtlg. apply regs_valid_incr with s1; eauto 3 with rtlg. apply regs_valid_cons; eauto 3 with rtlg. apply regs_valid_incr with s2; eauto 3 with rtlg. - apply tr_store_optvar_incr with s4; auto. - eapply store_optvar_charact; eauto with rtlg. + eapply alloc_optreg_map_ok with (s1 := s2); eauto 3 with rtlg. (* Stailcall *) assert (RV: regs_valid (x :: nil) s1). apply regs_valid_cons; eauto 3 with rtlg. @@ -1237,8 +1210,7 @@ Proof. (* Sbuiltin *) econstructor; eauto 4 with rtlg. eapply transl_exprlist_charact; eauto 3 with rtlg. - apply tr_store_optvar_incr with s2; auto. - eapply store_optvar_charact; eauto with rtlg. + eapply alloc_optreg_map_ok with (s1 := s0); eauto with rtlg. (* Sseq *) econstructor. apply tr_stmt_incr with s0; auto. -- cgit v1.2.3