Fusion des modifications faites sur les branches "tailcalls" et "smallstep".

En particulier:
- Semantiques small-step depuis RTL jusqu'a PPC
- Cminor independant du processeur
- Ajout passes Selection et Reload
- Ajout des langages intermediaires CminorSel et LTLin correspondants
- Ajout des tailcalls depuis Cminor jusqu'a PPC


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

1 files changed, 88 insertions, 294 deletions

diff --git a/backend/Allocation.v b/backend/Allocation.v
index 74c85cf..eab5233 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -1,7 +1,7 @@
-(** Register allocation, spilling, reloading and explicitation of
-   calling conventions. *)
+(** Register allocation. *)
 
 Require Import Coqlib.
+Require Import Errors.
 Require Import Maps.
 Require Import Lattice.
 Require Import AST.
@@ -16,15 +16,14 @@ Require Import Kildall.
 Require Import Locations.
 Require Import Conventions.
 Require Import Coloring.
-Require Import Parallelmove.
 
 (** * Liveness analysis over RTL *)
 
 (** A register [r] is live at a point [p] if there exists a path
-    from [p] to some instruction that uses [r] as argument,
-    and [r] is not redefined along this path.
-    Liveness can be computed by a backward dataflow analysis.
-    The analysis operates over sets of (live) pseudo-registers. *)
+  from [p] to some instruction that uses [r] as argument,
+  and [r] is not redefined along this path.
+  Liveness can be computed by a backward dataflow analysis.
+  The analysis operates over sets of (live) pseudo-registers. *)
 
 Notation reg_live := Regset.add.
 Notation reg_dead := Regset.remove.
@@ -50,25 +49,25 @@ Fixpoint reg_list_dead
   end.
 
 (** Here is the transfer function for the dataflow analysis.
-    Since this is a backward dataflow analysis, it takes as argument
-    the abstract register set ``after'' the given instruction,
-    i.e. the registers that are live after; and it returns as result
-    the abstract register set ``before'' the given instruction,
-    i.e. the registers that must be live before.
-    The general relation between ``live before'' and ``live after''
-    an instruction is that a register is live before if either
-    it is one of the arguments of the instruction, or it is not the result
-    of the instruction and it is live after.
-    However, if the result of a side-effect-free instruction is not 
-    live ``after'', the whole instruction will be removed later
-    (since it computes a useless result), thus its arguments need not
-    be live ``before''. *)
+  Since this is a backward dataflow analysis, it takes as argument
+  the abstract register set ``after'' the given instruction,
+  i.e. the registers that are live after; and it returns as result
+  the abstract register set ``before'' the given instruction,
+  i.e. the registers that must be live before.
+  The general relation between ``live before'' and ``live after''
+  an instruction is that a register is live before if either
+  it is one of the arguments of the instruction, or it is not the result
+  of the instruction and it is live after.
+  However, if the result of a side-effect-free instruction is not 
+  live ``after'', the whole instruction will be removed later
+  (since it computes a useless result), thus its arguments need not
+  be live ``before''. *)
 
 Definition transfer
             (f: RTL.function) (pc: node) (after: Regset.t) : Regset.t :=
   match f.(fn_code)!pc with
   | None =>
-      after
+      Regset.empty
   | Some i =>
       match i with
       | Inop s =>
@@ -88,18 +87,20 @@ Definition transfer
       | Icall sig ros args res s =>
           reg_list_live args
            (reg_sum_live ros (reg_dead res after))
+      | Itailcall sig ros args =>
+	  reg_list_live args (reg_sum_live ros Regset.empty)
       | Ialloc arg res s =>
           reg_live arg (reg_dead res after)
       | Icond cond args ifso ifnot =>
           reg_list_live args after
       | Ireturn optarg =>
-          reg_option_live optarg after
+          reg_option_live optarg Regset.empty
       end
   end.
 
 (** The liveness analysis is then obtained by instantiating the
-    general framework for backward dataflow analysis provided by
-    module [Kildall].  *)
+  general framework for backward dataflow analysis provided by
+  module [Kildall].  *)
 
 Module RegsetLat := LFSet(Regset).
 Module DS := Backward_Dataflow_Solver(RegsetLat)(NodeSetBackward).
