source: src/joint/semanticsUtils.ma @ 2946

Last change on this file since 2946 was 2946, checked in by tranquil, 7 years ago

main novelties:

  • there is an in-built stack_usage nat in joint states, at the base of the new division of RTL's semantics (with separate stacks, with separate stacks but with an artificial overflow error, with a unique stack)
  • a premain is added semantically to the global env, so initial cost label and main call and return are observed
  • proper initialization is now in LINToASM (to be sure, endianess should be checked ;-)

The update breaks proofs of back end atm. compiler.ma should be okay, but I have not had time to complete its compilation.

File size: 26.8 KB
Line 
1include "joint/joint_semantics.ma".
2include alias "common/Identifiers.ma".
3include "utilities/hide.ma".
4include "ASM/BitVectorTrie.ma".
5include "joint/TranslateUtils.ma".
6include "common/ExtraMonads.ma".
7include "common/extraGlobalenvs.ma".
8
9definition reg_store ≝ λreg,v,locals.add RegisterTag beval locals reg v.
10
11definition reg_retrieve : register_env beval → register → res beval ≝
12 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg).
13
14record hw_register_env : Type[0] ≝
15  { reg_env : BitVectorTrie beval 6
16  ; other_bit : bebit
17  }.
18
19include alias "ASM/BitVectorTrie.ma".
20
21definition hwreg_retrieve: hw_register_env → Register → beval ≝
22 λenv,r. lookup … (bitvector_of_register r) (reg_env env) BVundef.
23
24definition hwreg_store: Register → beval → hw_register_env → hw_register_env ≝
25 λr,v,env.mk_hw_register_env (insert … (bitvector_of_register r) v (reg_env env))
26  (other_bit env).
27
28definition hwreg_set_other : bebit → hw_register_env → hw_register_env ≝
29λv,env.mk_hw_register_env (reg_env env) v.
30
31definition hwreg_retrieve_sp : hw_register_env → res xpointer ≝
32λenv.
33let spl ≝ hwreg_retrieve env RegisterSPL in
34let sph ≝ hwreg_retrieve env RegisterSPH in
35! ptr ← pointer_of_address 〈spl, sph〉 ;
36match ptype ptr return λx.ptype ptr = x → res xpointer with
37[ XData ⇒ λprf.return «ptr, prf»
38| _ ⇒ λ_.Error … [MSG BadPointer]
39] (refl …).
40
41definition hwreg_store_sp : hw_register_env → xpointer → hw_register_env ≝
42λenv,sp.
43let 〈spl, sph〉 ≝ beval_pair_of_pointer sp in
44hwreg_store RegisterSPH sph (hwreg_store RegisterSPL spl env).
45
46definition init_hw_register_env: xpointer → hw_register_env ≝
47 hwreg_store_sp (mk_hw_register_env (Stub …) BBundef).
48
49(*** Store/retrieve on pseudo-registers ***)
50include alias "common/Identifiers.ma".
51
52unification hint 0 ≔ X ⊢ register_env X ≡ identifier_map RegisterTag X.
53
54(******************************** GRAPHS **************************************)
55
56record sem_graph_params : Type[1] ≝
57{ sgp_pars : uns_params
58; sgp_sup : ∀F.sem_unserialized_params sgp_pars F
59; graph_pre_main_generator :
60  ∀p : joint_program (mk_graph_params sgp_pars).
61  joint_closed_internal_function (mk_graph_params sgp_pars) (prog_var_names … p)
62}.
63
64
65definition sem_graph_params_to_graph_params :
66  ∀pars : sem_graph_params.graph_params ≝
67  λpars.mk_graph_params (sgp_pars pars).
68
69coercion graph_params_from_sem_graph_params nocomposites :
70  ∀pars : sem_graph_params.
71  graph_params ≝ sem_graph_params_to_graph_params
72  on _pars : sem_graph_params to graph_params.
73
74definition sem_graph_params_to_sem_params :
75  ∀pars : sem_graph_params.
76  sem_params ≝
77  λpars.
78  mk_sem_params
79    (mk_serialized_params
80      (pars : graph_params)
81      (sgp_sup pars ?)
82      (word_of_identifier ?)
83      (an_identifier ?)
84      ? (refl …))
85    (graph_pre_main_generator pars).
86* #p % qed.
87
88coercion sem_params_from_sem_graph_params :
89  ∀pars : sem_graph_params.
90  sem_params ≝ sem_graph_params_to_sem_params
91  on _pars : sem_graph_params to sem_params.
92
93
94(******************************** LINEAR **************************************)
95
96lemma succ_pos_of_nat_of_pos : ∀p.succ_pos_of_nat (nat_of_pos p) = succ p.
97@pos_elim [%]
98#p #IH >nat_possucc whd in ⊢ (??%?); >IH % qed.
99
100record sem_lin_params : Type[1] ≝
101{ slp_pars : uns_params
102; slp_sup : ∀F.sem_unserialized_params slp_pars F
103; lin_pre_main_generator :
104  ∀p : joint_program (mk_lin_params slp_pars).
105  joint_closed_internal_function (mk_lin_params slp_pars) (prog_var_names … p)
106}.
107
108definition sem_lin_params_to_lin_params :
109  ∀pars : sem_lin_params.lin_params ≝
110  λpars.mk_lin_params (slp_pars pars).
111
112coercion lin_params_from_sem_lin_params nocomposites :
113  ∀pars : sem_lin_params.
114  lin_params ≝ sem_lin_params_to_lin_params
115  on _pars : sem_lin_params to lin_params.
116
117definition sem_lin_params_to_sem_params :
118  ∀pars : sem_lin_params.
119  sem_params ≝
120  λpars.
121  mk_sem_params
122    (mk_serialized_params
123      (pars : lin_params)
124      (slp_sup pars ?)
125      succ_pos_of_nat
126      (λp.pred (nat_of_pos p))
127      ??)
128    (lin_pre_main_generator pars).
129[ @pos_cases [%] #p >nat_possucc @succ_pos_of_nat_of_pos
130| #n >nat_succ_pos %
131] qed.
132
133coercion sem_params_from_sem_lin_params :
134  ∀pars : sem_lin_params.
135  sem_params ≝ sem_lin_params_to_sem_params
136  on _pars : sem_lin_params to sem_params.
137
138(* watch out, implementation dependent:
139   an_identifier SymbolTag one must be unused (used for premain)
140*)
141definition pre_main_id : ident ≝ an_identifier … one.
142
143lemma lookup_opt_pm_set_elim : ∀A.∀P : option A → Prop.∀p,q,o,m.
144  (p = q → P o) →
145  (p ≠ q → P (lookup_opt A p m)) →
146  P (lookup_opt A p (pm_set A q o m)).
147#A #P #p #q
148@(eqb_elim p q) #H #o #m #H1 #H2
149[ >H >lookup_opt_pm_set_hit @H1 @H
150| >lookup_opt_pm_set_miss [ @H2 ] @H
151]
152qed.
153
154lemma lookup_add_elim : ∀tag,A.∀P : option A → Prop.∀m,i,j,x.
155  (i = j → P (Some ? x)) →
156  (i ≠ j → P (lookup tag A m j)) →
157  P (lookup tag A (add tag A m i x) j).
158#tag #A #P * #m * #p * #q #x
159#H1 #H2 whd in ⊢ (?%); normalize nodelta whd in match insert; normalize nodelta
160@lookup_opt_pm_set_elim #H destruct
161[ @H1 % | @H2 % #EQ destruct cases H #H @H % ]
162qed.
163
164(* we just manually overwrite genv_t tables with the pre_main.
165   the RTLabs → RTL pass will need to ensure no pre_main_id is actually present *)
166definition joint_globalenv :
167  ∀pars : sem_params.joint_program pars → genv_t ? ≝
168  λpars,prog.
169  let genv ≝ drop_fn … pre_main_id (globalenv … (λx.x) prog) in
170  mk_genv_t ?
171    (insert … one (Internal … (pre_main_generator … pars prog)) (functions … genv))
172    (nextfunction … genv)
173    (add … (symbols … genv) pre_main_id (mk_block (-1)))
174    ?.
175@hide_prf
176whd in match insert; normalize nodelta #b
177@lookup_opt_pm_set_elim #H destruct
178[ #_ %{pre_main_id} @lookup_add_hit ]
179#G cases (functions_inv … G) #id #EQ %{id}
180@lookup_add_elim #EQid destruct [2: assumption ]
181@⊥ whd in match drop_fn in EQ; normalize nodelta in EQ;
182>lookup_remove_hit in EQ; #ABS destruct
183qed.
184
185lemma fetch_statement_eq : ∀p:sem_params.∀g.
186  ∀ge : genv_t (joint_function p g).∀ptr : program_counter.
187  ∀i,fn,s.
188  fetch_internal_function … ge (pc_block ptr) = OK … 〈i, fn〉 →
189  let pt ≝ point_of_pc … ptr in
190  stmt_at … (joint_if_code … fn) pt = Some ? s →
191  fetch_statement … ge ptr = OK … 〈i, fn, s〉.
192#p #g #ge #ptr #i #f #s #EQ1 #EQ2
193whd in match fetch_statement; normalize nodelta >EQ1 >m_return_bind
194>EQ2 %
195qed.
196
197lemma fetch_statement_inv : ∀p:sem_params.∀g.
198  ∀ge : genv_t (joint_function p g).∀ptr : program_counter.
199  ∀i,fn,s.
200  fetch_statement … ge ptr = OK … 〈i, fn, s〉 →
201  fetch_internal_function … ge (pc_block ptr) = OK … 〈i, fn〉 ∧
202  let pt ≝ point_of_pc p ptr in
203  stmt_at … (joint_if_code … fn) pt = Some ? s.
204#p #g #ge #ptr #i #fn #s #H
205elim (bind_inversion ????? H) * #i #f' * #EQ1 -H #H
206elim (bind_inversion ????? H) #s' * #H
207lapply (opt_eq_from_res ???? H) -H #EQ2
208whd in ⊢ (??%%→?); #EQ destruct(EQ) %{EQ1 EQ2}
209qed.
210
211definition pm_P : ∀A,B.∀P : A → B → Prop.positive_map A → positive_map B → Prop ≝
212λA,B,P,mA,mB.
213∀p.
214match lookup_opt … p mA with
215[ Some a ⇒
216  match lookup_opt … p mB with
217  [ Some b ⇒ P a b
218  | _ ⇒ False
219  ]
220| _ ⇒ match lookup_opt … p mB with
221  [ Some _ ⇒ False
222  | _ ⇒ True
223  ]
224].
225
226definition match_funct_map :
227  ∀M : matching.
228  ∀vars.positive_map (m_A M vars) → positive_map (m_B M vars) → Prop ≝
229  λM,vars.pm_P … (match_fundef M ?).
230
231lemma pm_P_insert :
232  ∀A,B,P.
233  ∀p,a1,a2,m1,m2.P a1 a2 → pm_P A B P m1 m2 →
234  pm_P … P (insert … p a1 m1) (insert … p a2 m2).
235#A #B #P #p #a1 #a2 #m1 #m2 #Pa1a2 #Pm1m2
236#p'
237@(eqb_elim p' p) #H destruct
238[ >lookup_opt_insert_hit >lookup_opt_insert_hit @Pa1a2
239| >(lookup_opt_insert_miss … a1 … H) >(lookup_opt_insert_miss … a2 … H)
240  @Pm1m2
241]
242qed.
243
244lemma pm_P_set_None :
245  ∀A,B,P.
246  ∀p,m1,m2.pm_P A B P m1 m2 →
247  pm_P … P (pm_set … p (None ?) m1) (pm_set … p (None ?) m2).
248#A #B #P #p #m1 #m2 #Pm1m2
249#p'
250@(eqb_elim p' p) #H destruct
251[ >lookup_opt_pm_set_hit >lookup_opt_pm_set_hit %
252| >(lookup_opt_pm_set_miss … H) >(lookup_opt_pm_set_miss … H)
253  @Pm1m2
254]
255qed.
256
257record match_genv_t (M : matching)
258  (vars : list ident)
259  (ge1 : genv_t (m_A M vars)) (ge2 : genv_t (m_B M vars)) : Prop ≝
260{ symbols_eq : symbols … ge1 = symbols … ge2
261; nextfunction_eq : nextfunction … ge1 = nextfunction … ge2
262; functions_match : pm_P … (match_fundef M ?) (functions … ge1) (functions … ge2)
263}.
264
265lemma add_globals_match :
266  ∀M : matching.∀initV,initW.
267  ∀vars1,vars2.
268  ∀vars.
269(*  let vars1' ≝ map … (λx.\fst (\fst x)) vars1 in
270  let vars2' ≝ map … (λx.\fst (\fst x)) vars2 in *)
271  ∀env_mem1 : genv_t (m_A M vars) × mem.
272  ∀env_mem2 : genv_t (m_B M vars) × mem.
273  All2 (ident×region×(m_V M)) (ident×region×(m_W M))
274      (match_var_entry M) vars1 vars2 →
275  nextblock … (\snd env_mem1) = nextblock … (\snd env_mem2) →
276  match_genv_t M vars
277    (\fst env_mem1) (\fst env_mem2) →
278  match_genv_t M vars
279    (\fst (add_globals … initV env_mem1 vars1))
280    (\fst (add_globals … initW env_mem2 vars2)).
281#M #init1 #init2 #vars1
282elim vars1 -vars1 [2: ** #id1 #r1 #v1 #tl1 #IH ]
283* [2,4: ** #id2 #r2 #v2 #tl2 ]
284#vars * #env1 #mem1 * #env2 #mem2 *
285[2: #_ #H @H ]
286#H inversion H #id' #r' #v1' #v2' #P #EQ1 #EQ2 #_ destruct -H #H
287#EQnxtbl #G @(IH tl2 … H)
288cases mem1 in EQnxtbl; -mem1 #mem1 #nbl1 #prf1
289cases mem2 -mem2 #mem2 #nbl2 #prf2 #EQ destruct
290[ % ]
291normalize nodelta %
292whd in match add_symbol;
293whd in match drop_fn; normalize nodelta
294[ >(symbols_eq … G) %
295| @(nextfunction_eq … G)
296| >(symbols_eq … G) cases (lookup ? block ??) normalize nodelta
297  [2: ** [2,3: #p] normalize nodelta ]
298  try @pm_P_set_None
299  @(functions_match … G)
300]
301qed.
302
303lemma add_functs_match :
304  ∀M : matching.
305  ∀vars.
306  ∀functs1,functs2.
307(*  let vars1' ≝ map … (λx.\fst (\fst x)) vars1 in
308  let vars2' ≝ map … (λx.\fst (\fst x)) vars2 in *)
309  ∀env1 : genv_t (m_A M vars).
310  ∀env2 : genv_t (m_B M vars).
311  All2 …
312    (match_funct_entry M vars vars) functs1 functs2 →
313  match_genv_t M vars env1 env2 →
314  match_genv_t M vars
315    (add_functs … env1 functs1)
316    (add_functs … env2 functs2).
317#M #vars #functs1 elim functs1 -functs1 [2: * #id1 #f1 #tl1 #IH ]
318* [2,4: * #id2 #f2 #tl2 ]
319#env1 #env2 *
320[2: #H @H ]
321#H
322cut (id1 = id2 ∧ match_fundef M … f1 f2)
323[ @(match_funct_entry_inv M ??????? H) #v #i #f1 #f2 #H %{H} % ]
324* #EQ destruct #Pf1f2 #Ptl1tl2 #G
325lapply (IH … Ptl1tl2 G) -G #G
326%
327whd in
328  match (add_functs ?? (? :: tl1));
329whd in
330  match (add_functs ?? (? :: tl2));
331change with (add_functs ?? tl1) in match (foldr ???? tl1);
332change with (add_functs ?? tl2) in match (foldr ???? tl2);
333whd in match drop_fn; normalize nodelta
334[ >(nextfunction_eq … G)  >(symbols_eq … G) %
335| >(nextfunction_eq … G) %
336| >(symbols_eq … G) cases (lookup ? block ??) normalize nodelta
337  [2: ** [2,3: #p] normalize nodelta ]
338  >(nextfunction_eq … G)
339  @(pm_P_insert … Pf1f2)
340  try @pm_P_set_None @(functions_match … G)
341]
342qed.
343
344lemma globalenv_match:
345    ∀M:matching.∀initV,initW.
346     (∀v,w. match_var_entry M v w →
347      size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) →
348    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
349    ∀MATCH:match_program … M p p'.
350    match_genv_t M ? (globalenv … initV p)
351      (globalenv … initW p' ⌈prog_var_names … p' ↦ prog_var_names … p⌉).
352[2: @sym_eq @(matching_vars … (mp_vars … MATCH)) ]
353* #A #B #V #W #Pf #Pv #iV #iW #init_eq
354* #vars1 #functs1 #main1
355* #vars2 #functs2 #main2
356*
357whd in match prog_var_names;
358normalize nodelta;
359#Mvars #Mfns #EQmain destruct
360lapply (sym_eq ????)
361#E
362lapply Mfns lapply functs2 -functs2
363whd in match globalenv; whd in match globalenv_allocmem;
364whd in match prog_var_names in E ⊢ %;
365normalize nodelta in E ⊢ %;
366>E normalize nodelta #functs2 #Mfns
367@add_globals_match [ assumption | % ]
368@add_functs_match [ assumption ]
369% try % #p %
370qed.
371
372lemma symbols_transf:
373 ∀A,B,V,init.∀prog_in : program A V.
374 ∀trans : ∀vars.A vars → B vars.
375 let prog_out ≝ transform_program … prog_in trans in
376 symbols … (globalenv … init prog_out) = symbols … (globalenv … init prog_in).
377#A #B #V #iV #p #tf whd
378lapply (transform_program_match … tf p)
379#MATCH
380>(symbols_eq … (globalenv_match … MATCH))
381[2: @iV |3: #v #w * // ]
382lapply (sym_eq ????)
383whd in match (prog_var_names ???); whd in match (prog_vars B ??);
384#E >(K ?? E) normalize nodelta %
385qed.
386
387lemma functions_transf:
388 ∀A,B,V,init.∀prog_in : program A V.
389 ∀trans : ∀vars.A vars → B vars.
390 let prog_out ≝ transform_program … prog_in trans in
391 ∀p.lookup_opt … p (functions … (globalenv … init prog_out)) =
392 option_map ?? (trans ?) (lookup_opt … p (functions … (globalenv … init prog_in))).
393#A #B #V #iV #p #tf #n
394lapply (transform_program_match … tf p)
395#MATCH
396whd in match globalenv; whd in match globalenv_allocmem;
397normalize nodelta
398lapply (functions_match … (globalenv_match … MATCH) n)
399[ @iV | @iV | #v #w * // ]
400lapply (sym_eq ????)
401whd in match (prog_var_names ???); whd in match (prog_vars B ??);
402#E >(K ?? E) normalize nodelta
403cases (lookup_opt ???) [2: #x ] normalize nodelta
404cases (lookup_opt ???) [2,4: #y ] normalize nodelta
405[ #EQ <EQ % |*: * % ]
406qed.
407
408lemma symbol_for_block_transf :
409 ∀A,B,V,init.∀prog_in : program A V.
410 ∀trans : ∀vars.A vars → B vars.
411 let prog_out ≝ transform_program … prog_in trans in
412 ∀bl.
413 symbol_for_block … (globalenv … init prog_out) bl =
414 symbol_for_block … (globalenv … init prog_in) bl.
415#A #B #V #iV #p #tf whd
416#bl
417whd in match symbol_for_block; normalize nodelta
418>(symbols_transf … tf) %
419qed.
420
421include alias "common/Pointers.ma".
422
423lemma fetch_function_transf :
424 ∀A,B,V,init.∀prog_in : program A V.
425 ∀trans : ∀vars.A vars → B vars.
426 let prog_out ≝ transform_program … prog_in trans in
427 ∀bl.
428 fetch_function … (globalenv … init prog_out) bl =
429 ! 〈i, f〉 ← fetch_function … (globalenv … init prog_in) bl ;
430 return 〈i, trans … f〉.
431#A #B #V #init #prog_in #trans #bl
432whd in match fetch_function; normalize nodelta
433>(symbol_for_block_transf A B V init prog_in trans)
434cases (symbol_for_block ???) [ % ] #id >m_return_bind >m_return_bind
435whd in match find_funct_ptr; normalize nodelta
436whd in match (block_region (pi1 ?? bl));
437cases (block_id (pi1 ?? bl)) [2,3: #p] normalize nodelta try %
438>(functions_transf A B V init prog_in trans p)
439cases (lookup_opt ???) //
440qed.
441
442lemma fetch_internal_function_transf :
443 ∀A,B,V,init.∀prog_in : program (λvars.fundef (A vars)) V.
444 ∀trans : ∀vars.A vars → B vars.
445 let prog_out ≝ transform_program … prog_in (λvars.transf_fundef … (trans vars)) in
446 ∀bl.
447 fetch_internal_function … (globalenv … init prog_out) bl =
448 ! 〈i, f〉 ← fetch_internal_function … (globalenv … init prog_in) bl ;
449 return 〈i, trans … f〉.
450#A #B #V #init #prog #trans #bl
451 whd in match fetch_internal_function; normalize nodelta
452>(fetch_function_transf … prog)
453cases (fetch_function ???)
454[ * #id * #f % | #e % ]
455qed.
456
457include alias "utilities/binary/positive.ma".
458
459lemma pm_map_add_ind : ∀A.∀P : positive_map A → Prop.
460(∀m.(∀p.lookup_opt A p m = None ?) → P m) →
461(∀m,p,v.P m → lookup_opt A p m = None ? → P (insert A p v m)) →
462∀m.P m.
463#A #P #H1 #H2 #m lapply H2 lapply H1 lapply P -P elim m -m
464[ #P #H1 #_ @H1 #p % ]
465#o #l #r #IHl #IHr #P #H1 #H2
466@IHl #l'
467[ #empty_l' @IHr #r'
468  [ #empty_r' cases o [ @H1 * try #p normalize // ]
469    #v change with (P (insert ? one v (pm_node ? (None ?) ??)))
470    @H2 [ @H1 * try #p normalize // | % ]
471  ]
472]
473#p #v #H #G
474[ change with (P (insert ? (p1 p) v (pm_node ? ???)))
475| change with (P (insert ? (p0 p) v (pm_node ? ???)))
476] @H2 assumption
477qed.
478
479include alias "basics/logic.ma".
480include alias "common/PositiveMap.ma".
481
482lemma swap_neg : ∀A,B : Prop.(A → B) → ¬B → ¬A.
483#A #B #impl * #Bf % #At @Bf @impl @At qed-.
484
485definition b_graph_transform_program_props ≝
486  λsrc,dst : sem_graph_params.
487  λdata,prog_in.
488  λinit_regs : block → list register.
489  λf_lbls : block → label → list label.
490  λf_regs : block → label → list register.
491   let prog_out ≝ b_graph_transform_program src dst data prog_in in
492   let src_genv ≝ joint_globalenv src prog_in in
493   let dst_genv ≝ joint_globalenv dst prog_out in
494  ∀bl,def_in.
495  block_id … bl ≠ -1 →
496  find_funct_ptr … src_genv bl = return (Internal ? def_in) →
497  ∃init_data,def_out.
498  find_funct_ptr … dst_genv bl = return (Internal ? def_out) ∧
499  bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧
500  b_graph_translate_props src dst ? init_data
501    def_in def_out (f_lbls bl) (f_regs bl).
502
503lemma make_b_graph_transform_program_props :
504 ∀src,dst:sem_graph_params.
505 ∀data : ∀globals.joint_closed_internal_function src globals →
506  bound_b_graph_translate_data src dst globals.
507 ∀prog_in : joint_program src.
508 let prog_out ≝ b_graph_transform_program … data prog_in in
509 let src_genv ≝ joint_globalenv src prog_in in
510 let dst_genv ≝ joint_globalenv dst prog_out in
511 ∃init_regs : block → list register.
512 ∃f_lbls : block → label → list label.
513 ∃f_regs : block → label → list register.
514 b_graph_transform_program_props src dst data prog_in init_regs f_lbls f_regs.
515cases daemon (* TOREDO
516#src #dst #data #prog_in
517whd in match b_graph_transform_program_props; normalize nodelta
518whd in match joint_globalenv; normalize nodelta
519letin prog_out ≝ (b_graph_transform_program … data prog_in)
520letin src_genv ≝ (globalenv … (λx.x) prog_in)
521letin dst_genv ≝ (globalenv … (λx.x) prog_out)
522cut (∀p.lookup_opt ? p (functions ? dst_genv) =
523     option_map ?? (transf_fundef … (λf.b_graph_translate … (data … f) f))
524      (lookup_opt ? p (functions ? src_genv)))
525[ @functions_transf ]
526cut (symbols ? dst_genv = symbols ? src_genv)
527[ @symbols_transf ]
528cases dst_genv #functs2 #nextf2 #symbols2 #H2
529cases src_genv #functs1 #nextf1 #symbols1 #H1 #EQ destruct
530lapply H2 lapply H1 lapply functs2
531@(pm_map_add_ind … functs1) -functs1 -functs2 #functs1
532[ #functs1_empty | #p #f #IH #p_not_in ]
533#functs2 #H1 #H2 #transf
534[ %{(λ_.[ ])} %{(λ_.λ_.[])} %{(λ_.λ_.[])}
535  #bl #def_in #ABS1 #ABS2 @⊥ lapply ABS2 -ABS2 lapply ABS1 -ABS1
536  whd in match find_funct_ptr;
537  whd in match find_symbol;
538  normalize nodelta
539  cases bl; * normalize nodelta
540  [2,3: #p ]
541  [1,3: #_ whd in ⊢ (???%→?); #EQ destruct ]
542  >lookup_add_hit
543  #H >lookup_opt_insert_miss
544  [2: @(swap_neg … H) #EQ >EQ % ]
545  whd in match drop_fn; normalize nodelta
546  cases (lookup … symbols1 pre_main_id)
547  normalize nodelta
548  [ >functs1_empty | ** [2,3: #p' ] normalize nodelta
549    [1,3: >functs1_empty
550    | @lookup_opt_pm_set_elim #H destruct
551      [2: >functs1_empty ]
552    ]
553  ] whd in ⊢ (???%→?); #EQ destruct
554]
555cases (IH (pm_set … p (None ?) functs2) ???)
556[|*: @hide_prf
557  [ #b #G @(H1 b ?) @(swap_neg … G) -G
558    whd in match insert; normalize nodelta
559    @lookup_opt_pm_set_elim
560    [ #EQ #ABS destruct ]
561    #NEQ #H @H
562  | #b #G @(H2 b ?) @(swap_neg … G) -G
563    @lookup_opt_pm_set_elim
564    [ #_ #_ % ]
565    #_ #H @H
566  | #b @lookup_opt_pm_set_elim
567    [ #EQ destruct >p_not_in % ]
568    #NEQ >transf
569    >(lookup_opt_insert_miss ? f b p … NEQ) %
570  ]
571]
572#init_regs * #f_lbls * #f_regs #props
573-IH cases f in H1 transf; -f #f #H1 #transf
574[ (* internal *)
575  letin upd ≝ (λA : Type[0].λf : block → A.
576    λid.λv,id'.
577    if eq_block id id' then v else f id')
578  cases (pi2 ?? (b_graph_translate … (data … f) f))
579  #loc_data * #loc_init_regs * #loc_f_lbls * #loc_f_regs *
580  #inst_loc_data #loc_props
581  letin bl ≝ (mk_block (neg p))
582  %{(upd … init_regs bl loc_init_regs)}
583  %{(upd … f_lbls bl loc_f_lbls)}
584  %{(upd … f_regs bl loc_f_regs)}
585| (* external, nothing changes *)
586  %{init_regs}
587  %{f_lbls}
588  %{f_regs}
589]
590* #p' #def_in
591whd in match find_funct_ptr; normalize nodelta
592whd in match (block_region (mk_block p'));
593cases p' -p' [2,3,5,6: #p' ] normalize nodelta
594[1,3,5,6: #_ #ABS normalize in ABS; destruct]
595whd in match find_symbol;
596whd in match insert; normalize nodelta
597#bl_prf
598@lookup_opt_pm_set_elim #pp' destruct
599[1,3: whd in ⊢ (??%%→?); #EQ destruct(EQ)
600  [ %{loc_data} %
601    [2: % [ % ]
602      [ >lookup_opt_insert_hit %
603      |*: >eq_block_b_b assumption
604      ]
605    |]
606|*: >(lookup_opt_insert_miss ???? functs1 … pp')
607  [ @eq_block_elim [ #EQ destruct cases (absurd ?? pp') % ] #_ normalize nodelta]
608  #EQ lapply (props (mk_block (neg p')) def_in EQ)
609  whd in match find_funct_ptr; normalize nodelta
610  >(lookup_opt_pm_set_miss … functs2 … pp') #H @H
611] *)
612qed.
613
614lemma b_graph_transform_program_fetch_internal_function :
615 ∀src,dst:sem_graph_params.
616 ∀data : ∀globals.joint_closed_internal_function src globals →
617  bound_b_graph_translate_data src dst globals.
618 ∀prog_in : joint_program src.
619 ∀init_regs : block → list register.
620 ∀f_lbls : block → label → list label.
621 ∀f_regs : block → label → list register.
622 b_graph_transform_program_props … data prog_in init_regs f_lbls f_regs →
623 let prog_out ≝ b_graph_transform_program … data prog_in in
624 let src_genv ≝ joint_globalenv src prog_in in
625 let dst_genv ≝ joint_globalenv dst prog_out in
626 ∀bl : Σbl.block_region … bl = Code.∀id,def_in.
627 block_id … bl ≠ -1 →
628 fetch_internal_function … src_genv bl = return 〈id, def_in〉 →
629 ∃init_data,def_out.
630 fetch_internal_function … dst_genv bl = return 〈id, def_out〉 ∧
631 bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧
632 b_graph_translate_props src dst ? init_data
633    def_in def_out (f_lbls bl) (f_regs bl).
634#src #dst #data #prog_in
635#init_regs #f_lbls #f_regs #props
636#bl #id #def_in #NEQ
637#H @('bind_inversion H) * #id' * #def_in' -H
638normalize nodelta #H whd in ⊢ (??%%→?); #EQ destruct
639@('bind_inversion (opt_eq_from_res … H)) -H #id' #EQ1
640#H @('bind_inversion H) -H #def_in' #H
641whd in ⊢ (??%%→?); #EQ destruct
642cases (props … NEQ H)
643#loc_data * #def_out ** #H1 #H2 #H3
644%{loc_data} %{def_out}
645%{H3} %{H2}
646whd in match fetch_internal_function;
647whd in match fetch_function; normalize nodelta
648cases daemon (* TOREDO
649>symbol_for_block_transf >EQ1 >m_return_bind
650>H1 % *)
651qed.
652
653lemma b_graph_transform_program_fetch_statement :
654 ∀src,dst:sem_graph_params.
655 ∀data : ∀globals.joint_closed_internal_function src globals →
656  bound_b_graph_translate_data src dst globals.
657 ∀prog_in : joint_program src.
658 ∀init_regs : block → list register.
659 ∀f_lbls : block → label → list label.
660 ∀f_regs : block → label → list register.
661 b_graph_transform_program_props … data prog_in init_regs f_lbls f_regs →
662 let prog_out ≝ b_graph_transform_program … data prog_in in
663 let src_genv ≝ joint_globalenv src prog_in in
664 let dst_genv ≝ joint_globalenv dst prog_out in
665 ∀pc,id,def_in,s.
666 block_id … (pc_block … pc) ≠ -1 →
667 fetch_statement … src_genv pc = return 〈id, def_in, s〉 →
668 ∃init_data,def_out.
669 let bl ≝ pc_block pc in
670 fetch_internal_function … dst_genv bl = return 〈id, def_out〉 ∧
671 bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧
672 let l ≝ point_of_pc dst pc in
673 ∃lbls,regs.
674 f_lbls bl l = lbls ∧
675 f_regs bl l = regs ∧
676  match s with
677  [ sequential s' nxt ⇒
678    let block ≝
679      if eq_identifier … (joint_if_entry … def_in) l then
680        append_seq_list … (f_step … init_data l s') (added_prologue … init_data)
681      else
682        f_step … init_data l s' in
683    l ~❨block, l::lbls, regs❩~> nxt in joint_if_code … def_out
684  | final s' ⇒
685    l ~❨f_fin … init_data l s', l::lbls, regs❩~> it in joint_if_code … def_out
686  | FCOND abs _ _ _ ⇒ Ⓧabs
687  ].
688#src #dst #data #prog_in
689#init_regs #f_lbls #f_regs #props
690#pc #id #def_in #s #NEQ
691#H @('bind_inversion H) * #id' #def_in' -H
692#EQfif
693#H @('bind_inversion H) -H #s
694#H lapply (opt_eq_from_res ???? H) -H
695#EQstmt_at whd in ⊢ (??%%→?); #EQ destruct
696cases (b_graph_transform_program_fetch_internal_function … props … NEQ EQfif)
697#a * #b ** #H1 #H2 #H3 %{a} %{b} %
698[ %{H1 H2}
699| % [2: % [2: % [% %]] | skip] @(multi_fetch_ok … H3 … EQstmt_at) ]
700qed.
701
702lemma b_graph_transform_program_fetch_statement_plus :
703 ∀src,dst:sem_graph_params.
704 ∀data : ∀globals.joint_closed_internal_function src globals →
705  bound_b_graph_translate_data src dst globals.
706 ∀prog_in : joint_program src.
707 ∀init_regs : block → list register.
708 ∀f_lbls : block → label → list label.
709 ∀f_regs : block → label → list register.
710 b_graph_transform_program_props … data prog_in init_regs f_lbls f_regs →
711 let prog_out ≝ b_graph_transform_program … data prog_in in
712 let src_genv ≝ joint_globalenv src prog_in in
713 let dst_genv ≝ joint_globalenv dst prog_out in
714 ∀pc,id,def_in,s.
715 block_id … (pc_block … pc) ≠ -1 →
716 fetch_statement … src_genv pc = return 〈id, def_in, s〉 →
717 ∃init_data,def_out.
718 let bl ≝ pc_block pc in
719 fetch_internal_function … dst_genv bl = return 〈id, def_out〉 ∧
720 bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧
721 let l ≝ point_of_pc dst pc in
722 ∃lbls,regs.
723 f_lbls bl l = lbls ∧
724 f_regs bl l = regs ∧
725 joint_if_entry … def_out = joint_if_entry … def_in ∧
726 partial_partition … (f_lbls bl) ∧
727 partial_partition … (f_regs bl) ∧
728 (∀l.All …
729    (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧
730           fresh_for_univ … lbl (joint_if_luniverse … def_out)) (f_lbls bl l)) ∧
731  (∀l.All …
732    (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧
733           fresh_for_univ … reg (joint_if_runiverse … def_out)) (f_regs bl l)) ∧
734  match s with
735  [ sequential s' nxt ⇒
736    let block ≝
737      if eq_identifier … (joint_if_entry … def_in) l then
738        append_seq_list … (f_step … init_data l s') (added_prologue … init_data)
739      else
740        f_step … init_data l s' in
741    l ~❨block, l::lbls, regs❩~> nxt in joint_if_code … def_out
742  | final s' ⇒
743    l ~❨f_fin … init_data l s', l::lbls, regs❩~> it in joint_if_code … def_out
744  | FCOND abs _ _ _ ⇒ Ⓧabs
745  ].
746#src #dst #data #prog_in
747#init_regs #f_lbls #f_regs #props
748#pc #id #def_in #s #NEQ
749#H @('bind_inversion H) * #id' #def_in' -H
750#EQfif
751#H @('bind_inversion H) -H #s
752#H lapply (opt_eq_from_res ???? H) -H
753#EQstmt_at whd in ⊢ (??%%→?); #EQ destruct
754cases (b_graph_transform_program_fetch_internal_function … props … NEQ EQfif)
755#a * #b ** #H1 #H2 #H3 %{a} %{b} %
756[ %{H1 H2}
757| %
758   [2:
759      %
760        [2: %
761            [%
762               [%
763                  [%
764                     [%
765                        [%
766                           [%
767                              %
768                            | @(entry_eq … H3)
769                            ]
770                        | @(partition_lbls … H3)
771                        ]
772                     |  @(partition_regs … H3)
773                     ]
774                  | @(freshness_lbls … H3)
775                  ]
776               |  @(freshness_regs … H3)
777               ]
778            |  @(multi_fetch_ok … H3 … EQstmt_at)
779            ]
780        |
781        ]
782   |
783   ]
784]         
785qed.
Note: See TracBrowser for help on using the repository browser.