source: src/joint/TranslateUtils.ma

Last change on this file was 3263, checked in by tranquil, 6 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: 28.0 KB
Line 
1include "joint/Joint.ma".
2include "joint/blocks.ma".
3include "utilities/hide.ma".
4include "utilities/deqsets_extra.ma".
5
6(*include alias "basics/lists/list.ma".
7let rec repeat_fresh pars globals A (fresh : freshT pars globals A) (n : ℕ)
8  on n :
9  freshT pars globals (Σl : list A. |l| = n) ≝
10  match n  return λx.freshT … (Σl.|l| = x) with
11  [ O ⇒ return «[ ], ?»
12  | S n' ⇒
13    ! regs' ← repeat_fresh … fresh n';
14    ! reg ← fresh ;
15    return «reg::regs',?»
16  ]. [% | @hide_prf cases regs' #l #EQ normalize >EQ % ] qed.*)
17
18definition fresh_label:
19 ∀g_pars,globals.state_monad (joint_internal_function g_pars globals) label ≝
20  λg_pars,globals,def.
21    let 〈r,luniverse〉 ≝ fresh … (joint_if_luniverse … def) in
22     〈set_luniverse … def luniverse, r〉.
23
24definition fresh_register:
25 ∀g_pars,globals.state_monad (joint_internal_function g_pars globals) register ≝
26  λg_pars,globals,def.
27    let 〈r,runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
28     〈set_runiverse … def runiverse, r〉.
29
30(* insert into a graph a list of instructions *)
31let rec adds_graph_pre
32  X
33  (g_pars: graph_params)
34  (globals: list ident)
35  (* for ERTLptr: the label parameter is filled by the last label *)
36  (pre_process : label → X → joint_seq g_pars globals)
37  (insts: list X)
38  (src : label) on insts :
39  state_monad (joint_internal_function g_pars globals) label ≝
40  match insts with
41  [ nil ⇒ return src
42  | cons i rest ⇒
43    ! mid ← fresh_label … ;
44    ! dst ← adds_graph_pre … pre_process rest mid ;
45    !_ state_update … (add_graph … src (sequential … (pre_process dst i) mid)) ;
46    return dst
47  ].
48
49let rec adds_graph_post
50  (g_pars: graph_params)
51  (globals: list ident)
52  (insts: list (joint_seq g_pars globals))
53  (dst : label) on insts :
54  state_monad (joint_internal_function g_pars globals) label ≝
55  match insts with
56  [ nil ⇒ return dst
57  | cons i rest ⇒
58    ! src ← fresh_label … ;
59    ! mid ← adds_graph_post … rest dst ;
60    !_ state_update … (add_graph … src (sequential … i mid)) ;
61    return src
62  ].
63
64definition adds_graph :
65  ∀g_pars : graph_params.
66  ∀globals: list ident.
67  ∀b : step_block g_pars globals.
68  label → label →
69  joint_internal_function g_pars globals → joint_internal_function g_pars globals ≝
70  λg_pars,globals,insts,src,dst,def.
71  let pref ≝ \fst (\fst insts) in
72  let op ≝ \snd (\fst insts) in
73  let post ≝ \snd insts in
74  let 〈def, mid〉 ≝ adds_graph_pre … (λlbl,inst.inst lbl) pref src def in
75  let 〈def, mid'〉 ≝ adds_graph_post … post dst def in
76  add_graph … mid (sequential … (op mid) mid') def.
77
78definition fin_adds_graph :
79  ∀g_pars : graph_params.
80  ∀globals: list ident.
81  ∀b : fin_block g_pars globals.
82  label →
83  joint_internal_function g_pars globals → joint_internal_function g_pars globals ≝
84  λg_pars,globals,insts,src,def.
85  let pref ≝ \fst insts in
86  let last ≝ \snd insts in
87  let 〈def, mid〉 ≝ adds_graph_pre … (λ_.λi.i) pref src def in
88  add_graph … mid (final … last) def.
89
90(* ignoring register allocation for now *)
91
92(*
93definition luniverse_ok : ∀p : graph_params.∀g.joint_internal_function p g → Prop ≝
94λp,g,def.fresh_map_for_univ … (joint_if_code … def) (joint_if_luniverse … def).
95*)
96(*
97lemma All_fresh_not_memb : ∀tag,u,l,id,u'.
98  All (identifier tag) (λid'.¬fresh_for_univ tag id' u) l →
99  〈id, u'〉 = fresh tag u →
100  ¬id ∈ l.
101#tag #u #l elim l [2: #hd #tl #IH] #id #u' *
102[ #hd_fresh #tl_fresh #EQfresh
103  whd in ⊢ (?(?%));
104  change with (eq_identifier ???) in match (?==?);
105  >eq_identifier_sym
106  >(eq_identifier_false … (fresh_distinct … hd_fresh EQfresh))
107  normalize nodelta @(IH … tl_fresh EQfresh)
108| #_ %
109]
110qed.
111
112
113lemma fresh_was_fresh : ∀tag,id,id',u,u'.
114〈id,u'〉 = fresh tag u →
115fresh_for_univ tag id' u' →
116id' ≠ id →
117fresh_for_univ tag id' u.
118#tag * #id * #id' * #u * #u'
119normalize #EQfresh destruct
120#H #NEQ
121elim (le_to_or_lt_eq … H)
122[ (* not recompiling... /2 by monotonic_pred/ *) /2/ ]
123#H >(succ_injective … H) in NEQ;
124* #G elim (G (refl …))
125qed.
126
127lemma fresh_not_in_univ : ∀tag,id,u,u'.
128〈id, u'〉 = fresh tag u →
129¬fresh_for_univ tag id u.
130#tag * #id * #u * #u' normalize #EQ destruct //
131qed.
132*)
133(*
134lemma adds_graph_list_fresh_preserve :
135  ∀g_pars,globals,b,src,dst,def.
136  let def' ≝ adds_graph_list g_pars globals b src dst def in
137  ∀lbl.fresh_for_univ … lbl (joint_if_luniverse … def) →
138       fresh_for_univ … lbl (joint_if_luniverse … def').
139#g_pars #globals #l elim l -l
140[ #src #dst #def whd #lbl #H @H ]
141#hd1 * [ #_ #src #dst #def whd #lbl #H @H ] #hd2 #tl #IH #src #dst #def whd #lbl #H
142whd in match (adds_graph_list ??????);
143whd in match fresh_label; normalize nodelta
144inversion (fresh ??) #mid #luniv' #EQfresh lapply (sym_eq ??? EQfresh) -EQfresh #EQfresh
145normalize nodelta
146@IH whd in match (joint_if_luniverse ???);
147@(fresh_remains_fresh … EQfresh) @H
148qed.
149
150lemma with_last_not_empty : ∀X,pref,last.not_empty X (pref @ [last]).
151#X * [2: #hd #tl ] #last % qed.
152
153lemma split_on_last_ne_elim : ∀X,l.∀P : ((list X) × X) → Prop.
154(∀pref,last.pi1 ?? l = pref @ [last] → P 〈pref, last〉) →
155P (split_on_last_ne X l).
156#X * @list_elim_left [ * ] #last #pref #_ #prf #P #H
157>split_on_last_ne_def @H % qed.
158
159(* use Russell? *)
160lemma adds_graph_list_ok :
161  ∀g_pars,globals,b,src,dst,def.
162  fresh_for_univ … src (joint_if_luniverse … def) →
163  luniverse_ok ?? def →
164  let def' ≝ adds_graph_list g_pars globals b src dst def in
165  luniverse_ok ?? def' ∧
166  (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) →
167                      stmt_at … (joint_if_code … def') lbl =
168                      stmt_at … (joint_if_code … def) lbl) ∧
169  let B ≝ ensure_step_block … b in
170  ∃l.bool_to_Prop (uniqueb … l) ∧
171    All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
172                 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
173    src ~❨B,l❩~> dst in joint_if_code … def'.
174#p #g #l elim l -l [2: #hd1 * [ #_ | #hd2 #tl #IH ]]
175#src #dst #def #Hsrc #Hdef
176[1,3: %
177  [1,3: %
178    [1,3: #lbl @(eq_identifier_elim … lbl src) #H destruct [1,3: #_ @Hsrc ]
179      whd in ⊢ (%→?); whd in match (adds_graph_list ??????);
180      >(lookup_add_miss ?????? H) @Hdef
181    |*: #lbl #H #G @lookup_add_miss @H
182    ]
183  |*: %{[]} % [1,3: %% ] %{src} % [1,3:%] %{dst} % [1,3: @lookup_add_hit ] %
184  ]
185]
186whd in match (adds_graph_list ??????);
187whd in match (fresh_label ???);
188inversion (fresh ??) normalize nodelta
189#mid #luniverse' #EQfresh lapply (sym_eq ??? EQfresh) -EQfresh #EQfresh
190letin def' ≝ (add_graph p g src (sequential … hd1 mid) (set_luniverse … def luniverse'))
191lapply (IH mid dst def' ??)
192[ #lbl @(eq_identifier_elim … lbl src) #H destruct
193  [2: whd in ⊢ (%→?); whd in match (adds_graph_list ??????);
194    >(lookup_add_miss ?????? H) ]
195  #Hpres @(fresh_remains_fresh … EQfresh) [ @Hdef ] assumption
196| whd in match def';
197  @(fresh_is_fresh … EQfresh)
198]
199whd in match (joint_if_luniverse ???);
200whd in match (joint_if_code ???);
201** #Hdef'' #stmt_preserved * #l ** #Hl1 #Hl2
202whd in ⊢ (%→?); @split_on_last_ne_elim #pref #last #EQ * #mid' * #Hl3 #Hl4
203%
204[ %{Hdef''} #lbl #NEQ
205  @(eq_identifier_elim ?? lbl mid)
206  [ #EQ destruct #ABS cases (absurd ? ABS ?) @(fresh_not_in_univ … EQfresh)
207  | #NEQ' #H >(stmt_preserved … NEQ')
208    [ whd in match (joint_if_code ???);
209      whd in match (stmt_at ????); >lookup_add_miss [2: @NEQ ] %
210    | @(fresh_remains_fresh … EQfresh) @H
211    ]
212  ]
213]
214%{(mid::l)}
215% [ % ]
216[ whd in ⊢ (?%);
217  cut (Not (bool_to_Prop (mid∈l)))
218  [ % #H elim (All_memb … Hl2 H)
219    whd in match (joint_if_luniverse ???);
220    #G #_ @(absurd ?? G)
221    @ (fresh_is_fresh … EQfresh)
222  | #H >H assumption
223  ]
224| %
225  [ %{(fresh_not_in_univ … EQfresh)}
226    @adds_graph_list_fresh_preserve @(fresh_is_fresh … EQfresh)
227  | @(All_mp … Hl2) #lbl * * #H1 #H2 %{H2} % #H3 @H1
228    @(fresh_remains_fresh … EQfresh) assumption
229  ]
230| whd in match (ensure_step_block ???) in EQ ⊢ %;
231  whd in match (map ??? (hd2 :: ?)); >EQ whd
232  change with ((?::?)@?) in match (?::?@?); >split_on_last_ne_def
233  %{mid'} % [2: @Hl4 ]
234  %{Hl3} %{mid} >stmt_preserved
235  [ % [2: % ] @lookup_add_hit
236  | @(fresh_remains_fresh … EQfresh) assumption
237  | % #ABS destruct @(absurd ? Hsrc) @(fresh_not_in_univ … EQfresh)
238  ]
239]
240qed.
241*)
242(*
243axiom adds_graph_ok :
244  ∀g_pars,globals,B,src,dst,def.
245  fresh_for_univ … src (joint_if_luniverse … def) →
246  luniverse_ok ?? def →
247  let def' ≝ adds_graph g_pars globals B src dst def in
248  luniverse_ok ?? def' ∧
249  (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) →
250                      stmt_at … (joint_if_code … def') lbl =
251                      stmt_at … (joint_if_code … def) lbl) ∧
252  ∃l.bool_to_Prop (uniqueb … l) ∧
253    All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
254                 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
255    src ~❨B,src::l❩~> dst in joint_if_code … def'.
256 
257axiom fin_adds_graph_ok :
258  ∀g_pars,globals,B,src,def.
259  fresh_for_univ … src (joint_if_luniverse … def) →
260  luniverse_ok ?? def →
261  let def' ≝ fin_adds_graph g_pars globals B src def in
262  luniverse_ok ?? def' ∧
263  (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) →
264                      stmt_at … (joint_if_code … def') lbl =
265                      stmt_at … (joint_if_code … def) lbl) ∧
266  ∃l.bool_to_Prop (uniqueb … l) ∧
267    All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
268                 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
269    src ~❨B,src::l❩~> it in joint_if_code … def'.
270*)
271
272(*
273definition insert_epilogue ≝
274  λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals).
275  λdef : joint_internal_function g_pars globals.
276  let exit ≝ joint_if_exit … def in
277  match stmt_at … exit
278  return λx.match x with [None ⇒ false | Some _ ⇒ true] → ?
279  with
280  [ Some s ⇒ λ_.
281    let 〈def', tmp〉 as prf ≝ adds_graph_list ?? insts exit def in
282    let def'' ≝ add_graph … tmp s def' in
283    set_joint_code … def'' (joint_if_code … def'') (joint_if_entry … def'') tmp
284  | None ⇒ Ⓧ
285  ] (pi2 … exit).
286whd in match def''; >graph_code_has_point //
287qed.
288*)
289
290definition b_adds_graph :
291  ∀g_pars: graph_params.
292  ∀globals: list ident.
293  ∀b : bind_step_block g_pars globals.
294  label → label →
295  joint_internal_function g_pars globals→
296  joint_internal_function g_pars globals ≝
297  λg_pars,globals,insts,src,dst,def.
298  let 〈def, stmts〉 ≝ bcompile ??? (fresh_register …) insts def in
299  adds_graph … stmts src dst def.
300
301(*
302axiom b_adds_graph_ok :
303  ∀g_pars,globals,B,src,dst,def.
304  fresh_for_univ … src (joint_if_luniverse … def) →
305  luniverse_ok ?? def →
306  let def' ≝ b_adds_graph g_pars globals B src dst def in
307  luniverse_ok ?? def' ∧
308  (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) →
309                      stmt_at … (joint_if_code … def') lbl =
310                      stmt_at … (joint_if_code … def) lbl) ∧
311  ∃l,r.
312    bool_to_Prop (uniqueb … l) ∧
313    bool_to_Prop (uniqueb … r) ∧
314    All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
315                 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
316    All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def) ∧
317                 fresh_for_univ … reg (joint_if_runiverse … def')) r ∧
318    src ~❨B,src::l,r❩~> dst in joint_if_code … def'.
319*)
320definition b_fin_adds_graph :
321  ∀g_pars: graph_params.
322  ∀globals: list ident.
323  ∀b : bind_fin_block g_pars globals.
324  label →
325  joint_internal_function g_pars globals→
326  joint_internal_function g_pars globals ≝
327  λg_pars,globals,insts,src,def.
328  let 〈def, stmts〉 ≝ bcompile ??? (fresh_register …) insts def in
329  fin_adds_graph … stmts src def.
330
331(*
332axiom b_fin_adds_graph_ok :
333  ∀g_pars,globals,B,src,def.
334  fresh_for_univ … src (joint_if_luniverse … def) →
335  luniverse_ok ?? def →
336  let def' ≝ b_fin_adds_graph g_pars globals B src def in
337  luniverse_ok ?? def' ∧
338  (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) →
339                      stmt_at … (joint_if_code … def') lbl =
340                      stmt_at … (joint_if_code … def) lbl) ∧
341  ∃l,r.
342    bool_to_Prop (uniqueb … l) ∧
343    bool_to_Prop (uniqueb … r) ∧
344    All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
345                 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
346    All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def) ∧
347                 fresh_for_univ … reg (joint_if_runiverse … def')) r ∧
348    src ~❨B,src::l,r❩~> it in joint_if_code … def'.
349*)
350
351lemma opt_All_intro : ∀X,P,o.
352(∀x.o = Some ? x → P x) → opt_All X P o. #X #P * [//] #x #H @H % qed.
353 
354(*
355definition points_of : ∀p,g.joint_internal_function p g → Type[0] ≝
356λp,g,def.Σl.bool_to_Prop (code_has_point … (joint_if_code … def) l).
357
358unification hint 0 ≔ p, g, def;
359points ≟ code_point p,
360code ≟ joint_if_code p g def,
361P ≟ λl : points.bool_to_Prop (code_has_point p g code l)
362
363points_of p g def ≡ Sig points P.
364
365definition stmt_at_safe : ∀p,g,def.points_of p g def → joint_statement p g ≝
366  λp,g,def,pt.opt_safe ? (stmt_at ?? (joint_if_code ?? def) (pi1 … pt)) ?.
367@hide_prf cases pt -pt #pt whd in ⊢ (?%→?); #H % #G >G in H; * qed.
368*)
369
370let rec bind_new_P' R X (P : list R → X → Prop) (m : bind_new R X) on m : Prop ≝
371match m with
372[ bret x ⇒ P [ ] x
373| bnew f ⇒
374  ∀r.bind_new_P' R X (λl.P (r::l)) (f r)
375].
376
377definition step_registers :  ∀p : uns_params.∀globals.
378  joint_step p globals → list register ≝
379λp,globals,s.get_used_registers_from_step … (functs … p) s.
380
381definition step_forall_registers : ∀p : uns_params.∀globals.
382  (register → Prop) → joint_step p globals → Prop ≝
383λp,globals,P,s.All … P (step_registers … s).
384
385definition fin_step_registers :  ∀p : uns_params.
386  joint_fin_step p → list register ≝
387λp,s.match s with [ TAILCALL _ _ r ⇒ f_call_args … (functs … p) r | _ ⇒ [ ] ].
388
389definition fin_step_forall_registers : ∀p : uns_params.
390  (register → Prop) → joint_fin_step p → Prop ≝
391λp,P,s.All … P (fin_step_registers … s).
392
393definition fin_step_forall_labels : ∀p : uns_params.
394  (label → Prop) → joint_fin_step p → Prop ≝
395λp,P,s.All … P (fin_step_labels … s).
396
397definition step_labels_and_registers_in : ∀p : uns_params.∀globals.
398  list label → list register → joint_step p globals → Prop ≝
399λp,g,allowed_l,allowed_r,s.
400  step_forall_labels … (In ? allowed_l) s ∧
401  step_forall_registers … (In ? allowed_r) s.
402
403definition fin_step_labels_and_registers_in : ∀p : uns_params.
404  list label → list register → joint_fin_step p → Prop ≝
405λp,allowed_l,allowed_r,s.
406  fin_step_forall_labels … (In ? allowed_l) s ∧
407  fin_step_forall_registers … (In ? allowed_r) s.
408
409record b_graph_translate_data
410  (src, dst : graph_params)
411  (globals : list ident) : Type[0] ≝
412{ init_ret : call_dest dst
413; init_params : paramsT dst
414; added_local_stacksize : ℕ
415; added_params_stacksize : ℕ
416; added_spilled_stacksize : ℕ
417; added_prologue : list (joint_seq dst globals)
418; new_regs : list register (* new registers added globally *)
419; f_step : label → joint_step src globals → bind_step_block dst globals
420; f_fin : label → joint_fin_step src → bind_fin_block dst globals
421; good_f_step :
422  ∀l,s.bind_new_P' ??
423    (λlocal_new_regs,block.let 〈pref, op, post〉 ≝ block in
424       ∀l.
425       let allowed_labels ≝ l :: step_labels … s in
426       let allowed_registers ≝ new_regs @ local_new_regs @ step_registers … s in
427       All (label → joint_seq ??)
428         (λs'.step_labels_and_registers_in … allowed_labels allowed_registers (step_seq dst globals (s' l)))
429         pref ∧
430       step_labels_and_registers_in … allowed_labels allowed_registers (op l) ∧
431       All (joint_seq ??) (step_labels_and_registers_in … allowed_labels allowed_registers) post)
432    (f_step l s)
433; good_f_fin :
434  ∀l,s.bind_new_P' ??
435    (λlocal_new_regs,block.let 〈pref, op〉 ≝ block in
436       let allowed_labels ≝ l :: fin_step_labels … s in
437       let allowed_registers ≝ new_regs @ local_new_regs @ fin_step_registers … s in
438       All (joint_seq ??) (λs.step_labels_and_registers_in … allowed_labels allowed_registers s) pref ∧
439       fin_step_labels_and_registers_in … allowed_labels allowed_registers op)
440    (f_fin l s)
441; f_step_on_cost :
442  ∀l,c.f_step l (COST_LABEL … c) =
443    bret ? (step_block ??) 〈[ ], λ_.COST_LABEL dst globals c, [ ]〉
444; cost_in_f_step :
445  ∀l,s,c.
446  bind_new_P ??
447    (λblock.∀l'.\snd (\fst block) l' = COST_LABEL dst globals c →
448       s = COST_LABEL … c) (f_step l s)
449}.
450
451definition bound_b_graph_translate_data ≝
452λsrc,dst,globals.
453Σd : bind_new register (b_graph_translate_data src dst globals).
454bind_new_P' ?? (λregs,data.new_regs ??? data = regs) d.
455
456unification hint 0 ≔ src,dst,globals ⊢
457bound_b_graph_translate_data src dst globals ≡
458Sig (bind_new register (b_graph_translate_data src dst globals)) (λd.bind_new_P' ?? (λregs,data.new_regs ??? data = regs) d).
459
460definition get_first_costlabel_next : ∀p,g.
461  joint_closed_internal_function p g → costlabel × (succ p) ≝
462  λp,g,def.
463  match stmt_at … (joint_if_code … def) (joint_if_entry … def)
464  return λx.stmt_at ???? = x → ? with
465  [ Some s ⇒
466    match s return λx.stmt_at ???? = Some ? x → ? with
467    [ sequential s' nxt ⇒
468      match s' return λx.stmt_at ???? = Some ? (sequential … x nxt) → ? with
469      [ COST_LABEL c ⇒ λ_.〈c, nxt〉
470      | _ ⇒ λabs.⊥
471      ]
472    | _ ⇒ λabs.⊥
473    ]
474  | _ ⇒ λabs.⊥
475  ] (refl …).
476@hide_prf
477cases def in abs; -def #def #good_def
478cases (entry_is_cost … good_def) #nxt' * #c #EQ >EQ #ABS destruct
479qed.
480
481definition get_first_costlabel ≝ λp,g,f.\fst (get_first_costlabel_next p g f).
482
483definition partial_partition : ∀X.∀Y : DeqSet.(X → list Y) → Prop ≝
484λX,Y,f.
485(∀x.bool_to_Prop (uniqueb … (f x))) ∧
486(∀x1,x2,y.y ∈ f x1 → y ∈ f x2 → x1 = x2).
487
488definition not_emptyb : ∀X.list X → bool ≝
489λX,l.match l with [ nil ⇒ false | cons _ _ ⇒ true].
490
491record b_graph_translate_props
492  (src_g_pars, dst_g_pars : graph_params)
493  (globals: list ident)
494  (data : b_graph_translate_data src_g_pars dst_g_pars globals)
495  (def_in : joint_closed_internal_function src_g_pars globals)
496  (def_out : joint_closed_internal_function dst_g_pars globals)
497  (f_lbls : label → list label)
498  (f_regs : label → list register) : Prop ≝
499{ res_def_out_eq :
500           joint_if_result … def_out = init_ret … data
501; pars_def_out_eq :
502           joint_if_params … def_out = init_params … data
503; local_ss_def_out_eq :
504           joint_if_local_stacksize … def_out =
505           joint_if_local_stacksize … def_in + added_local_stacksize … data
506; params_ss_def_out_eq :
507           joint_if_params_stacksize … def_out =
508           joint_if_params_stacksize … def_in + added_params_stacksize … data
509; spilled_ss_def_out_eq :
510           joint_if_spilled_stacksize … def_out =
511           joint_if_spilled_stacksize … def_in + added_spilled_stacksize … data
512; partition_lbls : partial_partition … f_lbls
513; partition_regs : partial_partition … f_regs
514; freshness_lbls :
515  (∀l.All …
516    (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧
517           fresh_for_univ … lbl (joint_if_luniverse … def_out)) (f_lbls l))
518; freshness_regs :
519  (∀l.All …
520    (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧
521           fresh_for_univ … reg (joint_if_runiverse … def_out)) (f_regs l))
522; freshness_data_regs :
523  All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧
524               fresh_for_univ … reg (joint_if_runiverse … def_out)) (new_regs … data)
525; data_regs_disjoint : ∀l,r.r ∈ f_regs l → r ∈ new_regs … data → False
526; multi_fetch_ok :
527  ∀l,s.stmt_at … (joint_if_code … def_in) l = Some ? s →
528  let lbls ≝ f_lbls l in let regs ≝ f_regs l in
529  match s with
530  [ sequential s' nxt ⇒
531    let block ≝
532      if not_emptyb … (added_prologue … data) ∧
533         eq_identifier … (joint_if_entry … def_in) l then
534        bret … [ ]
535      else
536        f_step … data l s' in
537    l ~❨block, l::lbls, regs❩~> nxt in joint_if_code … def_out
538  | final s' ⇒
539    l ~❨f_fin … data l s', l::lbls, regs❩~> it in joint_if_code … def_out
540  | FCOND abs _ _ _ ⇒ Ⓧabs
541  ]
542; prologue_ok :
543  if not_emptyb … (added_prologue … data) then
544    ∃lbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧
545    joint_if_entry … def_out
546      ~❨〈[ ],λ_.COST_LABEL … (get_first_costlabel … def_in), added_prologue … data〉,
547        f_lbls … lbl❩~> joint_if_entry … def_in in joint_if_code … def_out
548  else (joint_if_entry … def_out = joint_if_entry … def_in)
549}.
550
551definition pair_swap : ∀A,B.(A × B) → B × A ≝ λA,B,pr.〈\snd pr, \fst pr〉.
552
553definition set_entry ≝
554  λglobals: list ident.
555  λpars: params.
556  λint_fun: joint_internal_function pars globals.
557  λentry.
558  (*λexit.*)
559    mk_joint_internal_function pars globals
560      (joint_if_luniverse … int_fun) (joint_if_runiverse … int_fun) (joint_if_result … int_fun)
561      (joint_if_params … int_fun) (joint_if_stacksize … int_fun)
562       (joint_if_local_stacksize … int_fun)
563       (joint_if_params_stacksize … int_fun)
564      (joint_if_code … int_fun) entry (*exit*).
565
566(* translation with inline fresh register allocation *)
567definition b_graph_translate :
568  ∀src_g_pars,dst_g_pars : graph_params.
569  ∀globals: list ident.
570  (* initialization info *)
571  ∀data : bound_b_graph_translate_data src_g_pars dst_g_pars globals.
572  (* source function *)
573  ∀def_in : joint_closed_internal_function src_g_pars globals.
574  (* destination function *)
575  Σdef_out : joint_closed_internal_function dst_g_pars globals.
576  ∃data',regs,f_lbls,f_regs.
577    bind_new_instantiates ?? data' data regs ∧ (* so new_regs … data = regs *)
578    b_graph_translate_props … data' def_in def_out f_lbls f_regs
579   ≝
580  λsrc_g_pars,dst_g_pars,globals,data,def.
581  let runiv_data ≝ bcompile … (pair_swap ?? ∘ fresh RegisterTag) data (joint_if_runiverse … def) in
582  let runiv ≝ \fst runiv_data in
583  let data ≝ \snd runiv_data in
584  let entry ≝ joint_if_entry … def in
585  let init ≝
586    mk_joint_internal_function dst_g_pars globals
587    (joint_if_luniverse … def)
588    runiv
589    (init_ret … data) (init_params … data)
590    (joint_if_local_stacksize … def + added_local_stacksize … data)
591    (joint_if_params_stacksize … def + added_params_stacksize … data)
592    (joint_if_spilled_stacksize … def + added_spilled_stacksize … data)
593    (empty_map ? (joint_statement ??))
594    entry in
595  let f : label → joint_statement (src_g_pars : params) globals →
596    joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝
597    λlbl,stmt,def.
598    match stmt with
599    [ sequential inst next ⇒
600      b_adds_graph … (f_step … data lbl inst) lbl next def
601    | final inst ⇒
602      b_fin_adds_graph … (f_fin … data lbl inst) lbl def
603    | FCOND abs _ _ _ ⇒ Ⓧabs
604    ] in
605  let def_out ≝ foldi ??? f (joint_if_code … def) init in
606  let prologue ≝ added_prologue … data in
607  let def_out ≝
608    if not_emptyb … prologue then
609      (* retrieve initial cost label and its next from src *)
610      let 〈init_c, nxt〉 ≝
611        get_first_costlabel_next … def in
612      (* erase in dst the initial cost label *)
613      let def_out ≝ add_graph … entry
614        (sequential dst_g_pars … (NOOP …) nxt) def_out in
615      (* generate a new entry label *)
616      let 〈def_out, entry'〉 ≝ fresh_label … def_out in
617      (* add the initial cost label followed by the prologue *)
618      let def_out ≝ adds_graph … 〈[ ], λ_.COST_LABEL … init_c, prologue〉
619        entry' entry def_out in
620      (* redirect the entry *)
621      set_entry … def_out entry'
622    else def_out in
623  ««def_out, ?», ?».
624@hide_prf
625[ cases daemon
626| cases daemon (* TODO *)
627] qed.
628
629definition b_graph_transform_program :
630  ∀src_g_pars,dst_g_pars : graph_params.
631  (* initialization *)
632  (∀globals.joint_closed_internal_function src_g_pars globals →
633    bound_b_graph_translate_data src_g_pars dst_g_pars globals) →
634  joint_program src_g_pars →
635  joint_program dst_g_pars ≝
636  λsrc,dst,init.
637  transform_joint_program …
638        (λvarnames,def_in.b_graph_translate … (init varnames def_in) … def_in).
639
640definition added_registers :
641  ∀p : graph_params.∀g.
642  joint_internal_function p g → (label → list register) → list register ≝
643  λp,g,def,f_regs.
644  let f ≝ λlbl : label.λ_.λacc.(f_regs lbl)@acc in
645  foldi … f (joint_if_code p g def) [ ].
646
647axiom added_registers_ok :
648  ∀p,g,def,f_regs.
649  ∀l,s.stmt_at … (joint_if_code … def) l = Some ? s →
650  (All … (λlbl.bool_to_Prop (lbl ∈ added_registers p g def f_regs)) (f_regs l)).
651
652(*(* translation without register allocation (more or less an alias) *)
653definition graph_translate :
654  ∀src_g_pars,dst_g_pars : graph_params.
655  ∀globals: list ident.
656  (* initialization info *)
657  call_dest dst_g_pars → (* joint_if_result *)
658  paramsT dst_g_pars → (* joint_if_params *)
659  ℕ → (* joint_if_stacksize *)
660  (* functions dictating the translation *)
661  (label → joint_step src_g_pars globals → step_block dst_g_pars globals) →
662  (label → joint_fin_step src_g_pars → fin_block dst_g_pars globals) →
663  (* source function *)
664  joint_internal_function src_g_pars globals →
665  (* destination function *)
666  joint_internal_function dst_g_pars globals ≝
667  λsrc_g_pars,dst_g_pars,globals,init1,init2,init3,trans_step,trans_fin_step.
668  b_graph_translate … init1 init2 init3
669    (λl,s.return trans_step l s)
670    (λl,s.return trans_fin_step l s).
671*)
672(*
673let rec add_translates
674  (pars1: params1) (globals: list ident)
675  (translate_list: list ?) (start_lbl: label) (dest_lbl: label)
676  (def: joint_internal_function … (graph_params pars1 globals))
677    on translate_list ≝
678  match translate_list with
679  [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def
680  | cons trans translate_list ⇒
681    match translate_list with
682    [ nil ⇒ trans start_lbl dest_lbl def
683    | _ ⇒
684      let 〈tmp_lbl, def〉 ≝ fresh_label … def in
685      let def ≝ trans start_lbl tmp_lbl def in
686        add_translates pars1 globals translate_list tmp_lbl dest_lbl def]].
687
688definition adds_graph ≝
689 λpars1:params1.λglobals. λstmt_list: list (label → joint_statement (graph_params_ pars1) globals).
690  add_translates … (map ?? (λf,start_lbl,dest_lbl. add_graph pars1 ? start_lbl (f dest_lbl)) stmt_list).
691  *)
692
693include "joint/joint_stacksizes.ma".
694
695lemma bind_new_P_mp' : ∀R,X,P,Q,m.
696(∀l,x.P l x → Q l x) →
697bind_new_P' R X P m → bind_new_P' R X Q m.
698#R #X #P #Q #m lapply Q -Q lapply P -P elim m -m
699[ #x #P #Q #H #G @H @G
700| #f #IH #P #Q #H #G #r
701  @IH [3: @(G r) |*:] #l @H
702]
703qed.
704
705lemma joint_transform_monotone_stacksizes :
706∀src_g_pars,dst_g_pars : graph_params.
707(* initialization *)
708∀data.
709∀p_in.
710let p_out ≝ b_graph_transform_program src_g_pars dst_g_pars data p_in in
711stack_cost_model_le (stack_cost ? p_in) (stack_cost ? p_out).
712#src #dst #data #p_in
713whd
714@list_map_opt_All2
715[ @(λid_def1,id_def2.
716   match \snd id_def1 with
717   [ Internal f1 ⇒
718     match \snd id_def2 with
719     [ Internal f2 ⇒
720       \fst id_def1 = \fst id_def2 ∧
721       le (joint_if_stacksize … f1) (joint_if_stacksize … f2)
722     | _ ⇒ False
723     ]
724   | External _ ⇒ match \snd id_def2 with [ Internal _ ⇒ False | External _ ⇒ True ]
725   ])
726| * #id * #f1 * #id' * #f2 normalize nodelta [|*: * %]
727  ** #H %{H} % ]
728@All2_of_map * #id * #f normalize nodelta [2: %]
729% [%]
730cases (b_graph_translate ?????)
731whd in match (jp_functions dst ?);
732lapply f -f
733generalize in match (?@jp_functions ??); #globals
734#f_in #f_out * #data' * #regs * #f_lbls * #f_regs * #inst #props
735whd in match joint_if_stacksize; normalize nodelta
736@le_plus [ @le_plus ]
737[ >(spilled_ss_def_out_eq … props)
738| >(params_ss_def_out_eq … props)
739| >(local_ss_def_out_eq … props)
740] //
741qed.
Note: See TracBrowser for help on using the repository browser.