source: src/RTL/RTLToERTL_paolo.ma @ 2162

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