source: src/RTL/RTLToERTL.ma @ 2659

Last change on this file since 2659 was 2659, checked in by sacerdot, 8 years ago

Tailcall elimination no longer necessary:

  1. the back-end is almost ready for tailcalls
  2. tailcalls are never generated by the frontend
File size: 11.4 KB
Line 
1include "utilities/RegisterSet.ma".
2include "common/Identifiers.ma".
3include "ERTL/ERTL.ma".
4include "joint/TranslateUtils.ma".
5
6include alias "basics/lists/list.ma".
7
8definition ertl_fresh_reg:
9 ∀globals.freshT ERTL globals register ≝
10  λglobals,def.
11    let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
12    〈set_locals ?? (set_runiverse ?? def runiverse)(r::joint_if_locals ?? def), r〉.
13
14definition save_hdws :
15  ∀globals.list (register×Register) → list (joint_seq ERTL globals) ≝
16 λglobals.
17  let save_hdws_internal ≝
18   λdestr_srcr.PSD (\fst destr_srcr) ← HDW (\snd destr_srcr) in
19  map ?? save_hdws_internal.
20
21definition restore_hdws :
22  ∀globals.list (psd_argument×Register) → list (joint_seq ERTL globals) ≝
23  λglobals.
24   let restore_hdws_internal ≝
25    λdestr_srcr:psd_argument×?.HDW (\snd destr_srcr) ← \fst destr_srcr in
26    map ? ? restore_hdws_internal.
27
28definition get_params_hdw :
29  ∀globals.list register → list (joint_seq ERTL globals) ≝
30  λglobals,params.
31  save_hdws … (zip_pottier … params RegisterParams).
32
33definition get_param_stack :
34  ∀globals.register → register → register →
35  list (joint_seq ERTL globals) ≝
36  λglobals,addr1,addr2,destr.
37  (* liveness analysis will erase the last useless ops *)
38  [ LOAD ?? destr addr1 addr2 ;
39    addr1 ← addr1 .Add. (int_size : Byte) ;
40    addr2 ← addr2 .Addc. zero_byte
41  ].
42
43definition get_params_stack :
44  ∀globals.list register →
45  bind_new (localsT ERTL) (list (joint_seq ERTL globals)) ≝
46  λglobals,params.
47  νtmpr,addr1,addr2 in
48  let params_length_byte : Byte ≝ bitvector_of_nat ? (|params|) in
49  [ (ertl_frame_size tmpr : joint_seq ??) ;
50    CLEAR_CARRY ?? ;
51    tmpr ← tmpr .Sub. params_length_byte ; (* will be constant later *)
52    PSD addr1 ← HDW RegisterSPL ;
53    PSD addr2 ← HDW RegisterSPH ;
54    addr1 ← addr1 .Add. tmpr ;
55    addr2 ← addr2 .Addc. zero_byte ] @   
56  flatten … (map ?? (get_param_stack globals addr1 addr2) params).
57
58definition get_params ≝
59  λglobals,params.
60  let n ≝ min (length … params) (length … RegisterParams) in
61  let 〈hdw_params, stack_params〉 ≝ list_split … n params in
62  get_params_hdw globals hdw_params @@ get_params_stack … stack_params.
63
64definition prologue :
65  ∀globals.list register → register → register → list (register×Register) →
66  bind_new (localsT ERTL) (list (joint_seq ERTL globals)) ≝
67  λglobals,params,sral,srah,sregs.
68  [ (ertl_new_frame : joint_seq ??) ;
69    POP … sral ;
70    POP … srah
71  ] @@ save_hdws … sregs @@ get_params … params.
72
73definition save_return :
74  ∀globals.list psd_argument → list (joint_seq ERTL globals) ≝
75  λglobals,ret_regs.
76  match reduce_strong ? ? RegisterSTS ret_regs with
77  [ mk_Sig crl crl_proof ⇒
78    let commonl ≝ \fst (\fst crl) in
79    let commonr ≝ \fst (\snd crl) in
80    let restl ≝ \snd (\fst crl) in
81    (* let restr ≝ \snd (\snd crl) in *)
82    map2 … (λst.λr : psd_argument.HDW st ← r) commonl commonr crl_proof @
83    map … (λst.HDW st ← zero_byte) restl
84  ].
85
86definition assign_result : ∀globals.list (joint_seq ERTL globals) ≝
87  λglobals.
88  match reduce_strong ?? RegisterRets RegisterSTS with
89  [ mk_Sig crl crl_proof ⇒
90    let commonl ≝ \fst (\fst crl) in
91    let commonr ≝ \fst (\snd crl) in
92    map2 … (λret,st.HDW ret ← HDW st) commonl commonr crl_proof
93  ].
94
95definition epilogue :
96  ∀globals.list register → register → register → list (register × Register) →
97  list (joint_seq ERTL globals) ≝
98  λglobals,ret_regs,sral,srah,sregs.
99  save_return … (map … (Reg ?) ret_regs) @
100  restore_hdws … (map … (λpr.〈Reg ? (\fst pr),\snd pr〉) sregs) @
101  [ PUSH ERTL ? srah ;
102    PUSH … sral ;
103    ertl_del_frame ] @
104  assign_result globals.
105
106definition allocate_regs :
107  ∀globals,rs.rs_set rs →
108  freshT ERTL globals (list (register×Register)) ≝
109  λglobals,rs,saved,def.
110   let allocate_regs_internal ≝
111    λr: Register.
112    λdef_sregs.
113    let 〈def, r'〉 ≝ ertl_fresh_reg … (\fst def_sregs) in
114    〈def, 〈r', r〉::\snd def_sregs〉 in
115  rs_fold ?? allocate_regs_internal saved 〈def, [ ]〉.
116
117definition add_pro_and_epilogue :
118  ∀globals.list register → list register →
119  joint_internal_function ERTL globals →
120  joint_internal_function ERTL globals ≝
121  λglobals,params,ret_regs,def.
122  let start_lbl ≝ joint_if_entry … def in
123  let end_lbl ≝ joint_if_exit … def in
124  state_run … def (
125    ! sral ← ertl_fresh_reg … ;
126    ! srah ← ertl_fresh_reg … ;
127    ! sregs ← allocate_regs … register_list_set RegisterCalleeSaved ;
128    ! prologue' ← bcompile … (ertl_fresh_reg …) (prologue … params sral srah sregs) ;
129    let epilogue' ≝ epilogue … ret_regs sral srah sregs in
130    ! def' ← state_get … ;
131    let def'' ≝ insert_prologue … prologue' def' in
132    return insert_epilogue … epilogue' def''
133  ).
134
135definition set_params_hdw :
136  ∀globals.list psd_argument → list (joint_seq ERTL globals) ≝
137  λglobals,params.
138  restore_hdws globals (zip_pottier ? ? params RegisterParams).
139
140(* Paolo: The following can probably be done way more efficiently with INC DPTR *)
141
142definition set_param_stack :
143  ∀globals.register → register → psd_argument →
144  list (joint_seq ERTL globals) ≝
145  λglobals,addr1,addr2,arg.
146  [ STORE … addr1 addr2 arg ;
147    addr1 ← addr1 .Add. (int_size : Byte) ;
148    addr2 ← addr2 .Addc. zero_byte
149  ].
150
151definition set_params_stack :
152  ∀globals.list psd_argument → bind_new (localsT ERTL) ? ≝
153  λglobals,params.
154  νaddr1,addr2 in
155  let params_length_byte : Byte ≝ bitvector_of_nat ? (|params|) in
156  [ PSD addr1 ← HDW RegisterSPL ;
157    PSD addr2 ← HDW RegisterSPH ;
158    CLEAR_CARRY ?? ;
159    addr1 ← addr1 .Sub. params_length_byte ;
160    addr2 ← addr2 .Sub. zero_byte
161  ] @
162  flatten … (map … (set_param_stack globals addr1 addr2) params).
163
164definition set_params ≝
165  λglobals,params.
166  let n ≝ min (|params|) (|RegisterParams|) in
167  let hdw_stack_params ≝ split ? params n in
168  let hdw_params ≝ \fst hdw_stack_params in
169  let stack_params ≝ \snd hdw_stack_params in
170  set_params_hdw globals hdw_params @@ set_params_stack globals stack_params.
171
172definition fetch_result :
173  ∀globals.list register → list (joint_seq ERTL globals) ≝
174  λglobals,ret_regs.
175  match reduce_strong ?? RegisterSTS RegisterRets with
176  [ mk_Sig crl crl_proof ⇒
177    let commonl ≝ \fst (\fst crl) in
178    let commonr ≝ \fst (\snd crl) in
179    map2 … (λst,r.HDW st ← HDW r) commonl commonr crl_proof @
180    match reduce_strong ?? ret_regs RegisterSTS with
181    [ mk_Sig crl crl_proof ⇒
182      let commonl ≝ \fst (\fst crl) in
183      let commonr ≝ \fst (\snd crl) in
184      map2 … (λret,st.PSD ret ← HDW st) commonl commonr crl_proof
185    ]
186  ].
187
188definition translate_step :
189  ∀globals.label → joint_step RTL_ntc globals →
190    bind_seq_block ERTL globals (joint_step ERTL globals) ≝
191  λglobals.λ_.λs.
192  match s return λ_.bind_seq_block ?? (joint_step ??) with
193  [ step_seq s ⇒
194    match s return λ_.bind_seq_block ?? (joint_step ??) with
195    [ PUSH _ ⇒ NOOP … (*CSC: XXXX should not be in the syntax *)
196    | POP _ ⇒ NOOP …  (*CSC: XXXX should not be in the syntax *)
197    | MOVE rs ⇒ PSD (\fst rs) ← \snd rs
198    | COST_LABEL lbl ⇒
199      COST_LABEL … lbl
200    | ADDRESS x prf r1 r2 ⇒
201      ADDRESS ERTL ? x prf r1 r2
202    | OPACCS op destr1 destr2 srcr1 srcr2 ⇒
203      OPACCS ERTL ? op destr1 destr2 srcr1 srcr2 
204    | OP1 op1 destr srcr ⇒
205      OP1 ERTL ? op1 destr srcr
206    | OP2 op2 destr srcr1 srcr2 ⇒
207      OP2 ERTL ? op2 destr srcr1 srcr2
208    | CLEAR_CARRY ⇒
209      CLEAR_CARRY …
210    | SET_CARRY ⇒
211      SET_CARRY …
212    | LOAD destr addr1 addr2 ⇒
213      LOAD ERTL ? destr addr1 addr2
214    | STORE addr1 addr2 srcr ⇒
215      STORE ERTL ? addr1 addr2 srcr
216    | COMMENT msg ⇒
217      COMMENT … msg
218    | extension_seq ext ⇒
219      match ext with
220      [ rtl_stack_address addr1 addr2 ⇒
221        [ PSD addr1 ← HDW RegisterSPL ; PSD addr2 ← HDW RegisterSPH ]
222      ]
223    | CALL f args ret_regs ⇒
224      set_params ? args @@
225      CALL ERTL ? f (|args|) it :::
226      fetch_result ? ret_regs
227    ]
228  | COND r ltrue ⇒
229    COND ERTL ? r ltrue
230  ].
231
232definition translate_fin_step :
233  ∀globals.label → joint_fin_step RTL_ntc →
234    bind_seq_block ERTL globals (joint_fin_step ERTL) ≝
235  λglobals.λ_.λs.
236  match s with
237  [ GOTO lbl' ⇒ GOTO … lbl'
238  | RETURN ⇒ RETURN ?
239  | TAILCALL abs _ _ ⇒ match abs in False with [ ]
240  ].
241
242(* hack with empty graphs used here *)
243definition translate_funct :
244  ∀globals.joint_closed_internal_function RTL_ntc globals →
245    joint_closed_internal_function ERTL globals ≝
246  λglobals,def.
247  let nb_params ≝ |joint_if_params ?? def| in
248  let added_stacksize ≝ max 0 (minus nb_params (|RegisterParams|)) in
249  let new_locals ≝ nub_by ? (eq_identifier ?) ((joint_if_locals … def) @ (joint_if_params … def)) in
250  let entry' ≝ pi1 … (joint_if_entry … def) in
251  let exit' ≝ pi1 … (joint_if_exit … def) in
252  let def' ≝ init_graph_if ERTL globals
253      (joint_if_luniverse … def) (joint_if_runiverse … def) it (*Paolo: to be checked, unit or list register? *)
254      nb_params new_locals ((joint_if_stacksize … def) + added_stacksize)
255      entry' exit' in
256  let def'' ≝ b_graph_translate …
257    (ertl_fresh_reg …)
258    def'
259    (translate_step globals)
260    (translate_fin_step globals)
261    def in
262  add_pro_and_epilogue ? (joint_if_params ?? def) (joint_if_result ?? def) def'.
263 cases daemon (* TODO *) qed.
264
265(* removing this because of how insert_prologue is now defined
266definition generate ≝
267  λglobals.
268  λstmt.
269  λdef: joint_internal_function globals ERTL.
270  let 〈entry, def〉 ≝ fresh_label … def in
271  let graph ≝ add … (joint_if_code … def) entry stmt in
272   set_joint_if_graph … (ERTL globals) graph def ??.
273  [ (*% [ @entry | @graph_add ]*) cases daemon (*CSC: XXX *)
274  | (*cases (joint_if_exit … def) #LBL #LBL_PRF % [ @LBL | @graph_add_lookup @LBL_PRF
275    *) cases daemon (*CSC: XXX *)
276  ]
277qed.
278
279let rec find_and_remove_first_cost_label_internal (globals: list ident)
280  (def: ertl_internal_function globals) (lbl: label) (num_nodes: nat)
281    on num_nodes ≝
282  match num_nodes with
283  [ O ⇒ 〈None ?, def〉
284  | S num_nodes' ⇒
285    match lookup … (joint_if_code … def) lbl with
286    [ None ⇒ 〈None ?, def〉
287    | Some stmt ⇒
288      match stmt with
289      [ sequential inst lbl ⇒
290         match inst with
291          [ COST_LABEL cost_lbl ⇒
292             〈Some … cost_lbl, add_graph ERTL1 globals lbl (GOTO … lbl) def〉
293          | _ ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ]
294      | RETURN ⇒ 〈None …, def〉
295      | GOTO lbl ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes'
296      ]]].
297   
298definition find_and_remove_first_cost_label ≝
299  λglobals,def. 
300    find_and_remove_first_cost_label_internal globals def (joint_if_entry … def) (graph_num_nodes ? (joint_if_code … def)).
301
302definition move_first_cost_label_up_internal ≝
303  λglobals,def.
304  let 〈cost_label, def〉 ≝ find_and_remove_first_cost_label … def in
305  match cost_label with
306  [ None ⇒ def
307  | Some cost_label ⇒ generate … (sequential ERTL_ globals (COST_LABEL … cost_label) (joint_if_entry … def)) def
308  ].
309
310definition translate_funct ≝ λglobals,def. (move_first_cost_label_up_internal … (translate_funct_internal globals def)).
311*)
312
313definition rtl_to_ertl : rtl_program → ertl_program ≝
314 λp.
315  transform_program ??? p (λvarnames. transf_fundef ?? (translate_funct varnames)).
Note: See TracBrowser for help on using the repository browser.