Changeset 1259


Ignore:
Timestamp:
Sep 23, 2011, 11:49:44 AM (8 years ago)
Author:
sacerdot
Message:

More progress towards new Joint data type.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLtoERTL.ma

    r1258 r1259  
    295295
    296296definition set_param_stack ≝
     297  λglobals.
    297298  λoff.
    298299  λsrcr.
    299300  λstart_lbl: label.
    300301  λdest_lbl: label.
    301   λdef: ertl_internal_function.
    302   let 〈def, addr1〉 ≝ fresh_reg def in
    303   let 〈def, addr2〉 ≝ fresh_reg def in
    304   let 〈def, tmpr〉 ≝ fresh_reg def in
     302  λdef: ertl_internal_function globals.
     303  let 〈def, addr1〉 ≝ fresh_reg def in
     304  let 〈def, addr2〉 ≝ fresh_reg def in
     305  let 〈def, tmpr〉 ≝ fresh_reg def in
    305306  let 〈ignore, int_off〉 ≝ half_add ? off int_size in
    306     adds_graph [
    307       ertl_st_int addr1 int_off start_lbl;
    308       ertl_st_get_hdw tmpr RegisterSPL start_lbl;
    309       ertl_st_clear_carry start_lbl;
    310       ertl_st_op2 Sub addr1 tmpr addr1 start_lbl;
    311       ertl_st_get_hdw tmpr RegisterSPH start_lbl;
    312       ertl_st_int addr2 (zero ?) start_lbl;
    313       ertl_st_op2 Sub addr2 tmpr addr2 start_lbl;
    314       ertl_st_store addr1 addr2 srcr start_lbl
     307    adds_graph ? [
     308      joint_st_sequential … (joint_instr_int … addr1 int_off) start_lbl;
     309      joint_st_sequential … (joint_instr_move … 〈pseudo tmpr, hardware RegisterSPL〉) start_lbl;
     310      joint_st_sequential … (joint_instr_clear_carry …) start_lbl;
     311      joint_st_sequential … (joint_instr_op2 … Sub addr1 tmpr addr1) start_lbl;
     312      joint_st_sequential … (joint_instr_move … 〈pseudo tmpr, hardware RegisterSPH〉) start_lbl;
     313      joint_st_sequential … (joint_instr_int … addr2 (zero ?)) start_lbl;
     314      joint_st_sequential … (joint_instr_op2 … Sub addr2 tmpr addr2) start_lbl;
     315      joint_st_sequential … (joint_instr_store … addr1 addr2 srcr) start_lbl
    315316    ] start_lbl dest_lbl def.   
    316317
    317318definition set_params_stack ≝
    318   λparams.
     319  λglobals,params.
    319320  match params with
    320   [ nil ⇒ [ λstart_lbl. adds_graph [ertl_st_skip start_lbl] start_lbl]
     321  [ nil ⇒ [ λstart_lbl. adds_graph globals [joint_st_goto … start_lbl] start_lbl]
    321322  | _ ⇒
    322     let f ≝ λi. λr. set_param_stack (bitvector_of_nat ? i) r in
    323       mapi ? ? f params
    324   ].
    325 
    326 axiom min_fst:
    327   ∀m, n: nat.
    328     min m n ≤ m.
     323    let f ≝ λi. λr. set_param_stack … (bitvector_of_nat ? i) r in
     324      mapi ? ? f params].
    329325
    330326definition set_params ≝
    331   λparams.
     327  λglobals,params.
    332328  let n ≝ min (|params|) (|RegisterParams|) in
    333329  let hdw_stack_params ≝ split ? params n ? in
    334330  let hdw_params ≝ \fst hdw_stack_params in
    335331  let stack_params ≝ \snd hdw_stack_params in
    336     set_params_hdw hdw_params @ set_params_stack stack_params.
    337   @min_fst
     332    set_params_hdw globals hdw_params @ set_params_stack globals stack_params.
     333/2/
    338334qed.
    339335
    340336definition fetch_result ≝
     337  λglobals.
    341338  λret_regs.
    342339  λstart_lbl: label.
     
    345342    let commonl ≝ \fst (\fst crl) in
    346343    let commonr ≝ \fst (\snd crl) in
    347     let f_save ≝ λst. λret. ertl_st_hdw_to_hdw st ret start_lbl in
     344    let f_save ≝ λst. λret. joint_st_sequential ertl_params_ globals (joint_instr_move … 〈hardware st, hardware ret〉) start_lbl in
    348345    let saves ≝ map2 ? ? ? f_save commonl commonr ? in
    349346    match reduce_strong ? ? ret_regs RegisterSTS with
     
    351348      let commonl ≝ \fst (\fst crl) in
    352349      let commonr ≝ \fst (\snd crl) in
    353       let f_restore ≝ λr. λst. ertl_st_get_hdw r st start_lbl in
     350      let f_restore ≝ λr. λst. joint_st_sequential ertl_params_ … (joint_instr_move … 〈pseudo r, hardware st〉) start_lbl in
    354351      let restores ≝ map2 ? ? ? f_restore commonl commonr ? in
    355         adds_graph (saves @ restores) start_lbl
    356     ]
    357   ].
    358   [ normalize nodelta; @second_crl_proof
    359   | @first_crl_proof
    360   ]
     352        adds_graph … (saves @ restores) start_lbl]].
     353[@second_crl_proof | @first_crl_proof]
    361354qed.
    362355
    363356definition translate_call_id ≝
    364   λf.
     357  λglobals,f.
    365358  λargs.
    366359  λret_regs.
     
    369362  λdef.
    370363  let nb_args ≝ |args| in
    371     add_translates (
    372       set_params args @ [
    373       adds_graph [ ertl_st_call_id f nb_args start_lbl ];
    374       fetch_result ret_regs
     364    add_translates globals (
     365      set_params args @ [
     366      adds_graph … [ joint_st_sequential … (joint_instr_call_id … f nb_args) start_lbl ];
     367      fetch_result ret_regs
    375368      ]
    376369    ) start_lbl dest_lbl def.
    377370
    378371definition translate_stmt ≝
     372  λglobals.
    379373  λlbl.
    380374  λstmt.
    381375  λdef.
    382376  match stmt with
    383   [ rtl_st_skip lbl' ⇒ add_graph lbl (ertl_st_skip lbl') def
    384   | rtl_st_cost cost_lbl lbl' ⇒ add_graph lbl (ertl_st_cost cost_lbl lbl') def
    385   | rtl_st_addr r1 r2 x lbl' ⇒ add_graph lbl (ertl_st_addr r1 r2 x lbl') def
     377  [ rtl_st_skip lbl' ⇒ add_graph lbl (ertl_st_skip lbl') def
     378  | rtl_st_cost cost_lbl lbl' ⇒ add_graph lbl (ertl_st_cost cost_lbl lbl') def
     379  | rtl_st_addr r1 r2 x lbl' ⇒ add_graph lbl (ertl_st_addr r1 r2 x lbl') def
    386380  | rtl_st_stack_addr r1 r2 lbl' ⇒
    387     adds_graph [
     381    adds_graph [
    388382      ertl_st_get_hdw r1 RegisterSPL lbl;
    389383      ertl_st_get_hdw r2 RegisterSPH lbl
    390384    ] lbl lbl' def
    391   | rtl_st_int r i lbl' ⇒  add_graph lbl (ertl_st_int r i lbl') def
    392   | rtl_st_move r1 r2 lbl' ⇒ add_graph lbl (ertl_st_move r1 r2 lbl') def
     385  | rtl_st_int r i lbl' ⇒  add_graph lbl (ertl_st_int r i lbl') def
     386  | rtl_st_move r1 r2 lbl' ⇒ add_graph lbl (ertl_st_move r1 r2 lbl') def
    393387  | rtl_st_opaccs op destr1 destr2 srcr1 srcr2 lbl' ⇒
    394       add_graph lbl (ertl_st_opaccs op destr1 destr2 srcr1 srcr2 lbl) def
    395 (* XXX: change from o'caml
    396     adds_graph [
    397       ertl_st_opaccs_a op destr1 srcr1 srcr2 lbl;
    398       ertl_st_opaccs_b op destr2 srcr1 srcr2 lbl
    399       ] lbl lbl' def
    400 *)
     388      add_graph … lbl (ertl_st_opaccs op destr1 destr2 srcr1 srcr2 lbl) def
    401389  | rtl_st_op1 op1 destr srcr lbl' ⇒
    402     add_graph lbl (ertl_st_op1 op1 destr srcr lbl') def
     390    add_graph lbl (ertl_st_op1 op1 destr srcr lbl') def
    403391  | rtl_st_op2 op2 destr srcr1 srcr2 lbl' ⇒
    404     add_graph lbl (ertl_st_op2 op2 destr srcr1 srcr2 lbl') def
     392    add_graph lbl (ertl_st_op2 op2 destr srcr1 srcr2 lbl') def
    405393  | rtl_st_clear_carry lbl' ⇒
    406     add_graph lbl (ertl_st_clear_carry lbl') def
     394    add_graph lbl (ertl_st_clear_carry lbl') def
    407395  | rtl_st_set_carry lbl' ⇒
    408     add_graph lbl (ertl_st_set_carry lbl') def
     396    add_graph lbl (ertl_st_set_carry lbl') def
    409397  | rtl_st_load destr addr1 addr2 lbl' ⇒
    410     add_graph lbl (ertl_st_load destr addr1 addr2 lbl') def
     398    add_graph lbl (ertl_st_load destr addr1 addr2 lbl') def
    411399  | rtl_st_store addr1 addr2 srcr lbl' ⇒
    412     add_graph lbl (ertl_st_store addr1 addr2 srcr lbl') def
     400    add_graph lbl (ertl_st_store addr1 addr2 srcr lbl') def
    413401  | rtl_st_call_id f args ret_regs lbl' ⇒
    414     translate_call_id f args ret_regs lbl lbl' def
     402    translate_call_id f args ret_regs lbl lbl' def
    415403  | rtl_st_cond srcr lbl_true lbl_false ⇒
    416     add_graph lbl (ertl_st_cond srcr lbl_true lbl_false) def
     404    add_graph lbl (ertl_st_cond srcr lbl_true lbl_false) def
    417405  | rtl_st_return ⇒
    418     add_graph lbl ertl_st_return def
     406    add_graph lbl ertl_st_return def
    419407  | _ ⇒ ? (* assert false: not implemented or should not happen *)
    420408  ].
Note: See TracChangeset for help on using the changeset viewer.