Reorganized the development, modularizing away machine-dependent parts.

Started to merge the ARM code generator.
Started to add support for PowerPC/EABI.
Use ocamlbuild to construct executable from Caml files.


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

1 files changed, 0 insertions, 625 deletions

diff --git a/caml/Coloringaux.ml b/caml/Coloringaux.ml
deleted file mode 100644
index f11738df..00000000
--- a/caml/Coloringaux.ml
+++ /dev/null
@@ -1,625 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-open Camlcoq
-open Datatypes
-open BinPos
-open BinInt
-open AST
-open Maps
-open Registers
-open Locations
-open RTL
-open RTLtyping
-open InterfGraph
-open Conventions
-
-(* George-Appel graph coloring *)
-
-(* \subsection{Internal representation of the interference graph} *)
-
-(* To implement George-Appel coloring, we first transform the representation
-   of the interference graph, switching to the following 
-   imperative representation that is well suited to the coloring algorithm. *)
-
-(* Each node of the graph (i.e. each pseudo-register) is represented as
-   follows. *)
-
-type node =
-  { ident: reg;                         (*r register identifier *)
-    typ: typ;                           (*r its type *)
-    regclass: int;                      (*r identifier of register class *)
-    spillcost: float;                   (*r estimated cost of spilling *)
-    mutable adjlist: node list;         (*r all nodes it interferes with *)
-    mutable degree: int;                (*r number of adjacent nodes *)
-    mutable movelist: move list;        (*r list of moves it is involved in *)
-    mutable alias: node option;         (*r [Some n] if coalesced with [n] *)
-    mutable color: loc option;          (*r chosen color *)
-    mutable nstate: nodestate;          (*r in which set of nodes it is *)
-    mutable nprev: node;                (*r for double linking *)
-    mutable nnext: node                 (*r for double linking *)
-  }
-
-(* These are the possible states for nodes. *)
-
-and nodestate =
-  | Colored
-  | Initial
-  | SimplifyWorklist
-  | FreezeWorklist
-  | SpillWorklist
-  | CoalescedNodes
-  | SelectStack
-
-(* Each move (i.e. wish to be put in the same location) is represented
-   as follows. *)
-
-and move =
-  { src: node;                          (*r source of the move *)
-    dst: node;                          (*r destination of the move *)
-    mutable mstate: movestate;          (*r in which set of moves it is *)
-    mutable mprev: move;                (*r for double linking *)
-    mutable mnext: move                 (*r for double linking *)
-  }
-
-(* These are the possible states for moves *)
-
-and movestate =
-  | CoalescedMoves
-  | ConstrainedMoves
-  | FrozenMoves
-  | WorklistMoves
-  | ActiveMoves
-
-(* The algorithm manipulates partitions of the nodes and of the moves
-   according to their states, frequently moving a node or a move from
-   a state to another, and frequently enumerating all nodes or all moves
-   of a given state.  To support these operations efficiently,
-   nodes or moves having the same state are put into imperative doubly-linked
-   lists, allowing for constant-time insertion and removal, and linear-time
-   scanning.  We now define the operations over these doubly-linked lists. *)
-
-module DLinkNode = struct
-  type t = node
-  let make state =
-    let rec empty =
-      { ident = Coq_xH; typ = Tint; regclass = 0;
-        adjlist = []; degree = 0; spillcost = 0.0;
-        movelist = []; alias = None; color = None;
-        nstate = state; nprev = empty; nnext = empty }
-    in empty
-  let dummy = make Colored
-  let clear dl = dl.nnext <- dl; dl.nprev <- dl
-  let notempty dl = dl.nnext != dl
-  let insert n dl =
-    n.nstate <- dl.nstate;
-    n.nnext <- dl.nnext; n.nprev <- dl;
-    dl.nnext.nprev <- n; dl.nnext <- n
-  let remove n dl =
-    assert (n.nstate = dl.nstate);
-    n.nnext.nprev <- n.nprev; n.nprev.nnext <- n.nnext
-  let move n dl1 dl2 =
-    remove n dl1; insert n dl2
-  let pick dl =
-    let n = dl.nnext in remove n dl; n
-  let iter f dl =
-    let rec iter n = if n != dl then (f n; iter n.nnext)
-    in iter dl.nnext
-  let fold f dl accu =
-    let rec fold n accu = if n == dl then accu else fold n.nnext (f n accu)
-    in fold dl.nnext accu
-end
-
-module DLinkMove = struct
-  type t = move
-  let make state =
-    let rec empty =
-      { src = DLinkNode.dummy; dst = DLinkNode.dummy; 
-        mstate = state; mprev = empty; mnext = empty }
-    in empty
-  let dummy = make CoalescedMoves
-  let clear dl = dl.mnext <- dl; dl.mprev <- dl
-  let notempty dl = dl.mnext != dl
-  let insert m dl =
-    m.mstate <- dl.mstate;
-    m.mnext <- dl.mnext; m.mprev <- dl;
-    dl.mnext.mprev <- m; dl.mnext <- m
-  let remove m dl =
-    assert (m.mstate = dl.mstate);
-    m.mnext.mprev <- m.mprev; m.mprev.mnext <- m.mnext
-  let move m dl1 dl2 =
-    remove m dl1; insert m dl2
-  let pick dl =
-    let m = dl.mnext in remove m dl; m
-  let iter f dl =
-    let rec iter m = if m != dl then (f m; iter m.mnext)
-    in iter dl.mnext
-  let fold f dl accu =
-    let rec fold m accu = if m == dl then accu else fold m.mnext (f m accu)
-    in fold dl.mnext accu
-end
-
-(* \subsection{The George-Appel algorithm} *)
-
-(* Below is a straigthforward translation of the pseudo-code at the end
-   of the TOPLAS article by George and Appel.  Two bugs were fixed
-   and are marked as such.  Please refer to the article for explanations. *)
-
-(* Low-degree, non-move-related nodes *)
-let simplifyWorklist = DLinkNode.make SimplifyWorklist
-
-(* Low-degree, move-related nodes *)
-let freezeWorklist = DLinkNode.make FreezeWorklist
-
-(* High-degree nodes *)
-let spillWorklist = DLinkNode.make SpillWorklist
-
-(* Nodes that have been coalesced *)
-let coalescedNodes = DLinkNode.make CoalescedNodes
-
-(* Moves that have been coalesced *)
-let coalescedMoves = DLinkMove.make CoalescedMoves
-
-(* Moves whose source and destination interfere *)
-let constrainedMoves = DLinkMove.make ConstrainedMoves
-
-(* Moves that will no longer be considered for coalescing *)
-let frozenMoves = DLinkMove.make FrozenMoves
-
-(* Moves enabled for possible coalescing *)
-let worklistMoves = DLinkMove.make WorklistMoves
-
-(* Moves not yet ready for coalescing *)
-let activeMoves = DLinkMove.make ActiveMoves
-
-(* Initialization of all global data structures *)
-
-let init() =
-  DLinkNode.clear simplifyWorklist;
-  DLinkNode.clear freezeWorklist;
-  DLinkNode.clear spillWorklist;
-  DLinkNode.clear coalescedNodes;
-  DLinkMove.clear coalescedMoves;
-  DLinkMove.clear frozenMoves;
-  DLinkMove.clear worklistMoves;
-  DLinkMove.clear activeMoves
-
-(* Determine if two nodes interfere *)
-
-let interfere n1 n2 =
-  if n1.degree < n2.degree
-  then List.memq n2 n1.adjlist
-  else List.memq n1 n2.adjlist
-
-(* Add an edge to the graph.  Assume edge is not in graph already *)
-
-let addEdge n1 n2 =
-  n1.adjlist <- n2 :: n1.adjlist;
-  n1.degree  <- 1 + n1.degree;
-  n2.adjlist <- n1 :: n2.adjlist;
-  n2.degree  <- 1 + n2.degree
-
-(* Apply the given function to the relevant adjacent nodes of a node *)
-
-let iterAdjacent f n =
-  List.iter
-    (fun n ->
-      match n.nstate with
-      | SelectStack | CoalescedNodes -> ()
-      | _ -> f n)
-    n.adjlist
-
-(* Determine the moves affecting a node *)
-
-let moveIsActiveOrWorklist m =
-  match m.mstate with
-  | ActiveMoves | WorklistMoves -> true
-  | _ -> false
-
-let nodeMoves n =
-  List.filter moveIsActiveOrWorklist n.movelist
-
-(* Determine whether a node is involved in a move *)
-
-let moveRelated n =
-  List.exists moveIsActiveOrWorklist n.movelist
-
-(*i
-(* Check invariants *)
-
-let degreeInvariant n =
-  let c = ref 0 in
-  iterAdjacent (fun n -> incr c) n;
-  if !c <> n.degree then
-    fatal_error("degree invariant violated by " ^ name_of_node n)
-
-let simplifyWorklistInvariant n =
-  if n.degree < num_available_registers.(n.regclass)
-  && not (moveRelated n)
-  then ()
-  else fatal_error("simplify worklist invariant violated by " ^ name_of_node n)
-
-let freezeWorklistInvariant n =
-  if n.degree < num_available_registers.(n.regclass)
-  && moveRelated n
-  then ()
-  else fatal_error("freeze worklist invariant violated by " ^ name_of_node n)
-
-let spillWorklistInvariant n =
-  if n.degree >= num_available_registers.(n.regclass)
-  then ()
-  else fatal_error("spill worklist invariant violated by " ^ name_of_node n)
-
-let checkInvariants () =
-  DLinkNode.iter
-    (fun n -> degreeInvariant n; simplifyWorklistInvariant n)
-    simplifyWorklist;
-  DLinkNode.iter
-    (fun n -> degreeInvariant n; freezeWorklistInvariant n)
-    freezeWorklist;
-  DLinkNode.iter
-    (fun n -> degreeInvariant n; spillWorklistInvariant n)
-    spillWorklist
-i*)
-
-(* Register classes *)
-
-let class_of_type = function Tint -> 0 | Tfloat -> 1
-
-let num_register_classes = 2
-
-let caller_save_registers = [|
-  Array.of_list Conventions.int_caller_save_regs;
-  Array.of_list Conventions.float_caller_save_regs
-|]
-
-let callee_save_registers = [|
-  Array.of_list Conventions.int_callee_save_regs;
-  Array.of_list Conventions.float_callee_save_regs
-|]
-
-let num_available_registers = 
-  [| Array.length caller_save_registers.(0)
-           + Array.length callee_save_registers.(0);
-     Array.length caller_save_registers.(1)
-           + Array.length callee_save_registers.(1) |]
-
-(* Build the internal representation of the graph *)
-
-let nodeOfReg r typenv spillcosts =
-  let ty = typenv r in
-  { ident = r; typ = ty; regclass = class_of_type ty;
-    spillcost = (try float(Hashtbl.find spillcosts r) with Not_found -> 0.0);
-    adjlist = []; degree = 0; movelist = []; alias = None;
-    color = None;
-    nstate = Initial;
-    nprev = DLinkNode.dummy; nnext = DLinkNode.dummy }
-
-let nodeOfMreg mr =
-  let ty = mreg_type mr in
-  { ident = Coq_xH; typ = ty; regclass = class_of_type ty;
-    spillcost = 0.0;
-    adjlist = []; degree = 0; movelist = []; alias = None;
-    color = Some (R mr);
-    nstate = Colored;
-    nprev = DLinkNode.dummy; nnext = DLinkNode.dummy }
-
-let build g typenv spillcosts =
-  (* Associate an internal node to each pseudo-register and each location *)
-  let reg_mapping = Hashtbl.create 27
-  and mreg_mapping = Hashtbl.create 27 in
-  let find_reg_node r =
-    try
-      Hashtbl.find reg_mapping r
-    with Not_found ->
-      let n = nodeOfReg r typenv spillcosts in
-      Hashtbl.add reg_mapping r n;
-      n
-  and find_mreg_node mr =
-    try
-      Hashtbl.find mreg_mapping mr
-    with Not_found ->
-      let n = nodeOfMreg mr in
-      Hashtbl.add mreg_mapping mr n;
-      n in
-  (* Fill the adjacency lists and compute the degrees. *)
-  SetRegReg.fold
-    (fun (Coq_pair(r1, r2)) () ->
-      addEdge (find_reg_node r1) (find_reg_node r2))
-    g.interf_reg_reg ();
-  SetRegMreg.fold
-    (fun (Coq_pair(r1, mr2)) () ->
-      addEdge (find_reg_node r1) (find_mreg_node mr2))
-    g.interf_reg_mreg ();
-  (* Process the moves and insert them in worklistMoves *)
-  let add_move n1 n2 =
-    let m =
-      { src = n1; dst = n2; mstate = WorklistMoves;
-        mnext = DLinkMove.dummy; mprev = DLinkMove.dummy } in
-    n1.movelist <- m :: n1.movelist;
-    n2.movelist <- m :: n2.movelist;
-    DLinkMove.insert m worklistMoves in
-  SetRegReg.fold
-    (fun (Coq_pair(r1, r2)) () ->
-      add_move (find_reg_node r1) (find_reg_node r2))
-    g.pref_reg_reg ();
-  SetRegMreg.fold
-    (fun (Coq_pair(r1, mr2)) () ->
-      add_move (find_reg_node r1) (find_mreg_node mr2))
-    g.pref_reg_mreg ();
-  (* Initial partition of nodes into spill / freeze / simplify *)
-  Hashtbl.iter
-    (fun r n ->
-      assert (n.nstate = Initial);
-      let k = num_available_registers.(n.regclass) in
-      if n.degree >= k then
-        DLinkNode.insert n spillWorklist
-      else if moveRelated n then
-        DLinkNode.insert n freezeWorklist
-      else
-        DLinkNode.insert n simplifyWorklist)
-    reg_mapping;
-  reg_mapping
-
-(* Enable moves that have become low-degree related *)
-
-let enableMoves n =
-  List.iter
-    (fun m ->
-      if m.mstate = ActiveMoves
-      then DLinkMove.move m activeMoves worklistMoves)
-    (nodeMoves n)
-
-(* Simulate the removal of a node from the graph *)
-
-let decrementDegree n =
-  let k = num_available_registers.(n.regclass) in
-  let d = n.degree in
-  n.degree <- d - 1;
-  if d = k then begin
-    enableMoves n;
-    iterAdjacent enableMoves n;
-    if n.nstate <> Colored then begin
-      if moveRelated n
-      then DLinkNode.move n spillWorklist freezeWorklist
-      else DLinkNode.move n spillWorklist simplifyWorklist
-    end
-  end
-
-(* Simulate the effect of combining nodes [n1] and [n3] on [n2],
-   where [n2] is a node adjacent to [n3]. *)
-
-let combineEdge n1 n2 =
-  assert (n1 != n2);
-  if interfere n1 n2 then begin
-    decrementDegree n2
-  end else begin
-    n1.adjlist <- n2 :: n1.adjlist;
-    n2.adjlist <- n1 :: n2.adjlist;
-    n1.degree  <- n1.degree + 1
-  end
-
-(* Simplification of a low-degree node *)
-
-let simplify () =
-  let n = DLinkNode.pick simplifyWorklist in
-  (*i Printf.printf "Simplifying %s\n" (name_of_node n); i*)
-  n.nstate <- SelectStack;
-  iterAdjacent decrementDegree n;
-  n
-
-(* Briggs' conservative coalescing criterion *)
-
-let canConservativelyCoalesce n1 n2 =
-  let seen = ref Regset.empty in
-  let k = num_available_registers.(n1.regclass) in
-  let c = ref 0 in
-  let consider n =
-    if not (Regset.mem n.ident !seen) then begin
-      seen := Regset.add n.ident !seen;
-      if n.degree >= k then incr c
-    end in
-  iterAdjacent consider n1;
-  iterAdjacent consider n2;
-  !c < k
-
-(* Update worklists after a move was processed *)
-
-let addWorkList u =
-  if (not (u.nstate = Colored))
-  && u.degree < num_available_registers.(u.regclass)
-  && (not (moveRelated u))
-  then DLinkNode.move u freezeWorklist simplifyWorklist
-
-(* Return the canonical representative of a possibly coalesced node *)
-
-let rec getAlias n =
-  match n.alias with None -> n | Some n' -> getAlias n'
-
-(* Combine two nodes *)
-
-let combine u v =
-  (*i Printf.printf "Combining %s and %s\n" (name_of_node u) (name_of_node v); i*)
-  if v.nstate = FreezeWorklist
-  then DLinkNode.move v freezeWorklist coalescedNodes
-  else DLinkNode.move v spillWorklist coalescedNodes;
-  v.alias <- Some u;
-  u.movelist <- u.movelist @ v.movelist;
-  iterAdjacent (combineEdge u) v;  (*r original code using [decrementDegree] is buggy *)
-  enableMoves v;                   (*r added as per Appel's book erratum *)
-  if u.degree >= num_available_registers.(u.regclass)
-  && u.nstate = FreezeWorklist
-  then DLinkNode.move u freezeWorklist spillWorklist
-
-(* Attempt coalescing *)
-
-let coalesce () =
-  let m = DLinkMove.pick worklistMoves in
-  let x = getAlias m.src and y = getAlias m.dst in
-  let (u, v) = if y.nstate = Colored then (y, x) else (x, y) in
-  if u == v then begin
-    DLinkMove.insert m coalescedMoves;
-    addWorkList u
-  end else if v.nstate = Colored || interfere u v then begin
-    DLinkMove.insert m constrainedMoves;
-    addWorkList u;
-    addWorkList v
-  end else if canConservativelyCoalesce u v then begin
-    DLinkMove.insert m coalescedMoves;
-    combine u v;
-    addWorkList u
-  end else begin
-    DLinkMove.insert m activeMoves    
-  end
-
-(* Freeze moves associated with node [u] *)
-
-let freezeMoves u =
-  let au = getAlias u in
-  let freeze m =
-    let y = getAlias m.src in
-    let v = if y == au then getAlias m.dst else y in
-    DLinkMove.move m activeMoves frozenMoves;
-    if not (moveRelated v)
-    && v.degree < num_available_registers.(v.regclass)
-    && v.nstate <> Colored
-    then DLinkNode.move v freezeWorklist simplifyWorklist in
-  List.iter freeze (nodeMoves u)
-
-(* Pick a move and freeze it *)
-
-let freeze () =
-  let u = DLinkNode.pick freezeWorklist in
-  (*i Printf.printf "Freezing %s\n" (name_of_node u); i*)
-  DLinkNode.insert u simplifyWorklist;
-  freezeMoves u
-
-(* Chaitin's cost measure *)
-
-let spillCost n = n.spillcost /. float n.degree
-
-(* Spill a node *)
-
-let selectSpill () =
-  (* Find a spillable node of minimal cost *)
-  let (n, cost) =
-    DLinkNode.fold
-      (fun n (best_node, best_cost as best) ->
-        let cost = spillCost n in
-        if cost < best_cost then (n, cost) else best)
-      spillWorklist (DLinkNode.dummy, infinity) in
-  assert (n != DLinkNode.dummy);
-  DLinkNode.remove n spillWorklist;
-  (*i Printf.printf "Spilling %s\n" (name_of_node n); i*)
-  freezeMoves n;
-  n.nstate <- SelectStack;
-  iterAdjacent decrementDegree n;
-  n
-
-(* Produce the order of nodes that we'll use for coloring *)
-
-let rec nodeOrder stack =
-  (*i checkInvariants(); i*)
-  if DLinkNode.notempty simplifyWorklist then
-    (let n = simplify() in nodeOrder (n :: stack))
-  else if DLinkMove.notempty worklistMoves then
-    (coalesce(); nodeOrder stack)
-  else if DLinkNode.notempty freezeWorklist then
-    (freeze(); nodeOrder stack)
-  else if DLinkNode.notempty spillWorklist then
-    (let n = selectSpill() in nodeOrder (n :: stack))
-  else
-    stack
-
-(* Assign a color (i.e. a hardware register or a stack location)
-   to a node.  The color is chosen among the colors that are not
-   assigned to nodes with which this node interferes.  The choice
-   is guided by the following heuristics: consider first caller-save
-   hardware register of the correct type; second, callee-save registers;
-   third, a stack location.  Callee-save registers and stack locations
-   are ``expensive'' resources, so we try to minimize their number
-   by picking the smallest available callee-save register or stack location.
-   In contrast, caller-save registers are ``free'', so we pick an
-   available one pseudo-randomly. *)
-
-module Locset =
-  Set.Make(struct type t = loc let compare = compare end)
-
-let start_points = Array.make num_register_classes 0
-
-let find_reg conflicts regclass =
-  let rec find avail curr last =
-    if curr >= last then None else begin
-      let l = R avail.(curr) in
-      if Locset.mem l conflicts
-      then find avail (curr + 1) last
-      else Some l
-    end in
-  let caller_save = caller_save_registers.(regclass)
-  and callee_save = callee_save_registers.(regclass)
-  and start = start_points.(regclass) in
-  match find caller_save start (Array.length caller_save) with
-  | Some _ as res ->
-      start_points.(regclass) <-
-        (if start + 1 < Array.length caller_save then start + 1 else 0);
-      res
-  | None ->
-      match find caller_save 0 start with
-      | Some _ as res ->
-          start_points.(regclass) <-
-            (if start + 1 < Array.length caller_save then start + 1 else 0);
-          res
-      | None ->
-          find callee_save 0 (Array.length callee_save)
-
-let find_slot conflicts typ =
-  let rec find curr =
-    let l = S(Local(curr, typ)) in
-    if Locset.mem l conflicts then find (coq_Zsucc curr) else l
-  in find Z0
-
-let assign_color n =
-  let conflicts = ref Locset.empty in
-  List.iter
-    (fun n' ->
-      match (getAlias n').color with
-      | None -> ()
-      | Some l -> conflicts := Locset.add l !conflicts)
-    n.adjlist;
-  match find_reg !conflicts n.regclass with
-  | Some loc ->
-      n.color <- Some loc
-  | None ->
-      n.color <- Some (find_slot !conflicts n.typ)
-
-(* Extract the location of a node *)
-
-let location_of_node n =
-  match n.color with
-  | None -> assert false
-  | Some loc -> loc
-
-(* Estimate spilling costs - TODO *)
-
-let spill_costs f = Hashtbl.create 7
-
-(* This is the entry point for graph coloring. *)
-
-let graph_coloring (f: coq_function) (g: graph) (env: regenv) (regs: Regset.t)
-                   : (reg -> loc) =
-  init();
-  Array.fill start_points 0 num_register_classes 0;
-  let mapping = build g env (spill_costs f) in
-  List.iter assign_color (nodeOrder []);
-  fun r ->
-    try location_of_node (getAlias (Hashtbl.find mapping r))
-    with Not_found -> R IT1 (* any location *)