Changeset 1075


Ignore:
Timestamp:
Jul 18, 2011, 5:21:14 PM (8 years ago)
Author:
mulligan
Message:

nearly completed rtl -> ertl pass removing all option types with dep. types

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/I8051.ma

    r1071 r1075  
    146146definition RegisterSPH ≝ Register07.
    147147definition RegisterRets ≝ [RegisterDPL; RegisterDPH; Register00; Register01].
     148definition RegisterCalleeSaved ≝
     149  [Register20 ; Register21 ; Register22 ; Register23 ; Register24 ; Register25 ; Register26 ; Register27].
    148150
    149151definition register_address: Register → [[ acc_a; direct; registr ]] ≝
  • src/ASM/Util.ma

    r1071 r1075  
    152152
    153153let rec split
    154   (A: Type[0]) (l: list A) (index: nat) (proof: index < |l|)
     154  (A: Type[0]) (l: list A) (index: nat) (proof: index |l|)
    155155    on index ≝
    156   match index return λx. x < |l| → (list A) × (list A) with
     156  match index return λx. x |l| → (list A) × (list A) with
    157157  [ O ⇒ λzero_prf. 〈[], l〉
    158158  | S index' ⇒ λsucc_prf.
    159     match l return λx. S index' < |x| → (list A) × (list A) with
     159    match l return λx. S index' |x| → (list A) × (list A) with
    160160    [ nil ⇒ λnil_absrd. ?
    161161    | cons hd tl ⇒ λcons_prf.
     
    165165  ] proof.
    166166  [1: normalize in nil_absrd;
    167       cases(not_le_Sn_O (S index'))
     167      cases(not_le_Sn_O index')
    168168      #HYP
    169169      cases(HYP nil_absrd)
    170170  |2: normalize in cons_prf;
    171       normalize
    172171      @le_S_S_to_le
    173172      assumption
  • src/RTL/RTLtoERTL.ma

    r1071 r1075  
    11include "RTL/RTL.ma".
    2 (* include "RTL/RTLTailcall.ma". *)
     2include "utilities/RegisterSet.ma".
    33include "ERTL/ERTL.ma".
    44
     
    148148  ].
    149149 
     150axiom fresh_regs_length:
     151  ∀def: ertl_internal_function.
     152  ∀n: nat.
     153    |(\snd (fresh_regs def n))| = n.
     154
     155definition fresh_regs_strong: ? → ∀n: nat. Σregs: ertl_internal_function × (list register). |\snd regs| = n ≝
     156  λdef: ertl_internal_function.
     157  λn: nat.
     158    fresh_regs def n.
     159  @fresh_regs_length
     160qed.
     161 
    150162definition save_hdws_internal ≝
    151163  λdestr_srcr: register × hardware_register.
     
    232244  let start_lbl ≝ ertl_if_entry def in
    233245  let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in
    234   match lookup ? ? (ertl_if_graph def) start_lbl with
    235   [ None ⇒ ?
    236   | Some last_stmt ⇒
     246  match lookup ? ? (ertl_if_graph def) start_lbl
     247    return λx. lookup ? ? (ertl_if_graph def) start_lbl ≠ None ? → ertl_internal_function with
     248  [ None ⇒ λnone_absrd. ?
     249  | Some last_stmt ⇒ λsome_prf.
    237250    let def ≝
    238251      add_translates
     
    249262    in
    250263      add_graph tmp_lbl last_stmt def
    251   ].
    252   cases not_implemented (* until Brian gives goahead for dep. types *)
     264  ] ?.
     265  cases not_implemented (* dep. types here *)
    253266qed.
    254267
     
    259272  λdef: ertl_internal_function.
    260273  let 〈def, tmpr〉 ≝ fresh_reg def in
    261   match reduce_strong ? RegisterSTS ret_regs with
     274  match reduce_strong ? ? RegisterSTS ret_regs with
    262275  [ dp crl crl_proof ⇒
    263276    let commonl ≝ \fst (\fst crl) in
     
    267280    let init_tmpr ≝ ertl_st_int tmpr (zero ?) start_lbl in
    268281    let f_save ≝ λst. λr. ertl_st_set_hdw st r start_lbl in
    269     let saves ≝ map2 ? ? ? f_save commonl commonr ? in
     282    let saves ≝ map2 ? ? ? f_save commonl commonr crl_proof in
    270283    let f_default ≝ λst. ertl_st_set_hdw st tmpr start_lbl in
    271284    let defaults ≝ map ? ? f_default restl in
     
    273286  ].
    274287
    275 let save_return ret_regs start_lbl dest_lbl def =
    276   let (def, tmpr) = fresh_reg def in
    277   let ((common1, rest1), (common2, _)) =
    278     MiscPottier.reduce I8051.sts ret_regs in
    279   let init_tmpr = ERTL.St_int (tmpr, 0, start_lbl) in
    280   let f_save st r = ERTL.St_set_hdw (st, r, start_lbl) in
    281   let saves = List.map2 f_save common1 common2 in
    282   let f_default st = ERTL.St_set_hdw (st, tmpr, start_lbl) in
    283   let defaults = List.map f_default rest1 in
    284   adds_graph (init_tmpr :: saves @ defaults) start_lbl dest_lbl def
     288definition assign_result ≝
     289  λstart_lbl: label.
     290  match reduce_strong ? ? RegisterRets RegisterSTS with
     291  [ dp crl crl_proof ⇒
     292    let commonl ≝ \fst (\fst crl) in
     293    let commonr ≝ \fst (\snd crl) in
     294    let f ≝ λret. λst. ertl_st_hdw_to_hdw ret st start_lbl in
     295    let insts ≝ map2 ? ? ? f commonl commonr crl_proof in
     296      adds_graph insts start_lbl
     297  ].
     298
     299definition add_epilogue ≝
     300  λret_regs.
     301  λsral.
     302  λsrah.
     303  λsregs.
     304  λdef.
     305  let start_lbl ≝ ertl_if_exit def in
     306  let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in
     307  match lookup ? ? (ertl_if_graph def) start_lbl
     308    return λx. lookup ? ? (ertl_if_graph def) start_lbl ≠ None ? → ? with
     309  [ None ⇒ λnone_absd. ?
     310  | Some last_stmt ⇒ λsome_prf.
     311    let def ≝
     312      add_translates (
     313        [save_return ret_regs] @
     314        restore_hdws sregs @
     315        [adds_graph [
     316          ertl_st_push srah start_lbl;
     317          ertl_st_push sral start_lbl
     318        ]] @
     319        [adds_graph [
     320          ertl_st_del_frame start_lbl
     321        ]] @
     322        [assign_result]
     323      ) start_lbl tmp_lbl def
     324    in
     325    let def ≝ add_graph tmp_lbl last_stmt def in
     326      change_exit_label tmp_lbl def
     327  ] ?.
     328  cases not_implemented (* dep types here *)
     329qed.
    285330 
    286331definition allocate_regs_internal ≝
    287   λr: register.
     332  λr: Register.
    288333  λdef_sregs.
    289334  let 〈def, sregs〉 ≝ def_sregs in
     
    292337 
    293338definition allocate_regs ≝
    294   λrs: register_set.
     339  λrs.
    295340  λsaved: rs_set rs.
    296341  λdef.
    297342    rs_fold ? ? allocate_regs_internal saved 〈def, [ ]〉.
     343   
     344definition add_pro_and_epilogue ≝
     345  λparams.
     346  λret_regs.
     347  λdef.
     348  match fresh_regs_strong def 2 with
     349  [ dp def_sra def_sra_proof ⇒
     350    let def ≝ \fst def_sra in
     351    let sra ≝ \snd def_sra in
     352    let sral ≝ nth_safe ? 0 sra ? in
     353    let srah ≝ nth_safe ? 1 sra ? in
     354    let 〈def, sregs〉 ≝ allocate_regs register_list_set RegisterCalleeSaved def in
     355    let def ≝ add_prologue params sral srah sregs def in
     356    let def ≝ add_epilogue ret_regs sral srah sregs def in
     357      def
     358  ].
     359  [1: >def_sra_proof //
     360  |2: >def_sra_proof //
     361  ]
     362qed.
     363
     364definition set_params_hdw ≝
     365  λparams.
     366  match params with
     367  [ nil ⇒ [ λstart_lbl. adds_graph [ertl_st_skip start_lbl] start_lbl]
     368  | _ ⇒
     369    let l ≝ zip_pottier ? ? params parameters in
     370      restore_hdws l
     371  ].
     372
     373definition set_param_stack ≝
     374  λoff.
     375  λsrcr.
     376  λstart_lbl: label.
     377  λdest_lbl: label.
     378  λdef: ertl_internal_function.
     379  let 〈def, addr1〉 ≝ fresh_reg def in
     380  let 〈def, addr2〉 ≝ fresh_reg def in
     381  let 〈def, tmpr〉 ≝ fresh_reg def in
     382  let 〈ignore, int_off〉 ≝ half_add ? off int_size in
     383    adds_graph [
     384      ertl_st_int addr1 int_off start_lbl;
     385      ertl_st_get_hdw tmpr RegisterSPL start_lbl;
     386      ertl_st_clear_carry start_lbl;
     387      ertl_st_op2 Sub addr1 tmpr addr1 start_lbl;
     388      ertl_st_get_hdw tmpr RegisterSPH start_lbl;
     389      ertl_st_int addr2 (zero ?) start_lbl;
     390      ertl_st_op2 Sub addr2 tmpr addr2 start_lbl;
     391      ertl_st_store addr1 addr2 srcr start_lbl
     392    ] start_lbl dest_lbl def.   
     393
     394definition set_params_stack ≝
     395  λparams.
     396  match params with
     397  [ nil ⇒ [ λstart_lbl. adds_graph [ertl_st_skip start_lbl] start_lbl]
     398  | _ ⇒
     399    let f ≝ λi. λr. set_param_stack (bitvector_of_nat ? i) r in
     400      mapi ? ? f params
     401  ].
     402
     403axiom min_fst:
     404  ∀m, n: nat.
     405    min m n ≤ m.
     406
     407definition set_params ≝
     408  λparams.
     409  let n ≝ min (|params|) (|parameters|) in
     410  let hdw_stack_params ≝ split ? params n ? in
     411  let hdw_params ≝ \fst hdw_stack_params in
     412  let stack_params ≝ \snd hdw_stack_params in
     413    set_params_hdw hdw_params @ set_params_stack stack_params.
     414  @min_fst
     415qed.
     416
     417definition fetch_result ≝
     418  λret_regs.
     419  λstart_lbl: label.
     420  match reduce_strong ? ? RegisterSTS RegisterRets with
     421  [ dp crl first_crl_proof ⇒
     422    let commonl ≝ \fst (\fst crl) in
     423    let commonr ≝ \fst (\snd crl) in
     424    let f_save ≝ λst. λret. ertl_st_hdw_to_hdw st ret start_lbl in
     425    let saves ≝ map2 ? ? ? f_save commonl commonr ? in
     426    match reduce_strong ? ? ret_regs RegisterSTS with
     427    [ dp crl second_crl_proof ⇒
     428      let commonl ≝ \fst (\fst crl) in
     429      let commonr ≝ \fst (\snd crl) in
     430      let f_restore ≝ λr. λst. ertl_st_get_hdw r st start_lbl in
     431      let restores ≝ map2 ? ? ? f_restore commonl commonr ? in
     432        adds_graph (saves @ restores) start_lbl
     433    ]
     434  ].
     435  [ normalize nodelta; @second_crl_proof
     436  | @first_crl_proof
     437  ]
     438qed.
     439
     440definition translate_call_id ≝
     441  λf.
     442  λargs.
     443  λret_regs.
     444  λstart_lbl.
     445  λdest_lbl.
     446  λdef.
     447  let nb_args ≝ |args| in
     448    add_translates (
     449      set_params args @ [
     450      adds_graph [ ertl_st_call_id f (bitvector_of_nat ? nb_args) start_lbl ];
     451      fetch_result ret_regs
     452      ]
     453    ) start_lbl dest_lbl def.
     454
     455definition translate_stmt ≝
     456  λlbl.
     457  λstmt.
     458  λdef.
     459  match stmt with
     460  [ rtl_st_skip lbl' ⇒ add_graph lbl (ertl_st_skip lbl') def
     461  | rtl_st_cost cost_lbl lbl' ⇒ add_graph lbl (ertl_st_cost cost_lbl lbl') def
     462  | rtl_st_addr r1 r2 x lbl' ⇒
     463    adds_graph [
     464      ertl_st_addr_l r1 x lbl;
     465      ertl_st_addr_h r2 x lbl
     466    ] lbl lbl' def
     467  | rtl_st_stack_addr r1 r2 lbl' ⇒
     468    adds_graph [
     469      ertl_st_get_hdw r1 RegisterSPL lbl;
     470      ertl_st_get_hdw r2 RegisterSPH lbl
     471    ] lbl lbl' def
     472  | rtl_st_int r i lbl' ⇒ add_graph lbl (ertl_st_int r i lbl') def
     473  | rtl_st_move r1 r2 lbl' ⇒ add_graph lbl (ertl_st_move r1 r2 lbl') def
     474  | rtl_st_opaccs op destr1 destr2 srcr1 srcr2 lbl' ⇒
     475    adds_graph [
     476      ertl_st_opaccs_a op destr1 srcr1 srcr2 lbl;
     477      ertl_st_opaccs_b op destr2 srcr1 srcr2 lbl
     478      ] lbl lbl' def
     479  | rtl_st_op1 op1 destr srcr lbl' ⇒
     480    add_graph lbl (ertl_st_op1 op1 destr srcr lbl') def
     481  | rtl_st_op2 op2 destr srcr1 srcr2 lbl' ⇒
     482    add_graph lbl (ertl_st_op2 op2 destr srcr1 srcr2 lbl') def
     483  | rtl_st_clear_carry lbl' ⇒
     484    add_graph lbl (ertl_st_clear_carry lbl') def
     485  | rtl_st_set_carry lbl' ⇒
     486    add_graph lbl (ertl_st_set_carry lbl') def
     487  | rtl_st_load destr addr1 addr2 lbl' ⇒
     488    add_graph lbl (ertl_st_load destr addr1 addr2 lbl') def
     489  | rtl_st_store addr1 addr2 srcr lbl' ⇒
     490    add_graph lbl (ertl_st_store addr1 addr2 srcr lbl') def
     491  | rtl_st_call_id f args ret_regs lbl' ⇒
     492    translate_call_id f args ret_regs lbl lbl' def
     493  | rtl_st_cond srcr lbl_true lbl_false ⇒
     494    add_graph lbl (ertl_st_cond srcr lbl_true lbl_false) def
     495  | rtl_st_return ⇒
     496    add_graph lbl ertl_st_return def
     497  | _ ⇒ ? (* assert false: not implemented or should not happen *)
     498  ].
     499  cases not_implemented
     500qed.   
     501
     502   
    298503   
    299504definition save_return_internal ≝
  • src/utilities/RegisterSet.ma

    r782 r1075  
    66  rs_set: Type[0];
    77  rs_empty: rs_set;
    8   rs_singleton: register → rs_set;
    9   rs_fold: ∀A: Type[0]. (register → A → A) → rs_set → A → A;
    10   rs_insert: register → rs_set → rs_set;
    11   rs_exists: register → rs_set → bool;
     8  rs_singleton: Register → rs_set;
     9  rs_fold: ∀A: Type[0]. (Register → A → A) → rs_set → A → A;
     10  rs_insert: Register → rs_set → rs_set;
     11  rs_exists: Register → rs_set → bool;
    1212  rs_union: rs_set → rs_set → rs_set;
    13   rs_to_list: rs_set → list register;
    14   rs_from_list: list register → rs_set
     13  rs_to_list: rs_set → list Register;
     14  rs_from_list: list Register → rs_set
    1515}.
    1616
    1717(* dpm: horrendously inefficient, but will do for now *)
    1818
    19 definition rs_list_set_empty: list register ≝ [ ].
     19definition rs_list_set_empty: list Register ≝ [ ].
    2020
    21 definition rs_list_set_singleton: register → list register ≝ λr. [ r ].
     21definition rs_list_set_singleton: Register → list Register ≝ λr. [ r ].
    2222
    2323definition rs_list_set_fold ≝
    2424  λA: Type[0].
    25   λf: register → A → A.
    26   λl: list register.
     25  λf: Register → A → A.
     26  λl: list Register.
    2727  λa: A.
    2828    foldr ? ? f a l.
    2929   
    3030definition rs_list_set_insert ≝
    31   λr: register.
    32   λs: list register.
    33   match member ? (eq_identifier ?) r s with
     31  λr: Register.
     32  λs: list Register.
     33  match member ? eq_Register r s with
    3434  [ true ⇒ r :: s
    3535  | false ⇒ s
     
    3737 
    3838definition rs_list_set_exists ≝
    39   λr: register.
    40   λs: list register.
    41     member ? (eq_identifier ?) r s.
     39  λr: Register.
     40  λs: list Register.
     41    member ? eq_Register r s.
    4242   
    4343definition rs_list_set_union ≝
    44   λr: list register.
    45   λs: list register.
    46     nub_by ? (eq_identifier ?) (r @ s).
     44  λr: list Register.
     45  λs: list Register.
     46    nub_by ? eq_Register (r @ s).
    4747 
    4848definition rs_list_set_from_list ≝
    49   λr: list register.
    50     nub_by ? (eq_identifier ?) r.
     49  λr: list Register.
     50    nub_by ? eq_Register r.
    5151 
    5252definition register_list_set: register_set ≝
    53   mk_register_set (list register) rs_list_set_empty
     53  mk_register_set (list Register) rs_list_set_empty
    5454                  rs_list_set_singleton rs_list_set_fold
    5555                  rs_list_set_insert rs_list_set_exists
Note: See TracChangeset for help on using the changeset viewer.