source: src/RTL/RTLToERTL.ma @ 3255

Last change on this file since 3255 was 3255, checked in by tranquil, 7 years ago
  • dropped newframe and delframe (to be integrated in calls and returns

in the semantics), as they were too wild for the proof of ERTL to LTL

  • ERTL now has a policy on what hardware registers can be written or

read

  • Rearranged special hardware registers: dropped STS, ST2 and ST3, and

moved DPL and DPH out of RegistersRets?

File size: 15.0 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
30definition 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 → list (register × (Σr.?)) →
123  Σl : list (joint_seq ERTL globals).
124  All (joint_seq ??) (λs.step_labels ?? s = [ ]) l ≝
125  λglobals,ret_regs,sral,srah,sregs.
126  restore_hdws … (map ?? (λx.〈Reg ? (\fst x), \snd x〉) sregs) @
127  assign_result globals ret_regs @
128  [ PUSH ERTL ? sral ;
129    PUSH … srah ].
130@hide_prf
131@All_append
132[ @(All_map … (All_True …)) #x #_ %
133| @All_append
134  [ whd in match assign_result;
135    generalize in match reduce_strong; #f normalize nodelta
136    cases (f ????) #l #prf normalize nodelta
137    @All_append
138    [ @(All_map2 … (All2_True … prf)) #x #y #_ %
139    | @(All_map … (All_True …)) #x #_ %
140    ]
141  | %%%
142  ]
143]
144qed.
145
146definition prologue :
147  ∀globals.list register → register → register → register → register → register →
148  list (register×(Σr.?)) →
149  bind_new register (list (joint_seq ERTL globals)) ≝
150  λglobals,params,sral,srah,tmpr,addr1,addr2,sregs.
151  [ POP … srah ;
152    POP … sral
153  ] @ save_hdws … sregs @ get_params … tmpr addr1 addr2 params.
154
155definition set_params_hdw :
156  ∀globals.list psd_argument → list (joint_seq ERTL globals) ≝
157  λglobals,params.
158  restore_hdws globals (zip_pottier ? ? params RegisterParamsSig).
159
160definition set_param_stack :
161  ∀globals.register → register → psd_argument →
162  list (joint_seq ERTL globals) ≝
163  λglobals,addr1,addr2,arg.
164  [ STORE … addr1 addr2 arg ;
165    addr1 ← addr1 .Add. (int_size : Byte) ;
166    addr2 ← addr2 .Addc. zero_byte
167  ].
168
169definition set_params_stack :
170  ∀globals.list psd_argument → bind_new register ? ≝
171  λglobals,params.
172  νaddr1,addr2 in
173  let params_length_byte : Byte ≝ bitvector_of_nat ? (|params|) in
174  [ PSD addr1 ← HDW RegisterSPL ;
175    PSD addr2 ← HDW RegisterSPH ;
176    CLEAR_CARRY ?? ;
177    addr1 ← addr1 .Sub. params_length_byte ;
178    addr2 ← addr2 .Sub. zero_byte
179  ] @
180  flatten … (map … (set_param_stack globals addr1 addr2) params). % qed.
181
182definition set_params :
183  ∀globals.list psd_argument →
184  Σb : bind_new register (list (joint_seq ERTL globals)).
185  BindNewP … (All (joint_seq ??) (λs.step_labels … s = [ ])) b ≝
186  λglobals,params.
187  let n ≝ min (|params|) (|RegisterParamsSig|) in
188  let hdw_stack_params ≝ split ? params n in
189  let hdw_params ≝ \fst hdw_stack_params in
190  let stack_params ≝ \snd hdw_stack_params in
191  set_params_hdw globals hdw_params @@ set_params_stack globals stack_params.
192@hide_prf
193  @mp_bind [3: #l1 #H1 @mp_bind [3: #l2 #H2 @(All_append … H1 H2) ] |*:]
194  [ #r1 #r2
195    %{(refl …)} %{(refl …)} %{(refl …)} %{(refl …)} %{(refl …)}
196    @All_append [ % ]
197    elim stack_params [ % ] #hd #tl #IH whd in match flatten; normalize nodelta
198    whd in match (foldr ?????); %{(refl …)} %{(refl …)} %{(refl …)} @IH
199  | whd whd in match set_params_hdw; normalize nodelta
200    whd in match restore_hdws; normalize nodelta @(All_map … (All_True …))
201    #a #_ %
202  ]
203qed.
204
205definition fetch_result :
206  ∀globals.list register →
207  Σl : list (joint_seq ERTL globals).
208  All (joint_seq ??) (λs.step_labels ?? s = [ ]) l ≝
209  λglobals,ret_regs.
210  match reduce_strong ?? ret_regs RegisterRetsSig with
211  [ mk_Sig crl crl_proof ⇒
212    let commonl ≝ \fst (\fst crl) in
213    let commonr ≝ \fst (\snd crl) in
214    map2 … (λr.λR : Σr.?.PSD r ← HDW R) commonl commonr crl_proof
215  ].
216@hide_prf [2: % |3: @(π1 (pi2 … R)) ]
217@(All_map2 … (All2_True … crl_proof)) #x #y #_ %
218qed.
219
220definition translate_step :
221  ∀globals.label → joint_step RTL globals →
222    bind_step_block ERTL globals ≝
223  λglobals.λ_.λs.
224  match s return λ_.bind_step_block ?? with
225  [ step_seq s ⇒
226    bret … match s return λ_.step_block ?? with
227    [ PUSH _ ⇒ [ ] (*CSC: XXXX should not be in the syntax *)
228    | POP _ ⇒ [ ] (*CSC: XXXX should not be in the syntax *)
229    | MOVE rs ⇒ [PSD (\fst rs) ← \snd rs]
230    | ADDRESS x prf off r1 r2 ⇒
231      [ADDRESS ERTL ? x prf off r1 r2]
232    | OPACCS op destr1 destr2 srcr1 srcr2 ⇒
233      [OPACCS ERTL ? op destr1 destr2 srcr1 srcr2]
234    | OP1 op1 destr srcr ⇒
235      [OP1 ERTL ? op1 destr srcr]
236    | OP2 op2 destr srcr1 srcr2 ⇒
237      [OP2 ERTL ? op2 destr srcr1 srcr2]
238    | CLEAR_CARRY ⇒
239      [CLEAR_CARRY ??]
240    | SET_CARRY ⇒
241      [SET_CARRY ??]
242    | LOAD destr addr1 addr2 ⇒
243      [LOAD ERTL ? destr addr1 addr2]
244    | STORE addr1 addr2 srcr ⇒
245      [STORE ERTL ? addr1 addr2 srcr]
246    | COMMENT msg ⇒
247      [COMMENT … msg]
248    | extension_seq ext ⇒
249      match ext return λ_.step_block ?? with
250      [ rtl_stack_address addr1 addr2 ⇒
251        [ PSD addr1 ← HDW RegisterSPL ; PSD addr2 ← HDW RegisterSPH ]
252      ]
253    ]
254  | COST_LABEL lbl ⇒
255    bret … 〈[ ], λ_.COST_LABEL ERTL ? lbl, [ ]〉
256  | CALL f args ret_regs ⇒
257    ! pref ← pi1 … (set_params ? args) ;
258    bret ? (step_block ??) 〈add_dummy_variance … pref,
259             λ_.CALL ERTL ? f (|args|) it,
260             fetch_result ? ret_regs〉
261  | COND r ltrue ⇒
262    bret … 〈[ ], λ_.COND ERTL ? r ltrue, [ ]〉
263  ]. % qed.
264
265definition translate_fin_step :
266  ∀globals.list register → register → register → list (register × (Σr.?)) →
267    label → joint_fin_step RTL →
268    bind_fin_block ERTL globals ≝
269  λglobals.λret_regs,ral,rah,to_restore.λ_.λs.
270  match s return λ_.bind_fin_block ERTL ? with
271  [ GOTO lbl' ⇒ bret … 〈[ ], GOTO … lbl'〉
272  | RETURN ⇒ bret … 〈epilogue … ret_regs ral rah to_restore, RETURN ?〉
273  | TAILCALL b _ _ ⇒ match b in False with [ ]
274  ].
275
276definition allocate_regs :
277  ∀X : Type[0].
278  (list (register×(Σr.?)) → bind_new register X) →
279  bind_new register X ≝
280  λX,f.
281  let allocate_regs_internal ≝
282    λacc : bind_new register (list (register × (Σr.?))).
283    λr: Σr.?.
284    ! tl ← acc ;
285    νr' in return (〈r', r〉 :: tl) in
286  ! to_save ← foldl ?? allocate_regs_internal (return [ ]) RegisterCalleeSavedSig ;
287  f to_save.
288
289definition translate_data :
290 ∀globals.joint_closed_internal_function RTL globals →
291 bound_b_graph_translate_data RTL ERTL globals ≝
292λglobals,def.
293let params ≝ joint_if_params … def in
294let new_stacksize ≝
295  joint_if_stacksize … def + (|params| - |RegisterParams|) in
296allocate_regs ?
297  (λto_save.
298    νral,rah,tmpr,addr1,addr2 in
299    ! prologue ← prologue globals params ral rah tmpr addr1 addr2 to_save ;
300    return mk_b_graph_translate_data RTL ERTL globals
301    (* init_ret ≝ *) it
302    (* init_params ≝ *) (|params|)
303    (* init_stack_size ≝ *) new_stacksize
304    (* added_prologue ≝ *) prologue
305    (* new_regs ≝ *) (reverse … (addr2 :: addr1 :: tmpr :: rah :: ral :: map … (λx.\fst x) to_save))
306    (* f_step ≝ *) (translate_step globals)
307    (* f_fin ≝ *) (translate_fin_step globals (joint_if_result … def) ral rah to_save)
308    ????).
309@hide_prf
310[1,2: cases daemon (* TODO *)
311| #l #c %
312| #l * [ #c' | #f #args #dest | #a #ltrue | #s ] #c whd
313  [2: #r1 #r2 ] whd #l' #EQ destruct try %
314  cases s in EQ; whd in match ensure_step_block; normalize nodelta
315  try #a try #b try #c try #d try #e try #f destruct
316  cases a in b; #a1 #a2 normalize nodelta #EQ destruct
317| #r1 #r2 #r3 #r4 #r5 #r6 #r7 #r8 #ral #rah #tmpr #addr1 #addr2 %
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.