Changeset 2286 for src/RTL/RTLToERTL.ma


Ignore:
Timestamp:
Aug 2, 2012, 3:18:11 PM (8 years ago)
Author:
tranquil
Message:

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLToERTL.ma

    r2103 r2286  
    77include alias "basics/lists/list.ma".
    88
    9 definition save_hdws ≝
    10  λglobals,l.
     9definition ertl_fresh_reg:
     10 ∀globals.freshT ERTL globals register ≝
     11  λglobals,def.
     12    let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
     13    〈set_locals ?? (set_runiverse ?? def runiverse)(r::joint_if_locals ?? def), r〉.
     14
     15definition save_hdws :
     16  ∀globals.list (register×Register) → list (joint_seq ERTL globals) ≝
     17 λglobals.
    1118  let save_hdws_internal ≝
    12    λdestr_srcr.λstart_lbl.
    13     let 〈destr, srcr〉 ≝ destr_srcr in
    14      adds_graph ertl_params1 globals [ sequential ertl_params_ … (MOVE … 〈pseudo destr,hardware srcr〉) ] start_lbl
    15   in
    16    map ? ? save_hdws_internal l.
    17 
    18 definition restore_hdws ≝
    19   λglobals,l.
     19   λdestr_srcr.PSD (\fst destr_srcr) ← HDW (\snd destr_srcr) in
     20  map ?? save_hdws_internal.
     21
     22definition restore_hdws :
     23  ∀globals.list (psd_argument×Register) → list (joint_seq ERTL globals) ≝
     24  λglobals.
    2025   let restore_hdws_internal ≝
    21     λsrcr_destr: register × Register.
    22     λstart_lbl: label.
    23      let 〈srcr, destr〉 ≝ srcr_destr in
    24      adds_graph ertl_params1 globals [ sequential ertl_params_ … (MOVE … 〈hardware destr, pseudo srcr〉) ] start_lbl
    25    in
    26     map ? ? restore_hdws_internal l.
    27 
    28 definition get_params_hdw ≝
    29   λglobals.
    30   λparams: list register.
    31   match params with
    32   [ nil ⇒ [λstart_lbl: label. adds_graph ertl_params1 globals [ GOTO … ] start_lbl]
    33   | _ ⇒
    34     let l ≝ zip_pottier ? ? params RegisterParams in
    35       save_hdws globals l ].
    36 
    37 definition get_param_stack ≝
    38   λglobals.
    39   λoff: nat.
    40   λdestr.
    41   λstart_lbl, dest_lbl: label.
    42   λdef.
    43   let 〈def, addr1〉 ≝ fresh_reg … def in
    44   let 〈def, addr2〉 ≝ fresh_reg … def in
    45   let 〈def, tmpr〉 ≝ fresh_reg … def in
    46   let 〈carry, int_offset〉 ≝ half_add ? (bitvector_of_nat ? off) int_size in
    47   adds_graph ertl_params1 globals [
    48     sequential ertl_params_ … (extension … (ertl_st_ext_frame_size addr1));
    49     sequential ertl_params_ … (INT … tmpr int_offset);
    50     sequential ertl_params_ … (OP2 … Sub addr1 addr1 tmpr);
    51     sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPL〉);
    52     sequential ertl_params_ … (OP2 … Add addr1 addr1 tmpr);
    53     sequential ertl_params_ … (INT … addr2 (bitvector_of_nat 8 0));
    54     sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPH〉);
    55     sequential ertl_params_ … (OP2 … Addc addr2 addr2 tmpr);
    56     sequential ertl_params_ … (LOAD … destr addr1 addr2)
    57   ] start_lbl dest_lbl def.
    58  
    59 definition get_params_stack ≝
    60   λglobals,params.
    61   match params with
    62   [ nil ⇒ [ λstart_lbl. adds_graph … [GOTO …] start_lbl ]
    63   | _ ⇒ mapi ? ? (get_param_stack globals) params ].
     26    λdestr_srcr:psd_argument×?.HDW (\snd destr_srcr) ← \fst destr_srcr in
     27    map ? ? restore_hdws_internal.
     28
     29definition get_params_hdw :
     30  ∀globals.list register → list (joint_seq ERTL globals) ≝
     31  λglobals,params.
     32  save_hdws … (zip_pottier … params RegisterParams).
     33
     34definition get_param_stack :
     35  ∀globals.register → register → register →
     36  list (joint_seq ERTL globals) ≝
     37  λglobals,addr1,addr2,destr.
     38  (* liveness analysis will erase the last useless ops *)
     39  [ LOAD ?? destr addr1 addr2 ;
     40    addr1 ← addr1 .Add. (int_size : Byte) ;
     41    addr2 ← addr2 .Addc. zero_byte
     42  ].
     43
     44definition get_params_stack :
     45  ∀globals.list register →
     46  bind_new (localsT ERTL) (list (joint_seq ERTL globals)) ≝
     47  λglobals,params.
     48  νtmpr,addr1,addr2 in
     49  let params_length_byte : Byte ≝ bitvector_of_nat ? (|params|) in
     50  [ (ertl_frame_size tmpr : joint_seq ??) ;
     51    CLEAR_CARRY ?? ;
     52    tmpr ← tmpr .Sub. params_length_byte ; (* will be constant later *)
     53    PSD addr1 ← HDW RegisterSPL ;
     54    PSD addr2 ← HDW RegisterSPH ;
     55    addr1 ← addr1 .Add. tmpr ;
     56    addr2 ← addr2 .Addc. zero_byte ] @   
     57  flatten … (map ?? (get_param_stack globals addr1 addr2) params).
    6458
    6559definition get_params ≝
     
    6761  let n ≝ min (length … params) (length … RegisterParams) in
    6862  let 〈hdw_params, stack_params〉 ≝ list_split … n params in
    69   let hdw_params ≝ get_params_hdw globals hdw_params in
    70     hdw_params @ (get_params_stack … stack_params).
    71 
    72 definition add_prologue ≝
    73   λglobals.
    74   λparams: list register.
    75   λsral.
    76   λsrah.
    77   λsregs.
    78   λdef.
    79   let start_lbl ≝ joint_if_entry … (ertl_params globals) def in
    80   let 〈tmp_lbl, def〉 ≝ fresh_label … def in
    81   match lookup … (joint_if_code … def) start_lbl
    82     return λx. x ≠ None ? → ertl_internal_function globals with
    83   [ None ⇒ λnone_absrd. ⊥
    84   | Some last_stmt ⇒ λsome_prf.
    85     let def ≝
    86       add_translates …
    87          ((adds_graph ertl_params1 … [
    88                      sequential ertl_params_ … (extension ertl_params__ globals ertl_st_ext_new_frame)
    89                    ]) ::
    90          (adds_graph ertl_params1 … [
    91                       sequential ertl_params_ … (POP … sral);
    92                       sequential ertl_params_ … (POP … srah)
    93                    ]) ::
    94          (save_hdws … sregs) @
    95          (get_params … params))
    96         start_lbl tmp_lbl def
    97     in
    98       add_graph … tmp_lbl last_stmt def
    99   ] ?.
    100 [ cases start_lbl #x #H cases daemon (* @H *) (*CSC: XXXX, no Russell *)
    101 | cases (none_absrd) /2/ ]
    102 qed.
    103 
    104 definition save_return ≝
    105   λglobals.
    106   λret_regs.
    107   λstart_lbl: label.
    108   λdest_lbl: label.
    109   λdef: ertl_internal_function globals.
    110   let 〈def, tmpr〉 ≝ fresh_reg … def in
     63  get_params_hdw globals hdw_params @@ get_params_stack … stack_params.
     64
     65definition prologue :
     66  ∀globals.list register → register → register → list (register×Register) →
     67  bind_new (localsT ERTL) (list (joint_seq ERTL globals)) ≝
     68  λglobals,params,sral,srah,sregs.
     69  [ (ertl_new_frame : joint_seq ??) ;
     70    POP … sral ;
     71    POP … srah
     72  ] @@ save_hdws … sregs @@ get_params … params.
     73
     74definition save_return :
     75  ∀globals.list psd_argument → list (joint_seq ERTL globals) ≝
     76  λglobals,ret_regs.
    11177  match reduce_strong ? ? RegisterSTS ret_regs with
    11278  [ mk_Sig crl crl_proof ⇒
     
    11480    let commonr ≝ \fst (\snd crl) in
    11581    let restl ≝ \snd (\fst crl) in
    116     let restr ≝ \snd (\snd crl) in
    117     let init_tmpr ≝ sequential ertl_params_ … (INT … tmpr (zero …)) in
    118     let f_save ≝ λst. λr. sequential ertl_params_ … (MOVE … 〈hardware st, pseudo r〉) in
    119     let saves ≝ map2 … f_save commonl commonr crl_proof in
    120     let f_default ≝ λst. sequential ertl_params_ … (MOVE … 〈hardware st, pseudo tmpr〉) in
    121     let defaults ≝ map … f_default restl in
    122       adds_graph ertl_params1 ? (init_tmpr :: saves @ defaults) start_lbl dest_lbl def
    123   ].
    124 
    125 definition assign_result ≝
    126   λglobals.λstart_lbl: label.
    127   match reduce_strong ? ? RegisterRets RegisterSTS with
     82    (* let restr ≝ \snd (\snd crl) in *)
     83    map2 … (λst.λr : psd_argument.HDW st ← r) commonl commonr crl_proof @
     84    map … (λst.HDW st ← zero_byte) restl
     85  ].
     86
     87definition assign_result : ∀globals.list (joint_seq ERTL globals) ≝
     88  λglobals.
     89  match reduce_strong ?? RegisterRets RegisterSTS with
    12890  [ mk_Sig crl crl_proof ⇒
    12991    let commonl ≝ \fst (\fst crl) in
    13092    let commonr ≝ \fst (\snd crl) in
    131     let f ≝ λret. λst. sequential ertl_params_ globals (MOVE … 〈hardware ret, hardware st〉) in
    132     let insts ≝ map2 ? ? ? f commonl commonr crl_proof in
    133       adds_graph ertl_params1 … insts start_lbl
    134   ].
    135 
    136 definition add_epilogue ≝
    137   λglobals.
    138   λret_regs.
    139   λsral.
    140   λsrah.
    141   λsregs.
    142   λdef.
    143   let start_lbl ≝ joint_if_exit … (ertl_params globals) def in
    144   let 〈tmp_lbl, def〉 ≝ fresh_label … def in
    145   match lookup … (joint_if_code … def) start_lbl
    146     return λx. x ≠ None ? → ertl_internal_function globals with
    147   [ None ⇒ λnone_absrd. ⊥
    148   | Some last_stmt ⇒ λsome_prf.
    149     let def ≝
    150       add_translates ertl_params1 … (
    151         [save_return globals ret_regs] @
    152         restore_hdws … sregs @
    153         [adds_graph ertl_params1 … [
    154           sequential ertl_params_ … (PUSH … srah);
    155           sequential ertl_params_ … (PUSH … sral)
    156         ]] @
    157         [adds_graph ertl_params1 … [
    158           sequential ertl_params_ … (extension … ertl_st_ext_del_frame)
    159         ]] @
    160         [assign_result globals]
    161       ) start_lbl tmp_lbl def
    162     in
    163     let def' ≝ add_graph … tmp_lbl last_stmt def in
    164       set_joint_if_exit … tmp_lbl def' ?
    165   ] ?.
    166 [ cases start_lbl #x #H cases daemon (* @H *) (* CSC: XXXX *)
    167 | cases (none_absrd) /2/
    168 | cases daemon (* CSC: XXXXX *)
    169 ]
    170 qed.
    171  
    172 
    173 definition allocate_regs ≝
    174   λglobals.
    175   λrs.
    176   λsaved: rs_set rs.
    177   λdef.
     93    map2 … (λret,st.HDW ret ← HDW st) commonl commonr crl_proof
     94  ].
     95
     96definition epilogue :
     97  ∀globals.list register → register → register → list (register × Register) →
     98  list (joint_seq ERTL globals) ≝
     99  λglobals,ret_regs,sral,srah,sregs.
     100  save_return … (map … (Reg ?) ret_regs) @
     101  restore_hdws … (map … (λpr.〈Reg ? (\fst pr),\snd pr〉) sregs) @
     102  [ PUSH ERTL ? srah ;
     103    PUSH … sral ;
     104    ertl_del_frame ] @
     105  assign_result globals.
     106
     107definition allocate_regs :
     108  ∀globals,rs.rs_set rs →
     109  freshT ERTL globals (list (register×Register)) ≝
     110  λglobals,rs,saved,def.
    178111   let allocate_regs_internal ≝
    179112    λr: Register.
    180113    λdef_sregs.
    181     let 〈def, sregs〉 ≝ def_sregs in
    182     let 〈def, r'〉 ≝ fresh_reg ertl_params0 globals def in
    183       〈def, 〈r', r〉 :: sregs〉
    184    in
    185     rs_fold ? ? allocate_regs_internal saved 〈def, [ ]〉.
    186    
    187 definition add_pro_and_epilogue ≝
    188   λglobals.
    189   λparams.
    190   λret_regs.
    191   λdef.
    192   match fresh_regs_strong … globals def 2 with
    193   [ mk_Sig def_sra def_sra_proof ⇒
    194     let def ≝ \fst def_sra in
    195     let sra ≝ \snd def_sra in
    196     let sral ≝ nth_safe ? 0 sra ? in
    197     let srah ≝ nth_safe ? 1 sra ? in
    198     let 〈def, sregs〉 ≝ allocate_regs … register_list_set RegisterCalleeSaved def in
    199     let def ≝ add_prologue … params sral srah sregs def in
    200     let def ≝ add_epilogue … ret_regs sral srah sregs def in
    201       def
    202   ].
    203 >def_sra_proof //
    204 qed.
    205 
    206 definition set_params_hdw ≝
    207   λglobals,params.
    208   match params with
    209   [ nil ⇒ [ λstart_lbl. adds_graph … [GOTO …] start_lbl]
    210   | _ ⇒
    211     let l ≝ zip_pottier ? ? params RegisterParams in
    212       restore_hdws globals l
    213   ].
    214 
    215 definition set_param_stack ≝
    216   λglobals.
    217   λoff.
    218   λsrcr.
    219   λstart_lbl: label.
    220   λdest_lbl: label.
    221   λdef: ertl_internal_function globals.
    222   let 〈def, addr1〉 ≝ fresh_reg … def in
    223   let 〈def, addr2〉 ≝ fresh_reg … def in
    224   let 〈def, tmpr〉 ≝ fresh_reg … def in
    225   let 〈ignore, int_off〉 ≝ half_add ? off int_size in
    226     adds_graph ertl_params1 … [
    227       sequential ertl_params_ … (INT … addr1 int_off);
    228       sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPL〉);
    229       sequential ertl_params_ … (CLEAR_CARRY …);
    230       sequential ertl_params_ … (OP2 … Sub addr1 tmpr addr1);
    231       sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPH〉);
    232       sequential ertl_params_ … (INT … addr2 (zero ?));
    233       sequential ertl_params_ … (OP2 … Sub addr2 tmpr addr2);
    234       sequential ertl_params_ … (STORE … addr1 addr2 srcr)
    235     ] start_lbl dest_lbl def.   
    236 
    237 definition set_params_stack ≝
    238   λglobals,params.
    239   match params with
    240   [ nil ⇒ [ λstart_lbl. adds_graph ertl_params1 globals [GOTO …] start_lbl]
    241   | _ ⇒
    242     let f ≝ λi. λr. set_param_stack … (bitvector_of_nat ? i) r in
    243       mapi ? ? f params].
     114    let 〈def, r'〉 ≝ ertl_fresh_reg … (\fst def_sregs) in
     115    〈def, 〈r', r〉::\snd def_sregs〉 in
     116  rs_fold ?? allocate_regs_internal saved 〈def, [ ]〉.
     117
     118definition add_pro_and_epilogue :
     119  ∀globals.list register → list register →
     120  joint_internal_function ERTL globals →
     121  joint_internal_function ERTL globals ≝
     122  λglobals,params,ret_regs,def.
     123  let start_lbl ≝ joint_if_entry … def in
     124  let end_lbl ≝ joint_if_exit … def in
     125  state_run … def (
     126    ! sral ← ertl_fresh_reg … ;
     127    ! srah ← ertl_fresh_reg … ;
     128    ! sregs ← allocate_regs … register_list_set RegisterCalleeSaved ;
     129    ! prologue' ← bcompile … (ertl_fresh_reg …) (prologue … params sral srah sregs) ;
     130    let epilogue' ≝ epilogue … ret_regs sral srah sregs in
     131    ! def' ← state_get … ;
     132    let def'' ≝ insert_prologue … prologue' def' in
     133    return insert_epilogue … epilogue' def''
     134  ).
     135
     136definition set_params_hdw :
     137  ∀globals.list psd_argument → list (joint_seq ERTL globals) ≝
     138  λglobals,params.
     139  restore_hdws globals (zip_pottier ? ? params RegisterParams).
     140
     141(* Paolo: The following can probably be done way more efficiently with INC DPTR *)
     142
     143definition set_param_stack :
     144  ∀globals.register → register → psd_argument →
     145  list (joint_seq ERTL globals) ≝
     146  λglobals,addr1,addr2,arg.
     147  [ STORE … addr1 addr2 arg ;
     148    addr1 ← addr1 .Add. (int_size : Byte) ;
     149    addr2 ← addr2 .Addc. zero_byte
     150  ].
     151
     152definition set_params_stack :
     153  ∀globals.list psd_argument → bind_new (localsT ERTL) ? ≝
     154  λglobals,params.
     155  νaddr1,addr2 in
     156  let params_length_byte : Byte ≝ bitvector_of_nat ? (|params|) in
     157  [ PSD addr1 ← HDW RegisterSPL ;
     158    PSD addr2 ← HDW RegisterSPH ;
     159    CLEAR_CARRY ?? ;
     160    addr1 ← addr1 .Sub. params_length_byte ;
     161    addr2 ← addr2 .Sub. zero_byte
     162  ] @
     163  flatten … (map … (set_param_stack globals addr1 addr2) params).
    244164
    245165definition set_params ≝
     
    249169  let hdw_params ≝ \fst hdw_stack_params in
    250170  let stack_params ≝ \snd hdw_stack_params in
    251     set_params_hdw globals hdw_params @ set_params_stack globals stack_params.
    252 
    253 definition fetch_result ≝
    254   λglobals.
    255   λret_regs.
    256   λstart_lbl: label.
    257   match reduce_strong ? ? RegisterSTS RegisterRets with
    258   [ mk_Sig crl first_crl_proof ⇒
     171  set_params_hdw globals hdw_params @@ set_params_stack globals stack_params.
     172
     173definition fetch_result :
     174  ∀globals.list register → list (joint_seq ERTL globals) ≝
     175  λglobals,ret_regs.
     176  match reduce_strong ?? RegisterSTS RegisterRets with
     177  [ mk_Sig crl crl_proof ⇒
    259178    let commonl ≝ \fst (\fst crl) in
    260179    let commonr ≝ \fst (\snd crl) in
    261     let f_save ≝ λst. λret. sequential ertl_params_ globals (MOVE … 〈hardware st, hardware ret〉) in
    262     let saves ≝ map2 ? ? ? f_save commonl commonr ? in
    263     match reduce_strong ? ? ret_regs RegisterSTS with
    264     [ mk_Sig crl second_crl_proof ⇒
     180    map2 … (λst,r.HDW st ← HDW r) commonl commonr crl_proof @
     181    match reduce_strong ?? ret_regs RegisterSTS with
     182    [ mk_Sig crl crl_proof ⇒
    265183      let commonl ≝ \fst (\fst crl) in
    266184      let commonr ≝ \fst (\snd crl) in
    267       let f_restore ≝ λr. λst. sequential ertl_params_ … (MOVE … 〈pseudo r, hardware st〉) in
    268       let restores ≝ map2 ? ? ? f_restore commonl commonr ? in
    269         adds_graph ertl_params1 … (saves @ restores) start_lbl]].
    270 [@second_crl_proof | @first_crl_proof]
    271 qed.
    272 
    273 definition translate_call_id ≝
    274   λglobals,f.
    275   λargs.
    276   λret_regs.
    277   λstart_lbl.
    278   λdest_lbl.
    279   λdef.
    280   let nb_args ≝ |args| in
    281     add_translates ertl_params1 globals (
    282       set_params … args @ [
    283       adds_graph ertl_params1 … [ sequential ertl_params_ … (CALL_ID … f nb_args it) ];
    284       fetch_result … ret_regs
     185      map2 … (λret,st.PSD ret ← HDW st) commonl commonr crl_proof
     186    ]
     187  ].
     188
     189definition translate_step :
     190  ∀globals.label → joint_step RTL_ntc globals →
     191    bind_seq_block ERTL globals (joint_step ERTL globals) ≝
     192  λglobals.λ_.λs.
     193  match s return λ_.bind_seq_block ?? (joint_step ??) with
     194  [ step_seq s ⇒
     195    match s return λ_.bind_seq_block ?? (joint_step ??) with
     196    [ PUSH _ ⇒ NOOP … (*CSC: XXXX should not be in the syntax *)
     197    | POP _ ⇒ NOOP …  (*CSC: XXXX should not be in the syntax *)
     198    | MOVE rs ⇒ PSD (\fst rs) ← \snd rs
     199    | COST_LABEL lbl ⇒
     200      COST_LABEL … lbl
     201    | ADDRESS x prf r1 r2 ⇒
     202      ADDRESS ERTL ? x prf r1 r2
     203    | OPACCS op destr1 destr2 srcr1 srcr2 ⇒
     204      OPACCS ERTL ? op destr1 destr2 srcr1 srcr2 
     205    | OP1 op1 destr srcr ⇒
     206      OP1 ERTL ? op1 destr srcr
     207    | OP2 op2 destr srcr1 srcr2 ⇒
     208      OP2 ERTL ? op2 destr srcr1 srcr2
     209    | CLEAR_CARRY ⇒
     210      CLEAR_CARRY …
     211    | SET_CARRY ⇒
     212      SET_CARRY …
     213    | LOAD destr addr1 addr2 ⇒
     214      LOAD ERTL ? destr addr1 addr2
     215    | STORE addr1 addr2 srcr ⇒
     216      STORE ERTL ? addr1 addr2 srcr
     217    | COMMENT msg ⇒
     218      COMMENT … msg
     219    | extension_seq ext ⇒
     220      match ext with
     221      [ rtl_stack_address addr1 addr2 ⇒
     222        [ PSD addr1 ← HDW RegisterSPL ; PSD addr2 ← HDW RegisterSPH ]
    285223      ]
    286     ) start_lbl dest_lbl def.
    287 
    288 definition translate_stmt :
    289  ∀globals: list ident. label → rtlntc_statement globals → ertl_internal_function globals → ertl_internal_function globals
    290  ≝
    291   λglobals.
    292   λlbl.
    293   λstmt.
    294   λdef.
    295   match stmt with
    296   [ GOTO lbl' ⇒ add_graph … lbl (GOTO … lbl') def
    297   | RETURN ⇒ add_graph … lbl (RETURN …) def
    298   | sequential seq lbl' ⇒
    299      match seq with
    300       [ PUSH _ ⇒ ⊥ (*CSC: XXXX should not be in the syntax *)
    301       | POP _  ⇒ ⊥ (*CSC: XXXX should not be in the syntax *)
    302       | CALL_ID f args ret_regs ⇒
    303          translate_call_id … f args ret_regs lbl lbl' def
    304       | MOVE rs ⇒
    305          let 〈r1,r2〉 ≝ rs in
    306          let rs ≝ 〈pseudo r1, pseudo r2〉 in
    307           add_graph ertl_params1 ? lbl (sequential … (MOVE … rs) lbl') def
    308       | extension ext ⇒
    309          match ext with
    310           [ rtlntc_st_ext_call_ptr _ _ _ _ ⇒ ⊥ (*CSC: XXXX not implemented in OCaml too *)
    311           | rtlntc_st_ext_stack_address r1 r2 ⇒
    312              adds_graph ertl_params1 … [
    313               sequential ertl_params_ … (MOVE … 〈pseudo r1, hardware RegisterSPL〉);
    314               sequential ertl_params_ … (MOVE … 〈pseudo r2, hardware RegisterSPH〉)
    315              ] lbl lbl' def]
    316       (*CSC: everything is just copied to re-type it from now on;
    317         the problem is call_id that takes different parameters, but that is pattern-matched
    318         above. It could be made nicer at the cost of making all the rest of the code uglier *)
    319       | COST_LABEL cost_lbl ⇒ add_graph ertl_params1 … lbl (sequential … (COST_LABEL … cost_lbl) lbl') def
    320       | ADDRESS x prf r1 r2 ⇒ add_graph ertl_params1 … lbl (sequential … (ADDRESS … x prf r1 r2) lbl') def
    321       | INT r i ⇒  add_graph ertl_params1 … lbl (sequential … (INT … r i) lbl') def
    322       | OPACCS op destr1 destr2 srcr1 srcr2 ⇒
    323           add_graph ertl_params1 … lbl (sequential … (OPACCS … op destr1 destr2 srcr1 srcr2) lbl') def
    324       | OP1 op1 destr srcr ⇒
    325         add_graph ertl_params1 … lbl (sequential … (OP1 … op1 destr srcr) lbl') def
    326       | OP2 op2 destr srcr1 srcr2 ⇒
    327         add_graph ertl_params1 … lbl (sequential … (OP2 … op2 destr srcr1 srcr2) lbl') def
    328       | CLEAR_CARRY ⇒
    329         add_graph ertl_params1 … lbl (sequential … (CLEAR_CARRY …) lbl') def
    330       | SET_CARRY ⇒
    331         add_graph ertl_params1 … lbl (sequential … (SET_CARRY …) lbl') def
    332       | LOAD destr addr1 addr2 ⇒
    333         add_graph ertl_params1 … lbl (sequential … (LOAD … destr addr1 addr2) lbl') def
    334       | STORE addr1 addr2 srcr ⇒
    335         add_graph ertl_params1 … lbl (sequential … (STORE … addr1 addr2 srcr) lbl') def
    336       | COND srcr lbl_true ⇒
    337         add_graph ertl_params1 … lbl (sequential … (COND … srcr lbl_true) lbl') def
    338       | COMMENT msg ⇒
    339         add_graph ertl_params1 … lbl (sequential … (COMMENT … msg) lbl') def
    340       ]].
    341   @not_implemented (*CSC: XXXX spurious things in the syntax and ptr_calls *)
    342 qed.
     224    | CALL_ID f args ret_regs ⇒
     225      set_params ? args @@
     226      CALL_ID ERTL ? f (|args|) it :::
     227      fetch_result ? ret_regs
     228    | extension_call c ⇒
     229      match c with
     230      [ rtl_call_ptr f1 f2 args dest ⇒
     231        ?
     232      ]
     233    ]
     234  | COND r ltrue ⇒
     235    COND ERTL ? r ltrue
     236  ]. cases daemon (* pointer call to be ported yet *) qed.
     237
     238definition translate_fin_step :
     239  ∀globals.label → joint_fin_step RTL_ntc →
     240    bind_seq_block ERTL globals (joint_fin_step ERTL) ≝
     241  λglobals.λ_.λs.
     242  match s with
     243  [ GOTO lbl' ⇒ GOTO … lbl'
     244  | RETURN ⇒ RETURN ?
     245  | tailcall abs ⇒ match abs in void with [ ]
     246  ].
    343247
    344248(* hack with empty graphs used here *)
    345 definition translate_funct_internal ≝
    346   λglobals.λdef:rtlntc_internal_function globals.
     249definition translate_funct :
     250  ∀globals.joint_internal_function RTL_ntc globals →
     251    joint_internal_function ERTL globals ≝
     252  λglobals,def.
    347253  let nb_params ≝ |joint_if_params ?? def| in
    348254  let added_stacksize ≝ max 0 (minus nb_params (|RegisterParams|)) in
    349255  let new_locals ≝ nub_by ? (eq_identifier ?) ((joint_if_locals … def) @ (joint_if_params … def)) in
    350   let entry' ≝ joint_if_entry … def in
    351   let exit' ≝ joint_if_exit … def in
    352   let graph' ≝ add ? ? (empty_map ? ?) entry' (GOTO … entry') in
    353   let graph' ≝ add ? ? graph' exit' (GOTO … exit') in
    354   let def' ≝
    355     mk_joint_internal_function globals (ertl_params globals)
    356       (joint_if_luniverse … def) (joint_if_runiverse … def) (joint_if_result … def) (*CSC: different from OCaml code where joint_if_result is unit*)
     256  let entry' ≝ pi1 … (joint_if_entry … def) in
     257  let exit' ≝ pi1 … (joint_if_exit … def) in
     258  let def' ≝ init_graph_if ERTL globals
     259      (joint_if_luniverse … def) (joint_if_runiverse … def) it (*Paolo: to be checked, unit or list register? *)
    357260      nb_params new_locals ((joint_if_stacksize … def) + added_stacksize)
    358       graph' ? ? in
    359   let def' ≝ foldi ? ? ? (translate_stmt globals) (joint_if_code … def) def' in
    360    add_pro_and_epilogue ? (joint_if_params ?? def) (joint_if_result ?? def) def'.
    361 whd in match ertl_params; (* CSC: Matita's bug here; not enough/too much reduction
    362                                  makes the next application fail. Why? *)   
    363 %
    364  [ @entry' | @graph_add_lookup @graph_add
    365  | @exit'  | @graph_add ]
    366 qed.
    367 
     261      entry' exit' in
     262  let def'' ≝ b_graph_translate …
     263    (ertl_fresh_reg …)
     264    def'
     265    (translate_step globals)
     266    (translate_fin_step globals)
     267    def in
     268  add_pro_and_epilogue ? (joint_if_params ?? def) (joint_if_result ?? def) def'.
     269
     270(* removing this because of how insert_prologue is now defined
    368271definition generate ≝
    369272  λglobals.
    370273  λstmt.
    371   λdef: joint_internal_function … (ertl_params globals).
     274  λdef: joint_internal_function globals ERTL.
    372275  let 〈entry, def〉 ≝ fresh_label … def in
    373276  let graph ≝ add … (joint_if_code … def) entry stmt in
    374    set_joint_if_graph … (ertl_params globals) graph def ??.
     277   set_joint_if_graph … (ERTL globals) graph def ??.
    375278  [ (*% [ @entry | @graph_add ]*) cases daemon (*CSC: XXX *)
    376279  | (*cases (joint_if_exit … def) #LBL #LBL_PRF % [ @LBL | @graph_add_lookup @LBL_PRF
     
    392295         match inst with
    393296          [ COST_LABEL cost_lbl ⇒
    394              〈Some … cost_lbl, add_graph ertl_params1 globals lbl (GOTO … lbl) def〉
     297             〈Some … cost_lbl, add_graph ERTL1 globals lbl (GOTO … lbl) def〉
    395298          | _ ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ]
    396299      | RETURN ⇒ 〈None …, def〉
     
    407310  match cost_label with
    408311  [ None ⇒ def
    409   | Some cost_label ⇒ generate … (sequential ertl_params_ globals (COST_LABEL … cost_label) (joint_if_entry … def)) def
     312  | Some cost_label ⇒ generate … (sequential ERTL_ globals (COST_LABEL … cost_label) (joint_if_entry … def)) def
    410313  ].
    411314
    412315definition translate_funct ≝ λglobals,def. (move_first_cost_label_up_internal … (translate_funct_internal globals def)).
     316*)
    413317
    414318definition rtl_to_ertl : rtl_program → ertl_program ≝
Note: See TracChangeset for help on using the changeset viewer.