Changeset 2740


Ignore:
Timestamp:
Feb 27, 2013, 4:59:31 PM (7 years ago)
Author:
sacerdot
Message:

Graph colouring terminated up to Uses that will be implemented
in Matita.

Location:
extracted
Files:
3 added
10 edited

Legend:

Unmodified
Added
Removed
  • extracted/eRTLptrToLTL.ml

    r2730 r2740  
    805805    Liveness.analyse_liveness the_fixpoint globals (Types.pi1 int_fun)
    806806  in
    807   let coloured_graph0 = build after in
     807  let coloured_graph0 = build globals (Types.pi1 int_fun) after in
    808808  let stack_sz =
    809809    Nat.plus coloured_graph0.Interference.spilled_no
  • extracted/interference.ml

    r2730 r2740  
    297297    Obj.magic (fun _ dH -> dH __ __ __ __)) y
    298298
    299 type coloured_graph_computer = Fixpoints.valuation -> coloured_graph
    300 
     299type coloured_graph_computer =
     300  AST.ident List.list -> Joint.joint_internal_function -> Fixpoints.valuation
     301  -> coloured_graph
     302
  • extracted/interference.mli

    r2717 r2740  
    214214  Fixpoints.valuation -> coloured_graph -> coloured_graph -> __
    215215
    216 type coloured_graph_computer = Fixpoints.valuation -> coloured_graph
    217 
     216type coloured_graph_computer =
     217  AST.ident List.list -> Joint.joint_internal_function -> Fixpoints.valuation
     218  -> coloured_graph
     219
  • extracted/untrusted/coloring.ml

    r2738 r2740  
    5656
    5757let colors : ColorSet.t =
    58   List.foldr
    59    (fun reg set -> HwRegisterSet.add reg set)
    60    HwRegisterSet.empty I8051.registersAllocatable
     58 Untrusted_interference.hwregisterset_of_list I8051.registersAllocatable
    6159
    6260(* This is the number of available colors. *)
  • extracted/untrusted/compute_colouring.ml

    r2738 r2740  
    1 (* We try first with a stupid colourer: we spill everything *)
     1(* Adapted from Pottier's PP compiler *)
    22
    3 let colour_graph graph = assert false
     3let colour_graph globals int_fun liveafter =
     4  (* Build an interference graph for this function, and color
     5     it. Define a function that allows consulting the coloring. *)
     6
     7  let module G = struct
     8    let graph = Build.build globals int_fun liveafter
     9    let uses = Uses.examine_internal int_fun
     10    let verbose = false
     11(*
     12    let () =
     13      if verbose then
     14        Printf.printf "Starting hardware register allocation for %s.\n" f
     15*)
     16  end in
     17
     18  let module C = Coloring.Color (G) in
     19
     20  let lookup r =
     21    Untrusted_interference.Vertex.Map.find (Untrusted_interference.lookup G.graph r) C.coloring
     22  in
     23
     24  (* Restrict the interference graph to concern spilled vertices only,
     25     and color it again, this time using stack slots as colors. *)
     26
     27  let module H = struct
     28    let graph = Untrusted_interference.droph (Untrusted_interference.restrict G.graph (fun v ->
     29      match Untrusted_interference.Vertex.Map.find v C.coloring with
     30      | Coloring.Spill ->
     31          true
     32      | Coloring.Color _ ->
     33          false
     34    ))
     35    let verbose = false
     36(*
     37    let () =
     38      if verbose then
     39        Printf.printf "Starting stack slot allocation for %s.\n" f
     40*)
     41  end in
     42
     43  let module S = Spill.Color (H) in
     44
     45  (* Define a new function that consults both colorings at once. *)
     46
     47  let lookup r =
     48   match r with
     49      Types.Inl r ->
     50       (match lookup r with
     51       | Coloring.Spill ->
     52           Interference.Decision_spill (Glue.matitanat_of_int (Untrusted_interference.Vertex.Map.find (Untrusted_interference.lookup H.graph r) S.coloring))
     53       | Coloring.Color color ->
     54           Interference.Decision_colour color)
     55    | Types.Inr r -> Interference.Decision_colour r
     56  in
     57
     58   { Interference.colouring = lookup;
     59     spilled_no = Glue.matitanat_of_int S.locals
     60   }
  • extracted/untrusted/compute_colouring.mli

    r2738 r2740  
    1 val colour_graph : Interference.coloured_graph_computer
     1val colour_graph :
     2 AST.ident List.list ->
     3  Joint.joint_internal_function ->
     4   Fixpoints.valuation ->
     5    Interference.coloured_graph
  • extracted/untrusted/glue.ml

    r2738 r2740  
    1010  in
    1111    aux 1 (Vector.reverse0 Nat.O v)
     12
     13let option_of_matitaoption =
     14 function
     15    Types.None -> None
     16  | Types.Some v -> Some v
     17
     18let rec matitanat_of_int n =
     19 if n = 0 then Nat.O
     20 else if n < 0 then assert false
     21 else Nat.S (matitanat_of_int (n-1))
  • extracted/untrusted/glue.mli

    r2738 r2740  
    11val int_of_bitvector : BitVector.bitVector -> int
     2
     3val option_of_matitaoption: 'a Types.option -> 'a option
     4
     5val matitanat_of_int : int -> Nat.nat
  • extracted/untrusted/untrusted_interference.ml

    r2738 r2740  
    33module HwOrdReg = struct type t = hwregister let compare = compare end
    44module HwRegisterSet = Set.Make (HwOrdReg)
     5
     6let hwregisterset_of_list =
     7  List.foldr
     8   (fun reg set -> HwRegisterSet.add reg set)
     9   HwRegisterSet.empty
    510
    611(* Pasted from Pottier's PP compiler *)
  • extracted/untrusted/untrusted_interference.mli

    r2738 r2740  
    22type hwregister = I8051.register
    33module HwRegisterSet : Set.S with type elt = hwregister
     4
     5val hwregisterset_of_list : hwregister List.list -> HwRegisterSet.t
    46
    57(* Pasted from Pottier's PP compiler *)
Note: See TracChangeset for help on using the changeset viewer.