Changeset 1075 for src/RTL


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

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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 ≝
Note: See TracChangeset for help on using the changeset viewer.