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

1 files changed, 61 insertions, 30 deletions

diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index d8d5dc8..c82c051 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.