source: src/RTL/RTLToERTL.ma @ 2652

Last change on this file since 2652 was 2490, checked in by tranquil, 7 years ago

switched back to Byte immediate (instead of beval ones)
propagated pending changes to all passes

File size: 11.5 KB
Line 
1include "RTL/RTLTailcall.ma".
2include "utilities/RegisterSet.ma".
3include "common/Identifiers.ma".
4include "ERTL/ERTL.ma".
5include "joint/TranslateUtils.ma".
6
7include alias "basics/lists/list.ma".
8
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.
18  let save_hdws_internal ≝
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.
25   let restore_hdws_internal ≝
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).
58
59definition get_params ≝
60  λglobals,params.
61  let n ≝ min (length … params) (length … RegisterParams) in
62  let 〈hdw_params, stack_params〉 ≝ list_split … n params 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.
77  match reduce_strong ? ? RegisterSTS ret_regs with
78  [ mk_Sig crl crl_proof ⇒
79    let commonl ≝ \fst (\fst crl) in
80    let commonr ≝ \fst (\snd crl) in
81    let restl ≝ \snd (\fst crl) in
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
90  [ mk_Sig crl crl_proof ⇒
91    let commonl ≝ \fst (\fst crl) in
92    let commonr ≝ \fst (\snd crl) in
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.
111   let allocate_regs_internal ≝
112    λr: Register.
113    λdef_sregs.
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).
164
165definition set_params ≝
166  λglobals,params.
167  let n ≝ min (|params|) (|RegisterParams|) in
168  let hdw_stack_params ≝ split ? params n in
169  let hdw_params ≝ \fst hdw_stack_params in
170  let stack_params ≝ \snd hdw_stack_params in
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 ⇒
178    let commonl ≝ \fst (\fst crl) in
179    let commonr ≝ \fst (\snd crl) in
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 ⇒
183      let commonl ≝ \fst (\fst crl) in
184      let commonr ≝ \fst (\snd crl) in
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 ]
223      ]
224    | CALL f args ret_regs ⇒
225      set_params ? args @@
226      CALL ERTL ? f (|args|) it :::
227      fetch_result ? ret_regs
228    ]
229  | COND r ltrue ⇒
230    COND ERTL ? r ltrue
231  ].
232
233definition translate_fin_step :
234  ∀globals.label → joint_fin_step RTL_ntc →
235    bind_seq_block ERTL globals (joint_fin_step ERTL) ≝
236  λglobals.λ_.λs.
237  match s with
238  [ GOTO lbl' ⇒ GOTO … lbl'
239  | RETURN ⇒ RETURN ?
240  | TAILCALL abs _ _ ⇒ match abs in False with [ ]
241  ].
242
243(* hack with empty graphs used here *)
244definition translate_funct :
245  ∀globals.joint_closed_internal_function RTL_ntc globals →
246    joint_closed_internal_function ERTL globals ≝
247  λglobals,def.
248  let nb_params ≝ |joint_if_params ?? def| in
249  let added_stacksize ≝ max 0 (minus nb_params (|RegisterParams|)) in
250  let new_locals ≝ nub_by ? (eq_identifier ?) ((joint_if_locals … def) @ (joint_if_params … def)) in
251  let entry' ≝ pi1 … (joint_if_entry … def) in
252  let exit' ≝ pi1 … (joint_if_exit … def) in
253  let def' ≝ init_graph_if ERTL globals
254      (joint_if_luniverse … def) (joint_if_runiverse … def) it (*Paolo: to be checked, unit or list register? *)
255      nb_params new_locals ((joint_if_stacksize … def) + added_stacksize)
256      entry' exit' in
257  let def'' ≝ b_graph_translate …
258    (ertl_fresh_reg …)
259    def'
260    (translate_step globals)
261    (translate_fin_step globals)
262    def in
263  add_pro_and_epilogue ? (joint_if_params ?? def) (joint_if_result ?? def) def'.
264 cases daemon (* TODO *) qed.
265
266(* removing this because of how insert_prologue is now defined
267definition generate ≝
268  λglobals.
269  λstmt.
270  λdef: joint_internal_function globals ERTL.
271  let 〈entry, def〉 ≝ fresh_label … def in
272  let graph ≝ add … (joint_if_code … def) entry stmt in
273   set_joint_if_graph … (ERTL globals) graph def ??.
274  [ (*% [ @entry | @graph_add ]*) cases daemon (*CSC: XXX *)
275  | (*cases (joint_if_exit … def) #LBL #LBL_PRF % [ @LBL | @graph_add_lookup @LBL_PRF
276    *) cases daemon (*CSC: XXX *)
277  ]
278qed.
279
280let rec find_and_remove_first_cost_label_internal (globals: list ident)
281  (def: ertl_internal_function globals) (lbl: label) (num_nodes: nat)
282    on num_nodes ≝
283  match num_nodes with
284  [ O ⇒ 〈None ?, def〉
285  | S num_nodes' ⇒
286    match lookup … (joint_if_code … def) lbl with
287    [ None ⇒ 〈None ?, def〉
288    | Some stmt ⇒
289      match stmt with
290      [ sequential inst lbl ⇒
291         match inst with
292          [ COST_LABEL cost_lbl ⇒
293             〈Some … cost_lbl, add_graph ERTL1 globals lbl (GOTO … lbl) def〉
294          | _ ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ]
295      | RETURN ⇒ 〈None …, def〉
296      | GOTO lbl ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes'
297      ]]].
298   
299definition find_and_remove_first_cost_label ≝
300  λglobals,def. 
301    find_and_remove_first_cost_label_internal globals def (joint_if_entry … def) (graph_num_nodes ? (joint_if_code … def)).
302
303definition move_first_cost_label_up_internal ≝
304  λglobals,def.
305  let 〈cost_label, def〉 ≝ find_and_remove_first_cost_label … def in
306  match cost_label with
307  [ None ⇒ def
308  | Some cost_label ⇒ generate … (sequential ERTL_ globals (COST_LABEL … cost_label) (joint_if_entry … def)) def
309  ].
310
311definition translate_funct ≝ λglobals,def. (move_first_cost_label_up_internal … (translate_funct_internal globals def)).
312*)
313
314definition rtl_to_ertl : rtl_program → ertl_program ≝
315 λp.
316  let p ≝ tailcall_simplify p in (* tailcall simplification here *)
317    transform_program ??? p (λvarnames. transf_fundef ?? (translate_funct varnames)).
Note: See TracBrowser for help on using the repository browser.