source: src/joint/semanticsUtils.ma @ 2940

Last change on this file since 2940 was 2843, checked in by piccolo, 7 years ago

1) Fixed a litte bug in Joint.ma
2) ERTL to ERTLptr correctness proof in place

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