From 5c84fd4adbcd8a63cc29fb0286cb46f18abde55c Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 29 Apr 2013 17:11:47 +0000 Subject: Expand 64-bit integer comparisons into 32-bit integer comparisons. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2218 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/RTLgenspec.v | 91 +++++++++++++++++++++++++++++++++++----------------- 1 file changed, 61 insertions(+), 30 deletions(-) (limited to 'backend/RTLgenspec.v') diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index d8d5dc8c..c82c0510 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -703,11 +703,11 @@ Inductive tr_expr (c: code): c!n1 = Some (Iload chunk addr rl rd nd) -> reg_map_ok map rd dst -> ~In rd pr -> tr_expr c map pr (Eload chunk addr al) ns nd rd dst - | tr_Econdition: forall map pr cond bl ifso ifnot ns nd rd ntrue nfalse dst, - tr_condition c map pr cond bl ns ntrue nfalse -> + | tr_Econdition: forall map pr a ifso ifnot ns nd rd ntrue nfalse dst, + tr_condition c map pr a ns ntrue nfalse -> tr_expr c map pr ifso ntrue nd rd dst -> tr_expr c map pr ifnot nfalse nd rd dst -> - tr_expr c map pr (Econdition cond bl ifso ifnot) ns nd rd dst + tr_expr c map pr (Econdition a ifso ifnot) ns nd rd dst | tr_Elet: forall map pr b1 b2 ns nd rd n1 r dst, ~reg_in_map map r -> tr_expr c map pr b1 ns n1 r None -> @@ -730,17 +730,27 @@ Inductive tr_expr (c: code): tr_expr c map pr (Eexternal id sg al) ns nd rd dst -(** [tr_condition c map pr cond al ns ntrue nfalse rd] holds if the graph [c], +(** [tr_condition c map pr a ns ntrue nfalse rd] holds if the graph [c], starting at node [ns], contains instructions that compute the truth - value of the Cminor conditional expression [cond] and terminate + value of the Cminor conditional expression [a] and terminate on node [ntrue] if the condition holds and on node [nfalse] otherwise. *) with tr_condition (c: code): - mapping -> list reg -> condition -> exprlist -> node -> node -> node -> Prop := + mapping -> list reg -> condexpr -> node -> node -> node -> Prop := | tr_CEcond: forall map pr cond bl ns ntrue nfalse n1 rl, tr_exprlist c map pr bl ns n1 rl -> c!n1 = Some (Icond cond rl ntrue nfalse) -> - tr_condition c map pr cond bl ns ntrue nfalse + tr_condition c map pr (CEcond cond bl) ns ntrue nfalse + | tr_CEcondition: forall map pr a1 a2 a3 ns ntrue nfalse n2 n3, + tr_condition c map pr a1 ns n2 n3 -> + tr_condition c map pr a2 n2 ntrue nfalse -> + tr_condition c map pr a3 n3 ntrue nfalse -> + tr_condition c map pr (CEcondition a1 a2 a3) ns ntrue nfalse + | tr_CElet: forall map pr a b ns ntrue nfalse r n1, + ~reg_in_map map r -> + tr_expr c map pr a ns n1 r None -> + tr_condition c (add_letvar map r) pr b n1 ntrue nfalse -> + tr_condition c map pr (CElet a b) ns ntrue nfalse (** [tr_exprlist c map pr exprs ns nd rds] holds if the graph [c], between nodes [ns] and [nd], contains instructions that compute the values @@ -840,11 +850,11 @@ Inductive tr_stmt (c: code) (map: mapping): tr_stmt c map s2 n nd nexits ngoto nret rret -> tr_stmt c map s1 ns n nexits ngoto nret rret -> tr_stmt c map (Sseq s1 s2) ns nd nexits ngoto nret rret - | tr_Sifthenelse: forall cond al strue sfalse ns nd nexits ngoto nret rret ntrue nfalse, + | tr_Sifthenelse: forall a strue sfalse ns nd nexits ngoto nret rret ntrue nfalse, tr_stmt c map strue ntrue nd nexits ngoto nret rret -> tr_stmt c map sfalse nfalse nd nexits ngoto nret rret -> - tr_condition c map nil cond al ns ntrue nfalse -> - tr_stmt c map (Sifthenelse cond al strue sfalse) ns nd nexits ngoto nret rret + tr_condition c map nil a ns ntrue nfalse -> + tr_stmt c map (Sifthenelse a strue sfalse) ns nd nexits ngoto nret rret | tr_Sloop: forall sbody ns nd nexits ngoto nret rret nloop nend, tr_stmt c map sbody nloop nend nexits ngoto nret rret -> c!ns = Some(Inop nloop) -> @@ -914,9 +924,9 @@ Lemma tr_expr_incr: tr_expr s2.(st_code) map pr a ns nd rd dst with tr_condition_incr: forall s1 s2, state_incr s1 s2 -> - forall map pr cond al ns ntrue nfalse, - tr_condition s1.(st_code) map pr cond al ns ntrue nfalse -> - tr_condition s2.(st_code) map pr cond al ns ntrue nfalse + forall map pr a ns ntrue nfalse, + tr_condition s1.(st_code) map pr a ns ntrue nfalse -> + tr_condition s2.(st_code) map pr a ns ntrue nfalse with tr_exprlist_incr: forall s1 s2, state_incr s1 s2 -> forall map pr al ns nd rl, @@ -962,7 +972,14 @@ with transl_exprlist_charact: (OK: target_regs_ok map pr al rl) (VALID1: regs_valid pr s) (VALID2: regs_valid rl s), - tr_exprlist s'.(st_code) map pr al ns nd rl. + tr_exprlist s'.(st_code) map pr al ns nd rl + +with transl_condexpr_charact: + forall a map ntrue nfalse s ns s' pr INCR + (TR: transl_condexpr map a ntrue nfalse s = OK ns s' INCR) + (WF: map_valid map s) + (VALID: regs_valid pr s), + tr_condition s'.(st_code) map pr a ns ntrue nfalse. Proof. induction a; intros; try (monadInv TR); saturateTrans. @@ -981,12 +998,12 @@ Proof. eapply transl_exprlist_charact; eauto with rtlg. (* Econdition *) inv OK. - econstructor; eauto with rtlg. - econstructor; eauto with rtlg. eapply transl_exprlist_charact; eauto with rtlg. - apply tr_expr_incr with s2; auto. - eapply transl_expr_charact; eauto 2 with rtlg. constructor; auto. + econstructor. + eauto with rtlg. apply tr_expr_incr with s1; auto. eapply transl_expr_charact; eauto 2 with rtlg. constructor; auto. + apply tr_expr_incr with s0; auto. + eapply transl_expr_charact; eauto 2 with rtlg. constructor; auto. (* Elet *) inv OK. econstructor. eapply new_reg_not_in_map; eauto with rtlg. @@ -1031,6 +1048,22 @@ Proof. eapply transl_exprlist_charact; eauto with rtlg. apply regs_valid_cons. apply VALID2. auto with coqlib. auto. red; intros; apply VALID2; auto with coqlib. + +(* Conditional expressions *) + induction a; intros; try (monadInv TR); saturateTrans. + + (* CEcond *) + econstructor; eauto with rtlg. eapply transl_exprlist_charact; eauto with rtlg. + (* CEcondition *) + econstructor; eauto with rtlg. + apply tr_condition_incr with s1; eauto with rtlg. + apply tr_condition_incr with s0; eauto with rtlg. + (* CElet *) + econstructor; eauto with rtlg. + eapply transl_expr_charact; eauto with rtlg. + apply tr_condition_incr with s1; eauto with rtlg. + eapply transl_condexpr_charact; eauto with rtlg. + apply add_letvar_valid; eauto with rtlg. Qed. (** A variant of [transl_expr_charact], for use when the destination @@ -1056,10 +1089,10 @@ Proof. eapply transl_exprlist_charact; eauto with rtlg. (* Econdition *) econstructor; eauto with rtlg. - econstructor; eauto with rtlg. eapply transl_exprlist_charact; eauto with rtlg. - apply tr_expr_incr with s2; auto. - eapply IHa1; eauto 2 with rtlg. + eapply transl_condexpr_charact; eauto with rtlg. apply tr_expr_incr with s1; auto. + eapply IHa1; eauto 2 with rtlg. + apply tr_expr_incr with s0; auto. eapply IHa2; eauto 2 with rtlg. (* Elet *) econstructor. eapply new_reg_not_in_map; eauto with rtlg. @@ -1227,21 +1260,19 @@ Proof. eapply IHstmt2; eauto with rtlg. eapply IHstmt1; eauto with rtlg. (* Sifthenelse *) - destruct (more_likely c stmt1 stmt2); monadInv EQ0. + destruct (more_likely c stmt1 stmt2); monadInv TR. econstructor. - apply tr_stmt_incr with s2; auto. + apply tr_stmt_incr with s1; auto. eapply IHstmt1; eauto with rtlg. - apply tr_stmt_incr with s1; auto. + apply tr_stmt_incr with s0; auto. eapply IHstmt2; eauto with rtlg. - econstructor; eauto with rtlg. - eapply transl_exprlist_charact; eauto with rtlg. + eapply transl_condexpr_charact; eauto with rtlg. econstructor. - apply tr_stmt_incr with s1; auto. + apply tr_stmt_incr with s0; auto. eapply IHstmt1; eauto with rtlg. - apply tr_stmt_incr with s2; auto. + apply tr_stmt_incr with s1; auto. eapply IHstmt2; eauto with rtlg. - econstructor; eauto with rtlg. - eapply transl_exprlist_charact; eauto with rtlg. + eapply transl_condexpr_charact; eauto with rtlg. (* Sloop *) econstructor. apply tr_stmt_incr with s1; auto. -- cgit