Ignore:
Timestamp:
Aug 30, 2011, 6:55:12 PM (9 years ago)
Author:
campbell
Message:

Merge trunk into branch.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
5 edited
4 copied

Legend:

Unmodified
Added
Removed

  • Deliverables/D3.3/id-lookup-branch

  • Deliverables/D3.3/id-lookup-branch/ERTL/ERTL.ma

    r1109 r1153  
    2020  | ertl_st_pop: register → label → ertl_statement
    2121  | ertl_st_push: register → label → ertl_statement
     22  | ertl_st_addr: register → register → ident → label → ertl_statement
     23(* XXX: changed from O'Caml
    2224  | ertl_st_addr_h: register → ident → label → ertl_statement
    2325  | ertl_st_addr_l: register → ident → label → ertl_statement
     26*)
    2427  | ertl_st_int: register → Byte → label → ertl_statement
    2528  | ertl_st_move: register → register → label → ertl_statement
     29  | ertl_st_opaccs: OpAccs → register → register → register → register → label → ertl_statement
     30(* XXX: changed from O'Caml
    2631  | ertl_st_opaccs_a: OpAccs → register → register → register → label → ertl_statement
    2732  | ertl_st_opaccs_b: OpAccs → register → register → register → label → ertl_statement
     33*)
    2834  | ertl_st_op1: Op1 → register → register → label → ertl_statement
    2935  | ertl_st_op2: Op2 → register → register → register → label → ertl_statement
    … …  
    3238  | ertl_st_load: register → register → register → label → ertl_statement
    3339  | ertl_st_store: register → register → register → label → ertl_statement
    34   | ertl_st_call_id: ident → Byte → label → ertl_statement
     40  | ertl_st_call_id: ident → nat → label → ertl_statement
    3541  | ertl_st_cond: register → label → label → ertl_statement
    3642  | ertl_st_return: ertl_statement.

  • Deliverables/D3.3/id-lookup-branch/ERTL/ERTLToLTL.ma

    r1091 r1153  
    22include "ERTL/ERTLToLTLI.ma".
    33include "LTL/LTL.ma".
     4include "ERTL/spill.ma".
    45
    56definition translate_internal ≝
    67  λf.
    78  λint_fun: ertl_internal_function.
    8     mk_ltl_internal_function ?
    9       (ertl_if_luniverse int_fun)
    10       (ertl_if_runiverse int_fun)
    11       (ertl_if_stacksize int_fun)
    12       (ertl_if_graph int_fun)
    13       ?
    14       ?.
     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  }
    15117
    16118definition translate_funct ≝

  • Deliverables/D3.3/id-lookup-branch/ERTL/ERTLToLTLI.ma

    r1109 r1153  
    8383    [ decision_colour src_hwr ⇒
    8484      if eq_Register dest_hwr src_hwr then
    85         joint_st_sequential ? globals (joint_instr_skip globals) l
     85        joint_st_goto ? globals l
    8686      else
    8787        let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals dest_hwr) l) in
    … …  
    9494    | decision_spill src_off ⇒
    9595      if eq_bv ? dest_off src_off then
    96         joint_st_sequential ? globals (joint_instr_skip globals) l
     96        joint_st_goto ? globals l
    9797      else
    9898        let temp_hwr ≝ RegisterSST in
    … …  
    106106  λl.
    107107  if eq_nat stacksize 0 then
    108     joint_st_sequential ? globals (joint_instr_skip globals) l
     108    joint_st_goto ? globals l
    109109  else
    110110    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in
    … …  
    122122  λl.
    123123  if eq_nat stacksize 0 then
    124     joint_st_sequential ? globals (joint_instr_skip globals) l
     124    joint_st_goto ? globals l
    125125  else
    126126    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in
    … …  
    135135  λstmt: ertl_statement.
    136136  match stmt with
    137   [ ertl_st_skip l ⇒ joint_st_sequential ? globals (joint_instr_skip globals) l
     137  [ ertl_st_skip l ⇒ joint_st_goto ? globals l
    138138  | ertl_st_comment s l ⇒ joint_st_sequential ? globals (joint_instr_comment globals s) l
    139139  | ertl_st_cost cost_lbl l ⇒ joint_st_sequential ? globals (joint_instr_cost_label globals cost_lbl) l
    … …  
    155155    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_push globals) l) in
    156156    let l ≝ read globals r (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    157       joint_st_sequential ? globals (joint_instr_skip globals) l
    158   | ertl_st_addr_h r x l ⇒
    159     let 〈hdw, l〉 ≝ write globals r l in
    160     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     157      joint_st_goto ? globals l
     158  | ertl_st_addr rl rh x l ⇒
     159    let 〈hdw1, l〉 ≝ write globals rh l in
     160    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw1) l) in
    161161    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l) in
    162       joint_st_sequential ? globals (joint_instr_address globals x ?) l
    163   | ertl_st_addr_l r x l ⇒
    164     let 〈hdw, l〉 ≝ write globals r l in
    165     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     162    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l) in
     163    let 〈hdw2, l〉 ≝ write globals rl l in
     164    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw2) l) in
    166165    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l) in
    167166      joint_st_sequential ? globals (joint_instr_address globals x ?) l
     167(*  | ertl_st_addr_h r x l ⇒
     168    let 〈hdw, l〉 ≝ write globals r l in
     169    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
     170    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l)) in
     171      ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l)
     172  | ertl_st_addr_l r x l ⇒
     173    let 〈hdw, l〉 ≝ write globals r l in
     174    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
     175    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l)) in
     176      ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l)
     177*)
    168178  | ertl_st_int r i l ⇒
    169179    let 〈hdw, l〉 ≝ write globals r l in
    170180      joint_st_sequential ? globals (joint_instr_int globals hdw i) l
    171181  | ertl_st_move r1 r2 l ⇒ move globals (lookup r1) (lookup r2) l
     182  | ertl_st_opaccs opaccs destr1 destr2 srcr1 srcr2 l ⇒
     183    let 〈hdw, l〉 ≝ write globals destr1 l in
     184    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     185    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
     186    let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     187    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
     188    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     189    let l ≝ generate globals (joint_st_goto ? globals l) in
     190    let 〈hdw, l〉 ≝ write globals destr2 l in
     191    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     192    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l) in
     193    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
     194    let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     195    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
     196    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     197      joint_st_goto ? globals l
     198(*
    172199  | ertl_st_opaccs_a opaccs destr srcr1 srcr2 l ⇒
    173200    let 〈hdw, l〉 ≝ write globals destr l in
    … …  
    177204    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
    178205    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    179       joint_st_sequential ? globals (joint_instr_skip globals) l
     206      joint_st_goto ? globals l
    180207  | ertl_st_opaccs_b opaccs destr srcr1 srcr2 l ⇒
    181208    let 〈hdw, l〉 ≝ write globals destr l in
    … …  
    186213    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
    187214    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    188       joint_st_sequential ? globals (joint_instr_skip globals) l
     215      joint_st_goto ? globals l
     216*)
    189217  | ertl_st_op1 op1 destr srcr l ⇒
    190218    let 〈hdw, l〉 ≝ write globals destr l in
    … …  
    192220    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op1 globals op1) l) in
    193221    let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    194       joint_st_sequential ? globals (joint_instr_skip globals) l
     222      joint_st_goto ? globals l
    195223  | ertl_st_op2 op2 destr srcr1 srcr2 l ⇒
    196224    let 〈hdw, l〉 ≝ write globals destr l in
    … …  
    200228    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
    201229    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    202       joint_st_sequential ? globals (joint_instr_skip globals) l
     230      joint_st_goto ? globals l
    203231  | ertl_st_clear_carry l ⇒ joint_st_sequential ? globals (joint_instr_clear_carry globals) l
    204232  | ertl_st_set_carry l ⇒ joint_st_sequential ? globals (joint_instr_set_carry globals) l
    … …  
    213241    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in
    214242    let l ≝ read globals addr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    215       joint_st_sequential ? globals (joint_instr_skip globals) l
     243      joint_st_goto ? globals l
    216244  | ertl_st_store addr1 addr2 srcr l ⇒
    217245    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_store globals) l) in
    … …  
    225253    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST1) l) in
    226254    let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    227       joint_st_sequential ? globals (joint_instr_skip globals) l
    228   | ertl_st_call_id f ignore l ⇒  joint_st_sequential ? globals (joint_instr_call_id globals f) l
     255      joint_st_goto ? globals l
     256  | ertl_st_call_id f ignore l ⇒ joint_st_sequential ? globals (joint_instr_call_id globals f) l
    229257  | ertl_st_cond srcr lbl_true lbl_false ⇒
    230258    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_cond_acc globals lbl_true) lbl_false) in
    231259    let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    232       joint_st_sequential ? globals (joint_instr_skip globals) l
     260      joint_st_goto ? globals l
    233261  | ertl_st_return ⇒ joint_st_return ? globals
    234262  ].

  • Deliverables/D3.3/id-lookup-branch/ERTL/liveness.ma

    r1109 r1153  
    1 include "utilities/Fix.ma".
    21include "ASM/Util.ma".
    32include "ERTL/ERTL.ma".
    … …  
    3837  λs: ertl_statement.
    3938  match s with
    40   [ ertl_st_return _ ⇒ [ ]
     39  [ ertl_st_return ⇒ [ ]
    4140  | ertl_st_skip l ⇒ [ l ]
    4241  | ertl_st_comment c l ⇒ [ l ]
    … …  
    5049  | ertl_st_push _ l ⇒ [ l ]
    5150  | ertl_st_pop _ l ⇒ [ l ]
    52   | ertl_st_addr_h _ _ l ⇒ [ l ]
    53   | ertl_st_addr_l _ _ l ⇒ [ l ]
     51  | ertl_st_addr _ _ _ l ⇒ [ l ]
    5452  | ertl_st_int _ _ l ⇒ [ l ]
    5553  | ertl_st_move _ _ l ⇒ [ l ]
    56   | ertl_st_opaccs_a _ _ _ _ l ⇒ [ l ]
    57   | ertl_st_opaccs_b _ _ _ _ l ⇒ [ l ]
     54  | ertl_st_opaccs _ _ _ _ _ l ⇒ [ l ]
    5855  | ertl_st_op1 _ _ _ l ⇒ [ l ]
    5956  | ertl_st_op2 _ _ _ _ l ⇒ [ l ]
    … …  
    10097definition lattice_is_maximal: register_lattice → bool ≝ λl. false.
    10198
     99record lattice_property_sig: Type[1] ≝
     100{
     101  lp_type      : Type[0];
     102  lp_property  : Type[0];
     103  lp_bottom    : lp_type;
     104  lp_psingleton: register → lp_type;
     105  lp_hsingleton: Register → lp_type;
     106  lp_join      : lp_type → lp_type → lp_type;
     107  lp_diff      : lp_type → lp_type → lp_type;
     108  lp_equal     : lp_type → lp_type → bool;
     109  lp_is_maximal: lp_type → bool
     110}.
     111
     112definition property ≝
     113  mk_lattice_property_sig
     114    ((list register) × (list Register))
     115    lattice_property
     116    lattice_bottom
     117    lattice_psingleton
     118    lattice_hsingleton
     119    lattice_join
     120    lattice_diff
     121    lattice_equal
     122    lattice_is_maximal.
     123
    102124definition defined: ertl_statement → register_lattice ≝
    103125  λs.
    … …  
    109131  | ertl_st_store _ _ _ _ ⇒ lattice_bottom
    110132  | ertl_st_cond _ _ _ ⇒ lattice_bottom
    111   | ertl_st_return _ ⇒ lattice_bottom
     133  | ertl_st_return ⇒ lattice_bottom
    112134  | ertl_st_clear_carry _ ⇒ lattice_hsingleton RegisterCarry
    113135  | ertl_st_set_carry _ ⇒ lattice_hsingleton RegisterCarry
    … …  
    124146  | ertl_st_pop r _ ⇒ lattice_psingleton r
    125147  | ertl_st_int r _ _ ⇒ lattice_psingleton r
    126   | ertl_st_addr_h r _ _ ⇒ lattice_psingleton r
    127   | ertl_st_addr_l r _ _ ⇒ lattice_psingleton r
     148  | ertl_st_addr r1 r2 _ _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    128149  | ertl_st_move r _ _ ⇒ lattice_psingleton r
    129   | ertl_st_opaccs_a _ r _ _ _ ⇒ lattice_psingleton r
    130   | 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)
    131152  | ertl_st_load r _ _ _ ⇒ lattice_psingleton r
    132153  | ertl_st_set_hdw r _ _ ⇒ lattice_hsingleton r
    … …  
    156177  | ertl_st_frame_size _ _ ⇒ lattice_bottom
    157178  | ertl_st_pop _ _ ⇒ lattice_bottom
    158   | ertl_st_addr_h _ _ _ ⇒ lattice_bottom
    159   | ertl_st_addr_l _ _ _ ⇒ lattice_bottom
     179  | ertl_st_addr _ _ _ _ ⇒ lattice_bottom
    160180  | ertl_st_int _ _ _ ⇒ lattice_bottom
    161181  | ertl_st_clear_carry _ ⇒ lattice_bottom
    … …  
    163183    (* Reads the hardware registers that are used to pass parameters. *)
    164184  | ertl_st_call_id _ nparams _ ⇒
    165     〈[ ], list_set_of_list (prefix ? (nat_of_bitvector ? nparams) RegisterParameters)〉
     185    〈[ ], list_set_of_list (prefix ? nparams RegisterParameters)〉
    166186  | ertl_st_get_hdw _ r _ ⇒ lattice_hsingleton r
    167187  | ertl_st_hdw_to_hdw _ r _ ⇒ lattice_hsingleton r
    … …  
    177197    | _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    178198    ]
    179   | ertl_st_opaccs_a _ _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    180   | 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)
    181200  | ertl_st_load _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    182201  | ertl_st_store r1 r2 r3 _ ⇒
    … …  
    184203  | ertl_st_new_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    185204  | ertl_st_del_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    186   | ertl_st_return _ ⇒ 〈[ ], list_set_union ? eq_Register RegisterCalleeSaved ret_regs〉
     205  | ertl_st_return ⇒ 〈[ ], list_set_union ? eq_Register RegisterCalleeSaved ret_regs〉
    187206  ].
    188207
    … …  
    204223  | ertl_st_call_id _ _ _ ⇒ None ?
    205224  | ertl_st_cond _ _ _ ⇒ None ?
    206   | ertl_st_return _ ⇒ None ?
     225  | ertl_st_return ⇒ None ?
    207226  | ertl_st_get_hdw r _ l ⇒
    208227    if list_set_member register (eq_identifier ?) r pliveafter ∨
    … …  
    223242    else
    224243      Some ? l
    225   | ertl_st_addr_h r _ l ⇒
    226     if list_set_member register (eq_identifier ?) r pliveafter ∨
    227        list_set_member Register eq_Register RegisterCarry hliveafter then
    228       None ?
    229     else
    230       Some ? l
    231   | ertl_st_addr_l r _ l ⇒
    232     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 ∨
    233247       list_set_member Register eq_Register RegisterCarry hliveafter then
    234248      None ?
    … …  
    241255    else
    242256      Some ? l
    243   | ertl_st_opaccs_a _ r _ _ l ⇒
    244     if list_set_member register (eq_identifier ?) r pliveafter ∨
    245        list_set_member Register eq_Register RegisterCarry hliveafter then
    246       None ?
    247     else
    248       Some ? l
    249   | ertl_st_opaccs_b _ r _ _ l ⇒
    250     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 ∨
    251260       list_set_member Register eq_Register RegisterCarry hliveafter then
    252261      None ?
    … …  
    292301
    293302definition valuation ≝ label → register_lattice.
     303definition rhs ≝ valuation → lattice_property.
     304definition equations ≝ label → rhs.
     305
     306axiom fix_lfp: equations → valuation.
     307
     308definition livebefore ≝
     309  λint_fun.
     310  λlabel.
     311  λliveafter: valuation.
     312  match lookup ? ? (ertl_if_graph int_fun) label with
     313  [ None      ⇒ ?
     314  | Some stmt ⇒ statement_semantics stmt (liveafter label)
     315  ].
     316  cases not_implemented (* XXX *)
     317qed.
     318
     319definition liveafter ≝
     320  λint_fun.
     321  λlivebefore.
     322  λlabel.
     323  λliveafter: valuation.
     324  match lookup ? ? (ertl_if_graph int_fun) label with
     325  [ None      ⇒ ?
     326  | Some stmt ⇒ list_set_fold ? ? (λsuccessor. λaccu.
     327      lattice_join (livebefore successor liveafter) accu)
     328      lattice_bottom (statement_successors stmt)
     329  ].
     330  cases not_implemented (* XXX *)
     331qed.
    294332
    295333definition analyse: ertl_internal_function → valuation ≝
    296334  λint_fun.
    297   let livebefore ≝ λlabel. λliveafter: valuation.
    298     match lookup ? ? (ertl_if_graph int_fun) label with
    299     [ None      ⇒ ?
    300     | Some stmt ⇒ statement_semantics stmt (liveafter label)
    301     ]
    302   in
    303   let liveafter ≝ λlabel. λliveafter: valuation.
    304     match lookup ? ? (ertl_if_graph int_fun) label with
    305     [ None      ⇒ ?
    306     | Some stmt ⇒ list_set_fold ? ? (λsuccessor. λaccu.
    307         lattice_join (livebefore successor liveafter) accu)
    308         lattice_bottom (statement_successors stmt)
    309     ]
    310   in ?.
     335    fix_lfp (liveafter int_fun (livebefore int_fun)).
Note: See TracChangeset for help on using the changeset viewer.