Big merge of the newregalloc-int64 branch. Lots of changes in two directions:

1- new register allocator (+ live range splitting, spilling&reloading, etc)
   based on a posteriori validation using the Rideau-Leroy algorithm
2- support for 64-bit integer arithmetic (type "long long").


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

1 files changed, 10 insertions, 31 deletions

diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index 007191a0..f5e34e4b 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -362,18 +362,6 @@ Fixpoint alloc_regs (map: mapping) (al: exprlist)
       ret (r :: rl)
   end.
 
-(** A variant of [alloc_regs] for two-address instructions:
-  reuse the result register as destination for the first argument. *)
-
-Definition alloc_regs_2addr (map: mapping) (al: exprlist) (rd: reg)
-                            : mon (list reg) :=
-  match al with
-  | Enil =>
-      ret nil
-  | Econs a bl =>
-      do rl <- alloc_regs map bl; ret (rd :: rl)
-  end.
-
 (** [alloc_optreg] is used for function calls.  If a destination is
   specified for the call, it is returned.  Otherwise, a fresh
   register is returned. *)
@@ -406,9 +394,7 @@ Fixpoint transl_expr (map: mapping) (a: expr) (rd: reg) (nd: node)
   | Evar v =>
       do r <- find_var map v; add_move r rd nd
   | Eop op al =>
-      do rl <- if two_address_op op
-               then alloc_regs_2addr map al rd
-               else alloc_regs map al;
+      do rl <- alloc_regs map al;
       do no <- add_instr (Iop op rl rd nd);
       transl_exprlist map al rl no
   | Eload chunk addr al =>
@@ -427,6 +413,14 @@ Fixpoint transl_expr (map: mapping) (a: expr) (rd: reg) (nd: node)
          transl_expr map b r nc
   | Eletvar n =>
       do r <- find_letvar map n; add_move r rd nd
+  | Ebuiltin ef al =>
+      do rl <- alloc_regs map al;
+      do no <- add_instr (Ibuiltin ef rl rd nd);
+      transl_exprlist map al rl no
+  | Eexternal id sg al =>
+      do rl <- alloc_regs map al;
+      do no <- add_instr (Icall sg (inr id) rl rd nd);
+      transl_exprlist map al rl no
   end
 
 (** Translation of a list of expressions.  The expressions are evaluated
@@ -495,16 +489,6 @@ Fixpoint transl_switch (r: reg) (nexits: list node) (t: comptree)
       add_instr (Iop op (r :: nil) rt n3)
   end.
 
-(** Detect a two-address operator at the top of an expression. *)
-
-Fixpoint expr_is_2addr_op (e: expr) : bool :=
-  match e with
-  | Eop op _ => two_address_op op
-  | 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.
-
 (** Translation of statements.  [transl_stmt map s nd nexits nret rret]
   enriches the current CFG with the RTL instructions necessary to
   execute the CminorSel statement [s], and returns the node of the first
@@ -524,12 +508,7 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node)
       ret nd
   | Sassign v b =>
       do r <- find_var map v;
-      if expr_is_2addr_op b then
-        do rd <- new_reg;
-        do n1 <- add_move rd r nd;
-        transl_expr map b rd n1
-      else
-        transl_expr map b r nd
+      transl_expr map b r nd
   | Sstore chunk addr al b =>
       do rl <- alloc_regs map al;
       do r <- alloc_reg map b;