source: src/RTL/RTLToERTL.ma @ 1315

Last change on this file since 1315 was 1315, checked in by mulligan, 8 years ago

another move for the same reason. got rtlabs > rtl compiling again by using a daemon

File size: 16.0 KB
RevLine 
[1079]1include "RTL/RTLTailcall.ma".
[1075]2include "utilities/RegisterSet.ma".
[1076]3include "common/Identifiers.ma".
[759]4include "ERTL/ERTL.ma".
[1280]5include "joint/TranslateUtils.ma".
[1252]6
[763]7definition save_hdws ≝
[1254]8 λglobals,l.
9  let save_hdws_internal ≝
10   λdestr_srcr.λstart_lbl.
[777]11    let 〈destr, srcr〉 ≝ destr_srcr in
[1283]12     adds_graph ertl_params1 globals [ sequential ertl_params_ … (MOVE … 〈pseudo destr,hardware srcr〉) ] start_lbl
[1254]13  in
14   map ? ? save_hdws_internal l.
15
[777]16definition restore_hdws ≝
[1254]17  λglobals,l.
18   let restore_hdws_internal ≝
19    λsrcr_destr: register × Register.
20    λstart_lbl: label.
21     let 〈srcr, destr〉 ≝ srcr_destr in
[1283]22     adds_graph ertl_params1 globals [ sequential ertl_params_ … (MOVE … 〈hardware destr, pseudo srcr〉) ] start_lbl
[1254]23   in
24    map ? ? restore_hdws_internal l.
[777]25
26definition get_params_hdw ≝
[1254]27  λglobals.
[777]28  λparams: list register.
[1071]29  match params with
[1283]30  [ nil ⇒ [λstart_lbl: label. adds_graph ertl_params1 globals [ GOTO … ] start_lbl]
[777]31  | _ ⇒
[1149]32    let l ≝ zip_pottier ? ? params RegisterParams in
[1254]33      save_hdws globals l ].
[777]34
35definition get_param_stack ≝
[1254]36  λglobals.
[777]37  λoff: nat.
38  λdestr.
39  λstart_lbl, dest_lbl: label.
40  λdef.
[1254]41  let 〈def, addr1〉 ≝ fresh_reg … def in
42  let 〈def, addr2〉 ≝ fresh_reg … def in
43  let 〈def, tmpr〉 ≝ fresh_reg … def in
[1071]44  let 〈carry, int_offset〉 ≝ half_add ? (bitvector_of_nat ? off) int_size in
[1280]45  adds_graph ertl_params1 globals [
[1283]46    sequential ertl_params_ … (extension … (ertl_st_ext_frame_size addr1));
47    sequential ertl_params_ … (INT … tmpr int_offset);
48    sequential ertl_params_ … (OP2 … Sub addr1 addr1 tmpr);
49    sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPL〉);
50    sequential ertl_params_ … (OP2 … Add addr1 addr1 tmpr);
51    sequential ertl_params_ … (INT … addr2 (bitvector_of_nat 8 0));
52    sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPH〉);
53    sequential ertl_params_ … (OP2 … Addc addr2 addr2 tmpr);
[1284]54    sequential ertl_params_ … (LOAD … destr addr1 addr2)
[777]55  ] start_lbl dest_lbl def.
56 
57definition get_params_stack ≝
[1257]58  λglobals,params.
[1071]59  match params with
[1283]60  [ nil ⇒ [ λstart_lbl. adds_graph … [GOTO …] start_lbl ]
[1257]61  | _ ⇒ mapi ? ? (get_param_stack globals) params ].
[777]62
63definition get_params ≝
[1257]64  λglobals,params.
65  let n ≝ min (length … params) (length … RegisterParams) in
66  let 〈hdw_params, stack_params〉 ≝ list_split … n params in
67  let hdw_params ≝ get_params_hdw globals hdw_params in
68    hdw_params @ (get_params_stack … stack_params).
[1284]69
[777]70definition add_prologue ≝
[1257]71  λglobals.
[1071]72  λparams: list register.
[777]73  λsral.
74  λsrah.
75  λsregs.
76  λdef.
[1258]77  let start_lbl ≝ joint_if_entry … (ertl_params globals) def in
[1284]78  let 〈tmp_lbl, def〉 ≝ fresh_label … def in
[1280]79  match lookup … (joint_if_code … def) start_lbl
[1257]80    return λx. x ≠ None ? → ertl_internal_function globals with
81  [ None ⇒ λnone_absrd. ⊥
[1075]82  | Some last_stmt ⇒ λsome_prf.
[777]83    let def ≝
[1257]84      add_translates …
[1280]85         ((adds_graph ertl_params1 … [
[1283]86                     sequential ertl_params_ … (extension ertl_params__ globals ertl_st_ext_new_frame)
[1071]87                   ]) ::
[1283]88         (adds_graph ertl_params1 … [
89                      sequential ertl_params_ … (POP … sral);
90                      sequential ertl_params_ … (POP … srah)
[1071]91                   ]) ::
[1257]92         (save_hdws … sregs) @
93         (get_params … params))
[1071]94        start_lbl tmp_lbl def
95    in
[1257]96      add_graph … tmp_lbl last_stmt def
[1075]97  ] ?.
[1284]98[ cases start_lbl #x #H cases daemon (* @H *) (*CSC: XXXX, no Russell *)
[1257]99| cases (none_absrd) /2/ ]
[1071]100qed.
101
102definition save_return ≝
[1258]103  λglobals.
[1071]104  λret_regs.
105  λstart_lbl: label.
106  λdest_lbl: label.
[1258]107  λdef: ertl_internal_function globals.
108  let 〈def, tmpr〉 ≝ fresh_reg … def in
[1075]109  match reduce_strong ? ? RegisterSTS ret_regs with
[1071]110  [ dp crl crl_proof ⇒
111    let commonl ≝ \fst (\fst crl) in
112    let commonr ≝ \fst (\snd crl) in
113    let restl ≝ \snd (\fst crl) in
114    let restr ≝ \snd (\snd crl) in
[1283]115    let init_tmpr ≝ sequential ertl_params_ … (INT … tmpr (zero …)) in
116    let f_save ≝ λst. λr. sequential ertl_params_ … (MOVE … 〈hardware st, pseudo r〉) in
[1280]117    let saves ≝ map2 … f_save commonl commonr crl_proof in
[1283]118    let f_default ≝ λst. sequential ertl_params_ … (MOVE … 〈hardware st, pseudo tmpr〉) in
[1280]119    let defaults ≝ map … f_default restl in
120      adds_graph ertl_params1 … (init_tmpr :: saves @ defaults) start_lbl dest_lbl def
[1071]121  ].
122
[1075]123definition assign_result ≝
[1258]124  λglobals.λstart_lbl: label.
[1075]125  match reduce_strong ? ? RegisterRets RegisterSTS with
126  [ dp crl crl_proof ⇒
127    let commonl ≝ \fst (\fst crl) in
128    let commonr ≝ \fst (\snd crl) in
[1283]129    let f ≝ λret. λst. sequential ertl_params_ globals (MOVE … 〈hardware ret, hardware st〉) in
[1075]130    let insts ≝ map2 ? ? ? f commonl commonr crl_proof in
[1280]131      adds_graph ertl_params1 … insts start_lbl
[1075]132  ].
133
134definition add_epilogue ≝
[1258]135  λglobals.
[1075]136  λret_regs.
137  λsral.
138  λsrah.
139  λsregs.
140  λdef.
[1258]141  let start_lbl ≝ joint_if_exit … (ertl_params globals) def in
[1284]142  let 〈tmp_lbl, def〉 ≝ fresh_label … def in
[1280]143  match lookup … (joint_if_code … def) start_lbl
[1258]144    return λx. x ≠ None ? → ertl_internal_function globals with
145  [ None ⇒ λnone_absrd. ⊥
[1075]146  | Some last_stmt ⇒ λsome_prf.
147    let def ≝
[1280]148      add_translates ertl_params1 … (
[1258]149        [save_return globals ret_regs] @
150        restore_hdws … sregs @
[1283]151        [adds_graph ertl_params1 … [
152          sequential ertl_params_ … (PUSH … srah);
153          sequential ertl_params_ … (PUSH … sral)
[1075]154        ]] @
[1280]155        [adds_graph ertl_params1 … [
[1283]156          sequential ertl_params_ … (extension … ertl_st_ext_del_frame)
[1075]157        ]] @
[1258]158        [assign_result globals]
[1075]159      ) start_lbl tmp_lbl def
160    in
[1258]161    let def' ≝ add_graph … tmp_lbl last_stmt def in
162      set_joint_if_exit … tmp_lbl def' ?
[1075]163  ] ?.
[1284]164[ cases start_lbl #x #H cases daemon (* @H *) (* CSC: XXXX *)
[1258]165| cases (none_absrd) /2/
166| cases daemon (* CSC: XXXXX *)
167]
[1075]168qed.
[777]169 
[1258]170
[777]171definition allocate_regs ≝
[1258]172  λglobals.
[1075]173  λrs.
[777]174  λsaved: rs_set rs.
175  λdef.
[1258]176   let allocate_regs_internal ≝
177    λr: Register.
178    λdef_sregs.
179    let 〈def, sregs〉 ≝ def_sregs in
[1280]180    let 〈def, r'〉 ≝ fresh_reg ertl_params0 globals def in
[1258]181      〈def, 〈r', r〉 :: sregs〉
182   in
[777]183    rs_fold ? ? allocate_regs_internal saved 〈def, [ ]〉.
[1075]184   
185definition add_pro_and_epilogue ≝
[1258]186  λglobals.
[1075]187  λparams.
188  λret_regs.
189  λdef.
[1280]190  match fresh_regs_strong … globals def 2 with
[1075]191  [ dp def_sra def_sra_proof ⇒
192    let def ≝ \fst def_sra in
193    let sra ≝ \snd def_sra in
194    let sral ≝ nth_safe ? 0 sra ? in
195    let srah ≝ nth_safe ? 1 sra ? in
[1258]196    let 〈def, sregs〉 ≝ allocate_regs … register_list_set RegisterCalleeSaved def in
197    let def ≝ add_prologue … params sral srah sregs def in
198    let def ≝ add_epilogue … ret_regs sral srah sregs def in
[1075]199      def
200  ].
[1258]201>def_sra_proof //
[1075]202qed.
203
204definition set_params_hdw ≝
[1258]205  λglobals,params.
[1075]206  match params with
[1283]207  [ nil ⇒ [ λstart_lbl. adds_graph … [GOTO …] start_lbl]
[1075]208  | _ ⇒
[1149]209    let l ≝ zip_pottier ? ? params RegisterParams in
[1258]210      restore_hdws globals l
[1075]211  ].
212
213definition set_param_stack ≝
[1259]214  λglobals.
[1075]215  λoff.
216  λsrcr.
217  λstart_lbl: label.
218  λdest_lbl: label.
[1259]219  λdef: ertl_internal_function globals.
220  let 〈def, addr1〉 ≝ fresh_reg … def in
221  let 〈def, addr2〉 ≝ fresh_reg … def in
222  let 〈def, tmpr〉 ≝ fresh_reg … def in
[1075]223  let 〈ignore, int_off〉 ≝ half_add ? off int_size in
[1280]224    adds_graph ertl_params1 … [
[1283]225      sequential ertl_params_ … (INT … addr1 int_off);
226      sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPL〉);
227      sequential ertl_params_ … (CLEAR_CARRY …);
228      sequential ertl_params_ … (OP2 … Sub addr1 tmpr addr1);
229      sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPH〉);
230      sequential ertl_params_ … (INT … addr2 (zero ?));
231      sequential ertl_params_ … (OP2 … Sub addr2 tmpr addr2);
232      sequential ertl_params_ … (STORE … addr1 addr2 srcr)
[1075]233    ] start_lbl dest_lbl def.   
234
235definition set_params_stack ≝
[1259]236  λglobals,params.
[1075]237  match params with
[1283]238  [ nil ⇒ [ λstart_lbl. adds_graph ertl_params1 globals [GOTO …] start_lbl]
[1075]239  | _ ⇒
[1259]240    let f ≝ λi. λr. set_param_stack … (bitvector_of_nat ? i) r in
241      mapi ? ? f params].
[1075]242
243definition set_params ≝
[1259]244  λglobals,params.
[1149]245  let n ≝ min (|params|) (|RegisterParams|) in
[1075]246  let hdw_stack_params ≝ split ? params n ? in
247  let hdw_params ≝ \fst hdw_stack_params in
248  let stack_params ≝ \snd hdw_stack_params in
[1259]249    set_params_hdw globals hdw_params @ set_params_stack globals stack_params.
250/2/
[1075]251qed.
252
253definition fetch_result ≝
[1259]254  λglobals.
[1075]255  λret_regs.
256  λstart_lbl: label.
257  match reduce_strong ? ? RegisterSTS RegisterRets with
258  [ dp crl first_crl_proof ⇒
259    let commonl ≝ \fst (\fst crl) in
260    let commonr ≝ \fst (\snd crl) in
[1283]261    let f_save ≝ λst. λret. sequential ertl_params_ globals (MOVE … 〈hardware st, hardware ret〉) in
[1075]262    let saves ≝ map2 ? ? ? f_save commonl commonr ? in
263    match reduce_strong ? ? ret_regs RegisterSTS with
264    [ dp crl second_crl_proof ⇒
265      let commonl ≝ \fst (\fst crl) in
266      let commonr ≝ \fst (\snd crl) in
[1283]267      let f_restore ≝ λr. λst. sequential ertl_params_ … (MOVE … 〈pseudo r, hardware st〉) in
[1075]268      let restores ≝ map2 ? ? ? f_restore commonl commonr ? in
[1280]269        adds_graph ertl_params1 … (saves @ restores) start_lbl]].
[1259]270[@second_crl_proof | @first_crl_proof]
[1075]271qed.
272
273definition translate_call_id ≝
[1259]274  λglobals,f.
[1075]275  λargs.
276  λret_regs.
277  λstart_lbl.
278  λdest_lbl.
279  λdef.
280  let nb_args ≝ |args| in
[1280]281    add_translates ertl_params1 globals (
[1259]282      set_params … args @ [
[1283]283      adds_graph ertl_params1 … [ sequential ertl_params_ … (CALL_ID … f nb_args it) ];
[1259]284      fetch_result … ret_regs
[1075]285      ]
286    ) start_lbl dest_lbl def.
287
[1275]288definition translate_stmt :
[1278]289 ∀globals: list ident. label → rtlntc_statement globals → ertl_internal_function globals → ertl_internal_function globals
[1262]290 ≝
[1259]291  λglobals.
[1075]292  λlbl.
293  λstmt.
294  λdef.
295  match stmt with
[1282]296  [ GOTO lbl' ⇒ add_graph … lbl (GOTO … lbl') def
297  | RETURN ⇒ add_graph … lbl (RETURN …) def
298  | sequential seq lbl' ⇒
[1275]299     match seq with
[1282]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 ⇒
[1275]303         translate_call_id … f args ret_regs lbl lbl' def
[1282]304      | MOVE rs ⇒
[1275]305         let 〈r1,r2〉 ≝ rs in
306         let rs ≝ 〈pseudo r1, pseudo r2〉 in
[1282]307          add_graph ertl_params1 ? lbl (sequential … (MOVE … rs) lbl') def
308      | extension ext ⇒
[1275]309         match ext with
[1278]310          [ rtlntc_st_ext_call_ptr _ _ _ _ ⇒ ⊥ (*CSC: XXXX not implemented in OCaml too *)
311          | rtlntc_st_ext_address r1 r2 ⇒
[1280]312             adds_graph ertl_params1 … [
[1283]313              sequential ertl_params_ … (MOVE … 〈pseudo r1, hardware RegisterSPL〉);
314              sequential ertl_params_ … (MOVE … 〈pseudo r2, hardware RegisterSPH〉)
[1278]315             ] lbl lbl' def]
[1275]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 *)
[1282]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
[1275]340      ]].
[1280]341  @not_implemented (*CSC: XXXX spurious things in the syntax and ptr_calls *)
[1275]342qed.
[1075]343
[1079]344(* hack with empty graphs used here *)
[1076]345definition translate_funct_internal ≝
[1278]346  λglobals.λdef:rtlntc_internal_function globals.
[1270]347  let nb_params ≝ |joint_if_params ?? def| in
[1149]348  let added_stacksize ≝ max 0 (nb_params - |RegisterParams|) in
[1270]349  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
[1282]352  let graph' ≝ add ? ? (empty_map ? ?) entry' (GOTO … entry') in
353  let graph' ≝ add ? ? graph' exit' (GOTO … exit') in
[1076]354  let def' ≝
[1262]355    mk_joint_internal_function globals (ertl_params globals)
[1270]356      (joint_if_luniverse … def) (joint_if_runiverse … def) it
357      nb_params new_locals ((joint_if_stacksize … def) + added_stacksize)
[1079]358      graph' ? ? in
[1270]359  let def' ≝ foldi ? ? ? (translate_stmt globals) (joint_if_code … def) def' in
[1275]360   add_pro_and_epilogue ? (joint_if_params ?? def) (joint_if_result ?? def) def'.
[1262]361whd 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 ]
[1079]366qed.
[1077]367
368definition generate ≝
[1262]369  λglobals.
[1077]370  λstmt.
[1280]371  λdef: joint_internal_function … (ertl_params globals).
[1284]372  let 〈entry, def〉 ≝ fresh_label … def in
373  let graph ≝ add … (joint_if_code … def) entry stmt in
374   set_joint_if_graph … (ertl_params globals) graph def ??.
375  [ (*% [ @entry | @graph_add ]*) cases daemon (*CSC: XXX *)
376  | (*cases (joint_if_exit … def) #LBL #LBL_PRF % [ @LBL | @graph_add_lookup @LBL_PRF
377    *) cases daemon (*CSC: XXX *)
378  ]
[1079]379qed.
[1262]380
381let rec find_and_remove_first_cost_label_internal (globals: list ident)
382  (def: ertl_internal_function globals) (lbl: label) (num_nodes: nat)
[1079]383    on num_nodes ≝
384  match num_nodes with
385  [ O ⇒ 〈None ?, def〉
386  | S num_nodes' ⇒
[1262]387    match lookup … (joint_if_code … def) lbl with
[1079]388    [ None ⇒ 〈None ?, def〉
[1262]389    | Some stmt ⇒
[1079]390      match stmt with
[1282]391      [ sequential inst lbl ⇒
[1262]392         match inst with
[1282]393          [ COST_LABEL cost_lbl ⇒
394             〈Some … cost_lbl, add_graph ertl_params1 globals lbl (GOTO … lbl) def〉
[1262]395          | _ ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ]
[1282]396      | RETURN ⇒ 〈None …, def〉
397      | GOTO lbl ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes'
[1262]398      ]]].
[1079]399   
400definition find_and_remove_first_cost_label ≝
[1262]401  λglobals,def. 
402    find_and_remove_first_cost_label_internal globals def (joint_if_entry … def) (graph_num_nodes ? (joint_if_code … def)).
[1077]403
[1079]404definition move_first_cost_label_up_internal ≝
[1262]405  λglobals,def.
406  let 〈cost_label, def〉 ≝ find_and_remove_first_cost_label … def in
[1079]407  match cost_label with
408  [ None ⇒ def
[1282]409  | Some cost_label ⇒ generate … (sequential ertl_params_ globals (COST_LABEL … cost_label) (joint_if_entry … def)) def
[1079]410  ].
[1077]411
[1262]412definition translate_funct ≝ λglobals,def. (move_first_cost_label_up_internal … (translate_funct_internal globals def)).
413
414definition translate : rtl_program → ertl_program ≝
415 λp.
416  let p ≝ tailcall_simplify p in (* tailcall simplification here *)
[1280]417    transform_program ??? p (transf_fundef ?? (translate_funct …)).
Note: See TracBrowser for help on using the repository browser.