Changeset 1144


Ignore:
Timestamp:
Aug 30, 2011, 3:53:21 PM (8 years ago)
Author:
mulligan
Message:

added build.ma file. matita bug found

Location:
src/ERTL
Files:
1 added
2 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1128 r1144  
    77  λf.
    88  λint_fun: ertl_internal_function.
    9     mk_ltl_internal_function ?
    10       (ertl_if_luniverse int_fun)
    11       (ertl_if_runiverse int_fun)
    12       (ertl_if_stacksize int_fun)
    13       (ertl_if_graph int_fun)
    14       ?
    15       ?.
     9
     10  let fresh_label () = Label.Gen.fresh int_fun.ERTL.f_luniverse in
     11
     12  let add_graph lbl stmt = graph := Label.Map.add lbl stmt !graph in
     13
     14  let generate stmt =
     15    let l = fresh_label () in
     16    add_graph l stmt ;
     17    l in
     18
     19  (* Build an interference graph for this function, and color
     20     it. Define a function that allows consulting the coloring. *)
     21
     22  let module G = struct
     23    let liveafter, graph = Build.build int_fun
     24    let uses = Uses.examine_internal int_fun
     25    let verbose = false
     26    let () =
     27      if verbose then
     28        Printf.printf "Starting hardware register allocation for %s.\n" f
     29  end in
     30
     31  let module C = Coloring.Color (G) in
     32
     33  let lookup r =
     34    Interference.Vertex.Map.find (Interference.lookup G.graph r) C.coloring
     35  in
     36
     37  (* Restrict the interference graph to concern spilled vertices only,
     38     and color it again, this time using stack slots as colors. *)
     39
     40  let module H = struct
     41    let graph = Interference.droph (Interference.restrict G.graph (fun v ->
     42      match Interference.Vertex.Map.find v C.coloring with
     43      | Coloring.Spill ->
     44          true
     45      | Coloring.Color _ ->
     46          false
     47    ))
     48    let verbose = false
     49    let () =
     50      if verbose then
     51        Printf.printf "Starting stack slot allocation for %s.\n" f
     52  end in
     53
     54  let module S = Spill.Color (H) in
     55
     56  (* Define a new function that consults both colorings at once. *)
     57
     58  let lookup r =
     59    match lookup r with
     60    | Coloring.Spill ->
     61        ERTLToLTLI.Spill (Interference.Vertex.Map.find (Interference.lookup H.graph r) S.coloring)
     62    | Coloring.Color color ->
     63        ERTLToLTLI.Color color
     64  in
     65
     66  (* We are now ready to instantiate the functor that deals with the
     67     translation of instructions. The reason why we make this a
     68     separate functor is purely pedagogical. Smaller modules are
     69     easier to understand. *)
     70
     71  (* We add the additional stack size required for spilled register to the stack
     72     size previously required for the function: this is the final stack size
     73     required for the locals. *)
     74
     75  let locals = S.locals + int_fun.ERTL.f_stacksize in
     76
     77  (* The full stack size is then the size of the locals in the stack plus the
     78     size of the formal parameters of the function. *)
     79
     80  let stacksize = int_fun.ERTL.f_params + locals in
     81
     82  let module I = ERTLToLTLI.Make (struct
     83    let lookup = lookup
     84    let generate = generate
     85    let fresh_label = fresh_label
     86    let add_graph = add_graph
     87    let locals = locals
     88    let stacksize = stacksize
     89  end) in
     90
     91  (* Translate the instructions in the existing control flow graph.
     92     Pure instructions whose destination pseudo-register is dead are
     93     eliminated on the fly. *)
     94
     95  let () =
     96    Label.Map.iter (fun label stmt ->
     97      let stmt =
     98        match Liveness.eliminable (G.liveafter label) stmt with
     99        | Some successor ->
     100            LTL.St_skip successor
     101        | None ->
     102            I.translate_statement stmt
     103      in
     104      graph := Label.Map.add label stmt !graph
     105    ) int_fun.ERTL.f_graph
     106  in
     107
     108  (* Build a [LTL] function. *)
     109
     110  {
     111    LTL.f_luniverse = int_fun.ERTL.f_luniverse;
     112    LTL.f_stacksize = stacksize ;
     113    LTL.f_entry = int_fun.ERTL.f_entry;
     114    LTL.f_exit = int_fun.ERTL.f_exit;
     115    LTL.f_graph = !graph
     116  }
    16117
    17118definition translate_funct ≝
  • src/ERTL/liveness.ma

    r1124 r1144  
    4949  | ertl_st_push _ l ⇒ [ l ]
    5050  | ertl_st_pop _ l ⇒ [ l ]
    51   | ertl_st_addr_h _ _ l ⇒ [ l ]
    52   | ertl_st_addr_l _ _ l ⇒ [ l ]
     51  | ertl_st_addr _ _ _ l ⇒ [ l ]
    5352  | ertl_st_int _ _ l ⇒ [ l ]
    5453  | ertl_st_move _ _ l ⇒ [ l ]
    55   | ertl_st_opaccs_a _ _ _ _ l ⇒ [ l ]
    56   | ertl_st_opaccs_b _ _ _ _ l ⇒ [ l ]
     54  | ertl_st_opaccs _ _ _ _ _ l ⇒ [ l ]
    5755  | ertl_st_op1 _ _ _ l ⇒ [ l ]
    5856  | ertl_st_op2 _ _ _ _ l ⇒ [ l ]
     
    148146  | ertl_st_pop r _ ⇒ lattice_psingleton r
    149147  | ertl_st_int r _ _ ⇒ lattice_psingleton r
    150   | ertl_st_addr_h r _ _ ⇒ lattice_psingleton r
    151   | ertl_st_addr_l r _ _ ⇒ lattice_psingleton r
     148  | ertl_st_addr r1 r2 _ _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    152149  | ertl_st_move r _ _ ⇒ lattice_psingleton r
    153   | ertl_st_opaccs_a _ r _ _ _ ⇒ lattice_psingleton r
    154   | ertl_st_opaccs_b _ r _ _ _ ⇒ lattice_psingleton r
     150  (* XXX: change from o'caml *)
     151  | ertl_st_opaccs _ r1 r2 _ _ _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    155152  | ertl_st_load r _ _ _ ⇒ lattice_psingleton r
    156153  | ertl_st_set_hdw r _ _ ⇒ lattice_hsingleton r
     
    180177  | ertl_st_frame_size _ _ ⇒ lattice_bottom
    181178  | ertl_st_pop _ _ ⇒ lattice_bottom
    182   | ertl_st_addr_h _ _ _ ⇒ lattice_bottom
    183   | ertl_st_addr_l _ _ _ ⇒ lattice_bottom
     179  | ertl_st_addr _ _ _ _ ⇒ lattice_bottom
    184180  | ertl_st_int _ _ _ ⇒ lattice_bottom
    185181  | ertl_st_clear_carry _ ⇒ lattice_bottom
     
    187183    (* Reads the hardware registers that are used to pass parameters. *)
    188184  | ertl_st_call_id _ nparams _ ⇒
    189     〈[ ], list_set_of_list (prefix ? (nat_of_bitvector ? nparams) RegisterParameters)〉
     185    〈[ ], list_set_of_list (prefix ? nparams RegisterParameters)〉
    190186  | ertl_st_get_hdw _ r _ ⇒ lattice_hsingleton r
    191187  | ertl_st_hdw_to_hdw _ r _ ⇒ lattice_hsingleton r
     
    201197    | _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    202198    ]
    203   | ertl_st_opaccs_a _ _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    204   | ertl_st_opaccs_b _ _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
     199  | ertl_st_opaccs _ d1 d2 s1 s2 _ ⇒ lattice_join (lattice_psingleton s1) (lattice_psingleton s2)
    205200  | ertl_st_load _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    206201  | ertl_st_store r1 r2 r3 _ ⇒
     
    247242    else
    248243      Some ? l
    249   | ertl_st_addr_h r _ l ⇒
    250     if list_set_member register (eq_identifier ?) r pliveafter ∨
    251        list_set_member Register eq_Register RegisterCarry hliveafter then
    252       None ?
    253     else
    254       Some ? l
    255   | ertl_st_addr_l r _ l ⇒
    256     if list_set_member register (eq_identifier ?) r pliveafter ∨
     244  | ertl_st_addr r1 r2 _ l ⇒
     245    if list_set_member register (eq_identifier ?) r1 pliveafter ∨
     246       list_set_member register (eq_identifier ?) r2 pliveafter ∨
    257247       list_set_member Register eq_Register RegisterCarry hliveafter then
    258248      None ?
     
    265255    else
    266256      Some ? l
    267   | ertl_st_opaccs_a _ r _ _ l ⇒
    268     if list_set_member register (eq_identifier ?) r pliveafter ∨
    269        list_set_member Register eq_Register RegisterCarry hliveafter then
    270       None ?
    271     else
    272       Some ? l
    273   | ertl_st_opaccs_b _ r _ _ l ⇒
    274     if list_set_member register (eq_identifier ?) r pliveafter ∨
     257  | ertl_st_opaccs _ d1 d2 _ _ l ⇒
     258    if list_set_member register (eq_identifier ?) d1 pliveafter ∨
     259       list_set_member register (eq_identifier ?) d2 pliveafter ∨
    275260       list_set_member Register eq_Register RegisterCarry hliveafter then
    276261      None ?
Note: See TracChangeset for help on using the changeset viewer.