source: src/RTL/RTLToERTL.ma @ 2862

Last change on this file since 2862 was 2862, checked in by sacerdot, 7 years ago

Repaired, a reverse was enough.

File size: 13.7 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.register → register → register → list register →
40  list (joint_seq ERTL globals) ≝
41  λglobals.
42  λtmpr,addr1,addr2,params.
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,tmpr,addr1,addr2,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 … tmpr addr1 addr2 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 → register → register → register →
133  list (register×Register) →
134  bind_new register (list (joint_seq ERTL globals)) ≝
135  λglobals,params,sral,srah,tmpr,addr1,addr2,sregs.
136  [ (ertl_new_frame : joint_seq ??) ;
137    POP … sral ;
138    POP … srah
139  ] @ save_hdws … sregs @ get_params … tmpr addr1 addr2 params.
140
141definition set_params_hdw :
142  ∀globals.list psd_argument → list (joint_seq ERTL globals) ≝
143  λglobals,params.
144  restore_hdws globals (zip_pottier ? ? params RegisterParams).
145
146(* Paolo: The following can probably be done way more efficiently with INC DPTR *)
147
148definition set_param_stack :
149  ∀globals.register → register → psd_argument →
150  list (joint_seq ERTL globals) ≝
151  λglobals,addr1,addr2,arg.
152  [ STORE … addr1 addr2 arg ;
153    addr1 ← addr1 .Add. (int_size : Byte) ;
154    addr2 ← addr2 .Addc. zero_byte
155  ].
156
157definition set_params_stack :
158  ∀globals.list psd_argument → bind_new register ? ≝
159  λglobals,params.
160  νaddr1,addr2 in
161  let params_length_byte : Byte ≝ bitvector_of_nat ? (|params|) in
162  [ PSD addr1 ← HDW RegisterSPL ;
163    PSD addr2 ← HDW RegisterSPH ;
164    CLEAR_CARRY ?? ;
165    addr1 ← addr1 .Sub. params_length_byte ;
166    addr2 ← addr2 .Sub. zero_byte
167  ] @
168  flatten … (map … (set_param_stack globals addr1 addr2) params).
169
170definition set_params :
171  ∀globals.list psd_argument →
172  Σb : bind_new register (list (joint_seq ERTL globals)).
173  BindNewP … (All (joint_seq ??) (λs.step_labels … s = [ ])) b ≝
174  λglobals,params.
175  let n ≝ min (|params|) (|RegisterParams|) in
176  let hdw_stack_params ≝ split ? params n in
177  let hdw_params ≝ \fst hdw_stack_params in
178  let stack_params ≝ \snd hdw_stack_params in
179  set_params_hdw globals hdw_params @@ set_params_stack globals stack_params.
180@hide_prf
181  @mp_bind [3: #l1 #H1 @mp_bind [3: #l2 #H2 @(All_append … H1 H2) ] |*:]
182  [ #r1 #r2
183    %{(refl …)} %{(refl …)} %{(refl …)} %{(refl …)} %{(refl …)}
184    @All_append [ % ]
185    elim stack_params [ % ] #hd #tl #IH whd in match flatten; normalize nodelta
186    whd in match (foldr ?????); %{(refl …)} %{(refl …)} %{(refl …)} @IH
187  | whd whd in match set_params_hdw; normalize nodelta
188    whd in match restore_hdws; normalize nodelta @(All_map … (All_True …))
189    #a #_ %
190  ]
191qed.
192
193definition fetch_result :
194  ∀globals.list register →
195  Σl : list (joint_seq ERTL globals).
196  All (joint_seq ??) (λs.step_labels ?? s = [ ]) l ≝
197  λglobals,ret_regs.
198  match reduce_strong ?? RegisterSTS RegisterRets with
199  [ mk_Sig crl crl_proof ⇒
200    let commonl ≝ \fst (\fst crl) in
201    let commonr ≝ \fst (\snd crl) in
202    map2 … (λst,r.HDW st ← HDW r) commonl commonr crl_proof @
203    match reduce_strong ?? ret_regs RegisterSTS with
204    [ mk_Sig crl crl_proof ⇒
205      let commonl ≝ \fst (\fst crl) in
206      let commonr ≝ \fst (\snd crl) in
207      map2 … (λret,st.PSD ret ← HDW st) commonl commonr crl_proof
208    ]
209  ].
210@hide_prf
211@All_append
212[ @(All_map2 … (All2_True … crl_proof)) #x #y #_ %
213| cases (reduce_strong ????) #l #prf normalize nodelta
214  @(All_map2 … (All2_True … prf)) #x #y #_ %
215]
216qed.
217
218definition translate_step :
219  ∀globals.label → joint_step RTL globals →
220    bind_step_block ERTL globals ≝
221  λglobals.λ_.λs.
222  match s return λ_.bind_step_block ?? with
223  [ step_seq s ⇒
224    bret … match s return λ_.step_block ?? with
225    [ PUSH _ ⇒ [ ] (*CSC: XXXX should not be in the syntax *)
226    | POP _ ⇒ [ ] (*CSC: XXXX should not be in the syntax *)
227    | MOVE rs ⇒ [PSD (\fst rs) ← \snd rs]
228    | ADDRESS x prf r1 r2 ⇒
229      [ADDRESS ERTL ? x prf r1 r2]
230    | OPACCS op destr1 destr2 srcr1 srcr2 ⇒
231      [OPACCS ERTL ? op destr1 destr2 srcr1 srcr2]
232    | OP1 op1 destr srcr ⇒
233      [OP1 ERTL ? op1 destr srcr]
234    | OP2 op2 destr srcr1 srcr2 ⇒
235      [OP2 ERTL ? op2 destr srcr1 srcr2]
236    | CLEAR_CARRY ⇒
237      [CLEAR_CARRY ??]
238    | SET_CARRY ⇒
239      [SET_CARRY ??]
240    | LOAD destr addr1 addr2 ⇒
241      [LOAD ERTL ? destr addr1 addr2]
242    | STORE addr1 addr2 srcr ⇒
243      [STORE ERTL ? addr1 addr2 srcr]
244    | COMMENT msg ⇒
245      [COMMENT … msg]
246    | extension_seq ext ⇒
247      match ext return λ_.step_block ?? with
248      [ rtl_stack_address addr1 addr2 ⇒
249        [ PSD addr1 ← HDW RegisterSPL ; PSD addr2 ← HDW RegisterSPH ]
250      ]
251    ]
252  | COST_LABEL lbl ⇒
253    bret … 〈[ ], λ_.COST_LABEL ERTL ? lbl, [ ]〉
254  | CALL f args ret_regs ⇒
255    ! pref ← pi1 … (set_params ? args) ;
256    bret ? (step_block ??) 〈add_dummy_variance … pref,
257             λ_.CALL ERTL ? f (|args|) it,
258             fetch_result ? ret_regs〉
259  | COND r ltrue ⇒
260    bret … 〈[ ], λ_.COND ERTL ? r ltrue, [ ]〉
261  ].
262
263definition translate_fin_step :
264  ∀globals.list register → register → register → list (register × Register) →
265    label → joint_fin_step RTL →
266    bind_fin_block ERTL globals ≝
267  λglobals.λret_regs,ral,rah,to_restore.λ_.λs.
268  match s return λ_.bind_fin_block ERTL ? with
269  [ GOTO lbl' ⇒ bret … 〈[ ], GOTO … lbl'〉
270  | RETURN ⇒ bret … 〈epilogue … ret_regs ral rah to_restore, RETURN ?〉
271  | TAILCALL b _ _ ⇒ match b in False with [ ]
272  ].
273
274definition allocate_regs :
275  ∀X : Type[0].
276  (list (register×Register) → bind_new register X) →
277  bind_new register X ≝
278  λX,f.
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 to_save.
286
287definition translate_data :
288 ∀globals.joint_closed_internal_function RTL globals →
289 bound_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  (λto_save.
296    νral,rah,tmpr,addr1,addr2 in
297    ! prologue ← prologue globals params ral rah tmpr addr1 addr2 to_save ;
298    return mk_b_graph_translate_data RTL ERTL globals
299    (* init_ret ≝ *) it
300    (* init_params ≝ *) (|params|)
301    (* init_stack_size ≝ *) new_stacksize
302    (* added_prologue ≝ *) prologue
303    (* new_regs ≝ *) (reverse … (addr2 :: addr1 :: tmpr :: rah :: ral :: map … (λx.\fst x) to_save))
304    (* f_step ≝ *) (translate_step globals)
305    (* f_fin ≝ *) (translate_fin_step globals (joint_if_result … def) ral rah to_save)
306    ????).
307@hide_prf
308[1,2: cases daemon (* TODO *)
309| #l #c %
310| #l * [ #c' | #f #args #dest | #a #ltrue | #s ] #c whd
311  [2: #r1 #r2 ] whd #l' #EQ destruct try %
312  cases s in EQ; whd in match ensure_step_block; normalize nodelta
313  try #a try #b try #c try #d try #e try #f destruct
314  cases a in b; #a1 #a2 normalize nodelta #EQ destruct
315| #r1 #r2 #r3 #r4 #r5 #r6 #r7 #r8 #ral #rah #tmpr #addr1 #addr2
316% (* XXX: FAILS, unintentional list reversal??? *)
317]
318(* #l *
319[ #l whd %{I} %{I} %1 %
320| whd %{I} cases (epilogue ?????) @All_mp #s #EQ whd >EQ %
321| *
322| #c %{I} %{I} #l %
323| #called #args #dest @(mp_bind … (BindNewP …))
324  [2: @(pi2 ? (λ_.?)) |*:] #l1 #H1 whd % [%]
325    [ @(All_map … H1) #a #EQ #l whd >EQ %
326    | #l %
327    | cases (fetch_result ??) @All_mp #s #EQ whd >EQ %
328    ]
329| #a #l_true whd %{I} %{I} #l %{I} %2 %1 %
330| * try #a try #b try #c try #d try #e whd
331  try (%{I} %{I} #l %)
332  cases a -a #a #b whd %{I} % [ %{I} ] #l %
333]*)
334qed.
335
336(* removing this because of how insert_prologue is now defined
337definition generate ≝
338  λglobals.
339  λstmt.
340  λdef: joint_internal_function globals ERTL.
341  let 〈entry, def〉 ≝ fresh_label … def in
342  let graph ≝ add … (joint_if_code … def) entry stmt in
343   set_joint_if_graph … (ERTL globals) graph def ??.
344  [ (*% [ @entry | @graph_add ]*) cases daemon (*CSC: XXX *)
345  | (*cases (joint_if_exit … def) #LBL #LBL_PRF % [ @LBL | @graph_add_lookup @LBL_PRF
346    *) cases daemon (*CSC: XXX *)
347  ]
348qed.
349
350let rec find_and_remove_first_cost_label_internal (globals: list ident)
351  (def: ertl_internal_function globals) (lbl: label) (num_nodes: nat)
352    on num_nodes ≝
353  match num_nodes with
354  [ O ⇒ 〈None ?, def〉
355  | S num_nodes' ⇒
356    match lookup … (joint_if_code … def) lbl with
357    [ None ⇒ 〈None ?, def〉
358    | Some stmt ⇒
359      match stmt with
360      [ sequential inst lbl ⇒
361         match inst with
362          [ COST_LABEL cost_lbl ⇒
363             〈Some … cost_lbl, add_graph ERTL1 globals lbl (GOTO … lbl) def〉
364          | _ ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ]
365      | RETURN ⇒ 〈None …, def〉
366      | GOTO lbl ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes'
367      ]]].
368   
369definition find_and_remove_first_cost_label ≝
370  λglobals,def. 
371    find_and_remove_first_cost_label_internal globals def (joint_if_entry … def) (graph_num_nodes ? (joint_if_code … def)).
372
373definition move_first_cost_label_up_internal ≝
374  λglobals,def.
375  let 〈cost_label, def〉 ≝ find_and_remove_first_cost_label … def in
376  match cost_label with
377  [ None ⇒ def
378  | Some cost_label ⇒ generate … (sequential ERTL_ globals (COST_LABEL … cost_label) (joint_if_entry … def)) def
379  ].
380
381definition translate_funct ≝ λglobals,def. (move_first_cost_label_up_internal … (translate_funct_internal globals def)).
382*)
383
384definition rtl_to_ertl : rtl_program → ertl_program ≝
385  b_graph_transform_program … translate_data.
Note: See TracBrowser for help on using the repository browser.