Ignore:
Timestamp:
Aug 3, 2011, 2:48:11 PM (9 years ago)
Author:
campbell
Message:

Merge branch with trunk

Location:
Deliverables/D3.3/id-lookup-branch
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch

    • Property svn:mergeinfo changed
      /srcmerged: 1094
  • Deliverables/D3.3/id-lookup-branch/ERTL/liveness.ma

    r1091 r1098  
    3030  λr: list A.
    3131    foldr ? ? andb true (map ? ? (λx. member A eq_a x r) l).
     32
     33definition list_set_member ≝
     34  λA: Type[0].
     35  λeq_a: A → A → bool.
     36  λa: A.
     37  λl: list A.
     38    member A eq_a a l.
    3239
    3340definition statement_successors ≝
     
    106113  | ertl_st_cond _ _ _ ⇒ lattice_bottom
    107114  | ertl_st_return _ ⇒ lattice_bottom
    108   | ertl_st_clear_carry _ ⇒ 〈[ ], [ RegisterCarry ]〉
    109   | ertl_st_set_carry _ ⇒ 〈[ ], [ RegisterCarry ]〉
    110   | _ ⇒ ?
    111   ].
    112 
    113 let defined (stmt : statement) : L.t =
     115  | ertl_st_clear_carry _ ⇒ lattice_hsingleton RegisterCarry
     116  | ertl_st_set_carry _ ⇒ lattice_hsingleton RegisterCarry
     117  | ertl_st_op2 op2 r _ _ _ ⇒
     118    match op2 with
     119    [ Add ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
     120    | Addc ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
     121    | Sub ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
     122    | _ ⇒ lattice_psingleton r
     123    ]
     124  | ertl_st_op1 op1 r _ _ ⇒ lattice_psingleton r
     125  | ertl_st_get_hdw r _ _ ⇒ lattice_psingleton r
     126  | ertl_st_frame_size r _ ⇒ lattice_psingleton r
     127  | ertl_st_pop r _ ⇒ lattice_psingleton r
     128  | ertl_st_int r _ _ ⇒ lattice_psingleton r
     129  | ertl_st_addr_h r _ _ ⇒ lattice_psingleton r
     130  | ertl_st_addr_l r _ _ ⇒ lattice_psingleton r
     131  | ertl_st_move r _ _ ⇒ lattice_psingleton r
     132  | ertl_st_opaccs_a _ r _ _ _ ⇒ lattice_psingleton r
     133  | ertl_st_opaccs_b _ r _ _ _ ⇒ lattice_psingleton r
     134  | ertl_st_load r _ _ _ ⇒ lattice_psingleton r
     135  | ertl_st_set_hdw r _ _ ⇒ lattice_hsingleton r
     136  | ertl_st_hdw_to_hdw r _ _ ⇒ lattice_hsingleton r
     137  (* Potentially destroys all caller-save hardware registers. *)
     138  | ertl_st_call_id _ _ _ ⇒ 〈[ ], RegisterCallerSaved〉
     139  | ertl_st_new_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     140  | ertl_st_del_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     141  ].
     142
     143definition list_set_of_list ≝
     144  λrl.
     145    foldr ? ? (list_set_add Register eq_Register) rl [ ].
     146
     147definition list_set_of_list2 ≝
     148  let f ≝ λset. λr. list_set_add Register eq_Register r set in
     149    foldl ? ? f [ ].
     150
     151definition ret_regs ≝ list_set_of_list RegisterRets.
     152
     153definition used: ertl_statement → register_lattice ≝
     154  λstmt.
    114155  match stmt with
    115   | St_clear_carry _
    116   | St_set_carry _ ->
    117     Register.Set.empty, I8051.RegisterSet.singleton I8051.carry
    118   | St_op2 (I8051.Add, r, _, _, _)
    119   | St_op2 (I8051.Addc, r, _, _, _)
    120   | St_op2 (I8051.Sub, r, _, _, _) ->
    121     L.join (L.hsingleton I8051.carry) (L.psingleton r)
    122   | St_op1 (I8051.Inc, r, _, _)
    123   | St_get_hdw (r, _, _)
    124   | St_framesize (r, _)
    125   | St_pop (r, _)
    126   | St_int (r, _, _)
    127   | St_addrH (r, _, _)
    128   | St_addrL (r, _, _)
    129   | St_move (r, _, _)
    130   | St_opaccsA (_, r, _, _, _)
    131   | St_opaccsB (_, r, _, _, _)
    132   | St_op1 (_, r, _, _)
    133   | St_op2 (_, r, _, _, _)
    134   | St_load (r, _, _, _) ->
    135     L.psingleton r
    136   | St_set_hdw (r, _, _)
    137   | St_hdw_to_hdw (r, _, _) ->
    138     L.hsingleton r
    139   | St_call_id _ ->
    140       (* Potentially destroys all caller-save hardware registers. *)
    141     Register.Set.empty, I8051.caller_saved
    142   | St_newframe _
    143   | St_delframe _ ->
    144     L.join (L.hsingleton I8051.spl) (L.hsingleton I8051.sph)
     156  [ ertl_st_skip _ ⇒ lattice_bottom
     157  | ertl_st_cost _ _ ⇒ lattice_bottom
     158  | ertl_st_comment _ _ ⇒ lattice_bottom
     159  | ertl_st_frame_size _ _ ⇒ lattice_bottom
     160  | ertl_st_pop _ _ ⇒ lattice_bottom
     161  | ertl_st_addr_h _ _ _ ⇒ lattice_bottom
     162  | ertl_st_addr_l _ _ _ ⇒ lattice_bottom
     163  | ertl_st_int _ _ _ ⇒ lattice_bottom
     164  | ertl_st_clear_carry _ ⇒ lattice_bottom
     165  | ertl_st_set_carry _ ⇒ lattice_bottom
     166    (* Reads the hardware registers that are used to pass parameters. *)
     167  | ertl_st_call_id _ nparams _ ⇒
     168    〈[ ], list_set_of_list (prefix ? (nat_of_bitvector ? nparams) RegisterParameters)〉
     169  | ertl_st_get_hdw _ r _ ⇒ lattice_hsingleton r
     170  | ertl_st_hdw_to_hdw _ r _ ⇒ lattice_hsingleton r
     171  | ertl_st_set_hdw _ r _ ⇒ lattice_psingleton r
     172  | ertl_st_push r _ ⇒ lattice_psingleton r
     173  | ertl_st_move _ r _ ⇒ lattice_psingleton r
     174  | ertl_st_op1 _ _ r _ ⇒ lattice_psingleton r
     175  | ertl_st_cond r _ _ ⇒ lattice_psingleton r
     176  | ertl_st_op2 op2 _ r1 r2 _ ⇒
     177    match op2 with
     178    [ Addc ⇒
     179      lattice_join (lattice_join (lattice_psingleton r1) (lattice_psingleton r2)) (lattice_hsingleton RegisterCarry)
     180    | _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
     181    ]
     182  | ertl_st_opaccs_a _ _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
     183  | ertl_st_opaccs_b _ _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
     184  | ertl_st_load _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
     185  | ertl_st_store r1 r2 r3 _ ⇒
     186    lattice_join (lattice_join (lattice_psingleton r1) (lattice_psingleton r2)) (lattice_psingleton r3)
     187  | ertl_st_new_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     188  | ertl_st_del_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     189  | ertl_st_return _ ⇒ 〈[ ], list_set_union ? eq_Register RegisterCalleeSaved ret_regs〉
     190  ].
     191
     192definition eliminable: register_lattice → ertl_statement → option label ≝
     193  λl.
     194  λstmt.
     195  let 〈pliveafter, hliveafter〉 ≝ l in
     196  match stmt with
     197  [ ertl_st_skip _ ⇒ None ?
     198  | ertl_st_comment _ _ ⇒ None ?
     199  | ertl_st_cost _ _ ⇒ None ?
     200  | ertl_st_new_frame _ ⇒ None ?
     201  | ertl_st_del_frame _ ⇒ None ?
     202  | ertl_st_pop _ _ ⇒ None ?
     203  | ertl_st_push _ _ ⇒ None ?
     204  | ertl_st_clear_carry _  ⇒ None ?
     205  | ertl_st_set_carry _  ⇒ None ?
     206  | ertl_st_store _ _ _ _ ⇒ None ?
     207  | ertl_st_call_id _ _ _ ⇒ None ?
     208  | ertl_st_cond _ _ _ ⇒ None ?
     209  | ertl_st_return _ ⇒ None ?
     210  | ertl_st_get_hdw r _ l ⇒
     211    if list_set_member register (eq_identifier ?) r pliveafter ∨
     212       list_set_member Register eq_Register RegisterCarry hliveafter then
     213      None ?
     214    else
     215      Some ? l
     216  | ertl_st_frame_size r l ⇒
     217    if list_set_member register (eq_identifier ?) r pliveafter ∨
     218       list_set_member Register eq_Register RegisterCarry hliveafter then
     219      None ?
     220    else
     221      Some ? l
     222  | ertl_st_int r _ l ⇒
     223    if list_set_member register (eq_identifier ?) r pliveafter ∨
     224       list_set_member Register eq_Register RegisterCarry hliveafter then
     225      None ?
     226    else
     227      Some ? l
     228  | ertl_st_addr_h r _ l ⇒
     229    if list_set_member register (eq_identifier ?) r pliveafter ∨
     230       list_set_member Register eq_Register RegisterCarry hliveafter then
     231      None ?
     232    else
     233      Some ? l
     234  | ertl_st_addr_l r _ l ⇒
     235    if list_set_member register (eq_identifier ?) r pliveafter ∨
     236       list_set_member Register eq_Register RegisterCarry hliveafter then
     237      None ?
     238    else
     239      Some ? l
     240  | ertl_st_move r _ l ⇒
     241    if list_set_member register (eq_identifier ?) r pliveafter ∨
     242       list_set_member Register eq_Register RegisterCarry hliveafter then
     243      None ?
     244    else
     245      Some ? l
     246  | ertl_st_opaccs_a _ r _ _ l ⇒
     247    if list_set_member register (eq_identifier ?) r pliveafter ∨
     248       list_set_member Register eq_Register RegisterCarry hliveafter then
     249      None ?
     250    else
     251      Some ? l
     252  | ertl_st_opaccs_b _ r _ _ l ⇒
     253    if list_set_member register (eq_identifier ?) r pliveafter ∨
     254       list_set_member Register eq_Register RegisterCarry hliveafter then
     255      None ?
     256    else
     257      Some ? l
     258  | ertl_st_op1 _ r _ l ⇒
     259    if list_set_member register (eq_identifier ?) r pliveafter ∨
     260       list_set_member Register eq_Register RegisterCarry hliveafter then
     261      None ?
     262    else
     263      Some ? l
     264  | ertl_st_op2 _ r _ _ l ⇒
     265    if list_set_member register (eq_identifier ?) r pliveafter ∨
     266       list_set_member Register eq_Register RegisterCarry hliveafter then
     267      None ?
     268    else
     269      Some ? l
     270  | ertl_st_load r _ _ l ⇒
     271    if list_set_member register (eq_identifier ?) r pliveafter ∨
     272       list_set_member Register eq_Register RegisterCarry hliveafter then
     273      None ?
     274    else
     275      Some ? l
     276  | ertl_st_set_hdw r _ l ⇒
     277    if list_set_member Register eq_Register r hliveafter then
     278      None ?
     279    else
     280      Some ? l
     281  | ertl_st_hdw_to_hdw r _ l ⇒
     282    if list_set_member Register eq_Register r hliveafter then
     283      None ?
     284    else
     285      Some ? l
     286  ].
     287
     288definition statement_semantics: ertl_statement → register_lattice → register_lattice ≝
     289  λstmt.
     290  λliveafter.
     291  match eliminable liveafter stmt with
     292  [ None ⇒ lattice_join (lattice_diff liveafter (defined stmt)) (used stmt)
     293  | Some l ⇒ liveafter
     294  ].
     295
     296definition valuation ≝ label → register_lattice.
     297
     298definition analyse: ertl_internal_function → valuation ≝
     299  λint_fun.
     300  let livebefore ≝ λlabel. λliveafter: valuation.
     301    match lookup ? ? (ertl_if_graph int_fun) label with
     302    [ None      ⇒ ?
     303    | Some stmt ⇒ statement_semantics stmt (liveafter label)
     304    ]
     305  in ?.
Note: See TracChangeset for help on using the changeset viewer.