source: src/RTL/RTLToERTL.ma

Last change on this file was 3263, checked in by tranquil, 7 years ago

moved callee saved saving and restoring to ERTL -> LTL pass (untrusted
colourer and interference graph creator still need to be updated)
joint now has the stack size split in three (referenced locals, params
and spilled)

File size: 13.6 KB
Line 
1include "utilities/RegisterSet.ma".
2include "common/Identifiers.ma".
3include "RTL/RTL.ma".
4include "ERTL/ERTL.ma".
5include "joint/TranslateUtils.ma".
6include "joint/joint_stacksizes.ma".
7
8include alias "basics/lists/list.ma".
9
10definition save_hdws :
11  ∀globals.list (register×(Σr.ertl_hdw_readable r∧ertl_hdw_writable r)) → list (joint_seq ERTL globals) ≝
12 λglobals.
13  let save_hdws_internal : (register×(Σr.?)) → ? ≝
14     λdestr_srcr.PSD (\fst destr_srcr) ← HDW (\snd destr_srcr) in
15  map ?? save_hdws_internal.
16[ @(π1 (pi2 ?? (\snd destr_srcr))) | @I ] qed.
17
18definition restore_hdws :
19  ∀globals.list (psd_argument×(Σr.ertl_hdw_readable r∧ertl_hdw_writable r)) → list (joint_seq ERTL globals) ≝
20  λglobals.
21   let restore_hdws_internal ≝
22    λdestr_srcr:psd_argument×(Σr.?).HDW (\snd destr_srcr) ← \fst destr_srcr in
23    map ? ? restore_hdws_internal.
24  @(π2 (pi2 ?? (\snd destr_srcr))) qed.
25 
26definition RegisterParamsSig : list (Σr.ertl_hdw_readable r∧ertl_hdw_writable r) ≝
27[Register30; Register31; Register32; Register33; Register34; Register35;
28   Register36; Register37]. %% qed.
29
30(*definition RegisterCalleeSavedSig : list (Σr.ertl_hdw_readable r∧ertl_hdw_writable r) ≝
31[Register20; Register21; Register22; Register23; Register24; Register25;
32   Register26; Register27]. %% qed.*)
33
34definition RegisterRetsSig : list (Σr.ertl_hdw_readable r∧ertl_hdw_writable r) ≝
35 [Register00; Register01; Register02; Register03]. %% qed.
36
37definition get_params_hdw :
38  ∀globals.list register → list (joint_seq ERTL globals) ≝
39  λglobals,params.
40  save_hdws … (zip_pottier … params RegisterParamsSig).
41
42definition get_param_stack :
43  ∀globals.register → register → register →
44  list (joint_seq ERTL globals) ≝
45  λglobals,addr1,addr2,destr.
46  (* liveness analysis will erase the last useless ops *)
47  [ LOAD ?? destr addr1 addr2 ;
48    addr1 ← addr1 .Add. (int_size : Byte) ;
49    addr2 ← addr2 .Addc. zero_byte
50  ].
51
52definition get_params_stack :
53  ∀globals.register → register → register → list register →
54  list (joint_seq ERTL globals) ≝
55  λglobals.
56  λtmpr,addr1,addr2,params.
57  let params_length_byte : Byte ≝ bitvector_of_nat ? (|params|) in
58  [ (ertl_frame_size tmpr : joint_seq ??) ;
59    CLEAR_CARRY ?? ;
60    tmpr ← tmpr .Sub. params_length_byte ; (* will be constant later *)
61    PSD addr1 ← HDW RegisterSPL ;
62    PSD addr2 ← HDW RegisterSPH ;
63    addr1 ← addr1 .Add. tmpr ;
64    addr2 ← addr2 .Addc. zero_byte ] @   
65  flatten … (map ?? (get_param_stack globals addr1 addr2) params). % qed.
66
67definition get_params ≝
68  λglobals,tmpr,addr1,addr2,params.
69  let n ≝ min (length … params) (length … RegisterParams) in
70  let 〈hdw_params, stack_params〉 ≝ list_split … n params in
71  get_params_hdw globals hdw_params @ get_params_stack … tmpr addr1 addr2 stack_params.
72
73(*
74definition save_return :
75  ∀globals.list register → 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.?.λr : register.HDW st ← r) commonl commonr crl_proof @
84    map … (λst : Σr.?.HDW st ← zero_byte) restl
85  ]. @(pi2 ?? st) qed.
86*)
87
88
89definition assign_result : ∀globals.
90  list register → list (joint_seq ERTL globals) ≝
91  λglobals,ret_regs.
92  match reduce_strong ?? RegisterRetsSig ret_regs with
93  [ mk_Sig crl crl_proof ⇒
94    let commonl ≝ \fst (\fst crl) in
95    let commonr ≝ \fst (\snd crl) in
96    let restl ≝ \snd (\fst crl) in
97    map2 … (λR : Σr.?.λr : register.HDW R ← PSD r) commonl commonr crl_proof @
98    map … (λR : Σr.?.HDW R ← zero_byte) restl
99  ]. [ @I |*: @(π2 (pi2 ?? R)) ] qed.
100
101lemma All_map2 : ∀A,B,C,P,R,f,l1,l2,prf.
102 All2 A B P l1 l2 →
103 (∀x,y.P x y → R (f x y)) →
104 All C R (map2 A B C f l1 l2 prf).
105#A #B #C #P #R #f #l1 elim l1 -l1
106[ * [ #prf * #H % ] #hd' #tl'
107| #hd #tl #IH * [2: #hd' #tl' ]
108] #prf normalize in prf; destruct
109* #H1 #H2 #H % [ @H @H1 | @IH assumption ] qed.
110
111lemma All2_True : ∀A,B,l1,l2.|l1| = |l2| → All2 A B (λ_.λ_.True) l1 l2.
112#A #B #l1 elim l1 -l1
113[ * [ #prf % ] #hd' #tl'
114| #hd #tl #IH * [2: #hd' #tl' ]
115] #prf normalize in prf; destruct %{I} @IH assumption
116qed.
117
118lemma All_True : ∀A,l.All A (λ_.True) l.
119#A #l elim l -l [ % | #hd #tl #IH %{I IH} ] qed.
120
121definition epilogue :
122  ∀globals.list register → register → register →
123  Σl : list (joint_seq ERTL globals).
124  All (joint_seq ??) (λs.step_labels ?? s = [ ]) l ≝
125  λglobals,ret_regs,sral,srah.
126  assign_result globals ret_regs @
127  [ PUSH ERTL ? sral ;
128    PUSH … srah ].
129@hide_prf
130@All_append
131[ whd in match assign_result;
132  generalize in match reduce_strong; #f normalize nodelta
133  cases (f ????) #l #prf normalize nodelta
134  @All_append
135  [ @(All_map2 … (All2_True … prf)) #x #y #_ %
136  | @(All_map … (All_True …)) #x #_ %
137  ]
138| %%%
139]
140qed.
141
142definition prologue :
143  ∀globals.list register → register → register → register → register → register →
144  bind_new register (list (joint_seq ERTL globals)) ≝
145  λglobals,params,sral,srah,tmpr,addr1,addr2.
146  [ POP ERTL … srah ;
147    POP … sral
148  ] @ get_params … tmpr addr1 addr2 params.
149
150definition set_params_hdw :
151  ∀globals.list psd_argument → list (joint_seq ERTL globals) ≝
152  λglobals,params.
153  restore_hdws globals (zip_pottier ? ? params RegisterParamsSig).
154
155definition set_param_stack :
156  ∀globals.register → register → psd_argument →
157  list (joint_seq ERTL globals) ≝
158  λglobals,addr1,addr2,arg.
159  [ STORE … addr1 addr2 arg ;
160    addr1 ← addr1 .Add. (int_size : Byte) ;
161    addr2 ← addr2 .Addc. zero_byte
162  ].
163
164definition set_params_stack :
165  ∀globals.list psd_argument → bind_new register ? ≝
166  λglobals,params.
167  νaddr1,addr2 in
168  let params_length_byte : Byte ≝ bitvector_of_nat ? (|params|) in
169  [ PSD addr1 ← HDW RegisterSPL ;
170    PSD addr2 ← HDW RegisterSPH ;
171    CLEAR_CARRY ?? ;
172    addr1 ← addr1 .Sub. params_length_byte ;
173    addr2 ← addr2 .Sub. zero_byte
174  ] @
175  flatten … (map … (set_param_stack globals addr1 addr2) params). % qed.
176
177definition set_params :
178  ∀globals.list psd_argument →
179  Σb : bind_new register (list (joint_seq ERTL globals)).
180  BindNewP … (All (joint_seq ??) (λs.step_labels … s = [ ])) b ≝
181  λglobals,params.
182  let n ≝ min (|params|) (|RegisterParamsSig|) in
183  let hdw_stack_params ≝ split ? params n in
184  let hdw_params ≝ \fst hdw_stack_params in
185  let stack_params ≝ \snd hdw_stack_params in
186  set_params_hdw globals hdw_params @@ set_params_stack globals stack_params.
187@hide_prf
188  @mp_bind [3: #l1 #H1 @mp_bind [3: #l2 #H2 @(All_append … H1 H2) ] |*:]
189  [ #r1 #r2
190    %{(refl …)} %{(refl …)} %{(refl …)} %{(refl …)} %{(refl …)}
191    @All_append [ % ]
192    elim stack_params [ % ] #hd #tl #IH whd in match flatten; normalize nodelta
193    whd in match (foldr ?????); %{(refl …)} %{(refl …)} %{(refl …)} @IH
194  | whd whd in match set_params_hdw; normalize nodelta
195    whd in match restore_hdws; normalize nodelta @(All_map … (All_True …))
196    #a #_ %
197  ]
198qed.
199
200definition fetch_result :
201  ∀globals.list register →
202  Σl : list (joint_seq ERTL globals).
203  All (joint_seq ??) (λs.step_labels ?? s = [ ]) l ≝
204  λglobals,ret_regs.
205  match reduce_strong ?? ret_regs RegisterRetsSig with
206  [ mk_Sig crl crl_proof ⇒
207    let commonl ≝ \fst (\fst crl) in
208    let commonr ≝ \fst (\snd crl) in
209    map2 … (λr.λR : Σr.?.PSD r ← HDW R) commonl commonr crl_proof
210  ].
211@hide_prf [2: % |3: @(π1 (pi2 … R)) ]
212@(All_map2 … (All2_True … crl_proof)) #x #y #_ %
213qed.
214
215definition translate_step :
216  ∀globals.label → joint_step RTL globals →
217    bind_step_block ERTL globals ≝
218  λglobals.λ_.λs.
219  match s return λ_.bind_step_block ?? with
220  [ step_seq s ⇒
221    bret … match s return λ_.step_block ?? with
222    [ PUSH _ ⇒ [ ] (*CSC: XXXX should not be in the syntax *)
223    | POP _ ⇒ [ ] (*CSC: XXXX should not be in the syntax *)
224    | MOVE rs ⇒ [PSD (\fst rs) ← \snd rs]
225    | ADDRESS x prf off r1 r2 ⇒
226      [ADDRESS ERTL ? x prf off r1 r2]
227    | OPACCS op destr1 destr2 srcr1 srcr2 ⇒
228      [OPACCS ERTL ? op destr1 destr2 srcr1 srcr2]
229    | OP1 op1 destr srcr ⇒
230      [OP1 ERTL ? op1 destr srcr]
231    | OP2 op2 destr srcr1 srcr2 ⇒
232      [OP2 ERTL ? op2 destr srcr1 srcr2]
233    | CLEAR_CARRY ⇒
234      [CLEAR_CARRY ??]
235    | SET_CARRY ⇒
236      [SET_CARRY ??]
237    | LOAD destr addr1 addr2 ⇒
238      [LOAD ERTL ? destr addr1 addr2]
239    | STORE addr1 addr2 srcr ⇒
240      [STORE ERTL ? addr1 addr2 srcr]
241    | COMMENT msg ⇒
242      [COMMENT … msg]
243    | extension_seq ext ⇒
244      match ext return λ_.step_block ?? with
245      [ rtl_stack_address addr1 addr2 ⇒
246        [ PSD addr1 ← HDW RegisterSPL ; PSD addr2 ← HDW RegisterSPH ]
247      ]
248    ]
249  | COST_LABEL lbl ⇒
250    bret … 〈[ ], λ_.COST_LABEL ERTL ? lbl, [ ]〉
251  | CALL f args ret_regs ⇒
252    ! pref ← pi1 … (set_params ? args) ;
253    bret ? (step_block ??) 〈add_dummy_variance … pref,
254             λ_.CALL ERTL ? f (|args|) it,
255             fetch_result ? ret_regs〉
256  | COND r ltrue ⇒
257    bret … 〈[ ], λ_.COND ERTL ? r ltrue, [ ]〉
258  ]. % qed.
259
260definition translate_fin_step :
261  ∀globals.list register → register → register →
262    label → joint_fin_step RTL →
263    bind_fin_block ERTL globals ≝
264  λglobals.λral,rah,to_restore.λ_.λs.
265  match s return λ_.bind_fin_block ERTL ? with
266  [ GOTO lbl' ⇒ bret … 〈[ ], GOTO … lbl'〉
267  | RETURN ⇒ bret … 〈epilogue … ral rah to_restore, RETURN ?〉
268  | TAILCALL b _ _ ⇒ match b in False with [ ]
269  ].
270
271definition translate_data :
272 ∀globals.joint_closed_internal_function RTL globals →
273 bound_b_graph_translate_data RTL ERTL globals ≝
274λglobals,def.
275let params ≝ joint_if_params … def in
276    νral,rah,tmpr,addr1,addr2 in
277    ! prologue ← prologue globals params ral rah tmpr addr1 addr2 ;
278    return mk_b_graph_translate_data RTL ERTL globals
279    (* init_ret ≝ *) it
280    (* init_params ≝ *) it
281    (* init_local_stacksize ≝ *) (joint_if_local_stacksize … def)
282    (* init_params_stacksize ≝ *) (joint_if_params_stacksize … def + (* is 0, but needed for monotonicity *)
283                                   (|params| - |RegisterParams|))
284    (* init_spilled_stacksize ≝ *) (joint_if_spilled_stacksize … def(* is 0, but needed for monotonicity *))
285    (* added_prologue ≝ *) prologue
286    (* new_regs ≝ *) ([ral ; rah ; tmpr ; addr1 ; addr2 ])
287    (* f_step ≝ *) (translate_step globals)
288    (* f_fin ≝ *) (translate_fin_step globals (joint_if_result … def) ral rah)
289    ????.
290@hide_prf
291[2: #l #c %
292|1: #l * [ #c' | #f #args #dest | #a #ltrue | #s ] #c whd
293  [2: #r1 #r2 ] whd #l' #EQ destruct try %
294  cases s in EQ; whd in match ensure_step_block; normalize nodelta
295  try #a try #b try #c try #d try #e try #f destruct
296  cases a in b; #a1 #a2 normalize nodelta #EQ destruct
297|5: #ral #rah #tmpr #addr1 #addr2 %
298|*:  cases daemon (* TODO *)
299]
300(* #l *
301[ #l whd %{I} %{I} %1 %
302| whd %{I} cases (epilogue ?????) @All_mp #s #EQ whd >EQ %
303| *
304| #c %{I} %{I} #l %
305| #called #args #dest @(mp_bind … (BindNewP …))
306  [2: @(pi2 ? (λ_.?)) |*:] #l1 #H1 whd % [%]
307    [ @(All_map … H1) #a #EQ #l whd >EQ %
308    | #l %
309    | cases (fetch_result ??) @All_mp #s #EQ whd >EQ %
310    ]
311| #a #l_true whd %{I} %{I} #l %{I} %2 %1 %
312| * try #a try #b try #c try #d try #e whd
313  try (%{I} %{I} #l %)
314  cases a -a #a #b whd %{I} % [ %{I} ] #l %
315]*)
316qed.
317
318(* removing this because of how insert_prologue is now defined
319definition generate ≝
320  λglobals.
321  λstmt.
322  λdef: joint_internal_function globals ERTL.
323  let 〈entry, def〉 ≝ fresh_label … def in
324  let graph ≝ add … (joint_if_code … def) entry stmt in
325   set_joint_if_graph … (ERTL globals) graph def ??.
326  [ (*% [ @entry | @graph_add ]*) cases daemon (*CSC: XXX *)
327  | (*cases (joint_if_exit … def) #LBL #LBL_PRF % [ @LBL | @graph_add_lookup @LBL_PRF
328    *) cases daemon (*CSC: XXX *)
329  ]
330qed.
331
332let rec find_and_remove_first_cost_label_internal (globals: list ident)
333  (def: ertl_internal_function globals) (lbl: label) (num_nodes: nat)
334    on num_nodes ≝
335  match num_nodes with
336  [ O ⇒ 〈None ?, def〉
337  | S num_nodes' ⇒
338    match lookup … (joint_if_code … def) lbl with
339    [ None ⇒ 〈None ?, def〉
340    | Some stmt ⇒
341      match stmt with
342      [ sequential inst lbl ⇒
343         match inst with
344          [ COST_LABEL cost_lbl ⇒
345             〈Some … cost_lbl, add_graph ERTL1 globals lbl (GOTO … lbl) def〉
346          | _ ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ]
347      | RETURN ⇒ 〈None …, def〉
348      | GOTO lbl ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes'
349      ]]].
350   
351definition find_and_remove_first_cost_label ≝
352  λglobals,def. 
353    find_and_remove_first_cost_label_internal globals def (joint_if_entry … def) (graph_num_nodes ? (joint_if_code … def)).
354
355definition move_first_cost_label_up_internal ≝
356  λglobals,def.
357  let 〈cost_label, def〉 ≝ find_and_remove_first_cost_label … def in
358  match cost_label with
359  [ None ⇒ def
360  | Some cost_label ⇒ generate … (sequential ERTL_ globals (COST_LABEL … cost_label) (joint_if_entry … def)) def
361  ].
362
363definition translate_funct ≝ λglobals,def. (move_first_cost_label_up_internal … (translate_funct_internal globals def)).
364*)
365
366definition rtl_to_ertl : rtl_program → ertl_program ≝
367  b_graph_transform_program … translate_data.
368
369lemma RTLToERTL_monotone_stacksizes :
370∀p_in.let p_out ≝ rtl_to_ertl p_in in
371stack_cost_model_le (stack_cost ? p_in) (stack_cost ? p_out) ≝
372joint_transform_monotone_stacksizes ….
Note: See TracBrowser for help on using the repository browser.