source: src/RTL/RTLToERTL.ma @ 3145

Last change on this file since 3145 was 3145, checked in by tranquil, 7 years ago
  • removed sigma types from traces of intensional events
  • completed correctness.ma using axiom files, a single daemon remains
File size: 14.8 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×Register) → list (joint_seq ERTL globals) ≝
12 λglobals.
13  let save_hdws_internal ≝
14   λdestr_srcr.PSD (\fst destr_srcr) ← HDW (\snd destr_srcr) in
15  map ?? save_hdws_internal.
16
17definition restore_hdws :
18  ∀globals.list (psd_argument×Register) → list (joint_seq ERTL globals) ≝
19  λglobals.
20   let restore_hdws_internal ≝
21    λdestr_srcr:psd_argument×?.HDW (\snd destr_srcr) ← \fst destr_srcr in
22    map ? ? restore_hdws_internal.
23
24definition get_params_hdw :
25  ∀globals.list register → list (joint_seq ERTL globals) ≝
26  λglobals,params.
27  save_hdws … (zip_pottier … params RegisterParams).
28
29definition get_param_stack :
30  ∀globals.register → register → register →
31  list (joint_seq ERTL globals) ≝
32  λglobals,addr1,addr2,destr.
33  (* liveness analysis will erase the last useless ops *)
34  [ LOAD ?? destr addr1 addr2 ;
35    addr1 ← addr1 .Add. (int_size : Byte) ;
36    addr2 ← addr2 .Addc. zero_byte
37  ].
38
39definition get_params_stack :
40  ∀globals.register → register → register → list register →
41  list (joint_seq ERTL globals) ≝
42  λglobals.
43  λtmpr,addr1,addr2,params.
44  let params_length_byte : Byte ≝ bitvector_of_nat ? (|params|) in
45  [ (ertl_frame_size tmpr : joint_seq ??) ;
46    CLEAR_CARRY ?? ;
47    tmpr ← tmpr .Sub. params_length_byte ; (* will be constant later *)
48    PSD addr1 ← HDW RegisterSPL ;
49    PSD addr2 ← HDW RegisterSPH ;
50    addr1 ← addr1 .Add. tmpr ;
51    addr2 ← addr2 .Addc. zero_byte ] @   
52  flatten … (map ?? (get_param_stack globals addr1 addr2) params).
53
54definition get_params ≝
55  λglobals,tmpr,addr1,addr2,params.
56  let n ≝ min (length … params) (length … RegisterParams) in
57  let 〈hdw_params, stack_params〉 ≝ list_split … n params in
58  get_params_hdw globals hdw_params @ get_params_stack … tmpr addr1 addr2 stack_params.
59
60definition save_return :
61  ∀globals.list psd_argument → list (joint_seq ERTL globals) ≝
62  λglobals,ret_regs.
63  match reduce_strong ? ? RegisterSTS ret_regs with
64  [ mk_Sig crl crl_proof ⇒
65    let commonl ≝ \fst (\fst crl) in
66    let commonr ≝ \fst (\snd crl) in
67    let restl ≝ \snd (\fst crl) in
68    (* let restr ≝ \snd (\snd crl) in *)
69    map2 … (λst.λr : psd_argument.HDW st ← r) commonl commonr crl_proof @
70    map … (λst.HDW st ← zero_byte) restl
71  ].
72
73definition assign_result : ∀globals.list (joint_seq ERTL globals) ≝
74  λglobals.
75  match reduce_strong ?? RegisterRets RegisterSTS with
76  [ mk_Sig crl crl_proof ⇒
77    let commonl ≝ \fst (\fst crl) in
78    let commonr ≝ \fst (\snd crl) in
79    map2 … (λret,st.HDW ret ← HDW st) commonl commonr crl_proof
80  ].
81
82lemma All_map2 : ∀A,B,C,P,R,f,l1,l2,prf.
83 All2 A B P l1 l2 →
84 (∀x,y.P x y → R (f x y)) →
85 All C R (map2 A B C f l1 l2 prf).
86#A #B #C #P #R #f #l1 elim l1 -l1
87[ * [ #prf * #H % ] #hd' #tl'
88| #hd #tl #IH * [2: #hd' #tl' ]
89] #prf normalize in prf; destruct
90* #H1 #H2 #H % [ @H @H1 | @IH assumption ] qed.
91
92lemma All2_True : ∀A,B,l1,l2.|l1| = |l2| → All2 A B (λ_.λ_.True) l1 l2.
93#A #B #l1 elim l1 -l1
94[ * [ #prf % ] #hd' #tl'
95| #hd #tl #IH * [2: #hd' #tl' ]
96] #prf normalize in prf; destruct %{I} @IH assumption
97qed.
98
99lemma All_True : ∀A,l.All A (λ_.True) l.
100#A #l elim l -l [ % | #hd #tl #IH %{I IH} ] qed.
101
102definition epilogue :
103  ∀globals.list register → register → register → list (register × Register) →
104  Σl : list (joint_seq ERTL globals).
105  All (joint_seq ??) (λs.step_labels ?? s = [ ]) l ≝
106  λglobals,ret_regs,sral,srah,sregs.
107  save_return … (map … (Reg ?) ret_regs) @
108  restore_hdws … (map … (λpr.〈Reg ? (\fst pr),\snd pr〉) sregs) @
109  [ PUSH ERTL ? sral ;
110    PUSH … srah ;
111    ertl_del_frame ] @
112  assign_result globals.
113@hide_prf
114@All_append
115[ whd in match save_return; normalize nodelta
116  cases (reduce_strong ????) ** #a #b * #c #d #prf normalize nodelta
117  @All_append
118  [ @(All_map2 … (All2_True … prf)) #x #y #_ %
119  | @(All_map … (All_True …)) #x #_ %
120  ]
121| @All_append
122  [ @(All_map … (All_True …)) #x #_ %
123  | %{(refl …)} %{(refl …)} %{(refl …)}
124    whd in match assign_result;
125    generalize in match reduce_strong; #f normalize nodelta
126    cases (f ????) #l #prf normalize nodelta
127    @(All_map2 … (All2_True … prf)) #x #y #_ %
128  ]
129]
130qed.
131
132definition prologue :
133  ∀globals.list register → register → register → register → register → register →
134  list (register×Register) →
135  bind_new register (list (joint_seq ERTL globals)) ≝
136  λglobals,params,sral,srah,tmpr,addr1,addr2,sregs.
137  [ (ertl_new_frame : joint_seq ??) ;
138    POP … srah ;
139    POP … sral
140  ] @ save_hdws … sregs @ get_params … tmpr addr1 addr2 params.
141
142definition set_params_hdw :
143  ∀globals.list psd_argument → list (joint_seq ERTL globals) ≝
144  λglobals,params.
145  restore_hdws globals (zip_pottier ? ? params RegisterParams).
146
147(* Paolo: The following can probably be done way more efficiently with INC DPTR *)
148
149definition set_param_stack :
150  ∀globals.register → register → psd_argument →
151  list (joint_seq ERTL globals) ≝
152  λglobals,addr1,addr2,arg.
153  [ STORE … addr1 addr2 arg ;
154    addr1 ← addr1 .Add. (int_size : Byte) ;
155    addr2 ← addr2 .Addc. zero_byte
156  ].
157
158definition set_params_stack :
159  ∀globals.list psd_argument → bind_new register ? ≝
160  λglobals,params.
161  νaddr1,addr2 in
162  let params_length_byte : Byte ≝ bitvector_of_nat ? (|params|) in
163  [ PSD addr1 ← HDW RegisterSPL ;
164    PSD addr2 ← HDW RegisterSPH ;
165    CLEAR_CARRY ?? ;
166    addr1 ← addr1 .Sub. params_length_byte ;
167    addr2 ← addr2 .Sub. zero_byte
168  ] @
169  flatten … (map … (set_param_stack globals addr1 addr2) params).
170
171definition set_params :
172  ∀globals.list psd_argument →
173  Σb : bind_new register (list (joint_seq ERTL globals)).
174  BindNewP … (All (joint_seq ??) (λs.step_labels … s = [ ])) b ≝
175  λglobals,params.
176  let n ≝ min (|params|) (|RegisterParams|) in
177  let hdw_stack_params ≝ split ? params n in
178  let hdw_params ≝ \fst hdw_stack_params in
179  let stack_params ≝ \snd hdw_stack_params in
180  set_params_hdw globals hdw_params @@ set_params_stack globals stack_params.
181@hide_prf
182  @mp_bind [3: #l1 #H1 @mp_bind [3: #l2 #H2 @(All_append … H1 H2) ] |*:]
183  [ #r1 #r2
184    %{(refl …)} %{(refl …)} %{(refl …)} %{(refl …)} %{(refl …)}
185    @All_append [ % ]
186    elim stack_params [ % ] #hd #tl #IH whd in match flatten; normalize nodelta
187    whd in match (foldr ?????); %{(refl …)} %{(refl …)} %{(refl …)} @IH
188  | whd whd in match set_params_hdw; normalize nodelta
189    whd in match restore_hdws; normalize nodelta @(All_map … (All_True …))
190    #a #_ %
191  ]
192qed.
193
194definition fetch_result :
195  ∀globals.list register →
196  Σl : list (joint_seq ERTL globals).
197  All (joint_seq ??) (λs.step_labels ?? s = [ ]) l ≝
198  λglobals,ret_regs.
199  match reduce_strong ?? RegisterSTS RegisterRets with
200  [ mk_Sig crl crl_proof ⇒
201    let commonl ≝ \fst (\fst crl) in
202    let commonr ≝ \fst (\snd crl) in
203    map2 … (λst,r.HDW st ← HDW r) commonl commonr crl_proof @
204    match reduce_strong ?? ret_regs RegisterSTS with
205    [ mk_Sig crl crl_proof ⇒
206      let commonl ≝ \fst (\fst crl) in
207      let commonr ≝ \fst (\snd crl) in
208      map2 … (λret,st.PSD ret ← HDW st) commonl commonr crl_proof
209    ]
210  ].
211@hide_prf
212@All_append
213[ @(All_map2 … (All2_True … crl_proof)) #x #y #_ %
214| cases (reduce_strong ????) #l #prf normalize nodelta
215  @(All_map2 … (All2_True … prf)) #x #y #_ %
216]
217qed.
218
219definition translate_step :
220  ∀globals.label → joint_step RTL globals →
221    bind_step_block ERTL globals ≝
222  λglobals.λ_.λs.
223  match s return λ_.bind_step_block ?? with
224  [ step_seq s ⇒
225    bret … match s return λ_.step_block ?? with
226    [ PUSH _ ⇒ [ ] (*CSC: XXXX should not be in the syntax *)
227    | POP _ ⇒ [ ] (*CSC: XXXX should not be in the syntax *)
228    | MOVE rs ⇒ [PSD (\fst rs) ← \snd rs]
229    | ADDRESS x prf off r1 r2 ⇒
230      [ADDRESS ERTL ? x prf off r1 r2]
231    | OPACCS op destr1 destr2 srcr1 srcr2 ⇒
232      [OPACCS ERTL ? op destr1 destr2 srcr1 srcr2]
233    | OP1 op1 destr srcr ⇒
234      [OP1 ERTL ? op1 destr srcr]
235    | OP2 op2 destr srcr1 srcr2 ⇒
236      [OP2 ERTL ? op2 destr srcr1 srcr2]
237    | CLEAR_CARRY ⇒
238      [CLEAR_CARRY ??]
239    | SET_CARRY ⇒
240      [SET_CARRY ??]
241    | LOAD destr addr1 addr2 ⇒
242      [LOAD ERTL ? destr addr1 addr2]
243    | STORE addr1 addr2 srcr ⇒
244      [STORE ERTL ? addr1 addr2 srcr]
245    | COMMENT msg ⇒
246      [COMMENT … msg]
247    | extension_seq ext ⇒
248      match ext return λ_.step_block ?? with
249      [ rtl_stack_address addr1 addr2 ⇒
250        [ PSD addr1 ← HDW RegisterSPL ; PSD addr2 ← HDW RegisterSPH ]
251      ]
252    ]
253  | COST_LABEL lbl ⇒
254    bret … 〈[ ], λ_.COST_LABEL ERTL ? lbl, [ ]〉
255  | CALL f args ret_regs ⇒
256    ! pref ← pi1 … (set_params ? args) ;
257    bret ? (step_block ??) 〈add_dummy_variance … pref,
258             λ_.CALL ERTL ? f (|args|) it,
259             fetch_result ? ret_regs〉
260  | COND r ltrue ⇒
261    bret … 〈[ ], λ_.COND ERTL ? r ltrue, [ ]〉
262  ].
263
264definition translate_fin_step :
265  ∀globals.list register → register → register → list (register × Register) →
266    label → joint_fin_step RTL →
267    bind_fin_block ERTL globals ≝
268  λglobals.λret_regs,ral,rah,to_restore.λ_.λs.
269  match s return λ_.bind_fin_block ERTL ? with
270  [ GOTO lbl' ⇒ bret … 〈[ ], GOTO … lbl'〉
271  | RETURN ⇒ bret … 〈epilogue … ret_regs ral rah to_restore, RETURN ?〉
272  | TAILCALL b _ _ ⇒ match b in False with [ ]
273  ].
274
275definition allocate_regs :
276  ∀X : Type[0].
277  (list (register×Register) → bind_new register X) →
278  bind_new register X ≝
279  λX,f.
280  let allocate_regs_internal ≝
281    λacc : bind_new register (list (register × Register)).
282    λr: Register.
283    ! tl ← acc ;
284    νr' in return (〈r', r〉 :: tl) in
285  ! to_save ← foldl ?? allocate_regs_internal (return [ ]) RegisterCalleeSaved ;
286  f to_save.
287
288definition translate_data :
289 ∀globals.joint_closed_internal_function RTL globals →
290 bound_b_graph_translate_data RTL ERTL globals ≝
291λglobals,def.
292let params ≝ joint_if_params … def in
293let new_stacksize ≝
294  joint_if_stacksize … def + (|params| - |RegisterParams|) in
295allocate_regs ?
296  (λto_save.
297    νral,rah,tmpr,addr1,addr2 in
298    ! prologue ← prologue globals params ral rah tmpr addr1 addr2 to_save ;
299    return mk_b_graph_translate_data RTL ERTL globals
300    (* init_ret ≝ *) it
301    (* init_params ≝ *) (|params|)
302    (* init_stack_size ≝ *) new_stacksize
303    (* added_prologue ≝ *) prologue
304    (* new_regs ≝ *) (reverse … (addr2 :: addr1 :: tmpr :: rah :: ral :: map … (λx.\fst x) to_save))
305    (* f_step ≝ *) (translate_step globals)
306    (* f_fin ≝ *) (translate_fin_step globals (joint_if_result … def) ral rah to_save)
307    ????).
308@hide_prf
309[1,2: cases daemon (* TODO *)
310| #l #c %
311| #l * [ #c' | #f #args #dest | #a #ltrue | #s ] #c whd
312  [2: #r1 #r2 ] whd #l' #EQ destruct try %
313  cases s in EQ; whd in match ensure_step_block; normalize nodelta
314  try #a try #b try #c try #d try #e try #f destruct
315  cases a in b; #a1 #a2 normalize nodelta #EQ destruct
316| #r1 #r2 #r3 #r4 #r5 #r6 #r7 #r8 #ral #rah #tmpr #addr1 #addr2
317% (* XXX: FAILS, unintentional list reversal??? *)
318]
319(* #l *
320[ #l whd %{I} %{I} %1 %
321| whd %{I} cases (epilogue ?????) @All_mp #s #EQ whd >EQ %
322| *
323| #c %{I} %{I} #l %
324| #called #args #dest @(mp_bind … (BindNewP …))
325  [2: @(pi2 ? (λ_.?)) |*:] #l1 #H1 whd % [%]
326    [ @(All_map … H1) #a #EQ #l whd >EQ %
327    | #l %
328    | cases (fetch_result ??) @All_mp #s #EQ whd >EQ %
329    ]
330| #a #l_true whd %{I} %{I} #l %{I} %2 %1 %
331| * try #a try #b try #c try #d try #e whd
332  try (%{I} %{I} #l %)
333  cases a -a #a #b whd %{I} % [ %{I} ] #l %
334]*)
335qed.
336
337(* removing this because of how insert_prologue is now defined
338definition generate ≝
339  λglobals.
340  λstmt.
341  λdef: joint_internal_function globals ERTL.
342  let 〈entry, def〉 ≝ fresh_label … def in
343  let graph ≝ add … (joint_if_code … def) entry stmt in
344   set_joint_if_graph … (ERTL globals) graph def ??.
345  [ (*% [ @entry | @graph_add ]*) cases daemon (*CSC: XXX *)
346  | (*cases (joint_if_exit … def) #LBL #LBL_PRF % [ @LBL | @graph_add_lookup @LBL_PRF
347    *) cases daemon (*CSC: XXX *)
348  ]
349qed.
350
351let rec find_and_remove_first_cost_label_internal (globals: list ident)
352  (def: ertl_internal_function globals) (lbl: label) (num_nodes: nat)
353    on num_nodes ≝
354  match num_nodes with
355  [ O ⇒ 〈None ?, def〉
356  | S num_nodes' ⇒
357    match lookup … (joint_if_code … def) lbl with
358    [ None ⇒ 〈None ?, def〉
359    | Some stmt ⇒
360      match stmt with
361      [ sequential inst lbl ⇒
362         match inst with
363          [ COST_LABEL cost_lbl ⇒
364             〈Some … cost_lbl, add_graph ERTL1 globals lbl (GOTO … lbl) def〉
365          | _ ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ]
366      | RETURN ⇒ 〈None …, def〉
367      | GOTO lbl ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes'
368      ]]].
369   
370definition find_and_remove_first_cost_label ≝
371  λglobals,def. 
372    find_and_remove_first_cost_label_internal globals def (joint_if_entry … def) (graph_num_nodes ? (joint_if_code … def)).
373
374definition move_first_cost_label_up_internal ≝
375  λglobals,def.
376  let 〈cost_label, def〉 ≝ find_and_remove_first_cost_label … def in
377  match cost_label with
378  [ None ⇒ def
379  | Some cost_label ⇒ generate … (sequential ERTL_ globals (COST_LABEL … cost_label) (joint_if_entry … def)) def
380  ].
381
382definition translate_funct ≝ λglobals,def. (move_first_cost_label_up_internal … (translate_funct_internal globals def)).
383*)
384
385definition rtl_to_ertl : rtl_program → ertl_program ≝
386  b_graph_transform_program … translate_data.
387
388lemma RTLToERTL_monotone_stacksizes :
389∀p_in.let p_out ≝ rtl_to_ertl p_in in
390stack_cost_model_le (stack_cost ? p_in) (stack_cost ? p_out).
391#p_in whd
392@list_map_opt_All2
393[ @(λid_def1,id_def2.
394   match \snd id_def1 with
395   [ Internal f1 ⇒
396     match \snd id_def2 with
397     [ Internal f2 ⇒
398       \fst id_def1 = \fst id_def2 ∧
399       le (joint_if_stacksize … f1) (joint_if_stacksize … f2)
400     | _ ⇒ False
401     ]
402   | External _ ⇒ match \snd id_def2 with [ Internal _ ⇒ False | External _ ⇒ True ]
403   ])
404| * #id * #f1 * #id' * #f2 normalize nodelta [|*: * %]
405  ** #H %{H} % ]
406@All2_of_map * #id * #f normalize nodelta [2: %]
407% [%]
408cases (b_graph_translate ?????) #f_out * #data
409* *[2:#r1*[2:#r2*[2:#r3*[2:#r4*[2:#r5*[2:#r6*[2:#r7*[2:#r8*
410  [2:#r9*[2:#r10*[2:#r11*[2:#r12*[2:#r13*[2:#r14 #tl]]]]]]]]]]]]]]
411* #f_lbls * #f_regs * try ( * @False) whd in ⊢ (%→?); #EQ_data
412#props >(ss_def_out_eq … props) >EQ_data
413generalize in match (joint_if_stacksize ???); generalize in match (length ??-length ??);
414-p_in //
415qed.
Note: See TracBrowser for help on using the repository browser.