Changeset 1223 for src/ERTL


Ignore:
Timestamp:
Sep 16, 2011, 5:15:35 PM (9 years ago)
Author:
mulligan
Message:

changes

Location:
src/ERTL
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r1221 r1223  
    2525  mk_sem_params_ ertl_params globals (graph (ertl_statement globals)) (lookup …).
    2626
    27 (*
    2827definition ertl_internal_function ≝
    29  λglobals. joint_internal_function globals … (ertl_sem_params_ globals).
    30 *)
     28  λglobals. joint_internal_function globals … (ertl_sem_params_ globals).
    3129
    3230definition ertl_program ≝ λglobals. joint_program globals … (ertl_sem_params_ globals).
  • src/ERTL/build.ma

    r1187 r1223  
    22include "utilities/Interference.ma".
    33
     4axiom graph : Type[0].
     5axiom create: ∀globals: list ident. ertl_internal_function globals → graph.
     6
     7record build_properties: Type[1] ≝
     8{
     9  lookup: graph → register → vertex
     10}.
     11
     12(*
    413definition build ≝
    514  λglobals: list ident.
     
    5968    〈liveafter, graph〉.
    6069  [*: @lattice_bottom ] (* XXX: matita bug here! *)
    61 qed.
     70qed. *)
  • src/ERTL/liveness.ma

    r1185 r1223  
    11include "ASM/Util.ma".
    22include "ERTL/ERTL.ma".
    3 
    4 definition list_set_union ≝
    5   λA: Type[0].
    6   λeq_a: A → A → bool.
    7   λl: list A.
    8   λr: list A.
    9     nub_by A eq_a (l @ r).
    10 
    11 definition list_set_add ≝
    12   λA: Type[0].
    13   λeq_a: A → A → bool.
    14   λa: A.
    15   λs: list A.
    16     nub_by A eq_a (a :: s).
    17 
    18 definition list_set_diff ≝
    19   λA: Type[0].
    20   λeq_a: A → A → bool.
    21   λl: list A.
    22   λr: list A.
    23     filter A (λx. member A eq_a x r) l.
    24 
    25 definition list_set_equal ≝
    26   λA: Type[0].
    27   λeq_a: A → A → bool.
    28   λl: list A.
    29   λr: list A.
    30     foldr ? ? andb true (map ? ? (λx. member A eq_a x r) l).
    31 
    32 definition list_set_member ≝ member.
    33 
    34 definition list_set_fold ≝ foldr.
     3include "utilities/adt/set_adt.ma".
    354
    365definition statement_successors ≝
     
    4110    match seq with
    4211    [ joint_instr_cond acc_a_reg lbl_true ⇒
    43         list_set_add ? (eq_identifier ?) lbl_true [ l ]
    44     | _ ⇒ [ l ]
     12        set_insert … lbl_true (set_singleton … l)
     13    | _ ⇒ set_singleton … l
    4514    ]
    4615  | joint_st_extension ext ⇒
    4716    match ext with
    48     [ ertl_st_ext_new_frame l ⇒ [ l ]
    49     | ertl_st_ext_del_frame l ⇒ [ l ]
    50     | ertl_st_ext_frame_size r l ⇒ [ l ]
    51     ]
    52   | joint_st_goto l ⇒ [ l ]
    53   | joint_st_return ⇒ [ ]
    54   ].
    55 
    56 definition register_lattice ≝ (list register) × (list Register).
     17    [ ertl_st_ext_new_frame l ⇒ set_singleton … l
     18    | ertl_st_ext_del_frame l ⇒ set_singleton … l
     19    | ertl_st_ext_frame_size r l ⇒ set_singleton … l
     20    ]
     21  | joint_st_goto l ⇒ set_singleton … l
     22  | joint_st_return ⇒ set_empty …
     23  ].
     24
     25definition register_lattice ≝ (set register) × (set Register).
    5726definition lattice_property ≝ register_lattice.
    58 definition lattice_bottom: register_lattice ≝ 〈[ ], [ ]〉.
     27definition lattice_bottom: register_lattice ≝ 〈set_empty register, set_empty Register〉.
    5928definition lattice_psingleton: register → register_lattice ≝
    6029  λr.
    61     〈[ r ], [ ]〉.
     30    〈set_singleton … r, set_empty …〉.
    6231definition lattice_hsingleton: Register → register_lattice ≝
    6332  λr.
    64     〈[ ], [ r ]〉.
     33    〈set_empty …, set_singleton … r〉.
    6534
    6635definition lattice_join: register_lattice → register_lattice → register_lattice ≝
     
    6938  let 〈lp, lh〉 ≝ left in
    7039  let 〈rp, rh〉 ≝ right in
    71     〈list_set_union ? (eq_identifier ?) lp rp, list_set_union ? eq_Register lh rh〉.
     40    〈set_union … lp rp, set_union … lh rh〉.
    7241
    7342definition lattice_diff: register_lattice → register_lattice → register_lattice ≝
     
    7645  let 〈lp, lh〉 ≝ left in
    7746  let 〈rp, rh〉 ≝ right in
    78     〈list_set_diff ? (eq_identifier ?) lp rp, list_set_diff ? eq_Register lh rh〉.
     47    〈set_diff … lp rp, set_diff … lh rh〉.
    7948
    8049definition lattice_equal: register_lattice → register_lattice → bool ≝
     
    8352  let 〈lp, lh〉 ≝ left in
    8453  let 〈rp, rh〉 ≝ right in
    85     andb (list_set_equal ? (eq_identifier ?) lp rp) (list_set_equal ? eq_Register lh rh).
     54    andb (set_equal … (eq_identifier …) lp rp) (set_equal … eq_Register lh rh).
    8655
    8756definition lattice_is_maximal: register_lattice → bool ≝ λl. false.
     
    10271definition property ≝
    10372  mk_lattice_property_sig
    104     ((list register) × (list Register))
     73    ((set register) × (set Register))
    10574    lattice_property
    10675    lattice_bottom
     
    134103    | joint_instr_load r _ _ ⇒ lattice_psingleton r
    135104    (* Potentially destroys all caller-save hardware registers. *)
    136     | joint_instr_call_id _ _ ⇒ 〈[ ], RegisterCallerSaved〉
     105    | joint_instr_call_id _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉
    137106    | joint_instr_comment c ⇒ lattice_bottom
    138107    | joint_instr_cond r lbl_true ⇒ lattice_bottom
     
    158127  ].
    159128
    160 definition list_set_of_list ≝
    161   λrl.
    162     foldr ? ? (list_set_add Register eq_Register) rl [ ].
    163 
    164 definition list_set_of_list2 ≝
    165   let f ≝ λset. λr. list_set_add Register eq_Register r set in
    166     foldl ? ? f [ ].
    167 
    168 definition ret_regs ≝ list_set_of_list RegisterRets.
     129definition ret_regs ≝ set_from_list … RegisterRets.
    169130
    170131definition used ≝
     
    190151    | joint_instr_load acc_a dpl dph ⇒ lattice_join (lattice_psingleton dpl) (lattice_psingleton dph)
    191152    (* Reads the hardware registers that are used to pass parameters. *)
    192     | joint_instr_call_id _ nparams ⇒ 〈[ ], list_set_of_list (prefix ? nparams RegisterParams)〉
     153    | joint_instr_call_id _ nparams ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉
    193154    | joint_instr_comment c ⇒ lattice_bottom
    194155    | joint_instr_cond r lbl_true ⇒ lattice_psingleton r
     
    205166      ]
    206167    ]
    207   | joint_st_return ⇒ 〈[ ], list_set_union ? eq_Register RegisterCalleeSaved ret_regs〉
     168  | joint_st_return ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉
    208169  | joint_st_goto l ⇒ lattice_bottom
    209170  | joint_st_extension ext ⇒
     
    224185    match seq with
    225186    [ joint_instr_op2 op2 acc_a r ⇒
    226       if list_set_member register (eq_identifier ?) acc_a pliveafter ∨
    227          list_set_member Register eq_Register RegisterCarry hliveafter then
     187      if set_member … (eq_identifier …) acc_a pliveafter ∨
     188         set_member … eq_Register RegisterCarry hliveafter then
    228189        None ?
    229190      else
     
    232193    | joint_instr_set_carry ⇒ None ?
    233194    | joint_instr_opaccs opaccs r1 r2 ⇒
    234       if list_set_member register (eq_identifier ?) r1 pliveafter ∨
    235          list_set_member register (eq_identifier ?) r2 pliveafter ∨
    236          list_set_member Register eq_Register RegisterCarry hliveafter then
     195      if set_member … (eq_identifier …) r1 pliveafter ∨
     196         set_member … (eq_identifier …) r2 pliveafter ∨
     197         set_member … eq_Register RegisterCarry hliveafter then
    237198        None ?
    238199      else
    239200        Some ? l
    240201    | joint_instr_op1 op1 r ⇒
    241       if list_set_member register (eq_identifier ?) r pliveafter ∨
    242          list_set_member Register eq_Register RegisterCarry hliveafter then
     202      if set_member … (eq_identifier …) r pliveafter ∨
     203         set_member … eq_Register RegisterCarry hliveafter then
    243204        None ?
    244205      else
     
    246207    | joint_instr_pop r ⇒ None ?
    247208    | joint_instr_int r _ ⇒
    248       if list_set_member register (eq_identifier ?) r pliveafter ∨
    249          list_set_member Register eq_Register RegisterCarry hliveafter then
     209      if set_member … (eq_identifier …) r pliveafter ∨
     210         set_member … eq_Register RegisterCarry hliveafter then
    250211        None ?
    251212      else
    252213        Some ? l
    253214    | joint_instr_address _ _ r1 r2 ⇒
    254       if list_set_member register (eq_identifier ?) r1 pliveafter ∨
    255          list_set_member register (eq_identifier ?) r2 pliveafter ∨
    256          list_set_member Register eq_Register RegisterCarry hliveafter then
     215      if set_member … (eq_identifier …) r1 pliveafter ∨
     216         set_member … (eq_identifier …) r2 pliveafter ∨
     217         set_member … eq_Register RegisterCarry hliveafter then
    257218        None ?
    258219      else
    259220        Some ? l
    260221    | joint_instr_load acc_a dpl dph ⇒
    261       if list_set_member register (eq_identifier ?) acc_a pliveafter ∨
    262          list_set_member Register eq_Register RegisterCarry hliveafter then
     222      if set_member ? (eq_identifier …) acc_a pliveafter ∨
     223         set_member … eq_Register RegisterCarry hliveafter then
    263224        None ?
    264225      else
     
    275236      match r1 with
    276237      [ pseudo p1 ⇒
    277         if list_set_member register (eq_identifier ?) p1 pliveafter ∨
    278            list_set_member Register eq_Register RegisterCarry hliveafter then
     238        if set_member … (eq_identifier …) p1 pliveafter ∨
     239           set_member … eq_Register RegisterCarry hliveafter then
    279240          None ?
    280241        else
    281242          Some ? l
    282243      | hardware h1 ⇒
    283         if list_set_member Register eq_Register h1 hliveafter then
     244        if set_member … eq_Register h1 hliveafter then
    284245          None ?
    285246        else
     
    294255    | ertl_st_ext_del_frame l ⇒ None ?
    295256    | ertl_st_ext_frame_size r l ⇒
    296       if list_set_member register (eq_identifier ?) r pliveafter ∨
    297         list_set_member Register eq_Register RegisterCarry hliveafter then
     257      if set_member ? (eq_identifier RegisterTag) r pliveafter ∨
     258         set_member ? eq_Register RegisterCarry hliveafter then
    298259        None ?
    299260      else
     
    319280definition livebefore ≝
    320281  λglobals: list ident.
    321   λint_fun.
     282  λint_fun: ertl_internal_function globals.
    322283  λlabel.
    323284  λliveafter: valuation.
    324   match lookup ? ? (ertl_if_graph globals int_fun) label with
     285  match lookup ? ? (joint_if_graph … int_fun) label with
    325286  [ None      ⇒ ?
    326287  | Some stmt ⇒ statement_semantics globals stmt (liveafter label)
     
    330291
    331292definition liveafter ≝
    332   λglobals.
    333   λint_fun.
    334   λlivebefore.
     293  λglobals: list ident.
     294  λint_fun: ertl_internal_function globals.
     295  λlivebefore: label → ?.
    335296  λlabel.
    336297  λliveafter: valuation.
    337   match lookup … (ertl_if_graph globals int_fun) label with
     298  match lookup … (joint_if_graph … int_fun) label with
    338299  [ None      ⇒ ?
    339   | Some stmt ⇒ list_set_fold … (λsuccessor. λaccu: register_lattice.
     300  | Some stmt ⇒ set_fold ? ? (λsuccessor. λaccu: register_lattice.
    340301      lattice_join (livebefore successor liveafter) accu)
    341       lattice_bottom (statement_successors globals stmt)
     302      (statement_successors globals stmt) lattice_bottom
    342303  ].
    343304  cases not_implemented (* XXX *)
Note: See TracChangeset for help on using the changeset viewer.