source: src/RTL/RTLToERTL_paolo.ma @ 2208

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