@@ -107,315 +108,108 @@ Module DS := Backward_Dataflow_Solver(RegsetLat)(NodeSetBackward).
 Definition analyze (f: RTL.function): option (PMap.t Regset.t) :=
   DS.fixpoint (successors f) f.(fn_nextpc) (transfer f) nil.
 
-(** * Spilling and reloading *)
-
-(** LTL operations, like those of the target processor, operate only
-  over machine registers, but not over stack slots.  Consider
-  the RTL instruction
-<<
-        r1 <- Iop(Oadd, r1 :: r2 :: nil)
->>
-  and assume that [r1] and [r2] are assigned to stack locations [S s1]
-  and [S s2], respectively.  The translated LTL code must load these
-  stack locations into temporary integer registers (this is called
-  ``reloading''), perform the [Oadd] operation over these temporaries,
-  leave the result in a temporary, then store the temporary back to
-  stack location [S s1] (this is called ``spilling'').  In other term,
-  the generated LTL code has the following shape:
-<<
-        IT1 <- Bgetstack s1;
-        IT2 <- Bgetstack s2;
-        IT1 <- Bop(Oadd, IT1 :: IT2 :: nil);
-        Bsetstack s1 IT1;
->>
-  This section provides functions that assist in choosing appropriate
-  temporaries and inserting the required spilling and reloading
-  operations. *)
-
-(** ** Allocation of temporary registers for reloading and spilling. *)
-
-(** [reg_for l] returns a machine register appropriate for working
-    over the location [l]: either the machine register [m] if [l = R m],
-    or a temporary register of [l]'s type if [l] is a stack slot. *)
-
-Definition reg_for (l: loc) : mreg :=
-  match l with
-  | R r => r
-  | S s => match slot_type s with Tint => IT1 | Tfloat => FT1 end
-  end.
-
-(** [regs_for ll] is similar, for a list of locations [ll] of length
-    at most 3.  We ensure that distinct temporaries are used for
-    different elements of [ll]. *)
-
-Fixpoint regs_for_rec (locs: list loc) (itmps ftmps: list mreg)
-                      {struct locs} : list mreg :=
-  match locs, itmps, ftmps with
-  | l1 :: ls, it1 :: its, ft1 :: fts =>
-      match l1 with
-      | R r => r
-      | S s => match slot_type s with Tint => it1 | Tfloat => ft1 end
-      end
-      :: regs_for_rec ls its fts
-  | _, _, _ => nil
-  end.
-
-Definition regs_for (locs: list loc) :=
-  regs_for_rec locs (IT1 :: IT2 :: IT3 :: nil) (FT1 :: FT2 :: FT3 :: nil).
-
-(** ** Insertion of LTL reloads, stores and moves *)
+(** * Translation from RTL to LTL *)
 
 Require Import LTL.
 
-(** [add_spill src dst k] prepends to [k] the instructions needed
-  to assign location [dst] the value of machine register [mreg]. *)
-
-Definition add_spill (src: mreg) (dst: loc) (k: block) :=
-  match dst with
-  | R rd => if mreg_eq src rd then k else Bop Omove (src :: nil) rd k
-  | S sl => Bsetstack src sl k
-  end.
-
-(** [add_reload src dst k] prepends to [k] the instructions needed
-  to assign machine register [mreg] the value of the location [src]. *)
-
-Definition add_reload (src: loc) (dst: mreg) (k: block) :=
-  match src with
-  | R rs => if mreg_eq rs dst then k else Bop Omove (rs :: nil) dst k
-  | S sl => Bgetstack sl dst k
-  end.
-
-(** [add_reloads] is similar for a list of locations (as sources)
-  and a list of machine registers (as destinations).  *)
-
-Fixpoint add_reloads (srcs: list loc) (dsts: list mreg) (k: block)
-                                            {struct srcs} : block :=
-  match srcs, dsts with
-  | s1 :: sl, t1 :: tl =>
-      add_reload s1 t1 (add_reloads sl tl k)
-  | _, _ =>
-      k
-  end.
-
-(** [add_move src dst k] prepends to [k] the instructions that copy
-  the value of location [src] into location [dst]. *)
-
-Definition add_move (src dst: loc) (k: block) :=
-  if Loc.eq src dst then k else
-    match src, dst with
-    | R rs, _ =>
-        add_spill rs dst k
-    | _, R rd =>
-        add_reload src rd k
-    | S ss, S sd =>
-        let tmp :=
-          match slot_type ss with Tint => IT1 | Tfloat => FT1 end in
-        add_reload src tmp (add_spill tmp dst k)
-    end.
-
-(** [parallel_move srcs dsts k] is similar, but for a list of
-  source locations and a list of destination locations of the same
-  length.  This is a parallel move, meaning that arbitrary overlap
-  between the sources and destinations is permitted. *)
-
-Definition parallel_move (srcs dsts: list loc) (k: block) : block :=
-  List.fold_right
-    (fun p k => add_move (fst p) (snd p) k)
-     k (parmove srcs dsts).
-
-(** ** Constructors for LTL instructions *)
-
-(** The following functions generate LTL instructions operating
-  over the given locations.  Appropriate reloading and spilling operations
-  are added around the core LTL instruction. *)
-
-Definition add_op (op: operation) (args: list loc) (res: loc) (s: node) :=
-  match is_move_operation op args with
-  | Some src =>
-      add_move src res (Bgoto s)
-  | None =>
-      let rargs := regs_for args in
-      let rres := reg_for res in
-      add_reloads args rargs (Bop op rargs rres (add_spill rres res (Bgoto s)))
-  end.
-
-Definition add_load (chunk: memory_chunk) (addr: addressing)
-                    (args: list loc) (dst: loc) (s: node) :=
-  let rargs := regs_for args in
-  let rdst := reg_for dst in
-  add_reloads args rargs
-    (Bload chunk addr rargs rdst (add_spill rdst dst (Bgoto s))).
-
-Definition add_store (chunk: memory_chunk) (addr: addressing)
-                     (args: list loc) (src: loc) (s: node) :=
-  match regs_for (src :: args) with
-  | nil => Breturn                      (* never happens *)
-  | rsrc :: rargs =>
-      add_reloads (src :: args) (rsrc :: rargs)
-        (Bstore chunk addr rargs rsrc (Bgoto s))
-  end.
-
-Definition add_alloc (arg: loc) (res: loc) (s: node) :=
-  add_reload arg Conventions.loc_alloc_argument
-    (Balloc (add_spill Conventions.loc_alloc_result res (Bgoto s))).
-
-(** For function calls, we also add appropriate moves to and from
-  the canonical locations for function arguments and function results,
-  as dictated by the calling conventions. *)
-
-Definition add_call (sig: signature) (ros: loc + ident)
-                    (args: list loc) (res: loc) (s: node) :=
-  let rargs := loc_arguments sig in
-  let rres  := loc_result sig in
-  match ros with
-  | inl fn =>
-      (add_reload fn IT3
-        (parallel_move args rargs
-          (Bcall sig (inl _ IT3) (add_spill rres res (Bgoto s)))))
-  | inr id =>
-      parallel_move args rargs
-        (Bcall sig (inr _ id) (add_spill rres res (Bgoto s)))
-  end.
-
-Definition add_cond (cond: condition) (args: list loc) (ifso ifnot: node) :=
-  let rargs := regs_for args in
-  add_reloads args rargs (Bcond cond rargs ifso ifnot).
-
-(** For function returns, we add the appropriate move of the result
-  to the conventional location for the function result.  If the function
-  returns with no value, we explicitly set the function result register
-  to the [Vundef] value, for consistency with RTL's semantics. *)
-
-Definition add_return (sig: signature) (optarg: option loc) :=
-  match optarg with
-  | Some arg => add_reload arg (loc_result sig) Breturn
-  | None     => Bop Oundef nil (loc_result sig) Breturn
-  end.
-  
-(** For function entry points, we move from the parameter locations
-  dictated by the calling convention to the locations of the function
-  parameters.  We also explicitly set to [Vundef] the locations
-  of pseudo-registers that are live at function entry but are not
-  parameters, again for consistency with RTL's semantics. *)
-
-Fixpoint add_undefs (ll: list loc) (b: block) {struct ll} : block :=
-  match ll with
-  | nil => b
-  | R r :: ls => Bop Oundef nil r (add_undefs ls b)
-  | S s :: ls => add_undefs ls b
-  end.
-
-Definition add_entry (sig: signature) (params: list loc) (undefs: list loc)
-                     (s: node) :=
-  parallel_move (loc_parameters sig) params (add_undefs undefs (Bgoto s)).
-
-(** * Translation from RTL to LTL *)
-
-(** Each [RTL] instruction translates to an [LTL] basic block.
+(** Each [RTL] instruction translates to an [LTL] instruction.
   The register assignment [assign] returned by register allocation
   is applied to the arguments and results of the RTL
-  instruction, followed by an invocation of the appropriate [LTL]
-  constructor function that will deal with spilling, reloading and
-  calling conventions.  In addition, dead instructions are eliminated.
+  instruction.  Moreover, dead instructions and redundant moves
+  are eliminated (turned into a [Lnop] instruction).
   Dead instructions are instructions without side-effects ([Iop] and
   [Iload]) whose result register is dead, i.e. whose result value
-  is never used. *)
+  is never used.  Redundant moves are moves whose source and destination
+  are assigned the same location. *)
+
+Definition is_redundant_move
+    (op: operation) (args: list reg) (res: reg) (assign: reg -> loc) : bool :=
+  match is_move_operation op args with
+  | None => false
+  | Some src => if Loc.eq (assign src) (assign res) then true else false
+  end.
 
 Definition transf_instr
          (f: RTL.function) (live: PMap.t Regset.t) (assign: reg -> loc)
-         (pc: node) (instr: RTL.instruction) : LTL.block :=
+         (pc: node) (instr: RTL.instruction) : LTL.instruction :=
   match instr with
   | Inop s =>
-      Bgoto s
+      Lnop s
   | Iop op args res s =>
       if Regset.mem res live!!pc then
-        add_op op (List.map assign args) (assign res) s
+        if is_redundant_move op args res assign then
+          Lnop s
+        else 
+          Lop op (List.map assign args) (assign res) s
       else
-        Bgoto s
+        Lnop s
   | Iload chunk addr args dst s =>
       if Regset.mem dst live!!pc then
-        add_load chunk addr (List.map assign args) (assign dst) s
+        Lload chunk addr (List.map assign args) (assign dst) s
       else
-        Bgoto s
+        Lnop s
   | Istore chunk addr args src s =>
-      add_store chunk addr (List.map assign args) (assign src) s
+      Lstore chunk addr (List.map assign args) (assign src) s
   | Icall sig ros args res s =>
-      add_call sig (sum_left_map assign ros) (List.map assign args)
-                   (assign res) s
+      Lcall sig (sum_left_map assign ros) (List.map assign args)
+                (assign res) s
+  | Itailcall sig ros args =>
+      Ltailcall sig (sum_left_map assign ros) (List.map assign args)
   | Ialloc arg res s =>
-      add_alloc (assign arg) (assign res) s
+      Lalloc (assign arg) (assign res) s
   | Icond cond args ifso ifnot =>
-      add_cond cond (List.map assign args) ifso ifnot
+      Lcond cond (List.map assign args) ifso ifnot
   | Ireturn optarg =>
-      add_return f.(RTL.fn_sig) (option_map assign optarg)
+      Lreturn (option_map assign optarg)
   end.
 
-Definition transf_entrypoint
-     (f: RTL.function) (live: PMap.t Regset.t) (assign: reg -> loc)
-     (newcode: LTL.code) : LTL.code :=
-  let oldentry := RTL.fn_entrypoint f in
-  let newentry := RTL.fn_nextpc f in
-  let undefs :=
-    Regset.elements (reg_list_dead (RTL.fn_params f)
-                                   (transfer f oldentry live!!oldentry)) in
-  PTree.set
-    newentry
-    (add_entry (RTL.fn_sig f)
-               (List.map assign (RTL.fn_params f))
-               (List.map assign undefs)
-               oldentry)
-    newcode.
-
-Lemma transf_entrypoint_wf:
+Lemma transf_body_wf:
   forall (f: RTL.function) (live: PMap.t Regset.t) (assign: reg -> loc),
-  let tc1 := PTree.map (transf_instr f live assign) (RTL.fn_code f) in
-  let tc2 := transf_entrypoint f live assign tc1 in
-  forall (pc: node), Plt pc (Psucc (RTL.fn_nextpc f)) \/ tc2!pc = None.
+  let tc := PTree.map (transf_instr f live assign) (RTL.fn_code f) in
+  forall (pc: node), Plt pc (RTL.fn_nextpc f) \/ tc!pc = None.
 Proof.
-  intros. case (plt pc (Psucc (RTL.fn_nextpc f))); intro.
-  left. auto. 
-  right. 
-  assert (pc <> RTL.fn_nextpc f).
-  red; intro. subst pc. elim n. apply Plt_succ.
-  assert (~ (Plt pc (RTL.fn_nextpc f))).
-  red; intro. elim n. apply Plt_trans_succ; auto.
-  unfold tc2. unfold transf_entrypoint. 
-  rewrite PTree.gso; auto. 
-  unfold tc1. rewrite PTree.gmap. 
-  elim (RTL.fn_code_wf f pc); intro.
-  contradiction. unfold option_map. rewrite H1. auto.
+  intros. elim (RTL.fn_code_wf f pc); intro.
+  left. auto. right. unfold tc. rewrite PTree.gmap.
+  unfold option_map. rewrite H. auto.
 Qed.
 
+Definition transf_fun (f: RTL.function) (live: PMap.t Regset.t)
+                      (assign: reg -> loc) : LTL.function :=
+  LTL.mkfunction
+     (RTL.fn_sig f)
+     (List.map assign (RTL.fn_params f))
+     (RTL.fn_stacksize f)
+     (PTree.map (transf_instr f live assign) (RTL.fn_code f))
+     (RTL.fn_entrypoint f)
+     (RTL.fn_nextpc f)
+     (transf_body_wf f live assign).
+
 (** The translation of a function performs liveness analysis,
   construction and coloring of the inference graph, and per-instruction
   transformation as described above. *)
 
-Definition transf_function (f: RTL.function) : option LTL.function :=
+Definition live0 (f: RTL.function) (live: PMap.t Regset.t) :=
+  transfer f f.(RTL.fn_entrypoint) live!!(f.(RTL.fn_entrypoint)).
+
+Open Scope string_scope.
+
+Definition transf_function (f: RTL.function) : res LTL.function :=
   match type_function f with
-  | None => None
-  | Some env =>
+  | Error msg => Error msg
+  | OK env =>
     match analyze f with
-    | None => None
+    | None => Error (msg "Liveness analysis failure")
     | Some live =>
-      let pc0 := f.(RTL.fn_entrypoint) in
-      let live0 := transfer f pc0 live!!pc0 in
-      match regalloc f live live0 env with
-      | None => None
-      | Some assign =>
-          Some (LTL.mkfunction
-            (RTL.fn_sig f)
-            (RTL.fn_stacksize f)
-            (transf_entrypoint f live assign
-                   (PTree.map (transf_instr f live assign) (RTL.fn_code f)))
-            (RTL.fn_nextpc f)
-            (transf_entrypoint_wf f live assign))
-      end
+        match regalloc f live (live0 f live) env with
+        | None => Error (msg "Incorrect graph coloring")
+        | Some assign => OK (transf_fun f live assign)
+        end
     end
   end.
 
-Definition transf_fundef (fd: RTL.fundef) : option LTL.fundef :=
-  transf_partial_fundef transf_function fd.
+Definition transf_fundef (fd: RTL.fundef) : res LTL.fundef :=
+  AST.transf_partial_fundef transf_function fd.
 
-Definition transf_program (p: RTL.program) : option LTL.program :=
+Definition transf_program (p: RTL.program) : res LTL.program :=
   transform_partial_program transf_fundef p.