From 74487f079dd56663f97f9731cea328931857495c Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 10 Nov 2009 12:50:57 +0000 Subject: Added support for jump tables in back end. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1171 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/RTLgenspec.v | 75 +++++++++++++++++++++++++++++++++++++++------------- 1 file changed, 56 insertions(+), 19 deletions(-) (limited to 'backend/RTLgenspec.v') diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index caf93c83..037eb3fb 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -713,22 +713,36 @@ Definition tr_store_optvar (c: code) (map: mapping) (** Auxiliary for the compilation of [switch] statements. *) +Definition tr_jumptable (nexits: list node) (tbl: list nat) (ttbl: list node) : Prop := + forall v act, + list_nth_z tbl v = Some act -> + exists n, list_nth_z ttbl v = Some n /\ nth_error nexits act = Some n. + Inductive tr_switch - (c: code) (r: reg) (nexits: list node): + (c: code) (map: mapping) (r: reg) (nexits: list node): comptree -> node -> Prop := | tr_switch_action: forall act n, nth_error nexits act = Some n -> - tr_switch c r nexits (CTaction act) n + tr_switch c map r nexits (CTaction act) n | tr_switch_ifeq: forall key act t' n ncont nfound, - tr_switch c r nexits t' ncont -> + tr_switch c map r nexits t' ncont -> nth_error nexits act = Some nfound -> c!n = Some(Icond (Ccompimm Ceq key) (r :: nil) nfound ncont) -> - tr_switch c r nexits (CTifeq key act t') n + tr_switch c map r nexits (CTifeq key act t') n | tr_switch_iflt: forall key t1 t2 n n1 n2, - tr_switch c r nexits t1 n1 -> - tr_switch c r nexits t2 n2 -> + tr_switch c map r nexits t1 n1 -> + tr_switch c map r nexits t2 n2 -> c!n = Some(Icond (Ccompuimm Clt key) (r :: nil) n1 n2) -> - tr_switch c r nexits (CTiflt key t1 t2) n. + tr_switch c map r nexits (CTiflt key t1 t2) n + | tr_switch_jumptable: forall ofs sz tbl t n n1 n2 n3 rt ttbl, + ~reg_in_map map rt -> rt <> r -> + c!n = Some(Iop (if Int.eq ofs Int.zero then Omove else Oaddimm (Int.neg ofs)) + (r ::nil) rt n1) -> + c!n1 = Some(Icond (Ccompuimm Clt sz) (rt :: nil) n2 n3) -> + c!n2 = Some(Ijumptable rt ttbl) -> + tr_switch c map r nexits t n3 -> + tr_jumptable nexits tbl ttbl -> + tr_switch c map r nexits (CTjumptable ofs sz tbl t) n. (** [tr_stmt c map stmt ns ncont nexits nret rret] holds if the graph [c], starting at node [ns], contains instructions that perform the Cminor @@ -786,7 +800,7 @@ Inductive tr_stmt (c: code) (map: mapping): | tr_Sswitch: forall a cases default ns nd nexits ngoto nret rret n r t, validate_switch default cases t = true -> tr_expr c map nil a ns n r -> - tr_switch c r nexits t n -> + tr_switch c map r nexits t n -> tr_stmt c map (Sswitch a cases default) ns nd nexits ngoto nret rret | tr_Sreturn_none: forall nret nd nexits ngoto, tr_stmt c map (Sreturn None) nret nd nexits ngoto nret None @@ -1000,9 +1014,9 @@ Qed. Lemma tr_switch_incr: forall s1 s2, state_incr s1 s2 -> - forall r nexits t ns, - tr_switch s1.(st_code) r nexits t ns -> - tr_switch s2.(st_code) r nexits t ns. + forall map r nexits t ns, + tr_switch s1.(st_code) map r nexits t ns -> + tr_switch s2.(st_code) map r nexits t ns. Proof. induction 2; econstructor; eauto with rtlg. Qed. @@ -1051,24 +1065,47 @@ Proof. destruct (nth_error nexits n); intro; monadInv H. auto. Qed. +Lemma transl_jumptable_charact: + forall nexits tbl s nl s' incr, + transl_jumptable nexits tbl s = OK nl s' incr -> + tr_jumptable nexits tbl nl /\ s' = s. +Proof. + induction tbl; intros. + monadInv H. split. red. simpl. intros. discriminate. auto. + monadInv H. exploit transl_exit_charact; eauto. intros [A B]. + exploit IHtbl; eauto. intros [C D]. + split. red. simpl. intros. destruct (zeq v 0). inv H. exists x; auto. auto. + congruence. +Qed. + Lemma transl_switch_charact: - forall r nexits t s ns s' incr, + forall map r nexits t s ns s' incr, + map_valid map s -> reg_valid r s -> transl_switch r nexits t s = OK ns s' incr -> - tr_switch s'.(st_code) r nexits t ns. + tr_switch s'.(st_code) map r nexits t ns. Proof. induction t; simpl; intros. exploit transl_exit_charact; eauto. intros [A B]. econstructor; eauto. - monadInv H. + monadInv H1. exploit transl_exit_charact; eauto. intros [A B]. subst s1. econstructor; eauto with rtlg. apply tr_switch_incr with s0; eauto with rtlg. - monadInv H. + monadInv H1. econstructor; eauto with rtlg. apply tr_switch_incr with s1; eauto with rtlg. apply tr_switch_incr with s0; eauto with rtlg. + + monadInv H1. + exploit transl_jumptable_charact; eauto. intros [A B]. subst s1. + econstructor. eauto with rtlg. + apply sym_not_equal. apply valid_fresh_different with s; eauto with rtlg. + eauto with rtlg. eauto with rtlg. eauto with rtlg. + apply tr_switch_incr with s3. eauto with rtlg. + eapply IHt with (s := s2); eauto with rtlg. + auto. Qed. Lemma transl_stmt_charact: @@ -1091,8 +1128,9 @@ Proof. apply tr_expr_incr with s3; eauto with rtlg. eapply transl_expr_charact; eauto with rtlg. (* Scall *) - assert (state_incr s0 s3) by eauto with rtlg. - assert (state_incr s3 s6) by eauto with rtlg. + assert (state_incr s0 s2) by eauto with rtlg. + assert (state_incr s2 s4) by eauto with rtlg. + assert (state_incr s4 s6) by eauto with rtlg. econstructor; eauto with rtlg. eapply transl_expr_charact; eauto with rtlg. apply tr_exprlist_incr with s6. auto. @@ -1101,7 +1139,6 @@ Proof. apply regs_valid_cons; eauto with rtlg. apply regs_valid_incr with s1; eauto with rtlg. apply regs_valid_cons; eauto with rtlg. - apply regs_valid_incr with s2; eauto with rtlg. apply tr_store_optvar_incr with s4; eauto with rtlg. eapply store_optvar_charact; eauto with rtlg. (* Stailcall *) @@ -1149,7 +1186,7 @@ Proof. econstructor; eauto with rtlg. eapply transl_expr_charact; eauto with rtlg. apply tr_switch_incr with s1; auto with rtlg. - eapply transl_switch_charact; eauto with rtlg. + eapply transl_switch_charact with (s := s0); eauto with rtlg. monadInv TR. (* Sreturn *) destruct o; destruct rret; inv TR. -- cgit