Merge of branch seq-and-or. See Changelog for details.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2059 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 16 insertions, 33 deletions

diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index 86c1177..d3b99bb 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -416,10 +416,12 @@ Fixpoint transl_expr (map: mapping) (a: expr) (rd: reg) (nd: node)
       do rl <- alloc_regs map al;
       do no <- add_instr (Iload chunk addr rl rd nd);
          transl_exprlist map al rl no
-  | Econdition b c d =>
-      do nfalse <- transl_expr map d rd nd;
-      do ntrue  <- transl_expr map c rd nd;
-         transl_condition map b ntrue nfalse
+  | Econdition cond al b c =>
+      do rl <- alloc_regs map al;
+      do nfalse <- transl_expr map c rd nd;
+      do ntrue  <- transl_expr map b rd nd;
+      do nt <- add_instr (Icond cond rl ntrue nfalse);
+         transl_exprlist map al rl nt
   | Elet b c =>
       do r  <- new_reg;
       do nc <- transl_expr (add_letvar map r) c rd nd;
@@ -428,28 +430,6 @@ Fixpoint transl_expr (map: mapping) (a: expr) (rd: reg) (nd: node)
       do r <- find_letvar map n; add_move r rd nd
   end
 
-(** Translation of a conditional expression.  Similar to [transl_expr],
-  but the expression is evaluated for its truth value, and the generated
-  code branches to one of two possible continuation nodes [ntrue] or 
-  [nfalse] depending on the truth value of [a]. *)
-
-with transl_condition (map: mapping) (a: condexpr) (ntrue nfalse: node)
-                      {struct a}: mon node :=
-  match a with
-  | CEtrue =>
-      ret ntrue
-  | CEfalse =>
-      ret nfalse
-  | CEcond cond bl =>
-      do rl <- alloc_regs map bl;
-      do nt <- add_instr (Icond cond rl ntrue nfalse);
-         transl_exprlist map bl rl nt
-  | CEcondition b c d =>
-      do nd <- transl_condition map d ntrue nfalse;
-      do nc <- transl_condition map c ntrue nfalse;
-         transl_condition map b nc nd
-  end
-
 (** Translation of a list of expressions.  The expressions are evaluated
   left-to-right, and their values stored in the given list of registers. *)
 
@@ -472,7 +452,7 @@ with transl_exprlist (map: mapping) (al: exprlist) (rl: list reg) (nd: node)
   no impact on program correctness.  We delegate the choice to an
   external heuristic (written in OCaml), declared below.  *)
 
-Parameter more_likely: condexpr -> stmt -> stmt -> bool.
+Parameter more_likely: condition -> stmt -> stmt -> bool.
 
 (** Auxiliary for translating [Sswitch] statements. *)
 
@@ -521,7 +501,7 @@ Fixpoint transl_switch (r: reg) (nexits: list node) (t: comptree)
 Fixpoint expr_is_2addr_op (e: expr) : bool :=
   match e with
   | Eop op _ => two_address_op op
-  | Econdition e1 e2 e3 => expr_is_2addr_op e2 || expr_is_2addr_op e3
+  | Econdition cond el e2 e3 => expr_is_2addr_op e2 || expr_is_2addr_op e3
   | Elet e1 e2 => expr_is_2addr_op e2
   | _ => false
   end.
@@ -587,15 +567,18 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node)
   | Sseq s1 s2 =>
       do ns <- transl_stmt map s2 nd nexits ngoto nret rret;
       transl_stmt map s1 ns nexits ngoto nret rret
-  | Sifthenelse a strue sfalse =>
-      if more_likely a strue sfalse then
+  | Sifthenelse cond al strue sfalse =>
+      do rl <- alloc_regs map al;
+      if more_likely cond strue sfalse then
         do nfalse <- transl_stmt map sfalse nd nexits ngoto nret rret;
         do ntrue  <- transl_stmt map strue  nd nexits ngoto nret rret;
-        transl_condition map a ntrue nfalse
+        do nt <- add_instr (Icond cond rl ntrue nfalse);
+           transl_exprlist map al rl nt
       else
         do ntrue  <- transl_stmt map strue  nd nexits ngoto nret rret;
         do nfalse <- transl_stmt map sfalse nd nexits ngoto nret rret;
-        transl_condition map a ntrue nfalse
+        do nt <- add_instr (Icond cond rl ntrue nfalse);
+           transl_exprlist map al rl nt
   | Sloop sbody =>
       do n1 <- reserve_instr;
       do n2 <- transl_stmt map sbody n1 nexits ngoto nret rret;
@@ -650,7 +633,7 @@ Fixpoint reserve_labels (s: stmt) (ms: labelmap * state)
                         {struct s} : labelmap * state :=
   match s with
   | Sseq s1 s2 => reserve_labels s1 (reserve_labels s2 ms)
-  | Sifthenelse c s1 s2 => reserve_labels s1 (reserve_labels s2 ms)
+  | Sifthenelse cond al s1 s2 => reserve_labels s1 (reserve_labels s2 ms)
   | Sloop s1 => reserve_labels s1 ms
   | Sblock s1 => reserve_labels s1 ms
   | Slabel lbl s1 => alloc_label lbl (reserve_labels s1 ms)