Changeset 1280 for src/RTL/RTLtoERTL.ma


Ignore:
Timestamp:
Sep 28, 2011, 2:43:37 AM (9 years ago)
Author:
sacerdot
Message:

Some progress in the porting of RTLAbstoRTL to the joint syntax:

1) common code with RTLtoERTL factorized out in joint/TranslateUtils.ma
2) this required yet another refactoring of the parameters in Joint.ma
3) RTLtoERTL ported to the new parameters; LTLtoLIN and LINtoASM are

probably broken but easily fixable a.t.m. RTLAbstoRTL still in progress,
but the difficult part is almost done.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/RTL/RTLtoERTL.ma

    r1278 r1280  
    33include "common/Identifiers.ma".
    44include "ERTL/ERTL.ma".
    5                            
    6 definition fresh_label ≝
    7   λglobals.λdef: joint_internal_function … (ertl_params globals).
    8     fresh LabelTag (joint_if_luniverse … def).
    9    
    10 definition change_label ≝
    11   λglobals.λe: joint_statement ertl_params_ globals.λl.
    12   match e with
    13   [ joint_st_goto _ ⇒ joint_st_goto … l
    14   | joint_st_return ⇒ joint_st_return ??
    15   | joint_st_sequential instr _ ⇒ joint_st_sequential … instr l].
    16 
    17 (*CSC: bad programming habit: the code below puts everywhere a fake
    18   label and then adds_graph fixes them *)
    19 (*CSC: the code is artificially fixed to work on ertl_statements, but
    20   it works on every graph_params *)
    21 (*CSC: this is just an instance of add_translates below! *)
    22 let rec adds_graph
    23   (globals: list ident)
    24   (stmt_list: list (ertl_statement globals)) (start_lbl: label)
    25   (dest_lbl: label) (def: ertl_internal_function globals)
    26     on stmt_list ≝
    27   match stmt_list with
    28   [ nil ⇒ add_graph … start_lbl (joint_st_goto … dest_lbl) def
    29   | cons stmt stmt_list ⇒
    30     match stmt_list with
    31     [ nil ⇒ add_graph … start_lbl (change_label … stmt dest_lbl) def
    32     | _ ⇒
    33       let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in
    34       let stmt ≝ change_label … stmt tmp_lbl in
    35       let def ≝ add_graph … start_lbl stmt def in
    36         adds_graph globals stmt_list tmp_lbl dest_lbl def]].
    37 
    38 (*CSC: bad programming habit: the code below puts everywhere a fake
    39   label and then adds_graph fixes them *)
    40 (*CSC: the code is artificially fixed to work on ertl_statements, but
    41   it works on every graph_params *)
    42 let rec add_translates
    43   (globals: list ident) (translate_list: list ?) (start_lbl: label) (dest_lbl: label)
    44   (def: ertl_internal_function globals)
    45     on translate_list ≝
    46   match translate_list with
    47   [ nil ⇒ add_graph … start_lbl (joint_st_goto … dest_lbl) def
    48   | cons trans translate_list ⇒
    49     match translate_list with
    50     [ nil ⇒ trans start_lbl dest_lbl def
    51     | _ ⇒
    52       let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in
    53       let def ≝ trans start_lbl tmp_lbl def in
    54         add_translates globals translate_list tmp_lbl dest_lbl def]].
    55 
    56 definition fresh_reg:
    57  ∀globals. ertl_internal_function globals → (ertl_internal_function globals) × register ≝
    58   λglobals,def.
    59     let 〈r,runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
    60      〈set_locals … (set_runiverse … def runiverse) (r::joint_if_locals … def), r〉.
    61 
    62 let rec fresh_regs (globals: list ident) (def: ertl_internal_function globals) (n: nat) on n ≝
    63   match n with
    64   [ O ⇒ 〈def, [ ]〉
    65   | S n' ⇒
    66     let 〈def', regs'〉 ≝ fresh_regs globals def n' in
    67     let 〈def', reg〉 ≝ fresh_reg … def' in
    68       〈def', reg :: regs'〉
    69   ].
    70  
    71 lemma fresh_regs_length:
    72  ∀globals.∀def: ertl_internal_function globals. ∀n: nat.
    73   |(\snd (fresh_regs … def n))| = n.
    74  #globals #def #n elim n
    75   [ %
    76   | #m whd in ⊢ (? → ??(??%)?) whd in ⊢ (? → ??(??match % with [ _ ⇒ ?])?)
    77     cases (fresh_regs globals def m) normalize nodelta
    78     #def' #regs #EQ change in EQ with (|regs| = m) <EQ
    79     change with
    80     (|let 〈a,b〉 ≝ let 〈x,y〉 ≝ let 〈r,runiverse〉 ≝ ? in ? in ? in ?| = ?)
    81     cases (fresh … (joint_if_runiverse … def')) normalize // ]
    82 qed.
    83 
    84 definition fresh_regs_strong:
    85  ∀globals. ertl_internal_function globals →
    86   ∀n: nat. Σregs: (ertl_internal_function globals) × (list register). |\snd regs| = n ≝
    87  λdef,n.fresh_regs def n. //
    88 qed.
     5include "joint/TranslateUtils.ma".
    896
    907definition save_hdws ≝
    … …  
    9310   λdestr_srcr.λstart_lbl.
    9411    let 〈destr, srcr〉 ≝ destr_srcr in
    95      adds_graph globals [ joint_st_sequential … (joint_instr_move … 〈pseudo destr,hardware srcr〉) start_lbl ] start_lbl
     12     adds_graph ertl_params1 globals [ joint_st_sequential … (joint_instr_move … 〈pseudo destr,hardware srcr〉) start_lbl ] start_lbl
    9613  in
    9714   map ? ? save_hdws_internal l.
    … …  
    10320    λstart_lbl: label.
    10421     let 〈srcr, destr〉 ≝ srcr_destr in
    105      adds_graph globals [ joint_st_sequential … (joint_instr_move … 〈hardware destr, pseudo srcr〉) start_lbl ] start_lbl
     22     adds_graph ertl_params1 globals [ joint_st_sequential … (joint_instr_move … 〈hardware destr, pseudo srcr〉) start_lbl ] start_lbl
    10623   in
    10724    map ? ? restore_hdws_internal l.
    … …  
    11128  λparams: list register.
    11229  match params with
    113   [ nil ⇒ [λstart_lbl: label. adds_graph globals [ joint_st_goto … start_lbl ] start_lbl]
     30  [ nil ⇒ [λstart_lbl: label. adds_graph ertl_params1 globals [ joint_st_goto … start_lbl ] start_lbl]
    11431  | _ ⇒
    11532    let l ≝ zip_pottier ? ? params RegisterParams in
    … …  
    12643  let 〈def, tmpr〉 ≝ fresh_reg … def in
    12744  let 〈carry, int_offset〉 ≝ half_add ? (bitvector_of_nat ? off) int_size in
    128   adds_graph globals [
     45  adds_graph ertl_params1 globals [
    12946    joint_st_sequential … (joint_instr_extension … (ertl_st_ext_frame_size addr1)) start_lbl;
    13047    joint_st_sequential … (joint_instr_int … tmpr int_offset) start_lbl;
    … …  
    16077  let start_lbl ≝ joint_if_entry … (ertl_params globals) def in
    16178  let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in
    162   match lookup … (joint_if_code … (ertl_params globals) def) start_lbl
     79  match lookup … (joint_if_code … def) start_lbl
    16380    return λx. x ≠ None ? → ertl_internal_function globals with
    16481  [ None ⇒ λnone_absrd. ⊥
    … …  
    16683    let def ≝
    16784      add_translates …
    168          ((adds_graph … [
    169                      joint_st_sequential … (joint_instr_extension ertl_params_ globals ertl_st_ext_new_frame) start_lbl
     85         ((adds_graph ertl_params1 … [
     86                     joint_st_sequential ertl_params_ … (joint_instr_extension ertl_params__ globals ertl_st_ext_new_frame) start_lbl
    17087                   ]) ::
    17188         (adds_graph … [
    … …  
    196113    let restl ≝ \snd (\fst crl) in
    197114    let restr ≝ \snd (\snd crl) in
    198     let init_tmpr ≝ joint_st_sequential ertl_params_ … (joint_instr_int … tmpr (zero ?)) start_lbl in
     115    let init_tmpr ≝ joint_st_sequential ertl_params_ … (joint_instr_int … tmpr (zero …)) start_lbl in
    199116    let f_save ≝ λst. λr. joint_st_sequential ertl_params_ … (joint_instr_move … 〈hardware st, pseudo r〉) start_lbl in
    200     let saves ≝ map2 ? ? ? f_save commonl commonr crl_proof in
     117    let saves ≝ map2 … f_save commonl commonr crl_proof in
    201118    let f_default ≝ λst. joint_st_sequential ertl_params_ … (joint_instr_move … 〈hardware st, pseudo tmpr〉) start_lbl in
    202     let defaults ≝ map ? ? f_default restl in
    203       adds_graph … (init_tmpr :: saves @ defaults) start_lbl dest_lbl def
     119    let defaults ≝ map … f_default restl in
     120      adds_graph ertl_params1 … (init_tmpr :: saves @ defaults) start_lbl dest_lbl def
    204121  ].
    205122
    … …  
    212129    let f ≝ λret. λst. joint_st_sequential ertl_params_ globals (joint_instr_move … 〈hardware ret, hardware st〉) start_lbl in
    213130    let insts ≝ map2 ? ? ? f commonl commonr crl_proof in
    214       adds_graph … insts start_lbl
     131      adds_graph ertl_params1 … insts start_lbl
    215132  ].
    216133
    … …  
    224141  let start_lbl ≝ joint_if_exit … (ertl_params globals) def in
    225142  let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in
    226   match lookup … (joint_if_code … (ertl_params globals) def) start_lbl
     143  match lookup … (joint_if_code … def) start_lbl
    227144    return λx. x ≠ None ? → ertl_internal_function globals with
    228145  [ None ⇒ λnone_absrd. ⊥
    229146  | Some last_stmt ⇒ λsome_prf.
    230147    let def ≝
    231       add_translates … (
     148      add_translates ertl_params1 … (
    232149        [save_return globals ret_regs] @
    233150        restore_hdws … sregs @
    … …  
    236153          joint_st_sequential … (joint_instr_push … sral) start_lbl
    237154        ]] @
    238         [adds_graph … [
     155        [adds_graph ertl_params1 … [
    239156          joint_st_sequential … (joint_instr_extension … ertl_st_ext_del_frame) start_lbl
    240157        ]] @
    … …  
    261178    λdef_sregs.
    262179    let 〈def, sregs〉 ≝ def_sregs in
    263     let 〈def, r'〉 ≝ fresh_reg globals def in
     180    let 〈def, r'〉 ≝ fresh_reg ertl_params0 globals def in
    264181      〈def, 〈r', r〉 :: sregs〉
    265182   in
    … …  
    271188  λret_regs.
    272189  λdef.
    273   match fresh_regs_strong globals def 2 with
     190  match fresh_regs_strong … globals def 2 with
    274191  [ dp def_sra def_sra_proof ⇒
    275192    let def ≝ \fst def_sra in
    … …  
    305222  let 〈def, tmpr〉 ≝ fresh_reg … def in
    306223  let 〈ignore, int_off〉 ≝ half_add ? off int_size in
    307     adds_graph ? [
     224    adds_graph ertl_params1 … [
    308225      joint_st_sequential … (joint_instr_int … addr1 int_off) start_lbl;
    309226      joint_st_sequential … (joint_instr_move … 〈pseudo tmpr, hardware RegisterSPL〉) start_lbl;
    … …  
    319236  λglobals,params.
    320237  match params with
    321   [ nil ⇒ [ λstart_lbl. adds_graph globals [joint_st_goto … start_lbl] start_lbl]
     238  [ nil ⇒ [ λstart_lbl. adds_graph ertl_params1 globals [joint_st_goto … start_lbl] start_lbl]
    322239  | _ ⇒
    323240    let f ≝ λi. λr. set_param_stack … (bitvector_of_nat ? i) r in
    … …  
    350267      let f_restore ≝ λr. λst. joint_st_sequential ertl_params_ … (joint_instr_move … 〈pseudo r, hardware st〉) start_lbl in
    351268      let restores ≝ map2 ? ? ? f_restore commonl commonr ? in
    352         adds_graph … (saves @ restores) start_lbl]].
     269        adds_graph ertl_params1 … (saves @ restores) start_lbl]].
    353270[@second_crl_proof | @first_crl_proof]
    354271qed.
    … …  
    362279  λdef.
    363280  let nb_args ≝ |args| in
    364     add_translates globals (
     281    add_translates ertl_params1 globals (
    365282      set_params … args @ [
    366       adds_graph … [ joint_st_sequential … (joint_instr_call_id … f nb_args it) start_lbl ];
     283      adds_graph ertl_params1 … [ joint_st_sequential … (joint_instr_call_id … f nb_args it) start_lbl ];
    367284      fetch_result … ret_regs
    368285      ]
    … …  
    388305         let 〈r1,r2〉 ≝ rs in
    389306         let rs ≝ 〈pseudo r1, pseudo r2〉 in
    390           add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_move … rs) lbl') def
     307          add_graph ertl_params1 ? lbl (joint_st_sequential … (joint_instr_move … rs) lbl') def
    391308      | joint_instr_extension ext ⇒
    392309         match ext with
    393310          [ rtlntc_st_ext_call_ptr _ _ _ _ ⇒ ⊥ (*CSC: XXXX not implemented in OCaml too *)
    394311          | rtlntc_st_ext_address r1 r2 ⇒
    395              adds_graph … [
     312             adds_graph ertl_params1 … [
    396313              joint_st_sequential … (joint_instr_move … 〈pseudo r1, hardware RegisterSPL〉) lbl;
    397314              joint_st_sequential … (joint_instr_move … 〈pseudo r2, hardware RegisterSPH〉) lbl
    … …  
    400317        the problem is call_id that takes different parameters, but that is pattern-matched
    401318        above. It could be made nicer at the cost of making all the rest of the code uglier *)
    402       | joint_instr_cost_label cost_lbl ⇒ add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_cost_label … cost_lbl) lbl') def
    403       | joint_instr_address x prf r1 r2 ⇒ add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_address … x prf r1 r2) lbl') def
    404       | joint_instr_int r i ⇒  add_graph … lbl (joint_st_sequential ertl_params_ globals (joint_instr_int … r i) lbl') def
     319      | joint_instr_cost_label cost_lbl ⇒ add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_cost_label … cost_lbl) lbl') def
     320      | joint_instr_address x prf r1 r2 ⇒ add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_address … x prf r1 r2) lbl') def
     321      | joint_instr_int r i ⇒  add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_int … r i) lbl') def
    405322      | joint_instr_opaccs op destr1 destr2 srcr1 srcr2 ⇒
    406           add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_opaccs … op destr1 destr2 srcr1 srcr2) lbl') def
     323          add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_opaccs … op destr1 destr2 srcr1 srcr2) lbl') def
    407324      | joint_instr_op1 op1 destr srcr ⇒
    408         add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_op1 … op1 destr srcr) lbl') def
     325        add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_op1 … op1 destr srcr) lbl') def
    409326      | joint_instr_op2 op2 destr srcr1 srcr2 ⇒
    410         add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_op2 … op2 destr srcr1 srcr2) lbl') def
     327        add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_op2 … op2 destr srcr1 srcr2) lbl') def
    411328      | joint_instr_clear_carry ⇒
    412         add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_clear_carry …) lbl') def
     329        add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_clear_carry …) lbl') def
    413330      | joint_instr_set_carry ⇒
    414         add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_set_carry …) lbl') def
     331        add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_set_carry …) lbl') def
    415332      | joint_instr_load destr addr1 addr2 ⇒
    416         add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_load … destr addr1 addr2) lbl') def
     333        add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_load … destr addr1 addr2) lbl') def
    417334      | joint_instr_store addr1 addr2 srcr ⇒
    418         add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_store … addr1 addr2 srcr) lbl') def
     335        add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_store … addr1 addr2 srcr) lbl') def
    419336      | joint_instr_cond srcr lbl_true ⇒
    420         add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_cond … srcr lbl_true) lbl') def
     337        add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_cond … srcr lbl_true) lbl') def
    421338      | joint_instr_comment msg ⇒
    422         add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_comment … msg) lbl') def
     339        add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_comment … msg) lbl') def
    423340      ]].
    424   cases not_implemented (*CSC: XXXX spurious things in the syntax and ptr_calls *)
     341  @not_implemented (*CSC: XXXX spurious things in the syntax and ptr_calls *)
    425342qed.
    426343
    … …  
    452369  λglobals.
    453370  λstmt.
    454   λdef.
     371  λdef: joint_internal_function … (ertl_params globals).
    455372  let 〈entry, nuniv〉 ≝ fresh_label … def in
    456373  let graph ≝ add ? ? (joint_if_code … def) entry stmt in
    … …  
    476393         match inst with
    477394          [ joint_instr_cost_label cost_lbl ⇒
    478              〈Some … cost_lbl, add_graph ertl_params_ globals lbl (joint_st_goto … lbl) def〉
     395             〈Some … cost_lbl, add_graph ertl_params1 globals lbl (joint_st_goto … lbl) def〉
    479396          | _ ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ]
    480397      | joint_st_return ⇒ 〈None …, def〉
Note: See TracChangeset for help on using the changeset viewer.