Changeset 782 for src/RTL/RTLtoERTL.ma


Ignore:
Timestamp:
Apr 28, 2011, 5:36:33 PM (10 years ago)
Author:
mulligan
Message:

More work on rtl-ertl pass from today, plus resolved conflict.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLtoERTL.ma

    r777 r782  
    11include "RTL/RTL.ma".
    22include "ERTL/ERTL.ma".
    3 include "ASM/RegisterSet.ma".
     3include "utilities/RegisterSet.ma".
    44
    55definition change_exit_label ≝
     
    1010  let ertl_if_params' ≝ ertl_if_params p in
    1111  let ertl_if_locals' ≝ ertl_if_locals p in
     12  let ertl_if_stacksize' ≝ ertl_if_stacksize p in
    1213  let ertl_if_graph' ≝ ertl_if_graph p in
    1314  let ertl_if_entry' ≝ ertl_if_entry p in
    1415  let ertl_if_exit' ≝ l in
    1516    mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse'
    16                               ertl_if_params' ertl_if_locals'
     17                              ertl_if_params' ertl_if_locals' ertl_if_stacksize'
    1718                              ertl_if_graph' ertl_if_entry' ertl_if_exit'.
    1819
     
    2425  let ertl_if_params' ≝ ertl_if_params p in
    2526  let ertl_if_locals' ≝ ertl_if_locals p in
     27  let ertl_if_stacksize' ≝ ertl_if_stacksize p in
    2628  let ertl_if_graph' ≝ ertl_if_graph p in
    2729  let ertl_if_entry' ≝ l in
    2830  let ertl_if_exit' ≝ ertl_if_exit p in
    2931    mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse'
    30                               ertl_if_params' ertl_if_locals'
     32                              ertl_if_params' ertl_if_locals' ertl_if_stacksize'
    3133                              ertl_if_graph' ertl_if_entry' ertl_if_exit'.
    3234                             
     
    3941  let ertl_if_params' ≝ ertl_if_params p in
    4042  let ertl_if_locals' ≝ ertl_if_locals p in
     43  let ertl_if_stacksize' ≝ ertl_if_stacksize p in
    4144  let ertl_if_graph' ≝ add ? ? (ertl_if_graph p) l stmt in
    4245  let ertl_if_entry' ≝ ertl_if_entry p in
    4346  let ertl_if_exit' ≝ ertl_if_exit p in
    4447    mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse'
    45                               ertl_if_params' ertl_if_locals'
     48                              ertl_if_params' ertl_if_locals' ertl_if_stacksize'
    4649                              ertl_if_graph' ertl_if_entry' ertl_if_exit'.
    4750                             
     
    330333    ]
    331334  ].
    332    
     335 
     336axiom add_pro_and_epilogue:
     337  ∀rs: register_set.
     338  ∀params: list register.
     339  ∀ret_args: list register.
     340  ∀def: ertl_internal_function.
     341    option ertl_internal_function.
     342   
     343(*
     344  dpm: address callee_saved problem   
    333345definition add_pro_and_epilogue ≝
    334346  λrs: register_set.
     
    337349  λdef.
    338350  let 〈def, sra〉 ≝ fresh_regs def 2 in
    339   let sral ≝ nth ? 0 sra in
    340   let srah ≝ nth sra 1 in
     351  let sral ≝ safe_nth ? 0 sra ? in
     352  let srah ≝ safe_nth ? 1 sra ? in
    341353  let 〈def, sregs〉 ≝ allocate_regs callee_saved def in
    342354  let def ≝ add_prologue params sral srah sregs def in
    343355  let def ≝ add_epilogue ret_args sral srah sregs def in
    344     def.
     356    def. 
     357*)
     358
     359definition set_params_hdw ≝
     360  λparams.
     361  match length ? params with
     362  [ O ⇒ Some ? [ get_params_hdw_internal ]
     363  | _ ⇒
     364    match zip ? ? params parameters with
     365    [ None ⇒ None ?
     366    | Some zipped_params ⇒ Some ? (restore_hdws zipped_params)
     367    ]
     368  ].
     369 
     370definition set_param_stack ≝
     371  λoff: nat.
     372  λsrcr.
     373  λstart_lbl, dest_lbl: label.
     374  λdef.
     375  let 〈def, addr1〉 ≝ fresh_reg def in
     376  let 〈def, addr2〉 ≝ fresh_reg def in
     377  let 〈def, tmpr〉 ≝ fresh_reg def in
     378  let 〈int_offset, ignore〉 ≝ add_8_with_carry (bitvector_of_nat ? off) int_size false in
     379    adds_graph [
     380      ertl_st_int addr2 int_offset start_lbl;
     381      ertl_st_get_hdw tmpr RegisterSPL start_lbl;
     382      ertl_st_clear_carry start_lbl;
     383      ertl_st_op2 Sub addr1 tmpr addr1 start_lbl;
     384      ertl_st_get_hdw tmpr RegisterSPH start_lbl;
     385      ertl_st_int addr2 (bitvector_of_nat ? 0) start_lbl;
     386      ertl_st_op2 Sub addr2 tmpr addr2 start_lbl;
     387      ertl_st_store addr1 addr2 srcr start_lbl
     388    ] start_lbl dest_lbl def.
     389
     390definition set_params_stack ≝
     391  λparams.
     392  match length ? params with
     393  [ O ⇒ [ get_params_hdw_internal ]
     394  | _ ⇒ mapi ? ? set_param_stack params
     395 
     396  ].
     397 
     398definition set_params ≝
     399  λparams.
     400  let n ≝ min (length ? params) (length ? parameters) in
     401  let 〈hdw_params, stack_params〉 ≝ list_split ? n params in
     402    match set_params_hdw hdw_params with
     403    [ None ⇒ None ?
     404    | Some hdw_params' ⇒ Some ? (hdw_params' @ (set_params_stack stack_params))
     405    ].
     406   
     407definition fetch_result ≝
     408  λret_regs.
     409  λstart_lbl.
     410  match ret_regs with
     411  [ nil ⇒ adds_graph [ertl_st_skip start_lbl] start_lbl
     412  | cons hd tl ⇒
     413    match tl with
     414    [ nil ⇒
     415      adds_graph [
     416        ertl_st_hdw_to_hdw RegisterST0 RegisterDPL start_lbl;
     417        ertl_st_get_hdw hd RegisterST0 start_lbl
     418      ] start_lbl
     419    | cons hd' tl' ⇒
     420      adds_graph [
     421        ertl_st_hdw_to_hdw RegisterST0 RegisterDPL start_lbl;
     422        ertl_st_hdw_to_hdw RegisterST1 RegisterDPH start_lbl;
     423        ertl_st_get_hdw hd RegisterST0 start_lbl;
     424        ertl_st_get_hdw hd' RegisterST1 start_lbl
     425      ] start_lbl
     426    ]
     427  ].
     428 
     429definition translate_call_id ≝
     430  λf.
     431  λargs.
     432  λret_regs.
     433  λstart_lbl, dest_lbl: label.
     434  λdef.
     435  let nb_args ≝ bitvector_of_nat ? (length ? args) in
     436  match set_params args with
     437  [ None ⇒ None ?
     438  | Some params_args ⇒
     439    add_translates (
     440      params_args @ [
     441        adds_graph [ ertl_st_call_id f nb_args start_lbl ] ;
     442        fetch_result ret_regs
     443      ]) start_lbl dest_lbl def
     444  ].
     445 
     446definition translate_stmt ≝
     447  λlbl: label.
     448  λstmt: rtl_statement.
     449  λdef: ertl_internal_function.
     450  match stmt with
     451  [ rtl_st_skip lbl' ⇒
     452    Some ? (add_graph lbl (ertl_st_skip lbl') def)
     453  | rtl_st_cost cost_lbl lbl' ⇒
     454    Some ? (add_graph lbl (ertl_st_cost cost_lbl lbl') def)
     455  | rtl_st_addr r1 r2 x lbl' ⇒
     456    adds_graph [
     457      ertl_st_addr_l r1 x lbl;
     458      ertl_st_addr_h r2 x lbl
     459    ] lbl lbl' def
     460  | rtl_st_stack_addr r1 r2 lbl' ⇒
     461    adds_graph [
     462      ertl_st_get_hdw r1 RegisterSPL lbl;
     463      ertl_st_get_hdw r2 RegisterSPH lbl
     464    ] lbl lbl' def
     465  | rtl_st_int r i lbl' ⇒
     466    Some ? (add_graph lbl (ertl_st_int r i lbl') def)
     467  | rtl_st_move r1 r2 lbl' ⇒
     468    Some ? (add_graph lbl (ertl_st_move r1 r2 lbl') def)
     469  | rtl_st_opaccs opaccs d s1 s2 lbl' ⇒
     470    Some ? (add_graph lbl (ertl_st_opaccs opaccs d s1 s2 lbl') def)
     471  | rtl_st_op1 op1 d s lbl' ⇒
     472    Some ? (add_graph lbl (ertl_st_op1 op1 d s lbl') def)
     473  | rtl_st_op2 op2 d s1 s2 lbl' ⇒
     474    Some ? (add_graph lbl (ertl_st_op2 op2 d s1 s2 lbl') def)
     475  | rtl_st_clear_carry lbl' ⇒
     476    Some ? (add_graph lbl (ertl_st_clear_carry lbl') def)
     477  | rtl_st_load d a1 a2 lbl' ⇒
     478    Some ? (add_graph lbl (ertl_st_load d a1 a2 lbl') def)
     479  | rtl_st_store a1 a2 s lbl' ⇒
     480    Some ? (add_graph lbl (ertl_st_store a1 a2 s lbl') def)
     481  | rtl_st_call_id f args ret_regs lbl' ⇒
     482    translate_call_id f args ret_regs lbl lbl' def
     483  | rtl_st_call_ptr r1 r2 regs1 regs2 lbl ⇒ None ? (* dpm: todo *)
     484  | rtl_st_cond_acc src lbl_true lbl_false ⇒
     485    Some ? (add_graph lbl (ertl_st_cond_acc src lbl_true lbl_false) def)
     486  | rtl_st_return ret_regs ⇒
     487    Some ? (add_graph lbl (ertl_st_return ret_regs) def)
     488  | rtl_st_tailcall_id ident regs ⇒ None ? (* dpm: impossible *)
     489  | rtl_st_tailcall_ptr r1 r2 regs ⇒ None ? (* dpm: impossible *)
     490  ].
     491
     492(* dpm: this should not be option, fix *)
     493axiom map_fold:
     494  ∀A, B: Type[0].
     495  ∀f: label → A → B → option B.
     496  ∀m: rtl_statement_graph.
     497  ∀b: B.
     498    B.
     499   
     500definition translate_internal ≝
     501  λdef.
     502  let nb_params ≝ length ? (rtl_if_params def) in
     503  let added_stacksize ≝ max 0 (nb_params - (length ? parameters)) in
     504  let new_locals ≝ nub_by ? (eq_identifier ?) ((rtl_if_locals def) @ (rtl_if_params def)) in
     505  let def' ≝
     506    mk_ertl_internal_function
     507      (rtl_if_luniverse def) (rtl_if_runiverse def)
     508      nb_params new_locals ((rtl_if_stacksize def) + added_stacksize)
     509      (empty_map ? ?) (rtl_if_entry def) (rtl_if_exit def) in
     510  let def' ≝ map_fold ? ? translate_stmt (rtl_if_graph def) def' in
     511  let def' ≝ add_pro_and_epilogue register_list_set (rtl_if_params def) (rtl_if_result def) def' in
     512    def'.
     513   
     514definition translate_funct ≝
     515  λid_def: ident × ?.
     516  let 〈id, def〉 ≝ id_def in
     517  let def' ≝
     518    match def with
     519    [ rtl_f_internal def ⇒
     520      match translate_internal def with
     521      [ None ⇒ None ?
     522      | Some internal_def ⇒ Some ? (ertl_f_internal internal_def)
     523      ]
     524    | rtl_f_external def ⇒ Some ? (ertl_f_external def)
     525    ] in
     526  〈id, def'〉.
     527
     528definition generate ≝
     529  λstmt.
     530  λdef.
     531  let entry ≝ fresh_label def in
     532  match entry with
     533  [ None ⇒ None ?
     534  | Some entry ⇒
     535    let def ≝ add_graph entry stmt def in
     536      Some ? (change_entry_label entry def)
     537  ].
     538 
Note: See TracChangeset for help on using the changeset viewer.