source: src/RTL/RTLToERTL.ma @ 2695

Last change on this file since 2695 was 2689, checked in by tranquil, 7 years ago
  • fixed passes up to linearisation
File size: 13.2 KB
Line 
1include "utilities/RegisterSet.ma".
2include "common/Identifiers.ma".
3include "RTL/RTL.ma".
4include "ERTL/ERTL.ma".
5include "joint/TranslateUtils.ma".
6
7include alias "basics/lists/list.ma".
8
9definition save_hdws :
10  ∀globals.list (register×Register) → list (joint_seq ERTL 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 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 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 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 register (list (joint_seq ERTL 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 save_return :
60  ∀globals.list psd_argument → list (joint_seq ERTL globals) ≝
61  λglobals,ret_regs.
62  match reduce_strong ? ? RegisterSTS ret_regs with
63  [ mk_Sig crl crl_proof ⇒
64    let commonl ≝ \fst (\fst crl) in
65    let commonr ≝ \fst (\snd crl) in
66    let restl ≝ \snd (\fst crl) in
67    (* let restr ≝ \snd (\snd crl) in *)
68    map2 … (λst.λr : psd_argument.HDW st ← r) commonl commonr crl_proof @
69    map … (λst.HDW st ← zero_byte) restl
70  ].
71
72definition assign_result : ∀globals.list (joint_seq ERTL globals) ≝
73  λglobals.
74  match reduce_strong ?? RegisterRets RegisterSTS with
75  [ mk_Sig crl crl_proof ⇒
76    let commonl ≝ \fst (\fst crl) in
77    let commonr ≝ \fst (\snd crl) in
78    map2 … (λret,st.HDW ret ← HDW st) commonl commonr crl_proof
79  ].
80
81lemma All_map2 : ∀A,B,C,P,R,f,l1,l2,prf.
82 All2 A B P l1 l2 →
83 (∀x,y.P x y → R (f x y)) →
84 All C R (map2 A B C f l1 l2 prf).
85#A #B #C #P #R #f #l1 elim l1 -l1
86[ * [ #prf * #H % ] #hd' #tl'
87| #hd #tl #IH * [2: #hd' #tl' ]
88] #prf normalize in prf; destruct
89* #H1 #H2 #H % [ @H @H1 | @IH assumption ] qed.
90
91lemma All2_True : ∀A,B,l1,l2.|l1| = |l2| → All2 A B (λ_.λ_.True) l1 l2.
92#A #B #l1 elim l1 -l1
93[ * [ #prf % ] #hd' #tl'
94| #hd #tl #IH * [2: #hd' #tl' ]
95] #prf normalize in prf; destruct %{I} @IH assumption
96qed.
97
98lemma All_True : ∀A,l.All A (λ_.True) l.
99#A #l elim l -l [ % | #hd #tl #IH %{I IH} ] qed.
100
101definition epilogue :
102  ∀globals.list register → register → register → list (register × Register) →
103  Σl : list (joint_seq ERTL globals).
104  All (joint_seq ??) (λs.step_labels ?? s = [ ]) l ≝
105  λglobals,ret_regs,sral,srah,sregs.
106  save_return … (map … (Reg ?) ret_regs) @
107  restore_hdws … (map … (λpr.〈Reg ? (\fst pr),\snd pr〉) sregs) @
108  [ PUSH ERTL ? srah ;
109    PUSH … sral ;
110    ertl_del_frame ] @
111  assign_result globals.
112@hide_prf
113@All_append
114[ whd in match save_return; normalize nodelta
115  cases (reduce_strong ????) ** #a #b * #c #d #prf normalize nodelta
116  @All_append
117  [ @(All_map2 … (All2_True … prf)) #x #y #_ %
118  | @(All_map … (All_True …)) #x #_ %
119  ]
120| @All_append
121  [ @(All_map … (All_True …)) #x #_ %
122  | %{(refl …)} %{(refl …)} %{(refl …)}
123    whd in match assign_result;
124    generalize in match reduce_strong; #f normalize nodelta
125    cases (f ????) #l #prf normalize nodelta
126    @(All_map2 … (All2_True … prf)) #x #y #_ %
127  ]
128]
129qed.
130
131definition prologue :
132  ∀globals.list register → register → register → list (register×Register) →
133  bind_new register (list (joint_seq ERTL globals)) ≝
134  λglobals,params,sral,srah,sregs.
135  [ (ertl_new_frame : joint_seq ??) ;
136    POP … sral ;
137    POP … srah
138  ] @@ save_hdws … sregs @@ get_params … params.
139
140definition set_params_hdw :
141  ∀globals.list psd_argument → list (joint_seq ERTL globals) ≝
142  λglobals,params.
143  restore_hdws globals (zip_pottier ? ? params RegisterParams).
144
145(* Paolo: The following can probably be done way more efficiently with INC DPTR *)
146
147definition set_param_stack :
148  ∀globals.register → register → psd_argument →
149  list (joint_seq ERTL globals) ≝
150  λglobals,addr1,addr2,arg.
151  [ STORE … addr1 addr2 arg ;
152    addr1 ← addr1 .Add. (int_size : Byte) ;
153    addr2 ← addr2 .Addc. zero_byte
154  ].
155
156definition set_params_stack :
157  ∀globals.list psd_argument → bind_new register ? ≝
158  λglobals,params.
159  νaddr1,addr2 in
160  let params_length_byte : Byte ≝ bitvector_of_nat ? (|params|) in
161  [ PSD addr1 ← HDW RegisterSPL ;
162    PSD addr2 ← HDW RegisterSPH ;
163    CLEAR_CARRY ?? ;
164    addr1 ← addr1 .Sub. params_length_byte ;
165    addr2 ← addr2 .Sub. zero_byte
166  ] @
167  flatten … (map … (set_param_stack globals addr1 addr2) params).
168
169definition set_params :
170  ∀globals.list psd_argument →
171  Σb : bind_new register (list (joint_seq ERTL globals)).
172  BindNewP … (All (joint_seq ??) (λs.step_labels … s = [ ])) b ≝
173  λglobals,params.
174  let n ≝ min (|params|) (|RegisterParams|) in
175  let hdw_stack_params ≝ split ? params n in
176  let hdw_params ≝ \fst hdw_stack_params in
177  let stack_params ≝ \snd hdw_stack_params in
178  set_params_hdw globals hdw_params @@ set_params_stack globals stack_params.
179@hide_prf
180  @mp_bind [3: #l1 #H1 @mp_bind [3: #l2 #H2 @(All_append … H1 H2) ] |*:]
181  [ #r1 #r2
182    %{(refl …)} %{(refl …)} %{(refl …)} %{(refl …)} %{(refl …)}
183    @All_append [ % ]
184    elim stack_params [ % ] #hd #tl #IH whd in match flatten; normalize nodelta
185    whd in match (foldr ?????); %{(refl …)} %{(refl …)} %{(refl …)} @IH
186  | whd whd in match set_params_hdw; normalize nodelta
187    whd in match restore_hdws; normalize nodelta @(All_map … (All_True …))
188    #a #_ %
189  ]
190qed.
191
192definition fetch_result :
193  ∀globals.list register →
194  Σl : list (joint_seq ERTL globals).
195  All (joint_seq ??) (λs.step_labels ?? s = [ ]) l ≝
196  λglobals,ret_regs.
197  match reduce_strong ?? RegisterSTS RegisterRets with
198  [ mk_Sig crl crl_proof ⇒
199    let commonl ≝ \fst (\fst crl) in
200    let commonr ≝ \fst (\snd crl) in
201    map2 … (λst,r.HDW st ← HDW r) commonl commonr crl_proof @
202    match reduce_strong ?? ret_regs RegisterSTS with
203    [ mk_Sig crl crl_proof ⇒
204      let commonl ≝ \fst (\fst crl) in
205      let commonr ≝ \fst (\snd crl) in
206      map2 … (λret,st.PSD ret ← HDW st) commonl commonr crl_proof
207    ]
208  ].
209@hide_prf
210@All_append
211[ @(All_map2 … (All2_True … crl_proof)) #x #y #_ %
212| cases (reduce_strong ????) #l #prf normalize nodelta
213  @(All_map2 … (All2_True … prf)) #x #y #_ %
214]
215qed.
216
217definition translate_step :
218  ∀globals.label → joint_step RTL globals →
219    bind_step_block ERTL globals ≝
220  λglobals.λ_.λs.
221  match s return λ_.bind_step_block ?? with
222  [ step_seq s ⇒
223    match s return λ_.bind_step_block ?? with
224    [ PUSH _ ⇒ bret … [ ] (*CSC: XXXX should not be in the syntax *)
225    | POP _ ⇒ bret … [ ] (*CSC: XXXX should not be in the syntax *)
226    | MOVE rs ⇒ bret … [PSD (\fst rs) ← \snd rs]
227    | ADDRESS x prf r1 r2 ⇒
228      bret … [ADDRESS ERTL ? x prf r1 r2]
229    | OPACCS op destr1 destr2 srcr1 srcr2 ⇒
230      bret … [OPACCS ERTL ? op destr1 destr2 srcr1 srcr2]
231    | OP1 op1 destr srcr ⇒
232      bret … [OP1 ERTL ? op1 destr srcr]
233    | OP2 op2 destr srcr1 srcr2 ⇒
234      bret … [OP2 ERTL ? op2 destr srcr1 srcr2]
235    | CLEAR_CARRY ⇒
236      bret … [CLEAR_CARRY ??]
237    | SET_CARRY ⇒
238      bret … [SET_CARRY ??]
239    | LOAD destr addr1 addr2 ⇒
240      bret … [LOAD ERTL ? destr addr1 addr2]
241    | STORE addr1 addr2 srcr ⇒
242      bret … [STORE ERTL ? addr1 addr2 srcr]
243    | COMMENT msg ⇒
244      bret … [COMMENT … msg]
245    | extension_seq ext ⇒
246      match ext return λ_.bind_step_block ?? with
247      [ rtl_stack_address addr1 addr2 ⇒
248        bret … [ PSD addr1 ← HDW RegisterSPL ; PSD addr2 ← HDW RegisterSPH ]
249      ]
250    ]
251  | COST_LABEL lbl ⇒
252    bret … 〈[ ], λ_.COST_LABEL ERTL ? lbl, [ ]〉
253  | CALL f args ret_regs ⇒
254    ! pref ← pi1 … (set_params ? args) ;
255    bret ? (step_block ??) 〈add_dummy_variance … pref,
256             λ_.CALL ERTL ? f (|args|) it,
257             fetch_result ? ret_regs〉
258  | COND r ltrue ⇒
259    bret … 〈[ ], λ_.COND ERTL ? r ltrue, [ ]〉
260  ].
261
262definition translate_fin_step :
263  ∀globals.list register → register → register → list (register × Register) →
264    label → joint_fin_step RTL →
265    bind_fin_block ERTL globals ≝
266  λglobals.λret_regs,ral,rah,to_restore.λ_.λs.
267  match s return λ_.bind_fin_block ERTL ? with
268  [ GOTO lbl' ⇒ bret … 〈[ ], GOTO … lbl'〉
269  | RETURN ⇒ bret … 〈epilogue … ret_regs ral rah to_restore, RETURN ?〉
270  | TAILCALL b _ _ ⇒ match b in False with [ ]
271  ].
272
273definition allocate_regs :
274  ∀X : Type[0].
275  (register → register → list (register×Register) → bind_new register X) →
276  bind_new register X ≝
277  λX,f.
278  νral,rah in
279  let allocate_regs_internal ≝
280    λacc : bind_new register (list (register × Register)).
281    λr: Register.
282    ! tl ← acc ;
283    νr' in return (〈r', r〉 :: tl) in
284  ! to_save ← foldl ?? allocate_regs_internal (return [ ]) RegisterCalleeSaved ;
285  f ral rah to_save.
286
287definition translate_data :
288 ∀globals.joint_closed_internal_function RTL globals →
289 bind_new register (b_graph_translate_data RTL ERTL globals) ≝
290λglobals,def.
291let params ≝ joint_if_params … def in
292let new_stacksize ≝
293  joint_if_stacksize … def + (|params| - |RegisterParams|) in
294allocate_regs …
295  (λral,rah,to_save.
296    ! prologue ← prologue globals params ral rah to_save ;
297    return mk_b_graph_translate_data RTL ERTL globals
298    (* init_ret ≝ *) it
299    (* init_params ≝ *) (|params|)
300    (* init_stack_size ≝ *) new_stacksize
301    (* added_prologue ≝ *) prologue
302    (* f_step ≝ *) (translate_step globals)
303    (* f_fin ≝ *) (translate_fin_step globals (joint_if_result … def) ral rah to_save)
304    ???).
305@hide_prf
306[ #l #c % ]
307#l *
308[ #l whd %{I} %{I} %1 %
309| whd %{I} cases (epilogue ?????) @All_mp #s #EQ whd >EQ %
310| *
311| #c %{I} %{I} #l %
312| #called #args #dest @(mp_bind … (BindNewP …))
313  [2: @(pi2 ? (λ_.?)) |*:] #l1 #H1 whd % [%]
314    [ @(All_map … H1) #a #EQ #l whd >EQ %
315    | #l %
316    | cases (fetch_result ??) @All_mp #s #EQ whd >EQ %
317    ]
318| #a #l_true whd %{I} %{I} #l %{I} %2 %1 %
319| * try #a try #b try #c try #d try #e whd
320  try (%{I} %{I} #l %)
321  cases a -a #a #b whd %{I} % [ %{I} ] #l %
322]
323qed.
324
325(* removing this because of how insert_prologue is now defined
326definition generate ≝
327  λglobals.
328  λstmt.
329  λdef: joint_internal_function globals ERTL.
330  let 〈entry, def〉 ≝ fresh_label … def in
331  let graph ≝ add … (joint_if_code … def) entry stmt in
332   set_joint_if_graph … (ERTL globals) graph def ??.
333  [ (*% [ @entry | @graph_add ]*) cases daemon (*CSC: XXX *)
334  | (*cases (joint_if_exit … def) #LBL #LBL_PRF % [ @LBL | @graph_add_lookup @LBL_PRF
335    *) cases daemon (*CSC: XXX *)
336  ]
337qed.
338
339let rec find_and_remove_first_cost_label_internal (globals: list ident)
340  (def: ertl_internal_function globals) (lbl: label) (num_nodes: nat)
341    on num_nodes ≝
342  match num_nodes with
343  [ O ⇒ 〈None ?, def〉
344  | S num_nodes' ⇒
345    match lookup … (joint_if_code … def) lbl with
346    [ None ⇒ 〈None ?, def〉
347    | Some stmt ⇒
348      match stmt with
349      [ sequential inst lbl ⇒
350         match inst with
351          [ COST_LABEL cost_lbl ⇒
352             〈Some … cost_lbl, add_graph ERTL1 globals lbl (GOTO … lbl) def〉
353          | _ ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ]
354      | RETURN ⇒ 〈None …, def〉
355      | GOTO lbl ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes'
356      ]]].
357   
358definition find_and_remove_first_cost_label ≝
359  λglobals,def. 
360    find_and_remove_first_cost_label_internal globals def (joint_if_entry … def) (graph_num_nodes ? (joint_if_code … def)).
361
362definition move_first_cost_label_up_internal ≝
363  λglobals,def.
364  let 〈cost_label, def〉 ≝ find_and_remove_first_cost_label … def in
365  match cost_label with
366  [ None ⇒ def
367  | Some cost_label ⇒ generate … (sequential ERTL_ globals (COST_LABEL … cost_label) (joint_if_entry … def)) def
368  ].
369
370definition translate_funct ≝ λglobals,def. (move_first_cost_label_up_internal … (translate_funct_internal globals def)).
371*)
372
373definition rtl_to_ertl : rtl_program → ertl_program ≝
374  b_graph_transform_program … translate_data.
Note: See TracBrowser for help on using the repository browser.